C*: Unifying Program and Proof in C

Proved View Shifts

EN | 中文

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 applied the result to the state with local_applylocal_apply. The symbolic state at that point already contained sll v_v l2sll v_v l2, so the loop owned the entire remaining list. Why was the unfolding step still needed?

The engine needed a view of that memory that exposed the cell for v->tailv->tail as a resource it could use directly:

data_at (field_addr v_v Tlist Ftail) Tptr nxt
data_at (field_addr v_v Tlist Ftail) Tptr nxt

Same Memory, Different Views

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, several different separation-logic assertions can describe the same state.

Definition 1 (View). A view is a separation-logic assertion describing the current concrete memory. Two views may draw different resource boundaries, use different logical names, and carry different functional models, while both being sound descriptions of the same state. A new view may forget information — it need not be logically equivalent to the old one — and shifting views never changes the memory at run time.

The view the engine requires depends on the next action to check, as well as on how we reason about the algorithm. Two requirements recur throughout verification.

Memory Access Needs an Addressable Cell

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 resource provides the information the engine needs: the cell at address field_addr v_v Tlist Ftailfield_addr v_v Tlist Ftail is owned and accessible, it is interpreted at type TptrTptr, a load yields nxtnxt, and a store replaces its value component with 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.

Calls Need the Precondition’s Shape

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

This entailment presents the resources as separating conjuncts that match the precondition. After the call, the postcondition may need to be folded back into the view the caller maintains. View changes thus support both field access and the composition of modular contracts.

The Representation Predicate Ties the Views Together

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 serves three purposes: it lists and encapsulates the concrete resources that make up the list; it supplies the logical list as the model for functional-correctness reasoning; and it establishes the logical connection between the folded view and the exposed-node view.

Two Views of a Non-Empty Node

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

Both views describe the same concrete memory: the folded view lets us treat the whole list as one logical object, while the exposed view lets us verify a field access on the current node. They draw different resource boundaries for different reasoning steps.

Shifts Alternate with Program Actions

A field update on a list node proceeds as follows:

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 chooses a view suited to the action being checked; there is no need for a single canonical way to write the state.

A View Shift Is an Entailment Theorem

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 it must also prove the change valid. 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.

Definition 2 (Proved view shift). A view shift is a separation-logic entailment S |-- S'S |-- S' from the current state to a new view, together with the theorem proving it.
Proposition 3 (Soundness is witnessed by the theorem). A function that computes view shifts may use any method to match, instantiate, and select resources: it extends the ways of producing proofs without adding unconditional reasoning principles. An implementation bug can cause failure or produce an unexpected but still proved view; it cannot make the kernel accept an invalid entailment. The theorem witness guarantees logical soundness; it does not replace testing and review of the function’s intended behavior.

Declarative and Operational View Shifts

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

Declarative Operational
the user supplies the complete target view an operation to perform
the system first obtains the open goal S |-- S'S |-- S' with its entailment proof
typical proof direction goal-directed, starting from the stated consequent forward, starting from the current state
untouched resources written into the target, then cancelled by frame tactics preserved automatically by the lifting machinery

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 contains the following assertions, in the engine’s order and with the local-variable cells omitted:

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

Declarative: State the Result

The declarative version (10_reverse_decl.c10_reverse_decl.c) writes out the entire target view, 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 specifies each part of the result: l2l2 must be split as hd :: tlhd :: tl, the current node must be exposed as two field cells, and qq must point to the list for tltl. The reversed prefix and every local-variable cell must also be written into the target for the entailment to 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.

Operational: State the Intent

The operational version (10_reverse_op.c10_reverse_op.c) does not declare a target view. 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, and instantiates a lemma proved once at declaration time. It preserves the remaining resources as the frame and commits the same kind of entailment theorem that the declarative version proved by hand. The next section explains how to declare unfold_sll_not_nullunfold_sll_not_null and what happens when it is applied.

How a Local Entailment Reaches the Full State

An operation’s lemma concerns only a small footprint. 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 operational library lifts the small-footprint entailment to the full state.

Proposition 4 (Frame and existential lifting).

If H |-- H'H |-- H' is proved, then for any frame not involved in the change:

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

and if the branch has outer existential variables :

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

The local_apply(symhp, local_ent)local_apply(symhp, local_ent) function introduced in the forward-proof section performs this lifting: 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, preserves 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

Two Layers of Operational Support

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

Generic State Transformers

These functions are independent of any particular data structure; each expresses a common operation on the state:

Intent Representative interface
rewrite with theorem schemas rewrite_strewrite_st
substitute exactly, or by consuming an equality fact substitute_stsubstitute_st, substitute_fact_stsubstitute_fact_st
introduce a logical name for an expression abbrev_stabbrev_st, abbrev_occurrences_stabbrev_occurrences_st
prove, add, or forget facts assert_fact_stassert_fact_st, add_fact_stadd_fact_st, forget_fact_stforget_fact_st
tidy existential and local-value names rename_hexists_strename_hexists_st, rename_locals_strename_locals_st
apply a one-off local entailment apply_hconv_stapply_hconv_st

Domain Operations

When reasoning about a representation predicate repeatedly uses the same consume/produce relationship, we can declare that relationship once as a domain operation. Examples include unfolding and folding empty and non-empty list nodes, focusing an array cell, splitting and joining array segments, filling an uninitialized region, and exposing and re-packing a tree node. A call site then supplies only the parameters that identify where to apply the operation; the operation selects the resources, checks the pure premises, instantiates its proved lemma, and produces the target view.

Choosing a Style

Current reasoning intent Reach for
the complete target view is known and used once a declarative target with a goal-directed proof
the post-state follows from a definite equation or conversion a generic state transformer
a stable, reusable representation transition a domain operation
a self-contained pure proposition inside an operational flow a local goal-directed proof, e.g. assert_fact_stassert_fact_st

Summary

  • 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 operations on the state and domain operations for stable predicate transitions. The user specifies a local reasoning action; the library preserves the frame automatically and justifies every committed change with a kernel-checked theorem.