Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qabs Coq.micromega.Psatz
        Coq.QArith.Qreals.
Require Import Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Typing
        Daisy.IntervalValidation Daisy.ErrorValidation Daisy.CertificateChecker
        Daisy.FPRangeValidator Daisy.Environments Daisy.Infra.RealRationalProps
        Daisy.Commands Daisy.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_exp_float (e:exp (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_exp_float e E with
    |Some v1 => Some (b64_opp v1)
    |_ => None
    end
  | Unop Inv e => None
  | Binop b e1 e2 =>
    match eval_exp_float e1 E, eval_exp_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
  | _ => None
  end.

Fixpoint bstep_float f E :option fl64 :=
  match f with
  | Let m x e g => optionLift (eval_exp_float e E)
                             (fun v => bstep_float g (updFlEnv x v E))
                             None
  | Ret e => eval_exp_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_exp_valid (e:exp fl64) E :=
  match e with
  | Var _ x => True (*isValid (eval_exp_float (Var n) E)*)
  | Const m v => True (*isValid (eval_exp_float (Const m v) E)*)
  | Unop u e => eval_exp_valid e E
  | Binop b e1 e2 =>
    (eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\
    (let e1_res := eval_exp_float e1 E in
     let e2_res := eval_exp_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)
  | Downcast m e => eval_exp_valid e E
  end.

Fixpoint bstep_valid f E :=
  match f with
  | Let m x e g => eval_exp_valid e E /\
                    (optionLift (eval_exp_float e E)
                               (fun v_e => bstep_valid g (updFlEnv x v_e E))
                               True)
  | Ret e => eval_exp_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 fexp := 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 (' 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 (' m)); unfold IZR;
      try rewrite P2R_INR; try 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; auto.
    + unfold Z2R, IZR. unfold Qinv; simpl.
      destruct (Z.pow_pos 2 p) eqn:? ; try rewrite P2R_INR; 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.
      * rewrite <- Ropp_mult_distr_l, Ropp_mult_distr_r, Ropp_inv_permute; try lra.
        hnf; intros.  pose proof (pos_INR_nat_of_P p0).
        rewrite H0 in H1; lra.
Qed.

Fixpoint B2Qexp (e: exp fl64) :=
  match e with
  | Var _ x =>  Var Q x
  | Const m v => Const m (B2Q v)
  | Unop u e => Unop u (B2Qexp e)
  | Binop b e1 e2 => Binop b (B2Qexp e1) (B2Qexp e2)
  | Downcast m e => Downcast m (B2Qexp e)
  end.

Fixpoint B2Qcmd (f:cmd fl64) :=
  match f with
  | Let m x e g => Let m x (B2Qexp e) (B2Qcmd g)
  | Ret e => Ret (B2Qexp 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:exp 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
  | 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:exp V) :=
  match e with
  | Var _ x => True
  | Const m e => True
  | Unop u e => noDowncast e
  | Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
  | 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_exp_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) ->
    tMap e  = Some M64.
Proof.
  induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
    simpl in *; try inversion noDowncast_e;
      subst.
  - destruct (tMap (Var Q n)); try congruence.
    rewrite types_valid in *; try set_tac.
    type_conv; subst; auto.
  - destruct (tMap (Const M64 v)) eqn:?; try congruence; type_conv; subst; auto.
  - destruct (tMap (Unop u e)) eqn:?; try congruence.
    erewrite IHe in *; eauto.
    + andb_to_prop typecheck_e; type_conv; subst; auto.
    + destruct (tMap e); try congruence; andb_to_prop typecheck_e; auto.
  - repeat (match goal with
            |H: _ /\ _ |- _=> destruct H
            end).
    destruct (tMap (Binop b e1 e2)) eqn:?; try congruence;
      erewrite IHe1 in *; eauto.
    + erewrite IHe2 in *; eauto.
      * unfold join in typecheck_e.
        rewrite isMorePrecise_refl in typecheck_e; andb_to_prop typecheck_e;
          type_conv; subst; auto.
      * destruct (tMap e2); try congruence.
        andb_to_prop typecheck_e; eauto.
      * intros.
        apply types_valid. set_tac.
    + destruct (tMap e1); destruct (tMap e2); try congruence;
        andb_to_prop typecheck_e; eauto.
    + intros; apply types_valid; set_tac.
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) ->
    tMap (getRetExp f)  = Some M64.
Proof.
  induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
    simpl in *;
    subst; try eauto using typing_exp_64_bit.
  andb_to_prop typecheck_f.
  destruct (tMap e) eqn:?; destruct (tMap (Var Q n)); try congruence.
  andb_to_prop R.
  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_exp e:
  forall E Gamma tMap v m1 m2,
    typeCheck e Gamma tMap = true ->
    eval_exp E Gamma (toRExp e) v m1 ->
    tMap e = Some m2 ->
    m1 = m2.
Proof.
  induction e; intros * typeCheck_e eval_e tMap_e; simpl in *;
    rewrite tMap_e in *;
    inversion eval_e; subst; simpl in *.
  - rewrite H0 in *; type_conv; subst; auto.
  - type_conv; subst; auto.
  - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
    andb_to_prop typeCheck_e.
    eapply IHe; eauto.
    type_conv; subst; auto.
  - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
    andb_to_prop typeCheck_e.
    eapply IHe; eauto.
    type_conv; subst; auto.
  - destruct (tMap e1) eqn:?; try congruence;
      destruct (tMap e2) eqn:?; try congruence.
    andb_to_prop typeCheck_e.
    type_conv; subst.
    assert (m0 = m).
    { eapply IHe1; eauto. }
    assert (m3 = m1).
    { eapply IHe2; eauto. }
    subst; auto.
  - destruct (tMap e) eqn:?; try congruence; type_conv; subst.
    andb_to_prop typeCheck_e.
    type_conv; 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 ->
    tMap (getRetExp f) = Some m2 ->
    m1 = m2.
Proof.
  induction f; intros * typeCheck_f eval_f tMap_f; simpl in *.
  - andb_to_prop typeCheck_f.
    inversion eval_f; subst; simpl in *.
    destruct (tMap e); destruct (tMap (Var Q n)); try congruence.
    andb_to_prop R; type_conv.
    specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2).
    apply IHf; auto.
  - inversion eval_f; subst; eapply typing_agrees_exp; eauto.
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 fexp_corr.
  assert (forall k : Z, (-1022 < k)%Z ->
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
    as exp_valid.
  { intros k k_pos.
    unfold Fcore_FLT.FLT_exp; simpl.
    destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
  pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
                                  (-1022)%Z 53%Z exp_valid)
    as rel_error_exists.
  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. 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; simpl; lra. }
        { vm_compute; congruence. }
      * rewrite zero_v. unfold bpow; simpl. rewrite Rabs_R0. lra.
  - rewrite zero_v.
    pose proof round_0_zero. simpl in H. rewrite H.
    rewrite Rabs_R0.
    unfold bpow. lra.
Qed.

