Skip to content

GitLab

Commit 40a32997 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add explanation of isMorePrecise for fixed-points, rename M0 into REAL and... 

Add explanation of isMorePrecise for fixed-points, rename M0 into REAL and remove unused import from Expressions.v
parent 8a64fbf4
Hide whitespace changes
Inline Side-by-side
coq/CertificateChecker.v
View file @ 40a32997
......@@ -38,7 +38,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
CertificateChecker e absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRExp e) vF m /\
(forall vF m,
eval_expr E2 defVars (toRExp e) vF m ->
......@@ -93,7 +93,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
CertificateCheckerCmd f absenv P defVars = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
bstep (toRCmd f) E2 defVars vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
......
coq/Commands.v
View file @ 40a32997
......@@ -29,7 +29,7 @@ Fixpoint toRCmd (f:cmd Q) :=
Fixpoint toREvalCmd (f:cmd R) :=
match f with
|Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
|Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
|Ret e => Ret (toREval e)
end.
......
coq/ErrorBounds.v
View file @ 40a32997
......@@ -8,7 +8,7 @@ Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.Real
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_expr E1 (toRMap defVars) (Const M0 n) nR M0 ->
eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
eval_expr E2 defVars (Const m n) nF m ->
(Rabs (nR - nF) <= computeErrorR n m)%R.
Proof.
......@@ -31,11 +31,11 @@ Qed.
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Plus (Var R 1) (Var R 2)) vF m ->
......@@ -46,11 +46,11 @@ Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion plus_real; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join M0 M0) delta); auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join REAL REAL) delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
......@@ -104,11 +104,11 @@ Qed.
**)
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Sub (Var R 1) (Var R 2)) vF m ->
......@@ -119,8 +119,8 @@ Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -182,11 +182,11 @@ Qed.
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Mult (Var R 1) (Var R 2)) vF m ->
......@@ -195,8 +195,8 @@ Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -231,11 +231,11 @@ Qed.
Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Div (Var R 1) (Var R 2)) vF m ->
......@@ -244,8 +244,8 @@ Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -280,13 +280,13 @@ Qed.
Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(e3:expr Q) (e3R:R) (e3F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R REAL ->
eval_expr E2 defVars (toRExp e3) e3F m3->
eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
......@@ -294,9 +294,9 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
Proof.
intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
inversion fma_real; subst;
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in fma_real; auto.
rewrite delta_0_deterministic; auto.
......@@ -345,7 +345,7 @@ Proof.
Qed.
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (mEps m:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval e) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval e) nR REAL ->
eval_expr E2 defVars e nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
......
coq/ErrorValidation.v
View file @ 40a32997
......@@ -151,7 +151,7 @@ Qed.
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P fVars
dVars Gamma exprTypes:
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
typeCheck (Var Q v) Gamma exprTypes = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
validIntervalbounds (Var Q v) A P dVars = true ->
......@@ -181,7 +181,7 @@ Qed.
Lemma validErrorboundCorrectVariable:
forall E1 E2 A (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma exprTypes,
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
eval_expr E2 Gamma (toRExp (Var Q v)) nF mF ->
typeCheck (Var Q v) Gamma exprTypes = true ->
approxEnv E1 Gamma A fVars dVars E2 ->
......@@ -226,7 +226,7 @@ Proof.
Qed.
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma:
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR M0 ->
eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR REAL ->
exists nF m',
eval_expr E2 Gamma (toRExp (Const m n)) nF m'.
Proof.
......@@ -238,7 +238,7 @@ Proof.
Qed.
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR REAL ->
eval_expr E2 defVars (toRExp (Const m n)) nF m ->
typeCheck (Const m n) defVars Gamma = true ->
validErrorbound (Const m n) Gamma A dVars = true ->
......@@ -265,9 +265,9 @@ Lemma validErrorboundCorrectAddition E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -327,9 +327,9 @@ Lemma validErrorboundCorrectSubtraction E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -859,9 +859,9 @@ Lemma validErrorboundCorrectMult E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -930,9 +930,9 @@ Lemma validErrorboundCorrectDiv E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
m = join m1 m2 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
......@@ -1845,10 +1845,10 @@ Lemma validErrorboundCorrectFma E1 E2 A
(e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error)
(alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars (m m1 m2 m3:mType) Gamma defVars:
m = join3 m1 m2 m3 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 REAL ->
eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR REAL ->
eval_expr E2 defVars (toRExp e1) nF1 m1 ->
eval_expr E2 defVars (toRExp e2) nF2 m2 ->
eval_expr E2 defVars (toRExp e3) nF3 m3 ->
......@@ -1938,7 +1938,7 @@ Proof.
Qed.
Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
eval_expr E2 defVars (toRExp e) nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
......@@ -1981,7 +1981,7 @@ Theorem validErrorbound_sound (e:expr Q):
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
validErrorbound e Gamma A dVars = true ->
validIntervalbounds e A P dVars = true ->
dVars_range_valid dVars E1 A ->
......@@ -2029,7 +2029,7 @@ Proof.
- cbn in *. rewrite A_eq in *.
Flover_compute; try congruence; type_conv; subst; simpl in *.
inversion eval_real; subst.
assert (m0 = M0 /\ m3 = M0) as [? ?] by (split; eapply toRMap_eval_M0; eauto); subst.
assert (m0 = REAL /\ m3 = REAL) as [? ?] by (split; eapply toRMap_eval_REAL; eauto); subst.
destruct i as [ivlo1 ivhi1]; destruct i1 as [ivlo2 ivhi2];
rename e into err1; rename e3 into err2.
destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars)
......@@ -2120,7 +2120,7 @@ Proof.
- cbn in *. rewrite A_eq in *.
Flover_compute; try congruence; type_conv; subst; simpl in *.
inversion eval_real; subst.
assert (m0 = M0 /\ m4 = M0 /\ m5 = M0) as [? [? ?]] by (split; try split; eapply toRMap_eval_M0; eauto); subst.
assert (m0 = REAL /\ m4 = REAL /\ m5 = REAL) as [? [? ?]] by (split; try split; eapply toRMap_eval_REAL; eauto); subst.
destruct i as [ivlo1 ivhi1]; destruct i2 as [ivlo2 ivhi2]; destruct i1 as [ivlo3 ivhi3];
rename e into err1; rename e5 into err2; rename e4 into err3.
destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars)
......@@ -2175,7 +2175,7 @@ Proof.
auto. }
- cbn in *; Flover_compute; try congruence; type_conv; subst.
inversion eval_real; subst.
apply M0_least_precision in H1.
apply REAL_least_precision in H1.
subst.
destruct i0 as [ivlo_e ivhi_e]; rename e1 into err_e.
destruct (IHe E1 E2 fVars dVars A v1 err_e P ivlo_e ivhi_e Gamma defVars)
......@@ -2212,7 +2212,7 @@ Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validIntervalboundsCmd f A P dVars = true ->
dVars_range_valid dVars E1 A ->
......@@ -2273,7 +2273,7 @@ Proof.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto. }
{ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n M0 (toRMap defVars));
{ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm. }
{ intros v1 v1_mem.
unfold updEnv.
......@@ -2324,7 +2324,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
bstep (toRCmd f) E2 defVars vF mF ->
validErrorboundCmd f Gamma A dVars = true ->
validIntervalboundsCmd f A P dVars = true ->
......@@ -2385,7 +2385,7 @@ Proof.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
+ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n M0 (toRMap defVars));
+ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm.
+ intros v1 v1_mem.
unfold updEnv.
......
coq/Expressions.v
View file @ 40a32997
(**
Formalization of the base exprression language for the flover framework
**)
From Coq
Require Import Structures.Orders.
From Flover
Require Import Infra.RealRationalProps Infra.Ltacs.
......@@ -127,16 +124,16 @@ Fixpoint toRExp (e:expr Q) :=
Fixpoint toREval (e:expr R) :=
match e with
| Var _ v => Var R v
| Const _ n => Const M0 n
| Const _ n => Const REAL n
| Unop o e1 => Unop o (toREval e1)
| Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
| Fma e1 e2 e3 => Fma (toREval e1) (toREval e2) (toREval e3)
| Downcast _ e1 => Downcast M0 (toREval e1)
| Downcast _ e1 => Downcast REAL (toREval e1)
end.
Definition toRMap (d:nat -> option mType) (n:nat) :=
match d n with
| Some m => Some M0
| Some m => Some REAL
| None => None
end.
......@@ -151,7 +148,7 @@ Arguments toRMap _ _/.
Definition perturb (rVal:R) (m:mType) (delta:R) :R :=
match m with
(* The Real-type has no error *)
|M0 => rVal
|REAL => rVal
(* Fixed-point numbers have an absolute error *)
|F w f => rVal + delta
(* Floating-point numbers have a relative error *)
......@@ -299,8 +296,8 @@ Fixpoint usedVars (V:Type) (e:expr V) :NatSet.t :=
| _ => NatSet.empty
end.
Lemma toRMap_eval_M0 f v E Gamma m:
eval_expr E (toRMap Gamma) (toREval f) v m -> m = M0.
Lemma toRMap_eval_REAL f v E Gamma m:
eval_expr E (toRMap Gamma) (toREval f) v m -> m = REAL.
Proof.
revert v E Gamma m.
induction f; intros * eval_f; inversion eval_f; subst;
......@@ -313,16 +310,16 @@ Proof.
end; try auto.
- eapply IHf; eauto.
- eapply IHf; eauto.
- assert (m1 = M0)
- assert (m1 = REAL)
by (eapply IHf1; eauto).
assert (m2 = M0)
assert (m2 = REAL)
by (eapply IHf2; eauto);
subst; auto.
- assert (m1 = M0)
- assert (m1 = REAL)
by (eapply IHf1; eauto).
assert (m2 = M0)
assert (m2 = REAL)
by (eapply IHf2; eauto).
assert (m3 = M0)
assert (m3 = REAL)
by (eapply IHf3; eauto);
subst; auto.
Qed.
......@@ -343,8 +340,8 @@ Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:expr R) (E:env) Gamma:
forall v1 v2,
eval_expr E (toRMap Gamma) (toREval f) v1 M0 ->
eval_expr E (toRMap Gamma) (toREval f) v2 M0 ->
eval_expr E (toRMap Gamma) (toREval f) v1 REAL ->
eval_expr E (toRMap Gamma) (toREval f) v2 REAL ->
v1 = v2.
Proof.
induction f;
......@@ -358,27 +355,27 @@ Proof.
+ rewrite (IHf v0 v3); eauto.
+ cbn in H1, H8. subst. rewrite (IHf v0 v3); eauto.
- inversion ev1; inversion ev2; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v4); try auto.
rewrite (IHf2 v3 v5); try auto.
- inversion ev1; inversion ev2; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v5); try auto.
rewrite (IHf2 v3 v6); try auto.
rewrite (IHf3 v4 v7); try auto.
- inversion ev1; inversion ev2; subst.
apply M0_least_precision in H1;
apply M0_least_precision in H7; subst.
apply REAL_least_precision in H1;
apply REAL_least_precision in H7; subst.
rewrite (IHf v0 v3); try auto.
Qed.
......
coq/FPRangeValidator.v
View file @ 40a32997
......@@ -196,7 +196,7 @@ Proof.
- rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ eapply (swap_Gamma_bstep (Gamma1 := updDefVars n M0 (toRMap Gamma))); eauto.
{ eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
eauto using Rmap_updVars_comm. }
{ set_tac; split.
- split; try auto.
......
coq/IEEE_connection.v
View file @ 40a32997
......@@ -911,7 +911,7 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
validIntervalboundsCmd (B2Qcmd f) A P dVars = true ->
validErrorboundCmd (B2Qcmd f) tMap A dVars = true ->
FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true ->
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) vR M0 ->
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) vR REAL ->
bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma vF M64 ->
NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
is64BitBstep (B2Qcmd f) ->
......@@ -1017,7 +1017,7 @@ Proof.
split; try auto. split; try auto.
hnf; intros; subst. apply H2. rewrite NatSet.add_spec. auto.
rewrite NatSet.add_spec in H2. hnf; intros; apply H2; auto.
- eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
- eapply (swap_Gamma_bstep (Gamma1:= updDefVars n REAL (toRMap Gamma)));
eauto.
intros; unfold updDefVars, toRMap.
destruct (n0 =? n); auto.
......@@ -1077,7 +1077,7 @@ Proof.
* rewrite NatSet.add_spec in H1;
rewrite NatSet.union_spec, NatSet.add_spec in *;
destruct H1; auto. destruct H1; auto.
+ eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
+ eapply (swap_Gamma_bstep (Gamma1:= updDefVars n REAL (toRMap Gamma)));
eauto.
intros; unfold updDefVars, toRMap.
destruct (n0 =? n); auto.
......@@ -1180,7 +1180,7 @@ Theorem IEEE_connection_expr e A P E1 E2 defVars:
CertificateChecker (B2Qexpr e) A P defVars = true ->
exists iv err vR vF, (* m, currently = M64 *)
FloverMap.find (B2Qexpr e) A = Some (iv, err) /\
eval_expr E1 (toRMap defVars) (toREval (toRExp (B2Qexpr e))) vR M0 /\
eval_expr E1 (toRMap defVars) (toREval (toRExp (B2Qexpr e))) vR REAL /\
eval_expr_float e E2 = Some vF /\
eval_expr (toREnv E2) defVars (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
(Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
......@@ -1226,7 +1226,7 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
CertificateCheckerCmd (B2Qcmd f) A P defVars = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) vR M0 /\
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) vR REAL /\
bstep_float f E2 = Some vF /\
bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (Q2R (B2Q vF)) m /\
(forall vF m,
......
coq/Infra/MachineType.v
View file @ 40a32997
......@@ -18,7 +18,7 @@ From Flover
like Flocq, where f:positive specifies the fraction size and w: the width of
the base field.
**)
Inductive mType: Type := M0 | M16 | M32 | M64
Inductive mType: Type := REAL | M16 | M32 | M64
| F (w:positive) (f:positive). (*| M128 | M256*)
(**
......@@ -26,7 +26,7 @@ Inductive mType: Type := M0 | M16 | M32 | M64
**)
Definition mTypeToR (m:mType) :R :=
match m with
| M0 => 0%R
| REAL => 0%R
| M16 => 1 / 2^11
| M32 => 1/ 2^24
| M64 => 1/ 2^53
......@@ -40,7 +40,7 @@ Definition mTypeToR (m:mType) :R :=
Definition mTypeToQ (m:mType) :Q :=
match m with
| M0 => 0
| REAL => 0
| M16 => (Qpower (2#1) (Zneg 11))
| M32 => (Qpower (2#1) (Zneg 24))
| M64 => (Qpower (2#1) (Zneg 53))
......@@ -54,14 +54,14 @@ Definition mTypeToQ (m:mType) :Q :=
Definition computeErrorR v m :R :=
match m with
|M0 => 0
|REAL => 0
|F w f => mTypeToR m
|_ => Rabs v * mTypeToR m
end.
Definition computeErrorQ v m :Q :=
match m with
|M0 => 0
|REAL =></