This file imports LibSepDirect.v instead of Hprop.v and Himpl.v. The file LibSepDirect.v contains definitions that are essentially similar to those from Hprop.v and Himpl.v, yet with one main difference: LibSepDirect makes the definition of Separation Logic operators opaque. As a result, one cannot unfold the definition of hstar, hpure, etc. To carry out reasoning, one must use the introduction and elimination lemmas (e.g. hstar_intro, hstar_elim). These lemmas enforce abstraction: they ensure that the proofs do not depend on the particular choice of the definitions used for constructing Separation Logic.

First Pass

In the previous chapters, we have:

• introduced the key heap predicate operators,
• introduced the notion of Separation Logic triple,
• introduced the entailment relation,
• introduced the structural rules of Separation Logic.

We are now ready to present the other reasoning rules, which enable establishing properties of concrete programs. These reasoning rules are proved correct with respect to the semantics of the programming language in which the programs are expressed. Thus, a necessary preliminary step is to present the syntax and the semantics of a (toy) programming language, for which we aim to provide Separation Logic reasoning rules. The present chapter is thus organized as follows:

• definition of the syntax of the language,
• definition of the semantics of the language,
• statements of the reasoning rules associated with each of the term constructions from the language,
• specification of the primitive operations of the language, in particular those associated with memory operations,
• review of the 4 structural rules introduced in prior chapters,
• examples of practical verification proofs.

The bonus section (optional) also includes:

• proofs of the reasoning rules associated with each term construct,
• proofs of the specification of the primitive operations.

Semantic of Terms

Syntax

The syntax described next captures the "abstract syntax tree" of a programming language. It follows a presentation that distiguishes between closed values and terms. This presentation is intended to simplify the definition and evaluation of the substitution function: because values are always closed (i.e., no free variables in them), the substitution function never needs to traverse through values. The grammar for values includes unit, boolean, integers, locations, functions, recursive functions, and primitive operations. For example, val_int 3 denotes the integer value 3. The value val_fun x t denotes the function fun x ⇒ t, and the value val_fix f x t denotes the function fix f x ⇒ t, which is written let rec f x = t in f in OCaml syntax. For conciseness, we include just a few primitive operations: ref, get, set and free for manipulating the mutable state, the operation add to illustrate a simple arithmetic operation, and the operation div to illustrate a partial operation.

The grammar for terms includes values, variables, function definitions, recursive function definitions, function applications, sequences, let-bindings, and conditionals.

Note that trm_fun and trm_fix denote functions that may feature free variables, unlike val_fun and val_fix which denote closed values. The intention is that the evaluation of a trm_fun in the empty context produces a val_fun value. Likewise, a trm_fix eventually evaluates to a val_fix. Several value constructors are declared as coercions, to enable more concise statements. For example, val_loc is declared as a coercion, so that a location p of type loc can be viewed as the value val_loc p where an expression of type val is expected. Likewise, a boolean b may be viewed as the value val_bool b, and an integer n may be viewed as the value val_int n.

State

The language we consider is an imperative language, with primitive functions for manipulating the state. Thus, the statement of the evaluation rules involve a memory state. Recall from Hprop that a state is represented as a finite map from location to values. Finite maps are presented using the type fmap. Details of the construction of finite maps are beyond the scope of this course; details may be found in the the file LibSepFmap.v.

For technical reasons related to the internal representation of finite maps, to enable reading in a state, we need to justify that the grammar of values is inhabited. This property is captured by the following command, whose details are not relevant for understanding the rest of the chapter.

Substitution

