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.