ch:separation-logic: ch:separation-logic
Problem and result. Implement the finite store, heap, command evaluator, and exact footprint predicates used by the chapter. The five grouped cases accept framed update, allocate–free, and exact-chain push–pop behavior, while reporting a use-after-free fault and rejecting an aliased separating conjunction.
Invariant. Maintain four conditions after every evaluator step: heap union is defined only for disjoint domains; a missing load, store, or free address produces a fault rather than a default; allocation chooses an address outside the current domain; and points-to and chain predicates check their exact footprint size as well as stored values.
Representation. Represent heaps as finite partial maps with an explicit disjoint-union check, and return either a state or a named fault from command evaluation. Represent points-to and exact chains as decidable predicates. A total map with a default null value would simplify lookup, but would erase the semantic distinction between stored null and an unallocated address.
First complete version. Implement lookup, update, allocation at a fresh address, and deallocation. Check singleton points-to exactly: both the stored value and the one-cell footprint matter. Run the framed update before adding list-shaped heaps.
Remaining cases. Add an exact two-cell chain, push, and pop, preserving distinct addresses and the final footprint. Then evaluate load after free and the aliased two-cell candidate so the evaluator and separating-conjunction checker expose different failure modes.
A failing version. Return null when heap lookup misses. The module still typechecks and audits cleanly, but the use-after-free case becomes an ordinary value and the frozen oracle rejects it.
Acceptance test. Run check, test, run, and audit from appendix E. Require the exact five-case summary, the named fault, alias rejection, mutation rejection, and audit output [].
Mathematical boundary. The executor illustrates the command semantics of definition 44.6 and the exact-footprint predicate of definition 44.18. It does not prove locality (theorem 44.11), the frame theorem (theorem 44.13), Hoare soundness (theorem 44.16), leak freedom, ownership safety, or termination.