Forward Proof in C*

In the previous section we saw that a proof is a program in the metalanguage, and that forward proof builds up from axioms and known theorems by applying inference rules until it reaches the goal. There the metalanguage was ML. C* writes proofs in the [[cst::proof]][[cst::proof]] blocks of C code — so how does C connect to HOL Light? And how does one construct a proof forward in C*? This section answers both. Forward proof comes in two flavors: general (only logic and arithmetic, no separation logic) and separation-logic ones. We cover only the “forward” construction of proofs here; backward (goal-directed) tactics and the operational style are left to later sections.

Classic LCF takes ML as its metalanguage: a proof is an ML program, and thmthm is an abstract type only the kernel can construct. C* goes one step further and makes C itself the language you write proofs in — the code in a [[cst::proof]][[cst::proof]] block is a proof program. But there is an obstacle: the theorem security of the previous section relies on the host language’s type abstraction, and C has none — pointer arithmetic and casts are enough to bypass the interface and overwrite a thmthm’s conclusion directly, forging a fake theorem.

The remedy is to put “the language you write proofs in” and “the language that implements the kernel” in two separate processes, joined by a guarded interface — a client/server model:

• The client is the C proof code in [[cst::proof]][[cst::proof]]. It does not hold the real logical objects, only opaque handles pointing to them — termterm, thmthm, and typetype are opaque types on the C side, and apart from passing them through interface functions there is no way to inspect or rewrite their innards.
• The server is a separate process containing HOL Light together with its trusted kernel, plus an object store mapping handles to the real logical objects.

A call like mp_rule(h1, h2)mp_rule(h1, h2) is thus really a remote procedure call: the server resolves the handles h1h1, h2h2 to real theorems, hands them to the kernel to run the primitive inference rules, then stores the new theorem in the object store and returns a fresh handle. The key is process isolation: however the client abuses pointers, it cannot reach the logical objects inside the server process. The trusted computing base (TCB) therefore remains just that small kernel, and the full expansiveness of the previous section carries over into C — whatever a [[cst::proof]][[cst::proof]] block contains, every theorem it produces is ultimately built by the kernel’s primitive rules.

