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 introduces the corresponding 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. We focus on writing assertions and predicates; proofs are covered in later chapters.

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:

The syntax differs from the mathematical notation in a few places:

• 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 connects the assertion to C semantics, as explained 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.

When practicing assertions, we want C* to parse and type-check them immediately. Assertions will eventually appear in contracts ([[cst::require]][[cst::require]] and similar annotations), whose rules we will cover later. For now, we can use a simpler form: the global proof declaration.

The [[cst::proof]][[cst::proof]] annotation marks code or declarations used only for verification: it can annotate a statement block inside a function body, [[cst::proof]] { ... }[[cst::proof]] { ... } (a proof block, used for writing proof code, covered in later chapters), or it can annotate a file-scope declaration, yielding a verification-time declaration — one that exists only at verification time and is absent from the compiled artifact. 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).

The following C* code lets us try an assertion:

#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. When you view the symbolic state on this line in VSCode, the HOL Light server parses and type-checks the assertion. A mistake, such as dropping the ii suffix, produces an immediate diagnostic explaining the type mismatch: a bare 4242 is a natural number (numnum), while an integer literal is written 42i42i. 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.

HOL Light lexes and parses the text inside backticks. Its conventions for terms, types, and formulas provide the basis for writing assertions and defining predicates. 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). HOL Light infers types, so a manual annotation is needed only when the context does not determine a type. 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

These notations apply at the boolbool layer. The assertion layer (hprophprop) has corresponding conjunction, disjunction, and quantifiers. By convention, C* writes boolbool-layer quantifiers as !!/?? and assertion-layer quantifiers as forallforall/existsexists to distinguish them when writing. Both layers print quantifiers as words, however, so in a dump the body’s type determines which layer a quantifier belongs to. The next section explains the use of &&&&/|||| at both layers. 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 central to HOL Light’s design: 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. This is how we obtain the thmthm values for representation predicates later in this section. Later chapters cover theorems and proofs in more detail.

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 express judgments about assertions: p |-- qp |-- q is a proposition about two assertions. The verification conditions shown in Your First C* Program have exactly this shape. The two groups of operators can occur in the same logical term. For example, we can write the previous section’s example, where relaxes an exact heap description to allow additional memory:

[[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 has type hprophprop; ex3ex3 has type boolbool and expresses a valid 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 defined within 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 . 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 proved as theorems from these definitions in C*‘s logic library, not additional axioms. Every step of reasoning about C* assertions can therefore be traced back to a proof accepted by the HOL Light kernel.

The mathematical notation says that address stores value . In C, we also need to specify the type of the stored value. intint and charchar occupy different numbers of bytes, and signed and unsigned types have different value ranges. The second argument of data_atdata_at specifies this type: it is a value of type ctypectype representing a C type in the logic. The following table lists common ctypectype constants and their sizeofsizeof:

TptrTptr uniformly represents pointer types (think of it as void *void *). The compound C types (structs, enums, unions, typedefs, arrays, function types) have ctypectype constructors too, but they seldom appear in an assertion: struct memory is reached field by field through field_addrfield_addr, introduced below, and TfunTfun appears only inside the fnspecfnspec of a function-pointer contract. 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 : in the byte-level memory model, it expands 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.

These validity constraints let us extract pure facts when needed. For example, the C* standard library provides the theorem:

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)

This theorem lets us extract the range of the stored value from a data_atdata_at resource whenever needed. 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.

Two further families of predicates accompany data_atdata_at:

• undef_data_at undef_data_at : address has an allocated location of type , but its content is uninitialized (corresponding to the NoninitNoninit state in the shallow embedding). 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 us to forget that a resource is initialized and treat it as uninitialized without compromising 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 separate an array element from the remainder (array_at_recarray_at_rec, array_at_missing_i_recarray_at_missing_i_rec, etc.), which we introduce as they are needed.

C programs use structstruct to define heap structures such as linked-list nodes. C* refers to structs in assertions through naming conventions. Consider this node type:

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.

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 need to refer to C program variables. The conventions introduced in Your First C* Program are summarized here:

• 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 — as in the symbolic state shown earlier:

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

The same conventions apply to pointer parameters: 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 follows the separation-logic requirement to characterize resources explicitly, using C*‘s conventions for C semantics.

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.

We use these logical variables with __addr__addr, __pre__pre, __return__return to write assertions in function contracts ([[cst::require]][[cst::require]], [[cst::ensure]][[cst::ensure]]) and loop invariants ([[cst::invariant]][[cst::invariant]]); the next section explains how to write these contracts and invariants.

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 in 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 verification-interface functions for these definitions. We call them in global proof declarations and obtain the thmthm corresponding to each definition.

new_fun_definitionnew_fun_definition defines a possibly recursive function or predicate from an equation and returns its definition theorem. The left side is a new constant applied to parameters; the right side is the definition body. 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 also be an assertion. For example, we can define a predicate for the single linked-list node described by ex4ex4:

[[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)`);

After this definition, 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) — type inference has no prior information about a new constant, so it is good practice to write out the types in full;
• 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 type error about ==; the diagnostic hints that one side is probably an hprophprop, which is the clue to look for.

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 a complete definition of the standard singly-linked list predicate 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.

This definition differs from the previous section’s in two ways. First, disjunction becomes pattern matching: the mathematical definition distinguishes the two cases with , whereas here separate clauses follow the list constructors [][], CONSCONS. This is the standard form of a HOL recursive definition. The first argument, get_theorem_by_name("list_RECURSION")get_theorem_by_name("list_RECURSION"), retrieves the list type’s recursion theorem by name from the theorem library. This theorem guarantees that the definition by cases is well-defined. Second, the predicate gains a content parameter: only says “the shape is valid”, whereas sll pt lsll pt l also describes what the linked list stores. This parameter lets us state functional correctness, for example that a reversal function reverses the list.

HOL’s existing list type can represent the contents of a linked list. For a tree structure, we first define 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, which can be passed directly as the first argument of new_rec_definitionnew_rec_definition; ty.indty.ind is the induction theorem, used later for inductive proofs. Order matters at file scope: a [[cst::proof]][[cst::proof]] global must be defined above its first use, and a definition that mentions ty.recty.rec before the line defining tyty is rejected at compile time with a message pointing at both lines. With this datatype and the corresponding C struct, we can define the binary-tree representation predicate:

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 be written in C* as a contract using store_treestore_tree.

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 functions and predicates, including recursive definitions whose admissibility conditions it can discharge automatically, 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.