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.