First Pass

The Separation Logic framework that we have constructed is well suited for a language with explicit deallocation, but cannot be used as-is for a language equipped with a garbage collector. As pointed out in chapter Basic, there is no rule in our basic Separation Logic that allows discarding a heap predicate from the precondition or the postcondition. From a theoretical perspective, discarding predicates from the postcondition is sufficient. From a practical perspective, however, the user may wish to clarify the proof obligations by discarding predicates appearing in the precondition as soon as they are no longer useful. In this chapter, we explain how to generalize the Separation Logic framework to support a "discard rule", which one may invoke to discard heap predicates from the precondition or postcondition. The framework extended with the discard rule corresponds to an "affine" logic, where heap predicates may be freely discarded, as opposed to a "linear" logic, where heap predicates cannot be thrown away. As we argue, it may be interesting for a program logic to accomodate both "affine" predicates and "linear" predicates. We will explain how to fine tune which heap predicates may be freely discarded. For example, even in a programming language featuring a garbage collector, it may be useful to ensure that every file handle opened eventually gets closed, or that every lock acquired is eventually released. File handles and locks are example of resources that may be described in Separation Logic, yet that one should not be allowed to discard freely. Regarding garbage-collected data, another possible approach is to require the programmer to integrate "free" operations defined as no-ops, to materialize the places where memory cells can and should be discarded. This approach, however, is cumbersome for freeing recursive data structures. For example, to free a mutable list, the programmer would need to iterate over the list to free its cells one by one. In contrast, with a "discard rule" in the program logic, the user can discard at once the representation predicate for the full list, without involving any form of iteration. The chapter is organized as follows:

• first, we recall the example illustrating the limitation of a logic without a discard rule for a garbage-collected language;
• second, we present several versions of the "discard rule";
• third, we show how to refine the definition of Separation Logic triples in such a way that the discard rules are satisfied for certain classes of heap predicates.

Motivation for the Discard Rule

Recall the example of the function succ_using_incr_attempt from chapter Basic. This function allocates a reference with contents n, then increments that reference, and finally returning its contents, that is, n+1. Let us revisit this example, this time with the intention of establishing for it a postcondition that does not leak the existence of a left-over reference cell.

In the framework developed so far, the heap predicate describing the reference cell allocated by the function cannot be discarded, because the code does not include a deallocation operation. Thus, we are forced to include in the postcondition the description of a left-over reference with a heap predicate, e.g., \∃ p, p ~~> (n+1), or \∃ p m, p ~~> m.

If we try to prove a specification that does not mention the left-over reference, then we get stuck with a proof obligation of the form p ~~> (n+1) ==> \[].

In what follows, we extend our Separation Logic with a "discard rule" that allows proving the above specification for succ_using_incr.

Statement of The Discard Rule

There are several ways to state the "discard rule". Let us begin with two variants: one that discards a heap predicate H' from the postcondition, and one that discards a heap predicate H' from the precondition. The first rule, named triple_hany_post, asserts that an arbitrary heap predicate H' can be dropped from the postcondition, simplifying it from Q \*+ H' to Q.

Let us show that, using the rule triple_hany_post, we can derive the desired specification for the motivating example from the specification that mentions the left-over postcondition.

A symmetric rule, named triple_hany_pre, asserts that an arbitrary heap predicate H' can be dropped from the precondition, simplifying it from H \* H' to H.

Observe the difference between the two rules. In triple_hany_post, the discarded predicate H' appears in the premise, reflecting the fact that we discard it after the evaluation of the term t. Conversely, in triple_hany_pre, the discarded predicate H' appears in the conclusion, reflecting the fact that we discard it before the evaluation of t. The rules triple_hany_pre and triple_hany_post can be derived from each other. As we will establish further on, triple_hany_pre is derivable from triple_hany_post by a simple application of the frame rule. Reciprocally, triple_hany_post is derivable from triple_hany_pre, though the proof is slightly more involved. This proof appears in lemma triple_hgc_post_from_hgc_pre in the "optional material" section.

Fine-grained Control of Collectable Predicates

Axiomatization of heap_affine and haffine

