ch:separation-logic: ch:separation-logic

Suppose $\sigma ,h\vDash P\ast (Q\vee R)$. Choose $h=h_1\uplus h_2$ with $P$ on $h_1$ and $Q\vee R$ on $h_2$. If the left disjunct holds on $h_2$, the same split witnesses $P\ast Q$; otherwise it witnesses $P\ast R$. Thus the right-hand disjunction holds. Conversely, a witness split for either $P\ast Q$ or $P\ast R$ is also a split for $P\ast (Q\vee R)$ after the corresponding disjunction introduction.

No state satisfies $P\ast \mathsf{false}$: its defining split would require one component to satisfy $\mathsf{false}$. Hence $P\ast \mathsf{false}\vDash \mathsf{false}$. The converse entailment is vacuous because $\mathsf{false}$ has no states. Together these arguments give both requested equivalences without appealing to the main-line separating algebra proposition.

Assume a state satisfies the antecedent and put $\ell =\sigma (x)=\sigma (y)$. The separating conjuncts would require a split $h=h_1\uplus h_2$ with $$h_1=\{\ell \mapsto 1\},h_2=\{\ell \mapsto 2\}.$$ Their domains both contain $\ell$, contradicting the disjointness required for $\uplus$. Hence the antecedent has no model and entails $\mathsf{false}$.

For the ordinary conjunction, take a store with $\sigma (x)=\sigma (y)=\ell$ and the singleton heap $h=\{\ell \mapsto 1\}$. Both exact points-to assertions inspect the same whole heap, so $\sigma ,h\vDash x=y\wedge x\mapsto 1\wedge y\mapsto 1$. The assertion $x\mapsto 1$ already describes ownership of that one-cell heap. Conjoining the same exact assertion under an alias does not create a second ownership claim; separating conjunction is the connective that demands disjoint footprints.

