Rework BufferedRandomAccessFile

This commit makes major alterations to `BufferedRandomAccessFile` to
bring it in line with the general `RandomAccessFile` contract:

 - Invariant V1 has been strengthened to include a contract for the
   `length` and `diskPos` fields.

 - Invariants V2-V5 have been altered to account for cases where
   `curr > length`, which the `RandomAccessFile` contract allows.

 - Additionally, invariant V5 has been adjusted to clarify that
   `dirty=true` does not imply that there are unflushed bytes.  The
   implication is only one-way: if there are unflushed bytes, then
   `dirty=true`.

 - The `hi` and `maxHi` fields have been removed.  These largely
   duplicate information that can be quickly recomputed, meaning they
   add additional complexity to the class invariants.  Without those
   fields, invariant V6 can be removed.

 - The `close()` method now closes the underlying file descriptor even
   if `flush()` throws an exception.

Due to the complexity of this change, I have added a TLA+ specification
for `BufferedRandomAccessFile` to enable model checking of its design.

To ensure that the code is correct, this commit also adds a substantial
amount of test infrastructure:

 - Several new regression tests have been added.  These are a little
   cryptic because they were randomly generated, but they do reflect
   true behaviors of the `RandomAccessFile` contract.

 - A fuzz test has been added.  This test ensures that many sequences
   of random operations behave correctly.  It also minimizes failures
   so they can be easily converted to regression tests.

This commit also makes some whitespace and formatting adjustments.

Fixes #835.  I have verified that the tests now pass under Java 21.

Signed-off-by: Calvin Loncaric <calvin.loncaric@oracle.com>