WIP: Add persistent points-to predicate to Iris

This MR adds a persistent points-to predicate, l ↦□ v, denoting that l points to v and that this never changes. The predicate l ↦□ v can be used much like a normal points to predicate (it works with the wp_load tactic, has agreement with other points-to predicates, etc.) except that it does not permit changing the value stored at l. In other words l ↦□ v it gives read-only access to l.

The persistent points-to predicate is useful for immutable data-structures that use pointers and for locations that at some point arrive at a final value after which they never change. At that point one can turn a normal points-to predicate into a persistent one by using the lemma:

Lemma mapsto_persist l q v : l ↦{q} v ==∗ l ↦□ v.

The intuition behind this lemmas is: It takes the entire points-to predicate to change the value at a location. Hence if one discards ownership of any fraction of a points-to predicate, the location can never be changed, and one can therefore in return get the persistent knowledge that the location will never change.

Implementation

This has been implemented by changing the RA used by gen_heap. The main challenge is to support the lemma mapsto_persist, due to the following:

1. It requires that one can make a frame preserving update from the ghost state owned by l ↦{q} v to the ghost state owned by l ↦□ v. The former must have no core while the latter should.
2. Since Auth only supports making frame preserving updates in fragments while also having the authoritative view and since the lemma does not have the authoritative view (it's in gen_heap_ctx) l ↦{q} v can't be a fragment in Auth.

To solve the first problem the MR introduces the discardable fractions RA. This is a generalisation of the fractional RA where elements can represent both ownership of a fraction and the knowledge that a fraction has been discarded. One can make a frame preserving update from owning a fraction q to knowing that q has been discarded.

To solve the second problem a slight generalisation of the authoritative RA is introduced. In this generalisation the authorative and fragment can contain different types, A and B respectively. The RA is then indexed by a projection π : B -> B and for ◯ b ⋅ ● a, in the definition of validity, b ≼ a is changed to π b ≼ a. In other words, in the normal authoritative RA values in fragments has to be included in the value in the authoritative view. However, in this generalisation only a part of the fragment, projected out by π needs to be included. The other part which π does not pick out, can exist independently from the authoritative element and frame preserving updates to this part is possible without having the authoritative element (shown in the lemma pauth_frag_update). For this to work π must be a monoid monomorphism.

Notation

The notation l ↦□ v is currently used by gen_inv_heap. I think the notation is very well suited to the persistent points-to predicate and from the discussion in !289 (merged) it doesn't seem like there was a strong preference towards using that particular notation for gen_inv_heap. I've therefore opted to use l ↦□ v for the persistent points-to predicate and change the notation used by gen_inv_heap. I actually think the new notation for gen_inv_heap is better. It currently uses the notation l ↦□ I for a location that points to anything satisfying I and the notation l ↦_I v for a location pointing to v and satisfying I. I've changed the former to l ↦_I -. IMO the new notation has two advantages: 1/ It adds commonality to the two notations making it clear that they are related. 2/ The use of the dash - is consistent with l ↦ - and hence makes it more obvious what the notion means.

Remaining work

The code is not particularly polished. In particular the new RAs, which I'm not sure in what direction to take. They're both generalisation of existing RAs. So they could replace those RAs.

But, Frac is defined with Qp directly as the carrier, and this can't be done for DFrac. So I don't think DFrac can replace Frac in a backwards-compatible manner. Maybe they should live side by side?

Additionally, the generalisation of Auth may not be the "best"/most general, #257 (closed) seems to propose something more general. Maybe PAuth should be included only as an internal RA until #257 (closed) is implemented? Or maybe #257 (closed) should be implemented right away? (I'm not sure how much work that is).

Extending this to work for locations pointing to arrays still needs to be done.