Closing Pure Goals with SMT

Purification in the previous section produced ordinary logic goals: the list equation l = REVERSE [] ++ ll = REVERSE [] ++ l at the loop head of reversereverse, and, once the array demo is completed, index bounds and replace_inthreplace_inth equations in clearclear. SMT solvers support reasoning about equalities, integer arithmetic, and quantified facts involving these operations. This section connects C*‘s proof layer to Z3 and uses SMT_TACSMT_TAC to close these goals. The resulting three-step pipeline verifies both examples without further proof steps at program points.

The SMT userlib calls Z3 through its C API, so the Z3 installation must include the C header and library. Installation steps vary by platform. After installing Z3, specify its location in the cstar.tomlcstar.toml at the repository root:

cflags = "-I/path/to/z3/include"
link_flags = "-L/path/to/z3/lib -lz3"

cflags = "-I/path/to/z3/include"
link_flags = "-L/path/to/z3/lib -lz3"

Replace /path/to/z3/path/to/z3 with the actual location on your machine. If Z3 is in the compiler’s default search paths, link_flags = "-lz3"link_flags = "-lz3" alone is enough, as in the strategy demo. cstarccstarc adds only its own include and library directories and the project root to the compiler’s search paths. If Z3 is installed under a prefix that the bundled clangclang does not search by default, such as a source build in /opt/z3/opt/z3, specify the -I-I and -L-L paths explicitly. A quick way to check the environment is to verify the finished examples:

cstarc verify strategy_demo/examples/reverse.c
cstarc verify strategy_demo/examples/clear.c

cstarc verify strategy_demo/examples/reverse.c
cstarc verify strategy_demo/examples/clear.c

PROOF gnode SMT_TAC(gnode gn);

PROOF gnode SMT_TAC(gnode gn);

SMT_TACSMT_TAC passes the current ordinary HOL goal to the initialized SMT userlib. If Z3 establishes that the goal is valid, the tactic closes the current gnodegnode. If translation fails, the solver cannot decide, or the goal is invalid, the goal remains open for the user to continue.

We can now combine the three tactics into one reusable function:

PROOF thm solve_vc_auto(term vc) {
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  SMT_TAC(g);
  return gnode_prove(root);
}

PROOF thm solve_vc_auto(term vc) {
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  SMT_TAC(g);
  return gnode_prove(root);
}

At each program point that requires the invariant or a postcondition state, read the symbolic state, form the entailment, and commit the proved theorem:

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

The finished strategy_demo/examples/reverse.cstrategy_demo/examples/reverse.c contains the same function as reverse_clean.creverse_clean.c, with the long assertion removed. It calls the helper at three places: to establish the invariant before the loop, reestablish it at the end of the body, and, after the loop, convert the state to the form required by returnreturn:

