Backward Proof for Separation Logic

In the previous section, we wrote goals as [Gamma ?- p][Gamma ?- p] and used tactics to decompose a general Boolean proposition into subgoals in a goal tree. C*‘s verification conditions are usually separation-logic entailments: in addition to handling propositions, the prover must split, select, and recombine linear heap resources. This section extends general goal trees with a goal representation and tactics for manipulating these resources, using the sllsll predicate introduced earlier.

We use a lemma from a list-reversal example: the sll_unfoldsll_unfold lemma that the forward-proof section used as an existing theorem. Here we prove it under the name unfold_sll_not_nullunfold_sll_not_null.

Recall the singly linked list predicate sll pt lsll pt l, which describes a linked list starting at address ptpt with logical contents given by the integer list ll:

// struct list { int head; struct list *tail; }, with Tlist, Fhead, Ftail
// registered as in the section on separation logic in C*
PROOF thm sll_def = cst_new_rec_definition(
  "sll", get_theorem_by_name("list_RECURSION"),
  `(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)`,
  `:addr->(int)list->hprop`);

// struct list { int head; struct list *tail; }, with Tlist, Fhead, Ftail
// registered as in the section on separation logic in C*
PROOF thm sll_def = cst_new_rec_definition(
  "sll", get_theorem_by_name("list_RECURSION"),
  `(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)`,
  `:addr->(int)list->hprop`);

An empty linked list is represented by the null pointer. A non-empty list’s head node owns the headhead and tailtail fields, and the tail pointer qq points to the linked list representing the remaining contents tt. cst_new_rec_definitioncst_new_rec_definition is a helper from the examples’ user library (userlib/qcp/veriftime.huserlib/qcp/veriftime.h): it creates the recursive definition and exports the new constant to the engine in one call. PROOFPROOF is the standard library’s shorthand for [[cst::proof]][[cst::proof]].

forall l pt.
  ~(pt == 0i)
  ==> (sll pt l |--
        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)

forall l pt.
  ~(pt == 0i)
  ==> (sll pt l |--
        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)

Proving this lemma requires several steps beyond unfolding the definition once: introduce the universal quantifiers and the pure antecedent ~(pt == 0i)~(pt == 0i); turn sll pt l |-- ...sll pt l |-- ... into a goal suited to manipulating resources; case-split on ll, using the contradiction in the empty branch; unfold sllsll in the non-empty branch and destructure the existential and separating conjunction; supply the three witnesses hh, tt, qq for the heap conclusion; and simplify the pure fact while framing away the spatial resources common to both sides.

We will follow these steps, starting with how a goal represents the resource structure.

A general goal keeps the entailment a black box. The previous section’s general goal was [Gamma ?- p][Gamma ?- p]. After introducing the outer universal quantifiers and the implication of unfold_sll_not_nullunfold_sll_not_null, we get:

(The boxes on this page are schematic. The tactics print general goals under Assumptions:Assumptions: and Conclusion:Conclusion:, and separation-logic goals under Assumptions:Assumptions:, Antecedents:Antecedents: and Consequent:Consequent:. They also label an automatically introduced assumption HH; we use P_ptP_pt to distinguish it from the heap antecedent HH below.) This is a general goal: the whole entailment sll pt l |-- ...sll pt l |-- ... is treated as one boolbool conclusion. The goal tree records the proposition to prove without exposing the entailment’s structure. The prover cannot manipulate heap resources by label as it does ordinary assumptions, and a goal transformation may change the entailment’s shape.

A separation-logic goal exposes the structure. We use this notation throughout:

p, q               : bool
H, K, P, Q         : hprop
Lambda             : ordered, labeled ordinary-logic antecedents
Delta              : ordered, labeled heap antecedents
ant(Delta)         = the separating conjunction of Delta's heap assertions

p, q               : bool
H, K, P, Q         : hprop
Lambda             : ordered, labeled ordinary-logic antecedents
Delta              : ordered, labeled heap antecedents
ant(Delta)         = the separating conjunction of Delta's heap assertions

The two kinds of antecedents print in separate regions:

For the linked-list lemma, entering this goal mode gives:

Here, P_ptP_pt is an ordinary-logic antecedent available for rewriting and contradiction, HH is a resource that can be used only through separation-logic rules, and the heap conclusion remains whole. This division reflects the structure of a separation-logic proof.

From an entailment: SL_MODESL_MODE.

The safest starting form names the whole antecedent "H""H":

gnode_list gns = SL_MODE(gn, "H");

gnode_list gns = SL_MODE(gn, "H");

If you know the antecedent’s structure, you can destructure it when entering goal mode. The pattern language has five constructs:

The parser uses parentheses to determine structure and defines no operator precedence, so a complex pattern must be parenthesized explicitly:

SL_MODE(g, "H_1 * ((x ? H_2) | H_3)");

SL_MODE(g, "H_1 * ((x ? H_2) | H_3)");

From a heap-assertion equality: EQ_SLTACEQ_SLTAC. Another common goal is that two heap assertions are equal. Here SL_MODESL_MODE does not apply; instead one uses antisymmetry to split the equality into two directed entailments.

The two branches have separate label namespaces, so L_1L_1 and L_2L_2 may be the same name.

In a separation-logic goal, we first examine the resources in DeltaDelta. These differ from ordinary-logic antecedents in their linearity: each resource is used exactly once and cannot be freely copied or discarded.

Destructuring the outer structure. For a single labeled heap antecedent, the most common atomic tactics are:

All of these preserve the heap conclusion. For instance, splitting a separating conjunction has the following form:

     [Lambda; Delta_R,L_1:P,L_2:Q ?- K]
------------------------------------------------
          [Lambda; Delta,L:(P ** Q) ?- K]

     [Lambda; Delta_R,L_1:P,L_2:Q ?- K]
------------------------------------------------
          [Lambda; Delta,L:(P ** Q) ?- K]

A separating conjunction yields one subgoal because both resources exist together; a disjunction yields two because the state may satisfy either side. Opening an existential requires a name that does not capture the goal’s free variables.

To destructure a whole antecedent recursively:

gnode_list HANT_DESTRUCT_SLTAC(
  const gnode gn, const char *L, const char *pattern);
gnode_list AUTO_HANT_DESTRUCT_SLTAC(const gnode gn);

gnode_list HANT_DESTRUCT_SLTAC(
  const gnode gn, const char *L, const char *pattern);
gnode_list AUTO_HANT_DESTRUCT_SLTAC(const gnode gn);

The first follows a given pattern. The second traverses the context in order, recursively splitting every visible ****, ||||, and existsexists, and continues on each new disjunction branch until no such outer structure remains.

Moving pure facts to the ordinary-logic region. To let fact(p)fact(p) take part in ordinary-logic rewriting, arithmetic, or contradiction, move it from the heap region into LambdaLambda:

gnode INTRO_FACT_SLTAC(
  const gnode gn, const const_cstr_list lbs);
gnode AUTO_INTRO_FACT_SLTAC(const gnode gn);

gnode INTRO_FACT_SLTAC(
  const gnode gn, const const_cstr_list lbs);
gnode AUTO_INTRO_FACT_SLTAC(const gnode gn);

INTRO_FACT_SLTACINTRO_FACT_SLTAC selects pure facts by label; the automatic version selects every top-level fact(p)fact(p) in the current heap antecedents. Once moved, these propositions behave like the ordinary assumptions in the previous section.

Rewriting, the magic wand, and closing contradictory branches. Three more common actions:

• HANT_CONV_SLTACHANT_CONV_SLTAC: rewrite named heap antecedents with a conversion;
• WAND_MP_SLTACWAND_MP_SLTAC: from (P -* Q)(P -* Q) and a resource PP, produce the resource QQ;
• CONTR_SLTACCONTR_SLTAC: close a branch when some heap antecedent normalizes to fact(false)fact(false).

For example, in the empty-list branch of the linked-list case, unfolding sll pt []sll pt [] gives fact(pt == 0i)fact(pt == 0i). Rewriting it with the ordinary-logic antecedent ~(pt == 0i)~(pt == 0i) yields a contradictory resource, which CONTR_SLTACCONTR_SLTAC then closes.

Heap antecedents describe the available resources; the heap conclusion describes what remains to be proved. The conclusion KK is kept whole, and its outermost structure determines which tactic applies.

A separating conjunction partitions resources. If the goal is K_1 ** K_2K_1 ** K_2, the two sides cannot both inherit all resources the way an ordinary-logic conjunction does. The prover must say which antecedent resources go to the left subgoal, with the rest going to the right:

Disjunction, existentials, and pure facts. The remaining tactics for the heap conclusion are also grouped by its structure:

For example:

     [Lambda; Delta ?- H[w/x]]
-------------------------------- EXISTS_SLTAC w
 [Lambda; Delta ?- exists x. H]

     [Lambda; Delta ?- H[w/x]]
-------------------------------- EXISTS_SLTAC w
 [Lambda; Delta ?- exists x. H]

where the witness must have the same type as the existential variable.

Many separation-logic goals hold semantically but have different syntactic forms on the two sides: a definition is unfolded on only one side, a pure fact has not been simplified, or the ****s are associated or ordered differently. To prove such goals, first normalize both sides, then cancel common resources.

Conversion and cleanup.

gnode CONV_SLTAC(const gnode gn, const conv cv);
gnode CONV_WITH_ASMP_SLTAC(
  const gnode gn,
  conv (*cvf)(thm_list),
  const thm_list ths);
