This adds a logic-level version of `gmap_view`

, dubbed `ghost_map`

(in parallel to the existing `ghost_var`

). The API mirrors that of `gen_heap`

. I think this also provides everything Perennial's `auth_map`

has, except for operations on "fragment maps" (for which we lack good support in `gmap_view`

). Cc @tchajed

This seems like something with many possible uses, so I went for full sealing and also added a notation for the elements: `k ↪[γ]{dq} v`

. Obviously, notation and naming are up for bikeshedding. Also for now this library enforces Leibniz equality, but I feel it might be worth supporting `Equiv`

(but it would probably help -- for client usability -- to not support arbitrary OFEs).

The notation follows @robbertkrebbers's proposal of using the shortest, "most desirable" notation for the general case of a discardable fraction, and using `k ↪[γ]{#q} v`

for `q: frac`

. I could also imagine doing this the other way around, i.e., letting `#`

indicate `dfrac`

. General lemmas should be written for `dfrac`

whenever possible, but clients that actually split this fraction will likely work with `1/2`

and `1/4`

and would have to add a `#`

everywhere currently.

Fixes #358 (closed)