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.