Function Contracts, Loop Invariants, and Assertions

In the previous section we learned to write spatial assertions in C*, and used the definition mechanisms to define representation predicates for linked lists and trees. This section puts assertions into programs: function contracts ([[cst::require]][[cst::require]], [[cst::ensure]][[cst::ensure]]), loop invariants ([[cst::invariant]][[cst::invariant]]), and inline assertions ([[cst::assert]][[cst::assert]]). They are the three homes for assertions inside a program—once written, C* can check them statement by statement along the program.

Recall the absolute-value function from Your First C* Program:

int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{ ... }

int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{ ... }

We have already seen the syntactic elements of a contract; here we state the reading conventions formally:

• a contract is written after the parameter list and before the function body (for a declaration that is only a prototype, before the semicolon);
• [[cst::require(...)]][[cst::require(...)]] is the precondition: an assertion that holds when the function begins executing—it characterizes the memory resources the function operates on and constrains the input;
• [[cst::ensure(...)]][[cst::ensure(...)]] is the postcondition: an assertion that holds when the function returns—it characterizes the memory resources at return, and describes the return value with __return__return;
• writing a parameter name directly in a contract (such as xx) refers to the value of that parameter at the function entry.

A contract is a two-way agreement: for the implementer it is an obligation that every returning path of the function must fulfill; for the caller it is an assumption that can be relied on without reading the function body—so the check at a call site only needs to consult the contract, not the implementation.

Here is another example that also involves only scalar local variables on the stack, the McCarthy 91 function:

int mc91(int n)
    [[cst::require(`fact(0i <= n)`)]]
    [[cst::ensure(`fact(n > 100i && __return == n - 10i) ||
                   fact(n <= 100i && __return == 91i)`)]]
{
  if (n > 100) {
    return n - 10;
  };
  int r1 = mc91(n + 11);
  int r2 = mc91(r1);
  return r2;
}

int mc91(int n)
    [[cst::require(`fact(0i <= n)`)]]
    [[cst::ensure(`fact(n > 100i && __return == n - 10i) ||
                   fact(n <= 100i && __return == 91i)`)]]
{
  if (n > 100) {
    return n - 10;
  };
  int r1 = mc91(n + 11);
  int r2 = mc91(r1);
  return r2;
}

Two things are worth noticing in this example:

• First, conditional postconditions: when the conclusion varies with the input, use |||| to do a case split, with each branch conjoining the condition the input satisfies onto the spatial assertion via &&&& (both are empty heaps factfact in this example).
• Second, recursive calls are checked against the same contract: when verifying the recursive calls on lines 9 and 10, both are advanced solely on the basis of the contract above; you can observe the values of r1r1 and r2r2 by viewing the symbolic state in VSCode.

Also, as we will see when we discuss proofs later, a contract must be written strong enough; if it is too weak, the proof at the recursive site may fail to go through. This is similar to inductive proofs in mathematics: during a proof one often discovers a need to go back and strengthen the induction hypothesis.

Pointers are where contracts start to genuinely use spatial assertions. The most classic example is swapping two integers:

void swap(int *a, int *b)
    [[cst::param(`a_v:int`, `b_v:int`)]]
    [[cst::require(`data_at a Tint a_v ** data_at b Tint b_v`)]]
    [[cst::ensure(`data_at a Tint b_v ** data_at b Tint a_v`)]]
{
  int t = *a;
  *a = *b;
  *b = t;
}

void swap(int *a, int *b)
    [[cst::param(`a_v:int`, `b_v:int`)]]
    [[cst::require(`data_at a Tint a_v ** data_at b Tint b_v`)]]
    [[cst::ensure(`data_at a Tint b_v ** data_at b Tint a_v`)]]
{
  int t = *a;
  *a = *b;
  *b = t;
}

