Purifying Entailments with Strategies

EN | 中文

The operations section verified in-place list reversal by specifying each resource operation. This section returns to declarative proofs: we write the loop invariant, let symbolic execution generate verification conditions, and automate their proofs. The running example is strategy_demo/examples/reverse_clean.cstrategy_demo/examples/reverse_clean.c, together with the strategy files under strategy_demo/sll/strategy_demo/sll/ and strategy_demo/array/strategy_demo/array/.

Two Kinds of Reasoning

Recall the reversal invariant: the original list ll splits into a reversed prefix l1l1 and an unprocessed suffix l2l2, represented by linked lists starting at ww and vv, respectively. At the loop head, the engine generates an establishment VC requiring the entry state to entail the invariant:

The establishment VC at the loop head of reversereverse


data_at t__addr Tptr 0i **
data_at v__addr Tptr p__pre **
data_at w__addr Tptr 0i **
data_at p__addr Tptr p__pre **
sll p__pre l
|--
exists t_v v_v w_v l1 l2.
  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


data_at t__addr Tptr 0i **
data_at v__addr Tptr p__pre **
data_at w__addr Tptr 0i **
data_at p__addr Tptr p__pre **
sll p__pre l
|--
exists t_v v_v w_v l1 l2.
  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

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 remaining proof requires two kinds of reasoning.

Spatial reasoning: match and cancel the four pairs of data_atdata_at assertions; match sll p__pre lsll p__pre l with sll p__pre l2sll p__pre l2; use sll 0i l1sll 0i l1, which describes a list at the null pointer, to conclude that l1 = []l1 = []. These steps reduce the VC to:
```
emp |-- fact (l == REVERSE [] ++ l) ** emp
```
```
emp |-- fact (l == REVERSE [] ++ l) ** emp
```
Pure reasoning: the remaining goal is an ordinary list equation with no reference to memory:
```
l == REVERSE [] ++ l
```
```
l == REVERSE [] ++ l
```

The two kinds require different forms of automation. This section automates spatial reasoning through purification, using user-registered strategies; the next section proves the remaining pure goals with an SMT solver.

The Starting Point: A Manual Unfold

reverse_clean.creverse_clean.c contains an initial version of the complete function, with a contract, an invariant, and a large [[cst::assert(...)]][[cst::assert(...)]] annotation. The annotation manually unfolds sll v_v l2sll v_v l2 into the head node’s two field 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 these VCs by hand, using backward tactics or operational steps, repeats the same matching and unfolding operations. The rest of this section shows how to automate these operations and remove the large assertion.

`PURIFY_TACPURIFY_TAC`


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 been applied, that step is never undone, even if the proof later gets stuck. A strategy that rewrites too aggressively can therefore 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 after the loop_invloop_inv declaration and before 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);
}

The goal returned by PURIFY_TACPURIFY_TAC


sll p__pre l
|--
exists l1 l2.
  fact (l == REVERSE l1 ++ l2) **
  sll 0i l1 **
  sll p__pre l2


sll p__pre l
|--
exists l1 l2.
  fact (l == REVERSE l1 ++ l2) **
  sll 0i l1 **
  sll p__pre l2

All four data_atdata_at pairs have been canceled, and the existential variables t_vt_v, w_vw_v, v_vv_v have been instantiated, although we have not written any rules yet. C* registers $CSTAR_HOME/include/common.strategies$CSTAR_HOME/include/common.strategies by default. This generic library handles existential-variable instantiation and data_atdata_at. Its data_atdata_at rules match a left-hand and a right-hand data_atdata_at assertion at the same address and type, cancel both resources, and leave equality of their values as a proof obligation. Matching addresses alone does not establish this equality. The following single rule summarizes their effect; the library implements this through several staged rules:


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(x == y);


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(x == y);

The stack cells of program variables carry no list structure, so the generic library handles them completely. Purification stops here because matching sll p__pre lsll p__pre l against sll p__pre l2sll p__pre l2, and deriving l1 = []l1 = [] from sll 0i l1sll 0i l1, require properties of sllsll that the generic library does not provide.

Writing Strategies for `sllsll`

strategy_demo/sll/sll.strategiesstrategy_demo/sll/sll.strategies supplies that knowledge as five declarative rules. The two rules that finish purifying 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:

Field	Meaning
`idid`	the rule’s number within its strategy file
`prioritypriority`	scheduling priority and phase for matching; the examples here keep the stock configuration
`leftleft`	assertions to match on the left of the entailment (the antecedent)
`rightright`	assertions to match on the right (the consequent)
`checkcheck`	conditions that must hold before the action may run
`actionaction`	the state change: erase or add assertions, instantiate existential variables

?p?p and ?l1?l1 are pattern variables; later occurrences without the question mark, such as pp, l1l1, refer to the values bound by the match. at 0at 0, at 1at 1 are position labels that the action uses to refer to matched assertions. leftleft and rightright refer only to 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 applies the generic library to data_atdata_at and the two rules to sllsll, producing the goal:


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


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

This goal requires no further spatial reasoning. Syntactically, it is still a separation-logic entailment, with empemp on the left and a factfact followed by empemp on the right.

From Purified Goals to Ordinary Logic


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 contains 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 performs the final conversion from purification’s output to a pure goal.

We complete the proof block as follows:


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 remaining obligation is a list equation. Purification ends here, and the SMT solver handles the pure reasoning.

Why Strategies Are Sound

A strategy’s formula transformations require justification. Conceptually, each strategy corresponds to a separation-logic lemma, guarded by its applicability conditions. For example, “same-address lists cancel” corresponds to the following entailment: canceling sll p l1sll p l1 against sll p l2sll p l2 leaves the obligation to prove 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. Proving this condition establishes the strategy’s soundness. 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.

The current trust boundary

C* does not yet implement the full process of automatically generating each registered strategy’s soundness lemma and checking its proof at load time. The demo directories provide the soundness proofs, but the runtime does not bind registered strategies to them. The PURIFY_TACPURIFY_TAC / POST_PURIFY_TACPOST_PURIFY_TAC adapters validate their results with explicit trust assumptions rather than derived rules. At this stage, registered strategies and the purification bridge belong to the trusted computing base: if a strategy is wrong, the system cannot yet reject the unsound conclusions it produces. The verification report records both dependencies. The bridge’s factfact lemmas appear in its axiomsaxioms array. Once a purified goal is closed, the implication used by PURIFY_TACPURIFY_TAC to accept that result as a proof of the original entailment also appears there. Each registered strategy file appears in strategiesstrategies, so the report distinguishes runs that rely on these assumptions and strategies from those that do not. The toolchain’s guidance for AI assistants describes these strategy hooks as fragile and recommends explicit proof steps that cite lemmas by name. This part of the tutorial presents strategies to demonstrate the approach used in the course.

Frame Inference: The Same Purification, Another Entry Point

So far, we have run PURIFY_TACPURIFY_TAC only on explicitly constructed VCs. The function in reverse_clean.creverse_clean.c still contains the large [[cst::assert]][[cst::assert]] annotation, which exposes the head node so that v->tailv->tail can be read. The remaining three rules of sll.strategiessll.strategies make that assertion unnecessary: once the full file is registered, we can delete the assertion, and t = v->tail;t = v->tail; no longer fails with Cannot derive the precondition of Memory ReadCannot derive the precondition of Memory Read. To see why, consider the resources required by the read.

What a Memory Read Actually Requires

When the symbolic execution engine executes v->tailv->tail, it must extract the read permission for that field from the current state. Abstractly, it looks for an unknown remainder ?H?H that makes 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.

Why Purification Solves It

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

This rule applies when the left holds a non-null sll p lsll p l and the right requires that node’s tailtail cell. It unfolds one list node on the left. The generic data_atdata_at strategy then matches and cancels the exposed tailtail cell against the required cell on the right. When purification stops, the left side holds the following, where l2l2 denotes the list written as ll in the schematic frame-inference goal above:


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


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

The resources left after this cancellation form the remainder ?H?H. Frame inference is thus another separation-logic entailment: purification cancels the required resources and retains the rest, using the same strategies.

From QCP to the User Layer

The underlying QCP symbolic execution engine performs frame inference, using strategies to drive its automation. C* exposes interfaces for setting strategy paths and registering strategies at 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");

Registration code in a C* file therefore also controls how the engine performs frame inference at memory accesses. Completing one .strategies.strategies file has two effects: explicit PURIFY_TACPURIFY_TAC goals can be processed, and the read that previously required the large assertion executes automatically.

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

id	Where it fires	Effect
`00`	`sll 0 lsll 0 l` on the right	replaces the null-pointer list by `l = []l = []`
`11`	same-address `sllsll` on both sides	cancels the spatial predicates, leaving a list equation
`22`	head cell on the left, `sllsll` needed on the right	unfolds the right-hand target, so the list can be refolded
`33`	`sll p lsll p l` on the left with `p = 0p = 0`	eliminates the empty list, adding `l = []l = []`
`44`	non-null `sllsll` on the left, `tailtail` cell needed on the right	unfolds one node, serving reads and frame inference

Strategies for Arrays

Arrays also require spatial reasoning. Their strategies add applicability checks that are decided by arithmetic reasoning. The predicates and rules live under strategy_demo/array/strategy_demo/array/.

The int_arrayint_array predicate

int_array p x y lint_array p x y l describes consecutive intint cells with indices in the half-open interval [x, y)[x, y), relative to base address pp; the logical list ll records the stored values in order. It is defined by recursion on the list:


int_array p x y []
  -|- fact(x = y)
int_array p x y (h :: t)
  -|- data_at (p + x * sizeof Tint) Tint h **
      int_array p (x + 1i) y t


int_array p x y []
  -|- fact(x = y)
int_array p x y (h :: t)
  -|- data_at (p + x * sizeof Tint) Tint h **
      int_array p (x + 1i) y t

So data_at q Tint vdata_at q Tint v owns a single intint cell, while int_array p x y lint_array p x y l owns every cell of [x, y)[x, y); for example, int_array p 0i 3i [a; b; c]int_array p 0i 3i [a; b; c] unfolds into the separating conjunction


data_at (p + 0i * sizeof Tint) Tint a **
data_at (p + 1i * sizeof Tint) Tint b **
data_at (p + 2i * sizeof Tint) Tint c


data_at (p + 0i * sizeof Tint) Tint a **
data_at (p + 1i * sizeof Tint) Tint b **
data_at (p + 2i * sizeof Tint) Tint c

When a read or write needs the data_atdata_at of cell ii alone, we split that cell from the owned segment and retain the rest. This does not turn the whole array into one data_atdata_at.

The int_array_with_holeint_array_with_hole predicate

int_array_with_hole p x y i lint_array_with_hole p x y i l is what remains of int_array p x y lint_array p x y l after the cell at index ii is temporarily taken out. It allows us to put the cell back and recover a complete array:


int_array_with_hole p x y i l
  -|-
  forall v.
    data_at (p + i * sizeof Tint) Tint v -*
    int_array p x y (replace_inth (i - x) v l)


int_array_with_hole p x y i l
  -|-
  forall v.
    data_at (p + i * sizeof Tint) Tint v -*
    int_array p x y (replace_inth (i - x) v l)

Here -*-* is separating implication (the magic wand): supplying a cell with value vv at index ii restores the array over [x, y)[x, y). Its logical list is ll with vv written at the relative index i - xi - x, i.e. replace_inth (i - x) v lreplace_inth (i - x) v l.

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

id	Sides matched	Rewriting effect
`00`	left: `int_array p x y lint_array p x y l`; right: the `data_atdata_at` at index `ii`	checks `x <= i < yx <= i < y`; the array becomes a hole on the left, the cell becomes `v = inth (i-x) lv = inth (i-x) l` on the right
`11`	left: `int_array_with_hole p x y i l1int_array_with_hole p x y i l1`; right: `int_array p x y l2int_array p x y l2`	cancels both; introduces on the right a value `vv`, the `data_atdata_at` at index `ii`, and `l2 = replace_inth (i-x) v l1l2 = replace_inth (i-x) v l1`
`22`	left: `int_array p x y l1int_array p x y l1`; right: `int_array p x y l2int_array p x y l2`	cancels both array predicates, leaving `l2 = l1l2 = l1`

Rule 00 shows how the applicability checks work:


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 requires the cell of array pp at index ii, matching the address alone does not justify extracting the cell; the rule must also establish that ii lies in [x, y)[x, y). The two inferinfer lines in the checkcheck field ask QCP’s built-in solver to derive x <= ix <= i and i < yi < y from the current pure facts. The action runs only if both checks 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 also initialize the SMT support; the next section explains these calls and completes the array demo.

Summary

A verification condition combines spatial reasoning (matching resources) with pure reasoning (list equations, integer bounds); purification automates the spatial reasoning and produces an ordinary logic goal for the pure reasoning.
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 completes purification by converting a purified factfact/empemp entailment into an ordinary logic formula.
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 it uses the same strategies: registering a .strategies.strategies file supports both discharging explicit VCs and automatically executing reads and writes through data-structure predicates, for sllsll and, with checkcheck-guarded rules, for array segments.