First Pass

The first two chapters have illustrated how to specify and verify programs using Separation Logic. The purpose of the coming chapters is to explain how to formally assign meaning to the tokens used in the statement of specifications (e.g., the star operator), formally define the notion of Separation Triples, and prove the reasoning rules of Separation Logic. These rules are exploited by the "x-tactics" used in the first two chapters. This chapter presents the formal definitions of the key heap predicate operators from Separation Logic:

• \[] denotes the empty heap predicate,
• \[P] denotes a pure fact,
• p ~~> v denotes a predicate that characterizes a singleton heap,
• H₁ \* H₂ denotes the separating conjunction,
• Q₁ \*+ H₂ denotes the separating conjunction between a postcondition and a heap predicate,
• \∃ x, H denotes an existential quantifier.

To begin with, we define the type state, for describing a full memory state. We then introduce the type heap, an alias for state, intended to describe pieces of state. In Separation Logic, specifications are expressed using "heap predicates", predicates over heaps, of type heap→Prop. We define hprop to be a shorthand for that type. By convention, throughout the course:

• H denotes a heap predicate of type hprop; it describes a piece of state,
• Q denotes a postcondition, of type val→hprop; it describes both a result value and a piece of state.

Description of Memory States

To reason about imperative programs, Separation Logic relies on heap predicates for describing memory states. As the name suggests, a "heap predicate" is a predicate over heaps, i.e., over memory states. Heap predicates such as p ~~> n, or H₁ \* H₂ admit the type state → Prop, where the type state corresponds to a finite map used to describe the contents of the memory. In what follows, we give the formal definition of state and of the type of heap predicates. In the previous chapters, we have assumed a type val to range over program values and a type loc to denote memory locations. Concrete definitions will be provided later on, in chapter Rules. At this point, we are interested in the definition of the type state, used to describe the contents of the memory during the execution of a program. A state is a finite map from locations to values. The file LibSepFmap.v provides a self-contained formalization of finite maps. An object of type fmap A B represents a finite map binding keys of type A to values of type B. We define the type state as a map from locations, of type loc, to program values, of type val.

By convention, we use the type state to describe a "full" memory state, and we use an alias, the type heap, to describe a "piece of" state.

The file LibSepReference introduces the module name Fmap as a shorthand for LibSepFmap. The key operations associated with finite maps are:

• Fmap.empty denotes the empty state,
• Fmap.single p v denotes a singleton state, that is, a unique cell at location p with contents v,
• Fmap.union h₁ h₂ denotes the union of the two states h₁ and h₂.
• Fmap.disjoint h₁ h₂ asserts that h₁ and h₂ have disjoint domains.

Note that the union operation is commutative only when its arguments have disjoint domains. Throughout the course, we only consider disjoint unions, for which commutativity holds.

Heap Predicates

In Separation Logic, the state is described using "heap predicates". A heap predicate is a predicate "over a piece of state", as opposed to "over a full state". Let hprop denote the type of heap predicates.

H ranges over heap predicates.

An essential aspect of Separation Logic is that all heap predicates defined and used in practice are built using a few basic combinators. In other words, except for the definition of the combinators themselves, we will never define a custom heap predicate directly as a function of the state. We next describe the most important combinators, which were pervasively used throughout the first two chapters. The hempty predicate, usually written \[], characterizes an empty state.

The pure fact predicate, written \[P], characterizes an empty state and moreover asserts that the proposition P is true.

The singleton heap predicate, written p ~~> v, characterizes a state with a single allocated cell, at location p, storing the value v.

The "separating conjunction", written H₁ \* H₂, characterizes a state that can be decomposed in two disjoint parts, one that satisfies H₁ and another that satisfies H₂. In the definition below, the two parts are named h₁ and h₂.

The existential quantifier for heap predicates, written \∃ x, H characterizes a heap that satisfies H for some x. The variable x has type A, for some arbitrary A. The notation \∃ x, H stands for hexists (fun x ⇒ H). The generalized notation \∃ x₁ ... xn, H is also available. The definition of hexists is a bit technical, and it is not essential to master it at this point. Additional explanations are provided near the end of this chapter.

Universal quantification in hprop is also possible, but it is only useful for more advanced features of Separation Logic. We postpone its introduction to chapter Wand. All the definitions above will eventually be made Opaque, after the appropriate introduction and elimination lemmas have been established, making it no longer possible to execute, say, unfold hstar. Opacity is essential to ensure that proofs do not depend on the details of the definitions.

Extensionality for Heap Predicates

To work in Separation Logic, it is extremely convenient to be able to state equalities between heap predicates. For example, we wish to establish the associativity property for the star operator in the form of an equality:

How can we prove a goal of the form H₁ = H₂ when H₁ and H₂ have type hprop, that is, heap→Prop? Intuitively, H and H' are equal if and only if they characterize exactly the same set of heaps, that is, if ∀ (h:heap), H₁ h ↔ H₂ h. This reasoning principle, a specific form of extensionality property, is not available by default in Coq. But we can safely assume it if we extend the logic of Coq with a standard axiom called "predicate extensionality".

