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. HOL Light definitions are quoted in the form introduced by the proof kernel, so their terms can be pasted unchanged into a backtick logical expression or used as arguments to a definition interface.

The memory model defines what a state is. The assertion language is then defined 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 = :int
byte = :int

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. This has three consequences.

• 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.

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:

A memory maps every address to a cell state:

mem = :addr->mem_var

mem = :addr->mem_var

The map is total: partiality is encoded in the codomain by NopermNoperm. This removes the need for finite maps or partial functions. Equality of memories is ordinary function equality, provable by extensionality, and a memory’s footprint is derived as the set of addresses whose state is not NopermNoperm. Memories are not required to be finite.

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. The clauses cover two cases:

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

The clauses exclude two cases. First, m1 pm1 p and m2 pm2 p cannot both differ from NopermNoperm: permission is exclusive, so a memory holding a cell cannot be split into two memories that both hold it. This restriction gives **** its disjointness property. Second, joining cannot turn NoninitNoninit into value nvalue n: it redistributes ownership without creating content. User-level assertions use the model through separation-logic connectives; specifications never state the relation directly.

An assertion is a predicate over memories:

model = :mem
expr  = :model->bool
hprop = :expr

model = :mem
expr  = :model->bool
hprop = :expr

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 or interpretation function: this is a shallow embedding. In the definitions below, joinjoin is the relation mem_joinmem_join and is_unit mis_unit m says that mm has no permission anywhere (!p. m p = Noperm!p. m p = Noperm); no connective mentions NopermNoperm or valuevalue directly.

Every connective is introduced by a definition, not an axiom. The definition adds a constant and its defining equation. Rewriting with that equation unfolds the constant to its lambda body, as in the semantic proofs of the rules.

Each family below is quoted as defined, followed by its surface notation in the parser and printer.

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 the assertion does not specify a particular split. Disjointness follows from the join relation and need not be 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. 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 -*-* 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 determines which meaning applies. -->--> (precedence 4) 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 to assertions; the binder notation exists . exists . is another way to write a lambda. 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, so the C* convention is to use the symbols ?? and !! for Boolean quantifiers and the words for assertion-layer quantifiers. This makes the two kinds visually distinct 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 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() requires to hold and ignores its memory argument; fact()fact() additionally requires that memory to be empty. Both are overrides, so purepure and factfact always mean these constants. Their different memory requirements are discussed below.

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

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

truetrue is satisfied by every memory and is the standard way to allow additional resources; falsefalse is satisfied by none. Both words are overloaded on :bool:bool and :hprop:hprop. The following identities are theorems: true -|- pure(T)true -|- pure(T), false -|- pure(F)false -|- pure(F) and fact(T) -|- empfact(T) -|- emp.

Relations between assertions have 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 coincides with equality of assertions because an assertion is a function into :bool:bool and HOL has both function and propositional extensionality. Thus, assertion equivalence needs no separate setoid, congruence rules or rewriting machinery. An established -|--|- is an ordinary HOL equation that REWRITE_TACREWRITE_TAC can use wherever 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, differing only in their requirements on memory:

pure(P)    holds exactly when P holds, regardless of the memory
fact(P)    holds exactly when P holds and the memory is empty
hfact_def  !p hp. fact(p) -|- (pure(p) && emp)

pure(P)    holds exactly when P holds, regardless of the memory
fact(P)    holds exactly when P holds and the memory is empty
hfact_def  !p hp. fact(p) -|- (pure(p) && emp)

This difference affects 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) places no restriction on its share, pure(P) ** qpure(P) ** q does not require that share to be empty: it requires PP to hold and some sub-memory to satisfy qq, allowing an arbitrary frame alongside that sub-memory. fact(P) ** qfact(P) ** q, by contrast, requires the factfact side to be empty, so qq still describes the whole memory. The theorem hfact_hpurehfact_hpure states this as fact() ** hp -|- pure() && hpfact() ** hp -|- pure() && hp.

Symbolic states and contracts are built with ****, so use factfact in them. 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, since a pure fact consumes 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

Purification extracts the pure content of an entailment goal, turning a goal about assertions into one about integers; see Purifying Entailments with Strategies.

One combinator expresses separating conjunction over a finite index set:

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 this side condition has been discharged: 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 in HOL Light’s library therefore specializes mechanically to a hitersep_*hitersep_* theorem:

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). The FINITEFINITE hypotheses are required by iterateiterate. The combinator is available for user-defined predicates over index sets. The library’s array predicate does not use it: array_atarray_at is defined by recursion on its list of values, with element ii at x + i * sizeof(ty)x + i * sizeof(ty). Its split, merge and rebase rules are stated directly in Typed Memory Predicates.

The table lists each surface notation, its kernel constant and its meaning. It corresponds to the tutorial table 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; specifications use it through separation-logic connectives.
• An assertion is a predicate over memories, hprop = :mem->boolhprop = :mem->bool, and every connective is introduced by a definition over the join relation, not an axiom.
• 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() and fact()fact() both require to hold. The former places no spatial constraint and the latter requires empty memory. Specifications should use factfact when composing with ****.
• hitersephitersep folds **** over a finite index set, justified by monoidal_hsepmonoidal_hsep; array_atarray_at is defined by recursion on its list rather than through it.