As suggested in the introduction, it may be useful to constrain the discard rule in such a way that it can be used to discard only certain types of heap predicates, not arbitrary ones. The idea is to restrict the discard rules so that only predicates satisfying a predicate called haffine may be discarded. The two discard rules should thus feature an extra premise: to discard a heap predicate H', the proposition haffine H' must hold.

The predicate haffine H is defined in terms of a lower-level predicate heap_affine. The proposition heap_affine h asserts that the piece of heap h may be freely discarded, in the sense that it does not have to be accounted for in the program logic. The question of whether a heap or a heap predicate should be affine or not is to be decided on a case-by-case basis. It depends on the intention of the designer of the program logic. For the moment, we leave the predicate heap_affine abstract, and allow it to be customized later on.

The only assumptions we need to make about heap_affine is that it holds of the empty heap and that it is preserved by a disjoint union operation.

We will later show two extreme instantiations: one that leads to a logic where all predicates are affine (i.e. can be freely discarded), and one that leads to a logic where all predicates are linear (i.e. none can be freely discarded, like in our previous set up).

Definition and Properties of heap_affine

The predicate haffine H captures the notion of "affine heap predicate". A heap predicate is affine iff it holds only of affine heaps.

The predicate haffine distributes in a natural way over each of the operators of Separation Logic -- i.e., the combination of affine heap predicates yields affine heap predicates. In particular:

• \[] and \[P], which describe empty heaps, can always be discarded;
• H₁ \* H₂ can be discarded if both H₁ and H₂ can be discarded;
• \∀ x, H can be discarded if H can be discarded for at least one x;
• \∃ x, H can be discarded if H can be discarded for every x.

The treatment of universal quantifiers can be explained as follows. Consider a heap h that satisfies \∀ (x:A), H, and consider a particular value v of type A. The heap h also satisfies [x:=v]H. Thus, if the heap predicate [x:=v]H can be discarded, the stronger predicate \∀ (x:A), H can also be discarded. Existential quantifiers can be explained as follows. Consider a heap h that satisfies \∃ (x:A), H. We know that there exists a value v of type A such that h satisfies [x:=v]H. However, we know nothing about this value v. Therefore, to discard \∃ (x:A), H, we need to know that [x:=v]H can be discarded for every possible v.

The rule haffine_hforall' requires the user to provide evidence that there exists at least one value x of type A for which haffine (J x) is true. In practice, the user is generally not interested in proving properties of a specific value x, but is happy to justify that J x is affine for any x. The corresponding statement appears below, with an assumption Inhab A asserting that the type A is inhabited. In practice, the \∀ quantifier is always invoked on inhabited types, so this is a benign restriction.

Another useful fact about haffine is that to prove haffine (\[P] \* H) it is sufficient to prove haffine H under the hypothesis that P is true. Formally:

The Affine-Top Heap Predicate: \GC

Definition of The Affine-Top Predicate

We next introduce a new heap predicate, called "affine top", that is very handy for describing "the possibility to discard a heap predicate". We use this predicate to reformulate the discard rules in a more concise and usable manner. This predicate is written \GC and named hgc in the formalization. The predicate \GC holds of any affine heap. The reason \GC is named "affine top" is because it refines a representation predicate called "top", and written \Top. The predicate \Top is the heap predicate that holds of any heap. It can be defined as fun (h:heap) ⇒ True, or, equivalently, as \∃ (H:hprop), H. The characteristic property of \Top is the entailment ∀ H, (H ==> \Top). The affine top predicate \GC can be defined as ∃ H, \[haffine H] \* H. As we prove further on, it could be equivalently defined as fun h ⇒ heap_affine h. We prefer the former definition as it is easier to manipulate using the xsimpl tactic.

The following introduction lemma asserts that \GC h holds when h satisfies heap_affine.

Exercise: 2 stars, standard, especially useful (triple_frame)

Prove that the affine heap predicate holds of any affine heap.

The elimination lemma asserts the converse.

Exercise: 2 stars, standard, optional (hgc_inv)

Prove the elimination lemma for \GC expressed using heap_affine.

Together, the introduction and the elimination rule justify the fact that hgc could equivalently have been defined as heap_affine.

Properties of the Affine-Top Predicate

