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 we 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. 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.

Although in the present course we consider a language for which it is desirable that any heap predicate can be discarded, we will present general definitions allowing to fine-tune which heap predicates can be discarded and which cannot be discarded by the user. We argue further on why such a fine-tuning may be interesting.

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. In this chapter, we present an "affine" version of Separation Logic, where the above function succ_using_incr does admits the simple postcondition fun r ⇒ \[r = n+1], i.e., that needs not mention the left-over reference in the postcondition.

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 more involved (it appears in the bonus 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. 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. As another example, consider the extension of Separation Logic with "time credits", which are used for complexity analysis. In such a setting, it is desirable to be able to throw away a positive number of credits to reflect for over-approximations in the analysis. However, the logic must forbid discarding predicates that capture a negative number of credits, otherwise soundness would be compromised. The idea is to restrict the discard rules so that only predicates satisyfing a predicate called haffine may get discarded. The two discard rules will thus feature an extra premise requiring haffine H', where H' denotes the heap predicate being discarded.

To constraint the discard rule and allow fine-tuning of which heap predicates may be thrown away, we introduce the notions of "affine heap" and of "affine heap predicates", captured by the judgments heap_affine h and haffine H, respectively. The definition of heap_affine h is left abstract for the moment. We will 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 of heap_affine and of haffine

Concretely, the notion of "affine heap" is characterize by the abstract predicate named heap_affine, which is a predicate over heaps.

This predicate heap_affine is assumed to satisfy two properties: it holds of the empty heap, and it is stable by (disjoint) union of heaps.

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 and \∀ x, H can be discarded if H can be discarded for any 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.

In addition, haffine (\[P] \* H) should simplify to haffine H under the hypothesis P. Indeed, if a heap h satisfies \[P] \* H, then it must be the case that the proposition 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. It holds of any affine heap. \GC can be equivalently defined as heap_affine, or as ∃ H, \[haffine H] \* H. The latter formulation is expressed in terms of existing Separation Logic operators, hence it is easier to manipulate in proofs 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 that appears necessary in many of the soundness proofs is the following lemma, which asserts that two occurences of \GC can be collapsed into just one.

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).

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

Not only is this rule more concise than triple_haffine_post, it also 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, for example in an entailment, by instantiating the existential quantifier carried into the definition of \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.

With that instantiation, 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.

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

With that instantiation, the affine top predicate \GC is equivalent to the empty heap predicate hempty.

Refined Definition of Separation Logic Triples

