RulesReasoning Rules for Term Constructs
Set Implicit Arguments.
From SLF Require Export LibSepReference.
From SLF Require Basic.
Implicit Types n : int.
Implicit Types t : trm.
Implicit Types r v : val.
Implicit Types p : loc.
Implicit Types H : hprop.
Implicit Types Q : val→hprop.
From SLF Require Export LibSepReference.
From SLF Require Basic.
Implicit Types n : int.
Implicit Types t : trm.
Implicit Types r v : val.
Implicit Types p : loc.
Implicit Types H : hprop.
Implicit Types Q : val→hprop.
First Pass
Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
∀ s, H s → eval s t Q.
Reasoning Rule for Sequences
{H} t_{1} {fun v => H_{1}} {H_{1}} t_{2} {Q} | |
{H} (t_{1};t_{2}) {Q} |
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.
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}. It is
unconstrained in the rule. For well-typed programs, this result is
necessarily the unit value. For untyped programs, the result of t_{1} is
simply irrelevant.
Exercise: 2 stars, standard, especially useful (triple_seq)
Prove triple_seq by unfolding triple and using eval_seq.
Proof using. (* FILL IN HERE *) Admitted.
☐
☐
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} |
Lemma 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.
Proof using. introv M_{1} M_{2} Hs. applys* eval_let. Qed.
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.
Proof using. introv M_{1} M_{2} Hs. applys* eval_let. Qed.
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} |
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.
(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.
Exercise: 2 stars, standard, especially useful (triple_if_case)
Prove triple_if_case by unfolding triple and using eval_if. Hint: use the tactic case_if to perform a case analysis.
Proof using. (* FILL IN HERE *) Admitted.
☐
☐
Lemma triple_if : ∀ (b:bool) t_{1} t_{2} H Q,
triple (if b then t_{1} else t_{2}) H Q →
triple (trm_if b t_{1} t_{2}) H Q.
Proof using. introv M Hs. applys* eval_if. Qed.
triple (if b then t_{1} else t_{2}) H Q →
triple (trm_if b t_{1} t_{2}) H Q.
Proof using. introv M Hs. applys* eval_if. Qed.
Reasoning Rule for Values
{\[]} v {fun r => \[r = v]} |
H ==> Q v | |
{H} v {Q} |
Lemma triple_val : ∀ v H Q,
H ==> Q v →
triple (trm_val v) H Q.
Proof using. introv M Hs. applys* eval_val. Qed.
H ==> Q v →
triple (trm_val v) H Q.
Proof using. introv M Hs. applys* eval_val. Qed.
It may not be completely obvious at first sight why triple_val is
equivalent to the "minimalistic" rule {\[]} v {fun r ⇒ \[r = v]}. Let us
prove the equivalence.
Exercise: 1 star, standard, especially useful (triple_val_minimal)
Prove that the 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. Concretely, your goal is to prove triple_val' without unfolding the definition of triple. Use xsimpl, triple_val_minimal and the structural rules on triple such as triple_conseq_frame.
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.
(* FILL IN HERE *)
☐
☐
Reasoning Rule for Function Definitions
{\[]} (trm_fun x t_{1}) {fun r => \[r = val_fun x t_{1}]} |
Lemma triple_fun : ∀ x t_{1} H Q,
H ==> Q (val_fun x t_{1}) →
triple (trm_fun x t_{1}) H Q.
Proof using. introv M Hs. applys* eval_fun. Qed.
H ==> Q (val_fun x t_{1}) →
triple (trm_fun x t_{1}) H Q.
Proof using. introv M Hs. applys* eval_fun. Qed.
This reasoning rules for functions generalizes to recursive functions. A
term describing a recursive function is written trm_fix f x t_{1}, and the
corresponding value is written val_fix f x t_{1}.
Lemma 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.
Proof using. introv M Hs. applys* eval_fix. Qed.
H ==> Q (val_fix f x t_{1}) →
triple (trm_fix f x t_{1}) H Q.
Proof using. introv M Hs. applys* eval_fix. Qed.
Reasoning Rule for Function Calls
v_{1} = val_fun x t_{1} {H} (subst x v_{2} t_{1}) {Q} | |
{H} (trm_app v_{1} v_{2}) {Q} |
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 Hs. applys* eval_app_fun. 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 Hs. applys* eval_app_fun. Qed.
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.
Lemma 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.
Proof using. introv E M Hs. applys* eval_app_fix. Qed.
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 using. introv E M Hs. applys* eval_app_fix. Qed.
This concludes the presentation of the reasoning rules for term constructs.
Before we can tackle the verification of actual programs, there remains to
present the specifications for the primitive operations. We start with
arithmetic operations, then consider heap-manipulating operations.
Addition
Parameter 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.
Q (val_int (n_{1} + n_{2})) s →
eval s (val_add (val_int n_{1}) (val_int n_{2})) Q.
In the specification shown below, the precondition is written \[] and the
postcondition binds a return value r of type val specified to be equal
to val_int (n_{1}+n_{2}).
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.
introv Hs. applys* eval_add. lets ->: hempty_inv Hs.
applys hpure_intro. auto.
Qed.
triple (val_add n_{1} n_{2})
\[]
(fun r ⇒ \[r = val_int (n_{1} + n_{2})]).
Proof using.
introv Hs. applys* eval_add. lets ->: hempty_inv Hs.
applys hpure_intro. auto.
Qed.
Division
Parameter 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.
Lemma 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.
introv Hn_{2} Hs. applys* eval_div. lets ->: hempty_inv Hs.
applys hpure_intro. auto.
Qed.
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.
Lemma 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.
introv Hn_{2} Hs. applys* eval_div. lets ->: hempty_inv Hs.
applys hpure_intro. auto.
Qed.
Random-Number Generation
Parameter 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.
n > 0 →
(∀ n_{1}, 0 ≤ n_{1} < n → Q n_{1} s) →
eval s (val_rand (val_int n)) Q.
The postcondition of the triple for val_rand n asserts that the output
value r corresponds to an integer n_{1}, in the range from 0 ≤ n_{1} < n.
Exercise: 2 stars, standard, especially useful (triple_rand)
Prove the reasoning rule for calls to the random number generator.
Lemma triple_rand : ∀ n,
n > 0 →
triple (val_rand n)
\[]
(fun r ⇒ \[∃ n_{1}, r = val_int n_{1} ∧ 0 ≤ n_{1} < n]).
Proof using. (* FILL IN HERE *) Admitted.
☐
n > 0 →
triple (val_rand n)
\[]
(fun r ⇒ \[∃ n_{1}, r = val_int n_{1} ∧ 0 ≤ n_{1} < n]).
Proof using. (* FILL IN HERE *) Admitted.
☐
Rules for Primitive Heap-Manipulating Operations
Allocation
Lemma triple_ref : ∀ v,
triple (val_ref v)
\[]
(fun r ⇒ \∃ p, \[r = val_loc p] \* p ~~> v).
Proof using.
intros. intros s_{1} K. applys eval_ref. intros p D.
lets ->: hempty_inv K. rewrite Fmap.update_empty.
applys hexists_intro p. rewrite hstar_hpure_l. split*.
applys hsingle_intro.
Qed.
triple (val_ref v)
\[]
(fun r ⇒ \∃ p, \[r = val_loc p] \* p ~~> v).
Proof using.
intros. intros s_{1} K. applys eval_ref. intros p D.
lets ->: hempty_inv K. rewrite Fmap.update_empty.
applys hexists_intro p. rewrite hstar_hpure_l. split*.
applys hsingle_intro.
Qed.
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.
Lemma triple_ref' : ∀ v,
triple (val_ref v)
\[]
(funloc p ⇒ p ~~> v).
Proof using. apply triple_ref. Qed.
triple (val_ref v)
\[]
(funloc p ⇒ p ~~> v).
Proof using. apply triple_ref. Qed.
Deallocation
Exercise: 2 stars, standard, especially useful (triple_free')
Prove the reasoning rule for deallocation of a single cell. Hint: use Fmap.indom_single and Fmap.remove_single.
Lemma triple_free' : ∀ p v,
triple (val_free (val_loc p))
(p ~~> v)
(fun r ⇒ \[r = val_unit]).
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (val_free (val_loc p))
(p ~~> v)
(fun r ⇒ \[r = val_unit]).
Proof using. (* FILL IN HERE *) Admitted.
☐
Lemma triple_free : ∀ p v,
triple (val_free (val_loc p))
(p ~~> v)
(fun _ ⇒ \[]).
Proof using. intros. applys triple_conseq triple_free'; xsimpl*. Qed.
triple (val_free (val_loc p))
(p ~~> v)
(fun _ ⇒ \[]).
Proof using. intros. applys triple_conseq triple_free'; xsimpl*. Qed.
Read
Lemma triple_get : ∀ v p,
triple (val_get p)
(p ~~> v)
(fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
intros. intros s K. lets ->: hsingle_inv K. applys eval_get.
{ applys* Fmap.indom_single. }
{ rewrite hstar_hpure_l. split*. rewrite* Fmap.read_single. }
Qed.
triple (val_get p)
(p ~~> v)
(fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
intros. intros s K. lets ->: hsingle_inv K. applys eval_get.
{ applys* Fmap.indom_single. }
{ rewrite hstar_hpure_l. split*. rewrite* Fmap.read_single. }
Qed.
Write
Exercise: 2 stars, standard, especially useful (triple_set)
Prove the reasoning rule for a write operation. Hint: use Fmap.update_single.
Lemma triple_set : ∀ w p v,
triple (val_set (val_loc p) v)
(p ~~> w)
(fun r ⇒ \[r = val_unit] \* (p ~~> v)).
Proof using. (* FILL IN HERE *) Admitted.
☐
triple (val_set (val_loc p) v)
(p ~~> w)
(fun r ⇒ \[r = val_unit] \* (p ~~> v)).
Proof using. (* FILL IN HERE *) Admitted.
☐
Program Verification using the Reasoning Rules of 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 embedded programming language, the definition of incr is formalized 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
more concisely.
Let us check that the two definitions are indeed the same.
Recall from the first chapter the specification of the increment function.
Its precondition requires a singleton state of the form p ~~> n. Its
postcondition describes a state of the form p ~~> (n+1).
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_conseq_frame.
{ applys triple_set. }
{ xsimpl. }
{ xsimpl. }
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_conseq_frame.
{ applys triple_set. }
{ xsimpl. }
{ xsimpl. }
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. Use applys triple_seq for reasoning about a sequence. Use applys triple_val for reasoning about the final return value, namely x.
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.
A general principle is that if, according to the semantics, the terms t_{1}
and t_{2} admits the same behaviors, then t_{1} and t_{2} satisfy the same
triples. The statement can also be reformulated in an asymmetric fashion: if
t_{2} admits no more behaviors than t_{1}, then t_{2} satisfies all the triples
that t_{1} satisfies. This section explains how to formalize this asymmetric
statement, which is more general and more useful in practice than the
statement expressed in terms of equivalences.
The judgment eval_like t_{1} t_{2} asserts that if t_{1} terminates and produces
results in Q, then so does t_{2}.
Exercise: 1 star, standard, especially useful (eval_like_eta_expansion)
Prove that when the relation eval_like t_{1} t_{2} holds, any triple that t_{2} satisfies any triple that t_{1} satisfies.
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. (* FILL IN HERE *) Admitted.
☐
eval_like t_{1} t_{2} →
triple t_{1} H Q →
triple t_{2} H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
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.
introv Hv. applys eval_val Hv.
Qed.
eval_like t (trm_let x t x).
Proof using.
introv R. applys eval_let R.
simpl. rewrite var_eq_spec. case_if.
introv Hv. applys eval_val Hv.
Qed.
Exercise: 4 stars, standard, optional (eval_like_eta_expansion)
Prove that the symmetric relation eval_like (trm_let x t x) t also holds.
Lemma eval_like_eta_expansion : ∀ (t:trm) (x:var),
eval_like (trm_let x t x) t.
Proof using. (* FILL IN HERE *) Admitted.
☐
eval_like (trm_let x t x) t.
Proof using. (* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, especially useful (eta_same_triples)
Conclude that t and trm_let x t x satisfy exactly the same set of triples. (This result will be exploited in chapter Affine, for proving the equivalence of two versions of the garbage collection rule.)
Lemma eta_same_triples : ∀ (t:trm) (x:var) H Q,
triple t H Q ↔ triple (trm_let x t x) H Q.
Proof using. (* FILL IN HERE *) Admitted.
☐
triple t H Q ↔ triple (trm_let x t x) 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.
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.
A even more interesting application is a rule that allows to modify the
parenthesis structure of a sequence, from t_{1}; (t_{2}; t_{3}) to (t_{1};t_{2}); t_{3}.
Such a change in the parenthesis structure of a sequence might be helfpul to
apply the frame rule around t_{1};t_{2}, for example.
Exercise: 3 stars, standard, optional (triple_trm_seq_assoc)
Prove that the term t_{1}; (t_{2}; t_{3}), which corresponds to the natural parsing of t_{1}; t_{2}; t_{3}, satisfies any triple that the term (t_{1};t_{2}); t_{3} satisfies.
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 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.
☐
☐
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})]).
The two presentations are equivalent. First, let us prove triple_div'
using triple_div.
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.
intros. applys triple_hpure'. applys triple_div.
Qed.
triple (val_div n_{1} n_{2})
\[n_{2} ≠ 0]
(fun r ⇒ \[r = val_int (Z.quot n_{1} n_{2})]).
Proof using.
intros. applys triple_hpure'. applys triple_div.
Qed.
Exercise: 2 stars, standard, especially useful (triple_div_from_triple_div')
Prove triple_div using triple_div'.
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.
☐
Recall the specification for the function ref.
Its postcondition could be equivalently stated by using, instead of an
existential quantifier, a pattern matching construct.
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.
In this section, the corollary triple_hpure' established in the previous
chapter, can be useful.
Recall the function repeat_incr from chapter Basic.
let rec factorec n =
if n ≤ 1 then 1 else n * factorec (n-1)
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. Use triple_hpure', the corollary of triple_hpure. Exploit triple_le and triple_sub and triple_mul to reason about the behavior of the primitive operations involved. Exploit applys triple_if. case_if as C. to reason about the conditional; alternatively, if using triple_if_case, you'll need to use the tactic rew_bool_eq in * to simplify, e.g., the expression isTrue (m ≤ 1)) = true.
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.
☐
Historical Notes
(* 2023-11-29 09:22 *)