Some progress on specs and proofs for Bmap allocator cache. It is surprising that cancel in [alloc_ok] doesn't handle some of the obligations.
Some progress on specs and proofs for Bmap allocator cache.
It is surprising that cancel in [alloc_ok] doesn't handle some of the obligations.

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