One fundamental property of \GC that is useful in the soundness proofs is that the conjunction of two occurences of \GC may be merged into a single \GC.

Another useful property is that the heap predicate \GC itself satisifes haffine.

The process of exploiting \GC to "absorb" affine heap predicates is captured by the following lemma, which asserts that a heap predicate H entails \GC whenever H is affine.

In particular, the empty heap predicate \[] entails \GC, because the empty heap predicate is affine (lemma haffine_hempty).

Exercise: 3 stars, standard, especially useful (himpl_hgc_absorb)

Show that \GC * H entails \GC for any H satisfying haffine.

Using the predicate \GC, we can reformulate the constrained discard rule triple_haffine_post as follows.

This rule is more concise than triple_haffine_post. Moreover, the piece of heap being discarded, previously described by H', no longer needs to be provided up front, at the moment of applying the rule. Instead, it can be provided further on in the reasoning, by exploiting himpl_hgc_r to prove an entailment of the form H' ==> \GC.

Example Instantiations of heap_affine

Instantiation of heap_affine for a Fully Affine Logic

To set up a fully affine logic, we consider a definition of heap_affine that holds of any heap.

It is trivial to check that heap_affine satisfies the required distribution properties on the empty heap and the union of heaps.

With that instantiation, haffine holds of any heap predicate.

Moreover, the affine top predicate \GC is equivalent to the top predicate htop, defined as fun h ⇒ True or equivalently as \∃ H, H.

Instantiation of heap_affine for a Fully Linear Logic

To set up a fully affine logic, we consider a definition of heap_affine that holds only of empty heaps.

Again, it is not hard to check that heap_affine satisfies the required distributivity properties.

With that instantiation, the predicate haffine H is equivalent to H ==> \[], that is, it characterizes heap predicates that hold of the empty heap.

Moreover, the affine top predicate \GC is equivalent to the empty heap predicate hempty.

Definition of a Partially Affine Separation Logic

Refined Definition of Triples

We now explain how to refine the notion of Separation Logic triple so as to accomodate the discard rule. Recall the previous definition of triples, capturing a linear logic.
    Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
      ∀ s, H s → eval s t Q. The new discard rule triple_htop_post asserts that postconditions may be freely extended with the \GC predicate. To support this rule, it suffices to modify the definition of triple to include the predicate \GC in the postcondition of the underlying Hoare triple, as follows.

Next, for the updated definition of triple using \GC, we establish:

• that all the existing reasoning rules of Separation Logic remain sound, and
• that the new discard rules triple_htop_post, triple_haffine_hpost, and triple_haffine_hpre are provable.

Soundness of the Existing Rules

Let us update the soundness proof of the rules of Separation Logic to account for the addition of \GC in the definition of triples. All the rules are proved using exactly the same proof scripts as before, with xsimpl possibly performing extra work for cancelling out occurrences of \GC on both sides of an entailment.

We also need to update the reasoning rules for terms. We present one representative example: the proof rule for sequences.

The proof is structured like in lemma triple_seq from chapter Rules.

The main difference is the need to to invoke the lemma hstar_hgc_hgc for merging the left-over that originates from t₁ with the \GC that originates from t₂ into a single \GC.

Soundness of the Discard Rules

Let us first establish the soundness of the discard rule triple_htop_post.

Exercise: 3 stars, standard, especially useful (triple_hgc_post)

Prove triple_hgc_post with respect to the refined definition of triple that includes \GC in the postcondition. Hint: exploit hstar_hgc_hgc, with help from the tactics xchange and xsimpl.

Exercise: 1 star, standard, especially useful (triple_haffine_post)

Prove that triple_haffine_post is derivable from triple_hgc_post. Hint: use the property himpl_hgc_r, which asserts H' ==> \GC.

Exercise: 1 star, standard, optional (triple_hgc_post_from_triple_haffine_post)

Conversely, prove that triple_hgc_post is derivable from triple_haffine_post.

Exercise: 1 star, standard, optional (triple_haffine_pre)

Prove that triple_haffine_pre is derivable from triple_hgc_post. Hint: exploit the frame rule, and leverage triple_hgc_post either directly or by invoking its corollary triple_haffine_post.

