Closing Pure Goals with SMT

The previous section ended with purification handing over 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. Equalities, integer arithmetic, and quantified facts over them are exactly what SMT solvers are built for. This section connects C*‘s proof layer to Z3, closes those goals with SMT_TACSMT_TAC, and assembles the full three-step pipeline that verifies both examples with no other proof steps at program points.

The SMT userlib calls Z3 through its C API, so a Z3 installation with the C header and the link library is required; how to install it varies by platform. Once installed, point the build at it 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"

/path/to/z3/path/to/z3 is a placeholder for the actual location on your machine; when Z3 lives in the compiler’s default search paths, link_flags = "-lz3"link_flags = "-lz3" alone is enough (which is how cstar_examplescstar_examples ships). 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 hands 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 the translation fails, the solver cannot decide, or the goal is simply not valid, the goal is left open for the user to continue.

With all three tactics in place, the pipeline of this part becomes 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 every point that must reestablish the invariant or a postcondition state, the pattern is the same: 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 — the same function as reverse_clean.creverse_clean.c, with the big assertion deleted — calls it at three places: establishing the invariant before the loop, reestablishing it at the end of the body, and, after the loop, moving the state to the shape the returnreturn needs:

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

As always, the state is never edited directly: solve_vc_autosolve_vc_auto returns an entailment theorem, and cst_set_symbolic_statecst_set_symbolic_state commits it.

SMT solvers are at home with equalities, integer arithmetic, and quantifiers — but Z3 has no innate knowledge of the HOL definition of REVERSEREVERSE, nor of the theorem REVERSE_REVERSEREVERSE_REVERSE. smt_add_axiomsmt_add_axiom supplies such already-proved theorems as background knowledge for subsequent SMT calls; reverse.creverse.c installs 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 essential call is smt_add_axiomsmt_add_axiom: its argument is a theorem whose conclusion becomes available to the solver. Assumptions of the theorem are discharged first, but free term variables are not generalized — hence the explicit gen_all_rulegen_all_rule. One technical step is also required: monomorphization. The HOL list theorems are polymorphic in the element type AA, and the current translation does not handle HOL polymorphism; inst_type_ruleinst_type_rule fixes AA to the intint actually used here before the theorem is handed over.

SMT_TACSMT_TAC lives in userlib/smt/smt.cuserlib/smt/smt.c, and its core is not mysterious: recursively inspect the shape of a HOL term and build the semantically corresponding Z3 AST. The spine of term_to_z3term_to_z3 can be summarized as:

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 dispatch on the 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 translate become uninterpreted functions; the theorems added with smt_add_axiomsmt_add_axiom are what constrain their behavior. The handler registered by smt_register_seq_handlersmt_register_seq_handler additionally maps the list vocabulary 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 — so list goals are not left entirely uninterpreted.

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 cover its spatial reasoning; what remained open was the pure residue, which speaks about replace_inthreplace_inth — the function that the int_array_with_holeint_array_with_hole rules introduced into the logical lists. Three lemmas about it, proved once in strategy_demo/array/lemmas.cstrategy_demo/array/lemmas.c, say exactly what an update does to 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, then verifies with a single proof block at the end of the loop body:

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

One pass through the body reads 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’s facts give 0 <= i_v0 <= i_v and i_v < len__prei_v < len__pre;
3. the write executes, and the cell’s value becomes 00;
4. reestablishing 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 serves the states where both sides hold an int_arrayint_array over the same region directly, leaving a list equation;
7. POST_PURIFY_TACPOST_PURIFY_TAC produces the ordinary goal, and SMT_TACSMT_TAC — using the replace_inthreplace_inth lemmas — proves that the cleared prefix grew by one cell while the length and bound facts are maintained.

Loop entry and the postcondition after the loop need no proof block at all: with the strategies registered, the engine closes those obligations on its own.

• SMT_TACSMT_TAC closes an ordinary HOL goal by translating it — together with registered background theorems — to Z3, asserting the goal’s negation, and reading unsatisfiability as validity; the verdict is trusted, under a solver timeout.
• 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 maps term shapes to Z3 ASTs, dispatches applications on their head constants, and leaves translatable-but-unknown functions uninterpreted; the sequence handler maps the list vocabulary into Z3′s sequence theory.
• solve_vc_autosolve_vc_auto — purify, post-purify, SMT — discharges every remaining obligation of reversereverse at three program points, and of clearclear at one; the strategies of the previous section and the solver of this one are the whole proof.
• The inferinfer checks inside strategies and SMT_TACSMT_TAC are different levels: the former decides local rule applicability inside QCP, the latter closes whole pure goals in the C* proof layer.