Implement fast read_bytes on top of bf_read_range
Implement fast read_bytes on top of bf_read_range

Proof is complete except for the in-bounds obligation, which should be
the same as a part of the update_bytes_ok proof.

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