Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qabs Coq.micromega.Psatz Coq.QArith.Qreals. Require Import Flover.Expressions Flover.Infra.RationalSimps Flover.Typing Flover.IntervalValidation Flover.ErrorValidation Flover.CertificateChecker Flover.FPRangeValidator Flover.Environments Flover.Infra.RealRationalProps Flover.Commands Flover.Infra.Ltacs. Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative. Definition dmode := mode_NE. Definition fl64:Type := binary_float 53 1024. Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) := match e with | Some v => some_cont v | None => none_cont end. Definition normal_or_zero v := (v = 0 \/ (Q2R (minValue M64)) <= (Rabs v))%R. Definition updFlEnv x v E := fun y => if y =? x then Some (A:=(binary_float 53 1024)) v else E y. Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):= match e with | Var _ x => E x | Const m v => Some v | Unop Neg e => match eval_expr_float e E with |Some v1 => Some (b64_opp v1) |_ => None end | Unop Inv e => None | Binop b e1 e2 => match eval_expr_float e1 E, eval_expr_float e2 E with | Some f1, Some f2 => match b with | Plus => Some (b64_plus dmode f1 f2) | Sub => Some (b64_minus dmode f1 f2) | Mult => Some (b64_mult dmode f1 f2) | Div => Some (b64_div dmode f1 f2) end |_ , _ => None end | Fma e1 e2 e3 => match eval_expr_float e1 E, eval_expr_float e2 E, eval_expr_float e3 E with (* | Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3)) *) | _, _, _ => None end | _ => None end. Fixpoint bstep_float f E :option fl64 := match f with | Let m x e g => optionLift (eval_expr_float e E) (fun v => bstep_float g (updFlEnv x v E)) None | Ret e => eval_expr_float e E end. Definition isValid e := let trans_e := optionLift e (fun v => Some (B2R 53 1024 v)) None in optionLift trans_e normal_or_zero False. Fixpoint eval_expr_valid (e:expr fl64) E := match e with | Var _ x => True (*isValid (eval_expr_float (Var n) E)*) | Const m v => True (*isValid (eval_expr_float (Const m v) E)*) | Unop u e => eval_expr_valid e E | Binop b e1 e2 => (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 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 normal_or_zero (evalBinop b v1_real v2_real)) True) True) | 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 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 (* No support for fma yet *) (* normal_or_zero (evalFma v1_real v2_real v3_real)) *) False) True) True) True) | Downcast m e => eval_expr_valid e E end. Fixpoint bstep_valid f E := match f with | Let m x e g => eval_expr_valid e E /\ (optionLift (eval_expr_float e E) (fun v_e => bstep_valid g (updFlEnv x v_e E)) True) | Ret e => eval_expr_valid e E end. Definition bpowQ (r:radix) (e: Z) := match e with |0%Z => 1%Q | (' p)%Z => (Z.pow_pos r p) #1 | Z.neg p => Qinv ((Z.pow_pos r p)#1) end. Definition B2Q := fun prec emax : Z => let emin := (3 - emax - prec)%Z in let fexpr := Fcore_FLT.FLT_expr 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_finite _ _ s m e _ => let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (' m); Fcore_defs.Fexpr := e |} in (Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexpr f_new) end. Lemma B2Q_B2R_eq : forall v, is_finite 53 1024 v = true -> Q2R (B2Q v) = B2R 53 1024 v. Proof. intros; unfold B2Q, B2R, is_finite in *. destruct v eqn:?; try congruence; try rewrite Q2R0_is_0; try lra. unfold Fcore_defs.F2R. rewrite Q2R_mult. f_equal. - unfold Z2R, Q2R. simpl. rewrite RMicromega.Rinv_1. destruct (cond_Zopp b (' m)); unfold IZR; try rewrite P2R_INR, INR_IPR; lra. - unfold Q2R; simpl. unfold bpow, 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 IPR at 1; 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) := match e with | Var _ x => Var Q x | Const m v => Const m (B2Q v) | Unop u e => Unop u (B2Qexpr e) | Binop b e1 e2 => Binop b (B2Qexpr e1) (B2Qexpr e2) | Fma e1 e2 e3 => Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3) | Downcast m e => Downcast m (B2Qexpr e) end. Fixpoint B2Qcmd (f:cmd fl64) := match f with | Let m x e g => Let m x (B2Qexpr e) (B2Qcmd g) | Ret e => Ret (B2Qexpr e) end. Definition toREnv (E: nat -> option fl64) (x:nat):option R := match E x with |Some v => Some (Q2R (B2Q v)) |_ => None end. Fixpoint is64BitEval (V:Type) (e:expr V) := match e with | Var _ x => True | Const m e => m = M64 | Unop u e => is64BitEval e | 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 end. Fixpoint is64BitBstep (V:Type) (f:cmd V) := match f with | Let m x e g => is64BitEval e /\ m = M64 /\ is64BitBstep g | Ret e => is64BitEval e end. Fixpoint noDowncast (V:Type) (e:expr V) := match e with | Var _ x => True | Const m e => True | Unop u e => noDowncast e | Binop b e1 e2 => noDowncast e1 /\ noDowncast e2 | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3 | Downcast m e => False end. Fixpoint noDowncastFun (V:Type) (f:cmd V) := match f with | Let m x e g => noDowncast e /\ noDowncastFun g | Ret e => noDowncast e end. Opaque mTypeToQ. Lemma validValue_is_finite v: validFloatValue (Q2R (B2Q v)) M64 -> is_finite 53 1024 v = true. Proof. intros validVal. unfold is_finite. unfold validFloatValue, B2Q in *. destruct v; try auto; destruct validVal; unfold Normal in *; unfold Denormal in *; unfold maxValue, minValue, maxExponent, minExponentPos in*; rewrite Q2R_inv in *; unfold bpowQ in *. - assert (Z.pow_pos radix2 1024 = 179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216%Z) by (vm_compute;auto). rewrite H0 in H; destruct H; try lra. assert (Z.pow_pos 2 1023 = 89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608%Z) by (vm_compute; auto). rewrite H2 in *. clear H0 H2. rewrite Rabs_right in H1. apply Rle_Qle in H1. + rewrite <- Qle_bool_iff in H1. cbv in H1; try congruence. + rewrite <- Q2R0_is_0. apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto. - vm_compute; intros; congruence. - destruct H. + destruct H. rewrite Rabs_right in H. * rewrite <- Q2R_inv in H. apply Rlt_Qlt in H. vm_compute in H. congruence. vm_compute; congruence. * rewrite <- Q2R0_is_0. apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto. + rewrite <- Q2R0_is_0 in H. apply eqR_Qeq in H. vm_compute in H; congruence. - vm_compute; congruence. - destruct H. rewrite Rabs_right in H0. + apply Rle_Qle in H0. rewrite <- Qle_bool_iff in H0. vm_compute in H0; auto. + rewrite <- Q2R0_is_0. apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto. - vm_compute; congruence. - destruct H. + rewrite Rabs_right in H. * destruct H. rewrite <- Q2R_inv in H. { apply Rlt_Qlt in H. rewrite Qlt_alt in H. vm_compute in H. congruence. } { vm_compute; congruence. } * rewrite <- Q2R0_is_0. apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto. + rewrite <- Q2R0_is_0 in H. apply eqR_Qeq in H. vm_compute in H; congruence. - vm_compute; congruence. Qed. Lemma typing_expr_64_bit e: forall Gamma tMap, noDowncast e -> is64BitEval e -> typeCheck e Gamma tMap = true -> (forall v, NatSet.In v (usedVars e) -> Gamma v = Some M64) -> FloverMap.find e tMap = Some M64. Proof. induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid; cbn in *; try inversion noDowncast_e; subst; Flover_compute; try congruence; type_conv; subst. - rewrite types_valid in *; try set_tac. - destruct m; try congruence. - erewrite IHe in *; eauto. - repeat (match goal with |H: _ /\ _ |- _=> destruct H end). erewrite IHe1 in *; eauto. + erewrite IHe2 in *; eauto. * unfold join in *. destr_factorize. rewrite <- isMorePrecise_morePrecise. rewrite isMorePrecise_refl. inversion Heqo0; auto. * intros. apply types_valid. set_tac. + intros; apply types_valid; set_tac. - repeat (match goal with |H: _ /\ _ |- _=> destruct H end). erewrite IHe1 in *; eauto; try (intros; apply types_valid; set_tac; fail). erewrite IHe2 in *; eauto; try (intros; apply types_valid; set_tac; fail). unfold join3, join in *. erewrite IHe3 in *; eauto; try (intros; apply types_valid; set_tac; fail). repeat destr_factorize. repeat rewrite <- isMorePrecise_morePrecise. repeat rewrite isMorePrecise_refl; type_conv; subst; auto. Qed. Lemma typing_cmd_64_bit f: forall Gamma tMap, noDowncastFun f -> is64BitBstep f -> typeCheckCmd f Gamma tMap = true -> (forall v, NatSet.In v (freeVars f) -> Gamma v = Some M64) -> FloverMap.find (getRetExp f) tMap = Some M64. Proof. induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid; cbn in *; subst; try eauto using typing_expr_64_bit; Flover_compute; try congruence. destruct noDowncast_f; destruct is64BitEval_f as [Ha [Hb Hc]]. eapply IHf; eauto. intros. unfold updDefVars. destruct (v =? n) eqn:?. - type_conv; auto. - apply types_valid. rewrite NatSet.remove_spec, NatSet.union_spec. split; try auto. hnf; intros; subst. rewrite Nat.eqb_neq in Heqb. congruence. Qed. Lemma typing_agrees_expr e: forall E Gamma tMap v m1 m2, typeCheck e Gamma tMap = true -> eval_expr E Gamma (toRExp e) v m1 -> FloverMap.find e tMap = Some m2 -> m1 = m2. Proof. induction e; intros * typeCheck_e eval_e tMap_e; cbn in *; rewrite tMap_e in *; inversion eval_e; subst; cbn in *; Flover_compute; try congruence; type_conv; subst; try auto. - eapply IHe; eauto. - eapply IHe; eauto. - assert (m0 = m) by eauto using IHe1. assert (m3 = m1) by eauto using IHe2. subst; auto. - assert (m0 = m) by eauto using IHe1. assert (m3 = m1) by eauto using IHe2. assert (m4 = m5) by eauto using IHe3. subst; auto. Qed. Lemma typing_agrees_cmd f: forall E Gamma tMap v m1 m2, typeCheckCmd f Gamma tMap = true -> bstep (toRCmd f) E Gamma v m1 -> FloverMap.find (getRetExp f) tMap = Some m2 -> m1 = m2. Proof. induction f; intros * typeCheck_f eval_f tMap_f; cbn in *; Flover_compute; try congruence; type_conv; subst. - inversion eval_f; subst; simpl in *. specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2). apply IHf; auto. - inversion eval_f; subst; eapply typing_agrees_expr; eauto. Qed. Lemma round_0_zero: (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_expr (3 - 1024 - 53) 53) (round_mode mode_NE) 0) = 0%R. Proof. unfold Fcore_generic_fmt.round. simpl. unfold Fcore_generic_fmt.scaled_mantissa. rewrite Rmult_0_l. unfold Fcore_generic_fmt.Znearest. unfold 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. } rewrite H0. unfold Fcore_generic_fmt.canonic_expr. unfold Fcore_defs.F2R; simpl. rewrite Rmult_0_l. auto. Qed. Lemma validValue_bounded b v_e1 v_e2: (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) -> (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) -> Rlt_bool (Rabs (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_expr (3 - 1024 - 53) 53) (round_mode mode_NE) (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)))) (bpow radix2 1024) = true. Proof. simpl. pose proof (fexpr_correct 53 1024 eq_refl) as fexpr_corr. assert (forall k : Z, (-1022 < k)%Z -> (53 <= k - Fcore_FLT.FLT_expr (3 - 1024 - 53) 53 k)%Z) as expr_valid. { intros k k_pos. unfold Fcore_FLT.FLT_expr; simpl. destruct (Z.max_spec_le (k - 53) (-1074)); omega. } pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_expr (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)) (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2))%R). destruct (rel_error_exists) as [eps [bounded_eps round_eq]]. + eapply Rle_trans; eauto. unfold minValue, Z.pow_pos; simpl. rewrite Q2R_inv. * apply Rinv_le. { rewrite <- Q2R0_is_0. apply Qlt_Rlt. apply Qlt_alt. vm_compute; auto. } { unfold Q2R. unfold Qnum, Qden. lra. } * vm_compute; congruence. + simpl in *. rewrite round_eq. destruct (validVal eps) 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, 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. Qed. (* (fexpr_correct 53 1024 eq_refl) as fexpr_corr. *) (* (relative_error_N_ex radix2 (Fcore_FLT.FLT_expr (3 -1024 - 53) 53) *) (* (-1022)%Z 53%Z) *) Lemma eval_expr_gives_IEEE (e:expr fl64) : forall E1 E2 E2_real Gamma tMap vR A P fVars dVars, (forall x, (toREnv E2) x = E2_real x) -> typeCheck (B2Qexpr e) Gamma tMap = true -> approxEnv E1 Gamma A fVars dVars E2_real -> validIntervalbounds (B2Qexpr e) A P dVars = true -> validErrorbound (B2Qexpr e) tMap A dVars = true -> FPRangeValidator (B2Qexpr e) A tMap dVars = true -> eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) vR M64 -> NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars -> is64BitEval (B2Qexpr e) -> noDowncast (B2Qexpr e) -> eval_expr_valid e E2 -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) Gamma -> (forall v, NatSet.In v dVars -> exists vF m, (E2_real v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m)) -> (forall v, NatSet.In v (usedVars (B2Qexpr e)) -> Gamma v = Some M64) -> exists v, eval_expr_float e E2 = Some v /\ eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr 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 usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e fVars_defined vars_typed dVars_sound dVars_valid usedVars_64bit; (match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *)); Flover_compute_asm; try congruence; type_conv; subst; unfold Ltacs.optionLift. - unfold toREnv in *. destruct (E2 n) eqn:HE2; try congruence. exists f; split; try eauto. eapply Var_load; try auto. rewrite HE2; auto. - eexists; split; try eauto. eapply (Const_dist' (delta:=0%R)); eauto. + rewrite Rabs_R0; apply mTypeToQ_pos_R. + unfold perturb. lra. - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto. assert (is_finite 53 1024 v_e = true). { apply validValue_is_finite. eapply FPRangeValidator_sound; eauto. eapply eval_eq_env; eauto. } rewrite eval_float_e. exists (b64_opp v_e); split; try auto. unfold b64_opp. rewrite <- (is_finite_Bopp _ _ pair) in H. rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp. eapply Unop_neg'; eauto. unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto. - repeat (match goal with |H: _ /\ _ |- _ => destruct H end). assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\ FloverMap.find (B2Qexpr e2) tMap = Some M64 /\ FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64) as [tMap_e1 [tMap_e2 tMap_b]]. { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto. - intros; apply usedVars_64bit; set_tac. - intros; apply usedVars_64bit; set_tac. - rewrite Heqo, Heqo4, Heqo6. apply Is_true_eq_true; 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. } repeat destr_factorize. assert (m1 = M64). { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. } assert (m2 = M64). { eapply typing_agrees_expr; eauto. } subst. 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. edestruct (validIntervalbounds_sound (B2Qexpr e2)) as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]]; eauto; set_tac. destr_factorize. destruct iv_2 as [ivlo_2 ivhi_2]. assert (forall vF2 m2, eval_expr E2_real Gamma (toRExp (B2Qexpr e2)) vF2 m2 -> (Rabs (nR2 - vF2) <= Q2R err_2))%R. { eapply validErrorbound_sound; try eauto; try set_tac. } assert (contained (Q2R (B2Q v_e2)) (widenInterval (Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))). { 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 R3. apply le_neq_bool_to_lt_prop in L3. destruct L3; 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 (B2Qexpr e1) (B2Qexpr 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. - Flover_compute. apply Is_true_eq_true. repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left. - Flover_compute. 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. - inversion Heqo1; subst. rewrite Heqo0. rewrite Heqo. apply Is_true_eq_true. repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. rewrite Heqo3, Heqo5. apply Is_true_eq_left. inversion Heqo2; subst. auto. - rewrite Heqo, Heqo0. apply Is_true_eq_true. inversion Heqo1; inversion Heqo2; subst. repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. } assert (validFloatValue (Q2R (B2Q v_e1)) M64). { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac. eapply eval_eq_env; eauto. } assert (validFloatValue (Q2R (B2Q v_e2)) M64). { eapply (FPRangeValidator_sound (B2Qexpr 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 (B2Qexpr e1) (B2Qexpr 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. - cbn. Flover_compute. apply Is_true_eq_true. repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). - cbn. Flover_compute. apply Is_true_eq_true. repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). - cbn. Flover_compute. inversion Heqo1; inversion Heqo2; subst. apply Is_true_eq_true. repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). - cbn. Flover_compute. inversion Heqo1; inversion Heqo2; subst. 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 R3. apply le_neq_bool_to_lt_prop in L3. destruct L3 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 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1 IHe2. pose proof (fexpr_correct 53 1024 eq_refl) as fexpr_corr. assert (forall k : Z, (-1022 < k)%Z -> (53 <= k - Fcore_FLT.FLT_expr (3 - 1024 - 53) 53 k)%Z) as expr_valid. { intros k k_pos. unfold Fcore_FLT.FLT_expr; simpl. destruct (Z.max_spec_le (k - 53) (-1074)); omega. } pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_expr (3 -1024 - 53) 53) (-1022)%Z 53%Z expr_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. rewrite <- INR_IPR in H1. simpl in H1. lra. } pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid. destruct b; revert H1; intros case_eval. (* Addition *) + unfold evalBinop in *. unfold b64_plus. pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE v_e1 v_e2 finite_e1 finite_e2) as addition_correct. rewrite cond_valid in addition_correct. destruct addition_correct as [add_round [finite_res _]]. destruct case_eval as [eval_zero | eval_normal]. (* resutl is zero *) * rewrite eval_zero in *. rewrite round_0_zero in *. exists (Bplus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2). split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode; rewrite add_round. eapply Binop_dist' with (delta:=0%R); eauto. rewrite Rabs_R0; apply mTypeToQ_pos_R. unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto; lra. * simpl in *. destruct (rel_error_exists (fun x => negb (Zeven x)) (B2R 53 1024 v_e1 + B2R 53 1024 v_e2)%R) as [eps [eps_bounded round_eq]]. { eapply Rle_trans; eauto. unfold minValue, minExponentPos. rewrite Q2R_inv; [ | vm_compute; congruence]. unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR. vm_compute. lra. } { exists (Bplus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2); split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode. eapply Binop_dist' with (delta:=eps); eauto. - unfold mTypeToQ. assert (join M64 M64 = M64) by (vm_compute; auto). rewrite H1. eapply Rle_trans; eauto. unfold Qpower. unfold Qpower_positive. assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 ) by (vm_compute; auto). rewrite H12. rewrite Q2R_inv; try lra. - unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto. rewrite <- round_eq. rewrite <- add_round; auto. } (* Subtraction *) + unfold evalBinop in *. unfold b64_minus. pose proof (Bminus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE v_e1 v_e2 finite_e1 finite_e2) as subtraction_correct. rewrite cond_valid in subtraction_correct. destruct subtraction_correct as [add_round [finite_res _]]. destruct case_eval as [eval_zero | eval_normal]. (* resutl is zero *) * rewrite eval_zero in *. rewrite round_0_zero in *. exists (Bminus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2). split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode; rewrite add_round. eapply Binop_dist' with (delta:=0%R); eauto. rewrite Rabs_R0; apply mTypeToQ_pos_R. unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto; lra. * simpl in *. destruct (rel_error_exists (fun x => negb (Zeven x)) (B2R 53 1024 v_e1 - B2R 53 1024 v_e2)%R) as [eps [eps_bounded round_eq]]. { eapply Rle_trans; eauto. unfold minValue, minExponentPos. rewrite Q2R_inv; [ | vm_compute; congruence]. unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR. vm_compute. lra. } { exists (Bminus 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2); split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode. eapply Binop_dist' with (delta:=eps); eauto. - unfold mTypeToQ. assert (join M64 M64 = M64) by (vm_compute; auto). rewrite H1. eapply Rle_trans; eauto. unfold Qpower. unfold Qpower_positive. assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 ) by (vm_compute; auto). rewrite H12. rewrite Q2R_inv; try lra. - unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto. rewrite <- round_eq. rewrite <- add_round; auto. } (* Multiplication *) + unfold evalBinop in *. unfold b64_mult. pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE v_e1 v_e2) as mult_correct. rewrite cond_valid in mult_correct. destruct mult_correct as [mult_round [finite_res _]]. destruct case_eval as [eval_zero | eval_normal]. (* resutl is zero *) * rewrite eval_zero in *. rewrite round_0_zero in *. exists (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2). split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode; rewrite mult_round. eapply Binop_dist' with (delta:=0%R); eauto. rewrite Rabs_R0; apply mTypeToQ_pos_R. unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto; lra. rewrite finite_e1, finite_e2 in finite_res. auto. * simpl in *. destruct (rel_error_exists (fun x => negb (Zeven x)) (B2R 53 1024 v_e1 * B2R 53 1024 v_e2)%R) as [eps [eps_bounded round_eq]]. { eapply Rle_trans; eauto. unfold minValue, minExponentPos. rewrite Q2R_inv; [ | vm_compute; congruence]. unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR. vm_compute. lra. } { exists (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2); split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode. eapply Binop_dist' with (delta:=eps); eauto. - unfold mTypeToQ. assert (join M64 M64 = M64) by (vm_compute; auto). rewrite H1. eapply Rle_trans; eauto. unfold Qpower. unfold Qpower_positive. assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 ) by (vm_compute; auto). rewrite H12. rewrite Q2R_inv; try lra. - unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto. rewrite <- round_eq. rewrite <- mult_round; auto. - rewrite finite_e1, finite_e2 in finite_res; auto. } (* Division *) + unfold evalBinop in *. unfold b64_div. pose proof (Bdiv_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE v_e1 v_e2) as division_correct. rewrite cond_valid in division_correct. destruct division_correct as [div_round [finite_res _]]. rewrite <- B2Q_B2R_eq; auto. destruct case_eval as [eval_zero | eval_normal]. (* resutl is zero *) * rewrite eval_zero in *. rewrite round_0_zero in *. exists (Bdiv 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2). split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode; rewrite div_round. eapply Binop_dist' with (delta:=0%R); eauto. rewrite Rabs_R0; apply mTypeToQ_pos_R. unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto; lra. rewrite finite_e1 in finite_res; auto. * simpl in *. destruct (rel_error_exists (fun x => negb (Zeven x)) (B2R 53 1024 v_e1 / B2R 53 1024 v_e2)%R) as [eps [eps_bounded round_eq]]. { eapply Rle_trans; eauto. unfold minValue, minExponentPos. rewrite Q2R_inv; [ | vm_compute; congruence]. unfold Q2R, Qnum, Qden. rewrite <- Z2R_IZR. vm_compute. lra. } { exists (Bdiv 53 1024 eq_refl eq_refl binop_nan_pl64 dmode v_e1 v_e2); split; try auto. rewrite B2Q_B2R_eq; try auto. unfold dmode. eapply Binop_dist' with (delta:=eps); eauto. - unfold mTypeToQ. assert (join M64 M64 = M64) by (vm_compute; auto). rewrite H1. eapply Rle_trans; eauto. unfold Qpower. unfold Qpower_positive. assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 ) by (vm_compute; auto). rewrite H12. rewrite Q2R_inv; try lra. - unfold perturb, evalBinop. repeat rewrite B2Q_B2R_eq; try auto. rewrite <- round_eq. rewrite <- div_round; auto. - rewrite finite_e1 in finite_res; auto. } - repeat (match goal with |H: _ /\ _ |- _ => destruct H end). assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\ FloverMap.find (B2Qexpr e2) tMap = Some M64 /\ FloverMap.find (B2Qexpr e3) tMap = Some M64 /\ FloverMap.find (Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)) tMap = Some M64) as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]]. { repeat split; apply (typing_expr_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, Heqo4, Heqo6, Heqo8. 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. } repeat destr_factorize. inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst. assert (m1 = M64). { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. } assert (m2 = M64). { eapply (typing_agrees_expr (B2Qexpr e2)); eauto. } assert (m3 = M64). { eapply (typing_agrees_expr (B2Qexpr e3)); eauto. } subst. 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 | ]. 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) : forall E1 E2 E2_real Gamma tMap vR vF A P fVars dVars outVars, (forall x, (toREnv E2) x = E2_real x) -> approxEnv E1 Gamma A fVars dVars E2_real -> ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars -> typeCheckCmd (B2Qcmd f) Gamma tMap = true -> 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 (toRCmd (B2Qcmd f)) (toREnv E2) Gamma vF M64 -> NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars -> is64BitBstep (B2Qcmd f) -> noDowncastFun (B2Qcmd f) -> bstep_valid f E2 -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) Gamma -> (forall v, NatSet.In v dVars -> exists vF m, (E2_real v = Some vF /\ FloverMap.find (Var Q v) tMap= Some m /\ validFloatValue vF m)) -> (forall v, NatSet.In v (freeVars (B2Qcmd f)) -> Gamma v = Some M64) -> exists v, bstep_float f E2 = Some v /\ bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (Q2R (B2Q v)) M64. Proof. induction f; intros * envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f valid_roundoffs_f valid_float_ranges bstep_real bstep_float freeVars_sound is64_eval nodowncast_f bstep_sound dVars_sound fVars_defined vars_typed dVars_valid freeVars_typed; cbn in *; Flover_compute_asm; try congruence; type_conv; subst; unfold Ltacs.optionLift; inversion bstep_float; inversion bstep_real; inversion ssa_f; subst; simpl in *; repeat (match goal with | H: _ = true |- _ => andb_to_prop H end). - assert (FloverMap.find (B2Qexpr e) tMap= Some M64). { eapply typing_expr_64_bit; try eauto. simpl in *; destruct nodowncast_f; auto. destruct is64_eval; auto. intros; apply freeVars_typed. set_tac. split; [ set_tac | ]. hnf; intros; subst. apply H26. apply (H25 n H). } assert (m1 = M64). { eapply typing_agrees_expr; eauto. } subst. assert (exists v_e, eval_expr_float e E2 = Some v_e /\ eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64) as eval_float_e. { eapply eval_expr_gives_IEEE; try eauto. - hnf; intros. rewrite NatSet.diff_spec in H0. destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25. destruct H25; try congruence; auto. - destruct is64_eval; auto. - destruct nodowncast_f; auto. - destruct bstep_sound; auto. - intros. apply freeVars_typed. rewrite NatSet.remove_spec, NatSet.union_spec. split; try auto. hnf; intros; subst. specialize (H25 n H0). set_tac. apply H26; set_tac. } destruct eval_float_e as [v_e [eval_float_e eval_rel_e]]. assert (forall v m, eval_expr E2_real Gamma (toRExp (B2Qexpr e)) v m -> Rabs (v0 - v) <= Q2R e2)%R as err_e_valid. { eapply validErrorbound_sound; try eauto. - hnf; intros. rewrite NatSet.diff_spec in H0. destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25. destruct H25; try auto; congruence. } assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e2)%R. { eapply err_e_valid. eapply eval_eq_env; eauto. } (* Now construct a new evaluation according to our big-step semantics using lemma validErrorboundCmd_gives_eval *) (* destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f. *) (* destruct iv_f as [ivlo_f ivhi_f]. *) edestruct (validIntervalboundsCmd_sound) as [iv_ret [err_ret [v_ret [map_ret [eval_ret bound_ret]]]]]; eauto. { cbn. Flover_compute. rewrite L0, R4, R3, R2. auto. } assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m). { eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1) (elo:=fst(iv_ret)) (ehi:=snd(iv_ret)) (err:= err_ret); eauto. - eapply approxUpdBound; eauto. rewrite Qeq_bool_iff in R1. eapply Rle_trans; eauto. canonize_hyps. rewrite <- R1. inversion Heqo0; subst; lra. - eapply ssa_equal_set; eauto. hnf; split; intros. + rewrite NatSet.add_spec, NatSet.union_spec in *. rewrite NatSet.add_spec in H1; destruct H1; auto. destruct H1; auto. + rewrite NatSet.add_spec in H1; rewrite NatSet.union_spec, NatSet.add_spec in *; destruct H1; auto. destruct H1; auto. - hnf; intros. rewrite NatSet.diff_spec in H1. destruct H1. apply freeVars_sound. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. 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))); eauto. intros; unfold updDefVars, toRMap. destruct (n0 =? n); auto. - unfold dVars_range_valid in *. intros. unfold updEnv. set_tac. destruct H1; subst. + exists v0, (q1, q2), e1; split; try eauto. * rewrite Nat.eqb_refl; auto. * split; try auto. edestruct validIntervalbounds_sound as [iv_e [err_e [v_e' [map_e [? ?]]]]]; eauto. { set_tac; split; try auto. split; try auto. hnf; intros. eapply H26. subst; set_tac. } simpl. destr_factorize; simpl in *. canonize_hyps. rewrite <- R4, <- R3. rewrite <- (meps_0_deterministic _ H17 H1) in H2; auto. + destruct H1. rewrite <- Nat.eqb_neq in H1. rewrite H1. apply dVars_sound; auto. - unfold fVars_P_sound; intros; unfold updEnv. destruct (v1 =? n) eqn:?. + rewrite Nat.eqb_eq in Heqb; subst; exfalso. set_tac. apply H26; rewrite NatSet.union_spec; auto. + apply fVars_defined; auto. - unfold IntervalValidation.vars_typed. intros. unfold updDefVars. destruct (v1 =? n) eqn:?. + exists M64; auto. + apply vars_typed. rewrite Nat.eqb_neq in Heqb. rewrite NatSet.union_spec, NatSet.add_spec in H1. rewrite NatSet.union_spec. destruct H1 as [HA |[HB | HC]]; try auto; congruence. - destruct iv_ret; auto. } unfold optionLift. rewrite eval_float_e. assert (FloverMap.find (getRetExp (B2Qcmd f)) tMap= Some M64). { eapply typingSoundnessCmd; eauto. } destruct H1 as [vF_new [m_f bstep_float_new]]. assert (m_f = M64). { eapply typing_agrees_cmd; eauto. } subst. destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap vR vF_new A P fVars (NatSet.add n dVars) outVars); try eauto. + intros. unfold toREnv, updFlEnv, updEnv. destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto. + eapply approxUpdBound; eauto. eapply Rle_trans; eauto. canonize_hyps. inversion Heqo0; subst. lra. + eapply ssa_equal_set; eauto. hnf; split; intros. * rewrite NatSet.add_spec, NatSet.union_spec in *. rewrite NatSet.add_spec in H1; destruct H1; auto. destruct H1; auto. * 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))); eauto. intros; unfold updDefVars, toRMap. destruct (n0 =? n); auto. + eapply (bstep_eq_env (E1 := updEnv n (Q2R (B2Q v_e)) E2_real)); eauto. intros x; unfold updEnv, updFlEnv, toREnv. destruct (x =? n); try auto. rewrite <- envs_eq. auto. + hnf; intros. rewrite NatSet.diff_spec in *. destruct H1. apply freeVars_sound. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. split; try auto. hnf; intros; subst. apply H3. rewrite NatSet.add_spec. auto. rewrite NatSet.add_spec in H3. hnf; intros; apply H3; auto. + destruct is64_eval as [HA [HB HC]]; auto. + destruct nodowncast_f as [HA HB]; auto. + destruct bstep_sound as [eval_sound bstep_sound]. rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound. auto. + unfold dVars_range_valid in *; intros; unfold updEnv. destruct (v1 =? n) eqn:?. * set_tac. rewrite Nat.eqb_eq in Heqb; subst. destruct H1 as [? | [? ?]]; try congruence. exists v0. edestruct validIntervalbounds_sound as [iv_e [err_e [? [? [? ?]]]]]; eauto. { set_tac; split; auto. split; auto. hnf; intros; subst; set_tac. } canonize_hyps. destr_factorize; simpl in *. exists (q1,q2), e1. split; try auto. split; try auto. simpl in *. rewrite R4, R3 in *. rewrite <- (meps_0_deterministic _ H4 H17). auto. * eapply dVars_sound; set_tac. destruct H1; rewrite Nat.eqb_neq in Heqb; try congruence. destruct H1; auto. + unfold fVars_P_sound. intros; unfold updEnv. destruct (v1 =? n) eqn:?. * rewrite Nat.eqb_eq in Heqb; subst; exfalso. set_tac. apply H26; rewrite NatSet.union_spec; auto. * apply fVars_defined. auto. + unfold IntervalValidation.vars_typed. intros. unfold updDefVars. destruct (v1 =? n) eqn:?. * exists M64; auto. * apply vars_typed. rewrite Nat.eqb_neq in Heqb. rewrite NatSet.union_spec, NatSet.add_spec in H1. rewrite NatSet.union_spec. destruct H1 as [HA |[HB | HC]]; try auto; congruence. + intros. rewrite NatSet.add_spec in H1; unfold updEnv. destruct (v1 =? n) eqn:?; destruct H1; subst; try congruence. * exists (Q2R (B2Q v_e)). exists M64; repeat split; try auto. eapply FPRangeValidator_sound; eauto. { eapply eval_eq_env; eauto. } { set_tac. split; try auto. split; try auto. hnf; intros; subst. set_tac. } * rewrite Nat.eqb_eq in Heqb; subst. exists (Q2R (B2Q v_e)); rewrite H in *. exists M64; repeat split; try auto. eapply FPRangeValidator_sound; eauto. { eapply eval_eq_env; eauto. } { set_tac. split; try auto. split; try auto. hnf; intros; subst. set_tac. } * rewrite Nat.eqb_neq in Heqb; congruence. * apply dVars_valid; auto. + intros. unfold updDefVars. destruct (v1 =? n) eqn:?; try auto. apply freeVars_typed; set_tac. split; try auto. hnf; intros; subst; rewrite Nat.eqb_neq in Heqb; congruence. + exists x; destruct H1; split; try auto. eapply let_b; eauto. eapply bstep_eq_env with (E1:= toREnv (updFlEnv n v_e E2)); eauto. intros; unfold toREnv, updFlEnv, updEnv. destruct (x0 =? n); auto. - edestruct (eval_expr_gives_IEEE); eauto. exists x; destruct H. split; try auto. apply ret_b; auto. Qed. Theorem IEEE_connection_expr e A P E1 E2 defVars: approxEnv E1 defVars A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) -> is64BitEval (B2Qexpr e) -> noDowncast (B2Qexpr e) -> eval_expr_valid e E2 -> (forall v, NatSet.In v (usedVars (B2Qexpr e)) -> defVars v = Some M64) -> (forall v, NatSet.In v (usedVars (B2Qexpr e)) -> exists vR, (E1 v = Some vR) /\ Q2R (fst (P v)) <= vR <= Q2R(snd (P v)))%R -> (forall v, NatSet.In v (usedVars (B2Qexpr e)) -> exists m, defVars v = Some m) -> 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_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. Proof. intros. edestruct Certificate_checking_is_sound; eauto. destruct H7 as [err [vR [vF [mF [map_e [eval_real [eval_float roundoff_sound]]]]]]]. unfold CertificateChecker in H6. andb_to_prop H6. assert (FloverMap.find (B2Qexpr e) (typeMap defVars (B2Qexpr e) (FloverMap.empty mType)) = Some M64). { eapply typing_expr_64_bit; eauto. } assert (mF = M64). { eapply typing_agrees_expr; eauto. } subst. edestruct eval_expr_gives_IEEE; eauto. + set_tac. + unfold dVars_range_valid. intros. inversion H7. + unfold vars_typed. intros. apply H5. set_tac. destruct H7; try auto. inversion H7. + intros. inversion H7. + destruct H7 as [eval_float_f eval_rel]. exists x, err, vR, x0. repeat split; try auto. eapply roundoff_sound; eauto. Qed. Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P defVars E1 E2: approxEnv E1 defVars A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) -> is64BitBstep (B2Qcmd f) -> noDowncastFun (B2Qcmd f) -> bstep_valid f E2 -> (forall v, NatSet.In v (freeVars (B2Qcmd f)) -> defVars v = Some M64) -> (forall v, NatSet.mem v (freeVars (B2Qcmd f))= true -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> (forall v, (v) mem (freeVars (B2Qcmd f)) = true -> exists m : mType, defVars v = Some m) -> 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_float f E2 = Some vF /\ bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (Q2R (B2Q vF)) m /\ (forall vF m, bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars vF m -> (Rabs (vR - vF) <= Q2R err)%R). (** The proofs is a simple composition of the soundness proofs for the range validator and the error bound validator. **) Proof. intros. unfold CertificateCheckerCmd in *. andb_to_prop H6. pose proof (validSSA_sound _ _ R0). destruct H6 as [outVars ssa_f]. edestruct Certificate_checking_cmds_is_sound; eauto. - intros. apply H4. set_tac. - unfold CertificateCheckerCmd. apply Is_true_eq_true. repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). - destruct H6 as [err [vR [vF [m [map_ret [bstep_real [bstep_float roundoff_sound]]]]]]]. assert (FloverMap.find (getRetExp (B2Qcmd f)) (typeMapCmd defVars (B2Qcmd f) (FloverMap.empty mType)) = Some M64). { eapply typing_cmd_64_bit; eauto. } assert (m = M64). { eapply typing_agrees_cmd; eauto. } subst. edestruct bstep_gives_IEEE; eauto. + eapply ssa_equal_set; eauto. hnf; intros; split; intros; set_tac. destruct H7; try auto. inversion H7. + set_tac. + unfold dVars_range_valid. intros. inversion H7. + unfold fVars_P_sound; intros. apply H4; rewrite NatSet.mem_spec; auto. + unfold vars_typed. intros. apply H5. set_tac. destruct H7; try auto. inversion H7. + intros. inversion H7. + destruct H7. exists x, err, vR, x0, M64. repeat split; auto. Qed.