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: gen_heap, proph_map, and the invariant gmap in 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)