Add mostly-proven read_range function
Add mostly-proven read_range function

This can be used to implement BFILE.shrink more efficiently by only
retrieving the blocks that are being removed instead of those for the
entire file. The proof is complete except for a bit of slogging through
list rewrites that is left as an exercise to the reader.

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