Start working on a different chunking scheme
Start working on a different chunking scheme

Rather than breaking a write into all of its chunks and then applying
them, split it into three parts: preamble, full chunks, and postscript.
Each part covers some range of bytes that is easy to express, so that
the loop invariant for writing the full chunks is simple. Then
update_range just needs to show it writes all the bytes.

So far I have preamble and postscript functions to construct the
trickier first/last chunks, as well as theorems saying what bytes they
cover, where the coverage of a chunk is basically [blocknum*blocksize +
boff, blocknum*blocksize + bend). Full chunks have boff = 0 and bend =
blocksize.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl