Declaring and Applying Operations

EN | 中文

The previous section ended by unfolding a list node with one line of operational proof code, using an existing operation. This section explains how to declare and apply an operation: a sound local resource transformation described by a consume/produce schema, with a proof obligation discharged at declaration time. Applying the operation produces a single full-state theorem to commit. The running example is the verified tutorial/10_reverse_op.ctutorial/10_reverse_op.c, which reverses a list in place and expresses every view shift through an operation or a generic state transformer.

The Repeated Work an Operation Removes

The unfolding lemma in the previous section needs to be proved only once, but applying it requires repeated work. At each program point that unfolds a list node, the user must:

instantiate the lemma’s parameters with the current pointer and list (v_vv_v, l2l2);
select the right resource — sll v_v l2sll v_v l2, not the adjacent sll w_v l1sll w_v l1;
discharge the premise ~(v_v == 0i)~(v_v == 0i) from the branch’s facts;
choose stable names for the existential variables the unfolding produces;
keep every other resource as the frame, and commit the full-state entailment — once per branch if the state has several.

The forward-proof section supplied this code by hand for one program point. Ten unfold sites require ten copies of that code, all of which must be updated if the lemma’s statement changes.

Definition 1 (Operation). An operation is a parameterized protocol for one local resource transformation: it packages a proved lemma with instructions for instantiating its parameters and selecting the resources it consumes from the current state. To declare an operation, we write its schema; applying it performs selection, instantiation, lifting, and commit automatically.

Declaring an Operation

The Five Parts

A schema can be summarized as:


O = (name, inputs, consumes, facts, produce)


O = (name, inputs, consumes, facts, produce)

Part	Question it answers	Unfolding a non-empty list
`namename`	how is it bound and diagnosed?	`unfold_sll_not_nullunfold_sll_not_null`
`inputsinputs`	what does the caller supply?	`ptpt`
`consumesconsumes`	which resources are selected?	`sll pt lsll pt l`
`factsfacts`	which pure premises must hold?	`~(pt == 0i)~(pt == 0i)`
`produceproduce`	what do the selected resources become?	`exists h t q. ...exists h t q. ...`

The caller supplies inputsinputs: the stable parameters it already knows, here an address. Matching recovers unknown data within the resources, such as the logical list and successor pointer, from the current state.

A Real Declaration

An operation is declared with decl_operationdecl_operation. A proof callback whose name is the operation’s name followed by _proof_proof must be defined first. The following unfold operation is used throughout this part and is declared exactly as in 10_reverse_op.c10_reverse_op.c. Its callback proves the schema’s obligation using backward separation-logic tactics:


PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode g = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(g, `l:(int)list`, "P_l");
  g = gns[0];                       // l == []: contradicts ~(pt == 0i)
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(g, "H");
  g = gns[1];                       // l == a0 :: a1: unfold and match
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  g = AUTO_HANT_DESTRUCT_SLTAC(g)[0];
  g = LIST_EXISTS_SLTAC(g, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  g = CONV_SLTAC(g, simp_conv(thm_list_n(0)));
  g = AUTO_FRAME_SLTAC(g);
  return gnode_prove(root);
}
decl_operation(unfold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(1, `sll (KEY pt) (CAPTURE l)`),
  term_list_n(1, `~(pt == 0i)`),
  `exists h t q.
    fact(l == h :: t) **
    data_at (field_addr pt Tlist Fhead) Tint h **
    data_at (field_addr pt Tlist Ftail) Tptr q **
    sll q t`
)


PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode g = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(g, `l:(int)list`, "P_l");
  g = gns[0];                       // l == []: contradicts ~(pt == 0i)
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(g, "H");
  g = gns[1];                       // l == a0 :: a1: unfold and match
  g = CONV_WITH_ASMP_SLTAC(g, rewrite_conv, THM_LIST(sll_def));
  g = AUTO_HANT_DESTRUCT_SLTAC(g)[0];
  g = LIST_EXISTS_SLTAC(g, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  g = CONV_SLTAC(g, simp_conv(thm_list_n(0)));
  g = AUTO_FRAME_SLTAC(g);
  return gnode_prove(root);
}
decl_operation(unfold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(1, `sll (KEY pt) (CAPTURE l)`),
  term_list_n(1, `~(pt == 0i)`),
  `exists h t q.
    fact(l == h :: t) **
    data_at (field_addr pt Tlist Fhead) Tint h **
    data_at (field_addr pt Tlist Ftail) Tptr q **
    sll q t`
)