Combined Structural Rules

Exercise: 2 stars, standard, optional (triple_conseq_frame_hgc)

Prove the combined structural rule triple_conseq_frame_hgc, which extends triple_conseq_frame with the discard rule, replacing Q₁ \*+ H₂ ===> Q with Q₁ \*+ H₂ ===> Q \*+ \GC.

Exercise: 1 star, standard, optional (triple_ramified_frame_hgc)

Prove the following generalization of the ramified frame rule that includes the discard rule. Hint: take inspiration from the proof of triple_ramified_frame presented in the chapter Wand.

More Details

Discard Rules in WP Style

Definition of WP for a Partially Affine Separation Logic

In chapter WPsem, we defined wp t Q s as eval s t Q. To account for affine heaps, we refine the definition to eval s t (Q \*+ \GC).

The characteristic equivalence of wp remains valid, with respect to the definition of wp extended with \GC and the definition of triple extended with \GC.

The structural reasoning rules also remain valid.

In weakest precondition style, the discard rule triple_hgc_post translates into the entailment wp t (Q \*+ \GC) ==> wp t Q.

Exercise: 1 star, standard, optional (wp_hgc_post)

The wp-style presentation of the rule triple_hgc_pre is captured by the lemma wp_haffine_pre shown below.

Exercise: 3 stars, standard, optional (wp_haffine_pre)

Prove wp_haffine_pre. Hint: one possibility is to use eval_conseq and wp_frame, as well as himpl_hgc_r and hstar_hgc_hgc. Another possibility is to refine the proof of wp_frame.

The revised presentation of the wp-style ramified frame rule includes an extra \GC predicate. This rule captures at once all the structural properties of Separation Logic, including the discard rule.

Exercise: 3 stars, standard, optional (wp_haffine_pre)

Prove wp_ramified with support for \GC.

Exploiting the Discard Rule in Proofs

In a practical verification proof, there are two useful ways to discard heap predicates that are no longer needed:

• by invoking triple_haffine_pre to remove a specific predicate from the current state, i.e., the precondition; or
• by invoking triple_htop_post to add a \GC into the current postcondition and allow subsequent removal of any predicate that may be left-over in the final entailment justifying that the final state satisfies the postcondition.

Eager removal of predicates from the current state is never necessary: one can always be lazy and postpone the application of the discard rule until the last step of reasoning. It is cumbersome for the user to anticipate, right from the beginning of the proof of a function, the need to discard heap predicates at the last line of the function body. To ease the work of the user, it suffices to systematically apply the rule triple_htop_post as very first step of the proof of every function. The effect is to extend the postcondition of the function with a \GC predicate. This predicate may be used to absorb any garbage left-over at the end of the proof of the function body. If there is no such garbage, the tactic xsimpl automatically discards the \GC predicate. We implement this strategy by integrating the rule triple_htop_post into the tactic xwp, which sets up the verification proof by computing the characteristic formula. To that end, we generalize the lemma xwp_lemma, which the tactic xwp applies. Its original statement is as follows.

Its generalized form extends the postcondition from Q to Q \*+ \GC, as shown below.

We update the tactic xwp to exploit the lemma xwp_lemma' instead of xwp_lemma.

Example Proof in an Affine Separation Logic

Using the updated version of xwp, let us revisite the proof of our motivating example succ_using_incr in a fully affine logic where any predicate can be discarded.

Assume a fully affine logic.

Observe, in the proof below, the \GC introduced in the postcondition by the call to xwp.

We will show further on how to automate the work from the last line of the proof above, by setting up xsimpl to automatically resolve goals of the form H ==> \GC.

Revised Definition of mkstruct

