Memory Model and Assertions

This page specifies the two lowest layers of C*‘s separation logic: the memory model, and the assertion language defined over it. Everything below is a HOL Light definition, quoted in the form in which the proof kernel introduces it, so the terms can be pasted into a backtick logical expression or into the argument of a definition interface unchanged.

The layering matters when reading the definitions: the memory model fixes what a state is, and the assertion language is then defined purely in terms of two operations on states — a join relation and a unit predicate. No connective mentions bytes or permissions directly.

An address and a byte are both integers:

addr = :int
byte = :int
addr_eqb:addr->addr->bool = (=)
byte_eqb:byte->byte->bool = (=)

addr = :int
byte = :int
addr_eqb:addr->addr->bool = (=)
byte_eqb:byte->byte->bool = (=)

addraddr and bytebyte are type abbreviations, not new types: they are expanded away at parse time, so a term of type addraddr is a term of type :int:int and may be used wherever an integer is expected. Three consequences are worth stating explicitly.

• Address arithmetic is ordinary integer arithmetic. There is no wrapping, no notion of “provenance”, and no distinction between a valid and an invalid address at the level of the type — field_addr p Tlist Ftailfield_addr p Tlist Ftail and x + i * sizeof(ty)x + i * sizeof(ty) are integer expressions, and their validity is a pure fact carried by the typed predicates of Typed Memory Predicates.
• A byte is likewise an unbounded integer. That a stored byte lies in is not a consequence of its type; it is part of what the typed store predicates assert.
• Because the abbreviations are transparent, an integer literal in an assertion needs the ii suffix even in address position: data_at 0i Tint vdata_at 0i Tint v, never data_at 0 Tint vdata_at 0 Tint v.

addr_eqbaddr_eqb and byte_eqbbyte_eqb are defined to be HOL equality itself. They exist so that the model can be phrased with an explicit comparison function; single_byte_memsingle_byte_mem below is the only place they are used.

mem_var = Noperm | Noninit | value byte

mem_var = Noperm | Noninit | value byte

This is an inductive datatype with three constructors, and it is the one place where C* departs from the textbook heap model:

Introducing mem_varmem_var with define_typedefine_type also yields the distinctness and cases theorems for the three constructors; those are exactly the facts the primitive separation-algebra proofs in Proof Rules rewrite with.

A memory maps every address to a cell state:

mem = :addr->mem_var

mem = :addr->mem_var

The map is total: partiality is encoded inside the codomain, by NopermNoperm. This choice removes the need for any finite-map or partial-function machinery — equality of memories is ordinary function equality, provable by extensionality, and the “footprint” of a memory is a derived notion (the set of addresses whose state is not NopermNoperm) rather than a primitive one. Note also that memories are not required to be finite.

Four constants complete the model:

empty_mem:mem = (\p. Noperm)
single_byte_mem (p:addr) (n:byte) = (\p'. if (addr_eqb p' p) then value n else Noperm)
single_noninit_mem (p:addr) = (\p'. if (addr_eqb p' p) then Noninit else Noperm)
mem_empty (m:mem) : bool = (!p. m p = Noperm)

empty_mem:mem = (\p. Noperm)
single_byte_mem (p:addr) (n:byte) = (\p'. if (addr_eqb p' p) then value n else Noperm)
single_noninit_mem (p:addr) = (\p'. if (addr_eqb p' p) then Noninit else Noperm)
mem_empty (m:mem) : bool = (!p. m p = Noperm)

empty_memempty_mem and mem_emptymem_empty are easy to confuse: the first is a memory, the second is a predicate on memories. By extensionality empty_memempty_mem is the unique memory satisfying mem_emptymem_empty, which is why the unit laws can be proved by exhibiting empty_memempty_mem as the witness. The two singleton memories — one byte, and one owned-but-uninitialized cell — are the atoms from which every typed memory predicate is assembled.

Splitting and combining memory is expressed by one relation.

