Separation Logic in C*

The previous section introduced separation logic with formal notation: a program state is a store plus a heap, and spatial assertions (, , ) let a specification characterize memory properties precisely and locally. This section brings that mathematical notation down to concrete C* syntax: how to write spatial assertions in C*, which assumptions and conventions C* currently uses to connect assertions with C’s memory semantics, and how to use C*‘s definition mechanisms to define representation predicates for data structures such as linked lists and trees. This section is only about “how to write assertions and predicates”; it does not touch any proofs.

In Your First C* Program we already saw that C* specifications are written inside logical expressions wrapped in `...``...` backticks, whose syntax comes from HOL Light, the theorem prover integrated into C*. Every piece of math notation from the previous section has a corresponding form in this syntax:

A few differences from the math notation are worth pointing out first:

• separating conjunction is written **** rather than ** — in HOL Light’s syntax ** is already taken by multiplication;
• the points-to predicate data_atdata_at has one more argument than : a C type, which is the key to connecting assertions with C semantics, expanded on later in this section;
• integer constants take an ii suffix (e.g. 42i42i, 0i0i), negation is ----, logical not is ~~, and equality conventionally uses ==== — all of which already appeared in the verification conditions of Your First C* Program.

To practice writing assertions, it helps to have a place where C* will immediately parse and type-check them for us. Contracts ([[cst::require]][[cst::require]] and the like) are of course the final home of assertions, but this section does not yet want to bring in all the rules of contracts. Fortunately, C* offers a lighter-weight vehicle: the global proof declaration.

The [[cst::proof]][[cst::proof]] annotation marks what follows as serving verification only: it can annotate a statement block inside a function body, [[cst::proof]] { ... }[[cst::proof]] { ... } (a proof block, used for writing proof code, the protagonist of later chapters), or it can annotate a file-scope declaration, yielding a verification-time declaration — one that exists only at verification time and does not enter the compiled artifact at all. Verification-time declarations may use a set of verification-only C types; this section uses three:

• termterm: a HOL logical term;
• thmthm: a HOL theorem;
• indtypeindtype: an inductive datatype (introduced later, when we cover the definition mechanisms).

So the following piece of valid C* code is our “assertion scratchpad”:

#include "proof/proof.h"
// Register a printing function for the term type, used to print the contents of tm
// when viewing the symbolic state in VSCode
[[cst::proof]] static inline char *cst_string_of_term(const term tm) {
  if (IS_NULL(tm)) return "<null>";
  return cstr_term(tm);
}
[[cst::proof]] term ex1 = `data_at p Tint 42i`;

#include "proof/proof.h"
// Register a printing function for the term type, used to print the contents of tm
// when viewing the symbolic state in VSCode
[[cst::proof]] static inline char *cst_string_of_term(const term tm) {
  if (IS_NULL(tm)) return "<null>";
  return cstr_term(tm);
}
[[cst::proof]] term ex1 = `data_at p Tint 42i`;

It declares a logical term named ex1ex1 whose content is the assertion inside the backticks: the address denoted by the logical variable pp stores the intint-typed value 4242. If you view the symbolic state on this line in VSCode, the HOL Light server will parse this assertion and type-check it; a mistake (for instance, dropping the ii suffix so the types are inconsistent) yields a diagnostic immediately. The pp in the assertion need not be declared beforehand: an identifier undefined in a logical expression automatically becomes a logical variable, whose type is determined by type inference.

The part inside the backticks is lexed and parsed by HOL Light. Let us spend a few minutes getting to know this theorem prover’s conventions — terms, types, and formulas — which will make reading and writing assertions and defining predicates much smoother later. HOL Light implements higher-order logic, which can be roughly understood as “typed λ-calculus plus classical logic”, with a very small syntactic core.