Reading the schema from top to bottom: the operation is named unfold_sll_not_nullunfold_sll_not_null; the caller supplies the address ptpt; one resource is consumed, the sllsll at ptpt, whose logical list is captured as ll; the pure premise ~(pt == 0i)~(pt == 0i) must hold before application; and the selected resource becomes the structural fact l == h :: tl == h :: t, the two field cells, and the tail list. The callback proves essentially the unfolding lemma from the backward-proof section. This proof is required once at declaration time and need not be repeated at use sites.

The Soundness Goal

KEYKEY, CAPTURECAPTURE, and DEFERDEFER are identity functions in the logic; they carry meaning only for matching. To build the soundness goal, the library first erases them:


erase(CAPTURE t) = erase(KEY t) = erase(DEFER t) = t


erase(CAPTURE t) = erase(KEY t) = erase(DEFER t) = t

For consumes , facts , and produce , the generated goal is:


forall FV.
  f1 ==> ... ==> fn ==>
    (erase(c1) ** ... ** erase(cm) |-- Q)


forall FV.
  f1 ==> ... ==> fn ==>
    (erase(c1) ** ... ** erase(cm) |-- Q)

with all free schema variables universally quantified. The interface does not guarantee the quantifier order. The callback therefore receives the goal as goal_tmgoal_tm and must prove that term rather than reconstructing a similar-looking goal.

decl_operationdecl_operation expands to a call of operation_newoperation_new, which validates the schema, invokes the callback once on the generated goal, and checks the returned theorem: it must carry no undischarged hypotheses, and its conclusion must be α-equivalent to the goal.

Proposition 2 (Declaration introduces no unproved transformation). The resulting operation carries its closed lemma only after both the schema checks and the proof-callback checks pass. A failed proof, a theorem with undischarged hypotheses, or a proof of the wrong statement makes the declaration fail; there is no axiom or unchecked fallback path.

The Simplest Schema

Folding the empty list has no inputs and no pure premises:


decl_operation(fold_sll_null,
  term_list_n(0),
  term_list_n(1, `emp`),
  term_list_n(0),
  `sll 0i []`
)


decl_operation(fold_sll_null,
  term_list_n(0),
  term_list_n(1, `emp`),
  term_list_n(0),
  `sll 0i []`
)

It expresses the local resource transformation emp |-- sll 0i []emp |-- sll 0i []. This simple example lets us inspect the inputsinputs / consumesconsumes / factsfacts / produceproduce fields and the lemma=<proved>lemma=<proved> tag in an operation value.

A variant that needs no premise

When every use site’s contract expresses the list as a cons, as in the capsule preconditions sll p (h :: t)sll p (h :: t) in the PSI section, the consume pattern can match the cons by shape using nested captures:


sll (KEY pt) ((CAPTURE h) :: (CAPTURE t))


sll (KEY pt) ((CAPTURE h) :: (CAPTURE t))

This unfold requires no non-nullness premise and produces fact(~(pt == 0i))fact(~(pt == 0i)), the premise the fold operation consumes later. In the reversal loop below, the invariant represents the suffix by an abstract list l2l2, so we use the schema with a premise shown above.

Consume Patterns: `KEYKEY`, `CAPTURECAPTURE`, `DEFERDEFER`

A consume entry serves as both an antecedent conjunct of the lemma and a pattern for finding the corresponding resource in the branch. Matching proceeds left to right and uses three markers.

`KEYKEY`: Locate by Provable Equality

Suppose the branch holds both


sll w_v l1 ** sll v_v l2


sll w_v l1 ** sll v_v l2

and the operation is called with pt := v_vpt := v_v. The pattern sll (KEY pt) (CAPTURE l)sll (KEY pt) (CAPTURE l) is tried against the first candidate sll w_v l1sll w_v l1: this requires proving v_v = w_vv_v = w_v, which fails, so the candidate is rejected. Against the second candidate, v_v = v_vv_v = v_v holds, and sll v_v l2sll v_v l2 is selected.

KEY tKEY t matches by provable equality rather than string comparison. The library tries to establish the equality in order: exact equality; integer arithmetic when both sides are integers; then the normalization rules configured with set_normalization_rulesset_normalization_rules. KEYKEY filters candidates but does not guarantee uniqueness: if several resources satisfy the pattern, the first one is chosen. Schemas should therefore key on stable semantic identities: addresses, endpoints, owners.

`CAPTURECAPTURE`: Recover Unknowns from the State

After sll v_v l2sll v_v l2 is selected, CAPTURE lCAPTURE l yields the binding l := l2l := l2. CAPTURE xCAPTURE x must introduce a schema variable not yet bound; a variable is captured at most once, and later consumes may then use it directly or inside KEYKEY and DEFERDEFER. A capture reads an existing logical value from the state; it does not introduce a witness.

`DEFERDEFER`: Postpone an Equality Check

With pp and vv already bound, the pattern


data_at (KEY p) Tint (DEFER v)


data_at (KEY p) Tint (DEFER v)

matched against data_at p Tint ndata_at p Tint n locates the resource by KEY pKEY p, while DEFER vDEFER v only checks that vv and nn have compatible types and records the pending equality v = nv = n. After all consumes have selected successfully, the library tries to prove the deferred equalities, first by exact equality and then by solve_eqsolve_eq. Any unsolved equality is registered as a tracked obligation.

The Three Markers, Side by Side

Marker	During selection	Main use
`KEY tKEY t`	equality with the candidate must be proved	filter resources by semantic identity
`CAPTURE xCAPTURE x`	binds the candidate subterm to a fresh variable	recover unknown logical data or models
`DEFER tDEFER t`	type compatibility only	prove the equality after selection, leaving an obligation if needed

A plain variable may also appear in a pattern, but it must already be bound — by an input or an earlier capture — and then matches its bound value exactly.

Dependencies Between Consumes

Folding a non-empty node needs three resources, and later patterns use earlier captures:


decl_operation(fold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(3,
    `data_at (field_addr (KEY pt) Tlist Fhead) Tint (CAPTURE h)`,
    `data_at (field_addr (KEY pt) Tlist Ftail) Tptr (CAPTURE q)`,
    `sll (KEY q) (CAPTURE t)`
  ),
  term_list_n(1, `~(pt == 0i)`),
  `sll pt (h :: t)`
)


decl_operation(fold_sll_not_null,
  TERM_LIST(`pt:addr`),
  term_list_n(3,
    `data_at (field_addr (KEY pt) Tlist Fhead) Tint (CAPTURE h)`,
    `data_at (field_addr (KEY pt) Tlist Ftail) Tptr (CAPTURE q)`,
    `sll (KEY q) (CAPTURE t)`
  ),
  term_list_n(1, `~(pt == 0i)`),
  `sll pt (h :: t)`
)

Matching first selects the head cell keyed by ptpt and captures the head value hh. It then selects the tail cell keyed by ptpt and captures the cell’s current value qq. Finally, it uses the captured qq as the key to select the successor list and capture its contents tt. The operation produces sll pt (h :: t)sll pt (h :: t). Its proof callback plays the same role as before, this time proving the fold direction of the list lemma.

Each consume selects the first matching resource among the unused top-level conjuncts. Once made, a choice is never revisited:


consume_1 selects the first matching resource
    |
consume_2 selects among the remaining resources
    |
a later failure does not send consume_1 back to try another candidate


consume_1 selects the first matching resource
    |
consume_2 selects among the remaining resources
    |
