First Pass

This chapter introduces an additional Separation Logic operator, called the "magic wand", and written H₁ \−∗ H₂. This operator has multiple use:

• it helps reformulate the consequence-frame rule in an improved manner, through a rule called the "ramified frame rule",
• it helps stating the weakest-preconditions of a number of languages constructs in a concise manner,
• it can be useful to state specification for certain data structures.

This chapter is organized as follows:

• definition and properties of the magic wand operator,
• generalization of the magic wand to postconditions,
• statement and benefits of the ramified frame rule,
• statement of the ramified frame rule in weakest-precondition style,
• generalized definition of wpgen that recurses in local functions.

The addition and bonus section includes further discussion, including:

• presentation of alternative, equivalent definitions of the magic wand,
• statement and proofs of additional properties of the magic wand,
• a revised definition of mkstruct using the magic wand.
• "Texan triples", which express function specifications using the magic wand instead of using triples,
• two other operators, disjunction and non-separating conjunction, so as to complete the presentation of all Separation Logic operators.

Intuition for the Magic Wand

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 can think 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₂.

Definition of the Magic Wand

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 we establish further in this file, one can prove that hwand and hwand' 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, conducting all the reasoning at the level of hprop rather than having to work with explicit heaps of type heap.

Characteristic Property of the Magic Wand

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 for all arguments 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₀. What needs to be proved to establish H₀ ==> (H₁ \−∗ H₂) is that H₀, when starred with 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₂.

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

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

Magic Wand for Postconditions

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. The definition follows exactly the same pattern as hwand: it quantifies some heap predicate H₀ such that H₀ starred with Q₁ yields Q₂.

The operator qwand satisfies essentially the same properties as hwand. Let us begin with the associated equivalence rule, which captures both the introduction and the elimination rule.

The cancellation rule follows.

An interesting property of qwand is the fact that we can specialize Q₁ \−−∗ Q₂ to (Q₁ v) \−∗ (Q₂ v), for any value v.

Frame Expressed with hwand: 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 merging 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.

Ramified Frame Rule in Weakest-Precondition Style

The ramified frame rule, which we have just stated for triples, features a counterpart expressed in weakest-precondition style (wp). In what follows, we present the "wp ramified rule", named wp_ramified. This rule admits a concise statement and subsumes all other structural rules of Separation Logic. Its statement is as follows.
    (wp t Q₁) \* (Q₁ \−−∗ Q₂) ==> (wp t Q₂). To see where this statement comes from, recall from the chapter WPsem the rule named wp_conseq_frame, which combines the consequence rule and the frame rule for wp.

Let us reformulate this rule using a magic wand. The premise Q₁ \*+ H ===> Q₂ can be rewritten as H ==> (Q₁ \−−∗ Q₂). By replacing H with Q₁ \−−∗ Q₂ in the conclusion of wp_conseq_frame, we obtain the ramified rule for wp.

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

Prove that wp_conseq_frame is derivable from wp_ramified. To that end, prove the statement of wp_conseq_frame by using only wp_ramified, the characteristic property of the magic wand qwand_equiv, and properties of the entailment relation.

