First Pass

This chapter presents some additional Separation Logic operators:

• the disjunction, written hor H₁ H₂,
• the non-separating conjunction, written hand H₁ H₂,
• the "forall", named hforall and written \∀ x, H,
• the "magic wand", named hwand and written H₁ \−∗ H₂,
• the "magic wand for postconditions", named qwand and written Q₁ \−−∗ Q₂.

The magic wand operator has multiple uses:

• it is key to formulating the "ramified frame rule", a more practical rule for exploiting the frame and consequence properties,
• it will be used in the chapter WPgen to define a weakest-precondition generator, and
• it can be useful to state the specifications for certain data structures.

This chapter is organized as follows:

• definition and properties of hand, hor, and hforall,
• definition and properties of the magic wand operator,
• generalization of the magic wand to postconditions,
• extension of the xsimpl tactic to handle the magic wand,
• statement and benefits of the ramified frame rule.

The "optional material" presents several equivalent definitions for magic wand.

Definition of the Operator hforall

The heap predicate \∀ x, H holds of a heap h that, for any possible value of x, satisfies H. It may be puzzling at first what could possibly be the use case for such a universal quantification, but we will see several examples through this chapter -- in particular the encoding of the non-separating conjunction (hand) and of the magic wand on postconditions (qwand). The predicate \∀ x, H stands for hforall (fun x ⇒ H), where the definition of hforall follows the same pattern as hexists.

To follow the rest of this chapter, it suffices to have in mind the introduction and elimination rules for hforall.

The introduction rule in an entailment for \∀ appears below. To prove that a heap satisfies \∀ x, J x, we must show that, for any x, this heap satisfies J x.

The elimination rule in an entailment for \∀ appears below. Assuming a heap satisfies \∀ x, J x, we can derive that the same heap satisfies J v for any desired value v.

The lemma hforall_specialize can equivalently be formulated in the following way, which makes it easier to apply in some cases.

Universal quantifers that appear in the precondition of a triple may be specialized like universal quantifiers appearing on the left-hand side of an entailment.

Definition of the Operator hor

The heap predicate hor H₁ H₂ describes a heap that satisfies H₁ or satifies H₂ (or possibly both). In other words, the heap predicate hor H₁ H₂ lifts the disjunction operator P₁ ∨ P₂ from Prop to hprop. The disjunction operator does not appear to be critically useful in practice, because it can be encoded using Coq's conditional construct, or using pattern matching. Nevertheless, there are situations where it proves handy. The heap disjunction predicate admits a direct definition as a function over heaps, written hor'.

An alternative definition leverages the \∃ quantifier. The definition, shown below, reads as follows: "there exists an unspecified boolean value b such that if b is true then H₁ holds, else if b is false then H₂ holds". The benefit of this definition is that its properties can be established without manipulating heaps explicitly.

