# TriplesStructural Reasoning Rules

Set Implicit Arguments.

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

_{1}\* H

_{2}, Q

_{1}\*+ H

_{2}, and \∃ x, H. In chapter Himpl, we have formalized the heap entailment relations, written H

_{1}==> H

_{2}and Q

_{1}===> Q

_{2}. 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.

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

### Syntax

Inductive val : Type :=

| val_unit : val

| val_bool : bool → val

| val_int : int → val

| val_loc : loc → val

| val_fun : var → trm → val

| val_fix : var → var → trm → val

| val_ref : val

| val_get : val

| val_set : val

| val_free : val

| val_add : val

| val_div : val

| val_rand : val

| val_unit : val

| val_bool : bool → val

| val_int : int → val

| val_loc : loc → val

| val_fun : var → trm → val

| val_fix : var → var → trm → val

| val_ref : val

| val_get : val

| val_set : val

| val_free : val

| val_add : val

| val_div : val

| val_rand : val

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

with trm : Type :=

| trm_val : val → trm

| trm_var : var → trm

| trm_fun : var → trm → trm

| trm_fix : var → var → trm → trm

| trm_app : trm → trm → trm

| trm_seq : trm → trm → trm

| trm_let : var → trm → trm → trm

| trm_if : trm → trm → trm → trm.

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

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

_{1}t

_{2}) is defined as trm_let x (subst y w t

_{1}) (if var_eq x y then t

_{2}else (subst y w t

_{2})).

Fixpoint subst (y:var) (w:val) (t:trm) : trm :=

let aux t := subst y w t in

let if_y_eq x t

match t with

| trm_val v ⇒ trm_val v

| trm_var x ⇒ if_y_eq x (trm_val w) t

| trm_fun x t

| trm_fix f x t

| trm_app t

| trm_seq t

| trm_let x t

| trm_if t

end.

let aux t := subst y w t in

let if_y_eq x t

_{1}t_{2}:= if var_eq x y then t_{1}else t_{2}inmatch t with

| trm_val v ⇒ trm_val v

| trm_var x ⇒ if_y_eq x (trm_val w) t

| trm_fun x t

_{1}⇒ trm_fun x (if_y_eq x t_{1}(aux t_{1}))| trm_fix f x t

_{1}⇒ trm_fix f x (if_y_eq f t_{1}(if_y_eq x t_{1}(aux t_{1})))| trm_app t

_{1}t_{2}⇒ trm_app (aux t_{1}) (aux t_{2})| trm_seq t

_{1}t_{2}⇒ trm_seq (aux t_{1}) (aux t_{2})| trm_let x t

_{1}t_{2}⇒ trm_let x (aux t_{1}) (if_y_eq x t_{2}(aux t_{2}))| trm_if t

_{0}t_{1}t_{2}⇒ trm_if (aux t_{0}) (aux t_{1}) (aux t_{2})end.

### Implicit Types and Coercions

Implicit Types b : bool.

Implicit Types v r : val.

Implicit Types t : trm.

Implicit Types s : state.

Implicit Types v r : val.

Implicit Types t : trm.

Implicit Types s : state.

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

_{1}t_{2}as a shorthand for trm_app t_{1}t_{2}. The idea of associating trm_app as the "Funclass" coercion for the type trm is that if a term t_{1}of type trm is applied like a function to an argument, then t_{1}should be interpreted as trm_app t_{1}.
Interestingly, the "Funclass" coercion for trm_app can be iterated. The
expression t

_{1}t_{2}t_{3}is parsed by Coq as (t_{1}t_{2}) t_{3}. The first application t_{1}t_{2}is interpreted as trm_app t_{1}t_{2}. This expression, which itself has type trm, is applied to t_{3}. Hence, t_{1}t_{2}t_{3}is interpreted as trm_app (trm_app t_{1}t_{2}) t_{3}.### Standard Big-Step Semantics

_{0}t

_{1}t

_{2}, then it is required that t

_{0}be either a variable or a value. This is not a real restriction, because trm_if t

_{0}t

_{1}t

_{2}can always be encoded as let x = t

_{0}in if x then t

_{1}else t

_{2}.

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.

| big_val : ∀ s v,

big s (trm_val v) s v

| big_fun : ∀ s x t

_{1},

big s (trm_fun x t

_{1}) s (val_fun x t

_{1})

| big_fix : ∀ s f x t

_{1},

big s (trm_fix f x t

_{1}) s (val_fix f x t

_{1})

2. big for function applications.
The beta reduction rule asserts that (val_fun x t

_{1}) v_{2}evaluates to the same result as subst x v_{2}t_{1}. Likewise, (val_fix f x t_{1}) v_{2}evaluates to subst x v_{2}(subst f v_{1}t_{1}), where v_{1}denotes the recursive function itself, that is, val_fix f x t_{1}.| big_app_fun : ∀ s

_{1}s

_{2}v

_{1}v

_{2}x t

_{1}v,

v

_{1}= val_fun x t

_{1}→

big s

_{1}(subst x v

_{2}t

_{1}) s

_{2}v →

big s

_{1}(trm_app v

_{1}v

_{2}) s

_{2}v

| big_app_fix : ∀ s

_{1}s

_{2}v

_{1}v

_{2}f x t

_{1}v,

v

_{1}= val_fix f x t

_{1}→

big s

_{1}(subst x v

_{2}(subst f v

_{1}t

_{1})) s

_{2}v →

big s

_{1}(trm_app v

_{1}v

_{2}) s

_{2}v

3. big for structural constructs.
A sequence trm_seq t
The let-binding trm_let x t

_{1}t_{2}first biguates t_{1}, taking the state from s_{1}to s_{2}, drops the result of t_{1}, then evaluates t_{2}, taking the state from s_{2}to s_{3}._{1}t_{2}is similar, except that the variable x gets substituted for the result of t_{1}inside t_{2}.| big_seq : ∀ s

_{1}s

_{2}s

_{3}t

_{1}t

_{2}v

_{1}v,

big s

_{1}t

_{1}s

_{2}v

_{1}→

big s

_{2}t

_{2}s

_{3}v →

big s

_{1}(trm_seq t

_{1}t

_{2}) s

_{3}v

| big_let : ∀ s

_{1}s

_{2}s

_{3}x t

_{1}t

_{2}v

_{1}r,

big s

_{1}t

_{1}s

_{2}v

_{1}→

big s

_{2}(subst x v

_{1}t

_{2}) s

_{3}r →

big s

_{1}(trm_let x t

_{1}t

_{2}) s

_{3}r

4. big for conditionals.
A conditional in a source program is assumed to be of the form
if t
The term trm_if (val_bool true) t