The following reformulation of wp_ramified can be more practical to exploit in practice, because it applies to any goal of the form H ==> wp t Q.

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.

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 merged, leaving just 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 merged, leaving (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 merge Q₁ \−−∗ Q₂ with Q₁ v, leaving Q₂ v.

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

Evaluation of wpgen Recursively in Locally Defined Functions

Recall from chapter WPgen the original definition of wpgen, that is, before numerous refactoring. It admitted the following shape.
    Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=
      match t with
      | trm_val v ⇒ Q v
      | trm_fun x t₁ ⇒ Q (val_fun x t₁)
      | trm_fix f x t₁ ⇒ Q (val_fix f x t₁)
      ...
      end. This definition of wpgen t Q does not recurse inside the body of functions that occur in the argument t. Instead, it treats such locally defined functions just like values. Not processing local functions does not limit expressiveness, because it is always possible for the user to manually invoke wpgen for each locally defined function, during the verification proof. Nevertheless, it is much more satisfying and much more practical to set up wpgen so that it recursively computes the weakest precondition of all the local functions that it encounters during its evaluation. In what follows, we show how such a version of wpgen can be set up. We begin with the case of non-recursive functions of the form trm_fun x t₁, then generalize the definition to the slightly more complex case of recursive functions of the form trm_fix f x t₁. In both cases, the function wpgen will get recursively invoked on the body t₁ of the function, in a context extended with the appropriate bindings. The new definition of wpgen will take the shape shown below, for well-suited definitions of wpgen_fun and wpgen_fix yet to be introduced. In the code snippet below, vx denotes a value to which the function may be applied, and vf denotes the value associated with the function itself, this value being used in particular in the case of recursive calls.
    Fixpoint wpgen (E:ctx) (t:trm) : formula :=
      mkstruct match t with
      | trm_val v ⇒ wpgen_val v
      | trm_fun x t₁ ⇒ wpgen_fun (fun vx ⇒ wpgen ((x,vx)::E) t₁)
      | trm_fix f x t₁ ⇒ wpgen_fix (fun vf vx ⇒ wpgen ((f,vf)::(x,vx)::E) t₁)
      ...
      end.

1. Treatment of Non-Recursive Functions

For simplicity, let us assume for now the substitution context E to be empty, and let us ignore the presence of the predicate mkstruct. Our goal task is to provide a definition for wpgen (trm_fun x t₁) Q, expressed in terms of wpgen t₁. Let vf denote the function val_fun x t₁, which the term trm_fun x t₁ evaluates to. The heap predicate wpgen (trm_fun x t₁) Q should assert that that the postcondition Q holds of the result value vf, i.e., that Q vf should hold. Rather than specifying that vf is equal to val_fun x t₁ as we were doing previously, we would like to specify that vf denotes a function whose body admits wpgen t₁ as weakest precondition. This information no longer exposes the syntax of the term t₁, and is nevertheless sufficient for the user to reason about the behavior of the function vf. To that end, we define the heap predicate wpgen (trm_fun x t₁) Q to be of the form \∀ vf, \[P vf] \−∗ Q vf for a carefully crafted predicate P that describes the behavior of the function by means of its weakest precondition. P is defined further on. The universal quantification on vf is intended to hide away from the user the fact that vf actually denotes val_fun x t₁. It would be correct to replace \∀ vf, ... with let vf := val_fun x t₁ in ..., yet we are purposely trying to abstract away from the syntax of t₁, hence the universal quantification of vf. In the heap predicate \∀ vf, \[P vf] \−∗ Q vf, the magic wand features a left-hand side of the form \[P vf] is intended to provide to the user the knowledge of the weakest precondition of the body t₁ of the function, in such a way that the user is able to derive the specification aimed for the local function vf. Concretely, the proposition P vf should enable the user establishing properties of applications of the form trm_app vf vx, where vf denotes the function and vx denotes an argument to which the function is applied. To figure out the details of the statement of P, it is useful to recall from chapter WPgen the statement of the lemma triple_app_fun_from_wpgen, which we used for reasoning about top-level functions. Its statement appears below---variables were renamed to better match the current context.

The lemma above enables establishing a triple for an application trm_app vf vx with precondition H' and postcondition Q', from the premise H' ==> wgen ((x,vx)::nil) t₁ Q'. It therefore makes sense, in our definition of the predicate wpgen (trm_fun x t₁) Q, which we said would take the form \∀ vf, \[P vf] \−∗ Q vf, to define P vf as:
    ∀ vx H' Q', (H' ==> wpgen ((x,vx)::nil) t₁ Q') →
                     triple (trm_app vf vx) H' Q' This proposition can be slightly simplified, by using wp instead of triple, allowing to eliminate H'. We thus define P vf as:
    ∀ vx H', wpgen ((x,vx)::nil) t₁ Q' ==> wp (trm_app vf vx) Q' Overall, the definition of wpgen E t is as follows. Note that the occurence of nil is replaced with E to account for the case of a nonempty context.
  Fixpoint wpgen (E:ctx) (t:trm) : formula :=
    mkstruct match t with
    ...
    | trm_fun x t₁ ⇒ fun Q ⇒
       let P vf :=
         (∀ vx H', wpgen ((x,vx)::nil) t₁ Q' ==> wp (trm_app vf vx) Q') in
       \∀ vf, \[P vf] \−∗ Q vf
   ...
   end. The actual definition of wpgen exploits an intermediate definition called wpgen_fun, as shown below:
    Fixpoint wpgen (E:ctx) (t:trm) : formula :=
      mkstruct match t with
      ...
      | trm_fun x t₁ ⇒ wpgen_fun (fun vx ⇒ wpgen ((x,vx)::E) t₁)
      ...
      end. where wpgen_fun is defined as follows:

The soundness lemma for this construct follows from the wp-style reasoning rule for applications, called wp_app_fun, introduced in chapter WPsem. It is not needed to follow at this stage through the details of the proof. (The proof involves lemmas about \∀ and about \−∗ that are stated and proved only further on in this chapter.)

When we carry out the proof of soundness for the new version of wpgen that features wpgen_fun, we obtain the following new proof obligation. (To see it, play the proof of lemma wpgen_sound, in file LibSepDirect.v.)

The proof exploits the lemma wpgen_fun_sound that we just established, as well as a substitution lemma, the same as the one used to justify the soundness of the wpgen of a let-binding.

Like for other auxiliary functions associated with wpgen, we introduce a custom notation for wpgen_fun. Here, we let Fun x := F stand for wpgen_fun (fun x ⇒ F).

2. Treatment of Recursive Functions

The formula produced by wpgen for a recursive function trm_fix f x t₁ is almost the same as for a non-recursive function, the main difference being that we need to add a binding in the context to associate the name f of the recursive function with the value vf that corresponds to the recursive function. Here again, the heap predicate wpgen (trm_fun x t₁) Q will be of the form \∀ vf, \[P vf] \−∗ Q vf. To figure out the details of the statement of P, recall from WPgen the statement of triple_app_fix_from_wpgen, which is useful for reasoning about top-level recursive functions.

It therefore makes sense to define P vf as:
    ∀ vx H' Q', (H' ==> wpgen ((f,vf)::(x,vx)::nil) t₁ Q') →
                     triple (trm_app vf vx) H' Q' which can be rewritten as:
    ∀ vx H', wpgen ((f,vf)::(x,vx)::nil) t₁ Q' ==> wp (trm_app vf vx) Q' We thus consider:
    Fixpoint wpgen (E:ctx) (t:trm) : formula :=
      mkstruct match t with
      | ..
      | trm_fix f x t₁ ⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf)::(x,v)::E) t₁)
      | ..
      end with the following definition for wpgen_fix.