Everything is a term. The expressions inside backticks are collectively called terms, and a term is built in only four ways: variables (an undefined identifier automatically becomes a variable, like the earlier pp), constants (introduced by the logic library or by the user, like empemp, data_atdata_at), application, and λ-abstraction. Application is written f xf x; multi-argument functions are curried, so data_at x Tint vdata_at x Tint v is really ((data_at x) Tint) v((data_at x) Tint) v — arguments are separated only by spaces, with no parentheses or commas. A λ-abstraction is an anonymous function, written \. \. . Try it on the scratchpad:

[[cst::proof]] term tm1 = `\x. x + 1i`;          // λ-abstraction: the "add one" function on integers
[[cst::proof]] term tm2 = `(\x. x + 1i) 41i`;    // application: this term is provably equal to 42i
[[cst::proof]] term tm3 = `[1i; 2i; 3i]`;        // list literal, elements separated by semicolons

[[cst::proof]] term tm1 = `\x. x + 1i`;          // λ-abstraction: the "add one" function on integers
[[cst::proof]] term tm2 = `(\x. x + 1i) 41i`;    // application: this term is provably equal to 42i
[[cst::proof]] term tm3 = `[1i; 2i; 3i]`;        // list literal, elements separated by semicolons

Every term has a type. Common types are boolbool (propositions), numnum (natural numbers), intint (integers); A -> BA -> B is a function type (->-> is right-associative); type constructors use postfix application, so (int)list(int)list is the type “list of integers” — which is exactly the type of tm3tm3. A type annotation is written ::, and can be attached to any subterm, e.g. (x:int)(x:int). Normally there is no need to annotate everywhere: HOL Light performs type inference, and a manual annotation is needed only when the context is insufficient to determine a type. Another type-related detail: a literal without a suffix, 4242, is a natural number (numnum); only a suffixed 42i42i is an integer (intint). C*‘s modeling of C programs uses intint throughout, so numbers in this tutorial always carry the ii.

A formula is just a term of type boolbool. Higher-order logic has no separate syntactic layer for “formulas”: a proposition is a term of type boolbool, and a predicate is a function whose result type is boolbool. The logical connectives and quantifiers are written as follows (a binder can bind several variables at once, e.g. !x y. P!x y. P):

[[cst::proof]] term tm4 = `!x. ?y. y > (x:int)`;  // a (true) proposition: every integer has a larger one

[[cst::proof]] term tm4 = `!x. ?y. y > (x:int)`;  // a (true) proposition: every integer has a larger one

Note that these are notations at the boolbool layer. The conjunction, disjunction, and quantifiers at the assertion layer (hprophprop) are their counterparts: C*‘s convention is that boolbool-layer quantifiers use the symbols !!/??, while assertion-layer quantifiers use the words forallforall/existsexists, so the two do not interfere; the double life of &&&&/|||| is covered in the next section. The complete lexical and grammatical specification (operator precedence table, list of binders, etc.) can be found in the reference manual.

Theorems are computed. The distinction between termterm and thmthm is the soul of HOL Light: anyone can write down a boolbool term, but a thmthm value can only be assembled from the handful of inference rules in the kernel (this design comes from the LCF tradition — everything outside the kernel ultimately reduces to combinations of kernel rules). The mechanisms for defining new constants and new types likewise pass through the kernel and return a corresponding definition theorem — the thmthm we obtain later in this section when defining representation predicates comes from exactly this. More on theorems and proofs will be developed in later chapters.

In C*‘s logical layer, the spatial assertions of separation logic form a type of their own, named hprophprop (heap proposition). The operators in the comparison table at the start of this section can be split into two groups by their types:

• operators that construct assertions, with result type hprophprop: ****, &&&&, ||||, -*-*, empemp, fact(...)fact(...), existsexists, forallforall, etc.;
• operators that state relations between assertions, with result type boolbool: |--|-- (entailment) and -|--|- (equivalence).

The latter are judgments at the “meta level”: p |-- qp |-- q is itself no longer an assertion, but a proposition about two assertions — the verification conditions shown in Your First C* Program have exactly this shape. The two groups of operators can appear mixed in the same logical term; for example, writing the previous section’s “ relaxes exactly into at least” example onto the scratchpad:

[[cst::proof]] term ex2 = `data_at x Tint 7i ** true`;
[[cst::proof]] term ex3 = `data_at x Tint 7i |-- data_at x Tint 7i ** true`;

[[cst::proof]] term ex2 = `data_at x Tint 7i ** true`;
[[cst::proof]] term ex3 = `data_at x Tint 7i |-- data_at x Tint 7i ** true`;

ex2ex2 is an hprophprop; ex3ex3 is a boolbool — a (happens-to-hold) entailment judgment. Note that truetrue, falsefalse, existsexists, forallforall, &&&&, |||| are all overloaded on both boolbool and hprophprop: the &&&& in fact(x > 0i && y > 0i)fact(x > 0i && y > 0i) is boolean conjunction (the previous section’s /\/\), while the &&&& in fact(x > 0i) && empfact(x > 0i) && emp is assertion conjunction — type inference tells them apart automatically.

The operator precedence, from loosest to tightest, is: |--|--, -|--|- are loosest, then -*-*, then ||||, and the tightest are &&&& and **** (same level, both right-associative); function application (such as data_at x Tint vdata_at x Tint v) binds tighter than all infix operators. So fact(x > 0i) ** data_at x Tint v |-- truefact(x > 0i) ** data_at x Tint v |-- true needs no parentheses to mean “the entire separating conjunction on the left entails truetrue”.

In the previous section we defined the meaning of assertions via the satisfaction relation . In C*, this semantics is not a paper convention but a definition inside the logic: C* shallowly embeds separation logic into HOL Light, with hprophprop defined as the type “predicate over memory”, mem -> boolmem -> bool, where memory memmem is a function from addresses to memory-cell states, and a cell state has three possibilities:

On this model, each operator is an ordinary HOL definition, corresponding one by one to the previous section’s semantic definitions:

emp      =  (\m. is_unit m)                                  the allocated set is empty
pure     =  (\p m. p)                                        independent of m
p ** q   =  (\m. ?m1 m2. join m1 m2 m /\ p m1 /\ q m2)       disjoint splitting of the heap
p |-- q  =  (!m. p m ==> q m)                                pointwise entailment on all memories

emp      =  (\m. is_unit m)                                  the allocated set is empty
pure     =  (\p m. p)                                        independent of m
p ** q   =  (\m. ?m1 m2. join m1 m2 m /\ p m1 /\ q m2)       disjoint splitting of the heap
p |-- q  =  (!m. p m ==> q m)                                pointwise entailment on all memories

Here join m1 m2 mjoin m1 m2 m means mm can be split into disjoint m1m1 and m2m2 — exactly the previous section’s . It is worth emphasizing: the algebraic laws of separation logic (the associativity and commutativity of ****, empemp being the unit, the adjunction between the magic wand and ****, etc.) are all theorems proved from these definitions in C*‘s logic library, not additional axioms. In other words, the assertions you write in C* are not the input language of some black-box solver; every step of their reasoning can be traced back to a proof accepted by the HOL Light kernel.

In math notation only says “address stores value “; but in C, “stores” must answer a question: stored as what type? intint and charchar occupy different numbers of bytes, and signed versus unsigned differ in their value ranges. This is the second argument of data_atdata_at: a value of type ctypectype, the logical avatar of a C type. Common ctypectype constants and their sizeofsizeof:

TptrTptr uniformly represents pointer types (think of it as void *void *). The logical layer also provides three functions sizeof()sizeof(), min_of()min_of(), max_of()max_of(), giving a type’s size and value range respectively; the type of an address itself, addraddr, is a type abbreviation for intint.

With the type argument, data_at x Tint vdata_at x Tint v carries more information than the math notation : it expands, on the byte-granular memory model, into the separating conjunction of 4 consecutive byte cells starting at xx, and it builds in validity constraints — the address is 4-aligned and within the valid range, and the value vv lies within the range of intint.

“Built-in validity” means the assertion carries pure facts that can be drawn on as needed, for example the theorem provided in the C* standard library:

data_at x ty v |-- data_at x ty v ** fact(min_of ty <= v && v <= max_of ty)

data_at x ty v |-- data_at x ty v ** fact(min_of ty <= v && v <= max_of ty)

that is, from a block of data_atdata_at resource one can at any time “extract” the range information of its value. This is the first group of conventions connecting C* assertions with C semantics: the points-to predicate is modeled at the granularity of bytes and C types, and valid addresses, alignment, and value ranges are part of the predicate’s definition, not extra assumptions.

Accompanying data_atdata_at there are two more families of predicates:

• undef_data_at undef_data_at : address has an allocated location of type , but its content is uninitialized (precisely the avatar of the NoninitNoninit state in the shallow-embedding model). It differs subtly from the math notation : is “stores some value we do not care about”, whereas reading uninitialized memory is an error. The theorem data_at x ty v |-- undef_data_at x tydata_at x ty v |-- undef_data_at x ty allows “forgetting” an initialized resource down to uninitialized, since this does not compromise safety.
• array_at array_at : consecutive elements of type starting at address , whose contents are the values of the list in order. It is defined as the iterated separating conjunction of data_atdata_at along the index, with the -th element located at + * sizeof() + * sizeof() — this matches how C* handles array subscript expressions: arr[i]arr[i] expands in the logic to an address of exactly this shape. There is also an uninitialized version undef_array_atundef_array_at, together with the “segment” and “with a hole” variants used to split an element out of an array and split away the remainder (array_at_recarray_at_rec, array_at_missing_i_recarray_at_missing_i_rec, etc.), which we introduce as they are needed.

The genuinely interesting heap structures in C programs always start from structstruct. C* brings structs into assertions likewise via a set of naming conventions. Take a linked-list node as an example:

struct list {
  int head;
  struct list *tail;
};

struct list {
  int head;
  struct list *tail;
};

In the logical layer, struct names and field names each have a dedicated type: struct_namestruct_name and fieldfield. The convention is: the logical constant corresponding to a struct name is prefixed with TT, and the logical constant corresponding to a field name is prefixed with FF — struct liststruct list corresponds to TlistTlist, and the fields headhead, tailtail correspond to FheadFhead, FtailFtail. C* establishes this correspondence by name, so we need only introduce these constants into the logic (with global proof declarations):

[[cst::proof]] int _l = (new_const("Tlist", `:struct_name`), 0);
[[cst::proof]] int _h = (new_const("Fhead", `:field`), 0);
[[cst::proof]] int _t = (new_const("Ftail", `:field`), 0);

[[cst::proof]] int _l = (new_const("Tlist", `:struct_name`), 0);
[[cst::proof]] int _h = (new_const("Fhead", `:field`), 0);
[[cst::proof]] int _t = (new_const("Ftail", `:field`), 0);

new_constnew_const declares a new logical constant (given only a name and a type, with no definition). Its return type is voidvoid, whereas file scope requires a “declaration with initializer”, so here we use C’s comma expression to produce an intint initializer — an idiom worth remembering.

The address of a field is given by the function field_addrfield_addr: field_addr field_addr denotes the address of field in the struct (named ) pointed to by . So “ptpt points to a node whose headhead is xx and whose tailtail is qq” is written:

[[cst::proof]] term ex4 =
  `data_at (field_addr pt Tlist Fhead) Tint x **
   data_at (field_addr pt Tlist Ftail) Tptr q`;

[[cst::proof]] term ex4 =
  `data_at (field_addr pt Tlist Fhead) Tint x **
   data_at (field_addr pt Tlist Ftail) Tptr q`;

When accessing pt->headpt->head in C code, C* looks in the symbolic state for the data_atdata_at resource at field_addr pt Tlist Fheadfield_addr pt Tlist Fhead. Nested structs work the same way: an address like &it->node.next&it->node.next expands to field_addr (field_addr it Titem Fnode) Tlink Fnextfield_addr (field_addr it Titem Fnode) Tlink Fnext.