_{0}then t_{1}else t_{2}, where t_{0}is either a variable or a value. If t_{0}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_{0}then t_{1}else t_{2}. The value v_{0}must be a boolean value, otherwise evaluation gets stuck._{1}t_{2}behaves like t_{1}, whereas the term trm_if (val_bool false) t_{1}t_{2}behaves like t_{2}. This behavior is described by a single rule, leveraging Coq's "if" constructor to factor out the two cases.| big_if : ∀ s

_{1}s

_{2}b v t

_{1}t

_{2},

big s

_{1}(if b then t

_{1}else t

_{2}) s

_{2}v →

big s

_{1}(trm_if (val_bool b) t

_{1}t

_{2}) s

_{2}v

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
The division operation, on the same arguments, produces the quotient
n

_{1}and val_int n_{2}produces val_int (n_{1}+ n_{2})._{1}/ n_{2}, under the assumption that the dividor n_{2}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_{1}in the range from 0 inclusive to n exclusive.| big_add : ∀ s n

_{1}n

_{2},

big s (val_add (val_int n

_{1}) (val_int n

_{2})) s (val_int (n

_{1}+ n

_{2}))

| big_div : ∀ s n

_{1}n

_{2},

n

_{2}≠ 0 →

big s (val_div (val_int n

_{1}) (val_int n

_{2})) s (val_int (Z.quot n

_{1}n

_{2}))

| big_rand : ∀ s n n

_{1},

0 ≤ n

_{1}< n →

big s (val_rand (val_int n)) s (val_int n

_{1})

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.

| big_ref : ∀ s v p,

¬ Fmap.indom s p →

big s (val_ref v) (Fmap.update s p v) (val_loc p)

| big_get : ∀ s p,

Fmap.indom s p →

big s (val_get (val_loc p)) s (Fmap.read s p)

| big_set : ∀ s p v,

Fmap.indom s p →

big s (val_set (val_loc p) v) (Fmap.update s p v) val_unit

| big_free : ∀ s p,

Fmap.indom s p →

big s (val_free (val_loc p)) (Fmap.remove s p) val_unit.

### Omni-Big-Step Semantics

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.

| eval_val : ∀ s v Q,

Q v s →

eval s (trm_val v) Q

| eval_fun : ∀ s x t

_{1}Q,

Q (val_fun x t

_{1}) s →

eval s (trm_fun x t

_{1}) Q

| eval_fix : ∀ s f x t

_{1}Q,

Q (val_fix f x t

_{1}) s →

eval s (trm_fix f x t

_{1}) Q

2. eval for function applications.
Consider a function v

_{1}of the form val_fun x t_{1}. The term trm_app v_{1}v_{2}terminates with postcondition Q provided that the term subst x v_{2}t_{1}terminates with postcondition Q. Hence, to prove eval s_{1}(trm_app v_{1}v_{2}) Q, one must establish eval s_{1}(subst x v_{2}t_{1}) Q .| eval_app_fun : ∀ s

_{1}v

_{1}v

_{2}x t

_{1}Q,

v

_{1}= val_fun x t

_{1}→

eval s

_{1}(subst x v

_{2}t

_{1}) Q →

eval s

_{1}(trm_app v

_{1}v

_{2}) Q

| eval_app_fix : ∀ s v

_{1}v

_{2}f x t

_{1}Q,

v

_{1}= val_fix f x t

_{1}→

eval s (subst x v

_{2}(subst f v

_{1}t

_{1})) Q →

eval s (trm_app v

_{1}v

_{2}) Q

3. eval for structural constructs.
Consider a sequence trm_seq t

_{1}t_{2}in a state s. What is the requirement for this configuration to terminate with postcondition Q? First, we need the evaluation of t_{1}in s to terminate. Let Q_{1}be an overapproximation of the set of possible results for the execution of (s,t_{1}). To prove that the sequence trm_seq t_{1}t_{2}terminates in Q, we need to show that, for any intermediate state s_{2}satisfying Q_{1}, the evaluation of t_{2}terminates with postcondition Q. The case of let-bindings is similar, only with an additional substitution.| eval_seq : ∀ Q

_{1}s t

_{1}t

_{2}Q,

eval s t

_{1}Q

_{1}→

(∀ v

_{1}s

_{2}, Q

_{1}v

_{1}s

_{2}→ eval s

_{2}t

_{2}Q) →

eval s (trm_seq t

_{1}t

_{2}) Q

| eval_let : ∀ Q

_{1}s x t

_{1}t

_{2}Q,

eval s t

_{1}Q

_{1}→

(∀ v

_{1}s

_{2}, Q

_{1}v

_{1}s

_{2}→ eval s

_{2}(subst x v

_{1}t

_{2}) Q) →

eval s (trm_let x t

_{1}t

_{2}) Q

4. eval for conditionals.
The term (trm_if (val_bool b) t

_{1}t_{2}) admits the same behavior as the term t_{1}when b is true, and as the term t_{2}when b is false.| eval_if : ∀ s (b:bool) t

_{1}t

_{2}Q,

eval s (if b then t

_{1}else t

_{2}) Q →

eval s (trm_if (val_bool b) t

_{1}t

_{2}) Q

5. eval for primitive stateless operations.
The judgment eval s (val_add n
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

_{1}n_{2}) Q asserts that the pair made of the state s and the value n_{1}+n_{2}produced by the addition operation satisfy the postcondition Q. Hence, the relevant premise is: Q (val_int (n_{1}+ n_{2})) s._{1}that val_rand n may evaluate to, that is, such that 0 ≤ n_{1}< n, the configuration made of n_{1}and s satisfies the postcondition Q. Technically: ∀ n_{1}, (0 ≤ n_{1}< n) → (Q n_{1}s).| eval_add : ∀ s n

_{1}n

_{2}Q,

Q (val_int (n

_{1}+ n

_{2})) s →

eval s (val_add (val_int n

_{1}) (val_int n

_{2})) Q

| eval_div : ∀ s n

_{1}n

_{2}Q,

n

_{2}≠ 0 →

Q (val_int (Z.quot n

_{1}n

_{2})) s →

eval s (val_div (val_int n

_{1}) (val_int n

_{2})) Q

| eval_rand : ∀ s n Q,

n > 0 →

(∀ n

_{1}, 0 ≤ n

_{1}< n → Q n

_{1}s) →

eval s (val_rand (val_int n)) Q

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.

| eval_ref : ∀ s v Q,

(∀ p, ¬ Fmap.indom s p →

Q (val_loc p) (Fmap.update s p v)) →

eval s (val_ref v) Q

| eval_get : ∀ s p Q,

Fmap.indom s p →

Q (Fmap.read s p) s →