mem_join (m1:mem) (m2:mem) (m:mem) : bool =
  (!p.
  (m1 p = Noperm /\ m2 p = Noperm /\ m p = Noperm) \/
  (m1 p = Noperm /\ m2 p = Noninit /\ m p = Noninit) \/
  (m1 p = Noninit /\ m2 p = Noperm /\ m p = Noninit) \/
  (?n. m1 p = Noperm /\ m2 p = value n /\ m p = value n) \/
  (?n. m1 p = value n /\ m2 p = Noperm /\ m p = value n))

mem_join (m1:mem) (m2:mem) (m:mem) : bool =
  (!p.
  (m1 p = Noperm /\ m2 p = Noperm /\ m p = Noperm) \/
  (m1 p = Noperm /\ m2 p = Noninit /\ m p = Noninit) \/
  (m1 p = Noninit /\ m2 p = Noperm /\ m p = Noninit) \/
  (?n. m1 p = Noperm /\ m2 p = value n /\ m p = value n) \/
  (?n. m1 p = value n /\ m2 p = Noperm /\ m p = value n))

The relation is pointwise: mm is a join of m1m1 and m2m2 exactly when, at every address, the three cell states form one of the five listed configurations. Reading the clauses as a table of cases:

• if neither operand has permission, neither does the result;
• if exactly one operand has permission, the result inherits that operand’s state, uninitialized or valued, unchanged.

What is absent is as informative as what is present. There is no clause in which both m1 pm1 p and m2 pm2 p are different from NopermNoperm: permission is exclusive, so a memory holding a cell can never be split into two memories that both hold it — this is the model-level source of the disjointness built into ****. There is also no clause turning NoninitNoninit into value nvalue n: joining redistributes ownership and never invents content.

Two auxiliary constants accompany the relation:

mem_disjoint (m1:mem) (m2:mem) : bool = (!x. (m1 x = Noperm) \/ (m2 x = Noperm))
mem_merge (m1:mem) (m2:mem) : mem = (\x.
  match (m1 x) with
  | Noperm -> m2 x
  | Noninit -> (match (m2 x) with value v2 -> value v2 | _ -> Noninit)
  | value v1 -> value v1
)

mem_disjoint (m1:mem) (m2:mem) : bool = (!x. (m1 x = Noperm) \/ (m2 x = Noperm))
mem_merge (m1:mem) (m2:mem) : mem = (\x.
  match (m1 x) with
  | Noperm -> m2 x
  | Noninit -> (match (m2 x) with value v2 -> value v2 | _ -> Noninit)
  | value v1 -> value v1
)

mem_disjointmem_disjoint is the compatibility condition on its own: at every address at least one side has no permission. mem_mergemem_merge is a total combining function that resolves overlaps by a fixed priority. Neither is part of the assertion language, and neither should be used when writing specifications: mem_mergemem_merge exists only as a proof witness — it supplies the intermediate memory required by the existential in join_assocjoin_assoc — and on disjoint arguments it agrees with the join relation. User-level assertions see the model only through ****.

The assertion layer is defined against an abstract interface, and then that interface is instantiated with the memory model:

model = :mem
expr  = :model->bool
hprop = :expr
join:model->model->model->bool = mem_join
is_unit:model->bool = mem_empty

model = :mem
expr  = :model->bool
hprop = :expr
join:model->model->model->bool = mem_join
is_unit:model->bool = mem_empty

So an assertion is a predicate over memories: hprophprop unfolds to :mem->bool:mem->bool, and applying an assertion to a memory, p mp m, is the satisfaction relation. There is no separate syntactic category of formulas and no interpretation function — this is what “shallow embedding” means concretely.

The indirection through modelmodel, exprexpr, joinjoin and is_unitis_unit is deliberate. Every connective below is defined using joinjoin and is_unitis_unit only, never using NopermNoperm, valuevalue or mem_joinmem_join directly, so the assertion layer is parametric in the underlying separation algebra and the memory model can be revised without touching a single connective definition. It also means that unfolding an assertion down to bytes takes two rewriting steps rather than one.

Two facts hold of the whole layer:

• every connective is introduced by new_basic_definitionnew_basic_definition, that is, as a definitional extension — it adds a constant and its defining equation, and cannot make the logic inconsistent;
• consequently every connective can be unfolded to its lambda body by rewriting with its definition theorem, which is what the semantic proofs of the rules do.

Each family below is quoted as it is defined, followed by the surface notation that the parser and printer use for it.

hsep = (\x:expr y:expr m:model. ?m1 m2. join m1 m2 m /\ x m1 /\ y m2)

hsep = (\x:expr y:expr m:model. ?m1 m2. join m1 m2 m /\ x m1 /\ y m2)

p ** qp ** q holds of mm when mm can be split into two joinable parts satisfying pp and qq respectively. The split is existentially quantified, so an assertion never fixes one particular splitting, and disjointness is inherited from the join relation rather than being stated separately. The notation is ****, not **, because ** is already multiplication in HOL Light; it is infix at precedence 8, right-associative.

hwand = (\x:expr y:expr m:model. !m1 m2. join m m1 m2 ==> x m1 ==> y m2)

hwand = (\x:expr y:expr m:model. !m1 m2. join m m1 m2 ==> x m1 ==> y m2)

p -* qp -* q holds of mm when extending mm by any memory satisfying pp yields a memory satisfying qq. Note the argument order in join m m1 m2join m m1 m2: the described memory mm is the first operand, m1m1 is the memory being added, and m2m2 is the extended result, so the wand universally quantifies over both the added part and the result. It is infix at precedence 4, right-associative, and is an override rather than an overload — -*-* denotes the wand and nothing else.

hand  = (\x:expr y:expr m:model. x m /\ y m)
hor   = (\x:expr y:expr m:model. x m \/ y m)
himpl = (\x:expr y:expr m:model. x m ==> y m)

hand  = (\x:expr y:expr m:model. x m /\ y m)
hor   = (\x:expr y:expr m:model. x m \/ y m)
himpl = (\x:expr y:expr m:model. x m ==> y m)

These three lift the corresponding boolean connectives to the same memory: p && qp && q requires one memory to satisfy both operands, which is what distinguishes it from p ** qp ** q. &&&& (precedence 8) and |||| (precedence 6) are overloaded on :bool:bool and :hprop:hprop, so the same symbol means /\/\ or \/\/ when its operands are boolean; type inference disambiguates. -->--> (precedence 4) is an override and exists only at the hprophprop layer — boolean implication remains ==>==>. All three are right-associative.

hexists = (\x:A->expr m:model. ?a:A. x a m)
hforall = (\x:A->expr m:model. !a:A. x a m)

hexists = (\x:A->expr m:model. ?a:A. x a m)
hforall = (\x:A->expr m:model. !a:A. x a m)

Both take a function from the quantified type into assertions, so the binder notation exists . exists . is a lambda in disguise. The type AA is arbitrary: one can quantify over addresses, integers, lists, or any HOL type. The words existsexists and forallforall are overloaded on :bool:bool and :hprop:hprop, which is why the convention in C* is to write the boolean quantifiers with the symbols ?? and !! and the assertion-layer ones with the words — the two then never look alike in a term.

hemp = (\m:model. is_unit m)

hemp = (\m:model. is_unit m)

empemp holds exactly of the memory with no permission anywhere. It is the unit of **** (neutral_hsepneutral_hsep proves neutral(**) = empneutral(**) = emp), which is what makes iterated separating conjunction well-defined.

hpure = (\p:bool m:model. p)
hfact = (\p:bool m:model. hand (hpure p) hemp m)

hpure = (\p:bool m:model. p)
hfact = (\p:bool m:model. hand (hpure p) hemp m)

pure()pure() ignores its memory argument entirely; fact()fact() additionally requires that memory to be empty. Both are overrides, so purepure and factfact always mean these constants. The distinction is important enough to have its own section below.

htrue  = (\m:model. T)
hfalse = (\m:model. F)

htrue  = (\m:model. T)
hfalse = (\m:model. F)