The semantics of the evaluation of function is described by means of a substitution function. The substitution function, written subst y w t, replaces all occurrences of a variable y with a value w inside a term t. The substitution function is always the identity function on values, because our language only considers closed values. In other words, we define subst y w (trm_val v) = (trm_val v). The substitution function, when reaching a variable, performs a comparison between two variables. To that end, it exploits the comparison function var_eq x y, which produces a boolean value indicating whether x and y denote the same variable. "Optional contents": the remaining of this section describes further details about the substitution function that may be safely skipped over in first reading. The substitution operation traverses all other language constructs in a structural manner. It takes care of avoiding "variable capture" when traversing binders: subst y w t does not recurse below the scope of binders whose name is equal to y. For example, the result of subst y w (trm_let x t₁ t₂) is defined as trm_let x (subst y w t₁) (if var_eq x y then t₂ else (subst y w t₂)). The auxiliary function if_y_eq, which appears in the definition of subst shown below, helps performing the factorizing the relevant checks that prevent variable capture.

Implicit Types and Coercions

To improve the readability of the evaluation rules stated further, we take advantage of both implicit types and coercions. The implicit types are defined as shown below. For example, the first command indicates that variables whose name begins with the letter 'b' are, by default, variables of type bool.

We next introduce two key coercions. First, we declare trm_val as a coercion, so that, instead of writing trm_val v, we may write simply v wherever a term is expected.

Second, we declare trm_app as a "Funclass" coercion. This piece of magic enables us to write t₁ t₂ as a shorthand for trm_app t₁ t₂. The idea of associating trm_app as the "Funclass" coercion for the type trm is that if a term t₁ of type trm is applied like a function to an argument, then t₁ should be interpreted as trm_app t₁.

Interestingly, the "Funclass" coercion for trm_app can be iterated. The expression t₁ t₂ t₃ is parsed by Coq as (t₁ t₂) t₃. The first application t₁ t₂ is interpreted as trm_app t₁ t₂. This expression, which itself has type trm, is applied to t₃. Hence, it is interpreted as trm_app (trm_app t₁ t₂) t₃, which indeed corresponds to a function applied to two arguments.

Big-Step Semantics

The semantics is presented in big-step style. This presentation makes it slightly easier to establish reasoning rules than with small-step reduction rules, because both the big-step judgment and a triple judgment describe complete execution, relating a term with the value that it produces. The big-step evaluation judgment, written eval s t s' v, asserts that, starting from state s, the evaluation of the term t terminates in a state s', producing an output value v. For simplicity, we assume terms to be in "A-normal form": the arguments of applications and of conditionals are restricted to variables and values. Such a requirement does not limit expressiveness, yet it simplifies the statement of the evaluation rules. For example, if a source program includes a conditional trm_if t₀ t₁ t₂, then it is required that t₀ be either a variable or a value. This is not a real restriction, because trm_if t₀ t₁ t₂ can always be encoded as let x = t₀ in if x then t₁ else t₂. The big-step judgment is inductively defined as follows.

1. eval for values and function definitions. A value evaluates to itself. A term function evaluates to a value function. Likewise for a recursive function.

2. eval for function applications. The beta reduction rule asserts that (val_fun x t₁) v₂ evaluates to the same result as subst x v₂ t₁. In the recursive case, (val_fix f x t₁) v₂ evaluates to subst x v₂ (subst f v₁ t₁), where v₁ denotes the recursive function itself, that is, val_fix f x t₁.

3. eval for structural constructs. A sequence trm_seq t₁ t₂ first evaluates t₁, taking the state from s₁ to s₂, drops the result of t₁, then evaluates t₂, taking the state from s₂ to s₃. The let-binding trm_let x t₁ t₂ is similar, except that the variable x gets substituted for the result of t₁ inside t₂.

4. eval for conditionals. A conditional in a source program is assumed to be of the form if t₀ then t₁ else t₂, where t₀ is either a variable or a value. If it is a variable, then by the time it reaches an evaluation position, the variable must have been substituted by a value. Thus, the evaluation rule only considers the form if v₀ then t₁ else t₂. The value v₀ must be a boolean value, otherwise evaluation gets stuck. The term trm_if (val_bool true) t₁ t₂ behaves like t₁, whereas the term trm_if (val_bool false) t₁ t₂ behaves like t₂. This behavior is described by a single rule, leveraging Coq's "if" constructor to factor out the two cases.

