Forward Proof in C*

In the previous section, we represented proofs as programs in a metalanguage. Forward proof starts from axioms and known theorems and applies inference rules until it derives the desired conclusion. The metalanguage there was ML; in C*, proofs are written in [[cst::proof]][[cst::proof]] blocks in C code. We now explain how C connects to HOL Light and how to construct forward proofs in C*. We consider two kinds of forward proof: general proofs, involving only logic and arithmetic, and separation-logic proofs. This section covers forward proof construction; later sections introduce backward (goal-directed) tactics and the operational style.

Classic LCF uses ML as its metalanguage: a proof is an ML program, and thmthm is an abstract type whose values only the kernel can construct. C* uses C itself as the proof language: the code in a [[cst::proof]][[cst::proof]] block is a proof program. This presents a problem. The theorem security described in the previous section relies on the host language’s type abstraction, which C does not provide: pointer arithmetic and casts can bypass an interface and directly overwrite a thmthm’s conclusion, forging a theorem.

C* addresses this problem by running the proof code and the kernel in separate processes that communicate through a guarded interface—a client/server model:

• The client is the C proof code in [[cst::proof]][[cst::proof]]. It holds only opaque handles to logical objects stored on the server. On the C side, termterm, thmthm, and typetype are opaque types: proof code passes them through interface functions and cannot inspect or modify the objects they represent.
• The server is a separate process containing HOL Light and its trusted kernel, together with an object store that maps handles to logical objects.

A call such as mp_rule(h1, h2)mp_rule(h1, h2) is a remote procedure call. The server resolves h1h1, h2h2 to the corresponding theorems, passes them to the kernel to apply the primitive inference rules, stores the resulting theorem, and returns a fresh handle. Process isolation prevents the client from accessing logical objects in the server process, even if the client misuses pointers. The trusted computing base (TCB) therefore remains the small kernel. The full expansiveness described in the previous section also extends to C: whatever a [[cst::proof]][[cst::proof]] block contains, every theorem it produces is ultimately constructed by the kernel’s primitive rules.

The proof standard library follows a naming convention: *_rule*_rule constructs theorems forward, *_conv*_conv (conversion) maps a term to an equality theorem, and *_TAC*_TAC denotes a backward (goal-directed) tactic. Later sections cover these tactics. In practice, a forward proof is a sequence of calls to *_rule*_rule and conversions. The following examples show the basic operations for constructing theorems, all within [[cst::proof]][[cst::proof]] declarations:

#include "proof/proof.h"
[[cst::proof]] term t1 = `x + 1`;                     // backquotes: write a logical term directly
[[cst::proof]] term t2 = parse_term("x + 1");         // or parse from a string
[[cst::proof]] type ty = type_of(t1);
[[cst::proof]] thm r1 = refl_rule(`x + 1`);           // |- x + 1 = x + 1
[[cst::proof]] thm r2 = assume_rule(`x + 1 == y`);    // x + 1 == y |- x + 1 == y
[[cst::proof]] thm r3 = sym_rule(r2);                 // forward: flip the equation
[[cst::proof]] thm r4 = arith_rule(`a + b == b + a`); // linear-arithmetic decision procedure
[[cst::proof]] thm r5 = apply_conversion(             // apply a conversion to a term
    once_rewrite_conv(THM_LIST(r4)), `(a + b) * c`);

#include "proof/proof.h"
[[cst::proof]] term t1 = `x + 1`;                     // backquotes: write a logical term directly
[[cst::proof]] term t2 = parse_term("x + 1");         // or parse from a string
[[cst::proof]] type ty = type_of(t1);
[[cst::proof]] thm r1 = refl_rule(`x + 1`);           // |- x + 1 = x + 1
[[cst::proof]] thm r2 = assume_rule(`x + 1 == y`);    // x + 1 == y |- x + 1 == y
[[cst::proof]] thm r3 = sym_rule(r2);                 // forward: flip the equation
[[cst::proof]] thm r4 = arith_rule(`a + b == b + a`); // linear-arithmetic decision procedure
[[cst::proof]] thm r5 = apply_conversion(             // apply a conversion to a term
    once_rewrite_conv(THM_LIST(r4)), `(a + b) * c`);

