RulesReasoning Rules
Set Implicit Arguments.
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
- introduced the key heap predicate operators,
- introduced the notion of Separation Logic triple,
- introduced the entailment relation,
- introduced the structural rules of Separation Logic.
- 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.
- proofs of the reasoning rules associated with each term construct,
- proofs of the specification of the primitive operations.
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_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
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.
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
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
Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
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} in
match 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.
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} in
match 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.
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_{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, it is interpreted
as trm_app (trm_app t_{1} t_{2}) t_{3}, which indeed corresponds to a function
applied to two arguments.
Big-Step Semantics
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.
| eval_val : ∀ s v,
eval s (trm_val v) s v
| eval_fun : ∀ s x t_{1},
eval s (trm_fun x t_{1}) s (val_fun x t_{1})
| eval_fix : ∀ s f x t_{1},
eval s (trm_fix f x t_{1}) s (val_fix f x t_{1})
2. eval 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}.
In the recursive case, (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}.
| eval_app_fun : ∀ s_{1} s_{2} v_{1} v_{2} x t_{1} v,
v_{1} = val_fun x t_{1} →
eval s_{1} (subst x v_{2} t_{1}) s_{2} v →
eval s_{1} (trm_app v_{1} v_{2}) s_{2} v
| eval_app_fix : ∀ s_{1} s_{2} v_{1} v_{2} f x t_{1} v,
v_{1} = val_fix f x t_{1} →
eval s_{1} (subst x v_{2} (subst f v_{1} t_{1})) s_{2} v →
eval s_{1} (trm_app v_{1} v_{2}) s_{2} v
3. eval for structural constructs.
A sequence trm_seq t_{1} t_{2} first evaluates 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}.
The let-binding trm_let x t_{1} t_{2} is similar, except that the
variable x gets substituted for the result of t_{1} inside t_{2}.
| eval_seq : ∀ s_{1} s_{2} s_{3} t_{1} t_{2} v_{1} v,
eval s_{1} t_{1} s_{2} v_{1} →
eval s_{2} t_{2} s_{3} v →
eval s_{1} (trm_seq t_{1} t_{2}) s_{3} v
| eval_let : ∀ s_{1} s_{2} s_{3} x t_{1} t_{2} v_{1} r,
eval s_{1} t_{1} s_{2} v_{1} →
eval s_{2} (subst x v_{1} t_{2}) s_{3} r →
eval s_{1} (trm_let x t_{1} t_{2}) s_{3} r
4. eval for conditionals.
A conditional in a source program is assumed to be of the form
if t_{0} then t_{1} else t_{2}, where t_{0} 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_{0} then t_{1} else t_{2}. The value v_{0} must be a boolean value,
otherwise evaluation gets stuck.
The term trm_if (val_bool true) t_{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.
| eval_if : ∀ s_{1} s_{2} b v t_{1} t_{2},
eval s_{1} (if b then t_{1} else t_{2}) s_{2} v →
eval s_{1} (trm_if (val_bool b) t_{1} t_{2}) s_{2} v
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_{1} and val_int n_{2} produces val_int (n_{1} + n_{2}).
The division operation, on the same arguments, produces the
quotient n_{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 eval judgment.
| eval_add : ∀ s n_{1} n_{2},
eval s (val_add (val_int n_{1}) (val_int n_{2})) s (val_int (n_{1} + n_{2}))
| eval_div : ∀ s n_{1} n_{2},
n_{2} ≠ 0 →
eval s (val_div (val_int n_{1}) (val_int n_{2})) s (val_int (Z.quot n_{1} n_{2}))
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.
| eval_ref : ∀ s v p,
¬ Fmap.indom s p →
eval s (val_ref v) (Fmap.update s p v) (val_loc p)
| eval_get : ∀ s p,
Fmap.indom s p →
eval s (val_get (val_loc p)) s (Fmap.read s p)
| eval_set : ∀ s p v,
Fmap.indom s p →
eval s (val_set (val_loc p) v) (Fmap.update s p v) val_unit
| eval_free : ∀ s p,
Fmap.indom s p →
eval s (val_free (val_loc p)) (Fmap.remove s p) val_unit.
End SyntaxAndSemantics.
Loading of Definitions from Direcŧ
Implicit Types x 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.
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.
Rules for Terms
Reasoning Rule for Sequences
{H} t_{1} {fun v => H_{1}} {H_{1}} t_{2} {Q} | |
{H} (t_{1};t_{2}) {Q} |
Parameter triple_seq : ∀ t_{1} t_{2} H Q H_{1},
triple t_{1} H (fun v ⇒ H_{1}) →
triple t_{2} H_{1} Q →
triple (trm_seq t_{1} t_{2}) H Q.
triple t_{1} H (fun v ⇒ H_{1}) →
triple t_{2} H_{1} Q →
triple (trm_seq t_{1} t_{2}) H Q.
The variable v denotes the result of the evaluation of t_{1}. 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_{1} as a value irrelevant to the remaining of the
evaluation.
Reasoning Rule for Let-Bindings
{H} t_{1} {Q_{1}} (forall x, {Q_{1} x} t_{2} {Q}) | |
{H} (let x = t_{1} in t_{2}) {Q} |
{H} t_{1} {Q_{1}} (forall v, {Q_{1} v} (subst x v t_{2}) {Q}) | |
{H} (let x = t_{1} in t_{2}) {Q} |
Parameter triple_let : ∀ x t_{1} t_{2} Q_{1} H Q,
triple t_{1} H Q_{1} →
(∀ v_{1}, triple (subst x v_{1} t_{2}) (Q_{1} v_{1}) Q) →
triple (trm_let x t_{1} t_{2}) H Q.
triple t_{1} H Q_{1} →
(∀ v_{1}, triple (subst x v_{1} t_{2}) (Q_{1} v_{1}) Q) →
triple (trm_let x t_{1} t_{2}) H Q.
Reasoning Rule for Conditionals
b = true -> {H} t_{1} {Q} b = false -> {H} t_{2} {Q} | |
{H} (if b then t_{1} in t_{2}) {Q} |
Parameter triple_if_case : ∀ b t_{1} t_{2} H Q,
(b = true → triple t_{1} H Q) →
(b = false → triple t_{2} H Q) →
triple (trm_if (val_bool b) t_{1} t_{2}) H Q.
(b = true → triple t_{1} H Q) →
(b = false → triple t_{2} H Q) →
triple (trm_if (val_bool b) t_{1} t_{2}) H Q.
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
{\[]} v {fun r => \[r = v]} |
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.
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.
Lemma triple_val_minimal : ∀ v,
triple (trm_val v) \[] (fun r ⇒ \[r = v]).
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (trm_val v) \[] (fun r ⇒ \[r = v]).
Proof using. (* FILL IN HERE *) Admitted.
☐
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 appropriate structural rule(s).
Lemma triple_val' : ∀ v H Q,
H ==> Q v →
triple (trm_val v) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
H ==> Q v →
triple (trm_val v) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard, especially useful (triple_let_val)
Consider a term of the form let x = v_{1} in t_{2}, 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_{1} t_{2} H Q,
... →
triple (trm_let x v_{1} t_{2}) H Q. Hint: you'll need to guess the intermediate postcondition Q_{1} associated with the let-binding rule, and exploit the appropriate structural rules.
(* FILL IN HERE *)
☐
☐
Reasoning Rule for Functions
{\[]} (trm_fun x t_{1}) {fun r => \[r = val_fun x t_{1}]} |
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_{1} v_{2}.
Assume v_{1} to be a function, that is, to be of the form
val_fun x t_{1}. Then, according to the beta-reduction rule, the
semantics of trm_app v_{1} v_{2} is the same as that of subst x v_{2} t_{1}.
This reasoning rule is thus:
The corresponding Coq statement is as shown below.
v_{1} = val_fun x t_{1} {H} (subst x v_{2} t_{1}) {Q} | |
{H} (trm_app v_{1} v_{2}) {Q} |
Parameter triple_app_fun : ∀ x v_{1} v_{2} t_{1} H Q,
v_{1} = val_fun x t_{1} →
triple (subst x v_{2} t_{1}) H Q →
triple (trm_app v_{1} v_{2}) H Q.
v_{1} = val_fun x t_{1} →
triple (subst x v_{2} t_{1}) H Q →
triple (trm_app v_{1} v_{2}) H Q.
The generalization to the application of recursive functions is
straightforward. It is discussed further in this chapter.
Specification of Primitive Operations
Specification of Arithmetic Primitive Operations
Parameter triple_add : ∀ n_{1} n_{2},
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
The specification of the division operation val_div n_{1} n_{2} is similar,
yet with the extra requirement that the argument n_{2} must be nonzero.
This requirement n_{2} ≠ 0 is a pure fact, which can be asserted as
part of the precondition, as follows.
Parameter triple_div : ∀ n_{1} n_{2},
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Equivalently, the requirement n_{2} ≠ 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.
Parameter triple_div' : ∀ n_{1} n_{2},
n_{2} ≠ 0 →
triple (val_div n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
n_{2} ≠ 0 →
triple (val_div n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
This latter presentation with pure facts such as n_{2} ≠ 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
Parameter triple_get : ∀ v p,
triple (val_get (val_loc p))
(p ~~> v)
(fun r ⇒ \[r = v] \* (p ~~> v)).
triple (val_get (val_loc p))
(p ~~> v)
(fun r ⇒ \[r = v] \* (p ~~> v)).
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.
Parameter triple_ref : ∀ v,
triple (val_ref v)
\[]
(fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* p ~~> v).
triple (val_ref v)
\[]
(fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* p ~~> v).
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.
Review of the Structural Rules
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.)
Parameter triple_conseq_frame : ∀ H_{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.
triple t H_{1} Q_{1} →
H ==> H_{1} \* H_{2} →
Q_{1} \*+ H_{2} ===> Q →
triple t H Q.
The two extraction rules enable to extract pure facts and existentially
quantified variables, from the precondition into the Coq context.
Parameter triple_hpure : ∀ t (P:Prop) H Q,
(P → triple t H Q) →
triple t (\[P] \* H) Q.
Parameter triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,
(∀ (x:A), triple t (J x) Q) →
triple t (\∃ (x:A), J x) Q.
(P → triple t H Q) →
triple t (\[P] \* H) Q.
Parameter triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,
(∀ (x:A), triple t (J x) Q) →
triple t (\∃ (x:A), J x) Q.
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.
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.
☐
Verification Proof in Separation Logic
Proof of incr
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 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.
Definition incr : val :=
val_fun "p" (
trm_let "n" (trm_app val_get (trm_var "p")) (
trm_let "m" (trm_app (trm_app val_add
(trm_var "n")) (val_int 1)) (
trm_app (trm_app val_set (trm_var "p")) (trm_var "m")))).
val_fun "p" (
trm_let "n" (trm_app val_get (trm_var "p")) (
trm_let "m" (trm_app (trm_app val_add
(trm_var "n")) (val_int 1)) (
trm_app (trm_app val_set (trm_var "p")) (trm_var "m")))).
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 using.
(* initialize the proof *)
intros. applys triple_app_fun. { reflexivity. } simpl.
(* reason about let n = .. *)
applys triple_let.
(* reason about !p *)
{ apply triple_get. }
(* name n' the result of !p *)
intros n'. simpl.
(* substitute away the equality n' = n *)
apply triple_hpure. intros →.
(* reason about let m = .. *)
applys triple_let.
(* apply the frame rule to put aside p ~~> n *)
{ applys triple_conseq_frame.
(* reason about n+1 in the empty state *)
{ applys triple_add. }
{ xsimpl. }
{ xsimpl. } }
(* name m' the result of n+1 *)
intros m'. simpl.
(* substitute away the equality m' = m *)
apply triple_hpure. intros →.
(* reason about p := m *)
{ applys triple_set. }
Qed.
(* initialize the proof *)
intros. applys triple_app_fun. { reflexivity. } simpl.
(* reason about let n = .. *)
applys triple_let.
(* reason about !p *)
{ apply triple_get. }
(* name n' the result of !p *)
intros n'. simpl.
(* substitute away the equality n' = n *)
apply triple_hpure. intros →.
(* reason about let m = .. *)
applys triple_let.
(* apply the frame rule to put aside p ~~> n *)
{ applys triple_conseq_frame.
(* reason about n+1 in the empty state *)
{ applys triple_add. }
{ xsimpl. }
{ xsimpl. } }
(* name m' the result of n+1 *)
intros m'. simpl.
(* substitute away the equality m' = m *)
apply triple_hpure. intros →.
(* reason about p := m *)
{ applys triple_set. }
Qed.
Definition succ_using_incr : val :=
<{ fun 'n ⇒
let 'r = val_ref 'n in
incr 'r;
let 'x = ! 'r in
val_free 'r;
'x }>.
<{ fun 'n ⇒
let 'r = val_ref 'n in
incr 'r;
let 'x = ! 'r in
val_free 'r;
'x }>.
Recall the specification of succ_using_incr.
Lemma triple_succ_using_incr : ∀ (n:int),
triple (trm_app succ_using_incr n)
\[]
(fun v ⇒ \[v = val_int (n+1)]).
triple (trm_app succ_using_incr n)
\[]
(fun v ⇒ \[v = val_int (n+1)]).
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 using. (* FILL IN HERE *) Admitted.
☐
☐
Import Basic.Facto.
Recall from Basic the function repeat_incr.
let rec factorec n =
if n ≤ 1 then 1 else n * factorec (n-1)
if n ≤ 1 then 1 else n * factorec (n-1)
Definition factorec : val :=
<{ fix 'f 'n ⇒
let 'b = ('n ≤ 1) in
if 'b
then 1
else let 'x = 'n - 1 in
let 'y = 'f 'x in
'n * 'y }>.
<{ fix 'f 'n ⇒
let 'b = ('n ≤ 1) in
if 'b
then 1
else let 'x = 'n - 1 in
let 'y = 'f 'x in
'n * 'y }>.
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.
Lemma triple_factorec : ∀ n,
n ≥ 0 →
triple (factorec n)
\[]
(fun r ⇒ \[r = facto n]).
Proof using. (* FILL IN HERE *) Admitted.
☐
n ≥ 0 →
triple (factorec n)
\[]
(fun r ⇒ \[r = facto n]).
Proof using. (* FILL IN HERE *) Admitted.
☐
What's Next
- automating the application of the frame rule
- eliminating the need to manipulate program variables and substitutions during the verification proof.
Recall the specification for division.
Parameter triple_div : ∀ n_{1} n_{2},
n_{2} ≠ 0 →
triple (val_div n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
n_{2} ≠ 0 →
triple (val_div n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Equivalently, we could place the requirement n_{2} ≠ 0 in the
precondition:
Parameter triple_div' : ∀ n_{1} n_{2},
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Let us formally prove that the two presentations are equivalent.
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
Lemma triple_div_from_triple_div' : ∀ n_{1} n_{2},
n_{2} ≠ 0 →
triple (val_div n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Proof using. (* FILL IN HERE *) Admitted.
☐
n_{2} ≠ 0 →
triple (val_div n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Proof using. (* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, especially useful (triple_div'_from_triple_div)
Prove triple_div' by exploiting triple_div. Hint: the first key proof step is applys triple_hpure. Yet some preliminary rewriting is required for this tactic to apply. Hint: the second key proof step is applys triple_conseq.
Lemma triple_div'_from_triple_div : ∀ n_{1} n_{2},
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Proof using. (* FILL IN HERE *) Admitted.
☐
Recall the Separation Logic let rule.
Parameter triple_let : ∀ x t_{1} t_{2} Q_{1} H Q,
triple t_{1} H Q_{1} →
(∀ v_{1}, triple (subst x v_{1} t_{2}) (Q_{1} v_{1}) Q) →
triple (trm_let x t_{1} t_{2}) H Q.
triple t_{1} H Q_{1} →
(∀ v_{1}, triple (subst x v_{1} t_{2}) (Q_{1} v_{1}) Q) →
triple (trm_let x t_{1} t_{2}) H Q.
At first sight, it seems that, to reason about let x = t_{1} in t_{2}
in a state described by precondition H, we need to first reason
about t_{1} in that same state. Yet, t_{1} 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_{1} \* H_{2}, where H_{1} is the part
needed by t_{1}, and H_{2} denotes the rest of the state. The part
of the state covered by H_{2} remains unmodified during the evaluation
of t_{1}, and appears as part of the precondition of t_{2}.
The corresponding statement is as follows.
Lemma triple_let_frame : ∀ x t_{1} t_{2} Q_{1} H H_{1} H_{2} Q,
triple t_{1} H_{1} Q_{1} →
H ==> H_{1} \* H_{2} →
(∀ v_{1}, triple (subst x v_{1} t_{2}) (Q_{1} v_{1} \* H_{2}) Q) →
triple (trm_let x t_{1} t_{2}) H Q.
triple t_{1} H_{1} Q_{1} →
H ==> H_{1} \* H_{2} →
(∀ v_{1}, triple (subst x v_{1} t_{2}) (Q_{1} v_{1} \* H_{2}) Q) →
triple (trm_let x t_{1} t_{2}) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
☐
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).
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.
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 Hoare version of the reasoning rule for values is as follows.
1. We unfold the definition of hoare.
introv M. intros s K_{0}.
2. We provide the witnesses for the output value and heap.
These witnesses are dictated by the statement of eval_val.
∃ s v. splits.
3. We invoke the big-step rule eval_val
4. We establish the postcondition, exploiting the entailment hypothesis.
{ applys M. auto. }
Qed.
Qed.
The Separation Logic version of the rule then follows.
1. We unfold the definition of triple to reveal a hoare judgment.
introv M. intros H'.
2. We invoke the reasoning rule hoare_val that was just established.
3. We exploit the assumption and conclude using xchange.
xchange M.
Qed.
Qed.
Parameter eval_seq : ∀ s_{1} s_{2} s_{3} t_{1} t_{2} v_{1} v,
eval s_{1} t_{1} s_{2} v_{1} →
eval s_{2} t_{2} s_{3} v →
eval s_{1} (trm_seq t_{1} t_{2}) s_{3} v.
eval s_{1} t_{1} s_{2} v_{1} →
eval s_{2} t_{2} s_{3} v →
eval s_{1} (trm_seq t_{1} t_{2}) s_{3} v.
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.
Lemma hoare_seq : ∀ t_{1} t_{2} H Q H_{1},
hoare t_{1} H (fun v ⇒ H_{1}) →
hoare t_{2} H_{1} Q →
hoare (trm_seq t_{1} t_{2}) H Q.
Proof using.
hoare t_{1} H (fun v ⇒ H_{1}) →
hoare t_{2} H_{1} Q →
hoare (trm_seq t_{1} t_{2}) H Q.
Proof using.
1. We unfold the definition of hoare.
Let K_{0} describe the initial state.
2. We exploit the first hypothesis to obtain information about
the evaluation of the first subterm t_{1}.
The state before t_{1} executes is described by K_{0}.
The state after t_{1} executes is described by K_{1}.
forwards (s_{1}'&v_{1}&R_{1}&K_{1}): (rm M_{1}) K_{0}.
3. We exploit the second hypothesis to obtain information about
the evaluation of the first subterm t_{2}.
The state before t_{2} executes is described by K_{1}.
The state after t_{2} executes is described by K_{2}.
forwards (s_{2}'&v_{2}&R_{2}&K_{2}): (rm M_{2}) K_{1}.
4. We provide witness for the output value and heap.
They correspond to those produced by the evaluation of t_{2}.
∃ s_{2}' v_{2}. split.
5. We invoke the big-step rule.
6. We establish the final postcondition, which is directly
inherited from the reasoning on t_{2}.
{ apply K_{2}. }
Qed.
Qed.
The Separation Logic reasoning rule is proved as follows.
Lemma triple_seq : ∀ t_{1} t_{2} H Q H_{1},
triple t_{1} H (fun v ⇒ H_{1}) →
triple t_{2} H_{1} Q →
triple (trm_seq t_{1} t_{2}) H Q.
Proof using.
triple t_{1} H (fun v ⇒ H_{1}) →
triple t_{2} H_{1} Q →
triple (trm_seq t_{1} t_{2}) H Q.
Proof using.
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_{1},
we can invoke directly our first hypothesis.
{ applys M_{1}. }
{ applys M_{2}. }
Qed.
{ applys M_{2}. }
Qed.
Parameter eval_let : ∀ s_{1} s_{2} s_{3} x t_{1} t_{2} v_{1} v,
eval s_{1} t_{1} s_{2} v_{1} →
eval s_{2} (subst x v_{1} t_{2}) s_{3} v →
eval s_{1} (trm_let x t_{1} t_{2}) s_{3} v.
eval s_{1} t_{1} s_{2} v_{1} →
eval s_{2} (subst x v_{1} t_{2}) s_{3} v →
eval s_{1} (trm_let x t_{1} t_{2}) s_{3} v.
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.
(* FILL IN HERE *)
☐
☐
Parameter eval_add : ∀ s n_{1} n_{2},
eval s (val_add (val_int n_{1}) (val_int n_{2})) s (val_int (n_{1} + n_{2})).
eval s (val_add (val_int n_{1}) (val_int n_{2})) s (val_int (n_{1} + n_{2})).
In the proof, we will need to use the following result,
established in the first chapter.
As usual, we first establish a Hoare triple.
Lemma hoare_add : ∀ H n_{1} n_{2},
hoare (val_add n_{1} n_{2})
H
(fun r ⇒ \[r = val_int (n_{1} + n_{2})] \* H).
Proof using.
intros. intros s K_{0}. ∃ s (val_int (n_{1} + n_{2})). split.
{ applys eval_add. }
{ rewrite hstar_hpure_l. split.
{ auto. }
{ applys K_{0}. } }
Qed.
hoare (val_add n_{1} n_{2})
H
(fun r ⇒ \[r = val_int (n_{1} + n_{2})] \* H).
Proof using.
intros. intros s K_{0}. ∃ s (val_int (n_{1} + n_{2})). split.
{ applys eval_add. }
{ rewrite hstar_hpure_l. split.
{ auto. }
{ applys K_{0}. } }
Qed.
Deriving triple_add is then straightforward.
Lemma triple_add : ∀ n_{1} n_{2},
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_add. } { xsimpl. } { xsimpl. auto. }
Qed.
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_add. } { xsimpl. } { xsimpl. auto. }
Qed.
Parameter eval_div' : ∀ s n_{1} n_{2},
n_{2} ≠ 0 →
eval s (val_div (val_int n_{1}) (val_int n_{2})) s (val_int (Z.quot n_{1} n_{2})).
n_{2} ≠ 0 →
eval s (val_div (val_int n_{1}) (val_int n_{2})) s (val_int (Z.quot n_{1} n_{2})).
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 like triple_div except with hoare instead of triple.
(* FILL IN HERE *)
☐
☐
Proofs for Primitive Operations Operating on the State
Inductive hval : Type :=
| hval_val : val → hval.
Read in a Reference
Parameter eval_get : ∀ v s p,
Fmap.indom s p →
Fmap.read s p = v →
eval s (val_get (val_loc p)) s v.
Fmap.indom s p →
Fmap.read s p = v →
eval s (val_get (val_loc p)) s v.
We reformulate this rule by isolating from the current state s
the singleton heap made of the cell at location p, and let s_{2}
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.
Lemma eval_get_sep : ∀ s s_{2} p v,
s = Fmap.union (Fmap.single p v) s_{2} →
eval s (val_get (val_loc p)) s v.
s = Fmap.union (Fmap.single p v) s_{2} →
eval s (val_get (val_loc p)) s v.
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.
Proof using.
introv →. forwards Dv: Fmap.indom_single p v.
applys eval_get.
{ applys* Fmap.indom_union_l. }
{ rewrite* Fmap.read_union_l. rewrite* Fmap.read_single. }
Qed.
introv →. forwards Dv: Fmap.indom_single p v.
applys eval_get.
{ applys* Fmap.indom_union_l. }
{ rewrite* Fmap.read_union_l. rewrite* Fmap.read_single. }
Qed.
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.
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.
Lemma hoare_get : ∀ H v p,
hoare (val_get p)
((p ~~> v) \* H)
(fun r ⇒ \[r = v] \* (p ~~> v) \* H).
Proof using.
(* 1. We unfold the definition of hoare. *)
intros. intros s K_{0}.
(* 2. We provide the witnesses for the reduction,
as dictated by eval_get_sep. *)
∃ s v. split.
{ (* 3. To justify the reduction using eval_get_sep, we need to
argue that the state s decomposes as a singleton heap
Fmap.single p v and the rest of the state s_{2}. This is
obtained by eliminating the star in hypothesis K_{0}. *)
destruct K_{0} as (s_{1}&s_{2}&P_{1}&P_{2}&D&U).
(* 4. Inverting (p ~~> v) h_{1} simplifies the goal. *)
lets E_{1}: hsingle_inv P_{1}. subst s_{1}.
(* 5. At this point, the goal matches exactly eval_get_sep. *)
applys eval_get_sep U. }
{ (* 6. To establish the postcondition, we check the pure fact
\v = v, and check that the state, which has not changed,
satisfies the same heap predicate as in the precondition. *)
rewrite hstar_hpure_l. auto. }
Qed.
hoare (val_get p)
((p ~~> v) \* H)
(fun r ⇒ \[r = v] \* (p ~~> v) \* H).
Proof using.
(* 1. We unfold the definition of hoare. *)
intros. intros s K_{0}.
(* 2. We provide the witnesses for the reduction,
as dictated by eval_get_sep. *)
∃ s v. split.
{ (* 3. To justify the reduction using eval_get_sep, we need to
argue that the state s decomposes as a singleton heap
Fmap.single p v and the rest of the state s_{2}. This is
obtained by eliminating the star in hypothesis K_{0}. *)
destruct K_{0} as (s_{1}&s_{2}&P_{1}&P_{2}&D&U).
(* 4. Inverting (p ~~> v) h_{1} simplifies the goal. *)
lets E_{1}: hsingle_inv P_{1}. subst s_{1}.
(* 5. At this point, the goal matches exactly eval_get_sep. *)
applys eval_get_sep U. }
{ (* 6. To establish the postcondition, we check the pure fact
\v = v, and check that the state, which has not changed,
satisfies the same heap predicate as in the precondition. *)
rewrite hstar_hpure_l. auto. }
Qed.
Deriving the Separation Logic triple follows the usual pattern.
Lemma triple_get : ∀ v p,
triple (val_get p)
(p ~~> v)
(fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_get. }
{ xsimpl. }
{ xsimpl. auto. }
Qed.
triple (val_get p)
(p ~~> v)
(fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_get. }
{ xsimpl. }
{ xsimpl. auto. }
Qed.
Allocation of a Reference
Parameter eval_ref : ∀ s v p,
¬ Fmap.indom s p →
eval s (val_ref v) (Fmap.update s p v) (val_loc p).
¬ Fmap.indom s p →
eval s (val_ref v) (Fmap.update s p v) (val_loc 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_{1} to s_{1} \u s_{2},
where s_{2} denotes the singleton heap Fmap.single p v, and with
the requirement that Fmap.disjoint s_{2} s_{1}, to capture freshness.
Lemma eval_ref_sep : ∀ s_{1} s_{2} v p,
s_{2} = Fmap.single p v →
Fmap.disjoint s_{2} s_{1} →
eval s_{1} (val_ref v) (Fmap.union s_{2} s_{1}) (val_loc p).
Proof using.
s_{2} = Fmap.single p v →
Fmap.disjoint s_{2} s_{1} →
eval s_{1} (val_ref v) (Fmap.union s_{2} s_{1}) (val_loc p).
Proof using.
It is not needed to follow through this proof.
introv → D. forwards Dv: Fmap.indom_single p v.
rewrite <- Fmap.update_eq_union_single. applys* eval_ref.
{ intros N. applys* Fmap.disjoint_inv_not_indom_both D N. }
Qed.
rewrite <- Fmap.update_eq_union_single. applys* eval_ref.
{ intros N. applys* Fmap.disjoint_inv_not_indom_both D N. }
Qed.
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.
Lemma hoare_ref : ∀ H v,
hoare (val_ref v)
H
(fun r ⇒ (\∃ p, \[r = val_loc p] \* p ~~> v) \* H).
Proof using.
(* 1. We unfold the definition of hoare. *)
intros. intros s_{1} K_{0}.
(* 2. We claim the disjointness relation
Fmap.disjoint (Fmap.single p v) s_{1}. *)
forwards* (p&D): (single_fresh s_{1} v).
(* 3. We provide the witnesses for the reduction,
as dictated by eval_ref_sep. *)
∃ ((Fmap.single p v) \u s_{1}) (val_loc p). split.
{ (* 4. We exploit eval_ref_sep, which has exactly the desired shape! *)
applys eval_ref_sep D. auto. }
{ (* 5. We establish the postcondition
(\∃ p, \[r = val_loc p] \* p ~~> v) \* H
by providing p and the relevant pieces of heap. *)
applys hstar_intro.
{ ∃ p. rewrite hstar_hpure_l.
split. { auto. } { applys¬hsingle_intro. } }
{ applys K_{0}. }
{ applys D. } }
Qed.
hoare (val_ref v)
H
(fun r ⇒ (\∃ p, \[r = val_loc p] \* p ~~> v) \* H).
Proof using.
(* 1. We unfold the definition of hoare. *)
intros. intros s_{1} K_{0}.
(* 2. We claim the disjointness relation
Fmap.disjoint (Fmap.single p v) s_{1}. *)
forwards* (p&D): (single_fresh s_{1} v).
(* 3. We provide the witnesses for the reduction,
as dictated by eval_ref_sep. *)
∃ ((Fmap.single p v) \u s_{1}) (val_loc p). split.
{ (* 4. We exploit eval_ref_sep, which has exactly the desired shape! *)
applys eval_ref_sep D. auto. }
{ (* 5. We establish the postcondition
(\∃ p, \[r = val_loc p] \* p ~~> v) \* H
by providing p and the relevant pieces of heap. *)
applys hstar_intro.
{ ∃ p. rewrite hstar_hpure_l.
split. { auto. } { applys¬hsingle_intro. } }
{ applys K_{0}. }
{ applys D. } }
Qed.
We then derive the Separation Logic triple as usual.
Lemma triple_ref : ∀ v,
triple (val_ref v)
\[]
(funloc p ⇒ p ~~> v).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_ref. }
{ xsimpl. }
{ xsimpl. auto. }
Qed.
End Proofs.
triple (val_ref v)
\[]
(funloc p ⇒ p ~~> v).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_ref. }
{ xsimpl. }
{ xsimpl. auto. }
Qed.
End Proofs.
Reasoning Rules for Recursive Functions
Parameter triple_fix : ∀ f x t_{1} H Q,
H ==> Q (val_fix f x t_{1}) →
triple (trm_fix f x t_{1}) H Q.
H ==> Q (val_fix f x t_{1}) →
triple (trm_fix f x t_{1}) H Q.
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.
Parameter triple_app_fix : ∀ v_{1} v_{2} f x t_{1} H Q,
v_{1} = val_fix f x t_{1} →
triple (subst x v_{2} (subst f v_{1} t_{1})) H Q →
triple (trm_app v_{1} v_{2}) H Q.
v_{1} = val_fix f x t_{1} →
triple (subst x v_{2} (subst f v_{1} t_{1})) H Q →
triple (trm_app v_{1} v_{2}) H Q.
Proof of triple_fun and triple_fix
Proof of triple_if
Lemma eval_if : ∀ s_{1} s_{2} b v t_{1} t_{2},
eval s_{1} (if b then t_{1} else t_{2}) s_{2} v →
eval s_{1} (trm_if b t_{1} t_{2}) s_{2} v.
Proof using.
intros. case_if; applys eval_if; auto_false.
Qed.
eval s_{1} (if b then t_{1} else t_{2}) s_{2} v →
eval s_{1} (trm_if b t_{1} t_{2}) s_{2} v.
Proof using.
intros. case_if; applys eval_if; auto_false.
Qed.
The reasoning rule for conditional w.r.t. Hoare triples is as follows.
Lemma hoare_if_case : ∀ b t_{1} t_{2} H Q,
(b = true → hoare t_{1} H Q) →
(b = false → hoare t_{2} H Q) →
hoare (trm_if b t_{1} t_{2}) H Q.
Proof using.
introv M_{1} M_{2}. intros s K_{0}. destruct b.
{ forwards* (s_{1}'&v_{1}&R_{1}&K_{1}): (rm M_{1}) K_{0}.
∃ s_{1}' v_{1}. split*. { applys* eval_if. } }
{ forwards* (s_{1}'&v_{1}&R_{1}&K_{1}): (rm M_{2}) K_{0}.
∃ s_{1}' v_{1}. split*. { applys* eval_if. } }
Qed.
(b = true → hoare t_{1} H Q) →
(b = false → hoare t_{2} H Q) →
hoare (trm_if b t_{1} t_{2}) H Q.
Proof using.
introv M_{1} M_{2}. intros s K_{0}. destruct b.
{ forwards* (s_{1}'&v_{1}&R_{1}&K_{1}): (rm M_{1}) K_{0}.
∃ s_{1}' v_{1}. split*. { applys* eval_if. } }
{ forwards* (s_{1}'&v_{1}&R_{1}&K_{1}): (rm M_{2}) K_{0}.
∃ s_{1}' v_{1}. split*. { applys* eval_if. } }
Qed.
The corresponding Separation Logic reasoning rule is as follows.
Lemma triple_if_case : ∀ b t_{1} t_{2} H Q,
(b = true → triple t_{1} H Q) →
(b = false → triple t_{2} H Q) →
triple (trm_if (val_bool b) t_{1} t_{2}) H Q.
Proof using.
unfold triple. introv M_{1} M_{2}. intros H'.
applys hoare_if_case; intros Eb.
{ applys* M_{1}. }
{ applys* M_{2}. }
Qed.
(b = true → triple t_{1} H Q) →
(b = false → triple t_{2} H Q) →
triple (trm_if (val_bool b) t_{1} t_{2}) H Q.
Proof using.
unfold triple. introv M_{1} M_{2}. intros H'.
applys hoare_if_case; intros Eb.
{ applys* M_{1}. }
{ applys* M_{2}. }
Qed.
Observe that the above proofs contain a fair amount of duplication,
due to the symmetry between the b = true and b = false branches.
If we state the reasoning rules using Coq's conditional just like
it appears in the evaluation rule eval_if, we can better factorize
the proof script.
Lemma hoare_if : ∀ (b:bool) t_{1} t_{2} H Q,
hoare (if b then t_{1} else t_{2}) H Q →
hoare (trm_if b t_{1} t_{2}) H Q.
Proof using.
introv M_{1}. intros s K_{0}.
forwards (s'&v&R_{1}&K_{1}): (rm M_{1}) K_{0}.
∃ s' v. split. { applys eval_if R_{1}. } { applys K_{1}. }
Qed.
Lemma triple_if : ∀ b t_{1} t_{2} H Q,
triple (if b then t_{1} else t_{2}) H Q →
triple (trm_if (val_bool b) t_{1} t_{2}) H Q.
Proof using.
unfold triple. introv M_{1}. intros H'. applys hoare_if. applys M_{1}.
Qed.
hoare (if b then t_{1} else t_{2}) H Q →
hoare (trm_if b t_{1} t_{2}) H Q.
Proof using.
introv M_{1}. intros s K_{0}.
forwards (s'&v&R_{1}&K_{1}): (rm M_{1}) K_{0}.
∃ s' v. split. { applys eval_if R_{1}. } { applys K_{1}. }
Qed.
Lemma triple_if : ∀ b t_{1} t_{2} H Q,
triple (if b then t_{1} else t_{2}) H Q →
triple (trm_if (val_bool b) t_{1} t_{2}) H Q.
Proof using.
unfold triple. introv M_{1}. intros H'. applys hoare_if. applys M_{1}.
Qed.
Proof of triple_app_fun
Parameter eval_app_fun : ∀ s_{1} s_{2} v_{1} v_{2} x t_{1} v,
v_{1} = val_fun x t_{1} →
eval s_{1} (subst x v_{2} t_{1}) s_{2} v →
eval s_{1} (trm_app v_{1} v_{2}) s_{2} v.
v_{1} = val_fun x t_{1} →
eval s_{1} (subst x v_{2} t_{1}) s_{2} v →
eval s_{1} (trm_app v_{1} v_{2}) s_{2} v.
Lemma hoare_app_fun : ∀ v_{1} v_{2} x t_{1} H Q,
v_{1} = val_fun x t_{1} →
hoare (subst x v_{2} t_{1}) H Q →
hoare (trm_app v_{1} v_{2}) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
v_{1} = val_fun x t_{1} →
hoare (subst x v_{2} t_{1}) H Q →
hoare (trm_app v_{1} v_{2}) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
Lemma triple_app_fun : ∀ x v_{1} v_{2} t_{1} H Q,
v_{1} = val_fun x t_{1} →
triple (subst x v_{2} t_{1}) H Q →
triple (trm_app v_{1} v_{2}) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
v_{1} = val_fun x t_{1} →
triple (subst x v_{2} t_{1}) H Q →
triple (trm_app v_{1} v_{2}) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
Deallocation of a Reference
Parameter eval_free : ∀ s p,
Fmap.indom s p →
eval s (val_set (val_loc p)) (Fmap.remove s p) val_unit.
Fmap.indom s p →
eval s (val_set (val_loc p)) (Fmap.remove s p) val_unit.
Let us reformulate eval_free to replace references to Fmap.indom
and Fmap.remove with references to Fmap.single and Fmap.union
and Fmap.disjoint. The details are not essential, thus omitted.
Parameter eval_free_sep : ∀ s_{1} s_{2} v p,
s_{1} = Fmap.union (Fmap.single p v) s_{2} →
Fmap.disjoint (Fmap.single p v) s_{2} →
eval s_{1} (val_free p) s_{2} val_unit.
s_{1} = Fmap.union (Fmap.single p v) s_{2} →
Fmap.disjoint (Fmap.single p v) s_{2} →
eval s_{1} (val_free p) s_{2} val_unit.
Exercise: 3 stars, standard, optional (hoare_free)
Prove the Hoare triple for the operation free. Hint: exploit the lemma eval_free_sep.
Lemma hoare_free : ∀ H p v,
hoare (val_free (val_loc p))
((p ~~> v) \* H)
(fun _ ⇒ H).
Proof using. (* FILL IN HERE *) Admitted.
☐
hoare (val_free (val_loc p))
((p ~~> v) \* H)
(fun _ ⇒ H).
Proof using. (* FILL IN HERE *) Admitted.
☐
Exercise: 1 star, standard, optional (triple_free)
Derive from the Hoare triple for the operation free the corresponding Separation Logic triple. Hint: adapt the proof of lemma triple_set.
Lemma triple_free : ∀ p v,
triple (val_free (val_loc p))
(p ~~> v)
(fun _ ⇒ \[]).
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (val_free (val_loc p))
(p ~~> v)
(fun _ ⇒ \[]).
Proof using. (* FILL IN HERE *) Admitted.
☐
Write in a Reference
Parameter eval_set : ∀ m p v,
Fmap.indom m p →
eval m (val_set (val_loc p) v) (Fmap.update m p v) val_unit.
Fmap.indom m p →
eval m (val_set (val_loc p) v) (Fmap.update m p v) val_unit.
As for get, we first reformulate this lemma, to replace
references to Fmap.indom and Fmap.update with references
to Fmap.union, Fmap.single, and Fmap.disjoint, to
prepare for the introduction of separating conjunctions.
Lemma eval_set_sep : ∀ s_{1} s_{2} h_{2} p v_{1} v_{2},
s_{1} = Fmap.union (Fmap.single p v_{1}) h_{2} →
s_{2} = Fmap.union (Fmap.single p v_{2}) h_{2} →
Fmap.disjoint (Fmap.single p v_{1}) h_{2} →
eval s_{1} (val_set (val_loc p) v_{2}) s_{2} val_unit.
Proof using.
s_{1} = Fmap.union (Fmap.single p v_{1}) h_{2} →
s_{2} = Fmap.union (Fmap.single p v_{2}) h_{2} →
Fmap.disjoint (Fmap.single p v_{1}) h_{2} →
eval s_{1} (val_set (val_loc p) v_{2}) s_{2} val_unit.
Proof using.
It is not needed to follow through this proof.
introv → → D. forwards Dv: Fmap.indom_single p v_{1}.
applys_eq eval_set.
{ rewrite* Fmap.update_union_l. fequals.
rewrite* Fmap.update_single. }
{ applys* Fmap.indom_union_l. }
Qed.
applys_eq eval_set.
{ rewrite* Fmap.update_union_l. fequals.
rewrite* Fmap.update_single. }
{ applys* Fmap.indom_union_l. }
Qed.
The proof of the Hoare rule for set makes use of the following
fact (from LibSepFmap.v) about Fmap.disjoint: when one of its argument
is a singleton map, the value stored in that singleton map is irrelevant.
Check Fmap.disjoint_single_set : ∀ p v_{1} v_{2} h_{2},
Fmap.disjoint (Fmap.single p v_{1}) h_{2} →
Fmap.disjoint (Fmap.single p v_{2}) h_{2}.
Check Fmap.disjoint_single_set : ∀ p v_{1} v_{2} h_{2},
Fmap.disjoint (Fmap.single p v_{1}) h_{2} →
Fmap.disjoint (Fmap.single p v_{2}) h_{2}.
Exercise: 5 stars, standard, optional (hoare_set)
Prove the lemma hoare_set. Hints:- exploit the evaluation rule eval_set_sep presented above,
- exploit the lemma Fmap.disjoint_single_set presented above,
- to obtain an elegant proof, prefer invoking the lemmas hsingle_intro, hsingle_inv, hstar_intro, and hstar_inv, rather than unfolding the definitions of hstar and hsingle.
Lemma hoare_set : ∀ H v p v',
hoare (val_set (val_loc p) v)
((p ~~> v') \* H)
(fun _ ⇒ (p ~~> v) \* H).
Proof using. (* FILL IN HERE *) Admitted.
☐
hoare (val_set (val_loc p) v)
((p ~~> v') \* H)
(fun _ ⇒ (p ~~> v) \* H).
Proof using. (* FILL IN HERE *) Admitted.
☐
Lemma triple_set : ∀ w p v,
triple (val_set (val_loc p) w)
(p ~~> v)
(fun _ ⇒ p ~~> w).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_set. }
{ xsimpl. }
{ xsimpl. }
Qed.
End ProofsContinued.
triple (val_set (val_loc p) w)
(p ~~> v)
(fun _ ⇒ p ~~> w).
Proof using.
intros. intros H'. applys hoare_conseq.
{ applys hoare_set. }
{ xsimpl. }
{ xsimpl. }
Qed.
End ProofsContinued.
The proof that, e.g., triple_add is a consequence of
hoare_add follows the same pattern as many other similar
proofs, each time invoking the lemma hoare_conseq.
Thus, we could attempt at factorizing this proof pattern.
The following lemma corresponds to such an attempt.
Exercise: 2 stars, standard, optional (triple_of_hoare)
Prove the lemma triple_of_hoare stated below.
Lemma triple_of_hoare : ∀ t H Q,
(∀ H', ∃ Q', hoare t (H \* H') Q'
∧ Q' ===> Q \*+ H') →
triple t H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
(∀ H', ∃ Q', hoare t (H \* H') Q'
∧ Q' ===> Q \*+ H') →
triple t H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (triple_add')
Prove that triple_add is a consequence of hoare_add by exploiting triple_of_hoare.
Lemma triple_add' : ∀ n_{1} n_{2},
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
Proof using. (* FILL IN HERE *) Admitted.
☐
A general principle is that if t_{1} has the same semantics
as t_{2} (w.r.t. the big-step evaluation judgment eval),
then t_{1} and t_{2} satisfy the same triples.
Let us formalize this principle.
Two (closed) terms are semantically equivalent, written
trm_equiv t_{1} t_{2}, if two terms, when evaluated in the same
state, produce the same output.
Two terms that are equivalent satisfy the same Separation Logic
triples (and the same Hoare triples).
Indeed, the definition of a Separation Logic triple directly depends
on the notion of Hoare triple, and the latter directly depends
on the semantics captured by the predicate eval.
Let us formalize the result in three steps.
eval_like t_{1} t_{2} asserts that t_{2} evaluates like t_{1}.
In particular, this relation hold whenever t_{2} reduces
in small-step to t_{1}.
For example eval_like t (trm_let x t x) holds, reflecting the
fact that let x = t in x reduces in small-step to t.
Lemma eval_like_eta_reduction : ∀ (t:trm) (x:var),
eval_like t (trm_let x t x).
Proof using.
introv R. applys eval_let R.
simpl. rewrite var_eq_spec. case_if. applys eval_val.
Qed.
eval_like t (trm_let x t x).
Proof using.
introv R. applys eval_let R.
simpl. rewrite var_eq_spec. case_if. applys eval_val.
Qed.
It turns out that the symmetric relation eval_like (trm_let x t x) t
also holds: the term t does not exhibit more behaviors than those
of let x = t in x.
Lemma eval_like_eta_expansion : ∀ (t:trm) (x:var),
eval_like (trm_let x t x) t.
Proof using.
introv R. inverts R as. introv R_{1} R_{2}.
simpl in R_{2}. rewrite var_eq_spec in R_{2}. case_if.
inverts R_{2}. auto.
Qed.
eval_like (trm_let x t x) t.
Proof using.
introv R. inverts R as. introv R_{1} R_{2}.
simpl in R_{2}. rewrite var_eq_spec in R_{2}. case_if.
inverts R_{2}. auto.
Qed.
We deduce that a term t denotes a program equivalent to
the program let x = t in x.
Lemma trm_equiv_eta : ∀ (t:trm) (x:var),
trm_equiv t (trm_let x t x).
Proof using.
intros. intros s s' v. iff M.
{ applys eval_like_eta_reduction M. }
{ applys eval_like_eta_expansion M. }
Qed.
trm_equiv t (trm_let x t x).
Proof using.
intros. intros s s' v. iff M.
{ applys eval_like_eta_reduction M. }
{ applys eval_like_eta_expansion M. }
Qed.
If eval_like t_{1} t_{2}, then any triple that holds for t_{1}
also holds for t_{2}.
Lemma hoare_eval_like : ∀ t_{1} t_{2} H Q,
eval_like t_{1} t_{2} →
hoare t_{1} H Q →
hoare t_{2} H Q.
Proof using.
introv E M_{1} K_{0}. forwards (s'&v&R_{1}&K_{1}): M_{1} K_{0}.
∃ s' v. split. { applys E R_{1}. } { applys K_{1}. }
Qed.
Lemma triple_eval_like : ∀ t_{1} t_{2} H Q,
eval_like t_{1} t_{2} →
triple t_{1} H Q →
triple t_{2} H Q.
Proof using.
introv E M_{1}. intros H'. applys hoare_eval_like E. applys M_{1}.
Qed.
eval_like t_{1} t_{2} →
hoare t_{1} H Q →
hoare t_{2} H Q.
Proof using.
introv E M_{1} K_{0}. forwards (s'&v&R_{1}&K_{1}): M_{1} K_{0}.
∃ s' v. split. { applys E R_{1}. } { applys K_{1}. }
Qed.
Lemma triple_eval_like : ∀ t_{1} t_{2} H Q,
eval_like t_{1} t_{2} →
triple t_{1} H Q →
triple t_{2} H Q.
Proof using.
introv E M_{1}. intros H'. applys hoare_eval_like E. applys M_{1}.
Qed.
It follows that if two terms are equivalent, then they admit
the same triples.
Lemma triple_trm_equiv : ∀ t_{1} t_{2} H Q,
trm_equiv t_{1} t_{2} →
triple t_{1} H Q ↔ triple t_{2} H Q.
Proof using.
introv E. unfolds trm_equiv. iff M.
{ applys triple_eval_like M. introv R. applys* E. }
{ applys triple_eval_like M. introv R. applys* E. }
Qed.
trm_equiv t_{1} t_{2} →
triple t_{1} H Q ↔ triple t_{2} H Q.
Proof using.
introv E. unfolds trm_equiv. iff M.
{ applys triple_eval_like M. introv R. applys* E. }
{ applys triple_eval_like M. introv R. applys* E. }
Qed.
The reasoning rule triple_eval_like has a number of practical
applications. One, show below, is to revisit the proof of triple_app_fun
in a much more succint way, by arguing that trm_app (val_fun x t_{1}) v_{2} and
subst x v_{2} t_{1} are equivalent terms, hence they admit the same behavior.
Lemma triple_app_fun : ∀ x v_{1} v_{2} t_{1} H Q,
v_{1} = val_fun x t_{1} →
triple (subst x v_{2} t_{1}) H Q →
triple (trm_app v_{1} v_{2}) H Q.
Proof using.
introv E M_{1}. applys triple_eval_like M_{1}.
introv R. applys eval_app_fun E R.
Qed.
v_{1} = val_fun x t_{1} →
triple (subst x v_{2} t_{1}) H Q →
triple (trm_app v_{1} v_{2}) H Q.
Proof using.
introv E M_{1}. applys triple_eval_like M_{1}.
introv R. applys eval_app_fun E R.
Qed.
Another application is the following rule, which allows to modify the
parenthesis structure of a sequence.
Exercise: 3 stars, standard, optional (triple_trm_seq_assoc)
Prove that the term t_{1}; (t_{2}; t_{3}) satisfies the same triples as the term (t_{1};t_{2}); t_{3}.
Lemma triple_trm_seq_assoc : ∀ t_{1} t_{2} t_{3} H Q,
triple (trm_seq (trm_seq t_{1} t_{2}) t_{3}) H Q →
triple (trm_seq t_{1} (trm_seq t_{2} t_{3})) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (trm_seq (trm_seq t_{1} t_{2}) t_{3}) H Q →
triple (trm_seq t_{1} (trm_seq t_{2} t_{3})) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
Recall the specification for the function ref.
Its postcondition could be equivalently stated by using, instead
of an existential quantifier \∃, a pattern matching.
Parameter triple_ref' : ∀ v,
triple (val_ref v)
\[]
(fun r ⇒ match r with
| val_loc p ⇒ (p ~~> v)
| _ ⇒ \[False]
end).
triple (val_ref v)
\[]
(fun r ⇒ match r with
| val_loc p ⇒ (p ~~> v)
| _ ⇒ \[False]
end).
However, the pattern-matching presentation is less readable and
would be fairly cumbersome to work with in practice. Thus, we
systematically prefer using existentials.
Historical Notes
(* 2021-05-25 15:27 *)