5. eval for primitive stateless operations. For similar reasons as explained above, the behavior of applied primitive functions only need to be described for the case of value arguments. An arithmetic operation expects integer arguments. The addition of val_int n₁ and val_int n₂ produces val_int (n₁ + n₂). The division operation, on the same arguments, produces the quotient n₁ / n₂, under the assumption that the dividor n₂ is non-zero. In other words, if a program performs a division by zero, then it cannot satisfy the eval judgment.

6. eval for primitive operations on memory. There remains to describe operations that act on the mutable store. val_ref v allocates a fresh cell with contents v. The operation returns the location, written p, of the new cell. This location must not be previously in the domain of the store s. val_get (val_loc p) reads the value in the store s at location p. The location must be bound to a value in the store, else evaluation is stuck. val_set (val_loc p) v updates the store at a location p assumed to be bound in the store s. The operation modifies the store and returns the unit value. val_free (val_loc p) deallocates the cell at location p.

Loading of Definitions from Direct

Throughout the rest of this file, we rely not on the definitions shown above, but on the definitions from LibSepDirect.v. The latter are slightly more general, yet completely equivalent to the ones presented above for the purpose of establishing the reasoning rules that we are interested in. To reduce the clutter in the statement of lemmas, we associate default types to a number of common meta-variables.

Review of the Structural Rules

Let us review the essential structural rules, which were introduced in the previous chapters. These structural rules are involved in the practical verification proofs carried out further in this chapter. The frame rule asserts that the precondition and the postcondition can be extended together by an arbitrary heap predicate. Recall that the definition of triple was set up precisely to validate this frame rule, so in a sense in holds "by construction".

The consequence rule allows to strengthen the precondition and weaken the postcondition.

In practice, it is most convenient to exploit a rule that combines both frame and consequence into a single rule, as stated next. (Note that this "combined structural rule" was proved as an exercise in chapter Himpl.)

The two extraction rules enable to extract pure facts and existentially quantified variables, from the precondition into the Coq context.

Exercise: 1 star, standard, optional (triple_hpure')

The extraction rule triple_hpure assumes a precondition of the form \[P] \* H. The variant rule triple_hpure', stated below, assumes instead a precondition with only the pure part, i.e., of the form \[P]. Prove that triple_hpure' is indeed a corollary of triple_hpure.

Rules for Terms

We next present reasoning rule for terms. Most of these Separation Logic rules have a statement essentially identical to the statement of the corresponding Hoare Logic rule. The main difference lies in their interpretation: whereas Hoare Logic pre- and post-conditions describe the full state, a Separation Logic rule describes only a fraction of the mutable state.

Reasoning Rule for Sequences

Let us begin with the reasoning rule for sequences. The Separation Logic reasoning rule for a sequence t₁;t₂ is essentially the same as that from Hoare logic. The rule is:

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

The Coq statement corresponding to the above rule is:

The variable v denotes the result of the evaluation of t₁. For well-typed programs, this result would always be val_unit. Yet, because we here consider an untyped language, we do not bother adding the constraint v = val_unit. Instead, we simply treat the result of t₁ as a value irrelevant to the remaining of the evaluation.

Reasoning Rule for Let-Bindings

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

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

Yet, such a presentation makes a confusion between the x that denotes a program variable in let x = t₁ in t₂, and the x that denotes a value when quantified as ∀ x. 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 as follows.

Reasoning Rule for 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 appears next.

Note that the two premises may be factorized into a single one using Coq's conditional construct. Such an alternative statement is discussed further in this chapter.

Reasoning Rule for Values

The rule for 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]}

It is however more convenient in practice to work with a judgment whose conclusion is of the form {H} v {Q}, for an arbitrary H and Q. For this reason, we prefer the following rule for values.

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

