Function Contracts, Loop Invariants, and Assertions

In the previous section, we wrote 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]]). These annotations place assertions at three kinds of program points, where C* checks them as it proceeds through the program statement by statement.

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 syntax of a contract. Here is what each part means:

• 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 specifies the implementer’s obligations and the caller’s assumptions. The implementer must satisfy it on every returning path; the caller can rely on it without reading the function body. Checking a call site therefore requires only the contract.

The McCarthy 91 function gives another example involving only scalar local variables on the stack:

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;
}

The example illustrates two features:

• First, conditional postconditions: when the conclusion varies with the input, use |||| to combine the branches. Within each factfact, &&&& conjoins a pure condition on the input with a pure condition on the result.
• Second, recursive calls are checked against the same contract: verification of the recursive calls on lines 9 and 10 uses only the contract above. You can inspect the values of r1r1 and r2r2 in the symbolic state shown in VSCode.

As we will see when discussing proofs, the contract must be strong enough to support the reasoning at recursive calls. Otherwise, the proof may fail. This resembles induction in mathematics, where completing a proof may require strengthening the induction hypothesis.

Spatial assertions describe the memory addressed by pointer parameters. A standard example swaps 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. Here, a_va_v and b_vb_v are the initial contents of the two memory locations. The program does not need their specific values, but the postcondition must refer to them to specify the swap. Logical parameters are normally not passed 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 their values automatically. When that match is ambiguous, the annotation [[cst::where(`v`, `e`)]][[cst::where(`v`, `e`)]] placed before the calling statement supplies one logical argument explicitly, and [[cst::where_type(`:T`, `:ty`)]][[cst::where_type(`:T`, `:ty`)]] does the same for a type parameter.

In terms of resources, the caller lends the two memory cells aa, bb to swapswap and receives the same cells back, with their contents swapped. The pointer parameter aa serves directly as an address in the assertion because its value is an address. The notation __addr__addr used later in loop invariants instead denotes the address of the memory cell occupied by a local variable itself.

Pointers also serve as out-parameters. For example, the extended Euclidean algorithm returns 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)`)]]
{ ... }

Together with swapswap, this illustrates two patterns for 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 strengthen the specification for recursive calls, rather than state the conclusions of interest to the caller. When ext_gcdext_gcd calls itself, its proof can rely only on this contract, so these extra constraints are needed for arithmetic reasoning in the function body. Specifications of recursive functions often need such additional properties.

An array contract describes a segment of memory. Predicates such as array_atarray_at, introduced in the previous section, serve this purpose. Their direct use in contracts is subject to a limitation of the symbolic execution engine (explained 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 current recommendation is to use the definition mechanism from the previous section to define a monomorphic wrapper predicate that hides the ctypectype in its body. For example, consider a function that zeroes nn bytes:

[[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. A common specification technique is to use a model function to describe the result over pure mathematical values without enumerating individual memory cells. The linked-list and tree contracts below give further examples.

Data-structure contracts use the representation predicates defined in the previous section. The following three-line contract specifies reversal of a singly-linked list in place:

[[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 linked list’s logical content, represented as a pure HOL list; REVERSEREVERSE is a function from the HOL list library. The contract states that the function takes a linked list with content ll and returns a linked list with content REVERSE lREVERSE l. The implementation may reverse the list in any way that satisfies this contract. 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 requiring sll p l1 ** sll q l2sll p l1 ** sll q l2 before execution and ensuring sll __return (l1 ++ l2)sll __return (l1 ++ l2) when the function returns.

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

// 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)`)]];

These contracts illustrate four points:

• Both contracts appear on function prototypes, as the trailing semicolons indicate. A specification can therefore appear in a header file, although the function definition must currently repeat the same contract; a macro can reduce this repetition. Keeping interfaces and specifications together follows C conventions, and we also recommend header files for organizing multi-module C* projects.
• 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.
• The model-function application in store_tree qv (avl_insert k t)store_tree qv (avl_insert k t) specifies functional correctness: the heap implementation must produce the result described by the model on pure values. To use this approach, define the data structure’s behavior as a pure function (avl_insertavl_insert uses the definition mechanism from the previous section), then use the contract to relate the heap to the model.

