First Pass

This chapter establishes the remaining reasoning rules of Separation Logic: rules for reasoning about each language construct, and rules for reasoning about primitive operations. All these reasoning rules are expressed using the predicate triple, and are proved with respect to the formal semantics captured by the predicate eval introduced in the previous chapter (Triples). Throughout the chapter, one needs to have in mind the definition of triple:
    Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
      ∀ s, H s → eval s t Q. After establishing the reasoning rules, we present an example proof of a concrete program, using directly these reasoning rules, as opposed to using high-level "x-tactics" as in the first two chapters. This example proof reveals the proof patterns employed by the x-tactics. It also motivates the introduction of the x-tactics to avoid the tedious, repetitive proof patterns.

Rules for Term Constructors

Sequences

The Separation Logic reasoning rule for a sequence t₁;t₂ is essentially the same as that from Hoare logic. In the rule shown below, the underscore symbol indicates that the output value produced by t₁ is irrelevant to the semantics, as captured by the rule eval_seq.

{H} t1 {fun _ => H1}     {H1} t2 {Q}
{H} (t1;t2) {Q}

The Coq statement corresponding to the above rule is:

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

Prove triple_seq by unfolding triple and using eval_seq.

Let-Bindings

Next, we present the reasoning rule for let-bindings. Here again, there is nothing specific to Separation Logic: the rule is exactly the same as in Hoare Logic. The rule for a let-binding let x = t₁ in t₂ could be stated, informally, in the form:

{H} t1 {Q1}     (forall x, {Q1 x} t2 {Q})
{H} (let x = t1 in t2) {Q}

However, this presentation confuses the x that denotes a program variable in let x = t₁ in t₂, and the x that denotes a universally quantified Coq value. The correct statement involves a substitution from the variable x to a value quantified as ∀ (v:val).

{H} t1 {Q1}     (forall v, {Q1 v} (subst x v t2) {Q})
{H} (let x = t1 in t2) {Q}

The corresponding Coq statement is thus.

When we carry out proofs in practice, the application of the rule triple_let produces a second sub-goal of the form, e.g.: ∀ v₁, triple (subst "a" v₁ rest_of_the_program) (post1 v₁) post2, where "a" denotes the name of the program variable that was bound by the let-binding in the original source code. At this point, the user would typically type intros a, to introduce the Coq variable v₁ under the same name that it had in the source code. This operations produces: triple (subst "a" a rest_of_the_program) (post1 a) post2. At that point, the user may call simpl to effectively replace all occurences of the program variable "a" with the Coq variable a of type val. Doing so produces: triple rest_of_the_program_updated (post1 a) post2, where rest_of_the_program_updated refers to the Coq variable a. This process will be illustrated in the proof of triple_incr further on.

Conditionals

The rule for a conditional is, again, exactly like in Hoare logic.

b = true -> {H} t1 {Q}     b = false -> {H} t2 {Q}
{H} (if b then t1 in t2) {Q}

The corresponding Coq statement is:

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

Prove triple_if_case by unfolding triple and using eval_if. Hint: use the tactic case_if to perform a case analysis.

The two premises of the rule for if-statements may be factorized into a single one using Coq's conditional construct, as in eval_if.

Values

The triple specifying the behavior of a value v can be written as a triple with an empty precondition and a postcondition asserting that the result value r is equal to v, in the empty heap. Formally:

{\[]} v {fun r => \[r = v]}

In practice, however, it is more convenient to work with a judgment whose conclusion has the form {H} v {Q}, for an arbitrary precondition H and postcondition Q.

H ==> Q v
{H} v {Q}

The Coq statement of the rule for values is thus as follows.

It may not be obvious at first sight why triple_val is equivalent to the "minimalistic" rule {\[]} v {fun r ⇒ \[r = v]}. Let us prove the equivalence.

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

Prove that the first rule for values is derivable from triple_val. Hint: use the tactic xsimpl to conclude the proof.

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