Exercise: 3 stars, standard, optional (hor_eq_hor')

Prove the equivalence of the definitions hor and hor'.

The two introduction rules for hor assert that if H₁ holds, then hor H₁ H₂ holds; and, symmetrically, if H₂ holds, then hor H₁ H₂ holds.

In practice, these rules are easier to exploit when combined with a transitivity step.

The elimination rule asserts that, if hor H₁ H₂ holds, then we can perform a case analysis on whether it is H₁ or H₂ that holds. Concretely, to show that hor H₁ H₂ entails a heap predicate H₃, we must show both that H₁ entails H₃ and that H₂ entails H₃.

The operator hor is commutative. To establish this property, it is useful to exploit the following lemma, called if_neg, for swapping the two branches of a conditional by negating its boolean condition.

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

Prove that hor is a symmetric operator. Hint: exploit hprop_op_comm and if_neg (from chapter Himpl).

Exercise: 4 stars, standard, especially useful (hor_comm)

Prove that the representation predicate MList introduced in chapter Repr can be equivalently characterized using the predicate hor, as shown below. Hint: to prove this equivalence, do not attempt a proof by induction, and do not attempt to unfold MList. Instead, work using the equalities MList_nil and MList_cons. You may want to begin the proof by applying himpl_antisym and calling destruct on L.

Definition of the Operator hand

The heap predicate hand H₁ H₂ describes a single heap that satisfies H₁ and at the same time satifies H₂. In other words, the heap predicate hand H₁ H₂ lifts the disjunction operator P₁ ∧ P₂ from Prop to hprop. The heap predicate hand admits a direct definition as a function over heaps.

An alternative definition leverages the \∀ quantifier. The definition reads as follows: "for any boolean value b, if b is true then H₁ should hold, and if b is false then H₂ should hold".

Exercise: 2 stars, standard, especially useful (hand_eq_hand')

Prove the equivalence of the definitions hand and hand'. Use functional extensionality to get started.

The introduction and elimination rules for hand are as follows.

• If "H₁ and H₂" holds, then in particular H₁ holds.
• Symmetrically, if "H₁ and H₂" holds, then in particular H₂ holds.
• Reciprocally, to prove that a heap predicate H₃ entails "H₁ and H₂", we must prove that H₃ entails H₁, and that H₃ satisfies H₂.

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

Prove that hand is symmetric. Hint: use hprop_op_comm and rewrite if_neg, or a case analysis on the boolean value coming from hand.

Definition of the Magic Wand Operator: hwand

Definition of hwand

The magic wand operation H₁ \−∗ H₂, pronounced "H₁ wand H₂", defines a heap predicate such that, if we extend it with H₁, we obtain H₂. Formally, the following entailment holds:
      H₁ \* (H₁ \−∗ H₂) ==> H₂. Intuitively, if we think of the star H₁ \* H₂ as a sort of addition, H₁ + H₂, then we can think of H₁ \−∗ H₂ as the subtraction -H₁ + H₂. The entailment above intuitively captures the idea that (-H₁ + H₂) + H₁ simplifies to H₂. Note, however, that the operation H₁ \−∗ H₂ only makes sense if H₁ describes a piece of heap that "can" be subtracted from H₂. Otherwise, the predicate H₁ \−∗ H₂ characterizes a heap that cannot possibly exist. Informally speaking, H₁ must somehow be a subset of H₂ for the subtraction -H₁ + H₂ to make sense. Another possible analogy is that of logical operators. If P₁ and P₂ were propositions (of type Prop), then P₁ \* P₂ would mean P₁ ∧ P₂ and P₁ \−∗ P₂ would mean P₁ → P₂. The entailment P₁ \* (P₁ \−∗ P₂) ==> P₂ then corresponds to the tautology (P₁ ∧ (P₁ → P₂)) → P₂. Technically, H₁ \−∗ H₂ holds of a heap h if, for any heap h' disjoint from h and satisfying H₁, the union of h and h' satisfies H₂. The operator hwand, which implements the notation H₁ \−∗ H₂, may thus be defined as follows.

The definition above is perfectly fine, however it is more practical to use an alternative, equivalent definition of hwand, expressed in terms of previously introduced Separation Logic operators. Doing so enables us to establish all the properties of the magic wand by exploiting the tactic xsimpl, thereby conducting all the reasoning at the level of hprop, rather than having to work with concrete heaps. The alternative definition asserts that H₁ \−∗ H₂ corresponds to some heap predicate, called H₀, such that H₀ starred with H₁ yields H₂. In other words, H₀ is such that (H₁ \* H₀) ==> H₂. In the definition below, observe how H₀ is existentially quantified.

Characteristic Equivalence for hwand

The magic wand is not easy to make sense of at first. Reading its introduction and elimination rules may help further appreciate its meaning. The operator H₁ \−∗ H₂ satisfies the following equivalence. Informally speaking, think of H₀ = -H₁+H₂ and H₁+H₀ = H₂ being equivalent claims.

Indeed, we will see below that the magic wand operator is uniquely defined by the equivalence (H₀ ==> H₁ \−∗ H₂) ↔ (H₁ \* H₀ ==> H₂). In other words, any operator that satisfies the above equivalence is provably equal to hwand. The right-to-left direction of the equivalence is an introduction rule: it tells what needs to be proved for constructing a magic wand H₁ \−∗ H₂ from a state H₀. To establish that H₀ entails H₁ \−∗ H₂, we have to show that the conjunction of H₀ and H₁ yields H₂.

The left-to-right direction of the equivalence is an elimination rule: it tells what can be deduced from an entailment H₀ ==> (H₁ \−∗ H₂) -- namely, if H₀ is starred with H₁, then H₂ can be recovered.

This elimination rule can be equivalently reformulated in the following handy form: H₁ \−∗ H₂, when starred with H₁, yields H₂.

Further Properties of hwand

We next present the most important properties of the magic wand operator. Here, the tactic xsimpl is available only in a restricted form that does not support magic wand. (The full xsimpl tactic would trivially solve many of these lemmas, but using it here would be cheating because the implementation of xsimpl itself relies on several of these lemmas.) The operator H₁ \−∗ H₂ is contravariant in H₁ and covariant in H₂, like the implication operator →.

The predicates H₁ \−∗ H₂ and H₂ \−∗ H₃ together simplify to H₁ \−∗ H₃. This is reminiscent of the arithmetic identity (-H₁ + H₂) + (-H₂ + H₃) = (-H₁ + H₃) (and to the transitivity of ordinary implication).

The predicate H \−∗ H holds of the empty heap. Intuitively, we can rewrite 0 as -H + H.

Let's now study the interaction of hwand with hempty and hpure. The heap predicate \[] \−∗ H is equivalent to H. Intuitively, we can rewrite -0+H as +H.

The lemma above shows that \[] can be removed from the LHS of a magic wand. More generally, a pure predicate \[P] can be removed from the LHS of a magic wand as long as P is true. Formally:

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

Reciprocally, to prove that a heap satisfies \[P] \−∗ H₂, it suffices to prove that this heap satisfies H₂ under the assumption that P is true. Formally:

Exercise: 2 stars, standard, optional (himpl_hwand_hpure_lr)

Prove that \[P₁ → P₂] entails \[P₁] \−∗ \[P₂]. Hint: use xpull, then use xsimpl by providing an explicit argument to indicate how the \∃ on the right-hand side of the entailment should be instantiated.

Another interesting property is that arguments on the LHS of a magic wand can equivalently be "curried" or "uncurried", just as a function of type (A * B) → C is equivalent to a function of type A → B → C. The heap predicates (H₁ \* H₂) \−∗ H₃, H₁ \−∗ (H₂ \−∗ H₃), and H₂ \−∗ (H₁ \−∗ H₃) are all equivalent. Intuitively, they all describe H₃ with the missing pieces H₁ and H₂. The equivalence between the uncurried form (H₁ \* H₂) \−∗ H₃ and the curried form H₁ \−∗ (H₂ \−∗ H₃) is formalized by the lemma shown below. The third form, H₂ \−∗ (H₁ \−∗ H₃), follows from the commutativity property H₁ \* H₂ = H₂ \* H₁.

Yet another interesting property is that the RHS of a magic wand can absorb resources that the magic wand is starred with. Concretely, from (H₁ \−∗ H₂) \* H₃, we can get the predicate H₃ to be absorbed by the H₂ in the magic wand, yielding H₁ \−∗ (H₂ \* H₃). One way to read this: "if you own H₃ and, when given H₁, you own H₂, then, when given H₁, you own both H₂ and H₃."

The reciprocal entailment is false: H₁ \−∗ (H₂ \* H₃) does not entail (H₁ \−∗ H₂) \* H₃. To see why, instantiate H₁ with \[False]. The predicate \[False] \−∗ (H₂ \* H₃) is equivalent to True, hence imposes no restriction on the heap. But, to establish (\[False] \−∗ H₂) \* H₃, we would need to exhibit a piece of heap satisfiying H₃.

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

Prove that H₁ entails H₂ \−∗ (H₂ \* H₁).

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

Prove that H₁ \* ((H₁ \* H₂) \−∗ H₃) simplifies to H₂ \−∗ H₃.

Exercise: 3 stars, standard, optional (hwand_frame)

Prove that H₁ \−∗ H₂ entails to (H₁ \* H₃) \−∗ (H₂ \* H₃). Hint: use xsimpl.

Exercise: 3 stars, standard, optional (hwand_inv)

Prove the following inversion lemma for hwand. This lemma essentially captures the fact that hwand entails the alternative definition named hwand'.

Definition of the Magic Wand Operator for Postconditions: qwand

In what follows, we generalize the magic wand to operate on postconditions, introducing a heap predicate of the form Q₁ \−−∗ Q₂, of type hprop. Note that the magic wand between two postconditions produces a heap predicate, not a postcondition. There are two ways to define the operator qwand. The first is to follow the same pattern as for hwand, that is, to quantify some heap predicate H₀ such that H₀ starred with Q₁ yields Q₂.

The second possibility is to define qwand directly on top of hwand, by means of the hforall quantifier.

As we establish later in this chapter, qwand and qwand' both define the same operator. We prefer taking qwand as the definition because in practice instantiating the universal quantifier is the most useful way to exploit a magic wand between postconditions. This specialization operation is formalized next. This result is a direct consequence of the specialization result for \∀.

The predicate qwand satisfies numerous properties that are direct counterparts of the properties on hwand. First, qwand satisfies a characteristic equivalence rule.

Second, qwand satisfies a cancellation rule.

Third, the operation Q₁ \−−∗ Q₂ is contravariant in Q₁ and covariant in Q₂.

Fourth the operation Q₁ \−−∗ Q₂ can absorb in its RHS resources to which it is starred.

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

Prove that H entails Q \−−∗ (Q \*+ H).

Exercise: 2 stars, standard, optional (qwand_cancel_part)

Prove that H \* ((Q₁ \*+ H) \−−∗ Q₂) simplifies to Q₁ \−−∗ Q₂. Hint: use xchange.

Simplifications of Magic Wands using xsimpl

We can extend the tactic xsimpl to recognize the magic wand and automatically perform a number of obvious simplifications. This extension is implemented in the file LibSepSimpl, which exports the version of xsimpl illustrated here.

xsimpl is able to spot a magic wand that cancels out. For example, if an iterated separating conjunction includes both H₂ \−∗ H₃ and H₂, then these two heap predicates can be simplified into H₃.

xsimpl is able to simplify uncurried magic wands. For example, if an iterated separating conjunction includes (H₁ \* H₂ \* H₃) \−∗ H₄ and H₂, the two predicates can be simplified into (H₁ \* H₃) \−∗ H₄.

xsimpl automatically applies the introduction rule himpl_hwand_r when the right-hand-side, after prior simplification, reduces to just a magic wand. In the example below, H₁ is first cancelled out from both sides, then H₃ is moved from the RHS to the LHS.

xsimpl can iterate a number of simplifications involving different magic wands.

xsimpl can iterate simplifications on both sides.

xsimpl is also able to deal with the magic wand for postconditions. In particular, it is able to simplify the conjunction of Q₁ \−−∗ Q₂ and Q₁ v into Q₂ v.

xsimpl is able to prove entailments whose right-hand side is a magic wand.

Summary of All the Separation Logic Operators

The core operators are defined as functions over heaps.

The remaining operators can be defined in terms of the core operators.

Of course, these derived operators could also be defined directly as predicate over heaps. The definitions are shown below. However, establishing properties of such low-level definitions requires more effort than establishing properties for the derived definitions shown above. Indeed, when operators are defined as derived operations, their properties may be established with help of the powerful entailment simplification tactic xsimpl.

The Ramified Frame Rule

Recall the consequence-frame rule, which is used pervasively -- for example by the tactic xapp, for reasoning about applications.

This rule suffers from a practical issue, which we illustrate in detail on a concrete example further on. At a high-level, though, the problem stems from the fact that we need to instantiate H₂ when applying the rule. Providing H₂ by hand is not practical, thus we need to infer it. The value of H₂ can be computed as the subtraction of H minus H₁. The resulting value may then exploited in the last premise for constructing Q₁ \*+ H₂. This transfer of information via H₂ from one subgoal to another can be obtained by introducing an "evar" (Coq unification variable) for H₂. However this approach does not work well in cases where H contains existential quantifiers. This is because such existential quantifiers are typically first extracted out of the entailment H ==> H₁ \* H₂ by the tactic xsimpl. But these existentially quantified variables are not in the scope of H₂, so the instantiation of the evar associated with H₂ typically fails. The "ramified frame rule" exploits the magic wand operator to circumvent this problem, by merging the two premises H ==> H₁ \* H₂ and Q₁ \*+ H₂ ===> Q into a single premise that no longer mentions H₂. This replacement premise is H ==> H₁ \* (Q₁ \−−∗ Q). To understand where it comes from, observe first that the second premise Q₁ \*+ H₂ ===> Q is equivalent to H₂ ==> (Q₁ \−−∗ Q). By replacing H₂ with Q₁ \−−∗ Q inside the first premise H ==> H₁ \* H₂, we obtain the new premise H ==> H₁ \* (Q₁ \−−∗ Q). This merge of the two entailments leads us to the statement of the "ramified frame rule" shown below.

Reciprocally, we can prove that the ramified frame rule entails the consequence-frame rule. Hence, the ramified frame rule has the same expressive power as the consequence-frame rule.

More Details

Benefits of the Ramified Frame Rule

Earlier on, we sketched an argument claiming that the consequence-frame rule is not very well suited for carrying out proofs in practice, due to issues with working with evars for instantiating the heap predicate H₂ in the rule. Let us come back to this point and describe the issue in depth on a concrete example, then show how the ramified frame rule smoothly handles that example. Recall, once again, the consequence-frame rule.

One practical caveat with this rule is that we must resolve H₂, which corresponds to the difference between H and H₁. In practice, providing H₂ explicitly is extremely tedious. The alternative is to leave H₂ as an evar, and count on the fact that the tactic xsimpl, when applied to H ==> H₁ \* H₂, will correctly instantiate H₂. This approach works in simple cases, but fails in particular in the case where H contains an existential quantifier. For a concrete example, recall the specification of the primitive ref, which allocates a reference.

Assume that wish to derive the following triple, which extends both the precondition and the postcondition of triple_ref with the heap predicate \∃ l' v', l' ~~> v'. This predicate describes the existence of some other, totally unspecified, reference cell. It is a bit artificial but illustrates the issue.

Let's try to prove that this specification is derivable from the original triple_ref.

Now, let us apply the ramified frame rule to carry out the same proof, and observe how the problem does not show up.

Some Tempting, But False, Properties of the Magic Wand

The entailment \[] ==> (H \−∗ H) holds for any H. But the symmetrical entailement (H \−∗ H) ==> \[] is false. For a counterexample, instantiate H as \[False]. Any heap satisfies \[False] \−∗ \[False]. But only the empty heap satisfies \[].

As another tempting yet false property of the magic wand, consider the converse of the cancellation lemma, that is, H₂ ==> H₁ \* (H₁ \−∗ H₂). It does not hold in general. As a counter-example, consider H₂ = \[] and H₁ = \[False]. The empty heap satisfies the left-hand side of the entailment, but it does does not satisfy \[False] \* (\[False] \−∗ \[]), because there is no way to establish False out of thin air.

More generally, we should be suspicious of any entailment that introduces wands "out of nowhere". The entailment hwand_trans_elim: (H₁ \−∗ H₂) \* (H₂ \−∗ H₃) ==> (H₁ \−∗ H₃) is correct because, intuitively, the left-hand-side captures that H₁ ≤ H₂ and that H₂ ≤ H₃ for some vaguely defined notion of ≤ as "being a subset of". On the contrary, the reciprocal entailment (H₁ \−∗ H₃) ==> (H₁ \−∗ H₂) \* (H₂ \−∗ H₃) is false. Intuitively, from H₁ ≤ H₃ there is no way to justify H₁ ≤ H₂ nor H₂ ≤ H₃.

Optional Material

Equivalence Between Alternative Definitions of the Magic Wand

In what follows we prove the equivalence between the three characterizations of hwand H₁ H₂ that we have presented: 1. The definition hwand expressed directly in terms of heaps: fun h ⇒ ∀ h', Fmap.disjoint h h' → H₁ h' → H₂ (h' \u h) 2. The definition hwand expressed in terms of existing operators: \∃ H₀, H₀ \* \[ (H₁ \* H₀) ==> H₂] 3. The characterization via the equivalence hwand_equiv: ∀ H₀ H₁ H₂, (H₀ ==> H₁ \−∗ H₂) ↔ (H₁ \* H₀ ==> H₂). 4. The characterization via the pair of the introduction rule himpl_hwand_r and the elimination rule hwand_cancel. To prove the 4-way equivalence, we first prove the equivalence between (1) and (2), then prove the equivalence between (2) and (3), and finally the equivalence between (3) and (4).

The equivalence proofs are given here for reference. The reader needs not follow through the details of these proofs.