Skip to content

GitLab

F
FloVer
Commit 7ac1c370 authored by ='s avatar =
Browse files
Options

New typing, proved sound. Also, expressions do not contain machine precision... 

New typing, proved sound. Also, expressions do not contain machine precision anymore in the case of variables
parent 777b1d10
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 959 additions and 717 deletions
coq/Commands.v
View file @ 7ac1c370
......@@ -49,14 +49,14 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Daisy language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
let_b m m' x e s E v res:
eval_exp E e v m ->
bstep s (updEnv x m v E) res m' ->
bstep (Let m x e s) E res m'
|ret_b m e E v:
eval_exp E e v m ->
bstep (Ret e) E v m.
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_exp E defVars e v m ->
bstep s (updEnv x m v E) defVars res m' ->
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_exp E defVars e v m ->
bstep (Ret e) E defVars v m.
......
coq/Environments.v
View file @ 7ac1c370
......@@ -22,7 +22,7 @@ Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Pr
approxEnv (updEnv x M0 v1 E1) A (NatSet.add x fVars) dVars (updEnv x m v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars m:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q m x))))%R ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x M0 v1 E1) A fVars (NatSet.add x dVars) (updEnv x m v2 E2).
......
coq/ErrorBounds.v
View file @ 7ac1c370
......@@ -7,9 +7,9 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType):
eval_exp E1 (Const M0 n) nR M0 ->
eval_exp E2 (Const m n) nF m ->
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType) defVars:
eval_exp E1 defVars (Const M0 n) nR M0 ->
eval_exp E2 defVars (Const m n) nF m ->
(Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
Proof.
intros eval_real eval_float.
......@@ -44,13 +44,13 @@ Qed.
*)
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Plus (Var R m1 1) (Var R m2 2)) vF m->
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1->
eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 defVars (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Plus (Var R 1) (Var R 2)) vF m->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R.
......@@ -74,11 +74,11 @@ Proof.
unfold perturb; simpl.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
unfold updEnv in H6,H9; simpl in *.
symmetry in H6,H9.
inversion H6; inversion H9; subst.
unfold updEnv in H1,H6; simpl in *.
symmetry in H1,H6.
inversion H1; inversion H6; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H9.
clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -89,9 +89,9 @@ Proof.
eapply Rle_trans.
apply H.
pose proof (Rabs_triang (e2R + - e2F) (- ((e1F + e2F) * delta))).
pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H1).
eapply Rle_trans.
apply H1.
apply H4.
rewrite <- Rplus_assoc.
repeat rewrite <- Rsub_eq_Ropp_Rplus.
rewrite Rabs_Ropp.
......@@ -109,13 +109,13 @@ Qed.
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1 ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Sub (Var R m1 1) (Var R m2 2)) vF m ->
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1 ->
eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 defVars (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Sub (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R.
......@@ -139,11 +139,12 @@ Proof.
unfold perturb; simpl.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
symmetry in H6, H9.
unfold updEnv in H6, H9; simpl in H6, H9.
inversion H6; inversion H9; subst.
simpl in H0; simpl in H5; inversion H0; inversion H5; subst; clear H0 H5.
symmetry in H6, H1.
unfold updEnv in H6, H1; simpl in H6, H1.
inversion H6; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H6 H9 H8.
clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H1 H6.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -167,13 +168,13 @@ Proof.
Qed.
Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1 ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Mult (Var R m1 1) (Var R m2 2)) vF m->
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1 ->
eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 defVars (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Mult (Var R 1) (Var R 2)) vF m->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
......@@ -195,9 +196,10 @@ Proof.
unfold perturb; simpl.
inversion H3; subst; inversion H6; subst.
unfold updEnv in *; simpl in *.
inversion H5; inversion H8; subst.
inversion H6; inversion H1; subst.
simpl in H8; simpl in H9; intros; inversion H5; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H5 H8.
clear mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -215,13 +217,13 @@ Proof.
Qed.
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType):
eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 (toRExp e1) e1F m1 ->
eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 (toRExp e2) e2F m2 ->
eval_exp E1 (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Div (Var R m1 1) (Var R m2 2)) vF m ->
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1 ->
eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 defVars (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Div (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
......@@ -243,9 +245,9 @@ Proof.
unfold perturb; simpl.
inversion H3; subst; inversion H9; subst.
unfold updEnv in *; simpl in *.
inversion H8; inversion H11; subst.
inversion H8; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear div_float H8 H11 div_real e1_real e1_float e2_real e2_float.
clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -440,10 +442,10 @@ Proof.
rewrite Q2R0_is_0; auto.
Qed.
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType):
eval_exp E1 (toREval e) nR M0 ->
eval_exp E2 e nF1 m ->
eval_exp (updEnv 1 m nF1 emptyEnv) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon->
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
eval_exp E1 defVars (toREval e) nR M0 ->
eval_exp E2 defVars e nF1 m ->
eval_exp (updEnv 1 m nF1 emptyEnv) defVars (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
(Rabs (nR - nF1) <= err)%R ->
(Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
Proof.
......@@ -456,8 +458,9 @@ Proof.
- apply Rplus_le_compat_l.
inversion eval_float_rnd; subst.
inversion H5; subst.
inversion H7.
inversion H0; subst.
unfold perturb; simpl.
unfold updEnv in H3; simpl in H3; inversion H3; subst.
replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra.
replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp).
rewrite Rabs_mult.
......
coq/Expressions.v
View file @ 7ac1c370
......@@ -52,6 +52,12 @@ Definition unopEqBool (o1:unop) (o2:unop) :=
| _ , _ => false
end.
Lemma unopEqBool_refl b:
unopEqBool b b = true.
Proof.
case b; auto.
Qed.
(**
Define evaluation for unary operators on reals.
Errors are added in the expression evaluation level later.
......@@ -69,7 +75,7 @@ Definition evalUnop (o:unop) (v:R):=
Will ease reasoning about different instantiations later.
**)
Inductive exp (V:Type): Type :=
Var: mType -> nat -> exp V
Var: nat -> exp V
| Const: mType -> V -> exp V
| Unop: unop -> exp V -> exp V
| Binop: binop -> exp V -> exp V -> exp V
......@@ -81,7 +87,7 @@ Inductive exp (V:Type): Type :=
**)
Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
match e1, e2 with
| Var _ m1 v1, Var _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2)
| Var _ v1, Var _ v2 => (v1 =? v2)
| Const m1 n1, Const m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2)
| Unop o1 e11, Unop o2 e22 => andb (unopEqBool o1 o2) (expEqBool e11 e22)
| Binop o1 e11 e12, Binop o2 e21 e22 => andb (binopEqBool o1 o2) (andb (expEqBool e11 e21) (expEqBool e12 e22))
......@@ -93,7 +99,7 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
Lemma expEqBool_refl e:
expEqBool e e = true.
Proof.
induction e; apply andb_true_iff; split; simpl in *; auto; try (apply EquivEqBoolEq; auto).
induction e; try (apply andb_true_iff; split); simpl in *; auto; try (apply EquivEqBoolEq; auto).
- symmetry; apply beq_nat_refl.
- apply Qeq_bool_iff; lra.
- case u; auto.
......@@ -122,9 +128,7 @@ Lemma expEqBool_sym e e':
Proof.
revert e'.
induction e; intros e'; destruct e'; simpl; try auto.
- f_equal.
+ apply mTypeEqBool_sym; auto.
+ apply beq_nat_sym.
- apply beq_nat_sym.
- f_equal.
+ apply mTypeEqBool_sym; auto.
+ apply Qeq_bool_sym.
......@@ -146,13 +150,12 @@ Lemma expEqBool_trans e f g:
expEqBool f g = true ->
expEqBool e g = true.
Proof.
revert e f g; induction e; destruct f; intros; simpl in H; inversion H; rewrite H; clear H; destruct g; simpl in H0; inversion H0; rewrite H0; clear H0; apply andb_true_iff in H1; destruct H1; apply andb_true_iff in H2; destruct H2; simpl.
- apply EquivEqBoolEq in H1.
apply EquivEqBoolEq in H.
apply beq_nat_true in H2.
apply beq_nat_true in H0.
revert e f g; induction e; destruct f; intros; simpl in H; inversion H; rewrite H; clear H; destruct g; simpl in H0; inversion H0; rewrite H0; clear H0; try (apply andb_true_iff in H1; destruct H1; apply andb_true_iff in H2; destruct H2; simpl).
- apply beq_nat_true in H2.
apply beq_nat_true in H1.
subst.
rewrite <- beq_nat_refl,mTypeEqBool_refl.
unfold expEqBool.
rewrite <- beq_nat_refl.
auto.
- apply EquivEqBoolEq in H1.
apply EquivEqBoolEq in H.
......@@ -186,7 +189,7 @@ Qed.
Fixpoint toRExp (e:exp Q) :=
match e with
|Var _ m v => Var R m v
|Var _ v => Var R v
|Const m n => Const m (Q2R n)
|Unop o e1 => Unop o (toRExp e1)
|Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
......@@ -195,7 +198,7 @@ Fixpoint toRExp (e:exp Q) :=
Fixpoint toREval (e:exp R) :=
match e with
| Var _ _ v => Var R M0 v
| Var _ v => Var R v
| Const _ n => Const M0 n
| Unop o e1 => Unop o (toREval e1)
| Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
......@@ -223,32 +226,33 @@ The result value expresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
**)
Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
Inductive eval_exp (E:env) (defVars: nat -> option mType) :(exp R) -> R -> mType -> Prop :=
| Var_load m x v:
defVars x = Some m ->
E x = Some (v, m) ->
eval_exp E (Var R m x) v m
eval_exp E defVars (Var R x) v m
| Const_dist m n delta:
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E (Const m n) (perturb n delta) m
eval_exp E defVars (Const m n) (perturb n delta) m
| Unop_neg m f1 v1:
eval_exp E f1 v1 m ->
eval_exp E (Unop Neg f1) (evalUnop Neg v1) m
eval_exp E defVars f1 v1 m ->
eval_exp E defVars (Unop Neg f1) (evalUnop Neg v1) m
| Unop_inv m f1 v1 delta:
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E f1 v1 m ->
eval_exp E (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
eval_exp E defVars f1 v1 m ->
eval_exp E defVars (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
| Binop_dist m1 m2 op f1 f2 v1 v2 delta:
Rle (Rabs delta) (Q2R (meps (computeJoin m1 m2))) ->
eval_exp E f1 v1 m1 ->
eval_exp E f2 v2 m2 ->
eval_exp E defVars f1 v1 m1 ->
eval_exp E defVars f2 v2 m2 ->
((op = Div) -> (~ v2 = 0)%R) ->
eval_exp E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (computeJoin m1 m2)
eval_exp E defVars (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (computeJoin m1 m2)
| Downcast_dist m m1 f1 v1 delta:
(* Downcast expression f1 (evaluating to machine type m1), to a machine type m, less precise than m1.*)
isMorePrecise m1 m = true ->
Rle (Rabs delta) (Q2R (meps m)) ->
eval_exp E f1 v1 m1 ->
eval_exp E (Downcast m f1) (perturb v1 delta) m.
eval_exp E defVars f1 v1 m1 ->
eval_exp E defVars (Downcast m f1) (perturb v1 delta) m.
(**
......@@ -257,7 +261,7 @@ Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
**)
Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
match e with
| Var _ _ x => NatSet.singleton x
| Var _ x => NatSet.singleton x
| Unop u e1 => usedVars e1
| Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
| Downcast _ e1 => usedVars e1
......@@ -277,17 +281,17 @@ Proof.
Qed.
Lemma general_meps_0_deterministic (f:exp R) (E:env):
Lemma general_meps_0_deterministic (f:exp R) (E:env) defVars:
forall v1 v2 m1,
m1 = M0 ->
eval_exp E (toREval f) v1 m1 ->
eval_exp E (toREval f) v2 M0 ->
eval_exp E defVars (toREval f) v1 m1 ->
eval_exp E defVars (toREval f) v2 M0 ->
v1 = v2.
Proof.
induction f; intros v1 v2 m1 m10_eq eval_v1 eval_v2.
induction f; intros * m10_eq eval_v1 eval_v2.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
rewrite H7 in H3; inversion H3; subst; auto.
rewrite H6 in H1; inversion H1; subst; auto.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
- inversion eval_v1; inversion eval_v2; subst; auto;
......@@ -324,10 +328,10 @@ Qed.
(**
Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (E:env):
Lemma meps_0_deterministic (f:exp R) (E:env) defVars:
forall v1 v2,
eval_exp E (toREval f) v1 M0 ->
eval_exp E (toREval f) v2 M0 ->
eval_exp E defVars (toREval f) v1 M0 ->
eval_exp E defVars (toREval f) v2 M0 ->
v1 = v2.
Proof.
intros v1 v2 ev1 ev2.
......@@ -342,31 +346,32 @@ For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
variables in the Environment.
**)
Lemma binary_unfolding b f1 f2 m E vF:
eval_exp E (Binop b f1 f2) vF m ->
Lemma binary_unfolding b f1 f2 m E vF defVars:
eval_exp E defVars (Binop b f1 f2) vF m ->
exists vF1 vF2 m1 m2,
m = computeJoin m1 m2 /\
eval_exp E f1 vF1 m1 /\
eval_exp E f2 vF2 m2 /\
eval_exp (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv))
(Binop b (Var R m1 1) (Var R m2 2)) vF m.
eval_exp E defVars f1 vF1 m1 /\
eval_exp E defVars f2 vF2 m2 /\
eval_exp (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv))
(fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n)
(Binop b (Var R 1) (Var R 2)) vF m.
Proof.
intros eval_float.
inversion eval_float; subst.
exists v1 ; exists v2; exists m1; exists m2; repeat split; try auto.
eapply Binop_dist; eauto.
pose proof (isMorePrecise_refl m1).
eapply Var_load; eauto.
pose proof (isMorePrecise_refl m2).
eapply Var_load; eauto.
- pose proof (isMorePrecise_refl m1).
eapply Var_load; eauto.
- pose proof (isMorePrecise_refl m2).
eapply Var_load; eauto.
Qed.
(* Analogous lemma for unary expressions. *)
Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R):
(eval_exp E (Unop Inv e) v m ->
Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R) defVars:
(eval_exp E defVars (Unop Inv e) v m ->
exists v1 m1,
eval_exp E e v1 m1 /\
eval_exp (updEnv 1 m1 v1 E) (Unop Inv (Var R m1 1)) v m).
eval_exp E defVars e v1 m1 /\
eval_exp (updEnv 1 m1 v1 E) (fun n => if (n =? 1) then Some m1 else defVars n) (Unop Inv (Var R 1)) v m).
Proof.
intros eval_un.
inversion eval_un; subst.
......
coq/Infra/RationalSimps.v
View file @ 7ac1c370
......@@ -80,3 +80,10 @@ Proof.
rewrite H0 in H; auto.
+ auto.
Qed.
Lemma Qeq_bool_refl v:
(Qeq_bool v v = true).
Proof.
apply Qeq_bool_iff; lra.
Qed.
\ No newline at end of file
coq/IntervalValidation.v
View file @ 7ac1c370
......@@ -13,7 +13,7 @@ Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
let (intv, _) := absenv e in
match e with
| Var _ _ v =>
| Var _ v =>
if NatSet.mem v validVars
then true
else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
......@@ -70,31 +70,26 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
match f with
| Let m x e g =>
if (validIntervalbounds e absenv P validVars &&
Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q m x)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q m x)))))
Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x)))))
then validIntervalboundsCmd g absenv P (NatSet.add x validVars)
else false
|Ret e =>
validIntervalbounds e absenv P validVars
end.
Theorem ivbounds_approximatesPrecond_sound f absenv P V Gamma:
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true ->
(exists mF, validType Gamma f mF) ->
(*(exists mF, validType Gamma f mF) ->*)
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
exists m, Gamma (Var Q m v) = Some m /\
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q m v)))).
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))).
Proof.
induction f; unfold validIntervalbounds.
- simpl. intros approx_true valid_tf v v_in_fV; simpl in *.
inversion valid_tf; subst.
- simpl. intros approx_true v v_in_fV; simpl in *.
rewrite NatSet.diff_spec in v_in_fV.
rewrite NatSet.singleton_spec in v_in_fV;
destruct v_in_fV; subst.
destruct valid_tf as [mF valid_tf].
inversion valid_tf; subst.
exists mF; split; auto.
destruct (absenv (Var Q mF n)); simpl in *.
destruct (absenv (Var Q n)); simpl in *.
case_eq (NatSet.mem n V); intros case_mem;
rewrite case_mem in approx_true; simpl in *.
+ rewrite NatSet.mem_spec in case_mem.
......@@ -102,27 +97,22 @@ Proof.
+ apply Is_true_eq_left in approx_true.
apply andb_prop_elim in approx_true.
destruct approx_true; auto.
- intros approx_true valid_tf v0 v_in_fV; simpl in *.
- intros approx_true v0 v_in_fV; simpl in *.
inversion v_in_fV.
- intros approx_unary_true valid_tf v v_in_fV; simpl in *.
- intros approx_unary_true v v_in_fV; simpl in *.
apply Is_true_eq_left in approx_unary_true.
simpl in *.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
apply andb_prop_elim in approx_unary_true.
destruct approx_unary_true.
apply IHf; try auto.
+ apply Is_true_eq_true; auto.
+ destruct valid_tf as [mF valid_tf].
inversion valid_tf; subst; auto.
exists mF; auto.
- intros approx_bin_true valid_tf v v_in_fV.
apply Is_true_eq_true; auto.
- intros approx_bin_true v v_in_fV.
simpl in v_in_fV.
rewrite NatSet.diff_spec in v_in_fV.
destruct v_in_fV as [ v_in_fV v_not_in_V].
rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_bin_true.
destruct valid_tf as [mf valid_tf].
inversion valid_tf; subst.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
......@@ -132,20 +122,17 @@ Proof.
destruct v_in_fV.
+ apply IHf1; try auto.
* apply Is_true_eq_true; auto.
* eauto.
* rewrite NatSet.diff_spec; split; auto.
+ apply IHf2; try auto.
* apply Is_true_eq_true; auto.
* eauto.
* rewrite NatSet.diff_spec; split; auto.
- intros approx_rnd_true [mf valid_tf] v v_in_fV.
- intros approx_rnd_true v v_in_fV.
simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f).
apply Is_true_eq_left in approx_rnd_true.
apply andb_prop_elim in approx_rnd_true.
destruct approx_rnd_true.
apply IHf; auto.
apply Is_true_eq_true in H; try auto.
inversion valid_tf; subst; eauto.
Qed.
Corollary Q2R_max4 a b c d:
......@@ -184,32 +171,31 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) Gamma:
forall vR m,
validType Gamma f m ->
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) defVars:
forall vR,
(* validType Gamma f m -> *)
validIntervalbounds f absenv P dVars = true ->
(forall v mV, NatSet.mem v dVars = true ->
exists vR mv, E v = Some (vR, M0) /\ Gamma (Var Q mv v) = Some mV /\
(Q2R (fst (fst (absenv (Var Q mV v)))) <= vR <= Q2R (snd (fst (absenv (Var Q mV v)))))%R) ->
(forall v, NatSet.mem v dVars = true ->
exists vR, E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some (vR, M0) /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
eval_exp E (toREval (toRExp f)) vR M0 ->
eval_exp E defVars (toREval (toRExp f)) vR M0 ->
(Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof.
induction f; intros vR mf typing_ok valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f.
induction f; intros vR valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f.
- unfold validIntervalbounds in valid_bounds.
env_assert absenv (Var Q m n) absenv_var.
env_assert absenv (Var Q n) absenv_var.
destruct absenv_var as [ iv [err absenv_var]].
specialize (valid_usedVars n).
simpl; rewrite absenv_var in *; simpl in *.
inversion eval_f; subst.