More interestingly, prove that triple_val is derivable from triple_val_minimal. Concretely, your goal is to prove triple_val' without unfolding the definition of triple. Use triple_conseq_frame, triple_val_minimal, and xsimpl.

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

Consider a term of the form let x = v₁ in t₂, that is, where the argument of the let-binding is already a value. State and prove a reasoning rule of the form:
      Lemma triple_let_val : ∀ x v₁ t₂ H Q,
        ... →
        triple (trm_let x v₁ t₂) H Q.

Function Definitions

Recall from the previous chapter the distinction between val_fun x t₁, which denotes a closed value, and trm_fun x t₁, which corresponds to a term that may contain free variables. By the time the evaluation of a program reaches a trm_fun, all its free variables should have been substituted by values. At this point, the rule eval_fun reduces the trm_fun into a val_fun. We need a rule in the program logic to mimic this transition from trm_fun to val_fun. We have two ways to state this rule, similar to the two ways of stating the rule for reasoning about values. The first possibility is to consider a rule with an empty precondition.

{\[]} (trm_fun x t1) {fun r => \[r = val_fun x t1]}

The second possibility, which leads to a more practical rule, features a conclusion of the form {H} (trm_fun x t₁) {Q}, with H and Q unconstrained. The resulting rule, triple_fun is structured similarly to triple_val.

This reasoning rules for functions generalizes to recursive functions. A term describing a recursive function is written trm_fix f x t₁, and the corresponding value is written val_fix f x t₁.

Function Calls

Last but not least, we need a reasoning rule to reason about function applications. Consider an application trm_app v₁ v₂. Assume v₁ to be a function, that is, to be of the form val_fun x t₁. Then, according to the beta-reduction rule, the semantics of trm_app v₁ v₂ is the same as that of subst x v₂ t₁. This reasoning rule is thus:

v1 = val_fun x t1     {H} (subst x v2 t1) {Q}
{H} (trm_app v1 v2) {Q}

Observe that this reasoning rule requires v₁ to be a known value. In particular, v₁ cannot be a program variable or an unspecified program value. More precisely:

• If v₁ was a program variable (that is, a trm_var) in the original source code, then this program variable should have been substituted by a Coq value or variable of type val by the time we reach this function call. Otherwise, the variable would correspond to a dangling free variable.
• If v₁ is a Coq variable of type val but with no assumption of the form v₁ = val_fun x t₁, it is probably the case that we already have established a specification lemma for the function v₁ earlier in the reasoning. It this case, the rule above generally cannot be applied. Instead, one should apply the specification lemma for v₁, which is expected to have a conclusion of the form {..} (trm_app v₁ ..) {..}, matching the proof obligation at hand.

Let's come back to the case where we are interested in establishing a triple for a concrete function, whose code is known. The reasoning rule stated above translates in Coq as shown below.

The reasoning rule that corresponds to beta-reduction for a recursive function involves two substitutions: a first substitution for recursive occurrences of the function, followed with a second substitution for the argument provided to the call.

This concludes the presentation of the reasoning rules for term constructs. Before we can tackle the verification of actual programs, there remains to present the specifications for the primitive operations. We start with arithmetic operations, then consider heap-manipulating operations.

Primitive Arithmetic Operations

Addition

Consider a term of the form val_add n₁ n₂, which is short for trm_app (trm_app (trm_val val_add) (val_int n₁)) (val_int n₂), if we unfold the coercion val_int. The addition operation may execute in an empty state. It does not modify the state, and returns the value val_int (n₁+n₂). Recall the statement of the evaluation rule, in omni-big-step style.

In the specification shown below, the precondition is written \[] and the postcondition binds a return value r of type val specified to be equal to val_int (n₁+n₂).

Technically, for a simple function such as addition, we could state a specification in a similar form as triple_val, with an entailment of the form H ==> Q v, as shown below.