Recall the definition mkstruct, which is key to implementing wpgen and the x-tactics.
    Definition mkstruct (F:formula) : formula :=
      fun Q ⇒ \∃ Q', (F Q') \* (Q' \−−∗ Q). This definition can be generalized to handle not just the consequence and frame rules, but also the discard rule. To that end, mkstruct is extended with an additional \GC, as follows.

Let us prove that this revised definition of mkstruct does indeed satisfy the wp-style statement of the discard rule, which is stated in a way similar to wp_hgc_post.

Further, let us prove that the revised definition of mkstruct still satisfies the four originally required properties: erasure, consequence, frame, and monoticity.

Exercise: 2 stars, standard, optional (mkstruct_haffine_post)

Prove the reformulation of triple_haffine_post adapted to mkstruct, for discarding an affine piece of postcondition.

Exercise: 2 stars, standard, optional (mkstruct_haffine_pre)

Prove the reformulation of triple_haffine_pre adapted to mkstruct, for discarding an affine piece of postcondition.

The Tactic xaffine and the Behavior of xsimpl on \GC

The tactic xaffine applies to a goal of the form haffine H. It simplifies the goal using all the distributivity rules associated with haffine. Ultimately, it invokes eauto with haffine, which can leverage knowledge specific to the definition of haffine from the Separation Logic setup at hand.

The tactic xsimpl is extended with support for simplifying goals of the form H ==> \GC into haffine H, using lemma himpl_hgc_r. For example, xsimpl can simplify the goal H₁ \* H₂ ==> H₂ \* \GC into just haffine H₁.

In addition, xsimpl invokes the tactic xaffine to simplify side-conditions of the form haffine H. For example, xsimpl can prove the following lemma.

Tactics for Applying the Discard Rules

This section presents the discard tactics xgc, xc_keep, and xgc_post. Their implementation leverages the discard property of mkstruct, reproduced below.

The tactic xgc H₁ removes H₁ from the precondition (i.e., from the current state), in the course of a proof exploiting a formula produced by wpgen. More precisely, the tactic xgc H₁ removes H₁ from the current precondition H. It leverages xsimpl to simplify the entailment H ==> H₁ \* H₂ and infer H₂, which describes what remains after removing H₁ from H.

The tactic xgc_keep H is a variant of xgc that enables discarding everything but H from the precondition. The implementation of the tactic leverages the same lemma xgc_lemma, but providing H₂ instead of H₁.

The tactic xgc_post simply extends the postcondition with a \GC, to enable subsequent discarding of heap predicates in the final entailment.

The example below illustrates a usage of the xgc_post tactic.

Optional Material

Alternative Statement for Distribution of haffine on Quantifiers

Recall the lemmas haffine_hexists and haffine_hforall.
    Lemma haffine_hexists : ∀ A (J:A→hprop),
      (∀ x, haffine (J x)) →
      haffine (\∃ x, (J x)).
    Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),
      (∀ x, haffine (J x)) →
      haffine (\∀ x, (J x)). They can be reformulated in a more concise way, as explained next. First, to smoothly handle the distribution on the quantifiers, let us extend the notion of "affinity" to postconditions. The predicate haffine_post J asserts that haffine holds of J x for any x.

The rules then reformulate as follows.

Deriving the Rule GC-Post from the Rule GC-Pre

Earlier on, we proved that triple_hgc_pre is derivable from triple_hgc_post, through a simple application of the frame rule. We wrote that, reciprocally, the rule triple_hgc_post is derivable from triple_hgc_pre, yet with a slightly more involved proof. Let us present this proof. Concretely, assume triple_hgc_pre and let us prove the result triple_hgc_post.

The key idea of the proof is that a term t admits the same behavior as let x = t in x. Recall from chapter Rules the lemma eta_same_triples which asserts the equivalence of t and let x = t in x.

To discard a predicate from the postcondition of t if we only have at hand a rule for discarding predicates from preconditions, we replace t with let x = t in x and apply the discard rule after evaluating t but before returning the variable x.

Historical Notes

The seminal presentation of Separation Logic concerned a linear logic for a programming language with explicit deallocation. More recent works on Separation Logic for ML-style languages equipped with a garbage collector consider affine logics. For example, the original presentation of the Iris framework provides an affine entailment, for which H ==> \[] is always true. Follow-up work on Iris provides encodings for supporting linear resources, i.e., resources that cannot be dropped on the floor. The present chapter gives a presentation of Separation Logic featuring a customizable predicate haffine for controlling which resources should be treated as affine, and which ones should be treated as linear. This direct approach to controlling linearity was introduced in the context of CFML, in work by [Guéneau, Jourdan, Charguéraud, and Pottier 2019].