It may not be completely obvious at first sight why this alternative rule is equivalent to the former. We prove the equivalence further in this chapter. The Coq statement of the rule for values is thus as follows.

Let us prove that the "minimalistic" rule {\[]} v {fun r ⇒ \[r = v]} is equivalent to triple_val.

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

Prove that the alternative rule for values 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. Hint: you will need to exploit the structural rule triple_conseq_frame.

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. Hint: you'll need to guess the intermediate postcondition Q₁ associated with the let-binding rule, and exploit the appropriate structural rules.

Reasoning Rule for Functions

In addition to the reasoning rule for values, we need reasoning rules for functions and recursive functions that appear as terms in the source program (as opposed to appearing as values). A function definition trm_fun x t₁, expressed as a subterm in a program, evaluates to a value, more precisely to val_fun x t₁. Again, we could consider a rule with an empty precondition:

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

However, we prefer a conclusion of the form {H} (trm_fun x t₁) {Q}. We thus consider the following rule, very similar to triple_val.

The rule for recursive functions is similar. It is presented further in the file. Last but not least, we need a reasoning rule to reason about a function application. 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}

The corresponding Coq statement is as shown below.

The generalization to the application of recursive functions is straightforward. It is discussed further in this chapter.

Specification of Primitive Operations

Before we can tackle verification of actual programs, there remains to present the specifications for the primitive operations. Let us begin with basic arithmetic operations: addition and division.

Specification of Arithmetic Primitive Operations

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₂). Indeed, recall that val_int is declared as a coercion. The addition operation may execute in an empty state. It does not modify the state, and returns the value val_int (n₁+n₂). 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₂).

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 is a pure fact, which can be asserted as part of the precondition, as follows.

Equivalently, the requirement n₂ ≠ 0 may be asserted as an hypothesis to the front of the triple judgment, in the form of a standard Coq hypothesis, as shown below.

This latter presentation with pure facts such as n₂ ≠ 0 placed to the front of the triple turns out to be more practical to exploit in proofs. Hence, we always follow this style of presentation, and reserve the precondition for describing pieces of mutable state.

Specification of Primitive Operations Acting on Memory

There remains to describe the specification of operations on the heap. Recall that val_get denotes the operation for reading a memory cell. A call of the form val_get v' executes safely if v' is 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.

Remark: val_loc is registered as a coercion, so val_get (val_loc p) could be written simply as val_get p, where p has type loc. We here chose to write val_loc explicitly for clarity. 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.

Recall that val_ref denotes the operation for allocating a cell with a given contents. A call to val_ref v does not depend on the contents of the existing state. It extends the state with a fresh singleton cell, at some location p, assigning it v as contents. The fresh cell is then 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.

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 p ~~> v. The operation leaves an empty state, and asserts that the return value, named r, is equal to unit.

Verification Proof in Separation Logic

We have at hand all the necessary rules for carrying out actual verification proofs in Separation Logic. Let's do it!

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 Recall that, for simplicity, we assume programs to be written in "A-normal form", that is, with all intermediate expressions named by a let-binding. Thereafter, we thus consider the following definition for the incr.    let incr p =
      let n = !p in
      let m = n+1 in
      p := m Using the construct from our toy programming language, the definition of incr is written as shown below.

Alternatively, using notation and coercions, the same program can be written as shown below.

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

We next show a detailed proof for this specification. It exploits:

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

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. Hint: use applys triple_seq for reasoning about a sequence. Hint: use applys triple_val for reasoning about the final return value, namely x.

Proof of factorec

Recall from Basic the function repeat_incr.     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. Hint: triple_hpure', the corollary of triple_hpure, is helpful. Hint: exploit triple_le and triple_sub and triple_mul to reason about the behavior of the primitive operations involved. Hint: 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.

What's Next

The matter of the next chapter is to introduce additional technology to streamline the proof process, notably by:

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

The rest of this chapter is concerned with alternative statements for the reasoning rules, and with the proofs of the reasoning rules.