Yet, this pattern does not generalize well to more complex functions with nonempty preconditions. Instead, for specifying functions, we follow by convention the pattern of "minimal footprint specifications", where the precondition of the function covers no more than what the function needs to access. For example:

• the add operation does not access the memory state, so it should be specified with \[] as precondition;
• the get operation on a reference accesses exactly one cell, so it should be specified using a precondition of the form p ~~> v;
• the mlist_length operation traverses one mutable linked list, so it should be specified using a precondition of the form MList p L.

There are a few situations where the precondition of a function may be an over-approximation, to avoid complications. For example, a function that gives the index of the first occurrence of a value v in a mutable list at address p would typically be specified with a precondition of the form MList p L describing the full linked list, rather than a precondition describing the the smallest prefix of the list that reaches a cell with value v.

Division

The specification of the division operation val_div n₁ n₂ is similar, yet with the extra requirement that the argument n₂ must be nonzero. This requirement n₂ ≠ 0 appears in the evaluation rule as well as in the reasoning rule.

Random-Number Generation

The evaluation of val_rand n is particularly interesting because it involves nondeterminism. Assume n > 0. The output value may be any n₁ in the range 0 ≤ n₁ < n. The statement eval s (val_rand n) Q should capture the fact that Q s n₁ holds, for any possible output integer n₁. This condition is captured by ∀ n₁, 0 ≤ n₁ < n → Q n₁ s.

The postcondition of the triple for val_rand n asserts that the output value r corresponds to an integer n₁ in the range 0 ≤ n₁ < n.

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

Prove the reasoning rule for calls to the random number generator.

Primitive Heap-Manipulating Operations

Establishing triples for the operations ref, get, set and free requires reasoning about the definitions of certain primitive heap predicates. This reasoning is carried out using the introduction and elimination lemmas introduced in chapter Hprop. For example, hsingle_intro proves (p ~~> v) (Fmap.single p v). Also, the lemma hstar_hpure_l establishing (\[P] \* H) h = (P ∧ H h) will be used pervasively.

Allocation

Recall that val_ref v allocates a cell with contents v. A call to val_ref v does not depend on the current contents of the state. The operation extends the state with a fresh singleton cell, at some location p, assigning it v as contents. This fresh cell is described by the heap predicate p ~~> v. The evaluation of val_ref v produces the value val_loc p. Thus, if r denotes the result value, we have r = val_loc p for some p. In the corresponding specification shown below, observe how the location p is existentially quantified in the postcondition.

Using the notation funloc p ⇒ H as a shorthand for fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* H, the specification for val_ref becomes more concise.

Deallocation

Recall that val_free denotes the operation for deallocating a cell at a given address. A call of the form val_free p executes safely in a state described by p ~~> v. The operation leaves an empty state, and asserts that the return value, named r, is equal to unit.

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

Prove the reasoning rule for deallocation of a single cell. Hint: use Fmap.indom_single and Fmap.remove_single.

In practice, the information r = val_unit is generally useless. Thus, we state triple_free with an empty postcondition.

Read

Recall that val_get denotes the operation for reading a memory cell. A call of the form val_get v' executes safely if its argument v' is a value of the form val_loc p for some location p, in a state that features a memory cell at location p, storing some contents v. Such a state is described as p ~~> v. The read operation returns a value r such that r = v, and the memory state of the operation remains unchanged. The specification of val_get is thus expressed as follows.

Write

Recall that val_set denotes the operation for writing a memory cell. A call of the form val_set v' w executes safely if v' is of the form val_loc p for some location p, in a state p ~~> v. The write operation updates this state to p ~~> w, and returns the unit value, which can be ignored. Hence, val_set is specified as follows.

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

Prove the reasoning rule for a write operation. Hint: use Fmap.update_single.

Program Verification using the Reasoning Rules

We now have at hand all the necessary rules for carrying out actual verification proofs in Separation Logic.