The soundness lemma for wpgen_fix is very similar to that of wpgen_fun. Again, it is not needed to follow through the details of this proof.

The proof of soundness of wpgen involves the following proof obligation to handle the case of recursive functions. (To see it, play the proof of lemma wpgen_sound, in file LibSepDirect.v.)

Here again, we introduce a piece of notation for wpgen_fix. We let Fix f x := F stand for wpgen_fix (fun f x ⇒ F).

Remark: similarly to xfun, one could devise a xfix tactic. We omit the details.

3. Final Definition of wpgen, with Processing a Local Functions

The final definition of wpgen appears below.

The full soundness proof appears in file LibSepDirect, lemma wpgen_sound.

4. Tactic to Reason About Functions

Like for other language constructs, we introduce a custom tactic for wpgen_fun. It is called xfun, and helps the user to process a local function definition in the course of a verification script. The tactic xfun can be invoked either with or without providing a specification for the local function. First, we describe the tactic xfun S, where S describes the specification of the local function. A typical call is of the form xfun (fun (f:val) ⇒ ∀ ..., triple (f ..) .. ..). The tactic xfun S generates two subgoals. The first one requires the user to establish the specification S for the function whose body admits the weakest precondition Fof. The second one requires the user to prove that the rest of the program is correct, in a context where the local function can be assumed to satisfy the specification S. The definition of xfun S appears next. It is not required to understand the details. An example use case appears further on.

