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 — associativity and commutativity of ****, empemp as unit, the magic-wand adjunction, the frame rule, the pure-fact and quantifier rules. Every rule is proved from the memory model and the connective definitions; nothing at this layer is axiomatized. The typed memory predicates layered on top of raw bytes are proved as well; what their page records instead is where the theory stays silent, on the compound C types.

• 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 catalogue of rules, every one of them a proved theorem: 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.