Assertions ultimately need to talk about the variables of a C program. This set of conventions already appeared in Your First C* Program here we summarize them completely:

• a parameter or local variable itself occupies a block of memory, whose address in the logic is the variable __addr__addr (of type addraddr); global variables are the same;
• the initial value of a parameter at the function entry is written __pre__pre;
• in a postcondition, the function’s return value is written __return__return.

So an intint parameter xx contributes the resource data_at x__addr Tint x__predata_at x__addr Tint x__pre in the symbolic state at the function entry; an uninitialized local variable int rint r contributes undef_data_at r__addr Tintundef_data_at r__addr Tint — which is exactly what we saw in the previous section:

undef_data_at r__addr Tint **
data_at x__addr Tint x__pre

undef_data_at r__addr Tint **
data_at x__addr Tint x__pre

Pointer parameters are nothing special: the initial value pt__prept__pre of struct list *ptstruct list *pt is an address, and the memory it points to does not automatically appear in the symbolic state — to talk about *pt*pt, an assertion must explicitly characterize that block of resource (with data_atdata_at, or a representation predicate defined in the next section). This is the natural junction between separation logic’s principle that “resources must be explicitly characterized” and the conventions of C semantics.

There is one more detail: the value range of an intint parameter does not automatically appear as a standalone pure fact in the symbolic state — it is built into the resource data_at x__addr Tint x__predata_at x__addr Tint x__pre, and can be extracted with the range theorem above when needed.

These logical variables with __addr__addr, __pre__pre, __return__return are precisely the vocabulary used when writing assertions in function contracts ([[cst::require]][[cst::require]], [[cst::ensure]][[cst::ensure]]) and loop invariants ([[cst::invariant]][[cst::invariant]]); the way to write contracts and invariants will be developed in detail in the next section.

In the previous section, “ points to a valid binary tree” was a predicate defined inductively with spatial assertions:

To verify programs in C* that manipulate linked lists and trees, we need to define such predicates into the logic. These are called representation predicates: they associate a concrete block of memory with a pure mathematical value (a list, tree, etc. in HOL) — “the chain of nodes at address ptpt represents the list ll”. C* provides a set of definition mechanisms for this, all appearing as verification-interface functions, called in global proof declarations, and returning the thmthm corresponding to the definition.

new_fun_definitionnew_fun_definition takes an equation of the form “the left side is a new constant with parameters, the right side is the definition body” and defines a (possibly recursive) function or predicate, returning its definition theorem. The simplest example is a pure function:

// Register a printing function for the thm type, used to print the contents of th
// when viewing the symbolic state in VSCode
[[cst::proof]] static inline char *cst_string_of_thm(const thm th) {
  if (IS_NULL(th)) return "<null>";
  return cstr_thm(th);
}
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);

// Register a printing function for the thm type, used to print the contents of th
// when viewing the symbolic state in VSCode
[[cst::proof]] static inline char *cst_string_of_thm(const thm th) {
  if (IS_NULL(th)) return "<null>";
  return cstr_thm(th);
}
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);

The definition body can of course be an assertion. For instance, abstracting the “one linked-list node” from ex4ex4 above into a predicate:

[[cst::proof]] thm node_at_def = new_fun_definition(
  `node_at (pt:addr) (h:int) (t:addr) : hprop =
     (data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr t)`);

[[cst::proof]] thm node_at_def = new_fun_definition(
  `node_at (pt:addr) (h:int) (t:addr) : hprop =
     (data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr t)`);

From then on node_at pt x qnode_at pt x q is a valid assertion. Note two syntactic details:

• both the parameters and the result have type annotations ((pt:addr)(pt:addr), : hprop: hprop) — a new constant has no known information, type inference cannot help, so it is good practice to write out the types in full when defining;
• the whole definition body is wrapped in parentheses. This is not optional: **** binds looser than ==, so without the parentheses p x : hprop = A ** Bp x : hprop = A ** B would be parsed as (p x = A) ** B(p x = A) ** B and raise a baffling type error.