PROOF {
  term st = cst_get_symbolic_state();
  term return_ready = `exists t_v v_v w_v.
    data_at p__addr Tptr p__pre **
    data_at w__addr Tptr w_v **
    data_at v__addr Tptr v_v **
    data_at t__addr Tptr t_v **
    sll w_v (REVERSE l)
  `;
  term vc = `${st:hprop} |-- ${return_ready:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

PROOF {
  term st = cst_get_symbolic_state();
  term return_ready = `exists t_v v_v w_v.
    data_at p__addr Tptr p__pre **
    data_at w__addr Tptr w_v **
    data_at v__addr Tptr v_v **
    data_at t__addr Tptr t_v **
    sll w_v (REVERSE l)
  `;
  term vc = `${st:hprop} |-- ${return_ready:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

The state is updated through a theorem: solve_vc_autosolve_vc_auto returns an entailment theorem, and cst_set_symbolic_statecst_set_symbolic_state commits it. The state is never edited directly.

Z3 supports equalities, integer arithmetic, and quantifiers, but it does not know the HOL definition of REVERSEREVERSE or the theorem REVERSE_REVERSEREVERSE_REVERSE. smt_add_axiomsmt_add_axiom supplies these proved theorems as background knowledge for subsequent SMT calls; reverse.creverse.c registers them once, at load time:

PROOF static int install_smt(void) {
  smt_init();
  smt_register_seq_handler();
  type_pair_list int_inst = (type_pair_list)vector_create();
  vector_add(&int_inst, ((type_pair){`:int`, `:A`}));
  thm reverse_def_int = gen_all_rule(
    inst_type_rule(int_inst, get_REVERSE()));
  thm reverse_reverse_int = gen_all_rule(inst_type_rule(
    int_inst, get_theorem_by_name("REVERSE_REVERSE")));
  smt_add_axiom(reverse_def_int);
  smt_add_axiom(reverse_reverse_int);
  return 0;
}
PROOF static int _install_smt = install_smt();

PROOF static int install_smt(void) {
  smt_init();
  smt_register_seq_handler();
  type_pair_list int_inst = (type_pair_list)vector_create();
  vector_add(&int_inst, ((type_pair){`:int`, `:A`}));
  thm reverse_def_int = gen_all_rule(
    inst_type_rule(int_inst, get_REVERSE()));
  thm reverse_reverse_int = gen_all_rule(inst_type_rule(
    int_inst, get_theorem_by_name("REVERSE_REVERSE")));
  smt_add_axiom(reverse_def_int);
  smt_add_axiom(reverse_reverse_int);
  return 0;
}
PROOF static int _install_smt = install_smt();

The call to smt_add_axiomsmt_add_axiom takes a theorem and makes its conclusion available to the solver. The theorem’s assumptions are discharged first, but its free term variables are not generalized, so we call gen_all_rulegen_all_rule explicitly. The theorems also require monomorphization. The HOL list theorems are polymorphic in the element type AA, and the current translation does not handle HOL polymorphism. Before passing a theorem to the solver, inst_type_ruleinst_type_rule fixes AA to the intint type used in this example.

SMT_TACSMT_TAC is defined in userlib/smt/smt.cuserlib/smt/smt.c. Its core operation recursively inspects the structure of a HOL term and builds a semantically corresponding Z3 AST. The main cases of term_to_z3term_to_z3 are:

Z3_ast term_to_z3(Z3_context ctx, term tm) {
  if (is_int(tm))
    return Z3_mk_int(ctx, dest_int(tm), Z3_mk_int_sort(ctx));
  if (is_forall(tm)) {
    /* translate the bound variable's sort, recurse into
       the body, build a Z3 forall */
  }
  if (is_exists(tm)) {
    /* likewise, building a Z3 exists */
  }
  if (is_var(tm)) {
    /* a free variable becomes a Z3 constant of the same
       name and sort */
  }
  if (is_const(tm) || is_comb(tm))
    return smt_app_to_z3(ctx, tm);
  return NULL;
}

Z3_ast term_to_z3(Z3_context ctx, term tm) {
  if (is_int(tm))
    return Z3_mk_int(ctx, dest_int(tm), Z3_mk_int_sort(ctx));
  if (is_forall(tm)) {
    /* translate the bound variable's sort, recurse into
       the body, build a Z3 forall */
  }
  if (is_exists(tm)) {
    /* likewise, building a Z3 exists */
  }
  if (is_var(tm)) {
    /* a free variable becomes a Z3 constant of the same
       name and sort */
  }
  if (is_const(tm) || is_comb(tm))
    return smt_app_to_z3(ctx, tm);
  return NULL;
}

Applications are translated according to their head constant: ==>==> becomes Z3_mk_impliesZ3_mk_implies, /\/\ becomes Z3_mk_andZ3_mk_and, and integer ++, --, **, <<, <=<= map to the corresponding Z3 operations. Other functions whose types can be translated become uninterpreted functions, constrained by the theorems added with smt_add_axiomsmt_add_axiom. The handler registered by smt_register_seq_handlersmt_register_seq_handler also maps list operations into Z3′s sequence theory: NILNIL to the empty sequence, CONSCONS and APPENDAPPEND to sequence concatenation, inthinth to sequence indexing, and the type (A)list(A)list to a sequence sort. These parts of list goals therefore have an interpretation in Z3.

Finally, the solver asserts the background knowledge together with the negation of the goal. If Z3 reports unsatisfiable, no countermodel exists: the goal is valid, and SMT_TACSMT_TAC closes the gnodegnode.

The array demo strategy_demo/examples/clear.cstrategy_demo/examples/clear.c writes 00 into every element of an array. The strategies of the previous section already handle its spatial reasoning. The remaining pure goals involve replace_inthreplace_inth, the function that the int_array_with_holeint_array_with_hole rules introduced into the logical lists. Three lemmas, proved once in strategy_demo/array/lemmas.cstrategy_demo/array/lemmas.c, describe how an update affects reads and lengths:

|- forall i v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     inth i (replace_inth i v l) = v
|- forall i j v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     0i <= j ==> j < ilength l ==> ~(j = i) ==>
     inth j (replace_inth i v l) = inth j l
|- forall i v:int. forall l:(int)list.
     ilength (replace_inth i v l) = ilength l

|- forall i v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     inth i (replace_inth i v l) = v
|- forall i j v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     0i <= j ==> j < ilength l ==> ~(j = i) ==>
     inth j (replace_inth i v l) = inth j l
|- forall i v:int. forall l:(int)list.
     ilength (replace_inth i v l) = ilength l

clear.cclear.c installs the array strategies and registers these lemmas as SMT background knowledge. Two proof blocks then complete the verification: one at the end of the loop body, and one after the loop to convert the state to the form required by the postcondition:

PROOF static int _strategy_demo_array = install_strategy_demo_array();
PROOF static int install_clear_smt_axioms(void) {
  smt_add_axiom(replace_inth_at());
  smt_add_axiom(replace_inth_other());
  smt_add_axiom(replace_inth_length());
  return 0;
}
PROOF static int _clear_smt_axioms = install_clear_smt_axioms();
void clear(int *to, int len)
  [[cst::require(`exists l.
    fact(0i <= len && len <= 100i) **
    fact(ilength l == len) **
    int_array to 0i len l
  `)]]
  [[cst::ensure(`exists l.
    fact(forall i. 0i <= i && i < len ==> inth i l = 0i) **
    int_array to 0i len l
  `)]]
{
  int i = 0;
  PROOF term loop_inv = `exists i_v l.
    fact(0i <= i_v && i_v <= len__pre &&
         0i <= len__pre && len__pre <= 100i && ilength l == len__pre) **
    fact(forall j. 0i <= j && j < i_v ==> inth j l = 0i) **
    data_at to__addr Tptr to__pre **
    data_at len__addr Tint len__pre **
    data_at i__addr Tint i_v **
    int_array to__pre 0i len__pre l
  `;
  while (i < len)
    [[cst::invariant(loop_inv)]]
  {
    to[i] = 0;
    i = i + 1;
    PROOF {
      term st = cst_get_symbolic_state();
      term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
      cst_set_symbolic_state(solve_vc_auto(vc));
    }
  }
  PROOF {
    term st = cst_get_symbolic_state();
    term post_ready = `exists i_v l.
      fact(forall i. 0i <= i && i < len__pre ==> inth i l = 0i) **
      data_at to__addr Tptr to__pre **
      data_at len__addr Tint len__pre **
      data_at i__addr Tint i_v **
      int_array to__pre 0i len__pre l
    `;
    term vc = `${st:hprop} |-- ${post_ready:hprop}`;
    cst_set_symbolic_state(solve_vc_auto(vc));
  }
}

PROOF static int _strategy_demo_array = install_strategy_demo_array();
PROOF static int install_clear_smt_axioms(void) {
  smt_add_axiom(replace_inth_at());
  smt_add_axiom(replace_inth_other());
  smt_add_axiom(replace_inth_length());
  return 0;
}
PROOF static int _clear_smt_axioms = install_clear_smt_axioms();
void clear(int *to, int len)
  [[cst::require(`exists l.
    fact(0i <= len && len <= 100i) **
    fact(ilength l == len) **
    int_array to 0i len l
  `)]]
  [[cst::ensure(`exists l.
    fact(forall i. 0i <= i && i < len ==> inth i l = 0i) **
    int_array to 0i len l
  `)]]
{
  int i = 0;
  PROOF term loop_inv = `exists i_v l.
    fact(0i <= i_v && i_v <= len__pre &&
         0i <= len__pre && len__pre <= 100i && ilength l == len__pre) **
    fact(forall j. 0i <= j && j < i_v ==> inth j l = 0i) **
    data_at to__addr Tptr to__pre **
    data_at len__addr Tint len__pre **
    data_at i__addr Tint i_v **
    int_array to__pre 0i len__pre l
  `;
  while (i < len)
    [[cst::invariant(loop_inv)]]
  {
    to[i] = 0;
    i = i + 1;
    PROOF {
      term st = cst_get_symbolic_state();
      term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
      cst_set_symbolic_state(solve_vc_auto(vc));
    }
  }
  PROOF {
    term st = cst_get_symbolic_state();
    term post_ready = `exists i_v l.
      fact(forall i. 0i <= i && i < len__pre ==> inth i l = 0i) **
      data_at to__addr Tptr to__pre **
      data_at len__addr Tint len__pre **
      data_at i__addr Tint i_v **
      int_array to__pre 0i len__pre l
    `;
    term vc = `${st:hprop} |-- ${post_ready:hprop}`;
    cst_set_symbolic_state(solve_vc_auto(vc));
  }
}

For one iteration of the loop body, the proof proceeds as follows:

1. symbolic execution prepares to[i] = 0to[i] = 0 and needs the target cell’s data_atdata_at;
2. array rule 00 splits that cell off the int_arrayint_array, leaving an int_array_with_holeint_array_with_hole; its two inferinfer checks pass because the invariant gives 0 <= i_v0 <= i_v and the loop guard gives i_v < len__prei_v < len__pre;
3. the write executes, and the cell’s value becomes 00;
4. to reestablish the invariant, rule 11 matches the hole on the left against the target int_arrayint_array on the right, rewriting the target into an existential value vv, the data_atdata_at at index ii, and the equation l2 = replace_inth (i - x) v l1l2 = replace_inth (i - x) v l1;
5. the generic data_atdata_at strategy cancels the freshly written cell against that data_atdata_at, instantiating v = 0v = 0;
6. rule 22 handles states where both sides directly contain an int_arrayint_array over the same region, leaving a list equation;
7. POST_PURIFY_TACPOST_PURIFY_TAC produces the ordinary goal, and SMT_TACSMT_TAC uses the replace_inthreplace_inth lemmas to prove that the cleared prefix grew by one cell while the length and bound facts still hold.

Loop entry needs no proof block: with the strategies registered, the engine establishes the invariant on its own. The postcondition requires a separate proof block. After the loop, the state still carries the invariant’s i_vi_v and the exit fact i_v >= len__prei_v >= len__pre. The engine’s built-in solver does not derive the postcondition’s quantified fact from the invariant by itself: converting forall j. … j < i_v …forall j. … j < i_v … to forall i. … i < len__pre …forall i. … i < len__pre … remains an open verification condition. The second block expresses the required postcondition state as post_readypost_ready and applies solve_vc_autosolve_vc_auto, allowing SMT_TACSMT_TAC to complete the quantifier reasoning.

• SMT_TACSMT_TAC closes an ordinary HOL goal by translating it and the registered background theorems to Z3, asserting the goal’s negation, and interpreting unsatisfiability as validity. The solver runs under a timeout; its verdict is trusted, and each validated goal is listed in the report’s axiomsaxioms array.
• smt_add_axiomsmt_add_axiom turns proved HOL theorems into solver background knowledge; polymorphic list theorems are monomorphized with inst_type_ruleinst_type_rule (and generalized with gen_all_rulegen_all_rule) before being handed over.
• term_to_z3term_to_z3 recursively translates term structures to Z3 ASTs and handles applications according to their head constants. Functions with translatable types but unknown meanings remain uninterpreted; the sequence handler maps the list vocabulary into Z3′s sequence theory.
• solve_vc_autosolve_vc_auto combines purification, post-purification, and SMT solving to discharge every remaining obligation of reversereverse at three program points, and of clearclear at two. The strategies of the previous section and the solver of this one complete both proofs.
• The inferinfer checks inside strategies decide local rule applicability inside QCP, while SMT_TACSMT_TAC closes whole pure goals in the C* proof layer.