A third kind of contract annotation appears here: [[cst::param(...)]][[cst::param(...)]] declares logical parameters—extra parameters that exist only at the logical level. In this example, a_va_v and b_vb_v are the initial contents of the two memory locations: the program does not care what they actually are, but the postcondition needs to mention them in order to express the semantics of “swap”. In the current C*, logical parameters have no argument syntax at the call site: the symbolic execution engine (introduced in the next section) matches the callee’s requirerequire against the symbolic state at the call site (which is itself just the spatial assertion of separation logic) and infers the values of the logical parameters automatically.

Reading this contract from a resource point of view: the caller lends the two memory cells aa, bb to swapswap, and gets them back unchanged at return, only with their contents swapped. Note that the pointer parameter aa is used directly as an address in the assertion—the parameter’s value is itself an address; this is a different concept from the __addr__addr notation for local variables in loop invariants later (the address of the cell the variable itself occupies), so take care to distinguish them.

Another common role for pointers is as out-parameters. For instance, the extended Euclidean algorithm sends out the Bézout coefficients through two pointers:

int ext_gcd(int a, int b, int *x, int *y)
    [[cst::require(`fact(0i <= a) ** fact(0i <= b) **
                    undef_data_at x Tint ** undef_data_at y Tint`)]]
    [[cst::ensure(`exists xv yv.
                    data_at x Tint xv ** data_at y Tint yv **
                    fact(a * xv + b * yv == __return) **
                    fact(b == 0i ==> xv == 1i && yv == 0i) **
                    fact(1i <= b ==> --b <= xv && xv <= b) **
                    fact(1i <= b ==> (--a <= yv && yv <= a) || yv == 1i)`)]]
{ ... }

int ext_gcd(int a, int b, int *x, int *y)
    [[cst::require(`fact(0i <= a) ** fact(0i <= b) **
                    undef_data_at x Tint ** undef_data_at y Tint`)]]
    [[cst::ensure(`exists xv yv.
                    data_at x Tint xv ** data_at y Tint yv **
                    fact(a * xv + b * yv == __return) **
                    fact(b == 0i ==> xv == 1i && yv == 0i) **
                    fact(1i <= b ==> --b <= xv && xv <= b) **
                    fact(1i <= b ==> (--a <= yv && yv <= a) || yv == 1i)`)]]
{ ... }

Comparing with swapswap, we can summarize the two patterns of pointer contracts:

• in-parameter (a value that is already meaningful before the call): name the initial value with a logical parameter, e.g. data_at p Tint a_vdata_at p Tint a_v;
• out-parameter (a value produced only at return): the precondition only requires a writable memory cell undef_data_at x Tintundef_data_at x Tint (whose content may be uninitialized), and the postcondition introduces the content at return with an existential quantifier (e.g. exists xv yv.exists xv yv.), then states its properties with factfact, such as a * xv + b * yv == __returna * xv + b * yv == __return here.

The last three factfact lines of the postcondition are not conclusions the caller cares about, but specifications strengthened for the sake of the recursive call: when ext_gcdext_gcd calls itself recursively, the proof can only rely on this contract, and to complete some arithmetic reasoning in the function body, some extra constraints are needed. When writing the specification of a recursive function, one often has to “say a bit more” like this.

An array contract needs to talk about a segment of memory. Predicates such as array_atarray_at mentioned in the previous section are meant exactly for this, but writing them directly into a contract runs into a symbolic-execution-engine limitation (unfolded in the next section): in contracts and symbolic states, predicates other than data_atdata_at/undef_data_atundef_data_at may not carry a ctypectype parameter directly. The currently recommended solution is the definition mechanism mentioned in the previous section: wrap a layer that hides the ctypectype inside the definition body—a monomorphic wrapper predicate. Taking “zero out nn bytes” as an example:

[[cst::proof]] thm undef_bytes_def = new_fun_definition(
    `undef_bytes (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_bytes`);