Proof of incr

First, we consider the verification of the increment function, which is written in OCaml syntax as:    let incr p =
      p := !p + 1 and in "A-normal form" as:    let incr p =
      let n = !p in
      let m = n+1 in
      p := m Using the construct from our embedded programming language, the definition of incr is formalized as shown below.

Alternatively, using notation and coercions, the same program can be written more concisely.

Let us check that the two definitions are indeed the same.

Recall from the first chapter the specification of the increment function. Its precondition requires a singleton state of the form p ~~> n. Its postcondition describes a state of the form p ~~> (n+1).

In chapter Basic, we have seen that the proof of this lemma can be completed by the short script xwp. xapp. xapp. xapp. xsimpl.. The purpose of the detailed proof that follows is to explain how the x-tactics operate. It shows how, under the hood, the proof exploits:

• the structural reasoning rules,
• the reasoning rules for terms,
• the specification of the primitive functions,
• the xsimpl tactic for simplifying entailments.

Executing the proof script step by step leads to the display of intermediate proof obligations that involve Coq existential variables, a.k.a. "evars", whose name is prefixed by a question mark, e.g., "?x". These placeholders are typically introduced by applys (which calls eapply), and are typically instantiated when solving subgoals.

Initialize the proof

Provide the argument name and body for incr.

Compute the substitution from program variable "p" to Coq variable p

Reason about let n = ... Observe that this introduces an evar ?Q₁, which denotes the postcondition of !p.

In the body of the let-binding, reason about !p. Here we are in a favorable situation, where there is no need to apply a consequence or frame rule.

Observe how ?Q₁ has been instantiated as fun r ⇒ \[r = n] \* p ~~> n. We next introduce a name n' for the result of !p

Once again, we compute the substitution of a program variable.

We substitute away the equality n' = n.

Reason about let m = ... Observe the introduction of another evar ?Q₁.

Apply the frame rule to put aside p ~~> n.

We reason about n+1 in the empty state. Doing so instantiates ?Q₁.

We name m' the result of n+1.

We can extract the equality m' = n + 1 and substitute it away.

Finally, we reason about p := m.

Proof of succ_using_incr

Recall from Basic the function succ_using_incr.

Recall the specification of succ_using_incr.

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

Verify the function triple_succ_using_incr. Hint: follow the pattern of triple_incr. Use applys triple_seq for reasoning about a sequence. Use applys triple_val for reasoning about the final return value, namely x.

The job of the following chapters is to introduce additional technology to streamline the proof process, notably by:

• automating the application of the frame rule, and
• eliminating the need to manipulate program variables and substitutions during verification.

More Details

This "More Details" section presents several additional reasoning rules.

Triple for Terms with Same Semantics

A general principle is that if, according to the semantics, the terms t₁ and t₂ admit the same behaviors, then t₁ and t₂ satisfy the same triples. The statement can also be reformulated in an asymmetric fashion: if t₂ admits no more behaviors than t₁, then t₂ satisfies all the triples that t₁ satisfies. This section explains how to formalize this asymmetric statement, which is more general and more useful in practice. The judgment eval_like t₁ t₂ asserts that if t₁ terminates and produces results in Q, then so does t₂.

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

Prove that when the relation eval_like t₁ t₂ holds, any triple that t₂ satisfies any triple that t₁ satisfies.

The remaining of this section presents 4 examples applications of this reasoning principle. To begin with, consider the term let x = t in x, represented as trm_let x t x for a variable named x. This term reduces to t, hence the relation eval_like t (trm_let x t x) holds.

Exercise: 4 stars, standard, optional (eval_like_eta_expansion)

Prove that the symmetric relation eval_like (trm_let x t x) t also holds.

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

Conclude that t and trm_let x t x satisfy exactly the same set of triples. (This result will be exploited in chapter Affine, for proving the equivalence of two versions of the garbage collection rule.)

