Implicit Types

First Pass

In the previous chapter, we have introduced the type hprop and the key operators over this type: \[], \[P], p ~~> v, H₁ \* H₂, Q₁ \*+ H₂, and \∃ x, H. In order to state the reasoning rules of Separation Logic, we need to introduce the "entailment relation" on heap predicates. This relation, written H₁ ==> H₂, asserts that any heap that satisfies H₁ also satisfies H₂. We also need to extend the entailment relation to postconditions. We write Q₁ ===> Q₂ to asserts that, for any result value v, the entailment Q₁ v ==> Q₂ v holds. For example, the "consequence-frame rule", exploited by the tactic xapp for reasoning about every function call, is stated using entailements for pre- and postconditions. This rule explains how to derive a triple of the from triple t H Q, knowing that the term t admits the specification triple t H₁ Q₁. There are two requirements: First, the precondition H must decompose into H₁, which denotes the precondition expected by the specification, and the remaining part, called H₂. Second, the targeted postcondition Q must be a consequence of the conjunction of Q₁, which denotes the postcondition asserted by the specification, and H₂, which denotes the remaining part that has not been affected during the evaluation of the term t. The formal statement is as follows.
    Lemma triple_conseq_frame : ∀ H₂ H₁ Q₁ t H Q,
      triple t H₁ Q₁ →
      H ==> (H₁ \* H₂) →
      (Q₁ \*+ H₂) ===> Q →
      triple t H Q. This chapter presents:

• the formal definition of the entailment relations, for heap predicates and for postconditions,
• the lemmas capturing the interaction of entailment with the star operator,
• the tactics xsimpl and xchange that are critically useful for manipulating entailments in practice.

Definition of Entailment

The "entailment relationship" H₁ ==> H₂ asserts that any heap h that satisfies the heap predicate H₁ also satisfies the heap predicate H₂.

As we show next, the entailment relation is reflexive, transitive, and antisymmetric. It thus forms an order relation on heap predicates.

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

Prove the antisymmetry of entailment result shown below. Hint: use predicate_extensionality.

Entailment for Postconditions

The entailment relation can be used to capture that a precondition "entails" another one. We need a similar judgment to assert that a postcondition "entails" another one. For that purpose, we introduce the relation Q₁ ===> Q₂, which asserts that for any value v, the heap predicate Q₁ v entails Q₂ v.

In other words, Q₁ ===> Q₂ holds if and only if, for any value v and any heap h, the proposition Q₁ v h implies Q₂ v h. Entailment on postconditions also forms an order relation: it is reflexive, transitive, and antisymmetric.

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

Prove the antisymmetry of entailment on postconditions. Hint: exploit functional_extensionality.

Frame Rule for Entailment

