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:

- 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. - 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.