Another application of the reasoning rule triple_eval_like is to revisit the proof of triple_app_fun by arguing that trm_app (val_fun x t₁) v₂ reduces to subst x v₂ t₁, hence they admit the same behavior.

A even more interesting application is a rule that allows to modify the parenthesis structure of a sequence, from t₁; (t₂; t₃) to (t₁;t₂); t₃. Such a change in the parenthesis structure of a sequence might be helfpul to apply the frame rule around t₁;t₂, for example.

Exercise: 3 stars, standard, optional (triple_trm_seq_assoc)

Prove that the term t₁; (t₂; t₃), which corresponds to the natural parsing of t₁; t₂; t₃, satisfies any triple that the term (t₁;t₂); t₃ satisfies.

The Combined Let-Frame Rule

Recall the Separation Logic let rule.

At first sight, it seems that, to reason about let x = t₁ in t₂ in a state described by precondition H, we need to first reason about t₁ in that same state. But t₁ may well require only a subset of the state H to evaluate. The "let-frame" rule combines the rule for let-bindings with the frame rule to make it more explicit that the precondition H may be decomposed in the form H₁ \* H₂, where H₁ is the part needed by t₁, and H₂ denotes the rest of the state. The part of the state covered by H₂ remains unmodified during the evaluation of t₁, and appears as part of the precondition of t₂. The corresponding statement is as follows.

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

Prove the let-frame rule.

Optional Material

Alternative Specification Style for Pure Preconditions

Recall the specification for division.

Equivalently, we could place the requirement n₂ ≠ 0 in the precondition:

The two presentations are equivalent. First, let us prove triple_div' using triple_div.

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

Prove triple_div using triple_div'.

Placing pure preconditions outside of the triples makes it slightly more convenient to exploit specifications. For this reason, we adopt the style that precondition only contain the description of heap-allocated data structures.

Alternative Specification Style for Result Values

Recall the specification for the function ref.

Its postcondition could be equivalently stated by using, instead of an existential quantifier, a pattern matching construct.

However, the pattern-matching presentation is less readable and would be fairly cumbersome to work with in practice.

Proof of factorec

This section presents a manual proof for a recursive function.

In this section, the corollary triple_hpure' established in the previous chapter, can be useful.

Recall the function repeat_incr from chapter Basic.     let rec factorec n =
      if n ≤ 1 then 1 else n * factorec (n-1)

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

Verify the function factorec. Hint: exploit triple_app_fix for reasoning about the recursive function. Use triple_hpure', the corollary of triple_hpure. Exploit triple_le and triple_sub and triple_mul to reason about the behavior of the primitive operations involved. Exploit applys triple_if. case_if as C. to reason about the conditional; alternatively, if using triple_if_case, you'll need to use the tactic rew_bool_eq in * to simplify, e.g., the expression isTrue (m ≤ 1)) = true.

Historical Notes

[Gordon 1989] gave the first mechanization of Hoare logic in a proof assistant, using the HOL tool. Gordon's pioneering work was followed by numerous formalizations of Hoare logic, targeting various programming languages. The original presentation of Separation Logic (1999-2001) consists of a set of rules written down on paper. These rules were not formally described in a proof assistant. Nevertheless, mechanized presentation of Separation Logic emerged a few years later. [Yu, Hamid, and Shao 2003] present the CAP framework for the verification in Coq of assembly-level code. This framework exploits separation logic style specifications, with predicate for lists and list segments involving the separating conjunction operator. In parallel, [Weber 2004], advised by Nipkow, developed the first mechanization of the rules of Separation Logic for a while language, using the Isabelle/HOL tool. His presentation is quite close from the original, paper presentation. Numerous mechanized presentations of Separation Logic, targeting various languages (assembly, C, core-Java, ML, etc.) and using various tools (Isabelle/HOL, Coq, PVS, HOL4, HOL). For a detailed list, see the last chapter of the companion notes, linked from the Preface.