A fundamental property is that the star operator is "monotone" with respect to entailment, meaning that if H₁ ==> H₁' then (H₁ \* H₂) ==> (H₁' \* H₂). In other words, an arbitrary heap predicate H₂ can be "framed" on both sides of an entailment. Viewed the other way around, if we have to prove the entailment relation (H₁ \* H₂) ==> (H₁' \* H₂), we can "cancel out" H₂ on both sides. In this view, the monotonicity property is a sort of "frame rule for the entailment relation". Due to commutativity of star, it suffices to state the left version of the monotonicity property.

Introduction and Elimination Rules w.r.t. Entailments

The rules for introducing and eliminating pure facts and existential quantifiers in entailments are essential. They are presented next. The first rule is captured by the lemma himpl_hstar_hpure_r. Consider an entailment of the form H ==> (\[P] \* H'). To establish this entailment, one must prove that P is true, and that H entails H'.

Exercise: 2 stars, standard, especially useful (himpl_hstar_hpure_r).

Prove the rule himpl_hstar_hpure_r. Hint: recall from Hprop the lemma hstar_hpure_l, which asserts the equality (\[P] \* H) h = (P ∧ H h).

Reciprocally, consider an entailment of the form (\[P] \* H) ==> H'. To establish this entailment, one must prove that H entails H' under the assumption that P is true. The "extraction rule for pure facts in the left of an entailment" captures the property that the pure fact \[P] can be extracted into the Coq context. It is stated as follows.

Exercise: 2 stars, standard, especially useful (himpl_hstar_hpure_l).

Prove the rule himpl_hstar_hpure_l.

Consider an entailment of the form H ==> (\∃ x, J x), where x has some type A and J has type A→hprop. To establish this entailment, one must exhibit a value for x for which H entails J x.

Exercise: 2 stars, standard, especially useful (himpl_hexists_r).

Prove the rule himpl_hexists_r.

Reciprocally, consider an entailment (\∃ x, (J x)) ==> H. To establish this entailment, one has to prove that, whatever the value of x, the predicate J x entails H. Indeed the former proposition asserts that if a heap h satisfies J x for some x, then h satisfies H', while the latter asserts that if, for some x, the predicate h satisfies J x, then h satisfies H'. The "extraction rule for existentials in the left of an entailment" captures the property that existentials can be extracted into the Coq context. It is stated as follows. Observe how the existential quantifier on the left of the entailment becomes an universal quantifier outside of the arrow.

Exercise: 2 stars, standard, especially useful (himpl_hexists_l).

Prove the rule himpl_hexists_l.

Extracting Information from Heap Predicates

We next present an example showing how entailments can be used to state lemmas allowing to extract information from particular heap predicates. Concretely, we show that from a heap predicate of the form (p ~~> v₁) \* (p ~~> v₂) describes two "disjoint" cells that are both "at location p", one can extract a contradiction. Indeed, such a state cannot exist. The underlying contraction is formally captured by the following entailment relation, which concludes False.

The proof of this result exploits a result on finite maps. Essentially, the domain of a single singleton map that binds a location p to some value is the singleton set \{p}, thus such a singleton map cannot be disjoint from another singleton map that binds the same location p.
    Check disjoint_single_single_same_inv : ∀ (p:loc) (v₁ v₂:val),
      Fmap.disjoint (Fmap.single p v₁) (Fmap.single p v₂) →
      False. Using this lemma, we can prove hstar_hsingle_same_loc by unfolding the definition of hstar to reveal the contradiction on the disjointness assumption.

More generally, a heap predicate of the form H \* H is generally suspicious in Separation Logic. In the simple variant of Separation Logic that we consider in this course, there are only 3 typical situations where H \* H makes sense: (1) if H is the empty heap predicate \[], (2) If H is a pure heap predicate of the form \P], (3) if H of the form \∃ H₀, H₀, which will be written \GC in chapter Affine.

Rules for Naming Heaps

Thereafter, we write = h as a shorthand for fun h' ⇒ h' = h, that is, the heap predicate that only accepts heaps exactly equal to h.

Exercise: 3 stars, standard, optional (hexists_named_eq)

Prove that a heap predicate H is equivalent to \∃ h, \[H h] \* (= h)). Hint: use hstar_hpure_l and hexists_intro , as well as the extraction rules himpl_hexists_l and himpl_hstar_hpure_l.

Identifying True and False Entailments

In the rest of this file, we load the definition from LibSepReference.

Quiz: For each entailment relation, indicate (without a Coq proof) whether it is true or false. Solutions appear further on.

The answers to the quiz are as follows. 1. True, by commutativity. 2. False, because one cell does not entail two cells. 3. False, because two cells do not entail one cell. 4. False, because two cells do not entail one cell. 5. True, because \False entails anything. 6. False, because a satisfiable heap predicate does not entail \False. 7. True, because a cell cannot be starred with itself. 8. True, because a cell cannot be starred with itself. 9. True, by instantiating n with 3. 10. False, because n could be something else than 3. 11. True, by instantiating n in RHS with n+1 for the n of the LHS. 12. True, by instantiating n with 3. 13. True, because it is equivalent to \[False] ==> \[False]. Proofs for the true results appear below.

More Details

Proving Entailments by Hand

Proving an entailment by hand is generally a tedious task. This is why most frameworks based on Separation Logic include an automated tactic for simplifying entailments. In this course, the relevant tactic is named xsimpl. Further in this chapter, we describe by means of examples the behavior of this tactic. In order to best appreciate what a simplification tactic provides and best understand how it works, it is very useful to first complete a few proofs by hand.

Exercise: 3 stars, standard, optional (himpl_example_1)

Prove the example entailment below. Hint: exploit hstar_comm, hstar_assoc, or hstar_comm_assoc which combines the two, and exploit himpl_frame_l or himpl_frame_r to cancel out matching pieces.

Exercise: 3 stars, standard, optional (himpl_example_2)

Prove the example entailment below. Hint: use himpl_hstar_hpure_l to extract pure facts, once they appear at the head of the left-hand side of the entailment. For arithmetic inequalities, use the math tactic.

Exercise: 3 stars, standard, optional (himpl_example_3)

Prove the example entailment below. Hint: use lemmas among himpl_hexists_r , himpl_hexists_l, himpl_hstar_hpure_r and himpl_hstar_hpure_r to deal with pure facts and quantifiers.

The xsimpl Tactic

Performing manual simplifications of entailments by hand is an extremely tedious task. Fortunately, it can be automated using specialized Coq tactic. This tactic, called xsimpl, applies to an entailment and implements a 3-step process:

• extract pure facts and existential quantifiers from the LHS,
• cancel out equal predicates occurring both in the LHS and RHS,
• generate subgoals for the pure facts occurring in the RHS, and instantiate the existential quantifiers from the RHS (using either unification variables or user-provided hints).

These steps are detailed and illustrated next.

xsimpl to Extract Pure Facts and Quantifiers in LHS

The first feature of xsimpl is its ability to extract the pure facts and the existential quantifiers from the left-hand side out into the Coq context. In the example below, the pure fact n > 0 appears in the LHS. After calling xsimpl, this pure fact is turned into an hypothesis, which may be introduced with a name into the Coq context.

In case the LHS includes a contradiction, such as the pure fact False, the goal gets solved immediately by xsimpl.

The xsimpl tactic also extracts existential quantifier from the LHS. It turns them into universally quantified variables outside of the entailment relation, as illustrated through the following example.

A call to xsimpl extract at once all the pure facts and quantifiers from the LHS, as illustrated next.

xsimpl to Cancel Out Heap Predicates from LHS and RHS

The second feature of xsimpl is its ability to cancel out similar heap predicates that occur on both sides of an entailment. In the example below, H₂ occurs on both sides, so it is canceled out by xsimpl.

xsimpl actually cancels out at once all the heap predicates that it can spot appearing on both sides. In the example below, H₂, H₃, and H₄ are canceled out.

If all the pieces of heap predicate get canceled out, the remaining proof obligation is \[] ==> \[]. In this case, xsimpl automatically solves the goal by invoking the reflexivity property of entailment.

xsimpl to Instantiate Pure Facts and Quantifiers in RHS

The third feature of xsimpl is its ability to extract pure facts from the RHS as separate subgoals, and to instantiate existential quantifiers from the RHS. Let us first illustrate how it deals with pure facts. In the example below, the fact n > 0 gets spawned in a separated subgoal.

When it encounters an existential quantifier in the RHS, the xsimpl tactic introduces a unification variable denoted by a question mark, that is, an "evar", in Coq terminology. In the example below, the xsimpl tactic turns \∃ n, .. p ~~> n .. into .. p ~~> ?x ...

The "evar" often gets subsequently instantiated as a result of a cancellation step. For example, in the example below, xsimpl instantiates the existentially quantified variable n as ?x, then cancels out p ~~> ?x from the LHS against p ~~> 3 on the right-hand-side, thereby unifying ?x with 3.

