Proved View Shifts

In the forward-proof section, the list-reversal loop needed a proof block before it could read v->tailv->tail: the block instantiated an unfolding lemma and pushed the result into the state with local_applylocal_apply. Yet the symbolic state at that point already contained sll v_v l2sll v_v l2 — the loop owned the entire remaining list. What exactly was missing?

Not memory. What was missing is a view of that memory in which the cell for v->tailv->tail appears as a resource the symbolic-execution engine can use directly:

data_at (field_addr v_v Tlist Ftail) Tptr nxt

data_at (field_addr v_v Tlist Ftail) Tptr nxt

A symbolic state is a logical description of the resources owned and the facts known at the current program point. Even when the concrete memory does not change at all, the same state can be described by several different separation-logic assertions.

Which shape of view the engine demands comes from the next action to check, not only from how we like to think about the algorithm. Two demands recur constantly.

Consider the two statements at the heart of the reversal loop:

struct list *t = v->tail;
v->tail = w;

struct list *t = v->tail;
v->tail = w;

To check them mechanically, the current view must expose the cell that v->tailv->tail denotes:

data_at (field_addr v_v Tlist Ftail) Tptr nxt

data_at (field_addr v_v Tlist Ftail) Tptr nxt

This one resource says everything the engine needs: the address field_addr v_v Tlist Ftailfield_addr v_v Tlist Ftail is owned and accessible, the cell is interpreted at type TptrTptr, a load yields nxtnxt, and after a store the value component becomes the stored value. If the state only contains sll v_v l2sll v_v l2, we logically own that cell, but it has not been exposed in a form the engine can use for this access.

Suppose a callee’s precondition is P x ** Q yP x ** Q y, while the caller’s resources are currently folded inside another predicate R x yR x y. Applying the contract requires a local entailment first:

R x y |-- P x ** Q y

R x y |-- P x ** Q y

presenting the resources as the separating conjuncts the precondition can match. After the call, the postcondition may need to be folded back into the view the caller maintains. So view changes are not a quirk of field access; they are the basic step that lets modular contracts connect.

Recall the singly-linked-list predicate:

sll pt []       =  fact(pt == 0i)
sll pt (h :: t) =  fact(~(pt == 0i)) **
                   exists q.
                     data_at (field_addr pt Tlist Fhead) Tint h **
                     data_at (field_addr pt Tlist Ftail) Tptr q **
                     sll q t

sll pt []       =  fact(pt == 0i)
sll pt (h :: t) =  fact(~(pt == 0i)) **
                   exists q.
                     data_at (field_addr pt Tlist Fhead) Tint h **
                     data_at (field_addr pt Tlist Ftail) Tptr q **
                     sll q t

This definition does three jobs at once: it inventories and encapsulates the concrete resources that make up the list; it supplies the logical list as the model for functional-correctness reasoning; and it is itself the logical connection between the folded view and the exposed-node view.

When ptpt is non-null and the contents are h :: th :: t, the folded view sll pt (h :: t)sll pt (h :: t) and the following exposed-node view describe the same node and its successor list:

fact(~(pt == 0i)) **
exists q.
  data_at (field_addr pt Tlist Fhead) Tint h **
  data_at (field_addr pt Tlist Ftail) Tptr q **
  sll q t

fact(~(pt == 0i)) **
exists q.
  data_at (field_addr pt Tlist Fhead) Tint h **
  data_at (field_addr pt Tlist Ftail) Tptr q **
  sll q t

Neither view is “more real”: the folded view suits treating the whole list as one logical object; the exposed view suits verifying a field access on the current node. They simply draw different resource boundaries for different reasoning steps.

A field update on a list node follows a fixed rhythm:

folded view          sll pt (h :: t)
  |  view shift: unfold, backed by an entailment theorem
exposed view         two field cells as data_at
  |  C read / store, handled by symbolic execution
updated cells        the tail cell holds its new value
  |  view shift: fold, backed by an entailment theorem
updated folded view  sll reflects the new field value

