Purifying Entailments with Strategies

The operations section verified in-place list reversal by naming every resource step; this section returns to the declarative route — write the loop invariant, let symbolic execution emit verification conditions — and automates the proofs of those conditions. The running example is strategy_demo/examples/reverse_clean.cstrategy_demo/examples/reverse_clean.c from the cstar_examplescstar_examples repository, together with the strategy files under strategy_demo/sll/strategy_demo/sll/ and strategy_demo/array/strategy_demo/array/.

Recall the reversal invariant: the original list ll splits into a reversed prefix l1l1 (hanging off ww) and an unprocessed suffix l2l2 (hanging off vv). At the loop head, the engine emits an establishment VC — the state on entry must entail the invariant:

To prove it, pick the witnesses t_v = 0t_v = 0, w_v = 0w_v = 0, v_v = p__prev_v = p__pre, l1 = []l1 = [], l2 = ll2 = l. The reasoning that remains then falls into two distinct kinds.

1. Spatial reasoning: pair up the four data_atdata_at and cancel them; match sll p__pre lsll p__pre l with sll p__pre l2sll p__pre l2; conclude from sll 0i l1sll 0i l1 — a list at the null pointer — that l1 = []l1 = []. After this, the VC has shrunk to:

   Copy codeCopyCopied!

   emp |-- fact(l = REVERSE [] ++ l)
   

   Copy codeCopyCopied!

   emp |-- fact(l = REVERSE [] ++ l)
   

2. Pure reasoning: no memory is discussed anymore; what is left is an ordinary list equation:

   Copy codeCopyCopied!

   l = REVERSE [] ++ l
   

   Copy codeCopyCopied!

   l = REVERSE [] ++ l
   

The two kinds call for different automation. This section automates the spatial part with purification, driven by user-registered strategies; the next section closes the pure part with an SMT solver.

reverse_clean.creverse_clean.c is the whole function as one would first write it — contract, invariant, and one large [[cst::assert(...)]][[cst::assert(...)]] annotation that manually unfolds sll v_v l2sll v_v l2 into the head node’s two cells, so that the memory read v->tailv->tail can proceed:

struct list *reverse(struct list *p)
  [[cst::param(`l:(int)list`)]]
  [[cst::require(`sll p l`)]]
  [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = (void *)0;
  struct list *v = p;
  struct list *t = (void *)0;
  PROOF term loop_inv = `exists l1 l2 w_v v_v t_v.
    fact(l = (REVERSE l1) ++ l2) **
    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 l1 **
    sll v_v l2
  `;
  while (v)
    [[cst::invariant(loop_inv)]]
  {
    [[cst::assert(`
      exists l1 l2 w_v v_v t_v x xs v_tail.
        fact(~(v_v == 0i)) **
        fact(l = (REVERSE l1) ++ l2) **
        fact(l2 == CONS x xs) **
        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 l1 **
        data_at (field_addr v_v Tlist Fhead) Tint x **
        data_at (field_addr v_v Tlist Ftail) Tptr v_tail **
        sll v_tail xs
    `)]]
    t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}

struct list *reverse(struct list *p)
  [[cst::param(`l:(int)list`)]]
  [[cst::require(`sll p l`)]]
  [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = (void *)0;
  struct list *v = p;
  struct list *t = (void *)0;
  PROOF term loop_inv = `exists l1 l2 w_v v_v t_v.
    fact(l = (REVERSE l1) ++ l2) **
    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 l1 **
    sll v_v l2
  `;
  while (v)
    [[cst::invariant(loop_inv)]]
  {
    [[cst::assert(`
      exists l1 l2 w_v v_v t_v x xs v_tail.
        fact(~(v_v == 0i)) **
        fact(l = (REVERSE l1) ++ l2) **
        fact(l2 == CONS x xs) **
        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 l1 **
        data_at (field_addr v_v Tlist Fhead) Tint x **
        data_at (field_addr v_v Tlist Ftail) Tptr v_tail **
        sll v_tail xs
    `)]]
    t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}

As committed, the file does not verify: the establishment VC above, the preservation VC at the end of the body, the postcondition VC after the loop, and the assertion’s own VC all remain open. Discharging each by hand — with the backward tactics, or by operational steps — repeats the same matching and unfolding motions. The rest of this section replaces all of that, including the big assertion itself.

PROOF gnode PURIFY_TAC(gnode gn);

PROOF gnode PURIFY_TAC(gnode gn);

PURIFY_TACPURIFY_TAC takes a goal whose conclusion is a separation-logic entailment, repeatedly applies the currently registered strategies to it, and returns the purified goal that remains to be proved. It stops when no strategy matches; it is not required to close the goal in one call. The process does not backtrack: once a strategy has fired, the step is never undone, even if the proof later gets stuck — so a strategy that rewrites too aggressively can turn a provable goal into an unprovable one, and should not be registered.

To watch it work on the establishment VC, insert a proof block between the invariant and the whilewhile:

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
}

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
}

