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 = :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. 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.

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

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. User-level assertions see the model only through ****: the relation is never written in a specification.

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 and no interpretation function — this is what “shallow embedding” means concretely. 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 a definition, not an axiom: it adds a constant together with its defining equation, and can be unfolded to its lambda body by rewriting with that equation, 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 -*-* 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) 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. The combinator is available for user-defined predicates over index sets; the library’s own array predicate does not go through 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), and its split, merge and rebase rules are stated directly in Typed Memory Predicates.

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; specifications never write it, they see it only through ****.
• An assertion is literally a predicate over memories, hprop = :mem->boolhprop = :mem->bool, and every connective is 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() 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; array_atarray_at is defined by recursion on its list rather than through it.