Separation Logic

C* uses separation-logic assertions. Its separation logic is a shallow embedding in HOL Light, rather than a fixed notation supported by a black-box solver. This part describes its three layers as 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 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 memory model. 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, which includes 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 built on raw bytes are also proved; their reference page identifies what the theory leaves unspecified for 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, each 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 defined over byte cells, the validity and range constraints they build in, and the rules for splitting, merging and rebasing them.