## Add persistent points-to predicate to Iris

This is the same as !493 (closed) but based on !486 (merged). The overall description in !493 (closed) still applies.

### Notation

As in the previous MR I've used the notation `l ↦□ v`

for the new persistent points-to predicate and changed the notation used by `gen_inv_heap`

. In the original MR description I argued for this choice and @jung replied with some additional arguments to consider. I think the conclusion is that using `l ↦□ v`

for the persistent points-to predicate is a good idea but that we need to come up with some other notation for `gen_inv_heap`

than what currently is in this MR.