All four data_atdata_at pairs are gone, and the existential variables t_vt_v, w_vw_v, v_vv_v have been instantiated — without a single rule written by us. That is because C* registers $CSTAR_HOME/include/common.strategies$CSTAR_HOME/include/common.strategies by default, a generic library covering existential-variable instantiation and data_atdata_at. Its data_atdata_at rule captures a simple truth — two data_atdata_at at the same address and type must store the same value, after which both resources cancel — and its core effect reads:

left  : data_at(?p, ?ty, ?x) at 0
right : data_at(p, ty, ?y) at 1
action :
  left_erase(0);
  right_erase(1);
  right_add(y == x);

left  : data_at(?p, ?ty, ?x) at 0
right : data_at(p, ty, ?y) at 1
action :
  left_erase(0);
  right_erase(1);
  right_add(y == x);

The stack cells of program variables carry no list structure, so the generic library handles them completely. But purification has stalled: matching sll p__pre lsll p__pre l against sll p__pre l2sll p__pre l2, and reading l1 = []l1 = [] off sll 0i l1sll 0i l1, are facts about sllsll — knowledge the generic library cannot have.

strategy_demo/sll/sll.strategiesstrategy_demo/sll/sll.strategies supplies that knowledge as five declarative rules. The two that finish the establishment VC are the “null pointer means empty list” rule:

id : 0
priority : core(0)
right : sll(0, ?l) at 0
action : right_erase(0);
         right_add(l == NIL{Z});

id : 0
priority : core(0)
right : sll(0, ?l) at 0
action : right_erase(0);
         right_add(l == NIL{Z});

and the “same-address lists cancel” rule:

id : 1
priority : core(0)
left : sll(?p, ?l1) at 0
right : sll(p, ?l2) at 1
action : left_erase(0);
         right_erase(1);
         right_add(l2 == l1);

id : 1
priority : core(0)
left : sll(?p, ?l1) at 0
right : sll(p, ?l2) at 1
action : left_erase(0);
         right_erase(1);
         right_add(l2 == l1);

A rule is built from six fields:

?p?p and ?l1?l1 are pattern variables; a later occurrence without the question mark — pp, l1l1 — refers to the value bound by this match. at 0at 0, at 1at 1 are position labels the action uses to refer to matched assertions. leftleft and rightright carry no meaning beyond the two sides of H |-- KH |-- K.

Registering the file takes a path and a file name; reverse.creverse.c locates the folder relative to its own __FILE____FILE__:

PROOF static int install_sll_strategy(void) {
  char *source_path = strdup(__FILE__);
  char *strategy_folder = gc_sprintf(
    "%s/sll", dirname(dirname(source_path)));
  cst_add_strategy_folder_path(strategy_folder);
  cst_add_strategy_to_header("sll.strategies");
  return 0;
}
PROOF static int _install_sll_strategy = install_sll_strategy();

PROOF static int install_sll_strategy(void) {
  char *source_path = strdup(__FILE__);
  char *strategy_folder = gc_sprintf(
    "%s/sll", dirname(dirname(source_path)));
  cst_add_strategy_folder_path(strategy_folder);
  cst_add_strategy_to_header("sll.strategies");
  return 0;
}
PROOF static int _install_sll_strategy = install_sll_strategy();

With the file registered, rerunning PURIFY_TACPURIFY_TAC on the establishment VC leaves the generic library to data_atdata_at and the two rules to sllsll; the goal becomes:

emp |-- fact(l = REVERSE [] ++ l)

emp |-- fact(l = REVERSE [] ++ l)

No spatial reasoning is left in it — but syntactically it is still a separation-logic entailment, with empemp on the left and a factfact on the right.

PROOF gnode POST_PURIFY_TAC(gnode gn);

PROOF gnode POST_PURIFY_TAC(gnode gn);

POST_PURIFY_TACPOST_PURIFY_TAC takes a separation-logic goal that no longer holds real spatial resources, merges the remaining factfacts, moves their existential quantifiers, and rewrites the resulting factfact/empemp entailment into an ordinary logic goal. It applies no strategies; it is the finishing conversion from purification’s output to a pure reasoning target.

Completing the proof block:

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  /* the conclusion of g is now an ordinary logic formula */
}

PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  /* the conclusion of g is now an ordinary logic formula */
}

the goal becomes:

l = REVERSE [] ++ l

l = REVERSE [] ++ l

We leave it unproved for now. The question has changed from “which memory corresponds to which” to a plain list equation — this is where purification ends, and where the SMT solver takes over.

A strategy does not transform formulas by decree. Conceptually, each strategy corresponds to a separation-logic lemma, guarded by its applicability conditions. Behind “same-address lists cancel”, for instance, stands an entailment of this shape — canceling sll p l1sll p l1 against sll p l2sll p l2 at the price of the pure fact l2 = l1l2 = l1:

sll p l1 |-- forall l2. fact(l2 = l1) -* sll p l2

sll p l1 |-- forall l2. fact(l2 = l1) -* sll p l2

For rules with a checkcheck, the checked conditions enter the corresponding soundness obligation as premises.

The strategy language used here is Stellis; the paper Stellis: A Strategy Language for Purifying Separation Logic Entailments defines the language and gives an algorithm that generates a soundness condition for each strategy, reducing “is this strategy sound” to “is this condition provable”. In its evaluation, five strategy libraries totaling 98 strategies purify 219 of 229 entailments drawn from linked data structures and microkernel memory modules.

For the demo, the soundness lemmas have been stated and proved by hand:

• strategy_demo/sll/strategy_proof.hstrategy_demo/sll/strategy_proof.h and strategy_proof.cstrategy_proof.c — one lemma per rule of sll.strategiessll.strategies (the lemma numbering in the file does not follow the rule ids);
• strategy_demo/array/strategy_proof.hstrategy_demo/array/strategy_proof.h and strategy_proof.cstrategy_proof.c — likewise for array.strategiesarray.strategies below.

Understanding a strategy therefore means reading three things side by side: the match and action in the .strategies.strategies file, the soundness lemma stated in strategy_proof.hstrategy_proof.h, and its proof in strategy_proof.cstrategy_proof.c.

So far, PURIFY_TACPURIFY_TAC ran only on explicitly constructed VCs — and reverse_clean.creverse_clean.c still carries its big [[cst::assert]][[cst::assert]], whose only job is to expose the head node so v->tailv->tail can be read. The remaining three rules of sll.strategiessll.strategies make that assertion unnecessary: with the full file registered, the assertion can simply be deleted, and t = v->tail;t = v->tail; no longer fails with Cannot derive the precondition of Memory ReadCannot derive the precondition of Memory Read. Here is why.

When the symbolic execution engine executes v->tailv->tail, it must carve the read permission for that field out of the current state. Abstractly, it looks for an unknown remainder ?H?H making the following entailment true:

fact(~(v = 0)) ** sll v l ** ...
|--
exists val.
  data_at (field_addr v Tlist Ftail) Tptr val ** ?H

fact(~(v = 0)) ** sll v l ** ...
|--
exists val.
  data_at (field_addr v Tlist Ftail) Tptr val ** ?H

The data_atdata_at on the right is the resource this read needs; ?H?H is everything that should survive the read. Computing ?H?H is frame inference — an internal step of symbolic execution at every memory access, not an extra VC handed to the user.

Consider the unfold rule of sll.strategiessll.strategies:

id : 4
priority : core(0)
left : sll(?p, ?l) at 0
       (p != 0) at 1
right : data_at(field_addr(p, list, tail), PTR(struct list), ?v) at 2
action : left_erase(0);
         left_exist_add(x);
         left_exist_add(xs);
         left_exist_add(q);
         left_add(data_at(field_addr(p, list, head), I32, x));
         left_add(data_at(field_addr(p, list, tail), PTR(struct list), q));
         left_add(sll(q, xs));
         left_add(l == CONS{Z}(x, xs));

id : 4
priority : core(0)
left : sll(?p, ?l) at 0
       (p != 0) at 1
right : data_at(field_addr(p, list, tail), PTR(struct list), ?v) at 2
action : left_erase(0);
         left_exist_add(x);
         left_exist_add(xs);
         left_exist_add(q);
         left_add(data_at(field_addr(p, list, head), I32, x));
         left_add(data_at(field_addr(p, list, tail), PTR(struct list), q));
         left_add(sll(q, xs));
         left_add(l == CONS{Z}(x, xs));

It fires when the left holds a non-null sll p lsll p l and the right needs exactly that node’s tailtail cell, and unfolds the list by one node on the left. The generic data_atdata_at strategy then cancels the exposed tailtail cell against the right. When purification stops, the left side holds:

exists x xs q.
  fact(~(v = 0)) ** fact(l = x :: xs) **
  data_at (field_addr v Tlist Fhead) Tint x **
  sll q xs ** ...

