The file LibSepReference.v contains definitions that are essentially similar to those from Hprop.v and Himpl.v, yet with one main difference: LibSepReference makes the definition of Separation Logic operators opaque. This chapter and the following ones import LibSepReference.v instead of Hprop.v and Himpl.v. As a result, one cannot unfold the definition of hstar, hpure, etc. To carry out reasoning, one must use the introduction and elimination lemmas, such as hstar_intro and 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 chapter Hprop, we have formalized heap predicates, of type hprop , and operators on them: \[], \[P], p ~~> v, H₁ \* H₂, Q₁ \*+ H₂, and \∃ x, H. In chapter Himpl, we have formalized the heap entailment relations, written H₁ ==> H₂ and Q₁ ===> Q₂. The goal of the present chapter and the next one is to formalize the definition of triples, written triple t H Q, and the reasoning rules of Separation Logic. More precisely, the present chapter focuses on the definition of triples and the proof of the "structural rules", which are essential in particular for implementing the tactics xpull and xapp used in the first two chapters. The structural rules include the "frame rule", which is at the heart of Separation Logic, as well as the "consequence rule" and two "extraction rules", which admit similar statements as in Hoare Logic. The reasoning rules concerned with term constructs are discussed in the next chapter (Rules). The chapter starts with a formalization of the syntax and the semantics of the programming language. The semantics is axiomatized using a variant of the big-step semantics called the "omni-big-step semantics". This presentation is well suited for capturing safety and termination in nondeterministic programming languages. Near the end of the chapter, we explain how such an omni-big-step semantics can be formally related to a standard small-step semantics. This chapter exploit a few additional TLC tactics to enable concise proofs.

• applys is an enhanced version of eapply.
• specializes is an enhanced version of specialize.
• lets and forwards are forward-chaining tactics that enable instantiating a lemma.

Exploiting these tactics is not required for solving exercises, yet is highly recommmended. For details, the chapter UseTactics.v from the Volume 2 of Software Foundations ("Programming Language Foundations") explains the behavior of these tactics.

Formalization of the Syntax and Semantics of the Language

Syntax

The syntax is described using an "abstract syntax tree". It follows a presentation that distiguishes between closed values (i.e., values with no free variables inside) and terms. This presentation simplifies the definition and evaluation of the substitution function. Indeed, when values are always closed, 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, the operation div to illustrate a partial operation, and rand to illustrate nondeterminism.

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.

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 chapter 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. They may be found in the file LibSepFmap.v.

Recall from chapter Hprop that our convention is to write s for a full memory state, of type state, and write h for a piece of memory state, of type heap. 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 a program 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. The remaining of this subsection describes the implementation of subst. It may be safely skipped. 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. A collection of implicit types is 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.

A collection of coercions is then introduced. Coercions correspond to implicit function calls, which aim to make statements more concise. 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.

The constructor trm_val is also declared as a coercion. Thus, instead of writing trm_val v at a place where term is expected, we may write just v .

The constructor trm_app is declared 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, t₁ t₂ t₃ is interpreted as trm_app (trm_app t₁ t₂) t₃.

Standard Big-Step Semantics

We are now ready to present a formal semantics for the language. To begin with, we present a big-step evaluation judgment, written big s t s' v. This judgment asserts that, starting from state s, the evaluation of the term t terminates in a state s', and produces 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. big for values and function definitions. A value evaluates to itself. A term function evaluates to a value function. Likewise for a recursive function.