a later failure does not send consume_1 back to try another candidate

This deterministic, greedy policy makes matching predictable and requires schemas to use sufficiently discriminating KEYKEYs.

What Declaration Checks

At declaration time, operation_newoperation_new performs the following checks:

every entry of inputsinputs is a HOL variable, and they are pairwise distinct;
consumes are scanned left to right: CAPTURE xCAPTURE x must introduce a fresh variable; a plain variable, and every free variable inside a KEYKEY or DEFERDEFER argument, must already be bound; lambda abstractions are not supported in patterns;
every free variable of consumes, facts, and produce comes from an input or a capture;
the proof callback returns a hypothesis-free theorem whose conclusion is α-equivalent to the generated goal.

No symbolic state exists at declaration time. Whether a program point holds the consumed resources and satisfies the required facts is checked when the operation is applied.

Applying an Operation

Two State Interfaces


PROOF void apply_operation_st(
    const operation op, const term_list arguments);
PROOF void apply_operation_named_st(
    const operation op, const term_list arguments,
    const term_list existential_names);


PROOF void apply_operation_st(
    const operation op, const term_list arguments);
PROOF void apply_operation_named_st(
    const operation op, const term_list arguments,
    const term_list existential_names);

apply_operation_stapply_operation_st applies the operation to every branch of the current state. apply_operation_named_stapply_operation_named_st performs the same transformation and additionally renames, positionally, the outer existential prefix of the produced assertion.

One Application, Step by Step

For each branch, the application interface:

binds argumentsarguments to inputsinputs positionally, checking count and types;
freshens the non-input schema variables against the branch, preventing a schema variable named ll from colliding with a state variable of the same name;
selects resources for the consumes greedily from left to right among unused top-level conjuncts, accumulating the captures;
tries each DEFERDEFER equality with solve_eqsolve_eq, aligning the pattern with the actual resource;
instantiates the operation’s closed lemma with the inputs and captures;
proves the required facts from the branch’s top-level facts — propositional reasoning first, then integer arithmetic — and discharges them;
lifts the resulting local entailment with local_applylocal_apply, framing the unselected resources and preserving the outer existentials;
combines the branch theorems into one full-state entailment, and commits it with a single set_symbolic_stateset_symbolic_state call after all branches have succeeded.

Different branches may capture different values and produce different post-states, but the operation must apply to every branch.

Proposition 3 (From local soundness to full-state soundness). The operation’s lemma proves the consumes-to-produce transformation; the frame rule preserves the untouched resources of each branch; disjunction monotonicity merges the branches. The commit uses one closed full-state entailment; it never edits the symbolic state without a proof.

Renaming Only Renames


PROOF apply_operation_named_st(
    unfold_sll_not_null,
    TERM_LIST(`v_v:addr`),
    TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));


PROOF apply_operation_named_st(
    unfold_sll_not_null,
    TERM_LIST(`v_v:addr`),
    TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));

Here v_vv_v instantiates the input ptpt, while hdhd, tltl, nxtnxt name the three outermost existentials of the produced assertion. Their values come from the operation’s existential quantifiers; they are not user-supplied witnesses. The name vector must match the produced binders in count and type. Its names must be pairwise distinct and must not capture a free variable of the produced body; every branch uses the same vector. Stable names allow subsequent proof code, such as an assert_fact_stassert_fact_st or an abbrev_stabbrev_st, to refer to these variables. Proof blocks can use these names directly. An annotation that the compiler elaborates in C scope, such as a [[cst::where]][[cst::where]] on a later call or an inner loop’s invariant, cannot. For these annotations, [[cst::given(`hd:int`, `nxt:addr`)]];[[cst::given(`hd:int`, `nxt:addr`)]]; first binds the names from the current state, as described in Function Contracts, Loop Invariants, and Assertions.

The Reversal Loop, Operationally

The following is the complete function from the verified 10_reverse_op.c10_reverse_op.c. Three of its operation declarations appear above; the fourth, unfold_sll_nullunfold_sll_null, is symmetric to fold_sll_nullfold_sll_null and converts sll pt lsll pt l into fact(l == [])fact(l == []) under the premise pt == 0ipt == 0i:


PROOF void forget_facts_st(term_list facts) {
  for (int i = 0; i < vector_size(facts); i++) {
    forget_fact_st(facts[i]);
  }
}
struct list *reverse(struct list *pt)
  PARAM(`l:(int)list`)
  REQUIRE(`sll pt l`)
  ENSURE(`sll __return (REVERSE l)`)
{
  PROOF set_default_types(TERM_LIST(
    `l:(int)list`, `l1:(int)list`, `l2:(int)list`,
    `w_v:int`, `v_v:int`, `pt__pre:int`
  ));
  struct list *w, *v;
  w = (void *)0;
  PROOF {
    // create the reversed prefix list `l1` (initially `[]`),
    // pointed by `w_v` (initially `NULL`)
    apply_operation_st(fold_sll_null, NULL);
    abbrev_st(`w_v = 0i`);
    abbrev_st(`l1 = []`);
  }
  v = pt;
  PROOF {
    // mark the unprocessed suffix list `l2` (initially `l`),
    // pointed by `v_v` (initially `pt__pre`)
    abbrev_occurrences_st(
      `v_v == pt__pre`,
      TERM_LIST(
        `data_at v__addr Tptr v_v`,
        `sll v_v l`
    ));
    abbrev_st(`l2 = l`);
    assert_fact_st(
      `l == (REVERSE l1) ++ l2`,
      simp_conv, THM_LIST(REVERSE_def, APPEND_def));
  }
  PROOF forget_facts_st(TERM_LIST(
    `l2 == l`, `v_v == pt__pre`, `l1 == []`, `w_v == 0i`
  ));
  PROOF term loop_inv = get_symbolic_state();
  while (v)
    INV(loop_inv)
  {
    PROOF apply_operation_named_st(
      unfold_sll_not_null,
      TERM_LIST(`v_v:addr`),
      TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));
    struct list *t = v->tail;
    v->tail = w;
    PROOF apply_operation_st(
      fold_sll_not_null,
      TERM_LIST(`v_v:addr`)
    );
    PROOF forget_fact_st(`~(v_v == 0i)`);
    PROOF {
      assert_fact_st(
        `l == (REVERSE (hd :: l1)) ++ tl:(int)list`, simp_conv,
        THM_LIST(REVERSE_def, APPEND_def, gsym_rule(APPEND_ASSOC)));
      rename_hexists_st("[l1'/l1] [l2'/l2]");
      abbrev_st(`l1 = hd :: l1':(int)list`);
      abbrev_st(`l2 = tl:(int)list`);
    }
    PROOF forget_facts_st(TERM_LIST(
      `l2 == tl`,
      `l1 == hd :: l1'`,
      `l == REVERSE l1' ++ l2'`,
      `l2' == hd :: l2`
    ));
    w = v;
    PROOF rename_locals_st();
    v = t;
    PROOF rename_locals_st();
    PROOF {
      substitute_st(sym_rule(assume_rule(`w_v == v_v'`)));
      substitute_st(sym_rule(assume_rule(`v_v == nxt`)));
      forget_facts_st(TERM_LIST(`w_v == v_v'`, `v_v == nxt`));
    }
  }
  PROOF apply_operation_st(unfold_sll_null, TERM_LIST(`v_v:addr`));
  PROOF assert_fact_st(`l1 == (REVERSE l):(int)list`, simp_conv,
    THM_LIST(APPEND_NIL, REVERSE_REVERSE)
  );
  PROOF substitute_st(assume_rule(`l1 == (REVERSE l):(int)list`));
  return w;
}


PROOF void forget_facts_st(term_list facts) {
  for (int i = 0; i < vector_size(facts); i++) {
    forget_fact_st(facts[i]);
  }
}
struct list *reverse(struct list *pt)
  PARAM(`l:(int)list`)
  REQUIRE(`sll pt l`)
  ENSURE(`sll __return (REVERSE l)`)
{
  PROOF set_default_types(TERM_LIST(
    `l:(int)list`, `l1:(int)list`, `l2:(int)list`,
    `w_v:int`, `v_v:int`, `pt__pre:int`
  ));
  struct list *w, *v;
  w = (void *)0;
  PROOF {
    // create the reversed prefix list `l1` (initially `[]`),
    // pointed by `w_v` (initially `NULL`)
    apply_operation_st(fold_sll_null, NULL);
    abbrev_st(`w_v = 0i`);
    abbrev_st(`l1 = []`);
  }
  v = pt;
  PROOF {
    // mark the unprocessed suffix list `l2` (initially `l`),
    // pointed by `v_v` (initially `pt__pre`)
    abbrev_occurrences_st(
      `v_v == pt__pre`,
      TERM_LIST(
        `data_at v__addr Tptr v_v`,
        `sll v_v l`
    ));
    abbrev_st(`l2 = l`);
    assert_fact_st(
      `l == (REVERSE l1) ++ l2`,
      simp_conv, THM_LIST(REVERSE_def, APPEND_def));
  }
  PROOF forget_facts_st(TERM_LIST(
    `l2 == l`, `v_v == pt__pre`, `l1 == []`, `w_v == 0i`
  ));
  PROOF term loop_inv = get_symbolic_state();
  while (v)
    INV(loop_inv)
  {
    PROOF apply_operation_named_st(
      unfold_sll_not_null,
      TERM_LIST(`v_v:addr`),
      TERM_LIST(`hd:int`, `tl:(int)list`, `nxt:addr`));
    struct list *t = v->tail;
    v->tail = w;
    PROOF apply_operation_st(
      fold_sll_not_null,
      TERM_LIST(`v_v:addr`)
    );
    PROOF forget_fact_st(`~(v_v == 0i)`);
    PROOF {
      assert_fact_st(
        `l == (REVERSE (hd :: l1)) ++ tl:(int)list`, simp_conv,
        THM_LIST(REVERSE_def, APPEND_def, gsym_rule(APPEND_ASSOC)));
      rename_hexists_st("[l1'/l1] [l2'/l2]");
      abbrev_st(`l1 = hd :: l1':(int)list`);
      abbrev_st(`l2 = tl:(int)list`);
    }
    PROOF forget_facts_st(TERM_LIST(
      `l2 == tl`,
      `l1 == hd :: l1'`,
      `l == REVERSE l1' ++ l2'`,
      `l2' == hd :: l2`
    ));
    w = v;
    PROOF rename_locals_st();
    v = t;
    PROOF rename_locals_st();
    PROOF {
      substitute_st(sym_rule(assume_rule(`w_v == v_v'`)));
      substitute_st(sym_rule(assume_rule(`v_v == nxt`)));
      forget_facts_st(TERM_LIST(`w_v == v_v'`, `v_v == nxt`));
    }
  }
  PROOF apply_operation_st(unfold_sll_null, TERM_LIST(`v_v:addr`));
  PROOF assert_fact_st(`l1 == (REVERSE l):(int)list`, simp_conv,
    THM_LIST(APPEND_NIL, REVERSE_REVERSE)
  );
  PROOF substitute_st(assume_rule(`l1 == (REVERSE l):(int)list`));
  return w;
}

(set_default_typesset_default_types declares implicit HOL types for the listed variable names, so the quotations that follow need fewer type ascriptions.)

Initialization: Build the Invariant, Then Snapshot It

The two entry blocks construct the loop invariant through state transformations, without an explicit invariant assertion. The simplest operation, fold_sll_nullfold_sll_null, turns empemp into the empty reversed prefix sll 0i []sll 0i []; the abbrev_stabbrev_st and abbrev_occurrences_stabbrev_occurrences_st calls introduce the logical names w_vw_v, l1l1, v_vv_v, l2l2 for the values involved; assert_fact_stassert_fact_st proves the model equation l == (REVERSE l1) ++ l2l == (REVERSE l1) ++ l2 by simplification; and forget_facts_stforget_facts_st removes the temporary defining equations used to introduce the names. The remaining state is exactly what the loop maintains, so the code saves a snapshot:


PROOF term loop_inv = get_symbolic_state();
while (v)
  INV(loop_inv)


PROOF term loop_inv = get_symbolic_state();
while (v)
  INV(loop_inv)

The loop invariant, as snapshotted


exists w_v v_v l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll v_v l2 **
    sll w_v l1


exists w_v v_v l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll v_v l2 **
    sll w_v l1

The Loop Body: Unfold, Access, Fold

Inside the body, the loop condition contributes fact(~(v_v == 0i))fact(~(v_v == 0i)), so unfold_sll_not_nullunfold_sll_not_null applies. It selects sll v_v l2sll v_v l2 using KEYKEY to reject sll w_v l1sll w_v l1, discharges the premise from the branch fact, and exposes the node with new existentials named hdhd, tltl, nxtnxt. Symbolic execution can then check the read. After struct list *t = v->tail;struct list *t = v->tail; the engine reports:

Symbolic state after struct list *t = v->tail;struct list *t = v->tail;


exists nxt hd tl w_v l1 l2 v_v.
    fact (~(v_v == 0i)) **
    fact (l == REVERSE l1 ++ l2) **
    fact (l2 == hd :: tl) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr nxt **
    sll nxt tl


exists nxt hd tl w_v l1 l2 v_v.
    fact (~(v_v == 0i)) **
    fact (l == REVERSE l1 ++ l2) **
    fact (l2 == hd :: tl) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr nxt **
    sll nxt tl

The old model fact remains unchanged; unfolding adds the structural fact l2 == hd :: tll2 == hd :: tl. The store v->tail = w;v->tail = w; updates memory. After it, the same state holds except that the tail cell is described by data_at (field_addr v_v Tlist Ftail) Tptr w_vdata_at (field_addr v_v Tlist Ftail) Tptr w_v.

Now fold_sll_not_nullfold_sll_not_null consumes the head cell and the tail cell, capturing the tail cell’s current value w_vw_v. Using that capture as the key, it consumes sll w_v l1sll w_v l1, checks ~(v_v == 0i)~(v_v == 0i), and produces sll v_v (hd :: l1)sll v_v (hd :: l1), preserving sll nxt tlsll nxt tl in the frame. The tail cell’s current value determines which list is folded in, allowing the same fold schema to serve both this loop and the accessor capsules of the PSI section.

Bookkeeping: Restore the Invariant’s Shape

The rest of the body uses generic transformers to maintain the pure model and the variable names:

forget_fact_st(~(v_v == 0i))forget_fact_st(~(v_v == 0i)) drops the premise the invariant does not carry;
assert_fact_stassert_fact_st proves the updated model equation l == (REVERSE (hd :: l1)) ++ tll == (REVERSE (hd :: l1)) ++ tl by simplification with the REVERSEREVERSE/APPENDAPPEND lemmas — a declarative step embedded in the operational flow;
rename_hexists_st("[l1'/l1] [l2'/l2]")rename_hexists_st("[l1'/l1] [l2'/l2]") renames the previous iteration’s lists, and the two abbrev_stabbrev_st calls define l1 = hd :: l1'l1 = hd :: l1' and l2 = tll2 = tl for the next iteration; forget_facts_stforget_facts_st then removes the temporary equations;
after each cursor assignment, rename_locals_strename_locals_st restores the current-value names for the C variables: it introduces a fresh w_vw_v or v_vv_v binder for the cell’s new value and gives the previous binder a history name such as v_v'v_v';
the two substitute_stsubstitute_st calls rewrite the remaining resources from the history names to the new cursor names, and one last forget_facts_stforget_facts_st drops the renaming equations.

After w = v;w = v;, the engine shows the invariant’s resource shape with the updated lists: sll v_v l1sll v_v l1 is the extended prefix and sll nxt l2sll nxt l2 is the shortened suffix:

Symbolic state after w = v;w = v;


exists w_v v_v nxt l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr v_v **
    data_at pt__addr Tptr pt__pre **
    sll nxt l2 **
    sll v_v l1


exists w_v v_v nxt l1 l2.
    fact (l == REVERSE l1 ++ l2) **
    data_at t__addr Tptr nxt **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr v_v **
    data_at pt__addr Tptr pt__pre **
    sll nxt l2 **
    sll v_v l1

Once the cursors and names are aligned, the state matches the snapshotted loop_invloop_inv. The engine checks this entailment at the end of the body. (The cell of the block-local variable tt is reclaimed automatically by symbolic execution when the block ends; no proof code deletes it.)

Exit: The Suffix Is Empty

On exit, the branch has the fact v_v == 0iv_v == 0i, so unfold_sll_nullunfold_sll_null converts sll v_v l2sll v_v l2 into fact(l2 == [])fact(l2 == []). assert_fact_stassert_fact_st then proves l1 == REVERSE ll1 == REVERSE l from l == REVERSE l1 ++ l2l == REVERSE l1 ++ l2, l2 == []l2 == [], and REVERSE_REVERSEREVERSE_REVERSE. Finally, substitute_stsubstitute_st rewrites sll w_v l1sll w_v l1 into sll w_v (REVERSE l)sll w_v (REVERSE l), the postcondition for return w;return w;.

Example 4 (Operational and declarative steps, each in their place). The four unfold/fold operations describe reusable spatial transitions that compute the post-state from the current state. The user states the model equations l == (REVERSE (hd :: l1)) ++ tll == (REVERSE (hd :: l1)) ++ tl, l1 == REVERSE ll1 == REVERSE l and uses assert_fact_stassert_fact_st to prove them. The proof freely interleaves operational steps for resource protocols with declarative steps for pure targets.

When to Declare an Operation

A resource action is suitable for an operation when it recurs at several program points, has a clear, provable consume/produce protocol, needs to capture unknown parameters from the state, and selects resources by a semantic identity such as an address, endpoint, or owner. Typical examples include unfolding and folding data-structure nodes, opening and closing array segments, converting between abstract representations, and consuming a linear token to produce its successor.

A new operation is usually unnecessary for:

a one-off local entailment — apply it directly with apply_hconv_stapply_hconv_st;
a global rewrite or substitution — use rewrite_strewrite_st and its relatives;
a one-time existential introduction made only to tidy the state — abbrev_stabbrev_st;
several resource phases with a C memory access in between — that is never one operation.

Common Failures and Where to Look

Symptom	First check
declaration fails	variable sources, consume-pattern structure, and the callback’s hypotheses and conclusion
argument count or type error	do `argumentsarguments` correspond to `inputsinputs`, position by position?
a consume resource is not found	is the `KEYKEY` discriminating enough, and is the resource an unused top-level conjunct?
an unexpected resource is matched	is the schema relying on greedy order where it needs another semantic `KEYKEY`?
tracked obligations appear	why can the required fact or `DEFERDEFER` equality not be proved automatically?
the renaming interface fails	name count, types, pairwise distinctness, and variable capture
some branches succeed, the whole application fails	can the operation apply to every top-level branch?

When debugging, answer three questions in order: is the schema itself well-formed, with its closed proof? Does every branch complete instantiation, matching, and premise checking? Can all branches be framed, merged, and committed together?

Summary

An operation packages a proved local resource transformation with its parameter instantiation and resource selection; inputs come from the caller, captures come from the state, and facts state the pure premises.
KEYKEY filters resources by provable equality, CAPTURECAPTURE binds unknowns, DEFERDEFER postpones equality checks; consumes select left to right, greedily, and never backtrack.
Declaration validates the schema and demands a closed, α-equivalent lemma from the proof callback — there is no unproved fallback; resource matching happens at application time, per branch, with one commit for the whole state.
The reversal proof uses four operations and generic transformers in the sequence unfold — program access — fold — model update; the same transformers build the loop invariant, which is then snapshotted with get_symbolic_stateget_symbolic_state.