First Pass

The Separation Logic framework that we have constructed is well-suited for a language with explicit deallocation, but cannot be used as such for a language equipped with a garbage collector. As pointed out in the chapter Basic, there is no rule in our basic Separation Logic that allows discarding a heap predicate from the precondition or the postcondition. 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 from the 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 or may not be freely discared. 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. This 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

Let us 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, with this time 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 considered 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) ==> \[].

This situation is desirable in a programming language with explicit deallocation, because it ensures that the code written by the programmer is not missing any deallocation operation. However, it is ill-suited for a programming language equipped with a garbage collector that deallocates data automatically. This chapter presents an "affine" version of Separation Logic, where the above function succ_using_incr does admit the expected postcondition fun r ⇒ \[r = n+1].

Statement of the Discard Rule

There are several ways to state the "discard rule". Let us begin with two rules: 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. On the contrary, 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 two rules triple_hany_pre and triple_hany_post can be derived from each other. As we will establish further on, the rule 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, however 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 on Collectable Predicates

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, and not arbitrary heap predicates. The idea is to restrict the discard rules so that only predicates satisyfing 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. This predicate heap_affine may be customized depending on the logic one wants to set up. The definition of heap_affine h is left abstract for the moment.

The only assumptions we need to make about heap_affine is that this predicate 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), one 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 only holds of affine heaps.

The predicate haffine distributes in a natural way on each of the operators of Separation Logic: the combination of affine heap predicates yields affine heap predicates. In particular:

• \[] and \[P], which describes 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 any x;
• \∀ x, H can be discarded if H can be discarded for at least one x.

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:

Definition of the "Affine Top" Heap Predicates

We next introduce a new heap predicate, called "affine top" and written \GC, 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 more usable manner. This predicate is written \GC and named hgc in the formalization. The predicate \GC holds of any affine heap. \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, which is easier to manipulate using the xsimpl tactic.

The introduction lemmas 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 reciprocal.

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 \GC Predicate

One fundamental property of \GC that appears necessary 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. Indeed, \GC denotes some heap H such that H is affine; Thus, by essence, it denotes an affine heap predicate.

The process of exploiting the \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 (recall 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 more concise than triple_haffine_post. Moreover, it has the benefits that the piece of heap discarded, previously described by H', no longer needs to be provided upfront at the moment of applying the rule. It may be provided further on in the reasoning, by exploiting himpl_hgc_r to prove an entailment of the form H' ==> \GC.

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.

Refined Definition of Separation Logic Triples

This section explains how to refine the notion of Separation Logic triple so as to accomodate the discard rule. Recall the previous definition of triples, which capture a linear logic.
    Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
      ∀ s, H s → eval s t Q. The 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.

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

• that all the existing reasoning rules of Separation Logic remain sound,
• that the 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 the same proof script as before, only with xsimpl possibly performing extra work for cancelling out occurrences of \GC on both sides of an entailement.

We also need to update reasoning rule for terms. We present one representative example, namely 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 of 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)

Reciprocally, 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

In chapter WPsem, we have 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 remain valid for the definition of wp extended with \GC.

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

Exercise: 1 star, standard, optional (wp_hgc_post)

Prove the discard rule in wp-style.

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:

• either 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 use to anticipate, right from the beginning of the proof of a function, the need of discarding 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 Involving Discarded Heap Predicates

Using the updated version of xwp, let us revisite the proof of our motivating example succ_using_incr in a fully affine logic, i.e., a logical 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 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 the frame rule, 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 sastisfy the wp-style statement of the discard rule, which is stated in a way similar to wp_hgc_post.

Besides, let us prove that the revised definition of mkstruct still satisfies the three 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 Behavior of xsimpl on \GC

The tactic xaffine applys to a goal of the form haffine H. The tactic 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 set up 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.

The Proof 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₂ to infer the predicate H₂, which describes what remains after removing H₁ from H.

The tactic xgc_keep H is a variant of xgc that enables to discard 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 concerns 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 are not allowed to 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].