2. big for function applications. The beta reduction rule asserts that (val_fun x t₁) v₂ evaluates to the same result as subst x v₂ t₁. Likewise, (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. big for structural constructs. A sequence trm_seq t₁ t₂ first biguates 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. big 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 t₀ 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. big 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 big judgment. The random number generator val_rand n produces an integer n₁ in the range from 0 inclusive to n exclusive.

6. big 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.

Omni-Big-Step Semantics

A triple of the form triple t H Q aims to capture the property that, for any input state s satisfying the precondition H, any possible execution of the program starting from the initial configuration (s,t) does terminate and reach a final configuration satisfying the postcondition Q. Yet, the standard big-step judgment, of the form big s t s' v, only accounts for one possible execution. Using this judgment, we may be able capture the property that "if a particular execution terminates, then it reaches a final configuration satisfying Q". However, using the standard big-step judgment, we are totally unable to capture the property that "all possible executions do terminate". The omni-big-step judgment is a generalization of the standard big-step judgment that allows capturing properties of "all possible executions". The judgment takes the form eval s t Q, where Q denotes a set of final configurations. It captures the fact that all possible executions starting on the configuration (s,t) terminate safely and reach a final configuration in the set Q. One may think of Q as a set of pairs made of values and a state. Equivalently, one may think of Q as a postcondition, of type val→state→Prop. Indeed, the two views are isomorphic.

The inductive definition below defines the omni-big-step judgment, of the form eval s t Q, where Q is a postcondition. The generalization from standard-big-step to omni-big-step follows a regular pattern, which should become visible while stepping through the rules.

1. eval for values and function definitions. The judgment eval s v Q asserts that the value v in the state s satisfies the postcondition Q. The premise for deriving that judgment is thus that Q v s must hold.

2. eval for function applications. Consider a function v₁ of the form val_fun x t₁. The term trm_app v₁ v₂ terminates with postcondition Q provided that the term subst x v₂ t₁ terminates with postcondition Q. Hence, to prove eval s₁ (trm_app v₁ v₂) Q, one must establish eval s₁ (subst x v₂ t₁) Q .

3. eval for structural constructs. Consider a sequence trm_seq t₁ t₂ in a state s. What is the requirement for this configuration to terminate with postcondition Q? First, we need the evaluation of t₁ in s to terminate. Let Q₁ be an overapproximation of the set of possible results for the execution of (s,t₁). To prove that the sequence trm_seq t₁ t₂ terminates in Q, we need to show that, for any intermediate state s₂ satisfying Q₁, the evaluation of t₂ terminates with postcondition Q. The case of let-bindings is similar, only with an additional substitution.

4. eval for conditionals. The term (trm_if (val_bool b) t₁ t₂) admits the same behavior as the term t₁ when b is true, and as the term t₂ when b is false.

5. eval for primitive stateless operations. The judgment eval s (val_add n₁ n₂) Q asserts that the pair made of the state s and the value n₁+n₂ produced by the addition operation satisfy the postcondition Q. Hence, the relevant premise is: Q (val_int (n₁ + n₂)) s. A more interesting case is that that of a nondeterministic construct. The rule eval_rand gives the condition under which the term val_rand n, evaluated in a state s, produces an output satisfying Q. The first premise of the rule requires n > 0. The second premise requires that, for any value n₁ that val_rand n may evaluate to, that is, such that 0 ≤ n₁ < n, the configuration made of n₁ and s satisfies the postcondition Q. Technically: ∀ n₁, (0 ≤ n₁ < n) → (Q n₁ s).

6. eval for primitive operations on memory. The interesting case is that of allocation, which is nondeterministic. For val_ref v, evaluated in a state s, to produce a configuration in Q, we require that, for any location p fresh from the state s, the pair made of p and of the state s extended with a binding from p to v together satisfy Q.

Note that if eval s t Q holds, then Q does not correspond to the set of configurations reachable from (s,t), but to an overapproximation of that set. Trying to set up an inductive definition that relates (s,t) with exactly its set of reachable configurations would introduce unnecessary complications. Besides, observe that eval s t Q cannot hold if there exists one or more executions of (s,t) that runs into an error, i.e., that reaches a configuration that is stuck.

Loading of Definitions from LibSepReference

Throughout the rest of this file, we rely not on the definitions shown above, but on the definitions from LibSepReference.v, which are essentially equivalent. We reproduce the definition of eval to avoid having to consider in the proofs cases that correspond to language extensions.

Definition of Triples

Now comes the most important definition of the course. A triple triple t H Q asserts that, for any input state s satisfying the precondition H, any possible execution of (s,t) terminates and reaches a final configuration satisfying the postcondition Q. This statement is captured in terms of the omni-big-step semantics as follows.

Statement of Structural Rules

The "frame rule" asserts that an arbitrary heap predicate may be added to both the precondition and the postcondition of any triple.

The "consequence rule" asserts, like in Hoare Logic, that a triple is perserved when strengthening its precondition or weakening its postcondition.

The "extraction rule for pure facts" asserts that a judgment of the form triple t (\[P] \* H) Q is derivable from P → triple t H Q. This structural rule captures the extraction of the pure facts out of the precondition of a triple, in a similar way as himpl_hstar_hpure_l for entailments.

The "extraction rule for pure facts" asserts that judgment of the form triple t (\∃ x, J x) Q is derivable from ∀ x, triple t (J x) Q . Again, this rule is the counterpart of the corresponding rule on entailements, named himpl_hexists_l.

Derived Structural Rules

Given a triple to be established, is is very unlikely for the frame rule to be applicable directly to that goal, because the precondition must be exactly of the form H \* H' and the postcondition exactly of the form Q \*+ H', for some H'. For example, the frame rule would not apply to a proof obligation of the form triple t (H' \* H) (Q \*+ H'), simply because H' \* H does not match H \* H'. This limitation of the frame rule can be addressed by combining the frame rule with the rule of consequence into a single rule, called the "consequence-frame rule". This rule, shown below, enables deriving a triple from another triple, without syntactic restriction on the shape of the precondition and postcondition of the two triples involved.

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

Prove the combined consequence-frame rule.

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

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

Prove that triple_hpure' is indeed a corollary of triple_hpure.

More Details

Proof of the Consequence Rule

The proof of the consequence rule relies on establishing that the omni-big-step judgment is preserved when weakening its postcondition. Recall that in eval s t Q₁, the postcondition Q₁ is an overapproximation of the set of configurations reachable from (s,t). Thus, if Q₁ is included in a larger set Q₂, then Q₂ is also an overapproximation of the configurations reachable from (s,t). The formalization is straightforward by induction.

From there, it is straightforward to derive the consequence rule.

Proof of the Frame Rule

The second key property that we with to establish is the "frame rule". The frame rule asserts that if a specification triple H t Q holds, then one may derive triple (H \* H') t (Q \*+ H') for any H'. Recall from chapter Hprop that the operator Q \*+ H' is a notation for fun x ⇒ (Q x \* H'). Intuitively, if the term t executes safely in a heap H, then this this term should behave similarly in any extension of H with a disjoint part H'. Moreover, its evaluation should leave this piece of state H' unmodified throughout the execution of t. The crux of the proof of the frame rule is to argue that eval is stable by extension with a disjoint piece of heap.

This proof is by induction. The most interesting step is that of allocation. In a derivation built using eval_ref, we are given as assumption a property that holds for any location p fresh from h₁, and we are requested to prove a property that holds for any location p fresh from h₁ \u h₂. We are thus restricting the set of p that can be considered for allocation, hence the result holds.

The frame rule is derived from eval_frame and eval_conseq.

Proof of the Extraction Rules

The extraction rules are proved by unfolding the definition of triple and inverting the hypothesis capturing the fact that the input state satisfies the precondition.

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

Prove triple_hexists.

Rule for Naming Heaps

To prove triple t H Q, it suffices to show that, for any heap h satisfying H, the triple triple t (= h) Q holds. In other words, even though the predicate triple abstracts away from the input heap, it remains technically possible to assign a name to that heap.

Exercise: 1 star, standard, optional (triple_named_heap)

Prove the reasoning rule hoare_named_heap, which allows introducing a name for the input heap.

Optional Material

Alternative Structural Rule for Existentials

Traditional papers on Separation Logic do not include triple_hexists, but instead include a rule called triple_hexists2 that features an existential quantifier both in the precondition and the postcondition. As we show next, in the presence of the consequence rule, the two rules are equivalent.

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

Using triple_hexists and triple_conseq, as well as the tactic xsimpl, prove that triple_hexists2 is derivable.

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

Reciprocally, using triple_hexists2 and triple_conseq, as well as the tactic xsimpl, prove that triple_hexists is derivable. Of course, you may not use triple_hexists in this proof.)

Compared with triple_hexists2, the formulation of triple_hexists is more concise, and is easier to exploit in practice.

Small-Step Semantics

Suppose that one has at hand a language accompanied with a formal semantics not in big-step stype but in small-step style. What are the options for formalizing total correctness triples? We discuss two approaches. The first one consists of formally relating the small-step judgment with the omni-big-step judgment. The second one consists of directly defining triples in terms of the small-step judgment. Before explaining the two approaches, let us present the formalization of the small-step semantics. The judgment step s t s' t' describes the small-step reduction relation: it asserts that the program configuration (s,t) can take one reduction step towards the program configuration (s',t'). Its definition is standard.

The judgment steps s t s' t' corresponds to the reflexive-transitive closure of step. Concretely, this judgment asserts that the configuration (s,t) can reduce in zero, one, or several steps to (s',t').

The predicate trm_is_val t asserts that t is a value.

Consider a configuration (s,t), where t is not a value. If this configuration cannot take any reduction step, it is said to be "stuck". On the contrary, a configuration (s,t) that may take a step is said to be "reducible".

Values are not reducible.

The predicate notstuck s t asserts that either t is a value or t is reducible.

Equivalence Between Small-Step and Omni-Big-Step

If one considers the omni-big-step semantics to be the starting point of a development, then the definition of triple is obviously sound with respect to that semantics, as it concludes eval s t Q. If, however, one considers the small-step semantics to be the starting point, then to establish soundness it is required to prove that triple t H Q ensures that all possible evaluations of t in a heap satisfy H are: (1) terminating, (2) always reaching a value, and (3) this value and the final state obtained satisfy the postconditon Q. We begin by formalizing each of these properties w.r.t. the small-step judgment. The judgment terminates s t is defined inductively. The execution starting from (s,t) terminates if, for any possible step leads to a configuration that terminates. Note that a configuration that has reached a value cannot take a step, hence is considered terminating.

The judgment safe s t asserts that no execution may reach a stuck term. In other words, for any configuration (s',t') reachable from (s,t), it is the case that the configuration (s',t') is either a value or is reducible.

The judgment correct s t Q asserts that if the execution of (s,t) reaches a final configuration, then this final configuration satisfies Q.

The conjunction of safe and correct corresponds to "partial correctness". The conjunction of safe, correct and terminates corresponds to "total correctness". The soundness theorem that we aim for establishes that triple t H Q entails total correctness.
    triple t H Q →
    ∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q. In order to prove soundness, we introduce an inductively-defined predicate, named seval, which captures total correctness in small-step style. On the one hand, we prove that seval entails safe, correct, and terminates. On the other hand, we prove that seval is related to the omni-big-step judgment, namely eval. The judgment seval s t Q asserts that any execution of (s,t) terminates and reaches a configuration satisfying Q. In the "base" case, seval s v Q holds if the terminal configuration (s,v) satisfies Q. In the "step" case, seval s t Q holds if (1) the configuration (s,t) is reducible, and (2) if for any step that (s,t) may take to (s',t'), the predicate seval s' t' Q holds.

Exercise: 2 stars, standard, optional (seval_val_inv)

As a warm-up to get some familiary with seval, prove the following inversion lemma, which asserts that, given a value v, the property seval s v Q implies Q s v.

We begin with the three key properties of seval: termination, safety, and correctness.

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

Prove that seval captures termination.

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

Prove that seval captures safety.