More Details

Alternative Specification Style for Pure Preconditions

Recall the specification for division.

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

Let us formally prove that the two presentations are equivalent. Frist, we prove triple_div' by exploiting triple_div.

Exercise: 1 star, standard, especially useful (triple_div_from_triple_div')

Prove triple_div by exploiting triple_div'. Hint: the key proof step is applys triple_conseq

As we said, 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.

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. Yet, t₁ may well require only a subset of the state H to evaluate, and not all of H. 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.

Proofs for the Rules for Terms

The proofs for the Separation Logic reasoning rules all follow a similar pattern: first establish a corresponding rule for Hoare triples, then generalize it to a Separation Logic triple. To establish a reasoning rule w.r.t. a Hoare triple, we reveal the definition expressed in terms of the big-step semantics.
      Definition hoare (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
        ∀ s, H s →
        ∃ s' v, eval s t s' v ∧ Q v s'. Concretely, we consider a given initial state s satisfying the precondition, and we have to provide witnesses for the output value v and output state s' such that the reduction holds and the postcondition holds. Then, to lift the reasoning rule from Hoare logic to Separation Logic, we reveal the definition of a Separation Logic triple.
      Definition triple t H Q :=
       ∀ H', hoare t (H \* H') (Q \*+ H'). Recall that we already employed this two-step scheme in the previous chapter, e.g., to establish the consequence rule (rule_conseq).

Proof of triple_val

The big-step evaluation rule for values asserts that a value v evaluates to itself, without modification to the current state s.

The Hoare version of the reasoning rule for values is as follows.

1. We unfold the definition of hoare.

2. We provide the witnesses for the output value and heap. These witnesses are dictated by the statement of eval_val.

3. We invoke the big-step rule eval_val

4. We establish the postcondition, exploiting the entailment hypothesis.

The Separation Logic version of the rule then follows.

1. We unfold the definition of triple to reveal a hoare judgment.

2. We invoke the reasoning rule hoare_val that was just established.

3. We exploit the assumption and conclude using xchange.

Proof of triple_seq

The big-step evaluation rule for a sequence is given next.

The Hoare triple version of the reasoning rule is proved as follows. This lemma, called hoare_seq, has the same statement as triple_seq, except with occurrences of triple replaced with hoare.

1. We unfold the definition of hoare. Let K₀ describe the initial state.

2. We exploit the first hypothesis to obtain information about the evaluation of the first subterm t₁. The state before t₁ executes is described by K₀. The state after t₁ executes is described by K₁.

3. We exploit the second hypothesis to obtain information about the evaluation of the first subterm t₂. The state before t₂ executes is described by K₁. The state after t₂ executes is described by K₂.

4. We provide witness for the output value and heap. They correspond to those produced by the evaluation of t₂.

5. We invoke the big-step rule.

6. We establish the final postcondition, which is directly inherited from the reasoning on t₂.

The Separation Logic reasoning rule is proved as follows.

1. We unfold the definition of triple to reveal a hoare judgment.

2. We invoke the reasoning rule hoare_seq that we just established.

3. For the hypothesis on the first subterm t₁, we can invoke directly our first hypothesis.

4. Likewise, we invoke an induction hypothesis for t₂.

Proof of triple_let

Recall the big-step evaluation rule for a let-binding.

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

Following the same proof scheme as for triple_seq, establish the reasoning rule for triple_let, whose statement appears earlier in this file. Make sure to first state and prove the lemma hoare_let, which has the same statement as triple_let yet with occurrences of triple replaced with hoare.

Proofs for the Arithmetic Primitive Operations

Addition

Recall the evaluation rule for addition.

In the proof, we will need to use the following result, established in the first chapter.

As usual, we first establish a Hoare triple.

Deriving triple_add is then straightforward.

Division

Recall the evaluation rule for division.

Exercise: 3 stars, standard, optional (triple_div)

Following the same proof scheme as for triple_add, establish the reasoning rule for triple_div. Make sure to first state and prove hoare_div, which is similar to triple_div, except with hoare instead of triple, and with a precondition named H for describing the input state.

Proofs for Primitive Operations Operating on the State

The proofs for establishing the Separation Logic reasoning rules for ref, get and set follow a similar proof pattern, that is, they go through the proofs of rules for Hoare triples. Unlike before, however, the Hoare triples are not directly established with respect to the big-step evaluation rules. Instead, we start by proving corollaries to the big-step rules to reformulate them in a way that give already them a flavor of "Separation Logic". Concretely, we reformulate the evaluation rules, which are expressed in terms of read and updates in finite maps, to be expressed instead entirely in terms of disjoint unions. The introduction of these disjoint union operations then significantly eases the justification of the separating conjunctions that appear in the targeted Separation Logic triples. In this section, the constructor hval_val appears. This constructor converts a "value" into a "heap value". For the purpose, of this file, the two notion are identical. Yet, to allow for generalization to the semantics of allocation by blocks, we need to assume that states are finite maps from location to heap values. Heap values, of type hval, can be assumed to be defined by the following inductive data type.
    Inductive hval : Type :=
      | hval_val : val → hval.

Read in a Reference

The big-step rule for get p requires that p be in the domain of the current state s, and asserts that the output value is the result of reading in s at location p.

We reformulate this rule by isolating from the current state s the singleton heap made of the cell at location p, and let s₂ denote the rest of the heap. When the singleton heap is described as Fmap.single p v, then v is the result value returned by get p.

The proof of this lemma is of little interest. We show it only to demonstrate that it relies only a few basic facts related to finite maps.

Our goal is to establish the triple:
    triple (val_get p)
      (p ~~> v)
      (fun r ⇒ \[r = v] \* (p ~~> v)). Establishing this lemma requires us to reason about propositions of the form (\[P] \* H) h and (p ~~> v) h. To that end, recall lemma hstar_hpure_l, which was already exploited in the proof of triple_add, and recall hsingle_inv from Hprop.

We establish the specification of get first w.r.t. to the hoare judgment.

Deriving the Separation Logic triple follows the usual pattern.

Allocation of a Reference

Next, we consider the reasoning rule for operation ref, which involves a proof yet slightly more trickier than that for get and set. The big-step evaluation rule for ref v extends the initial state s with an extra binding from p to v, for some fresh location p.

Let us reformulate eval_ref to replace references to Fmap.indom and Fmap.update with references to Fmap.single and Fmap.disjoint. Concretely, ref v extends the state from s₁ to s₁ \u s₂, where s₂ denotes the singleton heap Fmap.single p v, and with the requirement that Fmap.disjoint s₂ s₁, to capture freshness.

It is not needed to follow through this proof.

In order to apply the rules eval_ref or eval_ref_sep, we need to be able to synthetize fresh locations. The following lemma (from LibSepFmap.v) captures the existence, for any state s, of a (non-null) location p not already bound in s.

We reformulate the lemma above in a way that better matches the premise of the lemma eval_ref_sep, which we need to apply for establishing the specification of ref. This reformulation, shown below, asserts that, for any h, there existence a non-null location p such that the singleton heap Fmap.single p v is disjoint from h.

It is not needed to follow through this proof.

The proof of the Hoare triple for ref is as follows.

We then derive the Separation Logic triple as usual.

Optional Material

Reasoning Rules for Recursive Functions

This reasoning rules for functions immediately 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₁.

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.

Other Proofs of Reasoning Rules for Terms

Proof of triple_fun and triple_fix

The proofs for triple_fun and triple_fix are essentially identical to that of triple_val, so we do not include them here.

Proof of triple_if

Recall the reasoning rule for conditionals. Recall that this rule is stated by factorizing the premises.

The reasoning rule for conditional w.r.t. Hoare triples is as follows.

The corresponding Separation Logic reasoning rule is as follows.