Commit cae6b2f6 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Complete FMA IEEE connection proofs

parent c2327db4
......@@ -15,6 +15,10 @@ Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e}
| Binop b e1 e2 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap dVars
| Fma e1 e2 e3 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap dVars &&
FPRangeValidator e3 A typeMap dVars
| Unop u e =>
FPRangeValidator e A typeMap dVars
| Downcast m e => FPRangeValidator e A typeMap dVars
......
......@@ -97,7 +97,9 @@ Fixpoint eval_exp_valid (e:exp fl64) E :=
optionLift e3_res
(fun v3 =>
let v3_real := B2R 53 1024 v3 in
normal_or_zero (evalFma v1_real v2_real v3_real))
(* No support for fma yet *)
(* normal_or_zero (evalFma v1_real v2_real v3_real)) *)
False)
True)
True)
True)
......@@ -548,6 +550,7 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
exists v,
eval_exp_float e E2 = Some v /\
eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v)) M64.
Proof.
induction e; simpl in *;
intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
valid_roundoffs valid_float_ranges eval_e_float
......@@ -1032,162 +1035,14 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
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 b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
{ eapply Rlt_le_trans; eauto.
repeat rewrite B2Q_B2R_eq; auto. }
lra.
- rewrite B2Q_B2R_eq in zero_b; auto.
rewrite B2Q_B2R_eq in zero_b; auto.
rewrite zero_b in *.
rewrite Rabs_R0 in H1.
unfold minValue, minExponentPos in H1.
rewrite Q2R_inv in H1; [|vm_compute; congruence].
unfold Q2R, Qnum, Qden in H1.
assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
by (vm_compute; auto).
rewrite H2 in H1. rewrite <- Z2R_IZR in H1. unfold IZR in H1.
simpl in H1. lra. }
pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
-
destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A P fVars dVars)
as [v_e3 [eval_float_e3 eval_rel_e3]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
unfold optionLift in H4.
rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
contradiction H4.
- inversion noDowncast_e.
Qed.
Lemma bstep_gives_IEEE (f:cmd fl64) :
......@@ -1570,7 +1425,6 @@ Proof.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- destruct H6 as [vF [m [bstep_real [bstep_float roundoff_sound]]]].
assert (typeMapCmd defVars (B2Qcmd f) (getRetExp (B2Qcmd f)) = Some M64).
{ eapply typing_cmd_64_bit; eauto. }
assert (m = M64).
......
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