The instantiation of the evar ?x can be observed if there is another occurrence of the same variable in the entailment. In the next example, which refines the previous one, observe how n > 0 becomes 3 > 0.

(Advanced.) In certain situations, it may be desirable to provide an explicit value for instantiating an existential quantifier that occurs in the RHS. The xsimpl tactic accepts arguments, which will be used to instantiate the existentials (on a first-match basis). The syntax is xsimpl v₁ .. vn, or xsimpl (>> v₁ .. vn) in the case n > 3.

(Advanced.) If two existential quantifiers quantify variables of the same type, it is possible to provide a value for only the second quantifier by passing as first argument to xsimpl the special value __. The following example shows how, on LHS of the form \∃ n m, ..., the tactic xsimpl __ 9 instantiates m with 9 while leaving n as an unresolved evar.

xsimpl on Entailments Between Postconditions

The tactic xsimpl also applies on goals of the form Q₁ ===> Q₂. For such goals, it unfolds the definition of ===> to reveal an entailment of the form ==>, then invokes the xsimpl tactic.

Example of Entailment Proofs using xpull and xsimpl

xpull is a simplified version of xsimpl that operates only the left-hand side of the entailement.

xsimpl first invokes xpull to simplify the left-hand side, then attempts to cancel out items from the right-hand side with items from the left-hand-side.

The xchange Tactic

The tactic xchange is to entailment what rewrite is to equality. Assume an entailment goal of the form H₁ \* H₂ \* H₃ ==> H₄. Assume an entailment assumption M, say H₂ ==> H₂'. Then xchange M turns the goal into H₁ \* H₂' \* H₃ ==> H₄, effectively replacing H₂ with H₂'.

The tactic xchange can also take as argument equalities. The tactic xchange M exploits the left-to-right direction of an equality M, whereas xchange <- M exploits the right-to-left direction .

The tactic xchange M does accept a lemma or hypothesis M featuring universal quantifiers, as long as its conclusion is an equality or an entailment. In such case, xchange M instantiates M before attemting to perform a replacement.

How does the xchange tactic work? Consider a goal of the form H ==> H' and assume xchange is invoked with an hypothesis of type H₁ ==> H₁' as argument. The tactic xchange should attempt to decompose H as the star of H₁ and the rest of H, call it H₂. If it succeeds, then the goal H ==> H' can be rewritten as H₁ \* H₂ ==> H'. To exploit the hypothesis H₁ ==> H₁', the tactic should replace the goal with the entailment H₁' \* H₂ ==> H'. The lemma shown below captures this piece of reasoning implemented by the tactic xchange.

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

Prove, without using the tactic xchange, the following lemma which captures the internal working of xchange.

Optional Material

Proofs of Rules for Entailment

We next show the details of the proofs establishing the fundamental properties of the Separation Logic operators. All these results must be proved without help of the tactic xsimpl, because the implementation of the tactic xsimpl itself depends on these fundamental properties. We begin with the frame property, which is the simplest to prove.

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

Prove the frame property for entailment. Hint: unfold the definition of hstar.

The lemma himpl_frame_l admits two useful corollaries, presented next.

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

Prove himpl_frame_r, which is the symmetric of himpl_frame_l.

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

The monotonicity property of the star operator w.r.t. entailment can also be stated in a symmetric fashion, as shown next. Prove this result. Hint: exploit the transitivity of entailment (himpl_trans) and the asymmetric monotonicity result (himpl_frame_l).

Historical Notes

Nearly every project that aims for practical program verification using Separation Logic features, in one way or another, some amount of tooling for automatically simplifying Separation Logic assertion. The tactic used here, xsimpl, was developed for the CFML tool. Its specification may be found in Appendix K from Charguéraud's ICFP'20 paper: http://www.chargueraud.org/research/2020/seq_seplogic/seq_seplogic.pdf