folded view          sll pt (h :: t)
  |  view shift: unfold, backed by an entailment theorem
exposed view         two field cells as data_at
  |  C read / store, handled by symbolic execution
updated cells        the tail cell holds its new value
  |  view shift: fold, backed by an entailment theorem
updated folded view  sll reflects the new field value

The prover does not chase one canonical way of writing the state; it keeps the view in step with the action currently being checked.

Only one interface between proof code and the symbolic state is needed here:

PROOF {
  term st = get_symbolic_state();
  thm vs_thm = /* prove  |- st |-- st'  */;
  set_symbolic_state(vs_thm);
}

PROOF {
  term st = get_symbolic_state();
  thm vs_thm = /* prove  |- st |-- st'  */;
  set_symbolic_state(vs_thm);
}

get_symbolic_state()get_symbolic_state() returns the current full state as a termterm. Proof code may inspect it and compute a candidate new view — but a candidate term is not enough. set_symbolic_stateset_symbolic_state accepts only a closed theorem of a full-state entailment

|- S |-- S'

|- S |-- S'

whose antecedent must match the current state modulo the associativity, commutativity, and units (ACU) of the separating conjunction; only then does the consequent become the new current state.

Both styles must end at a theorem of the same shape; they differ in where the target view comes from.

We compare the two at a single program point: exposing the current node before v->tailv->tail in the reversal loop. The loop splits the list into a reversed prefix sll w_v l1sll w_v l1 and an unprocessed suffix sll v_v l2sll v_v l2, related to the original list by a pure model fact. At loop entry the branch carries (eliding the local-variable cells):

fact(l == REVERSE l1 ++ l2) **
fact(~(v_v == 0i)) **
sll w_v l1 **
sll v_v l2 **
...

fact(l == REVERSE l1 ++ l2) **
fact(~(v_v == 0i)) **
sll w_v l1 **
sll v_v l2 **
...

The declarative version (10_reverse_decl.c10_reverse_decl.c) writes out the entire view it wants installed, then proves the entailment backward on the goal tree:

PROOF {
  term target_symst = `exists l1 hd tl w_v v_v q.
    fact(l == (REVERSE l1) ++ (hd :: tl)) **
    fact(~(v_v == 0i)) **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr q **
    sll q tl **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre
  `;
  gnode root =
      gnode_new_with_ccl(mk_sl_ent(get_symbolic_state(), target_symst));
  /* case-split on l2; the empty case contradicts ~(v_v == 0i); the cons case
     unfolds sll, supplies the witnesses, and frames the rest. */
  set_symbolic_state(gnode_prove(root));
}

PROOF {
  term target_symst = `exists l1 hd tl w_v v_v q.
    fact(l == (REVERSE l1) ++ (hd :: tl)) **
    fact(~(v_v == 0i)) **
    sll w_v l1 **
    data_at (field_addr v_v Tlist Fhead) Tint hd **
    data_at (field_addr v_v Tlist Ftail) Tptr q **
    sll q tl **
    data_at v__addr Tptr v_v **
    data_at w__addr Tptr w_v **
    data_at pt__addr Tptr pt__pre
  `;
  gnode root =
      gnode_new_with_ccl(mk_sl_ent(get_symbolic_state(), target_symst));
  /* case-split on l2; the empty case contradicts ~(v_v == 0i); the cons case
     unfolds sll, supplies the witnesses, and frames the rest. */
  set_symbolic_state(gnode_prove(root));
}

The target already decides everything: l2l2 must be split as hd :: tlhd :: tl, the current node must become two field cells, qq heads the list for tltl — and the reversed prefix plus every local-variable cell must be written into the target, or the entailment simply does not hold. Since the complete consequent is given, a goal-directed proof is natural: the tactics from the backward-proof section (CASES_TACCASES_TAC, conversions, existential tactics, AUTO_FRAME_SLTACAUTO_FRAME_SLTAC) decompose current |-- targetcurrent |-- target step by step, and goal-tree validation reassembles the final theorem for set_symbolic_stateset_symbolic_state.

The operational version (10_reverse_op.c10_reverse_op.c) declares no target at all. It names an operation and the parameters that identify where to apply it:

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

Read it as: “unfold the non-empty list at v_vv_v, and give the newly produced logical variables these three names.” The operation selects sll v_v l2sll v_v l2 from the current resources (not sll w_v l1sll w_v l1), checks the non-nullness premise against the branch’s facts, instantiates a lemma proved once at declaration time, preserves everything else as the frame, and commits the same kind of entailment theorem the declarative version proved by hand. How unfold_sll_not_nullunfold_sll_not_null is declared — and what exactly happens on application — is the subject of the next section.

An operation’s lemma talks about a small footprint only. For the unfold above, the underlying local entailment is:

~(v_v == 0i) ==>
  (sll v_v l2
   |--
   exists hd tl nxt.
     fact(l2 == hd :: tl) **
     data_at (field_addr v_v Tlist Fhead) Tint hd **
     data_at (field_addr v_v Tlist Ftail) Tptr nxt **
     sll nxt tl)

~(v_v == 0i) ==>
  (sll v_v l2
   |--
   exists hd tl nxt.
     fact(l2 == hd :: tl) **
     data_at (field_addr v_v Tlist Fhead) Tint hd **
     data_at (field_addr v_v Tlist Ftail) Tptr nxt **
     sll nxt tl)

The current branch also holds the reversed prefix, the model fact, and the local-variable cells. The key service of the operational library is lifting the small-footprint entailment to the full state.

H ** F |-- H' ** F

H ** F |-- H' ** F

exists X. (H ** F) |-- exists X. (H' ** F)

exists X. (H ** F) |-- exists X. (H' ** F)

This is exactly what local_apply(symhp, local_ent)local_apply(symhp, local_ent) — familiar from the forward-proof section — performs: it locates the local antecedent among the branch’s top-level separating conjuncts, checks the local theorem’s pure premises (here fact(~(v_v == 0i))fact(~(v_v == 0i))) against that branch’s facts, keeps every remaining resource as , and returns the branch-level entailment.

A full symbolic state may be a disjunction of several branches. Once each branch has its theorem, disjunction monotonicity combines them:

|- symhp_1 || ... || symhp_n  |--  symhp_1' || ... || symhp_n'

|- symhp_1 || ... || symhp_n  |--  symhp_1' || ... || symhp_n'

The whole proof-generation chain is:

local_ent
  -- local_apply: frame + existential lifting -->  branch entailment
  -- disjunction monotonicity ----------------->  full-state entailment
  -- set_symbolic_state ----------------------->  committed view

local_ent
  -- local_apply: frame + existential lifting -->  branch entailment
  -- disjunction monotonicity ----------------->  full-state entailment
  -- set_symbolic_state ----------------------->  committed view

The operational library splits its proof functions into two complementary layers.

These understand no particular data structure; each expresses one common state-shaping intent:

When a representation predicate keeps exhibiting the same stable consume/produce relationship, that relationship deserves to be declared once as a domain operation: unfolding and folding empty and non-empty list nodes, focusing an array cell, splitting and joining array segments, filling an uninitialized region, exposing and re-packing a tree node. A call site then supplies only the parameters that express where — the operation selects the resources, checks the pure premises, instantiates its proved lemma, and produces the target view.

• The same concrete memory admits many separation-logic views; data_atdata_at exposes an accessible cell, and a representation predicate organizes concrete resources, the functional model, and the connection between its views.
• A view shift is witnessed by an S |-- S'S |-- S' theorem and executes no program; local_applylocal_apply lifts a small-footprint entailment to a branch by frame and existential lifting, checking pure premises as branch facts, and disjunction monotonicity merges branches.
• Declarative reasoning states the complete target; operational reasoning states the operation, and the library computes the target view together with its entailment theorem.
• The library offers generic state transformers for common shaping intents and domain operations for stable predicate transitions — with the intent localized, the frame is preserved automatically, and the committed change is always a kernel-checked theorem.