By specializing P and Q above to the type hprop, we obtain exactly the desired extensionality principle.

More information about extensionality axioms may be found near the end of this chapter.

Statement of Fundamental Properties

By exploiting extensionality, the following properties of Separation Logic operators can be established. (1) The star operator is associative.

(2) The star operator is commutative.

(3) The empty heap predicate is a neutral element for the star. Because star is commutative, it is equivalent to state that hempty is a left or a right neutral element for hstar. We choose, arbitrarily, to state the left-neutrality property.

(4) Existentials can be "extruded" out of stars, that is: (\∃ x, J x) \* H is equivalent to \∃ x, (J x \* H).

(5) Pure facts can be extruded out stars.

Postconditions: Type, Syntax, and Extensionality

A specification takes the form triple t H Q, where t is a term, H is a precondition of type hprop, and Q is a postcondition. For example, a read at location p, written !p in OCaml, is specified as: triple <{ !p }> (p ~~> v) (fun r ⇒ (p ~~> v) \* \[r = v]). In general, a postcondition has type val → hprop, which is equivalent to val → state → Prop. The postcondition thereby capture the properties of both the output value and the output state.

One common operation is augmenting a postcondition with a description of another piece of state. This operation is written as Q \*+ H, which is just a convenient notation for fun x ⇒ (Q x \* H). We will use this operator in particular in the statement of the frame rule in the next chapter.

Intuitively, in order to prove that two postconditions Q₁ and Q₂ are equal, it suffices to show that the heap predicates Q₁ v and Q₂ v are equal for any value v. Again, the extensionality property that we need is not built into Coq. We need another axiom called "functional extensionality".

The desired equality property for postconditions follows directly from this axiom.

Introduction and Inversion Lemmas for Basic Operators

This section presents a collection of lemmas capturing the properties of the definitions of heap predicates. They include "introduction lemmas" for proving goals of the form H h, and "inversion lemmas" for extracting information from hypotheses of the form H h. These lemmas will be pervasively exploited in the next chapters for establishing reasoning rules. Hereafter, to improve readability of statements in proofs, we introduce the following notation for heap union.

The introduction lemmas show how to prove goals of the form H h, for various forms of the heap predicate H.

The tactic hnf, for "head normal form", unfolds the head constants.

The inversion lemmas show how to extract information from hypotheses of the form H h, for various forms of the heap predicate H.

More Details

Proofs of Fundamental Properties

Extraction of Existentials

Let us prove that (\∃ x, J x) \* H is equivalent to \∃ x, (J x \* H). Note that, somewhat confusingly, Coq displays none of the parentheses. You may want to use Set Printing Parentheses to more easily follow through the proof.

First, we exploit extensionality, using hprop_eq or himpl_antisym.

Then we reveal the definitions of ==>, hexists and hstar.

Neutral of Separating Conjunction

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

Prove that the empty heap predicate is a neutral element for the star. You will need to exploit the fact that the union with an empty map is the identity, as captured by lemma Fmap.union_empty_l.
  Check Fmap.union_empty_l : ∀ h,
    Fmap.empty \u h = h.

Commutativity of Separating Conjunction

We next aim to prove the commutativity of the star operator, i.e., that H₁ \* H₂ is equivalent to H₂ \* H₁. By symmetry, it suffices to prove the entailement in one direction, e.g., H₁ \* H₂ ==> H₂ \* H₁. The symmetry argument for any binary operator on heap predicates is captured by the lemma hprop_op_comm shown below.

To prove commutativity of star, we need to exploit the fact that the union of two finite maps with disjoint domains commutes. This fact is captured by a lemma coming from the finite map library.
    Check Fmap.union_comm_of_disjoint : ∀ h₁ h₂,
      Fmap.disjoint h₁ h₂ →
      h₁ \u h₂ = h₂ \u h₁. The commutativity result is then proved as follows.

Unfold the defnition of star.

Associativity of Separating Conjunction

Associativity of star is slightly more tedious to derive. We need to exploit the associativity of union on finite maps, as well as lemmas about the disjointness of a map with the result of the union of two maps.
  Check Fmap.union_assoc : ∀ h₁ h₂ h₃,
    (h₁ \u h₂) \u h₃ = h₁ \u (h₂ \u h₃).

  Check Fmap.disjoint_union_eq_l : ∀ h₁ h₂ h₃,
      Fmap.disjoint (h₂ \u h₃) h₁
    = (Fmap.disjoint h₁ h₂ ∧ Fmap.disjoint h₁ h₃).

  Check Fmap.disjoint_union_eq_r : ∀ h₁ h₂ h₃,
     Fmap.disjoint h₁ (h₂ \u h₃)
   = (Fmap.disjoint h₁ h₂ ∧ Fmap.disjoint h₁ h₃).

Exercise: 1 star, standard, optional (hstar_assoc)

