Garbage collection problem

Background: In separation logic we can make the assertion x → a, meaning “the variable x contains the address of a heap cell that contains the value a and that’s the only cell in the heap,” P ⋆ Q, meaning “we can partition the heap into a part where P holds and one where Q holds,” and emp, meaning “the heap is empty.” Just as we have rules that tell us how to manipulate formulas that contain ∧, ∨, and so on, we also have rules that tell us how to manipulate formulas that contain → and ⋆ without necessarily thinking about the meaning.

• x → _ ⋆ x → _ = ⊥, in other words x can’t point to two locations
• (P ∧ Q) ⋆ R = P ∧ (Q ⋆ R) if P is a pure assertion; an assertion is pure when it doesn’t say anything about the heap; that is, it does not contain ⋆, →, or emp.

We say that P is an intuitionistic assertion when P ⋆ ⊤ ⇒ P. In other words, if it is true for a heap, then it is also true for extended heaps. We say that P is a supported assertion when P ∧ (P ⋆ Q) ∧ (P ⋆ Q′) only if there exist R and R′ such that Q = P ⋆ R and Q′ = P ⋆ R′. In other words, if it holds in the current heap then there is a smallest subheap in which it holds. (A heap h is smaller than a heap h′ when h ⊆ h′.)

Conjecture [Matthew Parkinson, FIRST fall school on logics and semantics of state, 2008]: Show that if an assertion is intuitionistic and supported and holds in the current heap then it also holds in the garbage collected heap. (The garbage collected heap retains only the cells reachable from the stack.)

Problem: True or false?

Intuitionistic and supported properties P obey:

((P ∧ ¬(P ⋆ ¬emp)) ⋆ ⊤) ⇒ P

The lecture notes of Reynolds provide a more precise presentation of separation logic and many properties that may be useful in answering the problem.