The proof standard library has a naming law you can read off at a glance: *_rule*_rule builds theorems forward, a *_conv*_conv (conversion) maps a term to an equality theorem, and *_TAC*_TAC is a backward (goal-directed) tactic — the latter is the subject of later sections. So “forward proof,” in practice, is a sequence of calls to *_rule*_rule and conversions. First the basic vocabulary for building theorems (all written in [[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>) first computes an equality with the conversion and then hands back a thmthm. New constants, functions, and datatypes are introduced with the definition mechanisms from Separation Logic in C* they are all conservative extensions and return the corresponding definition / recursion / 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)`);

With these in hand we can prove a theorem forward. Below we prove forall l. app l nil = lforall l. app l nil = l (right identity of appapp), entirely bottom-up, setting up no goal at all:

[[cst::proof]] {
  // 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
}

[[cst::proof]] {
  // 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
}

Line by line, every step produces a new theorem from existing ones: base_eqbase_eq and step_eqstep_eq come from rewriting with app_defapp_def; ind_thmind_thm is the datatype’s own induction theorem nlist.indnlist.ind, specialized to the predicate \l. app l nil = l\l. app l nil = l by spec_rulespec_rule (instantiation) and beta_rulebeta_rule (-reduction); conj_ruleconj_rule combines base and step into one conjunction, and mp_rulemp_rule (modus ponens) feeds it to the induction theorem, giving resultresult. That is what “forward” means: start from the leaves (known theorems) and assemble upward until you reach the goal.

The appapp example above is pure logical calculation; it has not yet touched a C program. Recall Verification Condition Generation: when the symbolic-execution engine reaches a [[cst::proof]][[cst::proof]] block, it holds a symbolic state and may have left behind a verification condition (VC) to prove. Forward proof is used here as follows: read the current symbolic state, construct a theorem forward, and install it to advance the state. Three interface functions suffice: cst_get_symbolic_state()cst_get_symbolic_state() reads the current state (an assertion), cst_set_symbolic_state(...)cst_set_symbolic_state(...) installs an entailment “from the current state to a new one,” and eq2ent(...)eq2ent(...) turns an equality theorem into such an entailment.

Below we verify twicetwice: it computes (n+1) + (n-1)(n+1) + (n-1), and the spec says the result equals doubl(n)doubl(n) (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 blocks follow the same rhythm: read the state → construct an equality theorem forward → rewrite the state with it → install. The first block reduces (a+1) + (b-1)(a+1) + (b-1) to a + ba + b; the second uses doubldoubl’s definition (flipped by sym_rulesym_rule into the direction x + x == doubl(x)x + x == doubl(x)) to collapse a + ba + b into doubl(n)doubl(n). After the two steps, the return value in the symbolic state is exactly doubl(n)doubl(n), and the VC at the end is discharged.

The two proof blocks in the previous section were not written blind — while developing them, we kept watching the symbolic state. C*‘s VSCode extension provides exactly this feedback loop.

Right-click any line and choose Show Symbolic StateShow Symbolic State (shortcut alt+rightalt+right, or ctrl+alt+rightctrl+alt+right on macOS; we used it in Your First C* Program), and the panel on the right shows the symbolic state after that line executes; at a function’s exit or the end of the file it shows the pending verification condition instead (of the shape … |-- …… |-- …). Note you can only query ordinary statement lines outside a proof block — lines inside one cannot be queried.

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

The gap is plain to see: the rr cell holds the unsimplified sum (n+1) + (n-1)(n+1) + (n-1), while the postcondition wants it to equal doubl(n)doubl(n). Development is then a loop:

1. Look at the state: Show Symbolic StateShow Symbolic State on the lines around a proof block to read the current state and the gap;
2. Find a tool: locate the lemma or conversion that bridges the gap — C*‘s toolchain can search thousands of named theorems and conversions by name or by statement (say, the defining theorem of doubldoubl, or a decision procedure for integer arithmetic);
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: re-run Show Symbolic StateShow Symbolic State to confirm the state advanced as expected, and check at the end of the file whether the verification conditions are cleared;
5. Repeat until every verification condition is discharged.

After writing twicetwice’s two proof blocks, the same spot now reads:

The rr cell has become doubl n__predoubl n__pre, and the verification condition at the end clears with it. Forward-proof development is thus state-driven: you keep your eyes on the current state and push it, step by step, toward the postcondition.

Now let us put the moves above to work on a complete, recursive program. McCarthy 91 is a classic function: it 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 is conditional: it uses **** to conjoin two case-split facts — the n > 100n > 100 and n <= 100n <= 100 cases each assert the return value.

The single proof block, in the n > 100n > 100 branch, does a very common thing: make the parameter’s value range explicit. At entry we only know fact(0i <= n)fact(0i <= n), but in the symbolic state nn occupies a cell data_at n__addr Tint n__predata_at n__addr Tint n__pre, and an intint cell inherently implies n__pren__pre lies between intint’s bounds. get_data_at_range()get_data_at_range() is that generic lemma; the three nested spec_rulespec_rules instantiate it to nn’s address, 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 turn the bounds into concrete numerals; and local_applylocal_apply merges the resulting range fact into the state.

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

This is exactly the intint overflow safety check for n - 10n - 10: with only the two antecedent facts, n__pren__pre has no upper bound, so n__pre - 10i <= 2147483647in__pre - 10i <= 2147483647i on the right cannot be proved. The proof block supplies the bound n__pre <= 2147483647n__pre <= 2147483647 via get_data_at_rangeget_data_at_range, closing the gap — after which the engine can prove n - 10n - 10 does not overflow and advance the postconditions of both branches.

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

Once a proof has to talk about the heap, equality is not enough; we need the separation-logic entailment |--|-- (see Separation Logic in C*). In parallel with *_rule*_rule, the proof standard library offers a family of *_slrule*_slrule: they build, forward, theorems whose conclusion is a |--|--. A few common ones (in the rule boxes, stands for |--|-- and for the separating conjunction ****):

trans_slruletrans_slrule chains two entailments end to end; frame_right_slruleframe_right_slrule is separation logic’s frame rule, adding an unrelated chunk of heap FF on both sides; intro_fact_slruleintro_fact_slrule pushes a proved pure fact pp into the right-hand side of a spatial entailment. What actually advances the symbolic state is local_applylocal_apply: it takes the current state as antecedent and, via the frame rule, lifts a small-footprint entailment (which mentions only the few chunks it touches) onto the whole heap, deriving the next state — it is precisely the frame rule that lets a “local” entailment act on the “full” state.

Take the singly-linked-list predicate sllsll as an example. To read or write a list node, one must first unfold sll pt lsll pt l into the head and tail data_atdata_at chunks. This unfolding is an entailment lemma proved ahead of time (its proof uses backward tactics, the subject of a later section); here we reuse it as a ready-made forward theorem:

// sll_unfold (proved elsewhere):
//   forall pt l.
//     ~(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 pt l.
//     ~(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, knowing v != 0v != 0 (so the list is non-empty), we put it to use forward:

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

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

spec_rulespec_rule instantiates the lemma’s ptpt, ll to the current pointer vvvv and list l2l2; undisch_ruleundisch_rule discharges the premise ~(vv == 0i)~(vv == 0i) (already present as a fact in the symbolic state); local_applylocal_apply then applies this unfolding entailment to the current state, replacing sll vv l2sll vv l2 with the unfolded head and tail nodes. None of this sets up a goal for the VC — it takes the current state as antecedent and derives the next state left to right, which is exactly what “forward” means.

The two flavors of forward proof often work together: first prove a pure fact generally, then inject it into the spatial state. The snippet below pushes a proved equality fact wantwant (say some list identity) into the state via intro_fact_slruleintro_fact_slrule:

[[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) supplies a trivial empty-heap entailment emp |-- empemp |-- emp as a carrier, intro_fact_slruleintro_fact_slrule attaches the pure fact wantwant to it, and local_applylocal_apply merges this “adds only a fact, touches no heap” entailment into the state.

Earlier we demonstrated a single forward move on sllsll. Here is a complete program that is verified end to end and entirely forward: clear(char *arr, int n)clear(char *arr, int n) recursively zeroes the first nn bytes of arrarr — without a single backward proof.

For a single memory cell we use data_atdata_at; for a contiguous run we use its array form: array_at array_at means there are nn cells of type TT starting at address , holding the list in order; undef_array_at x T nundef_array_at x T n is nn uninitialized cells. Since a contract cannot take a predicate carrying a C-type argument directly, we first wrap each in a monomorphic predicate with new_fun_definitionnew_fun_definition and export it: undef_char_array arr nundef_char_array arr n (nn uninitialized bytes) and zeroed arr nzeroed arr n (nn bytes all equal to 00, i.e. 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 spec then reads: entry fact(0i <= n) ** undef_char_array arr nfact(0i <= n) ** undef_char_array arr n, exit zeroed arr nzeroed arr n.

#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)`);
    thm folded = rewrite_rule(THM_LIST(
        get_theorem_by_name("IREPLICATE_APPEND"),
        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)`);
    thm folded = rewrite_rule(THM_LIST(
        get_theorem_by_name("IREPLICATE_APPEND"),
        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 one step, and all have the same shape: use list_trans_slrulelist_trans_slrule to chain several small entailments end to end into one entailment from “this chunk of heap now” to “that chunk of heap we want,” then local_applylocal_apply it into the state.

• Base case n == 0n == 0: the empty array is equivalent both to empemp and to zeroed arr 0zeroed arr 0; the proof rewrites undef_char_array arr 0undef_char_array arr 0 through library lemmas undef_array_at_zeroundef_array_at_zero, array_at_zeroarray_at_zero, and so on, all the way to zeroed arr 0zeroed arr 0 — the chain of -|--|- equalities is joined into one by list_trans_rulelist_trans_rule, then turned into an entailment with eq2enteq2ent and installed.
• Before the recursive call: split one cell off the end of the array — undef_array_at_split_lastundef_array_at_split_last is instantiated via spec_rulespec_rule/undisch_ruleundisch_rule, frame_right_slruleframe_right_slrule frames the split-off last cell, and list_trans_slrulelist_trans_slrule splits undef_char_array arr nundef_char_array arr n into 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 need pure facts like n >= 1n >= 1 and n-1n-1 being in intint range — a single int_arith_ruleint_arith_rule produces all of them at once, injected with intro_fact_slruleintro_fact_slrule.
• After the recursive call, *p = 0*p = 0: fold the last cell back — array_at_merge_lastarray_at_merge_last plus an ireplicateireplicate append lemma, with 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, which is exactly the exit assertion.

That last step is clearest under Show Symbolic StateShow Symbolic State. Querying the line *p = 0;*p = 0;, the state holds (dropping several factfacts and other cells) exactly these two heap chunks side by side:

the already-zeroed first n-1n-1 bytes zeroed arr (n-1)zeroed arr (n-1), and the last cell just set to 00 — the final proof block’s job is to combine them into zeroed arr nzeroed arr n.

Throughout, no goal is ever set up for any verification condition: each step takes the current state as antecedent and derives the next state to its right. This is a complete proof that is 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;
• while developing, you can watch the state with Show Symbolic StateShow Symbolic State in VSCode as you push it forward — mc91mc91 and clearclear are complete, verifiable examples of the general and separation-logic flavors respectively.