C*‘s symbolic execution engine advances the symbolic state statement by statement, but the number of loop iterations 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 first checks that the invariant holds before entering the loop (establishment). It then assumes the invariant and the loop condition, symbolically executes the body once, and checks that the invariant holds again at the end (preservation). After the loop, it continues from a symbolic state consisting of the invariant and the negated loop condition. At the loop head, the engine retains only the invariant. Resources and facts omitted from it are no longer available in the symbolic state, so the invariant must describe that state completely.

Consider Gauss summation as a scalar example:

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;
}

Loop invariants usually contain three kinds of assertions, all present in this example:

• Resources: one data_atdata_at for each live variable. For variables that change (ss, ii), use existsexists to bind their current values svsv, iviv; for variables that remain unchanged (nn), use the entry value n__pren__pre directly. These assertions use the explicit forms __addr__addr/__pre__pre rather than program variable names, matching the symbolic state shown in VSCode.
• Progress fact: 2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i) is the partial-sum formula. At loop exit (iv == n__preiv == n__pre), it gives the postcondition.
• Boundary facts: 0i <= iv0i <= iv, iv <= n__preiv <= n__pre, n__pre <= 1000in__pre <= 1000i. The first two imply iv == n__preiv == n__pre at exit. The last comes from the precondition and is needed to verify that s + is + i does not overflow. Since the precondition is not automatically retained at the loop head, this fact must also appear in the invariant.

For a loop implementation of clearclear, the invariant must describe the array while it is being cleared. We first define a wrapper predicate for the suffix that has yet to be 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 has the standard form for a traversal invariant: processed prefix **** unprocessed suffix. Together, zero_bytes arr__pre ivzero_bytes arr__pre iv and undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre describe the entire memory segment from the precondition. Each iteration takes one byte from the suffix, zeroes it, and adds it to the prefix, moving the boundary iviv one cell to the right.

The definition of undef_suffixundef_suffix uses a practical technique: it expresses the suffix’s base address as x + i * sizeof Tcharx + i * sizeof Tchar. As explained in the previous section, pointer arithmetic such as arr + iarr + i expands to the sizeofsizeof form in the logic. Assertions are matched against symbolic states syntactically. Keeping this address expression inside the definition makes the invariant concise while allowing the symbolic execution engine to match addresses produced during execution.

The example still needs one step: the memory cell written by *p = 0*p = 0 has no undef_data_atundef_data_at resource directly available in the symbolic state. It is folded inside undef_suffixundef_suffix, so the symbolic execution engine reports an error at this statement. The inline assertions introduced at the end of this section, or proof code introduced in a later chapter, address this problem.

Now consider the loop in the program that reverses a linked list in place, using the contract given above:

[[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 splits the original linked list into two segments: ww points to the reversed prefix with content REVERSE l1REVERSE l1, and vv points to the unprocessed suffix with content l2l2. The pure fact l == l1 ++ l2l == l1 ++ l2 relates these segments to the original list.

The engine checks this invariant in three steps:

• Establishment: before the loop, w == 0w == 0 and v == pv == p. Choose l1 = []l1 = [], l2 = ll2 = l. Reversing the empty prefix gives the empty list (sll 0i (REVERSE [])sll 0i (REVERSE []) is the empty heap), the suffix is the whole linked list, and l == [] ++ ll == [] ++ l holds.
• Preservation: when v != 0v != 0, the suffix is non-empty. A proof block first unfolds its head node using the definition of sllsll, yielding the two data_atdata_at cells for headhead and tailtail. The assignment v->tail = wv->tail = w then attaches the head node to the reversed prefix, and ww, vv both move forward. Finally, the proof refolds the two sllsll segments with l1' = l1 ++ [head element]l1' = l1 ++ [head element], l2' = taill2' = tail. Accessing v->tailv->tail is possible because unfolding exposes the required data_atdata_at cell.
• Exit: when v == 0v == 0, the suffix is empty: l2 == []l2 == []. Hence l1 == ll1 == l, and sll wv (REVERSE l)sll wv (REVERSE l) on the ww side gives the postcondition.

As in the array example, the field resource needed by v->tailv->tail is folded inside sll vv l2sll vv l2. Symbolic execution reports an error unless it is unfolded. Proof code can perform the unfolding, or the inline assertion below can allow execution to proceed first.

The final annotation, [[cst::assert(`...`)]][[cst::assert(`...`)]], is written as a statement inside a function body and asserts the symbolic state at that point. The engine processes it in two steps: it generates a verification condition stating that the current symbolic state entails the asserted state, then takes the asserted state as the new symbolic state and continues. This replacement of the symbolic state gives assertassert two uses.

Symbolic execution of the clearclear and reversereverse loop bodies above needs resources that are still folded in the invariant (undef_suffixundef_suffix, sll vv l2sll vv l2). The statement *p = 0*p = 0 writes the cell addressed by pp, and v->tailv->tail reads a node’s tailtail field. Since the symbolic state does not directly contain the corresponding data_atdata_at/undef_data_atundef_data_at resources, the engine reports errors at these statements. Unfolding a predicate by its definition requires proof code, introduced in a later chapter. Before writing that proof, we can insert an assertassert that rewrites the symbolic state into the form obtained by one unfolding step, allowing execution to proceed. For clearclear, the loop body becomes:

  {
    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 makes three changes: it records the loop condition iv < n__preiv < n__pre in a factfact, which already holds on entry to the body; it adds the resource for the newly declared pp, whose value is the address in sizeofsizeof form; and it splits undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre into the first byte, undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar, and the remaining suffix, undef_suffix arr__pre (iv + 1i) n__preundef_suffix arr__pre (iv + 1i) n__pre. After the assertassert, the symbolic state explicitly contains the cell resource needed by *p*p, so execution can proceed. 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;
  }

The entailment from the old state to the asserted state remains a verification condition awaiting proof. Here, that proof requires unfolding undef_suffixundef_suffix/sllsll by definition. The assertassert allows symbolic execution to continue while retaining the proof obligation for later. This gives a practical C* workflow: use assertassert to complete symbolic execution of the function and inspect all verification conditions, then prove them one by one.

[[cst::invariant]][[cst::invariant]] also attaches to forfor and do-whiledo-while loops, as it does to whilewhile loops. A forfor header may not declare a variable, so use int i; for (i = 0; …)int i; for (i = 0; …). For a do-whiledo-while loop, the invariant is checked at the test, after the body. An assertassert at the same point can serve as a manual invariant, as in the following example:

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;
}

Like invariantinvariant, the assertassert describes the complete symbolic state at that point, so the invariant-writing guidelines above also apply.

• A function contract combines [[cst::require]][[cst::require]] and [[cst::ensure]][[cst::ensure]], with logical parameters declared by [[cst::param]][[cst::param]], and appears after the parameter list. Parameter names denote entry values, and __return__return denotes the return value. Contracts can also appear on prototypes; a prototype with a contract but no function body is an assumed spec and belongs 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 combines a representation predicate with a model function: the heap implementation must agree with the model’s behavior on pure values.
• A loop invariant describes the complete symbolic state at the loop head. Traversal invariants typically have the form “processed prefix **** unprocessed suffix”, together with progress and boundary factfacts, and should follow the five guidelines above.
• [[cst::assert]][[cst::assert]] asserts and replaces the complete symbolic state at a point. It can put resources into the form needed by the engine before a proof is written, allowing symbolic execution to proceed while leaving the entailment as a verification condition. It can also serve as a manual invariant inside a loop body.
• [[cst::where]][[cst::where]] passes one logical argument explicitly at a call when matching would be ambiguous; [[cst::given]][[cst::given]] names the existential witnesses of the current state so that an assertassert, a wherewhere, or an inner loop’s invariant can mention them.