exists x xs q.
  fact(~(v = 0)) ** fact(l = x :: xs) **
  data_at (field_addr v Tlist Fhead) Tint x **
  sll q xs ** ...

The resources this read did not take are precisely the remainder to fill in for ?H?H. In other words, the frame inference goal is itself a separation-logic entailment, and “cancel what is needed, keep the rest” is exactly what purification already does — the same strategies are reused as they are.

Frame inference is performed by the underlying QCP symbolic execution engine, and strategies are originally the component that drives QCP’s automation. C* lifts the strategy paths and the registration interface to the user layer:

cst_add_strategy_folder_path(strategy_folder);
cst_add_strategy_to_header("sll.strategies");

cst_add_strategy_folder_path(strategy_folder);
cst_add_strategy_to_header("sll.strategies");

So although the registration is written in a C* file, what it customizes includes how the engine completes frame inference at memory accesses. That is why completing one .strategies.strategies file has two visible effects at once: explicit PURIFY_TACPURIFY_TAC goals go through, and the read that previously needed the big assertion executes on its own.

The five rules of sll.strategiessll.strategies divide the labor as follows:

Linked lists are one shape of spatial reasoning; arrays are another, and their strategies bring in one new ingredient: applicability checks decided by arithmetic. The predicates and rules live under strategy_demo/array/strategy_demo/array/.

strategy_demo/array/array.strategiesstrategy_demo/array/array.strategies contains three rules:

The one worth reading in full is rule 00:

id : 0
priority : core(0)
left : int_array(?p, ?x, ?y, ?l) at 0
right : data_at(p + ?i * sizeof(I32), I32, ?v) at 1
check : infer(x <= i);
        infer(i < y);
action : left_erase(0);
         right_erase(1);
         left_add(int_array_with_hole(p, x, y, i, l));
         right_add(v == inth(i - x, l));

id : 0
priority : core(0)
left : int_array(?p, ?x, ?y, ?l) at 0
right : data_at(p + ?i * sizeof(I32), I32, ?v) at 1
check : infer(x <= i);
        infer(i < y);
action : left_erase(0);
         right_erase(1);
         left_add(int_array_with_hole(p, x, y, i, l));
         right_add(v == inth(i - x, l));

When the right needs the cell of array pp at index ii, the address shape alone does not justify splitting it off; the rule must also know that ii lies in [x, y)[x, y). That is what the two inferinfer lines in the checkcheck field do: they ask QCP’s built-in solver to derive x <= ix <= i and i < yi < y from the current pure facts, and the action runs only if both succeed. (This built-in solver decides local rule applicability only; it is not the SMT integration of the next section, which closes whole pure goals.)

Registration on the array side is packaged as a reusable, idempotent installer in strategy_demo/array/array.cstrategy_demo/array/array.c:

PROOF int install_strategy_demo_array(void) {
  static bool installed = false;
  if (installed) return 0;
  cst_add_strategy_folder_path(dirname(strdup(__FILE__)));
  cst_add_strategy_to_header("array.strategies");
  smt_init();
  smt_register_seq_handler();
  installed = true;
  return 0;
}

PROOF int install_strategy_demo_array(void) {
  static bool installed = false;
  if (installed) return 0;
  cst_add_strategy_folder_path(dirname(strdup(__FILE__)));
  cst_add_strategy_to_header("array.strategies");
  smt_init();
  smt_register_seq_handler();
  installed = true;
  return 0;
}

The two smt_smt_ calls initialize the SMT side along the way; they are the subject of the next section, where the array demo is completed.

• A verification condition mixes spatial reasoning (which resource corresponds to which) with pure reasoning (list equations, integer bounds); purification automates the former and hands the latter over as an ordinary logic goal.
• PURIFY_TACPURIFY_TAC applies registered strategies until none matches, without backtracking; the default common.strategiescommon.strategies handles existential instantiation and data_atdata_at, and user files like sll.strategiessll.strategies add per-predicate unfolding, folding, and cancellation.
• POST_PURIFY_TACPOST_PURIFY_TAC converts a purified factfact/empemp entailment into an ordinary logic formula — the end point of purification.
• Each strategy corresponds to a separation-logic lemma; the Stellis language makes the correspondence systematic, but in the current implementation registered strategies and the purification bridge remain in the trusted computing base.
• Frame inference at memory accesses is itself an entailment, so the same strategies drive it: registering a .strategies.strategies file both discharges explicit VCs and lets reads and writes through data-structure predicates execute automatically — for sllsll and, with checkcheck-guarded rules, for array segments.