Declaring and Applying Operations

EN | 中文

The previous section ended with a one-line operational unfold, taking the operation itself as a given tool. This section explains where that tool comes from: how a sound local resource transformation is packaged as an operation — a consume/produce schema with a proof obligation discharged at declaration time — and how one application turns into a single committed full-state theorem. The running example is the verified tutorial/10_reverse_op.ctutorial/10_reverse_op.c: in-place list reversal in which every view shift is expressed by an operation or a generic state transformer.

The Repeated Work an Operation Removes

The unfolding lemma behind the previous section’s example exists once and for all; what recurs is everything around it. At every program point that unfolds a list node, the user must again:

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 sll w_v l1sll w_v l1 sitting next to it;
discharge the premise ~(v_v == 0i)~(v_v == 0i) from the branch’s facts;
settle on 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 wrote this glue by hand for one program point. Ten unfold sites mean ten copies of it, and a change to the lemma’s statement means ten repairs.

Definition 1 (Operation). An operation is a parameterized protocol for one local resource transformation: a proved lemma packaged together with how to instantiate its parameters and how to select the resources it consumes from the current state. Declaring one is writing its schema; applying one runs the 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 division between inputsinputs and the rest matters: the caller provides only the stable parameters it already knows (here, an address); the unknown data inside the resources — the logical list, the successor pointer — is recovered from the current state by matching.

A Real Declaration

An operation is declared with decl_operationdecl_operation, which requires a proof callback of the same name with suffix _proof_proof to be defined first. Here is the unfold used throughout this part, exactly as 10_reverse_op.c10_reverse_op.c declares it; the callback proves the schema’s obligation on the spot, with the 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 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 obligation the callback proves is essentially the unfolding lemma of the backward-proof section — proved once, at declaration time, and never again at a use site.

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 quantifier order is not an interface guarantee, which is why the callback receives the goal as goal_tmgoal_tm and must prove the supplied term rather than reconstructing one that looks the same.

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). Only when both the schema checks and the proof-callback checks pass does the resulting operation carry its closed lemma. A failing proof, a theorem with leftover 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 [] — a good first place to observe 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 names the list as a cons in its own contract — as the capsule preconditions sll p (h :: t)sll p (h :: t) in the PSI section do — the consume pattern can match the cons by shape, with nested captures:


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


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

Such an unfold requires no non-nullness premise at all; instead it produces fact(~(pt == 0i))fact(~(pt == 0i)), which is exactly the premise the fold operation consumes later. In the reversal loop below, the invariant names the suffix by an abstract list l2l2, so the premise-based schema above is the right one.

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

A consume entry does double duty: it is one antecedent conjunct of the lemma, and it is a pattern describing how to find 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 is not 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 a logical value that already exists in the state — it does not invent 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. Only after all consumes have selected successfully does the library try to prove the deferred equalities — by exact equality, then solve_eqsolve_eq; what remains unsolved 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 runs: select the head cell keyed by ptpt, capturing the head value hh; select the tail cell keyed by ptpt, capturing the cell’s current value qq; then use the just-captured qq as the key to select the successor list, capturing its contents tt; produce 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 top-level conjuncts not yet used, and a committed 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 keeps behavior predictable — and puts the burden on the schema to use sufficiently discriminating KEYKEYs.

What Declaration Checks

With the markers understood, the declaration-time validation of operation_newoperation_new can be stated in full:

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, so nothing is checked about whether some program point actually holds the consumed resources or satisfies the required facts — that belongs to application.

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, so that a schema variable named ll can never collide with a state variable that happens to share the name;
selects resources for the consumes, left to right, greedy, 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. What is finally committed is one closed full-state entailment — never a direct, proof-free edit of the symbolic state.

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 is the argument instantiating the input ptpt, while hdhd, tltl, nxtnxt are merely names for 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, be pairwise distinct, and must not capture a free variable of the produced body; the same vector is used for every branch. Stable names matter because the proof code that follows — an assert_fact_stassert_fact_st, an abbrev_stabbrev_st — will refer to them.

The Reversal Loop, Operationally

The complete function from the verified 10_reverse_op.c10_reverse_op.c (its four operation declarations appear above; unfold_sll_nullunfold_sll_null is symmetric to fold_sll_nullfold_sll_null, converting 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 instead of writing it down. fold_sll_nullfold_sll_null — the simplest operation — 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 clears the temporary defining equations that were only needed to introduce the names. What remains is exactly the state the loop maintains, so the code simply snapshots it:


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 — the KEYKEY rejects sll w_v l1sll w_v l1 — discharges the premise from that fact, and exposes the node, naming the new existentials 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 survives untouched; unfolding only added the structural fact l2 == hd :: tll2 == hd :: tl. The store v->tail = w;v->tail = w; is a genuine program action — after it, the same state holds except that the tail cell reads 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, the tail cell — capturing its current value w_vw_v — and, keyed by that capture, sll w_v l1sll w_v l1; it checks ~(v_v == 0i)~(v_v == 0i) and produces sll v_v (hd :: l1)sll v_v (hd :: l1), with sll nxt tlsll nxt tl untouched in the frame. The tail cell’s current value decides which list gets folded in: that is why the same fold schema serves both this loop and the accessor capsules of the PSI section.

Bookkeeping: Restore the Invariant’s Shape

The rest of the body is pure-model and naming bookkeeping, all by generic transformers:

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]") retires the old round’s names, and the two abbrev_stabbrev_st calls install l1 = hd :: l1'l1 = hd :: l1' and l2 = tll2 = tl as the new round’s lists; forget_facts_stforget_facts_st then clears the temporary equations;
after each cursor assignment, rename_locals_strename_locals_st restores the current-value naming for the C variables — introducing a fresh w_vw_v or v_vv_v binder for the cell’s new value and freshening the previous binder to 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 already shows the invariant’s resource shape with the new lists in place — sll v_v l1sll v_v l1 is the extended prefix and sll nxt l2sll nxt l2 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 entailment the engine checks 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 knows 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 — and substitute_stsubstitute_st rewrites sll w_v l1sll w_v l1 into sll w_v (REVERSE l)sll w_v (REVERSE l), which is the postcondition for return w;return w;.

Example 4 (Operational and declarative steps, each in their place). The spatial transitions — the four unfold/fold operations — are protocol-like and reusable: they compute the post-state from the current one. The model equations — l == (REVERSE (hd :: l1)) ++ tll == (REVERSE (hd :: l1)) ++ tl, l1 == REVERSE ll1 == REVERSE l — are stated by the user and handed to assert_fact_stassert_fact_st to prove. Operational for resource protocols; declarative for pure targets: the two styles interleave freely.

When to Declare an Operation

A resource action is a good 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 — an address, an endpoint, an owner. Typical examples: unfolding and folding data-structure nodes, opening and closing array segments, converting between abstract representations, consuming a linear token and producing its successor.

Conversely, there is usually no need for a new operation 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 runs on four operations plus generic transformers, following the rhythm unfold — program access — fold — model update; the loop invariant is built by the same transformers and then snapshotted with get_symbolic_stateget_symbolic_state.