Each *_rule*_rule returns a thmthm; apply_conversion(<conv>, <term>)apply_conversion(<conv>, <term>) computes an equality using the conversion and returns it as a thmthm. The definition mechanisms introduced in Separation Logic in C* define new constants, functions, and datatypes. They are all conservative extensions and return the corresponding definition, recursion, or induction theorems:

[[cst::proof]] indtype nlist = new_datatype_definition(
    "nlist = nil | cons num nlist");
[[cst::proof]] thm app_def = new_rec_definition(nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);

[[cst::proof]] indtype nlist = new_datatype_definition(
    "nlist = nil | cons num nlist");
[[cst::proof]] thm app_def = new_rec_definition(nlist.rec,
    `app nil l = l &&
     app (cons h t) l = cons h (app t l)`);

We can now prove forall l. app l nil = lforall l. app l nil = l, the right identity of appapp, by constructing a theorem from the bottom up without setting up a goal:

[[cst::proof]] thm app_nil_r(void) {
  // base case: |- app nil nil = nil, by rewriting with app's definition
  thm base_eq = apply_conversion(rewrite_conv(THM_LIST(app_def)), `app nil nil`);
  // inductive step: rewrite under the induction hypothesis ih, then generalize + discharge
  thm ih = assume_rule(`app t nil = t`);
  thm step_eq = apply_conversion(
      rewrite_conv(THM_LIST(app_def, ih)), `app (cons h t) nil`);
  step_eq = gen_all_rule(disch_all_rule(step_eq));
  // instantiate the induction theorem to our predicate, then feed it base and step
  thm ind_thm = beta_rule(spec_rule(`\l. app l nil = l`, nlist.ind));
  thm result  = mp_rule(ind_thm, conj_rule(base_eq, step_eq));
  //  |- forall l. app l nil = l
  return result;
}
[[cst::proof]] thm app_nil_r_thm = app_nil_r();

[[cst::proof]] thm app_nil_r(void) {
  // base case: |- app nil nil = nil, by rewriting with app's definition
  thm base_eq = apply_conversion(rewrite_conv(THM_LIST(app_def)), `app nil nil`);
  // inductive step: rewrite under the induction hypothesis ih, then generalize + discharge
  thm ih = assume_rule(`app t nil = t`);
  thm step_eq = apply_conversion(
      rewrite_conv(THM_LIST(app_def, ih)), `app (cons h t) nil`);
  step_eq = gen_all_rule(disch_all_rule(step_eq));
  // instantiate the induction theorem to our predicate, then feed it base and step
  thm ind_thm = beta_rule(spec_rule(`\l. app l nil = l`, nlist.ind));
  thm result  = mp_rule(ind_thm, conj_rule(base_eq, step_eq));
  //  |- forall l. app l nil = l
  return result;
}
[[cst::proof]] thm app_nil_r_thm = app_nil_r();

(A bare block cannot appear at file scope, so the proof lives in a ghost function returning the theorem, and the declaration after it runs the function.) Each step produces a new theorem from existing ones. Rewriting with app_defapp_def gives base_eqbase_eq and step_eqstep_eq. The theorem ind_thmind_thm is obtained from the datatype’s induction theorem nlist.indnlist.ind, specialized to \l. app l nil = l\l. app l nil = l by spec_rulespec_rule (instantiation) and beta_rulebeta_rule (-reduction). Finally, conj_ruleconj_rule combines the base case and inductive step into a conjunction, and mp_rulemp_rule (modus ponens) applies the induction theorem to this conjunction to obtain resultresult. This is forward proof: start at the leaves, which are known theorems, and construct the derivation upward to the desired conclusion.

The appapp example is a purely logical calculation; it does not yet verify a C program. Recall from Verification Condition Generation that when the symbolic-execution engine reaches a [[cst::proof]][[cst::proof]] block, it holds a symbolic state and may have generated a verification condition (VC) to prove. To use forward proof here, we read the current symbolic state, construct a theorem, and apply it to advance the state. Three interface functions suffice: cst_get_symbolic_state()cst_get_symbolic_state() reads the current state as an assertion, cst_set_symbolic_state(...)cst_set_symbolic_state(...) installs an entailment from the current state to a new state, and eq2ent(...)eq2ent(...) converts an equality theorem into such an entailment.

