Proof Automation

EN | 中文

The previous parts made proofs shorter and easier to reuse: backward tactics decompose a stated goal, each operation packages one resource transformation, and capsules package code together with its proof. At every program point, the programmer still decides which memory cells match, which list to unfold before a read, and which equation remains to be proved. These proofs often repeat the same steps: pair up the data_atdata_at of each program variable, unfold a list node, fold it back, and finish by proving a simple list equation or an integer bound.

This part of the tutorial automates these routine steps.

Spatial and pure reasoning

Proving a separation-logic entailment combines two kinds of reasoning. Spatial reasoning determines which resources on the left correspond to those on the right: it matches cells, unfolds and folds predicates, and cancels resources that appear on both sides. Pure reasoning handles the remaining obligations that do not involve memory: list equations, integer arithmetic, and quantified facts. C* automates these two kinds of reasoning with separate engines, connected 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 single reusable function can replace a manual proof block:


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 in this part verify in-place list reversal and array clearing, with calls to this function as the only proof steps at program points.

What This Part Covers

Purifying Entailments with Strategies explains how to automate spatial reasoning. It introduces strategies: declarative rules describing how a predicate such as sllsll is unfolded, folded, and canceled. The tactic PURIFY_TACPURIFY_TAC applies these rules until an entailment contains no spatial resources; POST_PURIFY_TACPOST_PURIFY_TAC then 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. The section ends with strategies for array predicates.

Closing Pure Goals with SMT explains how to automate pure reasoning. It connects C*‘s proof layer to the Z3 SMT solver: SMT_TACSMT_TAC closes ordinary logic goals, and smt_add_axiomsmt_add_axiom supplies the solver with proved list theorems as background knowledge. A brief explanation of term_to_z3term_to_z3 shows how HOL terms are translated and which terms the translation supports. Combining this step with purification gives the three-step solve_vc_autosolve_vc_auto, whose use is demonstrated in full on the reversal and array examples.

AI-Assisted Verification with cstar_mcp uses an assistant to make the remaining decisions. It describes the cstar_mcpcstar_mcp server, which provides access to the verifier over the Model Context Protocol: how to register it, the six tools available to an assistant, the verification loop the assistant runs, and a short session on the twicetwice example.