Commit cc749eb4 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Update error bounds proofs

parent fcc58289
...@@ -258,6 +258,28 @@ Proof. ...@@ -258,6 +258,28 @@ Proof.
apply Rabs_pos. apply Rabs_pos.
Qed. Qed.
Lemma fma_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(e3:exp Q) (e3R:R) (e3F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 err3:Q) (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
eval_exp E2 defVars (toRExp e1) e1F m1->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
eval_exp E2 defVars (toRExp e3) e3F m1->
eval_exp E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
eval_exp (upd Env 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 ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (e3R - e3F) <= Q2R err3)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%R.
(Rabs (vR - vF) <= Rabs (err1 + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R.
Proof.
Qed.
Lemma err_prop_inversion_pos_real nF nR err elo ehi Lemma err_prop_inversion_pos_real nF nR err elo ehi
(float_iv_pos : (0 < elo - err)%R) (float_iv_pos : (0 < elo - err)%R)
(real_iv_pos : (0 < elo)%R) (real_iv_pos : (0 < elo)%R)
......
...@@ -79,13 +79,9 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *) ...@@ -79,13 +79,9 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
let upperBoundE1 := maxAbs ive1 in let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in let upperBoundE2 := maxAbs ive2 in
let upperBoundE3 := maxAbs ive3 in let upperBoundE3 := maxAbs ive3 in
Qleb (err1 + (err2 * err3)) err let errIntv_prod := multIntv errIve2 errIve3 in
(* match b with *) let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
(* | Plus => *) Qleb (err1 + mult_error_bound + (maxAbs (addIntv errIntv_prod errIve1)) * (mTypeToQ m)) err
(* Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err *)
(* | Mult => *)
(* Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err *)
(* end *)
else false else false
|Downcast m1 e1 => |Downcast m1 e1 =>
if validErrorbound e1 typeMap A dVars if validErrorbound e1 typeMap A dVars
...@@ -1940,6 +1936,39 @@ Proof. ...@@ -1940,6 +1936,39 @@ Proof.
rewrite (Qmult_inj_r) in H4; auto. } rewrite (Qmult_inj_r) in H4; auto. }
Qed. Qed.
Lemma validErrorboundCorrectFma E1 E2 absenv
(e1:exp Q) (e2:exp Q) (e3: exp 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_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) nR3 M0 ->
eval_exp E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR M0 ->
eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp E2 defVars (toRExp e3) nF3 m3 ->
eval_exp (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(toRExp (Fma (Var Q 1) (Var Q 2) (Var Q 3))) nF m ->
typeCheck (Fma e1 e2 e3) defVars Gamma = true ->
validErrorbound (Fma e1 e2 e3) Gamma absenv dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
(Q2R e3lo <= nR3 <= Q2R e3hi)%R ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv e3 = ((e3lo, e3hi),err3) ->
absenv (Fma e1 e2 e3) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR3 - nF3) <= (Q2R err3))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float
subexpr_ok valid_error valid_e1 valid_e2 valid_e3 absenv_e1 absenv_e2 absenv_e3 absenv_mult
err1_bounded err2_bounded err3_bounded.
eapply Rle_trans.
Admitted.
Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars: Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 -> eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
...@@ -2170,7 +2199,74 @@ Proof. ...@@ -2170,7 +2199,74 @@ Proof.
{ simpl; rewrite absenv_eq, type_b, L, L2, R1; simpl. { simpl; rewrite absenv_eq, type_b, L, L2, R1; simpl.
rewrite absenv_e1, absenv_e2; auto. } rewrite absenv_e1, absenv_e2; auto. }
{ andb_to_prop R; auto. } { andb_to_prop R; auto. }
- admit. - simpl in valid_error.
destruct (absenv e1) as [[ivlo1 ivhi1] err1] eqn:absenv_e1;
destruct (absenv e2) as [[ivlo2 ivhi2] err2] eqn:absenv_e2;
destruct (absenv e3) as [[ivlo3 ivhi3] err3] eqn:absenv_e3.
subst; simpl in *.
rewrite absenv_eq, absenv_e1, absenv_e2, absenv_e3 in *.
case_eq (Gamma (Fma e1 e2 e3));
intros * type_fma; rewrite type_fma in *; [ | inversion valid_error ].
case_eq (Gamma e1);
intros * type_e1; rewrite type_e1 in typing_ok; [ | inversion typing_ok ].
case_eq (Gamma e2);
intros * type_e2; rewrite type_e2 in typing_ok; [ | inversion typing_ok ].
case_eq (Gamma e3);
intros * type_e3; rewrite type_e3 in typing_ok; [ | inversion typing_ok ].
repeat match goal with
| [H: _ = true |- _] => andb_to_prop H
end.
type_conv.
inversion eval_real; subst.
assert (m3 = M0 /\ m4 = M0 /\ m5 = M0) as [? [? ?]] by (split; try split; eapply toRMap_eval_M0; eauto); subst.
destruct (IHe1 E1 E2 fVars dVars absenv v1 err1 P ivlo1 ivhi1 Gamma defVars)
as [[vF1 [mF1 eval_float_e1]] bounded_e1];
try auto; set_tac.
destruct (IHe2 E1 E2 fVars dVars absenv v2 err2 P ivlo2 ivhi2 Gamma defVars)
as [[vF2 [mF2 eval_float_e2]] bounded_e2];
try auto; set_tac.
destruct (IHe3 E1 E2 fVars dVars absenv v3 err3 P ivlo3 ivhi3 Gamma defVars)
as [[vF3 [mF3 eval_float_e3]] bounded_e3];
try auto; set_tac.
destruct (validIntervalbounds_sound _ _ _ E1 defVars L (fVars := fVars) (dVars:=dVars))
as [v1' [eval_real_e1 bounds_e1]];
try auto; set_tac.
rewrite absenv_e1 in bounds_e1.
pose proof (meps_0_deterministic _ eval_real_e1 H5); subst. clear H5.
destruct (validIntervalbounds_sound _ _ _ E1 defVars R1 (fVars:= fVars) (dVars:=dVars))
as [v2' [eval_real_e2 bounds_e2]];
try auto; set_tac.
rewrite absenv_e2 in bounds_e2; simpl in *.
pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6.
destruct (validIntervalbounds_sound _ _ _ E1 defVars R0 (fVars:= fVars) (dVars:=dVars))
as [v3' [eval_real_e3 bounds_e3]];
try auto; set_tac.
rewrite absenv_e3 in bounds_e3; simpl in *.
pose proof (meps_0_deterministic _ eval_real_e3 H7); subst; clear H7.
split.
+ repeat eexists; econstructor; eauto.
rewrite Rabs_right; try lra.
instantiate (1 := 0%R).
apply mTypeToQ_pos_R.
apply Rle_ge.
hnf; right. reflexivity.
+ intros * eval_float.
clear eval_float_e1 eval_float_e2 eval_float_e3.
inversion eval_float; subst.
eapply (fma_unfolding H4 H5 H8 H9) in eval_float; try auto.
eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) absenv); eauto.
{ simpl.
rewrite type_fma.
rewrite type_e1.
rewrite type_e2.
rewrite type_e3.
rewrite mTypeEq_refl, R5, R6, R7; auto. }
{ simpl.
rewrite absenv_eq.
rewrite type_fma.
rewrite R, L1, L2, R4; simpl.
rewrite absenv_e1, absenv_e2, absenv_e3.
auto. }
- destruct (absenv e) as [[ivlo_e ivhi_e] err_e] eqn: absenv_e. - destruct (absenv e) as [[ivlo_e ivhi_e] err_e] eqn: absenv_e.
subst; simpl in *. subst; simpl in *.
rewrite absenv_eq, absenv_e in *. rewrite absenv_eq, absenv_e in *.
...@@ -2217,7 +2313,7 @@ Proof. ...@@ -2217,7 +2313,7 @@ Proof.
rewrite L0; auto. rewrite L0; auto.
Unshelve. Unshelve.
intros. auto. intros. auto.
Admitted. Qed.
Theorem validErrorboundCmd_gives_eval (f:cmd Q) : Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
forall (absenv:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err P Gamma defVars, forall (absenv:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err P Gamma defVars,
......
...@@ -474,7 +474,7 @@ Proof. ...@@ -474,7 +474,7 @@ Proof.
Qed. Qed.
(** (**
Helping lemma. Needed in soundness proof. Helping lemmas. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different evaluating the subexpressions and then binding the result values to different
variables in the Environment. variables in the Environment.
...@@ -493,6 +493,19 @@ Proof. ...@@ -493,6 +493,19 @@ Proof.
econstructor; try auto. econstructor; try auto.
Qed. Qed.
Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 Gamma delta:
(Rabs delta <= Q2R (mTypeToQ (join3 m1 m2 m3)))%R ->
eval_exp E Gamma f1 v1 m1 ->
eval_exp E Gamma f2 v2 m2 ->
eval_exp E Gamma f3 v3 m3 ->
eval_exp E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3) ->
eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
(Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3).
Proof.
econstructor; try auto.
Qed.
Lemma eval_eq_env e: Lemma eval_eq_env e:
forall E1 E2 Gamma v m, forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) -> (forall x, E1 x = E2 x) ->
......
...@@ -149,6 +149,8 @@ Proof. ...@@ -149,6 +149,8 @@ Proof.
prove_fprangeval m v L1 R. prove_fprangeval m v L1 R.
- andb_to_prop H4. - andb_to_prop H4.
prove_fprangeval m v L1 R. prove_fprangeval m v L1 R.
- andb_to_prop H4.
prove_fprangeval m v L1 R.
Qed. Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q): Lemma FPRangeValidatorCmd_sound (f:cmd Q):
......
...@@ -45,6 +45,11 @@ Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option fl64):= ...@@ -45,6 +45,11 @@ Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option fl64):=
end end
|_ , _ => None |_ , _ => None
end end
| Fma e1 e2 e3 =>
match eval_exp_float e1 E, eval_exp_float e2 E, eval_exp_float e3 E with
| Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3))
| _, _, _ => None
end
| _ => None | _ => None
end. end.
...@@ -78,6 +83,24 @@ Fixpoint eval_exp_valid (e:exp fl64) E := ...@@ -78,6 +83,24 @@ Fixpoint eval_exp_valid (e:exp fl64) E :=
normal_or_zero (evalBinop b v1_real v2_real)) normal_or_zero (evalBinop b v1_real v2_real))
True) True)
True) True)
| Fma e1 e2 e3 =>
(eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\ (eval_exp_valid e3 E) /\
(let e1_res := eval_exp_float e1 E in
let e2_res := eval_exp_float e2 E in
let e3_res := eval_exp_float e3 E in
optionLift e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
optionLift e3_res
(fun v3 =>
let v3_real := B2R 53 1024 v3 in
normal_or_zero (evalFma v1_real v2_real v3_real))
True)
True)
True)
| Downcast m e => eval_exp_valid e E | Downcast m e => eval_exp_valid e E
end. end.
...@@ -153,6 +176,7 @@ Fixpoint B2Qexp (e: exp fl64) := ...@@ -153,6 +176,7 @@ Fixpoint B2Qexp (e: exp fl64) :=
| Const m v => Const m (B2Q v) | Const m v => Const m (B2Q v)
| Unop u e => Unop u (B2Qexp e) | Unop u e => Unop u (B2Qexp e)
| Binop b e1 e2 => Binop b (B2Qexp e1) (B2Qexp e2) | Binop b e1 e2 => Binop b (B2Qexp e1) (B2Qexp e2)
| Fma e1 e2 e3 => Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)
| Downcast m e => Downcast m (B2Qexp e) | Downcast m e => Downcast m (B2Qexp e)
end. end.
...@@ -174,6 +198,7 @@ Fixpoint is64BitEval (V:Type) (e:exp V) := ...@@ -174,6 +198,7 @@ Fixpoint is64BitEval (V:Type) (e:exp V) :=
| Const m e => m = M64 | Const m e => m = M64
| Unop u e => is64BitEval e | Unop u e => is64BitEval e
| Binop b e1 e2 => is64BitEval e1 /\ is64BitEval e2 | Binop b e1 e2 => is64BitEval e1 /\ is64BitEval e2
| Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
| Downcast m e => m = M64 /\ is64BitEval e | Downcast m e => m = M64 /\ is64BitEval e
end. end.
...@@ -189,6 +214,7 @@ Fixpoint noDowncast (V:Type) (e:exp V) := ...@@ -189,6 +214,7 @@ Fixpoint noDowncast (V:Type) (e:exp V) :=
| Const m e => True | Const m e => True
| Unop u e => noDowncast e | Unop u e => noDowncast e
| Binop b e1 e2 => noDowncast e1 /\ noDowncast e2 | Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
| Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
| Downcast m e => False | Downcast m e => False
end. end.
...@@ -294,6 +320,26 @@ Proof. ...@@ -294,6 +320,26 @@ Proof.
+ destruct (tMap e1); destruct (tMap e2); try congruence; + destruct (tMap e1); destruct (tMap e2); try congruence;
andb_to_prop typecheck_e; eauto. andb_to_prop typecheck_e; eauto.
+ intros; apply types_valid; set_tac. + intros; apply types_valid; set_tac.
- repeat (match goal with
|H: _ /\ _ |- _=> destruct H
end).
destruct (tMap (Fma e1 e2 e3)) eqn:?; try congruence;
erewrite IHe1 in *; eauto.
+ erewrite IHe2 in *; eauto.
* unfold join3, join in typecheck_e.
erewrite IHe3 in *; eauto.
++ rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
type_conv; subst; auto.
++ destruct (tMap e3); try congruence.
andb_to_prop typecheck_e; eauto.
++ intros; apply types_valid. set_tac.
* destruct (tMap e2); destruct (tMap e3); try congruence.
andb_to_prop typecheck_e; eauto.
* intros.
apply types_valid. set_tac.
+ destruct (tMap e1); destruct (tMap e2); destruct (tMap e3); try congruence;
andb_to_prop typecheck_e; eauto.
+ intros; apply types_valid; set_tac.
Qed. Qed.
Lemma typing_cmd_64_bit f: Lemma typing_cmd_64_bit f:
...@@ -352,6 +398,18 @@ Proof. ...@@ -352,6 +398,18 @@ Proof.
assert (m3 = m1). assert (m3 = m1).
{ eapply IHe2; eauto. } { eapply IHe2; eauto. }
subst; auto. subst; auto.
- destruct (tMap e1) eqn:?; try congruence;
destruct (tMap e2) eqn:?; try congruence;
destruct (tMap e3) eqn:?; try congruence.
andb_to_prop typeCheck_e.
type_conv; subst.
assert (m0 = m).
{ eapply IHe1; eauto. }
assert (m3 = m1).
{ eapply IHe2; eauto. }
assert (m4 = m5).
{ eapply IHe3; eauto. }
subst; auto.
- destruct (tMap e) eqn:?; try congruence; type_conv; subst. - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
andb_to_prop typeCheck_e. andb_to_prop typeCheck_e.
type_conv; subst; auto. type_conv; subst; auto.
...@@ -923,7 +981,213 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) : ...@@ -923,7 +981,213 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
repeat rewrite B2Q_B2R_eq; try auto. repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- div_round; auto. rewrite <- round_eq. rewrite <- div_round; auto.
- rewrite finite_e1 in finite_res; auto. } - rewrite finite_e1 in finite_res; auto. }
- inversion noDowncast_e. - repeat (match goal with
|H: _ /\ _ |- _ => destruct H
end).
destruct (tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?; try congruence;
destruct (tMap (B2Qexp e1)) eqn:?; try congruence;
destruct (tMap (B2Qexp e2)) eqn:?; try congruence;
destruct (tMap (B2Qexp e3)) eqn:?; try congruence.
andb_to_prop typecheck_e; type_conv; subst.
assert (tMap (B2Qexp e1) = Some M64 /\
tMap (B2Qexp e2) = Some M64 /\
tMap (B2Qexp e3) = Some M64 /\
tMap (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3)) = Some M64)
as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
{ repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
- intros; apply usedVars_64bit; set_tac.
- intros; apply usedVars_64bit; set_tac.
- intros; apply usedVars_64bit; set_tac.
- rewrite Heqo, Heqo0, Heqo1, Heqo2.
apply Is_true_eq_true; apply andb_prop_intro; split.
+ apply andb_prop_intro; split.
* apply andb_prop_intro; split.
++ apply Is_true_eq_left; auto.
apply mTypeEq_refl.
++ apply Is_true_eq_left; auto.
* apply Is_true_eq_left; auto.
+ apply Is_true_eq_left; auto. }
rewrite tMap_e1, tMap_e2, tMap_e3, tMap_fma in *.
inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
assert (m1 = M64).
{ eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
assert (m2 = M64).
{ eapply (typing_agrees_exp (B2Qexp e2)); eauto. }
assert (m3 = M64).
{ eapply (typing_agrees_exp (B2Qexp e3)); eauto. }
subst.
destruct (A (Fma (B2Qexp e1) (B2Qexp e2) (B2Qexp e3))) eqn:?;
destruct (A (B2Qexp e1)) eqn:?;
destruct (A (B2Qexp e2)) eqn:?;
destruct (A (B2Qexp e3)) eqn:?;
simpl in *.
repeat (match goal with
|H: _ = true |- _ => andb_to_prop H
end).
destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
as [v_e1 [eval_float_e1 eval_rel_e1]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
as [v_e2 [eval_float_e2 eval_rel_e2]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
rewrite eval_float_e1, eval_float_e2.
assert (exists nR2,
eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e2))) nR2 M0 /\
Q2R (fst (fst (A (B2Qexp e2)))) <= nR2 <= Q2R (snd (fst (A (B2Qexp e2)))))%R
as [nR2 [eval_e2_real e2_bounded_real]].
{ eapply validIntervalbounds_sound; eauto.
- intros; eapply dVars_sound; set_tac.
- set_tac. hnf in usedVars_sound. apply usedVars_sound.
set_tac.
- intros. eapply fVars_defined. rewrite NatSet.mem_spec in *; auto.
- intros. apply vars_typed. set_tac. rewrite NatSet.union_spec in *; auto. }
assert (forall vF2 m2,
eval_exp E2_real Gamma (toRExp (B2Qexp e2)) vF2 m2 ->
(Rabs (nR2 - vF2) <= Q2R (snd (A (B2Qexp e2)))))%R.
{ eapply validErrorbound_sound; try eauto; try set_tac.
- intros. eapply dVars_sound; set_tac.
- intros. eapply fVars_defined. rewrite NatSet.mem_spec in *; auto.
- intros. apply vars_typed; set_tac. rewrite NatSet.union_spec in *; auto.
- rewrite Heqp1.
simpl. instantiate (1:=snd(i1)).
instantiate (1:=fst(i1)). destruct i1; simpl; auto. }
assert (contained (Q2R (B2Q v_e2))
(widenInterval
(Q2R (fst (fst (A (B2Qexp e2)))), Q2R (snd (fst (A (B2Qexp e2)))))
(Q2R (snd(A (B2Qexp e2)))))).
{ eapply distance_gives_iv.
- simpl. eapply e2_bounded_real.
- eapply H11. instantiate(1:=M64).
eapply eval_eq_env; eauto. }
assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
{ intros; subst; simpl in *.
andb_to_prop R2.
apply le_neq_bool_to_lt_prop in L4.
rewrite Heqp1 in *; simpl in *.
destruct L4; hnf; intros.
- rewrite H15 in *.
apply Qlt_Rlt in H14.
rewrite Q2R0_is_0, Q2R_plus in H14. lra.
- rewrite H15 in *.
apply Qlt_Rlt in H14.
rewrite Q2R0_is_0, Q2R_minus in H14; lra. }
assert (validFloatValue
(evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
{ eapply (FPRangeValidator_sound (Binop b (B2Qexp e1) (B2Qexp e2)));
try eauto; set_tac.
- eapply eval_eq_env; eauto.
eapply (Binop_dist' (delta:=0)); eauto.
+ rewrite Rabs_R0. apply mTypeToQ_pos_R.
+ unfold perturb; lra.
- rewrite tMap_b, tMap_e1, tMap_e2.
apply Is_true_eq_true.
repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
- rewrite Heqp, Heqp0, Heqp1.
apply Is_true_eq_true.
repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
apply andb_prop_intro; split; auto using Is_true_eq_left.
- rewrite Heqp, Heqp0, Heqp1.
rewrite tMap_b.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
- rewrite tMap_b, Heqp.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
assert (validFloatValue (Q2R (B2Q v_e1)) M64).
{ eapply (FPRangeValidator_sound (B2Qexp e1)); try eauto; try set_tac.
eapply eval_eq_env; eauto. }
assert (validFloatValue (Q2R (B2Q v_e2)) M64).
{ eapply (FPRangeValidator_sound (B2Qexp e2)); try eauto; try set_tac.
- eapply eval_eq_env; eauto. }
assert (is_finite 53 1024 v_e1 = true) as finite_e1.
{ apply validValue_is_finite; simpl; auto. }
assert (is_finite 53 1024 v_e2 = true) as finite_e2.
{ apply validValue_is_finite; simpl; auto. }
assert (forall eps,
(Rabs eps <= / 2 * bpow radix2 (- 53 + 1))%R ->
validFloatValue
(evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2) * (1 + eps)) M64).
{ intros.
eapply FPRangeValidator_sound with (e:=Binop b (B2Qexp e1) (B2Qexp e2)); eauto.
- eapply eval_eq_env; eauto.
eapply Binop_dist' with (delta:=eps); eauto.
simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
eapply Rle_trans; eauto. unfold Qpower. unfold Qpower_positive.
assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
by (vm_compute; auto).
rewrite H19. rewrite Q2R_inv; try lra.
unfold Q2R, Qnum, Qden. unfold bpow.
assert (-53 + 1 = -52)%Z by auto.
rewrite H20.
assert (Z.pow_pos radix2 52 = 4503599627370496%Z) by (vm_compute; auto).
rewrite H21. unfold Z2R, P2R. lra.
unfold perturb.
repeat rewrite B2Q_B2R_eq; auto.
- simpl. rewrite tMap_b, tMap_e1, tMap_e2.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- simpl; rewrite Heqp, Heqp0, Heqp1.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- simpl. rewrite Heqp, Heqp0, Heqp1, tMap_b.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- simpl. rewrite Heqp, tMap_b.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
{ intros; subst; simpl in *.
andb_to_prop R2.
apply le_neq_bool_to_lt_prop in L4.
rewrite Heqp1 in *; simpl in *.
destruct L4 as [case_low | case_high]; hnf; intros.
- rewrite H19 in *.
apply Qlt_Rlt in case_low.
rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
- rewrite H19 in *.
apply Qlt_Rlt in case_high.
rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
usedVars_sound R2 R1 L1 L R6 L0 R3 L3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
IHe2.
pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
assert (forall k : Z, (-1022 < k)%Z ->
(53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
as exp_valid.
{ intros k k_pos.
unfold Fcore_FLT.FLT_exp; simpl.
destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
(-1022)%Z 53%Z exp_valid)
as rel_error_exists.
rewrite eval_float_e1, eval_float_e2 in H1.
unfold optionLift, normal_or_zero in *; simpl in *.
assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
(evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
{ revert H1; intros case_val. destruct case_val; try auto.
left; unfold Normal, Denormal in H15; unfold Normal;
destruct H15 as [normal_b | [denormal_b |zero_b]].
- repeat rewrite <- B2Q_B2R_eq; try auto.
- destruct denormal_b.
assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop</