Finite separation logic

Fix a countably infinite variable set $V$; each scoped program and derivation mentions only finitely many variables. The states of chapter 44 contain a total store $\sigma :V\to \mathsf{Val}$ and a finite partial heap. Assertions have exact points-to, Boolean operations, separating conjunction and implication, and existentials. The loop-free command language has the six heap/store commands, sequencing, and equality conditionals; allocation chooses a fresh non-null location.

Safety is defined structurally and distinguishes a fault from absence of a big-step derivation. Every displayed command is local: adding a disjoint frame preserves safety and every result factors into the changed footprint and the unchanged frame (theorem 44.11).

Triples mean partial correctness plus fault freedom. The frame theorem is theorem 44.13, with its necessary store-variable side condition; all displayed proof rules are sound by theorem 44.16. Assertion substitution and fresh-variable coincidence are lemma 44.14, lemma 44.9; the latter is the explicit semantic dependency of H-Exists. Each linked-chain operation changes one cell.

The pinned DeepSpec Software Foundations revision is b86f18667e88828b348bcd31458dfbedcf3ae3c0, volume slf-current. Separating conjunction is Hprop.v, lines 134–140; triple and triple_conseq_frame are Triples.v, lines 620–622 and 705–709; its soundness connection is lines 1294–1299. Primitive declarations triple_ref, triple_free, triple_get, and triple_set are in Rules.v, lines 445–535. The linked predicate MList and its unfolding lemma are Repr.v, lines 93–96 and 135–140; the linked append specification is lines 183–187. This is a read-only source-declaration replay. In this archived teaching tree, triple_conseq_frame, triple_free’, triple_set, and MList_if are Admitted exercises, so their statements are not counted as mechanized proof evidence. In particular, SLF uses a total-correctness omni-big-step triple, returns command values, and stores a data field in each MList node; none of those signatures is silently transferred to the book calculus.

No theorem gives loop termination, race or leak freedom, an ownership type system, or a concurrent frame rule. A semantic heap split is not by itself program authority.

Appendix E’s pinned Kappa corpus runs framed update, allocation/deallocation, chain push/pop, use-after-free, and alias rejection. It is implementation evidence, not a proof of locality or Hoare soundness.