Commit 623980fa authored by Joachim Bard's avatar Joachim Bard

adjusting IEEE connection

parent 1a34864b
......@@ -1170,10 +1170,10 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 A).
{ unfold dVars_range_valid.
intros; set_tac. }
(* assert (AffineValidation.affine_dVars_range_valid NatSet.empty E1 A 1 (FloverMap.empty _) (fun _ => None))
as affine_dvars_valid.
assert (AffineValidation.affine_dVars_range_valid NatSet.empty E1 A 1 (FloverMap.empty _)
(fun _ => None)) as affine_dvars_valid.
{ unfold AffineValidation.affine_dVars_range_valid.
intros; set_tac. } *)
intros; set_tac. }
assert (NatSet.Subset (usedVars (B2Qexpr e) -- NatSet.empty) (Expressions.usedVars (B2Qexpr e))).
{ hnf; intros a in_empty.
set_tac. }
......@@ -1187,8 +1187,7 @@ Proof.
exists (toRExpMap Gamma); intros approxE1E2.
pose proof RoundoffErrorValidator_sound as Hsound.
eapply validErrorBounds_single in Hsound; eauto.
2: unfold RoundoffErrorValidator; now rewrite L.
(* 2: intros v' Hin; set_tac. *)
2: intros v' Hin; set_tac.
specialize Hsound as ((v__FP & m__FP & Hbstepex) & Hsound).
assert (FloverMap.find (B2Qexpr e) Gamma = Some M64).
{ eapply typing_expr_64_bit; eauto. }
......@@ -1196,13 +1195,10 @@ Proof.
{ eapply validTypes_exec; try exact Hbstepex; eauto. }
subst.
edestruct eval_expr_gives_IEEE; eauto.
eapply RoundoffErrorValidator_sound; eauto.
1: unfold RoundoffErrorValidator; now rewrite L.
1: intros ? ?; set_tac.
(* 1: intros ? ?; set_tac. *)
exists (elo, ehi), err_e, vR, x.
intuition.
eapply Hsound; eauto.
- eapply RoundoffErrorValidator_sound; eauto. intros ? ?; set_tac.
- intros ? ?; set_tac.
- exists (elo, ehi), err_e, vR, x.
intuition. eapply Hsound; eauto.
Qed.
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
......@@ -1258,16 +1254,15 @@ Proof.
- eapply (ssa_equal_set (inVars:=preVars P)); eauto.
apply NatSetProps.empty_union_2. set_tac.
- unfold RealRangeArith.dVars_range_valid. intros; set_tac.
(* - unfold AffineValidation.affine_dVars_range_valid; intros.
set_tac. *)
- unfold AffineValidation.affine_dVars_range_valid; intros.
set_tac.
- eapply validSSA_checks_freeVars; eauto. }
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
pose proof RoundoffErrorValidatorCmd_sound as Hsound.
eapply validErrorBoundsCmd_single in Hsound; eauto.
2: unfold RoundoffErrorValidatorCmd; now rewrite L0.
(* 2: intros v' Hin; set_tac. *)
2: intros v' Hin; set_tac.
specialize Hsound as ((v__FP & m__FP & Hbstepex) & Hsound).
assert (M64 = m__FP).
{ pose proof H0 as validT.
......@@ -1278,10 +1273,8 @@ Proof.
congruence. }
subst.
edestruct bstep_gives_IEEE; eauto.
eapply RoundoffErrorValidatorCmd_sound; eauto.
1: unfold RoundoffErrorValidatorCmd; now rewrite L0.
1: intros ? ?; set_tac.
(* 1: intros ? ?; set_tac. *)
exists (f_lo, f_hi), err, vR, x, M64.
intuition.
- eapply RoundoffErrorValidatorCmd_sound; eauto. intros ? ?; set_tac.
- intros ? ?; set_tac.
- exists (f_lo, f_hi), err, vR, x, M64.
intuition.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment