Commit 2df64741 authored by Heiko Becker's avatar Heiko Becker

Prove some lemmas about IEEE map and fix global IEEE soundness structure

parent b4da184d
......@@ -8,19 +8,94 @@ From Flover
Environments Infra.RealRationalProps Commands Infra.Ltacs.
From Flocq
Require Import Appli.Fappli_IEEE_bits Appli.Fappli_IEEE Core.Fcore_Raux
Fprop_relative Fcore_generic_fmt.
Require Import Core.Generic_fmt Core.FLT Core.Zaux Calc.Round
IEEE754.Binary IEEE754.Bits.
From Flocq.Prop
Require Import Relative.
(* Appli.Fappli_IEEE_bits Appli.Fappli_IEEE Core.Fcore_Raux
Fprop_relative Fcore_generic_fmt. *)
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.
Definition flt_exp_64 := FLT_exp (3 - 1024 - 53) 53.
Lemma valid_flt_64:
Valid_exp flt_exp_64.
Proof.
apply FLT_exp_valid.
unfold FLX.Prec_gt_0. omega.
Qed.
Lemma valid_flt_64_assum:
forall k : Z,
(-1022 < k)%Z ->
(53 <= k - (flt_exp_64 k))%Z.
Proof.
intros k k_pos.
unfold flt_exp_64, Core.FLT.FLT_exp; simpl.
destruct (Z.max_spec_le (k - 53) (-1074)); omega.
Qed.
Definition relative_error_64_ex :=
@relative_error_N_ex radix2 flt_exp_64
valid_flt_64
(-1022) 53 valid_flt_64_assum
(fun x => negb (Z.even x)).
Definition IeeeDeltaMap (x:R) (m:mType): option R :=
match m with
| M64 => Some (((Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
(round_mode dmode) x) - x) / x)%R
| _ => None
| M64 => if (Raux.Rle_bool (Raux.bpow radix2 (-1022)) (Rabs x))
then Some (((round radix2 flt_exp_64 (round_mode dmode) x) - x) / x)%R
else Some 0%R (* failsafe case, no normal number provided *)
| _ => Some 0%R
end.
Ltac solve_0_tac :=
exists 0%R; split; try auto; rewrite Rabs_R0; apply mTypeToR_pos_R.
Lemma IeeeDeltaMap_valid:
forall (v : R) (m : mType),
exists d : R, IeeeDeltaMap v m = Some d /\ (Rabs d <= mTypeToR m)%R.
Proof.
intros. unfold IeeeDeltaMap.
destruct m; try (solve_0_tac; fail).
destruct (Raux.Rle_bool (Raux.bpow radix2 (-1022)) (Rabs v)) eqn:?.
(* Normal number case *)
- pose proof (relative_error_64_ex v) as rel_error_ex.
pose proof (Raux.Rle_bool_spec (Raux.bpow radix2 (-1022)) (Rabs v)) as Rle_reflect.
rewrite Heqb in *.
inversion Rle_reflect.
destruct rel_error_ex as (eps & rel_error_bounded & rel_error_def); [auto|].
unfold dmode.
assert (round_mode mode_NE = Znearest (fun x => negb (Z.even x)))
as round_mode_def by auto.
rewrite round_mode_def.
rewrite rel_error_def.
assert (v <> 0%R).
{ hnf; intros. subst. rewrite Rabs_R0 in *.
pose proof (Raux.bpow_gt_0 radix2 (-1022)). lra. }
rewrite Rmult_plus_distr_l, Rmult_1_r.
field_rewrite (v + v * eps - v = v * eps)%R.
field_rewrite (v * eps / v = eps)%R.
exists eps; split; try auto.
cut (mTypeToR M64 = / 2 * Raux.bpow radix2 (- (53) + 1))%R.
+ intros HeqType; rewrite HeqType; auto.
+ unfold mTypeToR.
change (- (53) + 1)%Z with (- (52))%Z.
rewrite Raux.bpow_opp.
rewrite <- Rinv_mult_distr; try lra.
2: {
pose proof (Raux.bpow_gt_0 radix2 52).
hnf; intros; lra. }
rewrite <- inv_eq_1_div. f_equal.
rewrite Raux.bpow_powerRZ.
field_rewrite (2 ^ 53 = 2 * 2 ^ 52)%R.
f_equal.
- solve_0_tac.
Qed.
Definition normal_or_zero v :=
(v = 0 \/ (Q2R (minValue_pos M64)) <= (Rabs v))%R.
......@@ -79,37 +154,41 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionBind e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
let op_real := evalBinop b v1_real v2_real in
plet delta := IeeeDeltaMap op_real M64 in
normal_or_zero (perturb op_real M64 delta) )
True)
True)
match e1_res with
| None => True
| Some v1 =>
let v1_real := B2R 53 1024 v1 in
match e2_res with
| None => True
| Some v2 =>
let v2_real := B2R 53 1024 v2 in
let op_real := evalBinop b v1_real v2_real in
(* plet delta := IeeeDeltaMap op_real M64 in *)
normal_or_zero op_real (* (perturb op_real M64 delta)*)
end
end)
| Fma e1 e2 e3 =>
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\ (eval_expr_valid e3 E) /\
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
let e3_res := eval_expr_float e3 E in
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionBind e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
optionBind e3_res
(fun v3 =>
let v3_real := B2R 53 1024 v3 in
(* No support for fma yet *)
(* normal_or_zero (evalFma v1_real v2_real v3_real)) *)
False)
True)
True)
True)
match e1_res with
| None => True
| Some v1 =>
let v1_real := B2R 53 1024 v1 in
match e2_res with
| None => True
| Some v2 =>
let v2_real := B2R 53 1024 v2 in
match e3_res with
| None => True
| Some v3 =>
let v3_real := B2R 53 1024 v3 in
False (* No support for fma yet; ideally this would be
normal_or_zero (evalFma v1_real v2_real v3_real) *)
end
end
end)
| Downcast m e => eval_expr_valid e E
end.
......@@ -133,15 +212,16 @@ Definition bpowQ (r:radix) (e: Z) :=
Definition B2Q :=
fun prec emax : Z =>
let emin := (3 - emax - prec)%Z in
let fexpr := Fcore_FLT.FLT_exp emin prec in
let fexpr := FLT_exp emin prec in
fun f : binary_float prec emax =>
match f with
| B754_zero _ _ _ => 0%Q
| B754_infinity _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_nan _ _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_nan _ _ _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_finite _ _ s m e _ =>
let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (Zpos m); Fcore_defs.Fexp := e |} in
(Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
let f_new: Core.Defs.float radix2 :=
{| Core.Defs.Fnum := cond_Zopp s (Zpos m); Core.Defs.Fexp := e |} in
(Core.Defs.Fnum f_new # 1) * bpowQ radix2 (Core.Defs.Fexp f_new)
end.
Lemma B2Q_B2R_eq :
......@@ -152,34 +232,31 @@ Proof.
intros; unfold B2Q, B2R, is_finite in *.
destruct v eqn:?; try congruence;
try rewrite Q2R0_is_0; try lra.
unfold Fcore_defs.F2R.
unfold Core.Defs.F2R.
rewrite Q2R_mult.
f_equal.
- unfold Z2R, Q2R.
simpl. rewrite RMicromega.Rinv_1.
destruct (cond_Zopp b (Zpos m)); unfold IZR;
try rewrite P2R_INR, INR_IPR; lra.
- unfold Q2R.
simpl. rewrite Rinv_1, Rmult_1_r.
auto.
- unfold Q2R; simpl.
unfold bpow, bpowQ.
unfold bpowQ.
destruct e; simpl; try lra.
+ rewrite RMicromega.Rinv_1.
unfold Z2R, IZR.
destruct (Z.pow_pos 2 p); try rewrite P2R_INR, INR_IPR; auto.
+ unfold Z2R, IZR. unfold Qinv; simpl.
destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR, INR_IPR; simpl; try lra.
* unfold bounded in e0. simpl in e0. unfold canonic_mantissa in e0.
simpl in e0.
pose proof (Is_true_eq_left _ e0).
apply Is_true_eq_true in H0; andb_to_prop H0.
assert (0 < Z.pow_pos 2 p)%Z.
{ apply Zpower_pos_gt_0. cbv; auto. }
rewrite Heqz in H0. inversion H0.
* unfold IPR at 1. rewrite Rmult_1_l; auto.
* rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute;
unfold IZR. unfold Qinv; simpl.
destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR, INR_IPR;
simpl; try lra.
+ unfold bounded in e0. simpl in e0. unfold canonical_mantissa in e0.
simpl in e0.
pose proof (Is_true_eq_left _ e0).
apply Is_true_eq_true in H0; andb_to_prop H0.
assert (0 < Z.pow_pos 2 p)%Z.
{ apply Zpower_pos_gt_0. cbv; auto. }
rewrite Heqz in H0. inversion H0.
+ unfold IPR at 1. rewrite Rmult_1_l; auto.
+ rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute;
[ unfold IPR at 1; lra | ].
hnf; intros. pose proof (pos_INR_nat_of_P p0).
rewrite INR_IPR in *.
rewrite H0 in H1; lra.
hnf; intros. pose proof (pos_INR_nat_of_P p0).
rewrite INR_IPR in *.
rewrite H0 in H1; lra.
Qed.
Fixpoint B2Qexpr (e: expr fl64) :=
......@@ -319,132 +396,369 @@ Proof.
Qed.
Lemma round_0_zero:
(Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE) 0) = 0%R.
(round radix2 flt_exp_64 (round_mode mode_NE) 0) = 0%R.
Proof.
unfold Fcore_generic_fmt.round. simpl.
unfold Fcore_generic_fmt.scaled_mantissa.
unfold round. simpl.
unfold scaled_mantissa.
rewrite Rmult_0_l.
unfold Fcore_generic_fmt.Znearest.
unfold Zfloor.
unfold Znearest.
unfold Raux.Zfloor.
assert (up 0 = 1%Z).
{ symmetry. apply tech_up; lra. }
rewrite H.
simpl. rewrite Rsub_eq_Ropp_Rplus. rewrite Rplus_opp_r.
assert (Rcompare (0) (/ 2) = Lt).
{ apply Rcompare_Lt. lra. }
assert (Raux.Rcompare (0) (/ 2) = Lt).
{ apply Raux.Rcompare_Lt. lra. }
rewrite H0.
unfold Fcore_generic_fmt.canonic_exp.
unfold Fcore_defs.F2R; simpl.
unfold cexp.
unfold Defs.F2R; simpl.
rewrite Rmult_0_l. auto.
Qed.
Lemma validValue_bounded' v delta:
(Normal v M64\/ (v = 0)%R) ->
(Rabs delta <= / 2 * bpow radix2 (- 53 + 1))%R ->
delta = (((Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE) v)
- v) / v)%R ->
validFloatValue (v * (1 + delta)) M64 ->
Rlt_bool (Rabs (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) v)) (bpow radix2 1024) = true.
Ltac find_cases :=
rewrite map_find_add;
match goal with
| [H: _ |- context[ Q_orderedExps.compare ?e1 ?e2]] =>
destruct (Q_orderedExps.compare e1 e2) eqn:?
end;
try auto.
Lemma getValidMap_preserving e:
forall defVars akk res,
(forall e m, FloverMap.find e akk = Some m -> m = M64) ->
is64BitEval e ->
getValidMap defVars e akk = Succes res ->
(forall e m, FloverMap.find e defVars = Some m -> m = M64) ->
forall e m, FloverMap.find e res = Some m -> m = M64.
Proof.
simpl.
pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
assert (forall k : Z, (-1022 < k)%Z ->
(53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
as expr_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 expr_valid)
as rel_error_exists.
intros [normal_v | zero_v] delta_small delta_eq validVal;
apply Rlt_bool_true.
- unfold Normal in *; destruct normal_v.
specialize (rel_error_exists (fun x => negb (Zeven x)) v).
specialize (rel_error_exists) as [eps [bounded_eps round_eq]].
+ eapply Rle_trans; eauto.
unfold minValue_pos.
rewrite Q2R_inv.
* apply Rinv_le.
{ rewrite <- Q2R0_is_0. apply Qlt_Rlt.
apply Qlt_alt. vm_compute; auto. }
{ unfold Q2R.
unfold Qnum, Qden. unfold minExponentPos.
rewrite Z2R_IZR.
rewrite Rinv_1. rewrite Rmult_1_r.
apply IZR_le; vm_compute; congruence. }
* vm_compute; congruence.
+ cbn in round_eq.
rewrite round_eq in delta_eq.
assert (v <> 0%R).
{
clear - H.
intros v_zero.
subst.
rewrite Rabs_R0 in H.
cbn in H.
lra.
}
field_simplify in delta_eq; [ | lra].
field_simplify in delta_eq; [ | lra].
replace (delta / 1)%R with delta in delta_eq by lra.
replace (eps / 1)%R with eps in delta_eq by lra.
subst.
simpl in *.
rewrite round_eq.
destruct validVal as [normal_v | [denormal_v | zero_v]]; try auto.
* unfold Normal in *. destruct normal_v.
eapply Rle_lt_trans; eauto.
unfold maxValue, bpow. unfold maxExponent. unfold Q2R.
unfold Qnum, Qden. rewrite <- Z2R_IZR. unfold IZR.
repeat rewrite <- INR_IPR. simpl. lra.
* unfold Denormal in *. destruct denormal_v.
eapply Rlt_trans; eauto.
unfold minValue_pos, minExponentPos, bpow.
rewrite Q2R_inv.
{ unfold Q2R, Qnum, Qden.
rewrite <- Z2R_IZR; unfold IZR.
repeat rewrite <- INR_IPR; simpl; lra. }
{ vm_compute; congruence. }
* rewrite zero_v. simpl. rewrite Rabs_R0. lra.
- rewrite zero_v.
pose proof round_0_zero. simpl in H. rewrite H.
rewrite Rabs_R0.
lra.
pose (eT := e);
induction e; intros * valid_akk is64Bit_e getMap_succeeds find_defVars *;
destruct (FloverMap.mem eT akk) eqn:case_mem;
cbn in *; subst eT; rewrite case_mem in *;
try (inversion getMap_succeeds; subst; now apply valid_akk).
- Flover_compute.
inversion getMap_succeeds; subst.
assert (m0 = M64) by (eapply find_defVars; eauto).
subst; find_cases; try (now apply valid_akk).
congruence.
- unfold isMonotone in *.
Flover_compute.
+ destruct (mTypeEq m1 m) eqn:?; try congruence; type_conv; subst.
inversion getMap_succeeds; subst.
find_cases; try (now apply valid_akk).
congruence.
+ inversion getMap_succeeds; subst.
find_cases; try (now apply valid_akk).
congruence.
- destruct (getValidMap defVars e akk) eqn:?; simpl in *; try congruence.
destruct (FloverMap.find e t) eqn:?; try congruence.
assert (m0 = M64).
{ eapply IHe with (akk:=akk); eauto. }
subst. cbn in getMap_succeeds.
unfold addMono, isMonotone in *.
destruct (FloverMap.find (Unop u e) defVars) eqn:?.
+ destruct (mTypeEq m0 M64) eqn:?; try congruence; type_conv; subst.
Flover_compute; inversion getMap_succeeds; subst.
find_cases; try (eapply IHe with (akk:=akk); eauto).
congruence.
+ Flover_compute; inversion getMap_succeeds; subst.
find_cases; try (eapply IHe with (akk:=akk); eauto).
congruence.
- destruct (getValidMap defVars e1 akk) eqn:?;
simpl in *; try congruence.
destruct (getValidMap defVars e2 t) eqn:?;
simpl in *; try congruence.
destruct (FloverMap.find e1 t0) eqn:?;
try congruence.
destruct (FloverMap.find e2 t0) eqn:?;
try congruence.
destruct is64Bit_e.
assert (forall e m, FloverMap.find e t = Some m -> m = M64)
as valid_t
by (eapply IHe1 with (akk:=akk); eauto).
assert (forall e m, FloverMap.find e t0 = Some m -> m = M64)
as valid_t0
by (eapply IHe2 with (akk:=t); eauto).
clear IHe1 IHe2.
assert (m0 = M64) by (eapply valid_t0; eauto).
assert (m1 = M64) by (eapply valid_t0; eauto).
subst; cbn in *.
unfold isMonotone, addMono in *.
destruct (FloverMap.find (Binop b e1 e2) defVars) eqn:?.
+ destruct (mTypeEq m0 M64) eqn:?; try congruence; type_conv; subst.
Flover_compute.
inversion getMap_succeeds; subst.
find_cases; try (eapply valid_t0; now eauto).
congruence.
+ Flover_compute.
inversion getMap_succeeds; subst.
find_cases; try (eapply valid_t0; now eauto).
congruence.
- destruct (getValidMap defVars e1 akk) eqn:?;
simpl in *; try congruence.
destruct (getValidMap defVars e2 t) eqn:?;
simpl in *; try congruence.
destruct (getValidMap defVars e3 t0) eqn:?;
simpl in *; try congruence.
destruct (FloverMap.find e1 t1) eqn:?;
try congruence.
destruct (FloverMap.find e2 t1) eqn:?;
try congruence.
destruct (FloverMap.find e3 t1) eqn:?;
try congruence.
destruct is64Bit_e as (? & ? & ?).
assert (forall e m, FloverMap.find e t = Some m -> m = M64)
as valid_t
by (eapply IHe1 with (akk:=akk); eauto).
assert (forall e m, FloverMap.find e t0 = Some m -> m = M64)
as valid_t0
by (eapply IHe2 with (akk:=t); eauto).
assert (forall e m, FloverMap.find e t1 = Some m -> m = M64)
as valid_t1
by (eapply IHe3 with (akk:=t0); eauto).
clear IHe1 IHe2 IHe3.
assert (m0 = M64 /\ m1 = M64 /\ m2 = M64)
as (? & ? & ?)
by (repeat split; eapply valid_t1; eauto).
subst; cbn in *.
unfold isMonotone, addMono in *.
destruct (FloverMap.find (Fma e1 e2 e3) defVars) eqn:?.
+ destruct (mTypeEq m0 M64) eqn:?; try congruence; type_conv; subst.
Flover_compute.
inversion getMap_succeeds; subst.
find_cases; try (eapply valid_t1; now eauto).
congruence.
+ Flover_compute.
inversion getMap_succeeds; subst.
find_cases; try (eapply valid_t1; now eauto).
congruence.
- destruct (getValidMap defVars e akk) eqn:?; simpl in *; try congruence.
destruct (FloverMap.find e t) eqn:?; try congruence.
destruct is64Bit_e; subst.
assert (m1 = M64).
{ eapply IHe with (akk:=akk); eauto. }
subst. cbn in getMap_succeeds.
unfold addMono, isMonotone in *.
destruct (FloverMap.find (Downcast M64 e) defVars) eqn:?.
+ destruct (mTypeEq m M64) eqn:?; try congruence; type_conv; subst.
Flover_compute; inversion getMap_succeeds; subst.
find_cases; try (eapply IHe with (akk:=akk); eauto).
congruence.
+ Flover_compute; inversion getMap_succeeds; subst.
find_cases; try (eapply IHe with (akk:=akk); eauto).
congruence.
Qed.
Lemma validValue_bounded v:
(Normal v M64\/ (v = 0)%R) ->
(forall eps, (Rabs eps <= / 2 * bpow radix2 (- 53 + 1))%R ->
validFloatValue (v * (1 + eps)) M64) ->
Rlt_bool (Rabs (Fcore_generic_fmt.round
radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
v))
(bpow radix2 1024) = true.
Lemma getValidMapCmd_preserving f:
forall defVars akk res,
(forall e m, FloverMap.find e akk = Some m -> m = M64) ->
is64BitBstep f ->
getValidMapCmd defVars f akk = Succes res ->
(forall e m, FloverMap.find e defVars = Some m -> m = M64) ->
forall e m, FloverMap.find e res = Some m -> m = M64.
Proof.
simpl.
pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
assert (forall k : Z, (-1022 < k)%Z ->
(53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
as expr_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 expr_valid)
as rel_error_exists.
intros [normal_v | zero_v] validVal;
apply Rlt_bool_true.
- unfold Normal in *; destruct normal_v.
specialize (rel_error_exists (fun x => negb (Zeven x)) v).
destruct (rel_error_exists) as [eps [bounded_eps round_eq]].
+ eapply Rle_trans; eauto.
unfold minValue_pos.
induction f; intros * valid_akk is64Bit_f validMap_succ find_def *;
cbn in *; unfold addMono in *; Flover_compute.
- destruct (mTypeEq m m1) eqn:?; try congruence.
type_conv; subst.
destruct is64Bit_f as (? & ? & ?); subst.
eapply IHf with (akk:=t0); eauto.
inversion Heqr0; subst.
intros *.
find_cases; try (eapply getValidMap_preserving with (akk:=akk); now eauto).
congruence.
- destruct is64Bit_f as (? & ? & ?); subst.
destruct (mTypeEq M64 m1) eqn:?; congruence.
- eapply getValidMap_preserving with (akk:=akk); eauto.
Qed.
Theorem IEEE_connection_expr e A P qMap E1 E2 defVars:
is64BitEval (B2Qexpr e) ->
is64BitEnv defVars ->
noDowncast (B2Qexpr e) ->
eval_expr_valid e E2 ->
unsat_queries qMap ->
eval_precond E1 P ->
CertificateChecker (B2Qexpr e) A P qMap defVars = true ->
exists Gamma, (* m, currently = M64 *)
approxEnv E1 Gamma A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
exists iv err vR vF,
FloverMap.find (B2Qexpr e) A = Some (iv, err) /\
eval_expr E1 (toRTMap Gamma) DeltaMapR (toREval (toRExp (B2Qexpr e))) vR REAL /\
eval_expr_float e E2 = Some vF /\
eval_expr (toREnv E2) Gamma IeeeDeltaMap (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
(Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
Proof.
intros * is64eval is64bitenv no_cast eval_valid unsat_qs
P_valid certificate_valid.
destruct (@Certificate_checking_is_sound_general (B2Qexpr e) A P qMap defVars
E1 (toREnv E2) IeeeDeltaMap)
as [Gamma validCert_general];
try eauto using IeeeDeltaMap_valid.
exists (toRExpMap Gamma). intros approxEnv_E1E2.
destruct validCert_general as (? & ? & ? & ? & ? & ? & ? & ? & ? & ?);
[ auto | ].
(*
repeat eexists; try eauto.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars (B2Qexpr e) (FloverMap.empty mType)) eqn:?; try congruence.
assert (is64BitEnv t).
{ unfold is64BitEnv.
eapply getValidMap_preserving with (akk:=FloverMap.empty mType); try eauto.
intros; cbn in *; congruence. }
rename t into Gamma.
assert (validTypes (B2Qexpr e) Gamma).
{ eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. }
rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
hnf in union_empty.
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.
{ unfold AffineValidation.affine_dVars_range_valid.
intros; set_tac. }
assert (NatSet.Subset (usedVars (B2Qexpr e) -- NatSet.empty) (Expressions.usedVars (B2Qexpr e))).
{ hnf; intros a in_empty.
set_tac. }
rename R0 into validFPRanges.
assert (validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma))) as valid_e.
{ eapply (RealRangeValidator.RangeValidator_sound (B2Qexpr e) (dVars:=NatSet.empty) (A:=A) (P:=P) (Qmap:=qMap));
auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
exists (toRExpMap Gamma); intros approxE1E2.
pose proof RoundoffErrorValidator_sound as Hsound.
eapply validErrorBounds_single in Hsound; eauto.
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. }
assert (M64 = m__FP).
{ eapply validTypes_exec; try exact Hbstepex; eauto. }
subst.
edestruct eval_expr_gives_IEEE; eauto.
- eapply RoundoffErrorValidator_sound; eauto. intros ? ?; set_tac.
- intros ? ?; set_tac.
- exists (elo, ehi), err_e, vR, x.
intuition. eapply Hsound; eauto.
Qed.
*)
Admitted.
(*
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
defVars E1 E2 DeltaMap:
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
is64BitBstep (B2Qcmd f) ->
is64BitEnv defVars ->
noDowncastFun (B2Qcmd f) ->
bstep_valid f E2 ->
unsat_queries qMap ->
eval_precond E1 P ->
CertificateCheckerCmd (B2Qcmd f) A P qMap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
exists iv err vR vF m,
FloverMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
bstep_float f E2 = Some vF /\
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap (Q2R (B2Q vF)) m /\
(forall vF m,
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap vF m ->
(Rabs (vR - vF) <= Q2R err)%R).
Proof.
intros * deltas_matched is64bitBstep is64BitEnv_def noDowncast bstep_valid unsat_qs
P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars (B2Qcmd f) (FloverMap.empty mType)) eqn:?;
try congruence.
rename t into Gamma.
assert (is64BitEnv Gamma).
{ unfold is64BitEnv.
eapply getValidMapCmd_preserving with (akk:=FloverMap.empty mType); eauto.
intros; cbn in *; congruence. }
assert (validTypesCmd (B2Qcmd f) Gamma).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2.
repeat rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
assert (validSSA (B2Qcmd f) (freeVars (B2Qcmd f) NatSet.empty) = true) as ssa_valid_small.
{ eapply validSSA_downward_closed; eauto; set_tac.
eapply validSSA_checks_freeVars; eauto. intuition. set_tac. }
apply validSSA_sound in ssa_valid_small as [outVars_small ssa_small].
rename L into ssa_valid.
pose proof (validSSA_sound _ _ ssa_valid) as [outVars ssa_f].
rename R into validFPRanges.
assert (NatSet.Subset (freeVars (B2Qcmd f) -- NatSet.empty) (freeVars (B2Qcmd f)))
as freeVars_contained by set_tac.
assert (validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply (RealRangeValidator.RangeValidatorCmd_sound _ (fVars:=preVars P));
eauto; set_tac.
- 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.
- 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: intros v' Hin; set_tac.
specialize Hsound as ((v__FP & m__FP & Hbstepex) & Hsound).
assert (M64 = m__FP).
{ pose proof H0 as validT.
eapply validTypesCmd_single in H0.
destruct H0 as (? & ? & valid_exec).
erewrite typing_cmd_64_bit in H0; eauto.
assert (m__FP = x) by ( eapply valid_exec; eauto).
congruence. }
subst.
edestruct bstep_gives_IEEE; eauto.
- eapply RoundoffErrorValidatorCmd_sound; eauto. intros ? ?; set_tac.
- intros ? ?; set_tac.
- exists (f_lo, f_hi), err, vR, x, M64.
intuition.
Qed.