Separation Logic

C*‘s assertions are separation-logic assertions, and in C* separation logic is not a fixed notation supported by a black-box solver: it is a shallow embedding inside HOL Light, built in three layers, each of which this part specifies as it is actually implemented in the proof kernel.

The bottom layer is a concrete memory model. Memory is a total function from addresses to memory cells, mem = addr -> mem_varmem = addr -> mem_var, where a cell is in one of three states: no permission, allocated but uninitialized, or initialized with one byte. Addresses and bytes are both integers, so the model is byte-granular and address arithmetic is integer arithmetic. Splitting memory is expressed by a three-place relation mem_join m1 m2 mmem_join m1 m2 m rather than by a partial operation.

The middle layer is the assertion language. An assertion is literally a predicate over memories: hprophprop abbreviates :mem->bool:mem->bool. Every connective — ****, -*-*, &&&&, ||||, -->-->, existsexists, forallforall, empemp, purepure, factfact, truetrue, falsefalse — is a HOL definition whose body is a lambda clause over the model, and entailment |--|-- unfolds to pointwise implication on all memories. Nothing at this layer is axiomatized, so no assertion you can write extends the trusted base.

The top layer is the rule set. Four separation-algebra laws (unit_joinunit_join, unit_specunit_spec, join_commjoin_comm, join_assocjoin_assoc) are proved from the memory model; every other law — associativity and commutativity of ****, empemp as unit, the magic-wand adjunction, the frame rule, the pure-fact and quantifier rules — is derived from those four together with the connective definitions. Only the typed memory predicates layered on top of raw bytes bring in axioms, and those are flagged individually where they appear.

• Memory Model and Assertions — addresses, bytes and the three-state cell; memories and the join relation; hprophprop and the definition of every connective; entailment and equivalence; purepure versus factfact; iterated separating conjunction; the notation summary.

• Proof Rules — the four primitive separation-algebra laws and the derived rule set, each tagged as proved or axiom: entailment, the algebra of ****, framing, the adjunctions, the propositional and quantifier rules, and how a rule is obtained as a thmthm in a C* proof.

• Typed Memory Predicates — how data_atdata_at, undef_data_atundef_data_at, array_atarray_at and their relatives are layered on top of byte cells, the validity and range constraints they build in, and the rules for splitting, merging and rebasing them.