Write $\ell =[[E{]]}_{\sigma }$. For safety monotonicity, suppose $\mathsf{free}(E)$ is safe on $(\sigma ,h_0)$ and $h_0\mathrm{\#}r$. Safety gives $\ell \in \mathrm{dom}(h_0)$, hence also $\ell \in \mathrm{dom}(h_0\uplus r)$; rule E-Free therefore applies to the larger heap.

For factorization, a large execution has result $$H=(h_0\uplus r)\upharpoonright (\mathrm{dom}(h_0\uplus r)\setminus \{\ell \}).$$ Disjointness gives $\ell \notin \mathrm{dom}(r)$. Put $h_0^{\prime }=h_0\upharpoonright (\mathrm{dom}(h_0)\setminus \{\ell \})$. The small execution is $$⟨\mathsf{free}(E),\sigma ,h_0⟩\Downarrow ⟨\sigma ,h_0^{\prime }⟩,$$ and the domains calculate as $$\mathrm{dom}(h_0^{\prime })=\mathrm{dom}(h_0)\setminus \{\ell \},\mathrm{dom}(H)=(\mathrm{dom}(h_0)\setminus \{\ell \})\cup \mathrm{dom}(r).$$ Consequently $h_0^{\prime }\mathrm{\#}r$ and $H=h_0^{\prime }\uplus r$, which are exactly the two conclusions of the factorization clause.

Deleting the side condition would let us frame $R:=x=1$ around $$\{\mathsf{true}\}x:=0\{x=0\}$$ and derive $$\{\mathsf{true}\ast (x=1)\}x:=0\{(x=0)\ast (x=1)\}.$$ Take $\sigma (x)=1$ and $h=\varnothing$. Splitting the empty heap into two empty heaps shows that the precondition holds. Execution produces the store ${\sigma }^{\prime }=\sigma [x\mapsto 0]$. The postcondition would require both ${\sigma }^{\prime }(x)=0$ and ${\sigma }^{\prime }(x)=1$, so it is false. In the proof of theorem 44.13, the invalid step is the appeal to lemma 44.8 to conclude ${\sigma }^{\prime },r\vDash R$: here $x\in \mathrm{mod}(x:=0)\cap \mathrm{fv}(R)$.

The small-footprint axiom is H-Store: $$⊢\{E\mapsto -\}[E]:=F\{E\mapsto F\}.$$ Frame $R:=z\mapsto 7$. The command modifies no store variable, so $\mathrm{mod}([E]:=F)=\varnothing$ and therefore $$\mathrm{mod}([E]:=F)\cap \mathrm{fv}(R)=\varnothing .$$ Rule H-Frame gives exactly $$⊢\{E\mapsto -\ast z\mapsto 7\}[E]:=F\{E\mapsto F\ast z\mapsto 7\}.$$ No syntactic freshness hypothesis is needed. The two starred factors in the precondition supply disjoint singleton heaps, and hence distinct addresses; the frame-rule side condition concerns modified store variables only and is automatic because this heap-store command has an empty modified-variable set.

With ordinary conjunction, the proposed precondition is $x\mapsto a\wedge y\mapsto b$. Because points-to is exact, its first conjunct forces the whole heap to be $\{\sigma (x)\mapsto [[a{]]}_{\sigma }\}$ and its second forces the same whole heap to be $\{\sigma (y)\mapsto [[b{]]}_{\sigma }\}$. It is satisfiable exactly when the two singleton maps are equal, hence when $$\sigma (x)=\sigma (y)\ne \mathsf{null}\text{and}[[a{]]}_{\sigma }=[[b{]]}_{\sigma }.$$ It never describes two distinct cells, so it cannot replace the starred precondition of proposition 44.17.

For an inexact global predicate, $x\mapsto a$ would merely assert that the heap contains the indicated entry. Two such conjuncts can then hold in a larger heap, but when $a=b$ they can also both name the same cell. The swap proof would therefore need the explicit premise $x\ne y$; the separating conjunction obtains that fact from disjointness instead.

Choose the temporary $z$ distinct from $x$, as required by proposition 44.21. Instantiate that proposition first at $n+1$ and then at $n$: $$\begin{array}{r}⊢\{{\mathsf{chain}}_{n+2}(x)\}\mathsf{pop}\{{\mathsf{chain}}_{n+1}(x)\},\\ ⊢\{{\mathsf{chain}}_{n+1}(x)\}\mathsf{pop}\{{\mathsf{chain}}_n(x)\}.\end{array}$$ One use of H-Seq yields $$⊢\{{\mathsf{chain}}_{n+2}(x)\}\mathsf{pop};\mathsf{pop}\{{\mathsf{chain}}_n(x)\}.$$ The smallest admissible value is $n=0$: the input then has exactly two cells and the result has length zero, namely an empty heap with $x=\mathsf{null}$.

Choose the outer separating split $h=h_1\uplus h_2$ with ${\mathsf{chain}}_n(x)$ on $h_1$ and ${\mathsf{chain}}_m(y)$ on $h_2$. By lemma 44.19, $|\mathrm{dom}(h_1)|=n$ and $|\mathrm{dom}(h_2)|=m$. The domains are disjoint, so finite-set cardinality gives $$|\mathrm{dom}(h)|=|\mathrm{dom}(h_1)|+|\mathrm{dom}(h_2)|=n+m.$$ If , the same lemma puts $\sigma (x)$ in the first domain and $\sigma (y)$ in the second. Disjointness of those domains therefore implies $\sigma (x)\ne \sigma (y)$. This last inference is the load-bearing use of the outer star; the two individual chain facts alone do not compare their heads.

Suppose a satisfiable precondition $P$ made the displayed sequence safe, and choose $\sigma ,h\vDash P$. Put $\ell =\sigma (x)$. Safety of the first command requires $\ell \in \mathrm{dom}(h)$, and E-Free produces $h^{\prime }=h\upharpoonright (\mathrm{dom}(h)\setminus \{\ell \})$. The store is unchanged, so the following load again asks for address $\ell$. But $\ell \notin \mathrm{dom}(h^{\prime })$; no load rule applies and the sequence faults. This contradicts validity of a Hoare triple with precondition $P$.

Proof-theoretically, H-Free consumes the small-footprint premise $x\mapsto -$ and returns $\mathsf{emp}$ on that footprint. The second premise of H-Seq would have to establish the points-to precondition $x\mapsto F$ required by H-Load; neither $\mathsf{emp}$ nor a frame disjoint from the freed cell can entail it. An intervening allocation can repair the derivation by executing $x:=\mathsf{alloc}(v)$, which changes $x$ to a freshly chosen location and establishes a new assertion $x\mapsto v$ before the load. Nondeterministic freshness does not promise reuse of the old location; safety follows because the program follows the new value of $x$.

Rule H-Alloc gives $$⊢\{\mathsf{emp}\}x:=\mathsf{alloc}(0)\{x\mapsto 0\}.$$ The postcondition entails $\mathsf{true}$, so consequence gives the same command the postcondition $\mathsf{true}$. Rule H-Assign, instantiated with the postcondition $\mathsf{true}$, gives $$⊢\{\mathsf{true}\}x:=\mathsf{null}\{\mathsf{true}\}.$$ Sequence therefore derives $$⊢\{\mathsf{emp}\}x:=\mathsf{alloc}(0);x:=\mathsf{null}\{\mathsf{true}\}.$$ This does not contradict proposition 44.22: the program does not fault, and $\mathsf{true}$ intentionally forgets the final heap.

A postcondition that exposes the leak is $$\mathrm{\exists }\ell .x=\mathsf{null}\wedge \ell \mapsto 0.$$ The existential remembers that the final heap is exactly one allocated cell, while the only command-visible root $x$ no longer retains its location. Thus the stronger assertion records the unreachable allocation in the stated one-root sublanguage even though the weaker valid triple hides it.

The comparison is statement by statement. SLF’s triple_conseq_frame combines consequence with an arbitrary separating frame, matching the composition of H-Conseq and H-Frame. Its triple_ref, triple_free, triple_get, and triple_set respectively match the one-cell footprints of H-Alloc, H-Free, H-Load, and H-Store. The exact archived file ranges are recorded in appendix D.

Three signature mismatches prevent literal identification. SLF’s triple is total correctness in an omni-big-step semantics, whereas definition 44.12 is fault freedom plus partial correctness. SLF commands return values in a postcondition family; the book’s load and allocation commands instead update named store variables. Finally, one unfolding of MList separates a record cell containing both data and a tail pointer from the recursive tail, whereas one unfolding of ${\mathsf{chain}}_{n+1}$ separates a single next-pointer cell from an exact-length tail. The common disjoint head–tail pattern explains the comparison; it does not identify the node layouts.

Consequently the archived declarations are independent comparison evidence. They cannot prove theorem 44.11, theorem 44.16, whose statements refer to the book’s different commands, store updates, and partial-correctness triple.