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 normal_or_zero v := (v = 0 \/ (Q2R (minValue_pos 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 => olet res := eval_expr_float e E in bstep_float g (updFlEnv x res E) | Ret e => eval_expr_float e E end. Definition isValid e := plet v := e in normal_or_zero (B2R 53 1024 v). 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 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 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 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) | 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 /\ (optionBind (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 | Zpos p => (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_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_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) 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 (Zpos 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_pos, maxExponent, minExponentPos in*; rewrite Q2R_inv in *; unfold bpowQ in *. - cbn in *. destruct H; try lra. rewrite Rabs_right in H0. apply Rle_Qle in H0. + rewrite <- Qle_bool_iff in H0. cbv in H0; 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 fBits: forall Gamma tMap, noDowncast e -> is64BitEval e -> typeCheck e Gamma tMap fBits = 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. - Flover_compute; try congruence; type_conv; subst. destruct m; try congruence. - Flover_compute; try congruence; type_conv; subst. erewrite IHe in *; eauto. - repeat (match goal with |H: _ /\ _ |- _=> destruct H end). erewrite IHe1 with (Gamma:=Gamma) in *; eauto. + erewrite IHe2 with (Gamma:=Gamma) in *; eauto. * simpl in *. Flover_compute; try congruence. type_conv; subst; auto. * Flover_compute; auto. * intros. apply types_valid. set_tac. + Flover_compute; auto. + intros; apply types_valid; set_tac. - repeat (match goal with |H: _ /\ _ |- _=> destruct H end). erewrite IHe1 with (Gamma:=Gamma) in *; eauto; [ | Flover_compute; try congruence; auto | intros; apply types_valid; set_tac]. erewrite IHe2 with (Gamma:=Gamma) in *; eauto; [ | Flover_compute; try congruence; auto | intros; apply types_valid; set_tac]. erewrite IHe3 with (Gamma:=Gamma) in *; eauto; [ | Flover_compute; try congruence; auto | intros; apply types_valid; set_tac]. unfold join3, join in *. simpl in *. Flover_compute; try congruence; type_conv; auto. Qed. Lemma typing_cmd_64_bit f: forall Gamma tMap fBits, noDowncastFun f -> is64BitBstep f -> typeCheckCmd f Gamma tMap fBits = 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 fBits, typeCheck e Gamma tMap fBits = true -> eval_expr E Gamma (toRBMap fBits) (toRExp e) v m1 -> FloverMap.find e tMap = Some m2 -> m1 = m2. Proof. intros. pose proof (typingSoundnessExp _ _ H H0). congruence. Qed. Lemma typing_agrees_cmd f: forall E Gamma tMap v m1 m2 fBits, typeCheckCmd f Gamma tMap fBits = true -> bstep (toRCmd f) E Gamma (toRBMap fBits) v m1 -> FloverMap.find (getRetExp f) tMap = Some m2 -> m1 = m2. Proof. intros. pose proof (typingSoundnessCmd _ _ H H0). congruence. 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. 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_exp. 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_exp (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 (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)) (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_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. + 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_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. Qed. (* (fexpr_correct 53 1024 eq_refl) as fexpr_corr. *) (* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (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 fVars dVars fBits, (forall x, (toREnv E2) x = E2_real x) -> typeCheck (B2Qexpr e) Gamma tMap fBits = true -> approxEnv E1 Gamma A fVars dVars E2_real -> validRanges (B2Qexpr e) A E1 Gamma (toRBMap fBits) -> validErrorbound (B2Qexpr e) tMap A dVars = true -> FPRangeValidator (B2Qexpr e) A tMap dVars = true -> eval_expr (toREnv E2) Gamma (toRBMap fBits) (toRExp (B2Qexpr e)) vR M64 -> NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars -> is64BitEval (B2Qexpr e) -> noDowncast (B2Qexpr e) -> eval_expr_valid e E2 -> 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 (toRBMap fBits) (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64. Proof. Opaque typeCheck. 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 vars_typed dVars_sound usedVars_64bit; (match_pat (eval_expr _ _ _ _ _ _) (fun H => inversion H; subst; simpl in *)); revert eval_IEEE_valid_e; Flover_compute_asm; try congruence; type_conv; subst; unfold optionBind; intros eval_IEEE_valid_e. Transparent typeCheck. - 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') with (delta:=0%R); eauto. + rewrite Rabs_R0; apply mTypeToR_pos_R. + unfold perturb. lra. - destruct valid_rangebounds as [valid_e valid_intv]. edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto. { cbn in typecheck_e; Flover_compute; auto. } assert (is_finite 53 1024 v_e = true). { apply validValue_is_finite. eapply FPRangeValidator_sound with (e:=B2Qexpr e); eauto. - eapply eval_eq_env; eauto. - cbn in typecheck_e; Flover_compute; auto. } 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 _ fBits Gamma); simpl; auto. - cbn in typecheck_e; Flover_compute; auto. - intros; apply usedVars_64bit; set_tac. - cbn in typecheck_e; Flover_compute; auto. - intros; apply usedVars_64bit; set_tac. } repeat destr_factorize. assert (m1 = M64). { apply (typing_agrees_expr (v:=v1) (B2Qexpr e1) (E:=toREnv E2) (Gamma:=Gamma) tMap (fBits:=fBits)); try auto. cbn in typecheck_e; Flover_compute; auto. } assert (m2 = M64). { apply (typing_agrees_expr (v:=v2) (B2Qexpr e2) (E:=toREnv E2) (Gamma:=Gamma) tMap (fBits:=fBits)); try auto. cbn in typecheck_e; Flover_compute; auto. } subst. destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars fBits) as [v_e1 [eval_float_e1 eval_rel_e1]]; try auto; try set_tac; [ cbn in typecheck_e; Flover_compute; auto | intros; apply usedVars_64bit ; set_tac | ]. destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars fBits) as [v_e2 [eval_float_e2 eval_rel_e2]]; try auto; try set_tac; [ cbn in typecheck_e; Flover_compute; auto | intros; apply usedVars_64bit ; set_tac | ]. pose proof (validRanges_single _ _ _ _ _ H15) as valid_e. destruct valid_e as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]]. rewrite eval_float_e1, eval_float_e2. inversion Heqo1; subst. destr_factorize. destruct iv_2 as [ivlo_2 ivhi_2]. assert (forall vF2 m2, eval_expr E2_real Gamma (toRBMap fBits) (toRExp (B2Qexpr e2)) vF2 m2 -> (Rabs (nR2 - vF2) <= Q2R err_2))%R. { eapply validErrorbound_sound; try eauto; set_tac. cbn in typecheck_e; Flover_compute; auto. } 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 H16. 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. rewrite Heqo2 in *. destruct i1; symmetry in map_e2; inversion map_e2; subst. destruct L3; hnf; intros. - rewrite H19 in *. apply Qlt_Rlt in H18. rewrite Q2R0_is_0, Q2R_plus in H18. simpl in *; lra. - rewrite H19 in *. apply Qlt_Rlt in H18. rewrite Q2R0_is_0, Q2R_minus in H18; simpl in *; 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' with (delta:=0%R); eauto. + rewrite Rabs_R0. apply mTypeToR_pos_R. + unfold perturb; lra. - repeat split; try auto. + intros ? iv2 err2 find. subst. destruct iv2; rewrite find in *; eapply H12; eauto. + rewrite Heqo0. auto. - Flover_compute. apply Is_true_eq_true. repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left. rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst. apply andb_prop_intro; split; apply Is_true_eq_left; try auto. rewrite L4, R1. auto. - Flover_compute. apply Is_true_eq_true. repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. } rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst. assert (validFloatValue (Q2R (B2Q v_e1)) M64). { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac. eapply eval_eq_env; eauto. cbn in typecheck_e; Flover_compute_asm; auto. } assert (validFloatValue (Q2R (B2Q v_e2)) M64). { eapply (FPRangeValidator_sound (B2Qexpr e2)); try eauto; try set_tac. - eapply eval_eq_env; eauto. - cbn in typecheck_e; Flover_compute_asm; auto. } 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. simpl. lra. + unfold perturb. repeat rewrite B2Q_B2R_eq; try auto. - cbn; repeat split; try auto. + intros ? iv2 err2 find. subst. destruct iv2; rewrite find in *; eapply H12; eauto. + rewrite Heqo0. 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. 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 H23 in *. apply Qlt_Rlt in case_low. rewrite Q2R0_is_0, Q2R_plus in case_low. lra. - rewrite H23 in *. apply Qlt_Rlt in case_high. rewrite Q2R0_is_0, Q2R_minus in case_high; lra. } clear H2 H12 dVars_sound usedVars_64bit vars_typed usedVars_sound R2 R1 L1 L L0 R3 L2 Heqo Heqo0 Heqo1 IHe1 IHe2. 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. rewrite eval_float_e1, eval_float_e2 in H1. unfold optionBind, 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 as [eval_is_zero | eval_normal]; try auto. left; unfold Normal, Denormal in H15; unfold Normal; destruct H19 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 eval_normal. unfold minValue_pos, minExponentPos in eval_normal. rewrite Q2R_inv in eval_normal; [|vm_compute; congruence]. unfold Q2R, Qnum, Qden in eval_normal. assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z) by (vm_compute; auto). rewrite H1 in eval_normal. rewrite <- Z2R_IZR in eval_normal. unfold IZR in eval_normal. simpl in eval_normal. rewrite <- INR_IPR in eval_normal. simpl in eval_normal. lra. } pose proof (validValue_bounded b v_e1 v_e2 H2 H22) 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 mTypeToR_pos_R. } { unfold perturb, evalBinop. cbn. 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_pos, 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. - cbn; 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 mTypeToR_pos_R. unfold perturb, evalBinop; cbn. 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_pos, 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. - cbn; lra. - unfold perturb, evalBinop; cbn. 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 mTypeToR_pos_R. unfold perturb, evalBinop; cbn. 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_pos, 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. - cbn; 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 mTypeToR_pos_R. unfold perturb, evalBinop; cbn. 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_pos, 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. - cbn; 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 (typeCheck (B2Qexpr e1) Gamma tMap fBits = true /\ typeCheck (B2Qexpr e2) Gamma tMap fBits = true /\ typeCheck (B2Qexpr e3) Gamma tMap fBits = true) as [typecheck_e1 [typecheck_e2 typecheck_e3]]. { repeat split; cbn in typecheck_e; Flover_compute; auto. } 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; try apply (typing_expr_64_bit _ fBits Gamma); simpl; auto. - intros; apply usedVars_64bit; set_tac. - intros; apply usedVars_64bit; set_tac. - intros; apply usedVars_64bit; set_tac. } 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 fVars dVars fBits) 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 fVars dVars fBits) 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 fVars dVars fBits) as [v_e3 [eval_float_e3 eval_rel_e3]]; try auto; try set_tac; [ intros; apply usedVars_64bit ; set_tac | ]. rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H6. contradiction H6. - inversion noDowncast_e. Qed. Lemma bstep_gives_IEEE (f:cmd fl64) : forall E1 E2 E2_real Gamma tMap vR vF A fVars dVars outVars fBits, (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 fBits = true -> validRangesCmd (B2Qcmd f) A E1 Gamma (toRBMap fBits) -> validErrorboundCmd (B2Qcmd f) tMap A dVars = true -> FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true -> bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) (toRBMap fBits) vR REAL -> bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (toRBMap fBits) vF M64 -> NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars -> is64BitBstep (B2Qcmd f) -> noDowncastFun (B2Qcmd f) -> bstep_valid f E2 -> 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 (toRBMap fBits) (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 vars_typed dVars_valid freeVars_typed; cbn in *; revert bstep_sound; Flover_compute_asm; try congruence; type_conv; subst; intros bstep_sound; unfold Ltacs.optionBind; 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 H28. apply (H27 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 (toRBMap fBits) (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64) as eval_float_e. { eapply eval_expr_gives_IEEE; try eauto. - destruct valid_ranges_f as [[? ?] ?]; auto. - hnf; intros. rewrite NatSet.diff_spec in H0. destruct H0. specialize (H27 a H0). rewrite NatSet.union_spec in H27. destruct H27; 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 (H27 n H0). set_tac. apply H28; set_tac. } destruct eval_float_e as [v_e [eval_float_e eval_rel_e]]. assert (forall v m, eval_expr E2_real Gamma (toRBMap fBits) (toRExp (B2Qexpr e)) v m -> Rabs (v0 - v) <= Q2R e0)%R as err_e_valid. { eapply validErrorbound_sound; try eauto. - hnf; intros. rewrite NatSet.diff_spec in H0. destruct H0. specialize (H27 a H0). rewrite NatSet.union_spec in H27. destruct H27; try auto; congruence. - destruct valid_ranges_f as [[? ?] ?]; auto. - instantiate (1:= snd i). instantiate (1:=fst i). destruct i; simpl in *; auto. } assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e0)%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 valid_ranges_f as [[valid_e valid_cont] valid_single]. destruct valid_single as [iv_ret [err_ret [v_ret [map_ret [eval_ret bound_ret]]]]]. assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) (toRBMap fBits) 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 REAL (toRMap Gamma))); eauto. intros; unfold updDefVars, toRMap. destruct (n0 =? n); auto. - eapply validRangesCmd_swap with (Gamma1 :=updDefVars n REAL Gamma); try auto. intros x; unfold toRMap, updDefVars. destruct (x =? n); auto. - unfold RealRangeArith.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 optionBind. 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 fVars (NatSet.add n dVars) outVars fBits); 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 validRangesCmd_swap with (Gamma1 := updDefVars n REAL Gamma); try auto. intros x; unfold toRMap, updDefVars. destruct (x =? n); auto. + eapply (swap_Gamma_bstep (Gamma1:= updDefVars n REAL (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 optionBind in bstep_sound. auto. + unfold RealRangeArith.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. - destruct valid_ranges_f as [? ?]. edestruct (eval_expr_gives_IEEE) as [v_res [eval_float eval_e]]; eauto. exists v_res; split; try auto. apply ret_b; auto. Qed. Theorem IEEE_connection_expr e A P E1 E2 defVars fBits: 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 fBits = true -> exists iv err vR vF, (* m, currently = M64 *) FloverMap.find (B2Qexpr e) A = Some (iv, err) /\ eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (B2Qexpr e))) vR REAL /\ eval_expr_float e E2 = Some vF /\ eval_expr (toREnv E2) defVars (toRBMap fBits) (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) fBits) = Some M64). { eapply typing_expr_64_bit; eauto. } assert (mF = M64). { eapply typing_agrees_expr; eauto. } subst. edestruct eval_expr_gives_IEEE; eauto. - eapply RealRangeValidator.RangeValidator_sound; eauto. + unfold dVars_range_valid; intros; set_tac. + hnf. intros; set_tac. + hnf; intros. apply H5. set_tac. destruct H7; set_tac. - set_tac. - hnf; intros. apply H5. set_tac. destruct H7; set_tac. - intros. set_tac. - 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 fBits: 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 fBits = true -> exists iv err vR vF m, FloverMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\ bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\ bstep_float f E2 = Some vF /\ bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (toRBMap fBits) (Q2R (B2Q vF)) m /\ (forall vF m, bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (toRBMap fBits) vF m -> (Rabs (vR - vF) <= Q2R err)%R). 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 with (fBits:=fBits); 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) fBits) = Some M64). { eapply typing_cmd_64_bit; eauto. } assert (m = M64). { eapply typing_agrees_cmd; eauto. } subst. assert (ssa (B2Qcmd f) (NatSet.union (freeVars (B2Qcmd f)) (NatSet.empty)) outVars). { eapply ssa_equal_set; eauto. hnf; intros; split; intros; set_tac. destruct H7; try auto. inversion H7. } edestruct bstep_gives_IEEE; eauto. + eapply RealRangeValidator.RangeValidatorCmd_sound; eauto. * hnf; intros; set_tac. * hnf; intros; set_tac. * hnf; intros. apply H4; set_tac. * hnf; intros. apply H5; set_tac. destruct H8; set_tac. * set_tac. + set_tac. + hnf; intros. apply H5. set_tac; destruct H8; set_tac. + intros; set_tac. + destruct H8. exists x, err, vR, x0, M64. repeat split; auto. Qed.