(* (fexp_correct 53 1024 eq_refl) as fexp_corr. *)
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
(*                                     (-1022)%Z 53%Z) *)
Lemma eval_exp_gives_IEEE (e:exp fl64) :
  forall E1 E2 E2_real Gamma tMap vR A P fVars dVars,
    (forall x, (toREnv E2) x = E2_real x) ->
    typeCheck (B2Qexp e) Gamma tMap = true ->
    approxEnv E1 Gamma A fVars dVars E2_real ->
    validIntervalbounds (B2Qexp e) A P dVars = true ->
    validErrorbound (B2Qexp e) tMap A dVars = true ->
    FPRangeValidator (B2Qexp e) A tMap dVars = true ->
    eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) vR M64 ->
    NatSet.Subset ((usedVars (B2Qexp e)) -- dVars) fVars ->
    is64BitEval (B2Qexp e) ->
    noDowncast (B2Qexp e) ->
    eval_exp_valid e E2 ->
    (forall v,
        NatSet.In v fVars ->
        exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
    (forall v, NatSet.In v fVars \/ NatSet.In v dVars -> exists m, Gamma v = Some m) ->
    (forall v,
        NatSet.In v dVars ->
        exists vR,
          E1 v = Some vR /\ Q2R (fst (fst (A (Var Q v)))) <= vR
          <= Q2R (snd (fst (A (Var Q v)))))%R ->
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
        (E2_real v = Some vF /\ tMap (Var Q v) = Some m /\
        validFloatValue vF m)) ->
      (forall v, NatSet.In v (usedVars (B2Qexp e)) -> Gamma v = Some M64) ->
      exists v,
        eval_exp_float e E2 = Some v /\
        eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v)) M64.
  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_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
  repeat match goal with
         | H : _ = true |- _ => andb_to_prop H
         end.
  - 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.
    + destruct (tMap (Unop Neg (B2Qexp e)));
        destruct (tMap (B2Qexp e)); try congruence; andb_to_prop typecheck_e; auto.
    + destruct (A (Unop Neg (B2Qexp e))); andb_to_prop valid_rangebounds; auto.
    + destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
        try congruence; andb_to_prop valid_roundoffs; auto.
    + destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
        try congruence; andb_to_prop valid_float_ranges; auto.
    + assert (is_finite 53 1024 v_e = true).
      { apply validValue_is_finite.
        eapply FPRangeValidator_sound; eauto.
        eapply eval_eq_env; eauto.
        destruct (tMap (Unop Neg (B2Qexp e)));
          destruct (tMap (B2Qexp e)); try congruence; andb_to_prop typecheck_e; auto.
        destruct (A (Unop Neg (B2Qexp e))); try congruence;
          andb_to_prop valid_rangebounds; auto.
        destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
          try congruence. andb_to_prop valid_roundoffs; auto.
        destruct (A (Unop Neg (B2Qexp e))); destruct (tMap (Unop Neg (B2Qexp e)));
          try congruence. andb_to_prop valid_float_ranges; auto. }
      exists (b64_opp v_e); rewrite eval_float_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.
  - destruct (A (Unop Inv (B2Qexp e))); destruct (tMap (Unop Inv (B2Qexp e)));
      try congruence; andb_to_prop valid_roundoffs; congruence.
  - repeat (match goal with
            |H: _ /\ _ |- _ => destruct H
            end).
    destruct (tMap (Binop b (B2Qexp e1) (B2Qexp e2))) eqn:?; try congruence;
      destruct (tMap (B2Qexp e1)) eqn:?; try congruence;
      destruct (tMap (B2Qexp e2)) eqn:?; try congruence.
    andb_to_prop typecheck_e; type_conv; subst.
    assert (tMap (B2Qexp e1) = Some M64 /\
            tMap (B2Qexp e2) = Some M64 /\
            tMap (Binop b (B2Qexp e1) (B2Qexp e2)) = Some M64)
           as [tMap_e1 [tMap_e2 tMap_b]].
    { repeat split; apply (typing_exp_64_bit _ Gamma); simpl; auto.
      - intros; apply usedVars_64bit; set_tac.
      - intros; apply usedVars_64bit; set_tac.
      - rewrite Heqo, Heqo0, Heqo1.
        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. }
    rewrite tMap_e1, tMap_e2, tMap_b in *.
    inversion Heqo; inversion Heqo0; inversion Heqo1; subst.
    assert (m1 = M64).
    { eapply (typing_agrees_exp (B2Qexp e1)); eauto. }
    assert (m2 = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    destruct (A (Binop b (B2Qexp e1) (B2Qexp e2))) eqn:?;
             destruct (A (B2Qexp e1)) eqn:?;
             destruct (A (B2Qexp e2)) eqn:?;
             simpl in *.
    repeat (match goal with
            |H: _ = true |- _ => andb_to_prop H
            end).
    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.
    assert (exists nR2,
               eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e2))) nR2 M0 /\
               Q2R (fst (fst (A (B2Qexp e2)))) <= nR2 <= Q2R (snd (fst (A (B2Qexp e2)))))%R
           as [nR2 [eval_e2_real e2_bounded_real]].
    { eapply validIntervalbounds_sound; eauto.
      - intros; eapply dVars_sound; set_tac.
      - set_tac. hnf in usedVars_sound. apply usedVars_sound.
        set_tac.
      - intros. eapply fVars_defined. rewrite NatSet.mem_spec in *; auto.
      - intros. apply vars_typed. set_tac. rewrite NatSet.union_spec in *; auto. }
    assert (forall vF2 m2,
               eval_exp E2_real Gamma (toRExp (B2Qexp e2)) vF2 m2 ->
               (Rabs (nR2 - vF2) <= Q2R (snd (A (B2Qexp e2)))))%R.
    { eapply validErrorbound_sound; try eauto; try set_tac.
      - intros. eapply dVars_sound; set_tac.
      - intros. eapply fVars_defined. rewrite NatSet.mem_spec in *; auto.
      - intros. apply vars_typed; set_tac. rewrite NatSet.union_spec in *; auto.
      - rewrite Heqp1.
        simpl. instantiate (1:=snd(i1)).
        instantiate (1:=fst(i1)). destruct i1; simpl; auto. }
    assert (contained (Q2R (B2Q v_e2))
                      (widenInterval
                         (Q2R (fst (fst (A (B2Qexp e2)))), Q2R (snd (fst (A (B2Qexp e2)))))
                         (Q2R (snd(A (B2Qexp e2)))))).
    { eapply distance_gives_iv.
      - simpl. eapply e2_bounded_real.
      - eapply H11. instantiate(1:=M64).
        eapply eval_eq_env; eauto. }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
    { intros; subst; simpl in *.
      andb_to_prop R2.
      apply le_neq_bool_to_lt_prop in L4.
      rewrite Heqp1 in *; simpl in *.
      destruct L4; hnf; intros.
      - rewrite H15 in *.
        apply Qlt_Rlt in H14.
        rewrite Q2R0_is_0, Q2R_plus in H14. lra.
      - rewrite H15 in *.
        apply Qlt_Rlt in H14.
        rewrite Q2R0_is_0, Q2R_minus in H14; lra. }
    assert (validFloatValue
              (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
    { eapply (FPRangeValidator_sound (Binop b (B2Qexp e1) (B2Qexp e2)));
        try eauto; set_tac.
      - eapply eval_eq_env; eauto.
        eapply (Binop_dist' (delta:=0)); eauto.
        + rewrite Rabs_R0. apply mTypeToQ_pos_R.
        + unfold perturb; lra.
      - rewrite tMap_b, tMap_e1, tMap_e2.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
      - rewrite Heqp, Heqp0, Heqp1.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
        apply andb_prop_intro; split; auto using Is_true_eq_left.
      - rewrite Heqp, Heqp0, Heqp1.
        rewrite tMap_b.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
      - rewrite tMap_b, Heqp.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
    assert (validFloatValue (Q2R (B2Q v_e1)) M64).
    { eapply (FPRangeValidator_sound (B2Qexp e1)); try eauto; try set_tac.
      eapply eval_eq_env; eauto. }
    assert (validFloatValue (Q2R (B2Q v_e2)) M64).
    { eapply (FPRangeValidator_sound (B2Qexp e2)); try eauto; try set_tac.
      - eapply eval_eq_env; eauto. }
    assert (is_finite 53 1024 v_e1 = true) as finite_e1.
    { apply validValue_is_finite; simpl; auto. }
    assert (is_finite 53 1024 v_e2 = true) as finite_e2.
    { apply validValue_is_finite; simpl; auto. }
    assert (forall eps,
               (Rabs eps <= / 2 * bpow radix2 (- 53 + 1))%R ->
               validFloatValue
                 (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2) * (1 + eps)) M64).
    { intros.
      eapply FPRangeValidator_sound with (e:=Binop b (B2Qexp e1) (B2Qexp e2)); eauto.
      - eapply eval_eq_env; eauto.
        eapply Binop_dist' with (delta:=eps); eauto.
        simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
        eapply Rle_trans; eauto.  unfold Qpower. unfold Qpower_positive.
        assert (pow_pos Qmult (2#1) 53 = 9007199254740992 # 1 )
          by (vm_compute; auto).
        rewrite H19. rewrite Q2R_inv; try lra.
        unfold Q2R, Qnum, Qden. unfold bpow.
        assert (-53 + 1 = -52)%Z by auto.
        rewrite H20.
        assert (Z.pow_pos radix2 52 = 4503599627370496%Z) by (vm_compute; auto).
        rewrite H21. unfold Z2R, P2R. lra.
        unfold perturb.
        repeat rewrite B2Q_B2R_eq; auto.
      - simpl. rewrite tMap_b, tMap_e1, tMap_e2.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
      - simpl; rewrite Heqp, Heqp0, Heqp1.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
      - simpl. rewrite Heqp, Heqp0, Heqp1, tMap_b.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
      - simpl. rewrite Heqp, tMap_b.
        apply Is_true_eq_true.
        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
    assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
    { intros; subst; simpl in *.
      andb_to_prop R2.
      apply le_neq_bool_to_lt_prop in L4.
      rewrite Heqp1 in *; simpl in *.
      destruct L4 as [case_low | case_high]; hnf; intros.
      - rewrite H19 in *.
        apply Qlt_Rlt in case_low.
        rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
      - rewrite H19 in *.
        apply Qlt_Rlt in case_high.
        rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
    clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
    usedVars_sound R2 R1 L1 L R6 L0 R3 L3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
    IHe2.
    pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
    assert (forall k : Z, (-1022 < k)%Z ->
                     (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
      as exp_valid.
    { intros k k_pos.
      unfold Fcore_FLT.FLT_exp; simpl.
      destruct (Z.max_spec_le (k - 53) (-1074)); omega. }
    pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
                                    (-1022)%Z 53%Z exp_valid)
      as rel_error_exists.
    rewrite eval_float_e1, eval_float_e2 in H1.
    unfold optionLift, normal_or_zero in *; simpl in *.
    assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
            (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
    { revert H1; intros case_val. destruct case_val; try auto.
      left; unfold Normal, Denormal in H15; unfold Normal;
        destruct H15 as [normal_b | [denormal_b |zero_b]].
      - repeat rewrite <- B2Q_B2R_eq; try auto.
      - destruct denormal_b.
        assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
        { eapply Rlt_le_trans; eauto.
          repeat rewrite B2Q_B2R_eq; auto. }
        lra.
      - rewrite B2Q_B2R_eq in zero_b; auto.
        rewrite B2Q_B2R_eq in zero_b; auto.
        rewrite zero_b in *.
        rewrite Rabs_R0 in H1.
        unfold minValue, minExponentPos in H1.
        rewrite Q2R_inv in H1; [|vm_compute; congruence].
        unfold Q2R, Qnum, Qden in H1.
        assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
          by (vm_compute; auto).
        rewrite H2 in H1. rewrite <- Z2R_IZR in H1.  unfold IZR in H1.
        simpl in H1. lra. }
    pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
    destruct 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 Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; 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 Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; 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 Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; 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 Q2R, Qnum, Qden. rewrite <- Z2R_IZR.
            simpl; 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. }
  - 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 ->
    (forall v,
        NatSet.In v fVars ->
        exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
    (forall v, NatSet.In v fVars \/ NatSet.In v dVars -> exists m, Gamma v = Some m) ->
    (forall v,
        NatSet.In v dVars ->
        exists vR,
          E1 v = Some vR /\ Q2R (fst (fst (A (Var Q v)))) <= vR
          <= Q2R (snd (fst (A (Var Q v)))))%R ->
      (forall v,
        NatSet.In v dVars ->
        exists vF m,
        (E2_real v = Some vF /\ tMap (Var Q v) = 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
                     fVars_defined vars_typed dVars_sound dVars_valid
                     freeVars_typed;
    inversion bstep_float; inversion bstep_real;
      inversion ssa_f; subst; simpl in *;
        repeat (match goal with
                | H: _ = true |- _ => andb_to_prop H
                end).
  - assert (tMap (B2Qexp e) = Some M64).
    { eapply typing_exp_64_bit; try eauto.
      simpl in *; destruct nodowncast_f; auto.
      destruct is64_eval; auto.
      intros; apply freeVars_typed.
      set_tac. rewrite NatSet.remove_spec.
      split; [ set_tac | ].
      hnf; intros; subst.
      apply H26.
      apply (H25 n H).  }
    assert (m = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    assert (exists v_e, eval_exp_float e E2 = Some v_e /\
                   eval_exp (toREnv E2) Gamma (toRExp (B2Qexp e)) (Q2R (B2Q v_e)) M64)
           as eval_float_e.
    { eapply eval_exp_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. }
    destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
    assert (forall v m, eval_exp E2_real Gamma (toRExp (B2Qexp e)) v m ->
                   Rabs (v0 - v) <= Q2R (snd (A (B2Qexp e))))%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.
      - intros. apply dVars_sound. rewrite <- NatSet.mem_spec; auto.
      - intros. apply fVars_defined. rewrite <- NatSet.mem_spec; auto.
      - intros. apply vars_typed.
        rewrite <- NatSet.union_spec, <- NatSet.mem_spec; auto.
      - instantiate (1:= snd (fst(A (B2Qexp e)))).
        instantiate (1:= fst (fst(A (B2Qexp e)))).
        destruct (A (B2Qexp e)) eqn:?. simpl.
        destruct i; auto. }
    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R( snd (A (B2Qexp e))))%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].
    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; eauto.
      - destruct (tMap (B2Qexp e)); destruct  (tMap (Var Q n)); try congruence;
          andb_to_prop R5; inversion H; subst; auto.
      - eapply approxUpdBound; eauto.
        instantiate (1:= v0).
        rewrite Qeq_bool_iff in R1.
        eapply Rle_trans; eauto.
        apply Qle_Rle. rewrite R1. 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.
      - intros. unfold updEnv. set_tac.
        rewrite NatSet.add_spec in H1. destruct (v1 =? n) eqn:?.
        destruct H1; subst; try congruence.
        + exists v0; split; try auto.
          assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e))) vR M0 /\
                        Q2R (fst (fst (A (B2Qexp e)))) <= vR <= Q2R (snd (fst (A (B2Qexp e)))))%R.
          { eapply validIntervalbounds_sound; eauto.
            - intros. eapply dVars_sound; rewrite NatSet.mem_spec in *; auto.
            - instantiate (1:=fVars).
              hnf; intros; rewrite NatSet.diff_spec in *.
              destruct H1.
              specialize (H25 a H1); rewrite NatSet.union_spec in H25;
                destruct H25; try auto; congruence.
            - intros; apply fVars_defined. rewrite NatSet.mem_spec in *; auto.
            - intros. apply vars_typed.
              rewrite NatSet.mem_spec, NatSet.union_spec in *; auto. }
          destruct H1 as [vR_e [eval_real_e bounded_e]].
          rewrite <- (meps_0_deterministic (toRExp (B2Qexp e)) eval_real_e H17).
          split;
            destruct bounded_e; eapply Rle_trans; eauto;
            apply Qle_Rle.
          apply Qeq_bool_iff in R4; rewrite R4; lra.
          apply Qeq_bool_iff in R3; rewrite R3; lra.
        + rewrite Nat.eqb_eq in Heqb; subst.
          exfalso; apply H26; rewrite NatSet.union_spec; auto.
        + rewrite Nat.eqb_neq in Heqb.
          destruct H1; try congruence.
          apply dVars_sound; auto.
      - 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; rewrite NatSet.mem_spec in *; auto.
      - intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
        + exists M64; auto.
        + apply vars_typed.
          rewrite Nat.eqb_neq in Heqb.
          set_tac.
          rewrite NatSet.union_spec, NatSet.add_spec in H1.
          destruct H1 as [HA |[HB | HC]]; try auto; congruence. }
    unfold optionLift. rewrite eval_float_e.
    assert (tMap (getRetExp (B2Qcmd f)) = Some M64).
    { eapply typingSoundnessCmd; eauto.
      destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
        andb_to_prop R5; type_conv; auto. }
    destruct H1 as [vF_new [m_f bstep_float_new]].
    assert (m_f = M64).
    { eapply typing_agrees_cmd; eauto.
      destruct (tMap (B2Qexp e));
        destruct (tMap (Var Q n)); try congruence; andb_to_prop R5;
          type_conv; subst; auto. }
    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.
    + apply approxUpdBound; auto.
      eapply Rle_trans; eauto.
      rewrite Qeq_bool_iff in R1; apply Qle_Rle; rewrite R1; 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.
    + destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
        andb_to_prop R5; type_conv; 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.
    + 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.
    + intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
      * exists M64; auto.
      * apply vars_typed.
        rewrite Nat.eqb_neq in Heqb.
        set_tac.
        destruct H1 as [HA |HB]; try auto.
        rewrite NatSet.add_spec in HB. destruct HB; try auto; congruence.
    + intros. unfold updEnv. set_tac.
      rewrite NatSet.add_spec in H1.
      destruct (v1 =? n) eqn:?;
      destruct H1; subst; try congruence.
      * exists v0; split; try auto.
        assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e))) vR M0 /\
                      Q2R (fst (fst (A (B2Qexp e)))) <= vR <= Q2R (snd (fst (A (B2Qexp e)))))%R.
        { eapply validIntervalbounds_sound; eauto.
            - intros. eapply dVars_sound; rewrite NatSet.mem_spec in *; auto.
            - instantiate (1:=fVars).
              hnf; intros; rewrite NatSet.diff_spec in *.
              destruct H1.
              specialize (H25 a H1); rewrite NatSet.union_spec in H25;
                destruct H25; try auto; congruence.
            - intros; apply fVars_defined. rewrite NatSet.mem_spec in *; auto.
            - intros. apply vars_typed.
              rewrite NatSet.mem_spec, NatSet.union_spec in *; auto. }
        destruct H1 as [vR_e [eval_real_e bounded_e]].
        rewrite <- (meps_0_deterministic (toRExp (B2Qexp e)) eval_real_e H17).
        rewrite Nat.eqb_eq in Heqb; subst.
        split;
            destruct bounded_e; eapply Rle_trans; eauto;
            apply Qle_Rle.
        apply Qeq_bool_iff in R4; rewrite R4; lra.
        apply Qeq_bool_iff in R3; rewrite R3; lra.
      * rewrite Nat.eqb_eq in Heqb; subst.
        exfalso; apply H26; rewrite NatSet.union_spec; auto.
      * rewrite Nat.eqb_neq in Heqb.
        congruence.
      * rewrite Nat.eqb_neq in Heqb.
        apply dVars_sound; auto.
    + intros. rewrite NatSet.add_spec in H1; unfold updEnv.
      destruct (v1 =? n) eqn:?; destruct H1; subst; try congruence.
      * destruct (tMap (Var Q n)) eqn:?; exists (Q2R (B2Q v_e)).
        exists m; repeat split; try auto.
        eapply FPRangeValidator_sound; eauto.
        { eapply eval_eq_env; eauto.
          rewrite H in *; andb_to_prop R5;
            type_conv; subst; auto. }
        { set_tac. split; try auto.
          rewrite NatSet.remove_spec, NatSet.union_spec.
          split; try auto.
          hnf; intros; subst. apply H26. apply H25; auto. }
        { rewrite H in *; congruence. }
      * rewrite Nat.eqb_eq in Heqb; subst.
        exists (Q2R (B2Q v_e)); rewrite H in *.
        destruct (tMap (Var Q n)) eqn:?; try congruence;
          andb_to_prop R5; type_conv; subst.
        exists M64; repeat split; try auto.
        eapply FPRangeValidator_sound; eauto.
        { eapply eval_eq_env; eauto. }
        { set_tac. split; try auto.
          rewrite NatSet.remove_spec, NatSet.union_spec.
          split; try auto.
          hnf; intros; subst. apply H26. apply H25; auto. }
      * 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.
      rewrite NatSet.remove_spec, NatSet.union_spec; 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_exp_gives_IEEE); eauto.
    exists x; destruct H.
    split; try auto. apply ret_b; auto.
