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.
Sequences
{H} t_{1} {fun _ => 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 _ ⇒ H_{1}) →
triple t_{2} H_{1} Q →
triple (trm_seq t_{1} t_{2}) H Q.
triple t_{1} H (fun _ ⇒ H_{1}) →
triple t_{2} H_{1} Q →
triple (trm_seq t_{1} t_{2}) H Q.
Exercise: 2 stars, standard, especially useful (triple_seq)
Prove triple_seq by unfolding triple and using eval_seq.
Proof using. (* FILL IN HERE *) Admitted.
☐
☐
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.
When we carry out proofs in practice, the application of the rule
triple_let produces a second sub-goal of the form, e.g.:
∀ v_{1}, triple (subst "a" v_{1} rest_of_the_program) (post1 v_{1}) post2,
where "a" denotes the name of the program variable that was bound by the
let-binding in the original source code. At this point, the user would
typically type intros a, to introduce the Coq variable v_{1} under the same
name that it had in the source code. This operations produces:
triple (subst "a" a rest_of_the_program) (post1 a) post2. At that point,
the user may call simpl to effectively replace all occurences of the
program variable "a" with the Coq variable a of type val. Doing so
produces: triple rest_of_the_program_updated (post1 a) post2, where
rest_of_the_program_updated refers to the Coq variable a. This process
will be illustrated in the proof of triple_incr further on.
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.
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 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 first rule for values is 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 triple_conseq_frame, triple_val_minimal, and xsimpl.
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 *)
☐
☐
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.
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} |
- If v_{1} was a program variable (that is, a trm_var) in the original source code, then this program variable should have been substituted by a Coq value or variable of type val by the time we reach this function call. Otherwise, the variable would correspond to a dangling free variable.
- If v_{1} is a Coq variable of type val but with no assumption of the form v_{1} = val_fun x t_{1}, it is probably the case that we already have established a specification lemma for the function v_{1} earlier in the reasoning. It this case, the rule above generally cannot be applied. Instead, one should apply the specification lemma for v_{1}, which is expected to have a conclusion of the form {..} (trm_app v_{1} ..) {..}, matching the proof obligation at hand.
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.
Technically, for a simple function such as addition, we could state a
specification in a similar form as triple_val, with an entailment of the
form H ==> Q v, as shown below.
Lemma triple_add' : ∀ H Q n_{1} n_{2},
H ==> Q (val_int (n_{1} + n_{2})) →
triple (val_add n_{1} n_{2}) H Q.
Proof using.
introv M. applys triple_conseq_frame.
{ applys triple_add. }
{ xsimpl. }
{ xpull. intros ? →. auto. }
Qed.
H ==> Q (val_int (n_{1} + n_{2})) →
triple (val_add n_{1} n_{2}) H Q.
Proof using.
introv M. applys triple_conseq_frame.
{ applys triple_add. }
{ xsimpl. }
{ xpull. intros ? →. auto. }
Qed.
Yet, this pattern does not generalize well to more complex functions with
nonempty preconditions. Instead, for specifying functions, we follow by
convention the pattern of "minimal footprint specifications", where the
precondition of the function covers no more than what the function needs to
access. For example:
There are a few situations where the precondition of a function may be an
over-approximation, to avoid complications. For example, a function that
gives the index of the first occurrence of a value v in a mutable list at
address p would typically be specified with a precondition of the form
MList p L describing the full linked list, rather than a precondition
describing the the smallest prefix of the list that reaches a cell with
value v.
- the add operation does not access the memory state, so it should be specified with \[] as precondition;
- the get operation on a reference accesses exactly one cell, so it should be specified using a precondition of the form p ~~> v;
- the mlist_length operation traverses one mutable linked list, so it should be specified using a precondition of the form MList p L.
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 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.
☐
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
Proof of incr
p := !p + 1 and in "A-normal form" as:
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).
In chapter Basic, we have seen that the proof of this lemma can be
completed by the short script xwp. xapp. xapp. xapp. xsimpl.. The purpose
of the detailed proof that follows is to explain how the x-tactics operate.
It shows how, under the hood, the proof exploits:
Executing the proof script step by step leads to the display of intermediate
proof obligations that involve Coq existential variables, a.k.a. "evars",
whose name is prefixed by a question mark, e.g., "?x". These placeholders
are typically introduced by applys (which calls eapply), and are
typically instantiated when solving subgoals.
- 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
Provide the argument name and body for incr.
{ reflexivity. }
Compute the substitution from program variable "p" to Coq variable p
simpl.
Reason about let n = ... Observe that this introduces an evar ?Q_{1}, which
denotes the postcondition of !p.
In the body of the let-binding, reason about !p. Here we are in a
favorable situation, where there is no need to apply a consequence or frame
rule.
Observe how ?Q_{1} has been instantiated as fun r ⇒ \[r = n] \* p ~~> n.
We next introduce a name n' for the result of !p
intros n'.
Once again, we compute the substitution of a program variable.
simpl.
We substitute away the equality n' = n.
Reason about let m = ... Observe the introduction of another evar ?Q_{1}.
Apply the frame rule to put aside p ~~> n.
We reason about n+1 in the empty state. Doing so instantiates ?Q_{1}.
We name m' the result of n+1.
intros m'. simpl.
We can extract the equality m' = n + 1 and substitute it away.
Finally, we reason about p := m.
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.
☐
☐
The job of the following chapters is to introduce additional technology to
streamline the proof process, notably by:
- automating the application of the frame rule, and
- eliminating the need to manipulate program variables and substitutions during verification.
A general principle is that if, according to the semantics, the terms t_{1}
and t_{2} admit 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.
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. But t_{1} may well require only a subset of the state H to
evaluate.
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
(* 2024-08-25 14:53 *)