[[cst::proof]] thm zero_bytes_def = new_fun_definition(
    `zero_bytes (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zero_bytes`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{ ... }

[[cst::proof]] thm undef_bytes_def = new_fun_definition(
    `undef_bytes (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_bytes`);
[[cst::proof]] thm zero_bytes_def = new_fun_definition(
    `zero_bytes (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zero_bytes`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{ ... }

The contract reads: given nn writable bytes starting at arrarr, the function ends with all nn bytes zeroed. Here ireplicate n 0iireplicate n 0i (a list of nn copies of 0i0i) is a pure function at the logical level. This is an idiom of specification: use a model function to describe the result over pure mathematical values, instead of enumerating memory cell by cell—the linked-list and tree contracts below will develop this method further.

Data-structure contracts build on the representation predicates defined in the previous section. The contract for reversing a singly-linked list in place is only three lines:

[[cst::proof]] int _sll = cst_add_const_to_header(`sll`);
[[cst::proof]] int _rev = cst_add_const_to_header(`REVERSE:(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{ ... }

[[cst::proof]] int _sll = cst_add_const_to_header(`sll`);
[[cst::proof]] int _rev = cst_add_const_to_header(`REVERSE:(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{ ... }

The logical parameter ll is the logical content of the linked list—a pure HOL list; REVERSEREVERSE is a ready-made function from the HOL list library. The whole contract reads: “give me a linked list with content ll, and I return you a linked list with content REVERSE lREVERSE l.” The implementation code may perform the reversal in any way it likes, as long as its behavior conforms to what the contract states. Logical parameters may be multiple, separated by commas: a function that concatenates two linked lists can declare [[cst::param(`l1:(int)list`, `l2:(int)list`)]][[cst::param(`l1:(int)list`, `l2:(int)list`)]], with a contract that sll p l1 ** sll q l2sll p l1 ** sll q l2 entails sll __return (l1 ++ l2)sll __return (l1 ++ l2).

Tree contracts are the same. The two examples below are taken from an AVL tree implementation (store_treestore_tree, theighttheight, avl_insertavl_insert are the tree’s representation predicate and model functions, respectively):

// Export every needed type and function via cst_add_const_to_header / cst_add_type_to_header
// *out = the height of the (possibly empty) subtree pointed to by nd.
void node_height_p(struct tree *nd, int *out)
    [[cst::param(`t0:tree`)]]
    [[cst::require(`store_tree nd t0 ** undef_data_at out Tint`)]]
    [[cst::ensure(`store_tree nd t0 ** data_at out Tint (theight t0)`)]];
// AVL insert: the tree pointed to by *root changes from t to avl_insert k t.
void insert(struct tree **root, int k)
    [[cst::param(`t:tree`)]]
    [[cst::require(`exists pv.
                      data_at root Tptr pv **
                      store_tree pv t **
                      fact(theight t <= 2147483646i)`)]]
    [[cst::ensure(`exists qv.
                     data_at root Tptr qv **
                     store_tree qv (avl_insert k t) **
                     fact(theight (avl_insert k t) <= theight t + 1i)`)]];

// Export every needed type and function via cst_add_const_to_header / cst_add_type_to_header
// *out = the height of the (possibly empty) subtree pointed to by nd.
void node_height_p(struct tree *nd, int *out)
    [[cst::param(`t0:tree`)]]
    [[cst::require(`store_tree nd t0 ** undef_data_at out Tint`)]]
    [[cst::ensure(`store_tree nd t0 ** data_at out Tint (theight t0)`)]];
// AVL insert: the tree pointed to by *root changes from t to avl_insert k t.
void insert(struct tree **root, int k)
    [[cst::param(`t:tree`)]]
    [[cst::require(`exists pv.
                      data_at root Tptr pv **
                      store_tree pv t **
                      fact(theight t <= 2147483646i)`)]]
    [[cst::ensure(`exists qv.
                     data_at root Tptr qv **
                     store_tree qv (avl_insert k t) **
                     fact(theight (avl_insert k t) <= theight t + 1i)`)]];

Points worth noting, one by one:

• These two contracts are annotated on function prototypes (note the trailing semicolon): that is, a specification may be written on a function prototype in a header file (though at present the function definition site still needs to repeat the same contract, and a macro can ease the burden). Placing the interface together with the specification is also just as C conventionally does; in C* we likewise recommend organizing multi-module projects with header files.
• node_height_pnode_height_p is a read-only function: store_tree nd t0store_tree nd t0 appears unchanged in both pre- and postcondition, indicating that the tree is borrowed and returned unchanged.
• insertinsert’s parameter is a double pointer: exists pv. data_at root Tptr pv ** store_tree pv texists pv. data_at root Tptr pv ** store_tree pv t characterizes the pointer cell pointed to by rootroot plus the whole tree that pointer points to.
• Functional correctness is compressed entirely into a single model-function application: store_tree qv (avl_insert k t)store_tree qv (avl_insert k t)—what the implementation on the heap did equals what the model did on pure values. This is “the specification is the model”: define the behavior of the data structure as a pure function (avl_insertavl_insert is defined by the definition mechanism of the previous section), and let the contract merely match the heap up with the model.

C*‘s symbolic execution engine advances the symbolic state statement by statement along the program, but how many rounds the loop body will execute is not known at verification time. Following the usual practice of Hoare logic, we need to provide a loop invariant: an assertion that holds each time control returns to the loop head. It is written between the while (...)while (...) condition and the loop body:

while (condition)
    [[cst::invariant(`...`)]]
{ loop body }

while (condition)
    [[cst::invariant(`...`)]]
{ loop body }

The engine’s use of the invariant is: before entering the loop, check that it holds (establishment); assuming it and the loop condition hold together, symbolically execute the loop body once, and check that it holds again at the end of the loop body (preservation); after the loop, continue advancing with “invariant + condition is false” as the new symbolic state. The key point: at the loop head, the engine only remembers the invariant—resources and facts not written in the invariant cease to exist once past the loop head. So the invariant must completely describe the symbolic state at the loop head.

First, a purely scalar teaching example—Gauss summation:

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

An invariant is usually composed of three kinds of ingredients, and this small example has all three:

• Resources: one data_atdata_at for each live variable. Variables that change (ss, ii) bind their current value svsv, iviv with existsexists; those that do not (nn) write the entry value n__pren__pre directly. Note that all of these use the explicit address form __addr__addr/__pre__pre, not the program variable name; this matches the form of the symbolic state shown in VSCode.
• Progress fact: 2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i)—the partial-sum formula, which collapses into the postcondition when the loop ends (iv == n__preiv == n__pre).
• Boundary facts: 0i <= iv0i <= iv, iv <= n__preiv <= n__pre, n__pre <= 1000in__pre <= 1000i. The first two let us conclude iv == n__preiv == n__pre on exit; the last comes from the precondition—but the precondition does not automatically pass through the loop head, and the verification condition that s + is + i does not overflow needs it, so it must be copied into the invariant to carry along.

Return to the earlier clearclear example. If it is implemented by iterating with a loop, then the invariant must characterize the “half-cleared” state, and for this we can first define another wrapper predicate—the suffix not yet zeroed:

[[cst::proof]] thm undef_suffix_def = new_fun_definition(
    `undef_suffix (x:addr) (i:int) (n:int) : hprop =
       undef_array_at (x + i * sizeof Tchar) Tchar (n - i)`);
[[cst::proof]] int _e3 = cst_add_const_to_header(`undef_suffix`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists iv.
                          data_at i__addr Tint iv **
                          data_at n__addr Tint n__pre **
                          data_at arr__addr Tptr arr__pre **
                          zero_bytes arr__pre iv **
                          undef_suffix arr__pre iv n__pre **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(n__pre <= 2147483647i)`)]]
  {
    char *p = arr + i;
    *p = 0;
    i = i + 1;
  }
}

[[cst::proof]] thm undef_suffix_def = new_fun_definition(
    `undef_suffix (x:addr) (i:int) (n:int) : hprop =
       undef_array_at (x + i * sizeof Tchar) Tchar (n - i)`);
[[cst::proof]] int _e3 = cst_add_const_to_header(`undef_suffix`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists iv.
                          data_at i__addr Tint iv **
                          data_at n__addr Tint n__pre **
                          data_at arr__addr Tptr arr__pre **
                          zero_bytes arr__pre iv **
                          undef_suffix arr__pre iv n__pre **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(n__pre <= 2147483647i)`)]]
  {
    char *p = arr + i;
    *p = 0;
    i = i + 1;
  }
}

