Proof Automation

EN | 中文

The previous parts made proofs shorter and reusable: backward tactics decompose a stated goal, operations package one resource transformation each, and capsules carry code together with its proof. What none of them changed is who does the work: at every program point, a person still decides which memory cell matches which, which list to unfold before a read, and which equation remains to be proved. Watch a few of these proofs side by side and the same moves repeat — pair up the data_atdata_at of each program variable, unfold a list node, fold it back, and finish with a small list equation or an integer bound.

This part of the tutorial automates that routine.

Spatial and pure reasoning

Proving a separation-logic entailment mixes two kinds of reasoning. Spatial reasoning decides which resource on the left corresponds to which on the right — matching cells, unfolding and folding predicates, canceling what appears on both sides. Pure reasoning is what remains once no memory is being discussed: list equations, integer arithmetic, quantified facts. C* automates them with two separate engines, arranged in a pipeline:


symbolic execution produces an SL entailment
              |
              |   strategies also drive frame inference
              |   at memory accesses
              v
         PURIFY_TAC
   match, unfold, fold, and cancel spatial resources
              |
              v
      POST_PURIFY_TAC
   a fact/emp-only SL goal becomes an ordinary logic goal
              |
              v
          SMT_TAC
   list equations, integer arithmetic, quantifiers


symbolic execution produces an SL entailment
              |
              |   strategies also drive frame inference
              |   at memory accesses
              v
         PURIFY_TAC
   match, unfold, fold, and cancel spatial resources
              |
              v
      POST_PURIFY_TAC
   a fact/emp-only SL goal becomes an ordinary logic goal
              |
              v
          SMT_TAC
   list equations, integer arithmetic, quantifiers

Where this shows up in code

Once strategies are registered and an SMT solver is connected, a whole manual proof block shrinks to 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);
}

The examples of this part verify in-place list reversal and array clearing with no proof steps at program points beyond calls to this function.

What This Part Covers

Purifying Entailments with Strategies automates the spatial half. It introduces strategies — declarative rules describing how a predicate like sllsll is unfolded, folded, and canceled — and the tactic PURIFY_TACPURIFY_TAC that applies them until an entailment contains no spatial resources, plus POST_PURIFY_TACPOST_PURIFY_TAC, which converts the purified goal into an ordinary logic formula. The same strategies also customize how the symbolic execution engine performs frame inference at memory reads and writes, and the section closes with strategies for array predicates.

Closing Pure Goals with SMT automates the pure half. It connects C*‘s proof layer to the Z3 SMT solver: SMT_TACSMT_TAC closes ordinary logic goals, smt_add_axiomsmt_add_axiom supplies the solver with proved list theorems as background knowledge, and a short look inside term_to_z3term_to_z3 shows how HOL terms are translated — and where the translation stops. Together with purification this yields the three-step solve_vc_autosolve_vc_auto, demonstrated on the reversal and array examples end to end.