eval s (val_get (val_loc p)) Q

| eval_set : ∀ s p v Q,

Fmap.indom s p →

Q val_unit (Fmap.update s p v) →

eval s (val_set (val_loc p) v) Q

| eval_free : ∀ s p Q,

Fmap.indom s p →

Q val_unit (Fmap.remove s p) →

eval s (val_free (val_loc p)) 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

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types p : loc.

Implicit Types n : int.

Implicit Types v w r : val.

Implicit Types t : trm.

Implicit Types h : heap.

Implicit Types s : state.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

Inductive eval : state → trm → (val→state→Prop) → Prop :=

| eval_val : ∀ s v Q,

Q v s →

eval s (trm_val v) Q

| eval_fun : ∀ s x t

Q (val_fun x t

eval s (trm_fun x t

| eval_fix : ∀ s f x t

Q (val_fix f x t

eval s (trm_fix f x t

| eval_app_fun : ∀ s

v

eval s

eval s

| eval_app_fix : ∀ s v

v

eval s (subst x v

eval s (trm_app v

| eval_seq : ∀ Q

eval s t

(∀ v

eval s (trm_seq t

| eval_let : ∀ Q

eval s t

(∀ v

eval s (trm_let x t

| eval_if : ∀ s (b:bool) t

eval s (if b then t

eval s (trm_if (val_bool b) t

| eval_add : ∀ s n

Q (val_int (n

eval s (val_add (val_int n

| eval_div : ∀ s n

n

Q (val_int (Z.quot n

eval s (val_div (val_int n

| eval_rand : ∀ s n Q,

n > 0 →

(∀ n

eval s (val_rand (val_int n)) Q

| eval_ref : ∀ s v Q,

(∀ p, ¬ Fmap.indom s p →

Q (val_loc p) (Fmap.update s p v)) →

eval s (val_ref v) Q

| eval_get : ∀ s p Q,

Fmap.indom s p →

Q (Fmap.read s p) s →

eval s (val_get (val_loc p)) Q

| eval_set : ∀ s p v Q,

Fmap.indom s p →

Q val_unit (Fmap.update s p v) →

eval s (val_set (val_loc p) v) Q

| eval_free : ∀ s p Q,

Fmap.indom s p →

Q val_unit (Fmap.remove s p) →

eval s (val_free (val_loc p)) Q.

Implicit Types b : bool.

Implicit Types p : loc.

Implicit Types n : int.

Implicit Types v w r : val.

Implicit Types t : trm.

Implicit Types h : heap.

Implicit Types s : state.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

Inductive eval : state → trm → (val→state→Prop) → Prop :=

| eval_val : ∀ s v Q,

Q v s →

eval s (trm_val v) Q

| eval_fun : ∀ s x t

_{1}Q,Q (val_fun x t

_{1}) s →eval s (trm_fun x t

_{1}) Q| eval_fix : ∀ s f x t

_{1}Q,Q (val_fix f x t

_{1}) s →eval s (trm_fix f x t

_{1}) Q| eval_app_fun : ∀ s

_{1}v_{1}v_{2}x t_{1}Q,v

_{1}= val_fun x t_{1}→eval s

_{1}(subst x v_{2}t_{1}) Q →eval s

_{1}(trm_app v_{1}v_{2}) Q| eval_app_fix : ∀ s v

_{1}v_{2}f x t_{1}Q,v

_{1}= val_fix f x t_{1}→eval s (subst x v

_{2}(subst f v_{1}t_{1})) Q →eval s (trm_app v

_{1}v_{2}) Q| eval_seq : ∀ Q

_{1}s t_{1}t_{2}Q,eval s t

_{1}Q_{1}→(∀ v

_{1}s_{2}, Q_{1}v_{1}s_{2}→ eval s_{2}t_{2}Q) →eval s (trm_seq t

_{1}t_{2}) Q| eval_let : ∀ Q

_{1}s x t_{1}t_{2}Q,eval s t

_{1}Q_{1}→(∀ v

_{1}s_{2}, Q_{1}v_{1}s_{2}→ eval s_{2}(subst x v_{1}t_{2}) Q) →eval s (trm_let x t

_{1}t_{2}) Q| eval_if : ∀ s (b:bool) t

_{1}t_{2}Q,eval s (if b then t

_{1}else t_{2}) Q →eval s (trm_if (val_bool b) t

_{1}t_{2}) Q| eval_add : ∀ s n

_{1}n_{2}Q,Q (val_int (n

_{1}+ n_{2})) s →eval s (val_add (val_int n

_{1}) (val_int n_{2})) Q| eval_div : ∀ s n

_{1}n_{2}Q,n

_{2}≠ 0 →Q (val_int (Z.quot n

_{1}n_{2})) s →eval s (val_div (val_int n

_{1}) (val_int n_{2})) Q| eval_rand : ∀ s n Q,

n > 0 →

(∀ n

_{1}, 0 ≤ n_{1}< n → Q n_{1}s) →eval s (val_rand (val_int n)) Q

| eval_ref : ∀ s v Q,

(∀ p, ¬ Fmap.indom s p →

Q (val_loc p) (Fmap.update s p v)) →

eval s (val_ref v) Q

| eval_get : ∀ s p Q,

Fmap.indom s p →

Q (Fmap.read s p) s →

eval s (val_get (val_loc p)) Q

| eval_set : ∀ s p v Q,

Fmap.indom s p →

Q val_unit (Fmap.update s p v) →

eval s (val_set (val_loc p) v) Q

| eval_free : ∀ s p Q,

Fmap.indom s p →

Q val_unit (Fmap.remove s p) →

eval s (val_free (val_loc p)) Q.

## Definition of Triples

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.

Parameter triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ x, triple t (J x) Q) →

triple t (\∃ x, J x) Q.

(∀ x, triple t (J x) Q) →

triple t (\∃ x, J x) Q.

## Derived Structural Rules

Lemma triple_conseq_frame : ∀ H

triple t H

H ==> H

Q

triple t H Q.

_{2}H_{1}Q_{1}t H Q,triple t H

_{1}Q_{1}→H ==> H

_{1}\* H_{2}→Q

_{1}\*+ H_{2}===> Q →triple t H Q.

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

Prove the combined consequence-frame rule.
Proof using. (* FILL IN HERE *) Admitted.

☐

☐

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

Prove that triple_hpure' is indeed a corollary of triple_hpure.
Lemma triple_hpure' : ∀ t (P:Prop) Q,

(P → triple t \[] Q) →

triple t \[P] Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

(P → triple t \[] Q) →

triple t \[P] Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

## Proof of the Consequence Rule

_{1}, the postcondition Q

_{1}is an overapproximation of the set of configurations reachable from (s,t). Thus, if Q

_{1}is included in a larger set Q

_{2}, then Q

_{2}is also an overapproximation of the configurations reachable from (s,t). The formalization is straightforward by induction.

Lemma eval_conseq : ∀ s t Q

eval s t Q

Q

eval s t Q

Proof using.

introv M W.

asserts W': (∀ v h, Q

induction M; try solve [ constructors* ].

Qed.

_{1}Q_{2},eval s t Q

_{1}→Q

_{1}===> Q_{2}→eval s t Q

_{2}.Proof using.

introv M W.

asserts W': (∀ v h, Q

_{1}v h → Q_{2}v h). { auto. } clear W.induction M; try solve [ constructors* ].

Qed.

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

Lemma triple_conseq : ∀ t H' Q' H Q,

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

Proof using. unfolds triple. introv M MH MQ HF. applys* eval_conseq. Qed.

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

Proof using. unfolds triple. introv M MH MQ HF. applys* eval_conseq. Qed.

## Proof of the Frame Rule

Lemma eval_frame : ∀ h

eval h

Fmap.disjoint h

eval (h

_{1}h_{2}t Q,eval h

_{1}t Q →Fmap.disjoint h

_{1}h_{2}→eval (h

_{1}\u h_{2}) t (Q \*+ (= h_{2})).
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

_{1}, and we are requested to prove a property that holds for any location p fresh from h_{1}\u h_{2}. We are thus restricting the set of p that can be considered for allocation, hence the result holds.
Proof using.

introv M HD. gen h

try solve [ hint hstar_intro; constructors* ].

{ rename M into M

specializes IH

lets (h

{ rename M into M

specializes IH

lets (h

{ (* Here is the interesting case about allocation. *)

rename H into M. applys eval_ref. intros p Hp.

rewrite Fmap.indom_union_eq in Hp. rew_logic in Hp.

destruct Hp as [Hp

rewrite* Fmap.update_union_not_r. applys hstar_intro.

{ applys* M. } { auto. } { applys* Fmap.disjoint_update_not_r. } }

{ applys eval_get. { rewrite* Fmap.indom_union_eq. }

{ rewrite* Fmap.read_union_l. applys* hstar_intro. } }

{ applys eval_set. { rewrite* Fmap.indom_union_eq. }

{ rewrite* Fmap.update_union_l. applys hstar_intro.

{ auto. } { auto. } { applys* Fmap.disjoint_update_l. } } }

{ applys eval_free. { rewrite* Fmap.indom_union_eq. }

{ rewrite* Fmap.remove_disjoint_union_l. applys hstar_intro.

{ auto. } { auto. } { applys* Fmap.disjoint_remove_l. } } }

Qed.

introv M HD. gen h

_{2}. induction M; intros;try solve [ hint hstar_intro; constructors* ].

{ rename M into M

_{1}, H into M_{2}, IHM into IH_{1}, H_{0}into IH_{2}.specializes IH

_{1}HD. applys eval_seq IH_{1}. introv HK.lets (h

_{1}'&h_{2}'&K_{1}'&K_{2}'&KD&KU): hstar_inv HK. subst. applys* IH_{2}. }{ rename M into M

_{1}, H into M_{2}, IHM into IH_{1}, H_{0}into IH_{2}.specializes IH

_{1}HD. applys eval_let IH_{1}. introv HK.lets (h

_{1}'&h_{2}'&K_{1}'&K_{2}'&KD&KU): hstar_inv HK. subst. applys* IH_{2}. }{ (* Here is the interesting case about allocation. *)

rename H into M. applys eval_ref. intros p Hp.

rewrite Fmap.indom_union_eq in Hp. rew_logic in Hp.

destruct Hp as [Hp

_{1}Hp_{2}].rewrite* Fmap.update_union_not_r. applys hstar_intro.

{ applys* M. } { auto. } { applys* Fmap.disjoint_update_not_r. } }

{ applys eval_get. { rewrite* Fmap.indom_union_eq. }

{ rewrite* Fmap.read_union_l. applys* hstar_intro. } }

{ applys eval_set. { rewrite* Fmap.indom_union_eq. }

{ rewrite* Fmap.update_union_l. applys hstar_intro.

{ auto. } { auto. } { applys* Fmap.disjoint_update_l. } } }

{ applys eval_free. { rewrite* Fmap.indom_union_eq. }

{ rewrite* Fmap.remove_disjoint_union_l. applys hstar_intro.

{ auto. } { auto. } { applys* Fmap.disjoint_remove_l. } } }

Qed.

The frame rule is derived from eval_frame and eval_conseq.

Lemma triple_frame : ∀ t H Q H',

triple t H Q →

triple t (H \* H') (Q \*+ H').

Proof.

introv M. intros h HF. lets (h

subst. specializes M M

{ applys eval_frame M MD. } { xsimpl. intros h' →. applys M

Qed.

triple t H Q →

triple t (H \* H') (Q \*+ H').

Proof.

introv M. intros h HF. lets (h

_{1}&h_{2}&M_{1}&M_{2}&MD&MU): hstar_inv (rm HF).subst. specializes M M

_{1}. applys eval_conseq.{ applys eval_frame M MD. } { xsimpl. intros h' →. applys M

_{2}. }Qed.

## Proof of the Extraction Rules

Lemma triple_hpure : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. intros h (h

lets E: hempty_inv HP. subst. rewrite Fmap.union_empty_l. applys¬M.

Qed.

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. intros h (h

_{1}&h_{2}&M_{1}&M_{2}&D&U). destruct M_{1}as (M_{1}&HP).lets E: hempty_inv HP. subst. rewrite Fmap.union_empty_l. applys¬M.

Qed.

Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ (x:A), triple t (J x) Q) →

triple t (hexists J) Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

(∀ (x:A), triple t (J x) Q) →

triple t (hexists J) Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

## Rule for Naming Heaps

#### Exercise: 1 star, standard, optional (triple_named_heap)

Prove the reasoning rule hoare_named_heap, which allows introducing a name for the input heap.
Lemma triple_named_heap : ∀ t H Q,

(∀ h, H h → triple t (= h) Q) →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

(∀ h, H h → triple t (= h) Q) →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

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.
Lemma triple_hexists2 : ∀ A (Hof:A→hprop) (Qof:A→val→hprop) t,

(∀ x, triple t (Hof x) (Qof x)) →

triple t (\∃ x, Hof x) (fun v ⇒ \∃ x, Qof x v).

Proof using. (* FILL IN HERE *) Admitted.

(* *)

(∀ x, triple t (Hof x) (Qof x)) →

triple t (\∃ x, Hof x) (fun v ⇒ \∃ x, Qof x v).

Proof using. (* FILL IN HERE *) Admitted.

(* *)

#### 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.)
Lemma triple_hexists_of_triple_hexists2 : ∀ t (A:Type) (Hof:A→hprop) Q,

(∀ x, triple t (Hof x) Q) →

triple t (\∃ x, Hof x) Q.

Proof using. (* FILL IN HERE *) Admitted.

(* *)

(∀ x, triple t (Hof x) Q) →

triple t (\∃ x, Hof x) Q.

Proof using. (* FILL IN HERE *) Admitted.

(* *)

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

## Small-Step Semantics

Inductive step : state → trm → state → trm → Prop :=

(* Context rules *)

| step_seq_ctx : ∀ s

step s

step s

| step_let_ctx : ∀ s

step s

step s

(* Reductions *)

| step_fun : ∀ s x t

step s (trm_fun x t

| step_fix : ∀ s f x t

step s (trm_fix f x t

| step_app_fun : ∀ s v

v

step s (trm_app v

| step_app_fix : ∀ s v

v

step s (trm_app v

| step_if : ∀ s b t

step s (trm_if (val_bool b) t

| step_seq : ∀ s t

step s (trm_seq v

| step_let : ∀ s x t

step s (trm_let x v

(* Primitive operations *)

| step_add : ∀ s n

step s (val_add (val_int n

| step_div : ∀ s n

n

step s (val_div (val_int n

| step_rand : ∀ s n n

0 ≤ n

step s (val_rand (val_int n)) s (val_int n

| step_ref : ∀ s v p,

¬ Fmap.indom s p →

step s (val_ref v) (Fmap.update s p v) (val_loc p)

| step_get : ∀ s p,

Fmap.indom s p →

step s (val_get (val_loc p)) s (Fmap.read s p)

| step_set : ∀ s p v,

Fmap.indom s p →

step s (val_set (val_loc p) v) (Fmap.update s p v) val_unit

| step_free : ∀ s p,

Fmap.indom s p →

step s (val_free (val_loc p)) (Fmap.remove s p) val_unit.

(* Context rules *)

| step_seq_ctx : ∀ s

_{1}s_{2}t_{1}t_{1}' t_{2},step s

_{1}t_{1}s_{2}t_{1}' →step s

_{1}(trm_seq t_{1}t_{2}) s_{2}(trm_seq t_{1}' t_{2})| step_let_ctx : ∀ s

_{1}s_{2}x t_{1}t_{1}' t_{2},step s

_{1}t_{1}s_{2}t_{1}' →step s

_{1}(trm_let x t_{1}t_{2}) s_{2}(trm_let x t_{1}' t_{2})(* Reductions *)

| step_fun : ∀ s x t

_{1},step s (trm_fun x t

_{1}) s (val_fun x t_{1})| step_fix : ∀ s f x t

_{1},step s (trm_fix f x t

_{1}) s (val_fix f x t_{1})| step_app_fun : ∀ s v

_{1}v_{2}x t_{1},v

_{1}= val_fun x t_{1}→step s (trm_app v

_{1}v_{2}) s (subst x v_{2}t_{1})| step_app_fix : ∀ s v

_{1}v_{2}f x t_{1},v

_{1}= val_fix f x t_{1}→step s (trm_app v

_{1}v_{2}) s (subst x v_{2}(subst f v_{1}t_{1}))| step_if : ∀ s b t

_{1}t_{2},step s (trm_if (val_bool b) t

_{1}t_{2}) s (if b then t_{1}else t_{2})| step_seq : ∀ s t

_{2}v_{1},step s (trm_seq v

_{1}t_{2}) s t_{2}| step_let : ∀ s x t

_{2}v_{1},step s (trm_let x v

_{1}t_{2}) s (subst x v_{1}t_{2})(* Primitive operations *)

| step_add : ∀ s n

_{1}n_{2},step s (val_add (val_int n

_{1}) (val_int n_{2})) s (val_int (n_{1}+ n_{2}))| step_div : ∀ s n

_{1}n_{2},n

_{2}≠ 0 →step s (val_div (val_int n

_{1}) (val_int n_{2})) s (Z.quot n_{1}n_{2})| step_rand : ∀ s n n

_{1},0 ≤ n

_{1}< n →step s (val_rand (val_int n)) s (val_int n

_{1})| step_ref : ∀ s v p,

¬ Fmap.indom s p →

step s (val_ref v) (Fmap.update s p v) (val_loc p)

| step_get : ∀ s p,

Fmap.indom s p →

step s (val_get (val_loc p)) s (Fmap.read s p)

| step_set : ∀ s p v,

Fmap.indom s p →

step s (val_set (val_loc p) v) (Fmap.update s p v) val_unit

| step_free : ∀ s p,

Fmap.indom s p →

step s (val_free (val_loc p)) (Fmap.remove s p) val_unit.

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

Inductive steps : state → trm → state → trm → Prop :=

| steps_refl : ∀ s t,

steps s t s t

| steps_step : ∀ s

step s

steps s

steps s

Lemma steps_of_step : ∀ s

step s

steps s

Proof using. introv M. applys steps_step M. applys steps_refl. Qed.

Lemma steps_trans : ∀ s

steps s

steps s

steps s

Proof using.

introv M

Qed.

| steps_refl : ∀ s t,

steps s t s t

| steps_step : ∀ s

_{1}s_{2}s_{3}t_{1}t_{2}t_{3},step s

_{1}t_{1}s_{2}t_{2}→steps s

_{2}t_{2}s_{3}t_{3}→steps s

_{1}t_{1}s_{3}t_{3}.Lemma steps_of_step : ∀ s

_{1}s_{2}t_{1}t_{2},step s

_{1}t_{1}s_{2}t_{2}→steps s

_{1}t_{1}s_{2}t_{2}.Proof using. introv M. applys steps_step M. applys steps_refl. Qed.

Lemma steps_trans : ∀ s

_{1}s_{2}s_{3}t_{1}t_{2}t_{3},steps s

_{1}t_{1}s_{2}t_{2}→steps s

_{2}t_{2}s_{3}t_{3}→steps s

_{1}t_{1}s_{3}t_{3}.Proof using.

introv M

_{1}. induction M_{1}; introv M_{2}. { auto. } { constructors*. }Qed.

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

Inductive terminates : state→trm→Prop :=

| terminates_step : ∀ s t,

(∀ s' t', step s t s' t' → terminates s' t') →

terminates s t.

| terminates_step : ∀ s t,

(∀ s' t', step s t s' t' → terminates s' t') →

terminates s t.

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.

triple t H Q →

∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.

Inductive seval : state→trm->(val→hprop)->Prop :=

| seval_val : ∀ s v Q,

Q v s →

seval s v Q

| seval_step : ∀ s t Q,

reducible s t → (* (exists s' t', step s t s' t') *)

(∀ s' t', step s t s' t' → seval s' t' Q) →

seval s t Q.

| seval_val : ∀ s v Q,

Q v s →

seval s v Q

| seval_step : ∀ s t Q,

reducible s t → (* (exists s' t', step s t s' t') *)

(∀ s' t', step s t s' t' → seval s' t' Q) →

seval s t Q.

#### 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.#### Exercise: 2 stars, standard, especially useful (seval_terminates)

Prove that seval captures termination.
Lemma seval_terminates : ∀ s t Q,

seval s t Q →

terminates s t.

Proof using. (* FILL IN HERE *) Admitted.

☐

seval s t Q →

terminates s t.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, standard, especially useful (seval_correct)

Prove that seval captures correctness.
Lemma seval_correct : ∀ s t Q,

seval s t Q →

correct s t Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

seval s t Q →

correct s t Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

Lemma seval_sound : ∀ s t Q,

seval s t Q →

terminates s t ∧ safe s t ∧ correct s t Q.

Proof using.

introv M. splits.

{ applys* seval_terminates. }

{ applys* seval_safe. }

{ applys* seval_correct. }

Qed.

seval s t Q →

terminates s t ∧ safe s t ∧ correct s t Q.

Proof using.

introv M. splits.

{ applys* seval_terminates. }

{ applys* seval_safe. }

{ applys* seval_correct. }

Qed.

We now establish that the omni-big-step evaluation judgment entails the
small-step-based seval judgment. The proof is carried out by induction on
the omni-big-step relation. It relies on a number of auxiliary results
establishing that, for each term construct, the seval judgment admits an
evaluation rule that mimics the omni-big-step evaluation rule. We begin with
the statements of the auxiliary lemmas.

Lemma seval_fun : ∀ s x t

Q (val_fun x t

seval s (trm_fun x t

Proof using.

introv M. applys seval_step.

{ do 2 esplit. constructor. }

{ introv R. inverts R. { applys seval_val. applys M. } }

Qed.

Lemma seval_fix : ∀ s f x t

Q (val_fix f x t

seval s (trm_fix f x t

Proof using.

introv M. applys seval_step.

{ do 2 esplit. constructor. }

{ introv R. inverts R. { applys seval_val. applys M. } }

Qed.

Lemma seval_app_fun : ∀ s x v

v

seval s (subst x v

seval s (trm_app v

Proof using.

introv E M. applys seval_step.

{ do 2 esplit. applys* step_app_fun. }

{ introv R. invert R; try solve [intros; false]. introv → → → → → R. inverts E. applys M. }

Qed.

Lemma seval_app_fix : ∀ s f x v

v

seval s (subst x v

seval s (trm_app v

Proof using.

introv E M. applys seval_step.

{ do 2 esplit. applys* step_app_fix. }

{ introv R. invert R; try solve [intros; false]. introv → → → → → R. inverts E. applys M. }

Qed.

_{1}Q,Q (val_fun x t

_{1}) s →seval s (trm_fun x t

_{1}) Q.Proof using.

introv M. applys seval_step.

{ do 2 esplit. constructor. }

{ introv R. inverts R. { applys seval_val. applys M. } }

Qed.

Lemma seval_fix : ∀ s f x t

_{1}Q,Q (val_fix f x t

_{1}) s →seval s (trm_fix f x t

_{1}) Q.Proof using.

introv M. applys seval_step.

{ do 2 esplit. constructor. }

{ introv R. inverts R. { applys seval_val. applys M. } }

Qed.

Lemma seval_app_fun : ∀ s x v

_{1}v_{2}t_{1}Q,v

_{1}= val_fun x t_{1}→seval s (subst x v

_{2}t_{1}) Q →seval s (trm_app v

_{1}v_{2}) Q.Proof using.

introv E M. applys seval_step.

{ do 2 esplit. applys* step_app_fun. }

{ introv R. invert R; try solve [intros; false]. introv → → → → → R. inverts E. applys M. }

Qed.

Lemma seval_app_fix : ∀ s f x v

_{1}v_{2}t_{1}Q,v

_{1}= val_fix f x t_{1}→seval s (subst x v

_{2}(subst f v_{1}t_{1})) Q →seval s (trm_app v

_{1}v_{2}) Q.Proof using.

introv E M. applys seval_step.

{ do 2 esplit. applys* step_app_fix. }

{ introv R. invert R; try solve [intros; false]. introv → → → → → R. inverts E. applys M. }

Qed.

#### Exercise: 5 stars, standard, especially useful (seval_seq)

Prove the big-step reasoning rule for sequence for seval.
Lemma seval_seq : ∀ s t

seval s t

(∀ s

seval s (trm_seq t

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}t_{2}Q_{1}Q,seval s t

_{1}Q_{1}→(∀ s

_{1}v_{1}, Q_{1}v_{1}s_{1}→ seval s_{1}t_{2}Q) →seval s (trm_seq t

_{1}t_{2}) Q.Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 5 stars, standard, optional (seval_let)

The proof of seval_let is the same as that of seval_seq. We also present it as an exercise to avoid giving away the solution.
Lemma seval_let : ∀ s x t

seval s t

(∀ s

seval s (trm_let x t

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}t_{2}Q_{1}Q,seval s t

_{1}Q_{1}→(∀ s

_{1}v_{1}, Q_{1}v_{1}s_{1}→ seval s_{1}(subst x v_{1}t_{2}) Q) →seval s (trm_let x t

_{1}t_{2}) Q.Proof using. (* FILL IN HERE *) Admitted.

☐

Lemma seval_if : ∀ s b t

seval s (if b then t

seval s (trm_if b t

Proof using.

introv M. applys seval_step.

{ do 2 esplit. constructors*. }

{ introv R. inverts R; tryfalse. { applys M. } }

Qed.

_{1}t_{2}Q,seval s (if b then t

_{1}else t_{2}) Q →seval s (trm_if b t

_{1}t_{2}) Q.Proof using.

introv M. applys seval_step.

{ do 2 esplit. constructors*. }

{ introv R. inverts R; tryfalse. { applys M. } }

Qed.

We are now ready to prove by induction that the omni-big-step judgment
entails the small-step-based judgment seval. Note that the reciprocal
entailment also holds, however it is not needed for establishing soundness.

Lemma seval_of_eval : ∀ s t Q,

eval s t Q →

seval s t Q.

Proof using.

introv M. induction M.

{ applys* seval_val. }

{ applys* seval_fun. }

{ applys* seval_fix. }

{ applys* seval_app_fun. }

{ applys* seval_app_fix. }

{ applys* seval_seq. }

{ applys* seval_let. }

{ applys* seval_if. }

{ applys seval_step.

{ do 2 esplit. applys* step_add. }

{ introv K. inverts K. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_div. }

{ introv K. inverts K. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_rand 0. math. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ forwards¬(p&D&N): (exists_fresh null s).

do 2 esplit. applys* step_ref. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_get. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_set. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_free. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

Qed.

eval s t Q →

seval s t Q.

Proof using.

introv M. induction M.

{ applys* seval_val. }

{ applys* seval_fun. }

{ applys* seval_fix. }

{ applys* seval_app_fun. }

{ applys* seval_app_fix. }

{ applys* seval_seq. }

{ applys* seval_let. }

{ applys* seval_if. }

{ applys seval_step.

{ do 2 esplit. applys* step_add. }

{ introv K. inverts K. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_div. }

{ introv K. inverts K. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_rand 0. math. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ forwards¬(p&D&N): (exists_fresh null s).

do 2 esplit. applys* step_ref. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_get. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_set. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

{ applys seval_step.

{ do 2 esplit. applys* step_free. }

{ introv K. inverts K; tryfalse. applys* seval_val. } }

Qed.

Putting it all together, we conclude on the soundness of Separation Logic
with respect to the small-step semantics defined by the relation step.

Lemma soundness_small_step : ∀ t H Q,

triple t H Q →

∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.

Proof using.

unfold triple. introv M Hs. specializes M Hs.

lets R: seval_of_eval M. applys seval_sound R.

Qed.

triple t H Q →

∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.

Proof using.

unfold triple. introv M Hs. specializes M Hs.

lets R: seval_of_eval M. applys seval_sound R.

Qed.

## Small-Step Based Triples

The first step is to check that this new definition of triple is sound. This
property has been essentially been established in the previous section via
the lemma seval_sound.

Lemma striple_sound : ∀ t H Q,

striple t H Q →

∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.

Proof using. introv M Hs. specializes M Hs. applys seval_sound M. Qed.

striple t H Q →

∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.

Proof using. introv M Hs. specializes M Hs. applys seval_sound M. Qed.

The second step is to establish reasoning rules for striple. Let us begin
with the consequence rule and the frame rule. For those, we need to
establish the consequence and the frame property directly for seval. The
proofs differ from the corresponding proofs on eval.
The consequence rule for seval is established by induction.

Lemma seval_conseq : ∀ s t Q Q',

seval s t Q' →

Q' ===> Q →

seval s t Q.

Proof using.

introv M WQ. induction M.

{ applys seval_val. applys* WQ. }

{ rename H

applys seval_step.

{ auto. }

{ introv HR. applys* IH. } }

Qed.

seval s t Q' →

Q' ===> Q →

seval s t Q.

Proof using.

introv M WQ. induction M.

{ applys seval_val. applys* WQ. }

{ rename H

_{1}into IH.applys seval_step.

{ auto. }

{ introv HR. applys* IH. } }

Qed.

The consequence rule follows directly.

Lemma striple_conseq : ∀ t H' Q' H Q,

striple t H' Q' →

H ==> H' →

Q' ===> Q →

striple t H Q.

Proof using.

introv M MH MQ HF. applys seval_conseq M MQ. applys* MH.

Qed.

striple t H' Q' →

H ==> H' →

Q' ===> Q →

striple t H Q.

Proof using.

introv M MH MQ HF. applys seval_conseq M MQ. applys* MH.

Qed.

The frame property for seval is also established by induction, however the
proof is more involved.

Section stepsFrame.

Hint Constructors step.

Lemma seval_frame : ∀ h

seval h

Fmap.disjoint h

seval (h

Proof using.

introv M HD. gen h

{ applys seval_val. applys* hstar_intro. }

{ rename H into M

applys seval_step.

{ unfolds reducible. clear M

induction R; tryfalse; try solve [ do 2 esplit; constructors* ].

{ forwards* (s'&t'&R'): IHR. }

{ forwards* (s'&t'&R'): IHR. }

{ lets (p'&F&_): exists_fresh null (Fmap.union s h

applys step_ref v p'. eauto. }

{ do 2 esplit. applys step_get. applys* Fmap.indom_union_l. }

{ do 2 esplit. applys step_set. applys* Fmap.indom_union_l. }

{ do 2 esplit. applys step_free. applys* Fmap.indom_union_l. } }

{ introv R. cuts (s

(∃ s

{ subst. applys* IH

clear M

gen_eq su: (s \u h

unfolds reducible. induction R; intros; subst; eauto.

{ destruct M

rename R into R

{ inverts R

{ destruct M

rename R into R

{ inverts R

{ rename H into D. rewrite Fmap.indom_union_eq in D. rew_logic in D.

destruct D as (D

{ rewrite* Fmap.update_union_not_r. }

{ applys* Fmap.disjoint_update_not_r. }

{ eauto. } }

{ destruct M

rewrite* Fmap.read_union_l. }

{ destruct M

{ rewrite* Fmap.update_union_l. }

{ applys* Fmap.disjoint_update_l. }

{ eauto. } }

{ destruct M

{ rewrite* remove_disjoint_union_l. }

{ applys* Fmap.disjoint_remove_l. }

{ eauto. } } } }

Qed.

End stepsFrame.

Hint Constructors step.

Lemma seval_frame : ∀ h

_{1}h_{2}t Q,seval h

_{1}t Q →Fmap.disjoint h

_{1}h_{2}→seval (h

_{1}\u h_{2}) t (Q \*+ (= h_{2})).Proof using.

introv M HD. gen h

_{2}. induction M; intros.{ applys seval_val. applys* hstar_intro. }

{ rename H into M

_{1}, H_{0}into M_{2}, H_{1}into IH_{2}.applys seval_step.

{ unfolds reducible. clear M

_{2}IH_{2}. destruct M_{1}as (s'&t'&R).induction R; tryfalse; try solve [ do 2 esplit; constructors* ].

{ forwards* (s'&t'&R'): IHR. }

{ forwards* (s'&t'&R'): IHR. }

{ lets (p'&F&_): exists_fresh null (Fmap.union s h

_{2}). do 2 esplit.applys step_ref v p'. eauto. }

{ do 2 esplit. applys step_get. applys* Fmap.indom_union_l. }

{ do 2 esplit. applys step_set. applys* Fmap.indom_union_l. }

{ do 2 esplit. applys step_free. applys* Fmap.indom_union_l. } }

{ introv R. cuts (s

_{1}'&E'&D'&R'):(∃ s

_{1}', s' = s_{1}' \u h_{2}∧ Fmap.disjoint s_{1}' h_{2}∧ step s t s_{1}' t').{ subst. applys* IH

_{2}. }clear M

_{2}IH_{2}.gen_eq su: (s \u h

_{2}). gen s.unfolds reducible. induction R; intros; subst; eauto.

{ destruct M

_{1}as (s_{0}&t_{0}&R_{0}).rename R into R

_{1}. forwards* (s_{1}'&E&D&R_{1}'): IHR s.{ inverts R

_{0}. { eauto. } { inverts R_{1}. } } }{ destruct M

_{1}as (s_{0}&t_{0}&R_{0}).rename R into R

_{1}. forwards* (s_{1}'&E&D&R_{1}'): IHR s.{ inverts R

_{0}. { eauto. } { inverts R_{1}. } } }{ rename H into D. rewrite Fmap.indom_union_eq in D. rew_logic in D.

destruct D as (D

_{1}&D_{2}). esplit. splits.{ rewrite* Fmap.update_union_not_r. }

{ applys* Fmap.disjoint_update_not_r. }

{ eauto. } }

{ destruct M

_{1}as (se&te&Re). inverts Re; tryfalse.rewrite* Fmap.read_union_l. }

{ destruct M

_{1}as (se&te&Re). inverts Re; tryfalse. esplit. splits.{ rewrite* Fmap.update_union_l. }

{ applys* Fmap.disjoint_update_l. }

{ eauto. } }

{ destruct M

_{1}as (se&te&Re). inverts Re; tryfalse. esplit. splits.{ rewrite* remove_disjoint_union_l. }

{ applys* Fmap.disjoint_remove_l. }

{ eauto. } } } }

Qed.

End stepsFrame.

The frame rule for striple then follows from the frame and the consequence
properties for seval.

Lemma striple_frame : ∀ t H Q H',

striple t H Q →

striple t (H \* H') (Q \*+ H').

Proof.

introv M. intros h HF. lets (h

subst. specializes M M

{ applys seval_frame M MD. } { xsimpl. intros h' →. applys M

Qed.

striple t H Q →

striple t (H \* H') (Q \*+ H').

Proof.

introv M. intros h HF. lets (h

_{1}&h_{2}&M_{1}&M_{2}&MD&MU): hstar_inv (rm HF).subst. specializes M M

_{1}. applys seval_conseq.{ applys seval_frame M MD. } { xsimpl. intros h' →. applys M

_{2}. }Qed.

To establish other reasoning rules for striple, one need to prove
big-step-style evaluation rules for seval, such as the lemma seval_let
stated earlier.
In summary, it is possible to set up a Separation Logic directly based on
the small-step-based judgment seval, without going through a definition of
the omni-big-step judgment eval. However, most of the proof effort
remains, as one needs to establish the frame property and to derive
big-step-style evaluation rules such as seval_let.

Consider a programming language that is deterministic, with the only
exception of the allocation operation, which may pick any fresh location.
For such languages, it is possible to define Separation Logic triples in
terms of the standard big-step semantics, using a technique known as the
"baked-in frame rule". Recall the big-step judgment.

First, we define a (total correctness) Hoare triple, written hoare t H Q.
This judgment asserts that, starting from a state s satisfying the
precondition H, the term t evaluates to a value v and to a state s'
that, together, satisfy the postcondition Q. Formally:

Definition hoare (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (s:state), H s →

∃ (s':state) (v:val), eval s t s' v ∧ Q v s'.

∀ (s:state), H s →

∃ (s':state) (v:val), eval s t s' v ∧ Q v s'.

#### Exercise: 2 stars, standard, especially useful (hoare_conseq)

To gain familiarity with the hoare judgment, prove the consequence rule for Hoare triples.
Lemma hoare_conseq : ∀ t H Q H' Q',

hoare t H' Q' →

H ==> H' →

Q' ===> Q →

hoare t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

hoare t H' Q' →

H ==> H' →

Q' ===> Q →

hoare t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

Definition btriple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

This definition inherently satisfies the frame rule, as we show below. The
proof essentially exploits the associativity of the star operator.

#### Exercise: 3 stars, standard, especially useful (btriple_frame)

Prove that btriple t H Q is a judgment satisfying the frame rule.
Lemma btriple_frame : ∀ t H Q H',

btriple t H Q →

btriple t (H \* H') (Q \*+ H').

Proof using. (* FILL IN HERE *) Admitted.

☐

btriple t H Q →

btriple t (H \* H') (Q \*+ H').

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}satisfies the precondition H and h

_{2}describes the rest of the state, then the evaluation of t produces a value v in a final state made that can be decomposed between a part h

_{1}' and h

_{2}unchanged, in such a way that v and h

_{1}' together satisfy the postcondition Q. Formally:

Definition btriple_lowlevel (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ h

Fmap.disjoint h

H h

∃ h

Fmap.disjoint h

∧ eval (h

∧ Q v h

∀ h

_{1}h_{2},Fmap.disjoint h

_{1}h_{2}→H h

_{1}→∃ h

_{1}' v,Fmap.disjoint h

_{1}' h_{2}∧ eval (h

_{1}\u h_{2}) t (h_{1}' \u h_{2}) v∧ Q v h

_{1}'.
Let us establish the equivalence between this alternative definition of
triple and the original one.

Lemma btriple_iff_btriple_lowlevel : ∀ t H Q,

btriple t H Q ↔ btriple_lowlevel t H Q.

Proof using.

unfold triple, btriple_lowlevel, hoare. iff M.

{ introv D P

forwards (h'&v&HR&HQ): M (=h

destruct HQ as (h

∃ h

{ intros H' h. introv (h

forwards (h

∃ (h

Qed.

btriple t H Q ↔ btriple_lowlevel t H Q.

Proof using.

unfold triple, btriple_lowlevel, hoare. iff M.

{ introv D P

_{1}.forwards (h'&v&HR&HQ): M (=h

_{2}) (h_{1}\u h_{2}). { applys* hstar_intro. }destruct HQ as (h

_{1}'&h_{2}'&N_{0}&N_{1}&N_{2}&N_{3}). subst.∃ h

_{1}' v. auto. }{ intros H' h. introv (h

_{1}&h_{2}&N_{1}&N_{2}&D&U).forwards (h

_{1}'&v&D'&HR&HQ): M h_{1}h_{2}; auto. subst.∃ (h

_{1}' \u h_{2}) v. split. { eauto. } { applys* hstar_intro. } }Qed.

The low-level definition of triple leveraging the baked-in frame rule may be
convenient for formalizing certain extensions of Separation Logic.

## Historical Notes

(* 2024-01-03 14:19 *)