First Pass

This chapter presents 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 use:

• it is key to formulate 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,
• 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 the magic wand.

Operator hforall

The heap predicate \∀ x, H holds of a heap h that, for any possibly value of x, satisfies H. It may be puzzling at first what could possibly be the use case for such a universal quantification. 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 exact same pattern as for hexists.

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

The introduction rule in an entailement for \∀ appears below. To prove that a heap satisfies \∀ x, J x, one 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, one 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 in a similar fashion as universal quantifiers appearing on the left-hand side of an entailment.

Operator hor

The heap predicate hor H₁ H₂ describes a heap that satisfies H₁ or satifies H₂ (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 appeared critically useful in practice, because it can be encoded using Coq conditional construct, or using Coq 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 benefits of this definition is that the proof of 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 asserts that if H₁ holds, then hor H₁ H₂ holds; and, symmetrically, if H₂ holds, then hor H₁ H₂ holds.

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

The elimination rule asserts that if hor H₁ H₂ holds, then one 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₃, one 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 if_neg and hprop_op_comm (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 to unfold MList, but instead work using the equalities MList_nil and MList_cons.

Operator hand

The heap predicate hand H₁ H₂ describes a 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, shown below, 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'.

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₂", one must prove that H₃ entails H₁, and that H₃ satisfies H₂.

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

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

Magic Wand: hwand

Definition of hwand

The magic wand operation H₁ \−∗ H₂, to be read "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 one thinks of the star H₁ \* H₂ as the addition H₁ + H₂, then one can think of H₁ \−∗ H₂ as the subtraction -H₁ + H₂. The entailment stated above essentially 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 that satisfies 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. 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 of hwand shown below, observe how H₀ is existentially quantified.

As established further in this file, hwand and hwand' both define the same operator. The reason we prefer taking hwand as definition rather than hwand' is that it 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.

Characteristic Equivalence for hwand

The magic wand is not so 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.

It turns out that the magic wand operator is uniquely defined by the equivalence (H₀ ==> H₁ \−∗ H₂) ↔ (H₁ \* H₀ ==> H₂). In other words, as we establish further on, 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₂, one has 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₂). What can be deduced from this entailment is that if H₀ is starred with H₁, then H₂ can be recovered.

This elimination rule can be equivalently reformulated in the following form, which makes clearer that H₁ \−∗ H₂, when starred with H₁, yields H₂.

Other Properties of hwand

We next present the most important properties of the magic wand operator. Thereafter, the tactic xsimpl is available, yet in a form that does not provide support for the magic wand. The actual 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₂, similarly to the implication operator →.

Two predicates H₁ \−∗ H₂ ans H₂ \−∗ H₃ may simplify to H₁ \−∗ H₃. This simplification is reminiscent of the arithmetic operation (-H₁ + H₂) + (-H₂ + H₃) = (-H₁ + H₃).

The predicate H \−∗ H holds of the empty heap. Intuitively, one 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, one can rewrite -0+H as +H.

The lemma above shows that the empty predicate \[] 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)

Prove hwand_hpure_l, whose statement appears below.

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₂].

An interesting property is that arguments on the LHS of a magic wand can equivalently be "curried" or "uncurried", just like a function of type (A * B) → C is equivalent to a function of type A → B → C. The heap predicates (H₁ \* H₂) \−∗ H₃ and H₁ \−∗ (H₂ \−∗ H₃) and H₂ \−∗ (H₁ \−∗ H₃) are all equivalent. Intuitively, they all describe the predicate 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₁.

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₃, one 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 H₁ \−∗ (H₂ \* H₃) is equivalent to True, hence imposes no restriction on the heap. Yet, to establish (H₁ \−∗ H₂) \* H₃, one 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'.

Magic Wand 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, and not a postcondition. There are two ways to define the operator qwand. The first possibility 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 on top of hwand, by means of the hforall quantifier.

As established further on in this chapter, qwand and qwand' both define the same operator. We prefer taking qwand as 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 the direct counterpart 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₂.

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

Automation with xsimpl for hwand Expressions

One 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 tactic xsimpl illustrated in this section.

The tactic 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 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 Separation Logic Operators

The core operators are defined as functions over heaps.

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

Note: these derived operators could also be defined directly as predicate over heaps. The definitions are shown below. 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 pervasively used for example by the tactic xapp for reasoning about applications.

This rule suffers from a practical issue, which we illustrate in details on a concrete example further on. For now, let us just attempt to describe the issue at a high-level. In short, the problem stems from the fact that we need to instantiate H₂ for 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 the cases where H contains existential quantifiers. Indeed, such existential quantifiers are typically first extracted out of the entailment H ==> H₁ \* H₂ by the tactic xsimpl. However, these existentially quantified variables are not in the scope of H₂, hence the instantiation of the evar associated with H₂ typically fails. The "ramified frame rule" exploits the magic wand operator to circumvent the 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, and show how the ramified frame rule smoothly handles that same 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, consider the specification of the function ref, which allocates a reference.

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

Let us prove that this specification is derivable from the original one, namely 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.

Tempting Yet False Properties for the Magic Wand

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

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

More generally, one has to 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.