gnode CLEAN_SLTAC(const gnode gn);
void EMP_SLTAC(const gnode gn);

gnode CONV_SLTAC(const gnode gn, const conv cv);
gnode CONV_WITH_ASMP_SLTAC(
  const gnode gn,
  conv (*cvf)(thm_list),
  const thm_list ths);
gnode CLEAN_SLTAC(const gnode gn);
void EMP_SLTAC(const gnode gn);

CONV_SLTACCONV_SLTAC rewrites the heap conclusion and every heap antecedent in turn. CONV_WITH_ASMP_SLTACCONV_WITH_ASMP_SLTAC also passes the ordinary-logic antecedents in LambdaLambda to the conversion as assumption theorems. This allows the conversion to unfold definitions and then simplify with the current branch’s facts. CLEAN_SLTACCLEAN_SLTAC removes units such as empemp and fact(true)fact(true) and normalizes the rest. If normalization leaves the heap conclusion as empemp and every heap antecedent as empemp or a trivially true fact, EMP_SLTACEMP_SLTAC closes the goal.

Framing. Besides EMP_SLTACEMP_SLTAC, the most common way to finish is to cancel resources common to both sides:

gnode FRAME_SLTAC(
  const gnode gn, const const_cstr_list labels);
gnode AUTO_FRAME_SLTAC(const gnode gn);

gnode FRAME_SLTAC(
  const gnode gn, const const_cstr_list labels);
gnode AUTO_FRAME_SLTAC(const gnode gn);

FRAME_SLTACFRAME_SLTAC selects heap antecedents by label, finds equal occurrences in the top-level multiset of the heap conclusion, and cancels them together (without closing the goal); AUTO_FRAME_SLTACAUTO_FRAME_SLTAC greedily cancels matchable resources in antecedent order, then cleans up units, closing the goal if it has become trivial.

Frame matching uses occurrence counts. If the antecedent has two copies of a resource but the conclusion has only one, that conclusion resource cannot be matched twice. Heap resources form a multiset, whereas ordinary-logic assumptions form a set.

Proofs often begin with the same sequence of mechanical steps: enter separation-logic goal mode, destructure heap antecedents, remove units, introduce pure facts, and attempt framing. The library packages these steps as a combined tactic.

The tactic first introduces the ordinary-logic quantifiers and antecedents, then enters separation-logic goal mode. It next destructures the visible heap antecedents, removes trivial resources, moves top-level pure facts into the ordinary-logic region, and attempts to cancel directly matchable frame resources. Because destructuring a disjunction may create branches, it returns all current unfinished leaves rather than a single gnodegnode.

We can now combine these tactics to prove the linked-list lemma from the opening, using AUTO_INIT_SLTACAUTO_INIT_SLTAC for the initial steps:

PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode gn = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(gn, `l:(int)list`, "P_l");
  gn = gns[0];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(gn, "H");
  gn = gns[1];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  gn = AUTO_HANT_DESTRUCT_SLTAC(gn)[0];
  gn = LIST_EXISTS_SLTAC(
    gn, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  gn = CONV_SLTAC(gn, simp_conv(thm_list_n(0)));
  gn = AUTO_FRAME_SLTAC(gn);
  return gnode_prove(root);
}

PROOF thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode gn = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(gn, `l:(int)list`, "P_l");
  gn = gns[0];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(gn, "H");
  gn = gns[1];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  gn = AUTO_HANT_DESTRUCT_SLTAC(gn)[0];
  gn = LIST_EXISTS_SLTAC(
    gn, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  gn = CONV_SLTAC(gn, simp_conv(thm_list_n(0)));
  gn = AUTO_FRAME_SLTAC(gn);
  return gnode_prove(root);
}

Initialize: from a general goal to a resourced goal. AUTO_INIT_SLTACAUTO_INIT_SLTAC introduces the outer quantifiers and antecedents and sets up the separation-logic goal. Only one unfinished leaf remains, so the example takes the first element of the returned list.

Case-split on the logical list. CASES_TAC(gn, CASES_TAC(gn, l:(int)list, "P_l"), "P_l") changes only the ordinary-logic antecedents, so both subgoals stay in separation-logic goal mode. The empty branch gains l = []l = []; the non-empty branch gains l = a0 :: a1l = a0 :: a1.

Empty branch: unfold to a contradiction. Unfold sll pt []sll pt [] with sll_defsll_def, then simplify with the branch’s logical antecedent; the resource HH becomes contradictory, and CONTR_SLTACCONTR_SLTAC closes the branch.

