Backward Proof for Separation Logic

In the previous section a goal was uniformly written [Gamma ?- p][Gamma ?- p], and a tactic decomposed one general boolean proposition into subgoals through a goal tree. But C*‘s verification conditions are usually separation-logic entailments: the prover must not only handle propositions, but split, choose, and recombine linear heap resources. This section introduces a dedicated goal representation and tactic family for exactly that, building on the general goal trees of the previous section (cross-link the sllsll predicate as we go).

We anchor the discussion on one lemma from a list-reversal example. It is precisely the sll_unfoldsll_unfold lemma that the forward-proof section reused as a ready-made theorem; here we finally prove it.

Recall the singly-linked-list predicate sll pt lsll pt l, which describes a list starting at address ptpt whose logical contents are the integer list ll:

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

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

The empty list is the null pointer; a non-empty list’s head node owns the headhead and tailtail fields, and the tail pointer qq points to the list for the rest tt.

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)

Although it looks like just “unfold the definition once,” the lemma really packs several distinct proof actions: 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, breaking out 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.

The section follows those steps. First: is a general goal enough to express this 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:

This is a general goal: the whole entailment sll pt l |-- ...sll pt l |-- ... is treated as one boolbool conclusion. The goal tree knows it is a proposition to prove, but nothing about the entailment’s structure. The prover cannot manipulate heap resources by label the way it manipulates ordinary assumptions, and any transform of the goal risks damaging 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

It prints as two antecedent regions:

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

Now P_ptP_pt is an ordinary-logic antecedent usable for rewriting and contradiction, HH is a resource usable only by separation-logic rules, and the heap conclusion stays whole. This split mirrors 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 the antecedent’s structure is known, you can destructure while entering. The pattern language has just four constructs:

The parser reads structure from parentheses and imposes 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.

Inside a separation-logic goal, the prover first faces the resources already in DeltaDelta. Their fundamental difference from ordinary-logic antecedents is linearity: a resource is used exactly once — it 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 keep the heap conclusion. For instance, splitting a separating conjunction is abstractly:

     [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 (both resources exist together); a disjunction yields two (the state may satisfy either side); opening an existential must choose a name not capturing 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 walks the context in order, recursively splitting every visible ****, ||||, and existsexists, continuing 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 picks the named labels; the automatic version picks every top-level fact(p)fact(p) in the current heap antecedents. Once moved, these propositions behave like the previous section’s ordinary assumptions.

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.

Analyzing heap antecedents answers “what do I have”; operating on the heap conclusion answers “what must I still build.” The conclusion KK is kept whole, and the tactic is chosen by its outermost structure.

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 conclusion-side tactics group by 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 already hold semantically; only the two sides differ syntactically — a definition is unfolded on one side, a pure fact is unsimplified, or the ****s are associated and ordered differently. Such goals need normalizing first, then cancelling 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 additionally hands the ordinary-logic antecedents in LambdaLambda to the conversion as assumption theorems, so it suits “unfold by definition, then simplify with the current branch’s facts.” CLEAN_SLTACCLEAN_SLTAC deletes units like empemp and fact(true)fact(true) and normalizes the rest. If after normalizing the heap conclusion is empemp and every heap antecedent is 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 goes by occurrence count. If the antecedent has two copies of a resource but the conclusion only one, the same conclusion resource cannot be matched twice. This resource multiset is the key difference from an ordinary-logic assumption set.

Entering separation-logic goal mode, destructuring heap antecedents, cleaning units, introducing pure facts, and attempting to frame are all mechanical steps that frequently open a proof in the same order. The library therefore packages them as a combined tactic.

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

We now have every atomic tactic the proof needs, and we know which steps AUTO_INIT_SLTACAUTO_INIT_SLTAC combines at the start. Back to the linked-list lemma from the opening, threading the tools together:

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

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 does the outer introductions and sets up the resourced goal; after it, 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/tail fields, and the successor sllsll. AUTO_HANT_DESTRUCT_SLTACAUTO_HANT_DESTRUCT_SLTAC turns the outer **** and existsexists into independent labeled resources. The case-split and unfolding have already fixed the three witnesses, so LIST_EXISTS_SLTACLIST_EXISTS_SLTAC supplies them; CONV_SLTACCONV_SLTAC simplifies the pure fact l == a0 :: a1l == a0 :: a1; the remaining spatial resources on both sides match term by term, and AUTO_FRAME_SLTACAUTO_FRAME_SLTAC cancels them all and closes the goal.

Finally, gnode_prove(root)gnode_prove(root) — every leaf in the tree is closed, so it can rebuild bottom-up and return the theorem for the original lemma.

AUTO_INIT_SLTACAUTO_INIT_SLTAC shows how the library wraps a stable mechanical routine. Users can compose existing tactics the same way, building smaller, more targeted automatic steps for 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;
}

But tactics like disjunction or a separating-conjunction conclusion may branch. Then 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);

Re-fetching gnode_leavesgnode_leaves matters: the previous step may have closed some goals or spawned new branches, so the old list need not still represent the subtree’s unfinished work.

The previous section already covered the general soundness mechanism: when a tactic expands a goal it must record a validation function; once the subgoals have theorems, the validation rebuilds the parent theorem, and gnode_provegnode_prove reduces the whole tree to the root’s theorem. Separation-logic tactics reuse that 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.

The extra thing to guarantee is resource linearity: ordinary-logic antecedents are checked as a set, heap antecedents as a multiset by occurrence count. One resource cannot be consumed twice. When labels, resource counts, variable freshness, or types do not meet a tactic’s requirements, the tactic simply fails; it never treats a missing 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 case shows a typical rhythm: initialize the goal, case-split on the pure data, unfold the spatial predicate, supply the witnesses, normalize both sides, and frame away the common resources. Later proofs over richer data structures reuse this same spine.