truetrue is satisfied by every memory — it is the standard way of saying “and possibly more resources beyond these” — and falsefalse by none. Both words are overloaded on :bool:bool and :hprop:hprop. The expected identities are theorems: true -|- pure(T)true -|- pure(T), false -|- pure(F)false -|- pure(F) and fact(T) -|- empfact(T) -|- emp.

Relations between assertions live at type :bool:bool, not :hprop:hprop:

hentail = (\x:expr y:expr. !m. x m ==> y m)
logic_equiv = (\x:expr y:expr. hentail x y /\ hentail y x)

hentail = (\x:expr y:expr. !m. x m ==> y m)
logic_equiv = (\x:expr y:expr. hentail x y /\ hentail y x)

• hp1 |-- hp2hp1 |-- hp2 (hentailhentail, precedence 2) is pointwise implication over all memories.
• hp1 -||- hp2hp1 -||- hp2 (logic_equivlogic_equiv, precedence 2) is entailment in both directions.
• hp1 -|- hp2hp1 -|- hp2 (precedence 2) is HOL equality specialized to :hprop:hprop: the notation -|--|- is an override of (=):hprop->hprop->bool(=):hprop->hprop->bool. This is why a definition of a representation predicate is written with == between assertions but prints back with -|--|-.

The last two notations denote different constants, but they are interchangeable:

!hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)

!hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)

Mutual entailment on assertions is the same thing as equality of assertions, because an assertion is a function into :bool:bool and HOL has both function and propositional extensionality. The practical consequence is large: equivalence of assertions needs no setoid, no congruence rules and no rewriting infrastructure of its own — an established -|--|- is an ordinary HOL equation and can be used by REWRITE_TACREWRITE_TAC anywhere an assertion occurs, including under binders and inside other connectives.

The laws of entailment themselves — reflexivity, transitivity, antisymmetry (hentail_reflhentail_refl, hentail_transhentail_trans, hentail_antisymhentail_antisym) and the rest of the rule set — are catalogued in Proof Rules.

Both embed a boolean proposition into an assertion, and they differ only in what they claim about memory:

pure(P)    holds of every memory, whatever it owns
fact(P)    holds of the empty memory only
hfact_def  !p hp. fact(p) -|- (pure(p) && emp)

pure(P)    holds of every memory, whatever it owns
fact(P)    holds of the empty memory only
hfact_def  !p hp. fact(p) -|- (pure(p) && emp)

The consequence is about composition. Under &&&& the two operands describe the same memory, so pure(P) && qpure(P) && q is exactly “qq, and moreover PP”. Under **** the memory is split, and since pure(P)pure(P) accepts whatever share it is given, pure(P) ** qpure(P) ** q does not pin down that share as empty: it says only that some sub-memory satisfies qq, weakening qq by an arbitrary frame. fact(P) ** qfact(P) ** q, by contrast, forces the factfact side to take the empty memory, so qq still describes everything — the theorem hfact_hpurehfact_hpure records this as fact() ** hp -|- pure() && hpfact() ** hp -|- pure() && hp.

Since symbolic states and contracts are built with ****, factfact is the form to write. It is also the form the rules are stated for: hsep_hfact_lefthsep_hfact_left and hsep_hfact_righthsep_hfact_right move a factfact conjunct freely across a separating conjunction, hfact_elimhfact_elim turns it into an ordinary hypothesis, and hfact_duphfact_dup duplicates it — a pure fact costs no resource.

pure(x == 1i) && data_at p Tint x
fact(x == 1i) ** data_at p Tint x

pure(x == 1i) && data_at p Tint x
fact(x == 1i) ** data_at p Tint x

Extracting the pure content of an entailment goal — turning a goal about assertions into a goal about integers — is the job of purification; see Purifying Entailments with Strategies.

Separating conjunction over a finite set of indices is a single combinator:

hitersep (s: A->bool) (f: A->hprop) = iterate (**) s f

hitersep (s: A->bool) (f: A->hprop) = iterate (**) s f