The spatial part is the standard shape of a traversal-style invariant: processed prefix **** unprocessed suffix—zero_bytes arr__pre ivzero_bytes arr__pre iv plus undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre, the two segments joined together being exactly the whole memory segment characterized by the precondition. Each round the loop body peels one byte off the suffix, zeroes it, and merges it into the prefix, moving the boundary iviv between the two segments one cell to the right.

The definition of undef_suffixundef_suffix also hides a practical trick: the base address of the suffix is written in the definition body as x + i * sizeof Tcharx + i * sizeof Tchar. As said in the previous section, pointer arithmetic like arr + iarr + i unfolds in the logic into the sizeofsizeof form, and the matching of assertions against symbolic states is syntactic—hiding this form inside the definition body keeps the invariant clean on the surface, while the addresses produced during execution can still be conveniently matched by the symbolic execution engine.

An attentive reader may ask: the memory cell that *p = 0*p = 0 writes to is not directly given by an undef_data_atundef_data_at in the symbolic state—it is folded inside undef_suffixundef_suffix, and the symbolic execution engine will report an error when it reaches this step. This is exactly the problem that the inline assertion at the end of this section (or proof code in a later chapter) is meant to solve.

The climactic example is the complete program that reverses a linked list in place. We have already read the contract above; now look at the loop:

[[cst::proof]] int _app = cst_add_const_to_header(`APPEND:(A)list->(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = 0;
  struct list *v = p;
  while (v != 0)
      [[cst::invariant(`exists wv vv l1 l2.
                          data_at p__addr Tptr p__pre **
                          data_at w__addr Tptr wv **
                          data_at v__addr Tptr vv **
                          sll wv (REVERSE l1) **
                          sll vv l2 **
                          fact(l == l1 ++ l2)`)]]
  {
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}

[[cst::proof]] int _app = cst_add_const_to_header(`APPEND:(A)list->(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = 0;
  struct list *v = p;
  while (v != 0)
      [[cst::invariant(`exists wv vv l1 l2.
                          data_at p__addr Tptr p__pre **
                          data_at w__addr Tptr wv **
                          data_at v__addr Tptr vv **
                          sll wv (REVERSE l1) **
                          sll vv l2 **
                          fact(l == l1 ++ l2)`)]]
  {
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}

The invariant says: at any moment, the original linked list is split into two segments—ww points to the already-reversed prefix (content REVERSE l1REVERSE l1), and vv points to the not-yet-processed suffix (content l2l2); the pure fact l == l1 ++ l2l == l1 ++ l2 ties the two segments to the original list.

Walking through the engine’s three steps:

• Establishment: before entering the loop w == 0w == 0, v == pv == p; take l1 = []l1 = [], l2 = ll2 = l—the empty prefix reversed is still the empty list (sll 0i (REVERSE [])sll 0i (REVERSE []) is the empty heap), the suffix is the whole linked list, and l == [] ++ ll == [] ++ l is obvious.
• Preservation: when v != 0v != 0 the suffix is non-empty. The loop body first (in a proof block) unfolds the head node according to the definition of sllsll, obtaining the two data_atdata_at cells for headhead and tailtail; then v->tail = wv->tail = w attaches the head node to the already-reversed prefix, and ww, vv both move forward; finally it re-folds the two sllsll segments with l1' = l1 ++ [head element]l1' = l1 ++ [head element], l2' = taill2' = tail. Note that v->tailv->tail can be executed precisely because, after unfolding, the invariant has that data_atdata_at cell.
• Exit: when v == 0v == 0 the suffix is the empty list, l2 == []l2 == [], so l1 == ll1 == l, and the sll wv (REVERSE l)sll wv (REVERSE l) on the ww side is exactly the postcondition.

As in the array example, the field resource that v->tailv->tail needs is folded inside sll vv l2sll vv l2, and executing without unfolding it will report an error—the unfolding can be done with proof code, or advanced first with the inline assertion below.

The last annotation is [[cst::assert([[cst::assert(…)]])]]: written as a statement inside the function body, it asserts the symbolic state at that point. The engine processes it in two steps: first it checks that the current symbolic state entails the asserted state—this entailment becomes a verification condition; then it takes the asserted state as the new symbolic state and continues advancing. “Switch to another form and keep going”—this gives assertassert two uses.

In the loop bodies of clearclear and reversereverse above, symbolic execution is actually one step short: the resources in the invariant are in folded form (undef_suffixundef_suffix, sll vv l2sll vv l2), while *p = 0*p = 0 writes the cell that pp points to and v->tailv->tail reads the tailtail field of a node—the symbolic state does not directly give these data_atdata_at/undef_data_atundef_data_at resources, and the symbolic execution engine will report an error at these two places. Unfolding a predicate by its definition requires proof code (introduced in a later chapter); but before any proof is written, one can first insert an assertassert to rewrite the symbolic state into the “unfolded one step” form, letting execution proceed. The loop body of clearclear:

  {
    char *p = arr + i;
    [[cst::assert(`exists iv.
        fact(0i <= iv && iv < n__pre && n__pre <= 2147483647i) **
        data_at p__addr Tptr (arr__pre + iv * sizeof Tchar) **
        data_at i__addr Tint iv **
        data_at n__addr Tint n__pre **
        data_at arr__addr Tptr arr__pre **
        zero_bytes arr__pre iv **
        undef_data_at (arr__pre + iv * sizeof Tchar) Tchar **
        undef_suffix arr__pre (iv + 1i) n__pre`)]];
    *p = 0;
    i = i + 1;
  }

  {
    char *p = arr + i;
    [[cst::assert(`exists iv.
        fact(0i <= iv && iv < n__pre && n__pre <= 2147483647i) **
        data_at p__addr Tptr (arr__pre + iv * sizeof Tchar) **
        data_at i__addr Tint iv **
        data_at n__addr Tint n__pre **
        data_at arr__addr Tptr arr__pre **
        zero_bytes arr__pre iv **
        undef_data_at (arr__pre + iv * sizeof Tchar) Tchar **
        undef_suffix arr__pre (iv + 1i) n__pre`)]];
    *p = 0;
    i = i + 1;
  }

Compared with the invariant, this assertassert does three things: it writes the iv < n__preiv < n__pre brought by the loop condition into a factfact (after entering the loop body it already holds); it supplies the resource for the newly declared pp (whose value is precisely the sizeofsizeof-form address); and, most crucially, it splits undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre into the head byte undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar plus the remaining suffix undef_suffix arr__pre (iv + 1i) n__preundef_suffix arr__pre (iv + 1i) n__pre. After the assertassert, the cell resource that *p*p needs is laid out plainly in the symbolic state, and execution passes smoothly. Similarly, before reading v->tailv->tail, the loop body of reversereverse uses an assertassert to unfold sll vv l2sll vv l2 into the two cells of the head node plus the remaining list (vvvv is non-null, so l2l2 must be some x :: xsx :: xs):

  {
    [[cst::assert(`exists q x xs l1 vv wv.
        fact(~(vv == 0i) && l == l1 ++ x :: xs) **
        data_at p__addr Tptr p__pre **
        data_at w__addr Tptr wv **
        data_at v__addr Tptr vv **
        sll wv (REVERSE l1) **
        data_at (field_addr vv Tlist Fhead) Tint x **
        data_at (field_addr vv Tlist Ftail) Tptr q **
        sll q xs`)]];
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }

  {
    [[cst::assert(`exists q x xs l1 vv wv.
        fact(~(vv == 0i) && l == l1 ++ x :: xs) **
        data_at p__addr Tptr p__pre **
        data_at w__addr Tptr wv **
        data_at v__addr Tptr vv **
        sll wv (REVERSE l1) **
        data_at (field_addr vv Tlist Fhead) Tint x **
        data_at (field_addr vv Tlist Ftail) Tptr q **
        sll q xs`)]];
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }

Of course, there is no free lunch: “the old state entails the asserted state” becomes a verification condition awaiting proof (here it is precisely the step of unfolding undef_suffixundef_suffix/sllsll by definition)—the assertassert does not eliminate the proof obligation, it only turns it from “stuck execution” into “left for proof”. This is a very practical workflow in C*: first use assertassert to walk the whole function’s symbolic execution through and see all the verification conditions, then go back and fill in the proofs one by one.

[[cst::invariant]][[cst::invariant]] can only be attached to a whilewhile loop; forfor and do-whiledo-while loops instead use an assertassert inside the loop body as a “manual invariant”:

int mul(int x, int y)
    [[cst::require(`fact(1i <= x && x <= 100i) **
                    fact(1i <= y && y <= 100i)`)]]
    [[cst::ensure(`fact(__return == x * y)`)]]
{
  int ans = 0;
  do {
    ans += y;
    x--;
    [[cst::assert(`exists xv av.
        data_at x__addr Tint xv **
        data_at y__addr Tint y__pre **
        data_at ans__addr Tint av **
        fact(1i <= x__pre && x__pre <= 100i &&
             1i <= y__pre && y__pre <= 100i) **
        fact(0i <= xv && xv <= 99i) **
        fact(av + xv * y__pre == x__pre * y__pre)`)]];
  } while (x > 0);
  return ans;
}

int mul(int x, int y)
    [[cst::require(`fact(1i <= x && x <= 100i) **
                    fact(1i <= y && y <= 100i)`)]]
    [[cst::ensure(`fact(__return == x * y)`)]]
{
  int ans = 0;
  do {
    ans += y;
    x--;
    [[cst::assert(`exists xv av.
        data_at x__addr Tint xv **
        data_at y__addr Tint y__pre **
        data_at ans__addr Tint av **
        fact(1i <= x__pre && x__pre <= 100i &&
             1i <= y__pre && y__pre <= 100i) **
        fact(0i <= xv && xv <= 99i) **
        fact(av + xv * y__pre == x__pre * y__pre)`)]];
  } while (x > 0);
  return ans;
}

Just like invariantinvariant, the assertassert asserts the complete symbolic state at that program point, and the writing guidelines of the previous section apply equally.

• A function contract = [[cst::require]][[cst::require]] + [[cst::ensure]][[cst::ensure]] (aided by [[cst::param]][[cst::param]] logical parameters), written after the parameter list; a parameter name in a contract refers to the entry value, __return__return to the return value; a contract may be attached to a prototype; a prototype with a contract but no function body is an assumed spec, belonging to the trusted base.
• A pointer in-parameter names its initial value with a logical parameter (data_at p Tint a_vdata_at p Tint a_v); an out-parameter uses undef_data_atundef_data_at in the precondition and introduces the new value with existsexists in the postcondition.
• An array contract uses a monomorphic wrapper predicate to hide the ctypectype (an engine limitation); new constants and new types appearing in a contract must be exported (cst_add_const_to_headercst_add_const_to_header/cst_add_type_to_headercst_add_type_to_header).
• A data-structure contract = representation predicate + model function: “what the implementation on the heap did equals what the model did on pure values”.
• A loop invariant describes the complete symbolic state at the loop head; the standard shape for traversals is “processed prefix **** unprocessed suffix”, plus progress and boundary factfacts; five writing guidelines.
• [[cst::assert]][[cst::assert]] asserts and replaces the complete symbolic state at a point: it can rewrite resources into the form the engine needs before any proof is written, walking the symbolic execution through first (the entailment becoming a verification condition awaiting proof), and it also serves as a manual invariant for forfor/do-whiledo-while.