The body of a representation predicate is usually recursive: a linked-list predicate recurses along the list, a tree predicate along the tree. For recursive functions or predicates that new_fun_definitionnew_fun_definition cannot define, one can use new_rec_definitionnew_rec_definition, which takes two arguments: the recursion theorem of the datatype being recursed on, and the definition clauses corresponding to each constructor, connected by &&&&. The following is the most classic representation predicate in separation logic — the complete definition of the singly-linked list sllsll:

[[cst::proof]] thm sll_def = new_rec_definition(
    get_theorem_by_name("list_RECURSION"),
    `(sll (pt:addr) ([]:(int)list) = fact(pt == 0i)) &&
     (sll (pt:addr) (CONS (x:int) (xs:(int)list)) =
        exists q. fact(~(pt == 0i)) **
                  data_at (field_addr pt Tlist Fhead) Tint x **
                  data_at (field_addr pt Tlist Ftail) Tptr q **
                  sll q xs)`);

[[cst::proof]] thm sll_def = new_rec_definition(
    get_theorem_by_name("list_RECURSION"),
    `(sll (pt:addr) ([]:(int)list) = fact(pt == 0i)) &&
     (sll (pt:addr) (CONS (x:int) (xs:(int)list)) =
        exists q. fact(~(pt == 0i)) **
                  data_at (field_addr pt Tlist Fhead) Tint x **
                  data_at (field_addr pt Tlist Ftail) Tptr q **
                  sll q xs)`);

sll pt lsll pt l reads as: “the chain of nodes starting at address ptpt represents the list ll”. The two clauses unfold along the two constructors of the list:

• empty list [][]: ptpt is the null pointer, and it occupies no memory (factfact characterizes the empty heap);
• nonempty list CONS x xsCONS x xs (i.e. x :: xsx :: xs): ptpt is non-null, pointing to a node whose headhead stores xx, whose tailtail stores some address qq, and the chain of nodes starting at qq represents the remainder xsxs.

Compared with the previous section’s , two changes become clear. First, disjunction becomes pattern matching: the mathematical definition distinguished the two cases with , whereas here they are written in separate clauses along the list constructors [][], CONSCONS — this is the standard form of a HOL recursive definition, and the first argument get_theorem_by_name("list_RECURSION")get_theorem_by_name("list_RECURSION") (fetching the recursion theorem of the list type from the theorem library by name) guarantees that such a case-by-case definition is well-defined. Second, the predicate gains a content parameter: only says “the shape is valid”, whereas sll pt lsll pt l simultaneously pins down what the linked list stores — this is what gives functional correctness (for example, “the reversal function really did reverse the list”) a vocabulary in which to be stated.

For a linked list, HOL’s ready-made list type is content enough; but a tree-shaped structure requires first defining the corresponding inductive datatype in the logic. new_datatype_definitionnew_datatype_definition takes a type-description string and returns an indtypeindtype value:

// Register a printing function for the indtype type, used to print the contents of idt
// when viewing the symbolic state in VSCode
[[cst::proof]] static inline char *cst_string_of_indtype(const indtype idt) {
  return cstr_indtype(idt);
}
[[cst::proof]] indtype ty = new_datatype_definition("tree = Leaf | Node tree int tree");

// Register a printing function for the indtype type, used to print the contents of idt
// when viewing the symbolic state in VSCode
[[cst::proof]] static inline char *cst_string_of_indtype(const indtype idt) {
  return cstr_indtype(idt);
}
[[cst::proof]] indtype ty = new_datatype_definition("tree = Leaf | Node tree int tree");