A set in HOL Light is a predicate A->boolA->bool, and iterateiterate is the library’s generic fold of a binary operation over a finite set. Folding in an unspecified order is only well-defined for a commutative monoid, and that side condition is discharged once and for all: neutral_hsepneutral_hsep proves neutral(**) = empneutral(**) = emp and monoidal_hsepmonoidal_hsep proves monoidal(**)monoidal(**) from associativity, commutativity and the unit laws. Every ITERATE_*ITERATE_* theorem of the HOL Light library therefore specializes to a hitersep_*hitersep_* theorem, obtained mechanically:

hitersep_empty
  !f. hitersep {} f -|- emp
hitersep_single
  !f x. hitersep {x} f -|- f x
hitersep_insert
  !f x s. FINITE s
          ==> (hitersep (x INSERT s) f -|-
               if x IN s then hitersep s f else (f x) ** (hitersep s f))
hitersep_disjoint_union
  !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
          ==> (hitersep (s UNION t) f -|- (hitersep s f) ** (hitersep t f))
hitersep_hsep
  !f g s. FINITE s
          ==> (hitersep s (\x. (f x) ** (g x)) -|-
               (hitersep s f) ** (hitersep s g))

hitersep_empty
  !f. hitersep {} f -|- emp
hitersep_single
  !f x. hitersep {x} f -|- f x
hitersep_insert
  !f x s. FINITE s
          ==> (hitersep (x INSERT s) f -|-
               if x IN s then hitersep s f else (f x) ** (hitersep s f))
hitersep_disjoint_union
  !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
          ==> (hitersep (s UNION t) f -|- (hitersep s f) ** (hitersep t f))
hitersep_hsep
  !f g s. FINITE s
          ==> (hitersep s (\x. (f x) ** (g x)) -|-
               (hitersep s f) ** (hitersep s g))

The same pattern produces hitersep_diffhitersep_diff, hitersep_deletehitersep_delete, hitersep_eqhitersep_eq (replace the body by a pointwise-equivalent one) and hitersep_caseshitersep_cases (split the index set by a predicate). Note the FINITEFINITE hypotheses: they are required by iterateiterate and are not decorative. Arrays are the main client of this combinator — array_atarray_at is an iterated separating conjunction of data_atdata_at over an index range, which is where the split, merge and rebase rules of Typed Memory Predicates come from.

The surface notation, the kernel constant it abbreviates, and what it means. This table is the reference counterpart of the one in Separation Logic in C*.

Infix precedence, from loosest to tightest: |--|--, -|--|-, -||--||- at 2; -*-*, -->--> at 4; |||| at 6; &&&& and **** at 8. All are right-associative, and function application binds tighter than all of them, so fact(x > 0i) ** data_at x Tint v |-- truefact(x > 0i) ** data_at x Tint v |-- true parses as intended without parentheses.

• addraddr and bytebyte are transparent abbreviations for :int:int; address arithmetic is integer arithmetic, and validity is asserted by predicates, never by types.
• A memory cell is in one of three states — NopermNoperm, NoninitNoninit, value value — and a memory is the total map addr->mem_varaddr->mem_var, with partiality encoded by NopermNoperm.
• Splitting is the three-place relation mem_joinmem_join, whose five clauses make permission exclusive; mem_disjointmem_disjoint is the compatibility condition and mem_mergemem_merge is a proof-only witness.
• An assertion is literally a predicate over memories, hprop = :mem->boolhprop = :mem->bool, and every connective is a definition — not an axiom — written against the abstract joinjoin and is_unitis_unit.
• Entailment |--|-- is pointwise implication; -|--|- is HOL equality on assertions, and by heqheq it coincides with mutual entailment -||--||-, so assertion equivalences are ordinary rewriting equations.
• pure()pure() constrains nothing spatially and fact()fact() asserts emptiness; factfact is the form that composes with **** and the one specifications should use.
• hitersephitersep folds **** over a finite index set, justified once by monoidal_hsepmonoidal_hsep, and underlies the array predicates.