The following program twicetwice computes (n+1) + (n-1)(n+1) + (n-1). Its specification requires the result to equal doubl(n)doubl(n), where doubl(x) = x + xdoubl(x) = x + x is a logical function defined and exported with new_fun_definitionnew_fun_definition.

#include "proof/proof.h"
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);
[[cst::proof]] int _e = cst_add_const_to_header(`doubl`);
int twice(int n)
    [[cst::require(`fact(0i <= n && n <= 100i)`)]]
    [[cst::ensure(`fact(__return == doubl(n))`)]]
{
  int a = n + 1;
  int b = n - 1;
  int r = a + b;
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm eq = int_arith_rule(`(a + 1i) + (b - 1i) == (a + b)`);    // build an equality forward
    thm st_eq = apply_conversion(rewrite_conv(THM_LIST(eq)), st); // rewrite the state
    cst_set_symbolic_state(eq2ent(st_eq));                        // advance
  }
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm st_eq = apply_conversion(
        rewrite_conv(THM_LIST(sym_rule(doubl_def))), st);         // rewrite by doubl's definition
    cst_set_symbolic_state(eq2ent(st_eq));
  }
  return r;
}

#include "proof/proof.h"
[[cst::proof]] thm doubl_def = new_fun_definition(`doubl(x:int) = x + x`);
[[cst::proof]] int _e = cst_add_const_to_header(`doubl`);
int twice(int n)
    [[cst::require(`fact(0i <= n && n <= 100i)`)]]
    [[cst::ensure(`fact(__return == doubl(n))`)]]
{
  int a = n + 1;
  int b = n - 1;
  int r = a + b;
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm eq = int_arith_rule(`(a + 1i) + (b - 1i) == (a + b)`);    // build an equality forward
    thm st_eq = apply_conversion(rewrite_conv(THM_LIST(eq)), st); // rewrite the state
    cst_set_symbolic_state(eq2ent(st_eq));                        // advance
  }
  [[cst::proof]] {
    term st = cst_get_symbolic_state();
    thm st_eq = apply_conversion(
        rewrite_conv(THM_LIST(sym_rule(doubl_def))), st);         // rewrite by doubl's definition
    cst_set_symbolic_state(eq2ent(st_eq));
  }
  return r;
}

Both proof blocks follow the same steps: read the state, construct an equality theorem forward, rewrite the state, and install the result. The first block simplifies (a+1) + (b-1)(a+1) + (b-1) to a + ba + b. The second uses the definition of doubldoubl, reversed by sym_rulesym_rule to x + x == doubl(x)x + x == doubl(x), to rewrite a + ba + b as doubl(n)doubl(n). After these steps, the return value in the symbolic state is doubl(n)doubl(n), and the final VC is discharged.

When developing the two proof blocks above, we inspect the symbolic state to see how each step changes it. C*‘s VSCode extension provides this feedback.

Right-click a line and choose Show Symbolic StateShow Symbolic State (shortcut alt+rightalt+right, or ctrl+alt+rightctrl+alt+right on macOS, as in Your First C* Program). The right panel shows the symbolic state after that line executes. At a function’s exit or the end of the file, it instead shows the pending verification condition, of the form … |-- …… |-- …. Inside a proof block, it shows the state after the queried proof step. A file-scope proof function’s body has no symbolic state and does not support this query.

Take twicetwice. Querying the line int r = a + b;int r = a + b; shows:

The cell for rr contains the unsimplified sum (n+1) + (n-1)(n+1) + (n-1), while the postcondition requires it to equal doubl(n)doubl(n). We can develop the proof by repeating these steps:

1. Look at the state: use Show Symbolic StateShow Symbolic State on the lines around a proof block to identify what remains to be proved;
2. Find a tool: locate a suitable lemma or conversion. C*‘s toolchain can search thousands of named theorems and conversions by name or statement, such as the defining theorem of doubldoubl or an integer-arithmetic decision procedure;
3. Write a forward block: in [[cst::proof]][[cst::proof]], build theorems with *_rule*_rule/*_slrule*_slrule/conversions and advance the state with local_applylocal_apply or cst_set_symbolic_statecst_set_symbolic_state;
4. Look again: use Show Symbolic StateShow Symbolic State to confirm that the state changed as expected, and check at the end of the file whether the verification conditions have been cleared;
5. Repeat until every verification condition is discharged.

When a rule fails, the error message gives its name and arguments and explains the mismatch. For example, if the term supplied to spec_rulespec_rule does not match the outermost bound variable, the message prints both with their types. This information usually indicates how to correct the proof.

After adding the two proof blocks in twicetwice, querying the last line of the second block shows:

The cell for rr now contains doubl n__predoubl n__pre, and the final verification condition is cleared. Forward-proof development is state-driven: inspect the current state and derive successive states until the postcondition holds.

We next apply these operations to a complete recursive program. The McCarthy 91 function returns n - 10n - 10 when n > 100n > 100, and 9191 otherwise.

#include "proof/proof.h"
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) {
    [[cst::proof]] {
      // extract the value range implied by n's data_at cell, merge it into the state
      thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                      get_theorem_by_name("max_of_def")),
          spec_rule(`n__pre:int`, spec_rule(`Tint`,
              spec_rule(`n__addr:int`, get_data_at_range()))));
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    }
    return n - 10;
  }
  return mc91(mc91(n + 11));
}

#include "proof/proof.h"
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) {
    [[cst::proof]] {
      // extract the value range implied by n's data_at cell, merge it into the state
      thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                      get_theorem_by_name("max_of_def")),
          spec_rule(`n__pre:int`, spec_rule(`Tint`,
              spec_rule(`n__addr:int`, get_data_at_range()))));
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    }
    return n - 10;
  }
  return mc91(mc91(n + 11));
}

The postcondition uses **** to conjoin two conditional facts, specifying the return value for the n > 100n > 100 and n <= 100n <= 100 cases.

The proof block in the n > 100n > 100 branch makes the parameter’s value range explicit. The entry condition supplies only fact(0i <= n)fact(0i <= n). The symbolic state also contains the cell for nn, namely data_at n__addr Tint n__predata_at n__addr Tint n__pre, and an intint cell implies that n__pren__pre lies within the bounds of intint. The generic lemma get_data_at_range()get_data_at_range() states this property. The three nested spec_rulespec_rules instantiate it with the address of nn, the type TintTint, and the value n__pren__pre. The enclosing rewrite_rulerewrite_rule uses the definitions of min_ofmin_of/max_ofmax_of to express the bounds as concrete numerals, and local_applylocal_apply adds the resulting range fact to the state.

To see why the proof block is needed, delete it and query the verification condition at the function’s exit. The panel shows:

This is the intint overflow check for n - 10n - 10. The two antecedent facts give no upper bound on n__pren__pre, so they do not suffice to prove n__pre - 10i <= 2147483647in__pre - 10i <= 2147483647i. The proof block adds the bound n__pre <= 2147483647n__pre <= 2147483647 using get_data_at_rangeget_data_at_range. The engine can then prove that n - 10n - 10 does not overflow and advance the postconditions of both branches.

The recursive calls require no special handling: at each call site, the engine applies the callee’s contract. Both the inner and outer calls in mc91(mc91(n + 11))mc91(mc91(n + 11)) are checked against the specification of mc91mc91. C* verifies only partial correctness and generates no termination obligation, so the recursion itself requires no separate proof.

For proofs about the heap, we need separation-logic entailments |--|-- as well as equalities; see Separation Logic in C*. Alongside *_rule*_rule, the proof standard library provides *_slrule*_slrule functions, which construct theorems whose conclusions are |--|-- entailments. The following are common rules; in these diagrams, denotes |--|-- and denotes the separating conjunction ****:

trans_slruletrans_slrule composes two entailments; frame_right_slruleframe_right_slrule applies the frame rule to add an unrelated heap fragment FF to both sides; and intro_fact_slruleintro_fact_slrule adds a proved pure fact pp to the right-hand side of a spatial entailment. The function local_applylocal_apply uses these entailments to advance the symbolic state. It takes the current state as its antecedent and applies the frame rule to extend a small-footprint entailment, which mentions only the heap fragments it uses, to the whole heap. The result derives the next state while preserving the remaining heap.

Consider the singly-linked-list predicate sllsll. To read or write a list node, we first unfold sll pt lsll pt l into the head and tail data_atdata_at fragments. An entailment lemma proves this unfolding. Its proof uses backward tactics, covered in a later section; here we use the lemma as a known theorem in a forward proof:

// sll_unfold (proved elsewhere):
//   forall l pt.
//     ~(pt == 0i) ==>
//     ( sll pt l |-- exists x xs q. fact(l == x :: xs)
//                      ** data_at (field_addr pt Tlist Fhead) Tint x
//                      ** data_at (field_addr pt Tlist Ftail) Tptr q
//                      ** sll q xs )

// sll_unfold (proved elsewhere):
//   forall l pt.
//     ~(pt == 0i) ==>
//     ( sll pt l |-- exists x xs q. fact(l == x :: xs)
//                      ** data_at (field_addr pt Tlist Fhead) Tint x
//                      ** data_at (field_addr pt Tlist Ftail) Tptr q
//                      ** sll q xs )

Inside the loop body, we know v != 0v != 0, so the list is non-empty and we can apply the lemma forward:

[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`vv:addr`, spec_rule(`l2:(int)list`, sll_unfold)));
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), ent));
}

[[cst::proof]] {
  thm ent = undisch_rule(
      spec_rule(`vv:addr`, spec_rule(`l2:(int)list`, sll_unfold)));
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), ent));
}

Each call to spec_rulespec_rule instantiates the lemma’s outermost variable: the inner call sets ll to the current list l2l2, and the outer call sets ptpt to the pointer vvvv. The call to undisch_ruleundisch_rule moves the premise ~(vv == 0i)~(vv == 0i) into the theorem’s assumptions. The function local_applylocal_apply discharges this assumption using the fact already present in the symbolic state, then applies the unfolding entailment to replace sll vv l2sll vv l2 with the unfolded head and tail nodes. This proof does not set up a goal for the VC: it derives the next state from the current state, proceeding from left to right.

The two kinds of forward proof often work together: a general forward proof establishes a pure fact, which we then add to the spatial state. The following snippet uses intro_fact_slruleintro_fact_slrule to add a proved equality wantwant, such as a list identity, to the state:

[[cst::proof]] {
  // want : |- ...  (a pure fact proved forward)
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
      intro_fact_slrule(want, refl_slrule(`emp`))));
}

[[cst::proof]] {
  // want : |- ...  (a pure fact proved forward)
  cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
      intro_fact_slrule(want, refl_slrule(`emp`))));
}

refl_slrule(emp)refl_slrule(emp) produces the empty-heap entailment emp |-- empemp |-- emp. The rule intro_fact_slruleintro_fact_slrule adds the pure fact wantwant to its conclusion, and local_applylocal_apply applies the entailment to the state, adding the fact while leaving the heap unchanged.

The sllsll example demonstrated one forward step. The following program is verified entirely by forward proof: clear(char *arr, int n)clear(char *arr, int n) recursively zeroes the first nn bytes of arrarr.

We use data_atdata_at for a single memory cell and its array form for contiguous cells: array_at array_at states that there are nn cells of type TT starting at address , storing the elements of list in order. The predicate undef_array_at x T nundef_array_at x T n describes nn uninitialized cells. Since contracts cannot directly accept predicates with C-type arguments, we use new_fun_definitionnew_fun_definition to define and export monomorphic wrappers: undef_char_array arr nundef_char_array arr n describes nn uninitialized bytes, and zeroed arr nzeroed arr n describes nn bytes containing 00. The latter is defined as array_at arr Tchar n (ireplicate n 0i)array_at arr Tchar n (ireplicate n 0i), where ireplicate n 0iireplicate n 0i is the list of nn zeros. The specification requires fact(0i <= n) ** undef_char_array arr nfact(0i <= n) ** undef_char_array arr n at entry and zeroed arr nzeroed arr n at exit.

#include "proof/proof.h"
// Contracts may not take ctype-carrying predicates directly, so wrap the two
// char-array predicates in monomorphic versions.
[[cst::proof]] thm undef_char_array_def = new_fun_definition(
    `undef_char_array (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_char_array`);
[[cst::proof]] thm zeroed_def = new_fun_definition(
    `zeroed (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zeroed`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_char_array arr n`)]]
    [[cst::ensure(`zeroed arr n`)]]
{
  if (n == 0) {
    // Base case: undef_char_array arr 0 -|- emp -|- zeroed arr 0.
    [[cst::proof]] {
      thm repl_nil = apply_conversion(
          pure_rewrite_conv(THM_LIST(
              assume_rule(`n__pre == 0i`),
              get_theorem_by_name("IREPLICATE_DEF"),
              get_theorem_by_name("NUM_OF_INT_OF_NUM"),
              get_theorem_by_name("REPLICATE"))),
          `ireplicate n__pre 0i`);
      thm e_uz = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
          spec_rule(`arr__pre:int`,
              get_theorem_by_name("undef_array_at_zero")))));
      thm e_az = mp_rule(mp_rule(
          spec_rule(`ireplicate n__pre 0i`, spec_rule(`n__pre:int`,
              spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                  get_theorem_by_name("array_at_zero"))))),
          assume_rule(`n__pre == 0i`)), repl_nil);
      thm d_all = apply_conversion(
          once_rewrite_conv(THM_LIST(undef_char_array_def)),
          `undef_char_array (arr__pre:int) (n__pre:int)`);
      thm d_z = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
          `zeroed (arr__pre:int) (n__pre:int)`);
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
          eq2ent(list_trans_rule(THM_LIST(
              d_all, e_uz, sym_rule(e_az), sym_rule(d_z))))));
    }
    return;
  };
  // n >= 1; split the last byte off the end:
  //   undef_char_array arr n |--
  //     undef_char_array arr (n-1) ** undef_data_at (arr + (n-1)*sizeof Tchar) Tchar
  [[cst::proof]] {
    // read n's value range off its cell, for the n - 1 indexing/subtraction checks
    thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                    get_theorem_by_name("max_of_def")),
        spec_rule(`n__pre:int`, spec_rule(`Tint`,
            spec_rule(`n__addr:int`, get_data_at_range()))));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    // one int_arith_rule produces all the pure facts this step needs
    thm facts = undisch_all_rule(int_arith_rule(
        `~(n__pre == 0i) ==> 0i <= n__pre ==> n__pre <= 2147483647i
         ==> n__pre >= 1i && 0i <= n__pre - 1i
             && n__pre - 1i <= 2147483647i && -- 2147483648i <= n__pre - 1i`));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        intro_fact_slrule(facts, refl_slrule(`emp`))));
    thm d_all = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre:int)`);
    thm split = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
        spec_rule(`arr__pre:int`,
            get_theorem_by_name("undef_array_at_split_last")))));
    thm d_sub = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre - 1i)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            eq2ent(d_all),
            split,
            frame_right_slrule(eq2ent(sym_rule(d_sub)),
                `undef_data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar`)))));
  }
  clear(arr, n - 1);
  char *p = arr + (n - 1);
  *p = 0;
  // Fold the last byte back: zeroed arr (n-1) ** data_at (arr+(n-1)*sizeof Tchar) Tchar 0i
  //                            |-- zeroed arr n
  [[cst::proof]] {
    thm d_sub = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre - 1i)`);
    // IREPLICATE_APPEND is guarded by `0i <= n`; discharge it from the fact in scope
    thm app = mp_rule(
        ispec_rule(`0i`, spec_rule(`n__pre - 1i`,
            get_theorem_by_name("IREPLICATE_APPEND"))),
        assume_rule(`0i <= n__pre - 1i`));
    thm folded = rewrite_rule(THM_LIST(
        app,
        int_arith_rule(`(n__pre - 1i) + 1i == n__pre`)),
        spec_rule(`ireplicate (n__pre - 1i) 0i`, spec_rule(`0i`,
            spec_rule(`n__pre - 1i`, spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                get_theorem_by_name("array_at_merge_last")))))));
    thm d_all = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre:int)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            frame_right_slrule(eq2ent(d_sub),
                `data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar 0i`),
            folded,
            eq2ent(sym_rule(d_all))))));
  }
}

#include "proof/proof.h"
// Contracts may not take ctype-carrying predicates directly, so wrap the two
// char-array predicates in monomorphic versions.
[[cst::proof]] thm undef_char_array_def = new_fun_definition(
    `undef_char_array (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_char_array`);
[[cst::proof]] thm zeroed_def = new_fun_definition(
    `zeroed (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zeroed`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_char_array arr n`)]]
    [[cst::ensure(`zeroed arr n`)]]
{
  if (n == 0) {
    // Base case: undef_char_array arr 0 -|- emp -|- zeroed arr 0.
    [[cst::proof]] {
      thm repl_nil = apply_conversion(
          pure_rewrite_conv(THM_LIST(
              assume_rule(`n__pre == 0i`),
              get_theorem_by_name("IREPLICATE_DEF"),
              get_theorem_by_name("NUM_OF_INT_OF_NUM"),
              get_theorem_by_name("REPLICATE"))),
          `ireplicate n__pre 0i`);
      thm e_uz = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
          spec_rule(`arr__pre:int`,
              get_theorem_by_name("undef_array_at_zero")))));
      thm e_az = mp_rule(mp_rule(
          spec_rule(`ireplicate n__pre 0i`, spec_rule(`n__pre:int`,
              spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                  get_theorem_by_name("array_at_zero"))))),
          assume_rule(`n__pre == 0i`)), repl_nil);
      thm d_all = apply_conversion(
          once_rewrite_conv(THM_LIST(undef_char_array_def)),
          `undef_char_array (arr__pre:int) (n__pre:int)`);
      thm d_z = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
          `zeroed (arr__pre:int) (n__pre:int)`);
      cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
          eq2ent(list_trans_rule(THM_LIST(
              d_all, e_uz, sym_rule(e_az), sym_rule(d_z))))));
    }
    return;
  };
  // n >= 1; split the last byte off the end:
  //   undef_char_array arr n |--
  //     undef_char_array arr (n-1) ** undef_data_at (arr + (n-1)*sizeof Tchar) Tchar
  [[cst::proof]] {
    // read n's value range off its cell, for the n - 1 indexing/subtraction checks
    thm rng = rewrite_rule(THM_LIST(get_theorem_by_name("min_of_def"),
                                    get_theorem_by_name("max_of_def")),
        spec_rule(`n__pre:int`, spec_rule(`Tint`,
            spec_rule(`n__addr:int`, get_data_at_range()))));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(), rng));
    // one int_arith_rule produces all the pure facts this step needs
    thm facts = undisch_all_rule(int_arith_rule(
        `~(n__pre == 0i) ==> 0i <= n__pre ==> n__pre <= 2147483647i
         ==> n__pre >= 1i && 0i <= n__pre - 1i
             && n__pre - 1i <= 2147483647i && -- 2147483648i <= n__pre - 1i`));
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        intro_fact_slrule(facts, refl_slrule(`emp`))));
    thm d_all = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre:int)`);
    thm split = undisch_rule(spec_rule(`n__pre:int`, spec_rule(`Tchar`,
        spec_rule(`arr__pre:int`,
            get_theorem_by_name("undef_array_at_split_last")))));
    thm d_sub = apply_conversion(
        once_rewrite_conv(THM_LIST(undef_char_array_def)),
        `undef_char_array (arr__pre:int) (n__pre - 1i)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            eq2ent(d_all),
            split,
            frame_right_slrule(eq2ent(sym_rule(d_sub)),
                `undef_data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar`)))));
  }
  clear(arr, n - 1);
  char *p = arr + (n - 1);
  *p = 0;
  // Fold the last byte back: zeroed arr (n-1) ** data_at (arr+(n-1)*sizeof Tchar) Tchar 0i
  //                            |-- zeroed arr n
  [[cst::proof]] {
    thm d_sub = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre - 1i)`);
    // IREPLICATE_APPEND is guarded by `0i <= n`; discharge it from the fact in scope
    thm app = mp_rule(
        ispec_rule(`0i`, spec_rule(`n__pre - 1i`,
            get_theorem_by_name("IREPLICATE_APPEND"))),
        assume_rule(`0i <= n__pre - 1i`));
    thm folded = rewrite_rule(THM_LIST(
        app,
        int_arith_rule(`(n__pre - 1i) + 1i == n__pre`)),
        spec_rule(`ireplicate (n__pre - 1i) 0i`, spec_rule(`0i`,
            spec_rule(`n__pre - 1i`, spec_rule(`Tchar`, spec_rule(`arr__pre:int`,
                get_theorem_by_name("array_at_merge_last")))))));
    thm d_all = apply_conversion(once_rewrite_conv(THM_LIST(zeroed_def)),
        `zeroed (arr__pre:int) (n__pre:int)`);
    cst_set_symbolic_state(local_apply(cst_get_symbolic_state(),
        list_trans_slrule(THM_LIST(
            frame_right_slrule(eq2ent(d_sub),
                `data_at (arr__pre + (n__pre - 1i) * sizeof Tchar) Tchar 0i`),
            folded,
            eq2ent(sym_rule(d_all))))));
  }
}

All three proof blocks advance the symbolic state by composing local proof steps into an entailment from the current heap fragment to the required one, then applying it to the state with local_applylocal_apply. The recursive case uses list_trans_slrulelist_trans_slrule to compose entailments; the base case instead composes equalities with list_trans_rulelist_trans_rule and converts the result to an entailment with eq2enteq2ent.

• Base case n == 0n == 0: the empty array is equivalent to both empemp and zeroed arr 0zeroed arr 0. The proof rewrites undef_char_array arr 0undef_char_array arr 0 to zeroed arr 0zeroed arr 0 using library lemmas such as undef_array_at_zeroundef_array_at_zero and array_at_zeroarray_at_zero. It combines the -|--|- equalities with list_trans_rulelist_trans_rule, converts the result to an entailment with eq2enteq2ent, and installs it.
• Before the recursive call: split off the array’s last cell. We instantiate undef_array_at_split_lastundef_array_at_split_last using spec_rulespec_rule/undisch_ruleundisch_rule, use frame_right_slruleframe_right_slrule to preserve the last cell, and use list_trans_slrulelist_trans_slrule to derive an entailment from undef_char_array arr nundef_char_array arr n to undef_char_array arr (n-1) ** undef_data_at …undef_char_array arr (n-1) ** undef_data_at …. The indexing and subtraction safety checks also require pure facts, including n >= 1n >= 1 and that n-1n-1 is in the intint range. One call to int_arith_ruleint_arith_rule produces these facts, which intro_fact_slruleintro_fact_slrule adds to the state.
• After the recursive call and *p = 0*p = 0: fold the last cell back into the array. The proof uses array_at_merge_lastarray_at_merge_last and an ireplicateireplicate append lemma, whose 0i <= n0i <= n guard is discharged using a fact in scope. The rules frame_right_slruleframe_right_slrule/list_trans_slrulelist_trans_slrule combine zeroed arr (n-1) ** data_at … 0izeroed arr (n-1) ** data_at … 0i into zeroed arr nzeroed arr n, the exit assertion.

We can inspect the final step with Show Symbolic StateShow Symbolic State. After *p = 0;*p = 0;, the state contains several factfacts, the cells for local variables, and these two heap fragments:

These describe the first n-1n-1 bytes, already zeroed as zeroed arr (n-1)zeroed arr (n-1), and the last cell, just set to 00. The final proof block combines them into zeroed arr nzeroed arr n.

Each step derives the next state from the current state without setting up a goal for a verification condition. The complete proof is therefore entirely forward.

• C* connects C to HOL Light with a client/server model: the C code in [[cst::proof]][[cst::proof]] is a client holding only opaque handles, while the real logical objects and the trusted kernel live in an isolated server process; process isolation keeps the TCB and full expansiveness intact;
• forward proof is calling *_rule*_rule/*_slrule*_slrule/*_conv*_conv to assemble new theorems, bottom-up, from known ones;
• general forward proof uses refl_rulerefl_rule/sym_rulesym_rule/arith_rulearith_rule/spec_rulespec_rule/conj_ruleconj_rule/mp_rulemp_rule and conversions — typically proving a theorem bottom-up by induction;
• separation-logic forward proof uses *_slrule*_slrule to build theorems concluding in |--|--, with intro_fact_slruleintro_fact_slrule injecting pure facts and local_applylocal_apply advancing the symbolic state via the frame rule;
• installing a forward-proved theorem back into the symbolic state through eq2enteq2ent/local_applylocal_apply discharges the verification conditions left by the symbolic-execution engine;
• during proof development, use Show Symbolic StateShow Symbolic State in VSCode to inspect each state change; mc91mc91 and clearclear are complete, verifiable examples of general and separation-logic forward proof, respectively.