This line defines the inductive type treetree: either the empty tree LeafLeaf, or a node Node l v rNode l v r (left subtree, value, right subtree). The return value tyty carries two theorems: ty.recty.rec is the recursion theorem — perfect as the first argument of new_rec_definitionnew_rec_definition; ty.indty.ind is the induction theorem, used later for inductive proofs. With the corresponding C struct, the representation predicate for the binary tree follows naturally:

struct tree {
  int val;
  struct tree *l;
  struct tree *r;
};
[[cst::proof]] int _s  = (new_const("Ttree", get_struct_name_type()), 0);
[[cst::proof]] int _fv = (new_const("Fval", get_field_type()), 0);
[[cst::proof]] int _fl = (new_const("Fl", get_field_type()), 0);
[[cst::proof]] int _fr = (new_const("Fr", get_field_type()), 0);
[[cst::proof]] thm store_tree_def = new_rec_definition(ty.rec,
    `(store_tree (pt:addr) Leaf = fact(pt == 0i)) &&
     (store_tree (pt:addr) (Node (lt:tree) (v:int) (rt:tree)) =
        exists pl pr. fact(~(pt == 0i)) **
                      data_at (field_addr pt Ttree Fval) Tint v **
                      data_at (field_addr pt Ttree Fl) Tptr pl **
                      data_at (field_addr pt Ttree Fr) Tptr pr **
                      store_tree pl lt ** store_tree pr rt)`);

struct tree {
  int val;
  struct tree *l;
  struct tree *r;
};
[[cst::proof]] int _s  = (new_const("Ttree", get_struct_name_type()), 0);
[[cst::proof]] int _fv = (new_const("Fval", get_field_type()), 0);
[[cst::proof]] int _fl = (new_const("Fl", get_field_type()), 0);
[[cst::proof]] int _fr = (new_const("Fr", get_field_type()), 0);
[[cst::proof]] thm store_tree_def = new_rec_definition(ty.rec,
    `(store_tree (pt:addr) Leaf = fact(pt == 0i)) &&
     (store_tree (pt:addr) (Node (lt:tree) (v:int) (rt:tree)) =
        exists pl pr. fact(~(pt == 0i)) **
                      data_at (field_addr pt Ttree Fval) Tint v **
                      data_at (field_addr pt Ttree Fl) Tptr pl **
                      data_at (field_addr pt Ttree Fr) Tptr pr **
                      store_tree pl lt ** store_tree pr rt)`);

The previous section’s specification for free_treefree_tree, , will in C* be written as a contract with store_treestore_tree as its vocabulary.

Besides the mechanisms above, the verification interface also provides the lower-level new_basic_definitionnew_basic_definition (definition of a parameterless constant), and more; for the complete list see the reference manual.

• C* assertions are written in backtick logical terms, of type hprophprop; the math notation corresponds one by one: is ****, is data_atdata_at (with an added C-type argument), is |--|--;
• inside the backticks is HOL Light’s higher-order logic: everything is a term, application is curried, a formula is a boolbool term, and a thmthm can only come from the kernel’s inference rules;
• a global proof declaration [[cst::proof]] term/thm name = ...;[[cst::proof]] term/thm name = ...; is a verification-time declaration, usable as a scratchpad for writing assertions and definitions;
• fact()fact() characterizes the empty heap, pure()pure() places no constraint on the heap; symbolic states and contracts conventionally use factfact together with ****;
• assertions are shallowly embedded in HOL: hprop = mem -> boolhprop = mem -> bool, and the algebraic laws are all theorems, not axioms;
• the connection with C semantics is a set of conventions: data_atdata_at builds in alignment and value range, an array element’s address has the form + * sizeof() + * sizeof(), structs enter the logic via TT/FF-prefixed constants and field_addrfield_addr, and program variables enter assertions via __addr__addr/__pre__pre/__return__return;
• representation predicates associate a block of memory with a pure mathematical value: new_fun_definitionnew_fun_definition defines non-recursive predicates, new_rec_definitionnew_rec_definition defines recursively along a datatype (like sllsll, store_treestore_tree), and new_datatype_definitionnew_datatype_definition defines new inductive types.