Qed.

Theorem IEEE_connection_exp e A P E1 E2 defVars:
  approxEnv E1 defVars A (usedVars (B2Qexp e)) (NatSet.empty) (toREnv E2) ->
  is64BitEval (B2Qexp e) ->
  noDowncast (B2Qexp e) ->
  eval_exp_valid e E2 ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      defVars v = Some M64) ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      exists vR,
        (E1 v = Some vR) /\
        Q2R (fst (P v)) <= vR <= Q2R(snd (P v)))%R ->
  (forall v,
      NatSet.In v (usedVars (B2Qexp e)) ->
      exists m, defVars v = Some m) ->
  CertificateChecker (B2Qexp e) A P defVars = true ->
  exists vR vF, (* m, currently = M64 *)
    eval_exp E1 (toRMap defVars) (toREval (toRExp (B2Qexp e))) vR M0 /\
    eval_exp_float e E2 = Some vF /\
    eval_exp (toREnv E2) defVars (toRExp (B2Qexp e)) (Q2R (B2Q vF)) M64 /\
    (Rabs (vR - Q2R (B2Q vF )) <= Q2R (snd (A (B2Qexp e))))%R.
Proof.
  intros.
  edestruct Certificate_checking_is_sound; eauto.
  - intros. set_tac.
  - intros. set_tac.
  - destruct H7 as [vF [mF [eval_real [eval_float roundoff_sound]]]].
    unfold CertificateChecker in H6.
    andb_to_prop H6.
    assert (typeMap defVars (B2Qexp e) (B2Qexp e) = Some M64).
    { eapply typing_exp_64_bit; eauto. }
    assert (mF = M64).
    { eapply typing_agrees_exp; eauto. }
    subst.
    edestruct eval_exp_gives_IEEE; eauto.
    + set_tac.
    + intros. apply H5. destruct H7; try auto.
      inversion H7.
    + intros. inversion H7.
    + intros. inversion H7.
    + destruct H7 as [eval_float_f eval_rel].
      exists x; exists x0. repeat split; try auto.
      eapply roundoff_sound; eauto.