Thereafter, we purposely leave the definition of haffine abstract, for the sake of generality. In what follows, we explain how to refine the notion of Separation Logic triple so as to accomodate the discard rule. Recall the definition of triple for a linear logic.
    Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
      ∀ (H':hprop), hoare t (H \* H') (Q \*+ H'). 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.

Observe that this definition of triple is strictly more general than the previous one. Indeed, as explained earlier on, when considering the fully linear instantiation of haffine, the predicate \GC is equivalent to the empty predicate \[]. In this case, the occurence of \GC that appears in the definition of triple can be replaced with \[], yielding a definition equivalent to our original definition of triple. For the updated definition of triple using \GC, one can prove that:

• all the existing reasoning rules of Separation Logic remain sound;
• the discard rules triple_htop_post, triple_haffine_hpost and triple_haffine_hpre can be proved sound.

Soundness of the Existing Rules

Let us update the soundness proof for the other structural rules.

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

Prove the frame rule for the definition of triple that includes \GC. Hint: unfold the definition of triple but not that of hoare, then exploit lemma hoare_conseq and conclude using the tactic xsimpl.

Exercise: 3 stars, standard, optional (triple_conseq)

Prove the frame rule for the definition of triple that includes \GC. Hint: follow the same approach as in the proof of triple_frame, and leverage the tactic xchange to conclude.

The extraction rules remain valid as well.

The standard reasoning rules of Separation Logic can be derived for the revised notion of Separation Logic triple, the one which includes \GC, following essentially the same proofs as for the original Separation Logic triples. The main difference is that one sometimes needs to invoke the lemma hstar_hgc_hgc for collapsing two \GC into a single one. In what follows, we present just one representative example of such proofs, namely the reasoning rule for sequences. This proof is similar to that of lemma triple_seq from chapter Rules.

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_h_post with respect to the refined definition of triple that includes \GC in the postcondition. Hint: exploit hoare_conseq, then 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: unfold the definition of \GC using unfold hgc.

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.

Exercise: 1 star, 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. Hint: invoke triple_conseq, triple_frame and triple_hgc_post in the appropriate order.

Exercise: 1 star, standard, optional (triple_ramified_frame_hgc)

Prove the following generalization of the ramified frame rule that includes the discard rule. Hint: it is a corollary of triple_conseq_frame_hgc. Take inspiration from the proof of triple_ramified_frame in chapter Wand.

Discard Rules in WP Style

Let us update the definition of wp to use the new definition of triple.

Recall the characteristic equivalence of wp.

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. Hint: exploit wp_equiv and triple_hgc_post.

Likewise, the wp-style presentation of the rule triple_hgc_pre takes the following form.

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.

For a change, let us present below a direct proof for this lemma, that is, not reusing the structural rules associated with triples.

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. In practical, it usually suffices to anticipate, right from the beginning of the verification proof, the possibility of discarding heap predicates from the final state. To that end, we apply the rule triple_htop_post as very first step of the proof to extend the postcondition with a \GC predicate, which will be used to absorb all the garbage left-over at the end of the proof. We implement this strategy in a systematic manner by integrating directly 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 to which the formula computed by wpgen is applied from Q to Q \*+ \GC, as shown below.

Let us 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.

More Details

Revised Definition of mkstruct

Recall the definition mkstruct, as stated in the file Wand.
    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, we augment mkstruct 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, and frame. Remark: the proofs shown below exploit a version of xsimpl that handles the magic wand but provides no built-in support for the \GC predicate.

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. Hint: haffine is an opaque definition at this stage; the assumption haffine needs to be exploited using the lemma himpl_hgc_r.

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

To present the discard tactics xgc, xc_keep and xgc_post, we import the definitions from LibSepDirect but assume that the definition of mkstruct is like the one presented in the present file, that is, including the \GC when defining mkstruct F as fun Q ⇒ \∃ Q', F Q' \* (Q' \−−∗ (Q \*+ \GC)). As argued earlier on, with this definition, mkstruct satisfies the following discard rule.

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 invokes the following variant of the rule triple_haffine_pre, which allows to leverage xsimpl for computing the heap predicate H₂ that remains after a predicate H₁ is removed from a precondition H, through the entailment H ==> H₁ \* 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, only 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.

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.

Pre and Post Rules

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. In other word, 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. Thus, to simulate discarding a predicate from the postcondition of t, one can invoke the discard rule on the precondition of the variable x that appears at the end of let x = t in x. To formalize this idea, recall from Rules the lemma eval_like_eta_expansion which asserts the equivalence of t and let x = t in x, and recall the lemma triple_eval_like, which asserts that two equivalent terms satisfy the same triples.

Low-level Definition of Refined Triples

Consider the updated definition of triple introduced in this chapter.

In chapter Hprop, we presented an alternative definition for Separation Logic triples, called triple_lowlevel, expressed directly in terms of heaps.
    Definition triple_lowlevel (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
      ∀ h₁ h₂,
      Fmap.disjoint h₁ h₂ →
      H h₁ →
      ∃ h₁' v,
           Fmap.disjoint h₁' h₂
        ∧ eval (h₁ \u h₂) t (h₁' \u h₂) v
        ∧ Q v h₁'. In what follows, we explain how to generalize this definition to match our revised definition of triple, and thereby obtain a direct definition expressed in terms of heap, that does not depend on the definition of hstar nor that of \GC. Let us aim instead for a direct definition, entirely expressed in terms of union of heaps. To that end, we need to introduce an additional piece of state to describe the piece of the final heap covered by the \GC predicate. We will need to describe the disjointness of the 3 pieces of heap that describe the final state. To that end, we exploit the auxiliary definition Fmap.disjoint_3 h₁ h₂ h₃, which asserts that the three arguments denote pairwise disjoint heaps. It is defined in the module Fmap as follows.
    Definition disjoint_3 (h₁ h₂ h₃:heap) : Prop :=
         disjoint h₁ h₂
      ∧ disjoint h₂ h₃
      ∧ disjoint h₁ h₃. We then formulate triple_lowlevel using a final state of the from h₁' \u h₂ \u h₃' instead of just h₁' \u h₂. There, h₃' denotes the piece of the final state covered by the \GC heap predicate. This piece of state is an affine heap, as captured by heap_affine h₃'.

One can prove the equivalence of triple and triple_lowlevel following a similar proof pattern as previously.

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". This 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]