Second, we describe the tactic xfun without argument. It applies to a goal of the form H ==> wpgen_fun Fof Q. The tactic xfun simply makes available an hypothesis about the local function. The user may subsequently exploit this hypothesis for reasoning about a call to that function, just like if the code of the function was inlined at its call site. The use of xfun without argument is usually relevant only for local functions that are invoked exactly once (as is often the case for functions passed to higher-order iterators). Again, an example use case appears further on.

A generalization of xfun that handles recursive functions may be defined following exactly the same pattern. This completes our presentation of a version of wpgen that recursively processes the local definition of non-recursive functions. An practical example is presented next.

5. Example Computation of wpgen in Presence of a Local Function

In the example that follows, we assume all the set up from WPgen to be reproduced with the definition of wpgen that leverages wpgen_fun and wpgen_fix. This set up is formalized in full in the file LibSepDirect.

Consider the following example program, which involves a local function definition, then two successive calls to that local function.

We first illustrate a call to xfun with an explicit specification. Here, the function f is specified as incrementing the reference p. Observe that the body function of the function f is verified only once. The reasoning about the two calls to the function f that appears in the code are done with respect to the specification that we provide as argument to xfun at the moment of the definition of f.

We next illustrate a call to xfun without argument. The "generic specification" that comes as hypothesis about the local function is a proposition that describes the behavior of the function in terms of the weakest-precondition of its body. When reasoning about a call to the function, one can invoke this generic specification. The effect is equivalent to that of inlining the code of the function at its call site. Here, there are two calls to the function. We will thus have to exploit twice the generic specification of f, which corresponds to its body incr p. We will therefore have to reason twice about the increment function.

More Details

Benefits of the Ramified Rule over the Consequence-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 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.

Properties of hwand

We next present the most important properties of H₁ \−∗ H₂. Thereafter, the tactic xsimpl is accessible, but in a form that does not provide support for the magic wand. The actual tactic would trivially solve many of these lemmas, but using it would be cheating because the implementation of xsimpl relies on several of these lemmas.

Structural Properties of hwand

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.

Tempting Yet False Properties for hwand

The reciprocal entailement (H \−∗ H) ==> \[] is false, however. For a counterexample, instantiate H as fun h ⇒ True, or, equivalently, \∃ H', H'. A singleton heap does satisfy H \−∗ H, although it clearly does not satisfy the empty predicate \[].

In technical terms, H \−∗ H characterizes the empty heap only in the case where H is "precise", that is, when it describes a heap of a specific shape. In the above counterexample, H is clearly not precise, because it is satisfied by heaps of any shape. The notion of "preciseness" can be defined formally, yet it is out of the scope of this course. 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]. We can prove that the empty heap does not satisfies \[False] \* (\[False] \−∗ \[]).

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". From that, we can derive H₁ ≤ H₃, and justify that the right-hand-side makes sense. On the contrary, the reciprocal entailment (H₁ \−∗ H₃) ==> (H₁ \−∗ H₂) \* (H₂ \−∗ H₃) is certainly false, because from H₁ ≤ H₃ there is no way to justify H₁ ≤ H₂ nor H₂ ≤ H₃.

Interaction of hwand with hempty and hpure

The heap predicate \[] \−∗ H is equivalent to 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:

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

Interaction of hwand with hstar

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₃."

Remark: the reciprocal entailment is false: it is not possible to extract a heap predicate out of the LHS of an entailment. Indeed, that heap predicate might not exist if it is mentioned in the RHS of the magic wand.

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: you can use xsimpl during the proof.

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. It is not needed to follow through the technical details.