Qed.

Theorem IEEE_connection_cmd (f:cmd fl64) (absenv:analysisResult) P
        defVars E1 E2:
    approxEnv E1 defVars absenv (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) absenv P defVars = true ->
    exists vR vF m,
    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 (snd (absenv (getRetExp (B2Qcmd f)))))%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.
  - unfold CertificateCheckerCmd.
    apply Is_true_eq_true.
    repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
  - destruct H6 as [vF [m [bstep_real [bstep_float roundoff_sound]]]].

    assert (typeMapCmd defVars (B2Qcmd f) (getRetExp (B2Qcmd f)) = Some M64).
    { eapply typing_cmd_64_bit; eauto.  }
    assert (m = M64).
    { eapply typing_agrees_cmd; eauto. }
    subst.
    edestruct bstep_gives_IEEE; eauto.
    + eapply ssa_equal_set; eauto.
      hnf; intros; split; intros; set_tac.
      rewrite NatSet.union_spec in H7; destruct H7; try auto.
      inversion H7.
    + set_tac.
    + intros. apply H4; rewrite NatSet.mem_spec; auto.
    + intros. apply H5. set_tac. destruct H7; try auto.
      inversion H7.
    + intros. inversion H7.
    + intros * HA; inversion HA.
    + exists x; exists x0; exists M64.
      destruct H7 as [bstep_float2 bstep_rel].
      repeat split; auto.
Qed.