Complete the right-to-left part of the proof of associativity of the star operator.

The lemma showing that hempty is a right neutral can be derived from the fact that hempty is a left neutral, and from commutativity.

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

The commutativity and associativity results combine into one result that is sometimes convenient to exploit in proofs.

Extract Pure Facts from Separating Conjunctions

The lemma hstar_hpure_l stated below explains how to extract a pure fact from an assertion. It asserts that the proposition (\[P] \* H) h is equivalent P ∧ H h. This lemma will also be pervasively used in proofs throughout the subsequent chapters.

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

Prove that a heap h satisfies \[P] \* H if and only if P is true and h it satisfies H. The proof requires two lemmas on finite maps from LibSepFmap.v:
    Check Fmap.union_empty_l : ∀ h,
      Fmap.empty \u h = h.
    Check Fmap.disjoint_empty_l : ∀ h,
      Fmap.disjoint Fmap.empty h. Note that auto can apply Fmap.disjoint_empty_l automatically. Hint: begin the proof by appyling propositional_extensionality.

Optional Material

Alternative Definitions for Heap Predicates

In what follows, we discuss alternative, equivalent definitions for the fundamental heap predicates. We write these equivalences using equalities of the form H₁ = H₂. Recall that the lemma hprop_eq enables deriving such equalities by invoking predicate extensionality. The empty heap predicate \[] is equivalent to the pure fact predicate \[True].

Thus, hempty could be defined in terms of hpure, as hpure True, written \[True].

The pure fact predicate [\P] is equivalent to the existential quantification over a proof of P in the empty heap, that is, to the heap predicate \∃ (p:P), \[].

Thus, hpure could be defined in terms of hexists and hempty, as hexists (fun (p:P) ⇒ hempty), also written \∃ (p:P), \[]. In fact, this is how hpure is defined in the rest of the course.

It is useful to minimize the number of combinators, both for elegance and to reduce proof effort. We cannot do without hexists, thus there remains a choice between considering either hpure or hempty as primitive, and the other one as derived. The predicate hempty is simpler and appears as more fundamental. Hence, in the subsequent chapters (and in the CFML tool), we define hpure in terms of hexists and hempty, as in the definition of hpure' shown above. In other words, we assume the definition:
  Definition hpure (P:Prop) : hprop :=
    \∃ (p:P), \[].

Additional Explanations for the Definition of \∃

The heap predicate \∃ (n:int), p ~~> (val_int n) characterizes a state that contains a single memory cell, at address p, storing the integer value n, for "some" (unspecified) integer n.
    Parameter (p:loc).
    Check (\∃ (n:int), p ~~> (val_int n)) : hprop. The type of \∃, which operates on hprop,is very similar to that of ∃, which operates on Prop. The key difference is that a witness for a \∃ can depend on the current heap, whereas a witness for a ∃ cannot. The notation ∃ x, P stands for ex (fun x ⇒ P), where ex has the following type:
    Check ex : ∀ A : Type, (A → Prop) → Prop. Likewise, \∃ x, H stands for hexists (fun x ⇒ H), where hexists has the following type:
    Check hexists : ∀ A : Type, (A → hprop) → hprop. The notation for \∃ is directly adapted from that of ∃, which supports the quantification an arbitrary number of variables, and is defined in Coq.Init.Logic as follows.
    Notation "'exists' x₁ .. xn , p" := (ex (fun x₁ ⇒ .. (ex (fun xn ⇒ p)) ..))
      (at level 200, x₁ binder, right associativity,
       format "'[' 'exists' '/ ' x₁ .. xn , '/ ' p ']'").

    Notation "'\exists' x₁ .. xn , H" :=
      (hexists (fun x₁ ⇒ .. (hexists (fun xn ⇒ H)) ..))
      (at level 39, x₁ binder, right associativity, H at level 50,
      format "'[' '\exists' '/ ' x₁ .. xn , '/ ' H ']'").

Formulation of the Extensionality Axioms

To establish extensionality of entailment, we have used the predicate extensionality axiom. In fact, this axiom can be derived by combining the axiom of "functional extensionality" with another one called "propositional extensionality". The axiom of "propositional extensionality" asserts that two propositions that are logically equivalent, in the sense that they imply each other, can be considered equal.

The axiom of "functional extensionality", as we saw above, asserts that two functions are equal if they provide equal result for every argument.

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

Use propositional_extensionality and functional_extensionality to derive predicate_extensionality.

Historical Notes

In this chapter, we have defined the Separation Logic operators, in particular the "separating conjunction" operator, as a Coq predicate. This formalization style is called "shallow embedding". It has been employed in the first mechanized formalizations of Separation Logic, in Coq by [Yu, Hamid, and Shao 2003], and in Isabelle/HOL by [Weber 2004]. These two formalizations were carried out soon after the invention of Separation Logic, by researcher who were used to mechanizing Hoare logic and had spotted the potential benefit of working with the separating conjunction.