Library iris.base_logic.lib.gen_heap

This file provides a generic mechanism for a language-level point-to connective l ↦{dq} v reflecting the physical heap. This library is designed to be used as a singleton (i.e., with only a single instance existing in any proof), with the gen_heapGS typeclass providing the ghost names of that unique instance. That way, pointsto does not need an explicit gname parameter. This mechanism can be plugged into a language and related to the physical heap by using gen_heap_interp σ in the state interpretation of the weakest precondition. See heap-lang for an example. If you are looking for a library providing "ghost heaps" independent of the physical state, you will likely want explicit ghost names to disambiguate multiple heaps and are thus better off using ghost_map, or (if you need more flexibility), directly using the underlying algebra.lib.gmap_view. This library is generic in the types L for locations and V for values and supports fractional permissions. Next to the point-to connective l ↦{dq} v, which keeps track of the value v of a location l, this library also provides a way to attach "meta" or "ghost" data to locations. This is done as follows:

• When one allocates a location, in addition to the point-to connective l ↦ v, one also obtains the token meta_token l ⊤. This token is an exclusive resource that denotes that no meta data has been associated with the namespaces in the mask ⊤ for the location l.
• Meta data tokens can be split w.r.t. namespace masks, i.e. meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2 if E1 ## E2.
• Meta data can be set using the update meta_token l E ==∗ meta l N x provided ↑N ⊆ E, and x : A for any countable A. The meta l N x connective is persistent and denotes the knowledge that the meta data x has been associated with namespace N to the location l.

To make the mechanism as flexible as possible, the x : A in meta l N x can be of any countable type A. This means that you can associate e.g. single ghost names, but also tuples of ghost names, etc. To further increase flexibility, the meta l N x and meta_token l E connectives are annotated with a namespace N and mask E. That way, one can assign a map of meta information to a location. This is particularly useful when building abstractions, then one can gradually assign more ghost information to a location instead of having to do all of this at once. We use namespaces so that these can be matched up with the invariant namespaces. To implement this mechanism, we use three pieces of ghost state:

• A ghost_map L V, which keeps track of the values of locations.
• A ghost_map L gname, which keeps track of the meta information of locations. More specifically, this RA introduces an indirection: it keeps track of a ghost name for each location.
• The ghost names in the aforementioned authoritative RA refer to namespace maps reservation_map (agree positive), which store the actual meta information. This indirection is needed because we cannot perform frame preserving updates in an authoritative fragment without owning the full authoritative element (in other words, without the indirection meta_set would need gen_heap_interp as a premise).

The CMRAs we need, and the global ghost names we are using.

TODO: The use of positives_flatten violates the namespace abstraction (see the proof of meta_set.

General properties of pointsto

Almost all the time, this is all you really need.

Permanently turn any points-to predicate into a persistent points-to predicate.

Recover fractional ownership for read-only element.

Framing support

General properties of meta and meta_token

Update lemmas

This variant of gen_heap_init should only be used when absolutely needed. The key difference to gen_heap_init is that the inG instances in the new gen_heapGS instance are related to the original gen_heapGpreS instance, whereas gen_heap_init forgets about that relation.