This adds a library for a separation logic view onto a
gmap K V, alongside appropriate lemmas. The library supports both standard fractional mutable heap elements as well as persistent read-only elements.
This is inspired by @tchajed's library in Perennial, but since I wanted it to work on the level of RAs (not Iris), I ended up re-doing the interface (copying the proofs from
gen_heap where possible). I think @tchajed's interface should be implementable on top of this; it would be nice to confirm this before landing. I ported everything fitting this pattern to the new interface:
proph_map, and the invariant
wsat -- and indeed it removed all the annoying update/validity/map reasoning.
Main topic to bikeshed are the names, which are getting awfully long.
Fixes #328 (closed)