Non-empty branch: unfold, supply witnesses, frame. Unfolding the definition exposes the non-null fact, the head and tail fields, and the successor sllsll. AUTO_HANT_DESTRUCT_SLTACAUTO_HANT_DESTRUCT_SLTAC destructures the outer **** and existsexists to obtain independent labeled resources. The case split and unfolding have already determined the three witnesses, which LIST_EXISTS_SLTACLIST_EXISTS_SLTAC supplies. CONV_SLTACCONV_SLTAC then simplifies the pure fact l == a0 :: a1l == a0 :: a1. The remaining spatial resources on both sides match term by term, so AUTO_FRAME_SLTACAUTO_FRAME_SLTAC cancels them all and closes the goal.

Finally, we call gnode_prove(root)gnode_prove(root). Every leaf in the tree is closed, so this call reconstructs the proof from the leaves to the root and returns the theorem for the original lemma.

AUTO_INIT_SLTACAUTO_INIT_SLTAC shows how to package a recurring sequence of mechanical steps. Users can compose existing tactics in the same way to automate specific parts of their own proofs.

If every step yields a single subgoal, chain them directly:

gnode MY_CLEAN_FRAME_SLTAC(const gnode gn) {
  gnode next_gn = CLEAN_SLTAC(gn);
  next_gn = AUTO_INTRO_FACT_SLTAC(next_gn);
  next_gn = AUTO_FRAME_SLTAC(next_gn);
  return next_gn;
}

gnode MY_CLEAN_FRAME_SLTAC(const gnode gn) {
  gnode next_gn = CLEAN_SLTAC(gn);
  next_gn = AUTO_INTRO_FACT_SLTAC(next_gn);
  next_gn = AUTO_FRAME_SLTAC(next_gn);
  return next_gn;
}

Tactics for disjunctions or separating-conjunction conclusions may produce branches. In that case, the next tactic must be applied to all current leaves:

gnode_list gns = AUTO_HANT_DESTRUCT_SLTAC(gn);
APPLY_ALL_TAC(CLEAN_SLTAC, gns);
gns = gnode_leaves(gn);

gnode_list gns = AUTO_HANT_DESTRUCT_SLTAC(gn);
APPLY_ALL_TAC(CLEAN_SLTAC, gns);
gns = gnode_leaves(gn);

Fetch gnode_leavesgnode_leaves again after applying the tactic: the previous step may have closed some goals or created new branches, so the old list may no longer contain exactly the subtree’s unfinished leaves.

The previous section described the general soundness mechanism: when a tactic expands a goal, it must record a validation function. Once the subgoals have been proved, this function reconstructs the parent theorem, and gnode_provegnode_prove reduces the whole tree to the root’s theorem. Separation-logic tactics reuse this mechanism.

A separation-logic goal [Lambda; Delta ?- K][Lambda; Delta ?- K] is only a structured presentation of the proposition |Lambda| ?- (ant(Delta) |-- K)|Lambda| ?- (ant(Delta) |-- K). When a tactic relabels, splits an antecedent, or chooses a conclusion, its validation function calls the forward rules already proved in proof_slproof_sl to recover the original entailment. Frame elimination, for instance, temporarily removes the common resources in the subgoal, and the validation rebuilds the parent with the frame rule.

Separation-logic tactics must also preserve resource linearity: ordinary-logic antecedents are checked as a set, and heap antecedents as a multiset with occurrence counts. One resource cannot be consumed twice. If labels, resource counts, variable freshness, or types do not meet a tactic’s requirements, the tactic fails; it never treats an unmet condition as a fact.

• A general goal treats H |-- KH |-- K as one whole proposition; a separation-logic goal keeps the ordinary-logic antecedents, the labeled heap antecedents, and the heap conclusion separate, directly reflecting the resource structure.
• SL_MODESL_MODE handles a separation-logic entailment; EQ_SLTACEQ_SLTAC handles a heap-assertion equality via two directed implications.
• HANT_*_SLTACHANT_*_SLTAC analyze existing resources; INTRO_FACT_SLTACINTRO_FACT_SLTAC moves pure facts into the ordinary-logic region; SEP_SLTACSEP_SLTAC and the disjunction/existential tactics build the heap conclusion.
• Conversion and cleanup are uniform; FRAME_SLTACFRAME_SLTAC and AUTO_FRAME_SLTACAUTO_FRAME_SLTAC cancel common resources by occurrence count.
• Combined tactics like AUTO_INIT_SLTACAUTO_INIT_SLTAC suit mechanical steps; branching, witnesses, and resource partitioning usually need the prover’s explicit input.
• Separation-logic tactics still rebuild theorems through goal-tree validation functions, ultimately checked by the HOL kernel.

The linked-list example follows a common sequence: initialize the goal, case-split on the pure data, unfold the spatial predicate, supply witnesses, normalize both sides, and frame away common resources. Proofs over more complex data structures use the same sequence.