open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics
     CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
     TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
     CommandsTheory ssaPrgsTheory EnvironmentsTheory FloverMapTheory
open preamble

val _ = new_theory "IEEE_connection";

val _ = temp_overload_on("abs",``real$abs``);

(** FloVer assumes rounding with ties to even, thus we explicitly define
    a rounding mode here **)
val dmode_def = Define `dmode = roundTiesToEven`;

val optionLift_def = Define `
  (optionLift (SOME v) some_cont none_cont = some_cont v) /\
  (optionLift (NONE) some_cont none_cont = none_cont)`;

val updFlEnv_def = Define `
  updFlEnv x v E = \ y. if y = x then SOME v else E y`;

val eval_exp_float_def = Define `
  (eval_exp_float (Var n) E = E n) /\
  (eval_exp_float (Const m v) E = SOME v) /\
  (eval_exp_float (Unop Neg e) E =
    case eval_exp_float e E of
      | SOME v =>  SOME (fp64_negate v)
      | _ => NONE) /\
  (eval_exp_float (Unop Inv e) E = NONE) /\
  (eval_exp_float (Binop b e1 e2) E =
    (case (eval_exp_float e1 E), (eval_exp_float e2 E) of
       | SOME v1, SOME v2 =>
             (case b of
                | Plus => SOME (fp64_add dmode v1 v2)
                | Sub => SOME (fp64_sub dmode v1 v2)
                | Mult => SOME (fp64_mul dmode v1 v2)
                | Div => SOME (fp64_div dmode v1 v2))
       | _, _ => NONE)) /\
  (eval_exp_float (Fma e1 e2 e3) E =
    (case (eval_exp_float e1 E), (eval_exp_float e2 E), (eval_exp_float e2 E) of
       | _, _, _ => NONE)) /\
  (eval_exp_float (Downcast m e) E = NONE)`;

val bstep_float_def = Define `
  (bstep_float (Let m x e g) E :word64 option=
     optionLift (eval_exp_float e E)
       (\ v. bstep_float g (updFlEnv x v E))
       NONE) /\
  (bstep_float (Ret e) E = eval_exp_float e E)`;

val normal_or_zero_def = Define `
  normal_or_zero (v:real) =
    (minValue_pos M64 <= abs v \/ v = 0)`;

val isValid_def = Define `
  isValid e =
    let trans_e = optionLift e (\ v. SOME (float_to_real (fp64_to_float v))) NONE in
        optionLift trans_e normal_or_zero F`;

val eval_exp_valid_def = Define `
  (eval_exp_valid (Var n) E = T) /\
  (eval_exp_valid (Const m v) E = T) /\
  (eval_exp_valid (Unop u e) E = eval_exp_valid e E) /\
  (eval_exp_valid (Binop b e1 e2) E =
    (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)
        (\ v1. let v1_real = float_to_real (fp64_to_float v1)
               in
                 optionLift e2_res
                            (\ v2.
                               let v2_real = float_to_real (fp64_to_float v2)
                               in
                                 normal_or_zero (evalBinop b v1_real v2_real))
                            T)
        T)) /\
  (eval_exp_valid (Fma e1 e2 e3) E =
    (eval_exp_valid e1 E /\ eval_exp_valid e2 E /\ eval_exp_valid e3 E /\
       let e1_res = eval_exp_float e1 E in
       let e2_res = eval_exp_float e2 E in
       let e3_res = eval_exp_float e3 E in
       optionLift (e1_res)
        (\ v1. let v1_real = float_to_real (fp64_to_float v1)
               in
                 optionLift e2_res
                            (\ v2.
                               let v2_real = float_to_real (fp64_to_float v2)
                               in
                                   optionLift e3_res
                                              (\ v3. let v3_real = float_to_real (fp64_to_float v3) in
                                                         F)
                                              T)
                            T)
        T)) /\
  (eval_exp_valid (Downcast m e) E = eval_exp_valid e E)`;

val bstep_valid_def = Define `
  (bstep_valid (Let m x e g) E =
   (eval_exp_valid e E /\
      optionLift (eval_exp_float e E)
        (\v_e. bstep_valid g (updFlEnv x v_e E))
        T)) /\
  (bstep_valid (Ret e) E = eval_exp_valid e E)`;

val toRExp_def = Define `
  (toRExp ((Var v):word64 exp) = Var v) /\
  (toRExp (Const m c) = Const m (float_to_real (fp64_to_float c))) /\
  (toRExp (Unop u e1) = Unop u (toRExp e1)) /\
  (toRExp (Binop b e1 e2) = Binop b (toRExp e1) (toRExp e2)) /\
  (toRExp (Fma e1 e2 e3) = Fma (toRExp e1) (toRExp e2) (toRExp e3)) /\
  (toRExp (Downcast m e1) = Downcast m (toRExp e1))`;

val toRCmd_def = Define `
  (toRCmd (Let m x e g) = Let m x (toRExp e) (toRCmd g)) /\
  (toRCmd (Ret e) = Ret (toRExp e))`;

val toREnv_def = Define `
  toREnv (E:num -> word64 option) (x:num):real option =
    case E x of
      | NONE => NONE
      | SOME v => SOME (float_to_real (fp64_to_float v))`;

val toWordEnv_def = Define `
  toWordEnv E = \x. case E x of
                      | SOME v => SOME (float_to_fp64 (real_to_float dmode v))
                      | NONE => NONE`;

val Binop_to_Rop_def = Define `
  Binop_to_Rop (b:binop) :real->real->real =
    case b of
      | Plus => $+
      | Sub => $-
      | Mult => $*
      | Div => $/ `;

val threshold_64_bit_lt_maxValue = store_thm ("threshold_64_bit_lt_maxValue",
  ``maxValue M64 < threshold (:52 # 11)``,
  fs[threshold_def, maxValue_def, maxExponent_def]
  \\ once_rewrite_tac [GSYM REAL_MUL_RID]
  \\ once_rewrite_tac [GSYM REAL_MUL_ASSOC]
  \\ irule REAL_LT_LMUL_IMP
  \\ fs[]
  \\ once_rewrite_tac [real_sub]
  \\ once_rewrite_tac [GSYM REAL_LT_ADDNEG2]
  \\ once_rewrite_tac [REAL_NEGNEG]
  \\ once_rewrite_tac [RealArith.REAL_ARITH ``2:real = 1+1``]
  \\ irule REAL_LT_IADD
  \\ once_rewrite_tac [GSYM REAL_INV1]
  \\ irule REAL_LT_INV \\ fs[]);

val normalValue_implies_normalization = store_thm ("validFloatValue_implies_normalization",
  ``!v.
      normal v M64 ==>
      normalizes (:52 #11) v``,
  rpt strip_tac
  \\ fs[normal_def, normalizes_def, wordsTheory.INT_MAX_def, minValue_pos_def,
        minExponentPos_def, wordsTheory.INT_MIN_def, wordsTheory.dimindex_11,
        wordsTheory.UINT_MAX_def, wordsTheory.dimword_11]
  \\ irule REAL_LET_TRANS
  \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]);

val normalValue_implies_finiteness = store_thm ("normalValue_implies_finiteness",
  ``!v.
      normal v M64 ==>
      float_is_finite ((real_to_float dmode v):(52 , 11) float)``,
  rpt strip_tac
  \\ fs [real_to_float_def, normal_def, dmode_def]
  \\ irule float_round_finite
  \\ irule REAL_LET_TRANS
  \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]);

val denormalValue_implies_finiteness = store_thm ("normalValue_implies_finiteness",
  ``!v.
      denormal v M64 ==>
      float_is_finite ((real_to_float dmode v):(52 , 11) float)``,
  rpt strip_tac
  \\ fs [real_to_float_def, denormal_def, dmode_def]
  \\ irule float_round_finite
  \\ irule REAL_LT_TRANS
  \\ qexists_tac `minValue_pos M64` \\ fs[]
  \\ irule REAL_LET_TRANS \\ qexists_tac `maxValue M64`
  \\ `minValue_pos M64 <= 1`
        by (once_rewrite_tac [GSYM REAL_INV1]
            \\ fs[minValue_pos_def, minExponentPos_def]
            \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
  \\ fs[threshold_64_bit_lt_maxValue]
  \\ irule REAL_LE_TRANS \\ qexists_tac `1`
  \\ fs[maxValue_def, maxExponent_def]);

val normal_value_is_float_value = store_thm (
  "normal_value_is_float_value",
  ``!ff.
      normal (float_to_real ((ff):(52,11) float)) M64 ==>
      float_value ff = Float (float_to_real ff)``,
  rpt strip_tac
  \\rewrite_tac[float_value_def]
  \\rw_thm_asm `normal _ _` normal_def
  \\fs[float_to_real_def]
  \\ every_case_tac \\ fs[maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def]
   >-( Cases_on `ff.Sign` \\ fs[]
  \\ Cases_on `n` \\ fs[]
  \\ Cases_on `n'` \\ fs[])
  >- (Cases_on `ff.Sign` \\ fs[]
      \\ Cases_on `n` \\ fs[]
      \\ TRY (Cases_on `n'` \\ fs[])
      \\ Cases_on `ff.Significand` \\ fs[]
      \\ Cases_on `n` \\ fs[]
      \\ qpat_x_assum `abs _ <= _` MP_TAC
      \\ qmatch_abbrev_tac `abs (cst1 * cst2) <= cst3 ==> _`
      \\ strip_tac
      >- (`abs (cst1 * cst2) = cst1 * cst2`
             by (once_rewrite_tac[ABS_REFL]
                 \\ irule REAL_LE_MUL
                 \\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
                 \\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
                 \\ fs[]
                 \\ irule REAL_LE_ADD \\ fs[]
                 \\ irule REAL_LE_MUL \\ fs[]
                 \\ once_rewrite_tac [REAL_INV_1OVER] \\ fs[])
          \\ rw_asm_star `abs _ = _`
          \\ `cst1 <= cst3` suffices_by (unabbrev_all_tac \\ fs[])
          \\ irule REAL_LE_TRANS
          \\ qexists_tac `cst1 * cst2` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``cst1:real = cst1 * 1``]
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``cst1 * cst2 * 1 = cst1 * cst2:real``]
          \\ irule REAL_LE_LMUL_IMP
          \\ unabbrev_all_tac \\ fs[]
          \\ once_rewrite_tac [REAL_LE_ADDR]
          \\ once_rewrite_tac [real_div]
          \\ irule REAL_LE_MUL \\ fs[]
          \\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[])
     \\ `abs (cst1 * cst2) = -(cst1 * cst2)`
             by (once_rewrite_tac[abs]
                 \\ `~ (0 <= cst1 * cst2)` suffices_by (fs[] )
                 \\ unabbrev_all_tac
                 \\ once_rewrite_tac [REAL_MUL_LNEG]
                 \\ fs[]
                 \\ qmatch_abbrev_tac `~ (cst1 * cst2 <= 0:real)`
                 \\ once_rewrite_tac [REAL_NOT_LE]
                 \\ irule REAL_LT_MUL
                 \\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
                 \\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
                 \\ irule REAL_LT_ADD \\ fs[]
                 \\ irule REAL_LT_MUL \\ fs[]
                 \\ once_rewrite_tac [REAL_INV_1OVER] \\ fs[])
          \\ rw_asm_star `abs _ = _`
          \\ `- cst1 <= cst3` suffices_by (unabbrev_all_tac \\ fs[])
          \\ irule REAL_LE_TRANS
          \\ qexists_tac `- (cst1 * cst2)` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``-cst1:real = -cst1 * 1``]
          \\ once_rewrite_tac [RealArith.REAL_ARITH ``- (cst1 * cst2) * 1 = - cst1 * cst2:real``]
          \\ irule REAL_LE_LMUL_IMP
          \\ unabbrev_all_tac \\ fs[]
          \\ once_rewrite_tac [REAL_LE_ADDR]
          \\ once_rewrite_tac [real_div]
          \\ irule REAL_LE_MUL \\ fs[]
          \\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[]));

val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
  ``!ff:(52,11) float.
      denormal (float_to_real ff) M64 ==>
      float_value ff = Float (float_to_real ff)``,
  rpt strip_tac
  \\rewrite_tac[float_value_def]
  \\rw_thm_asm `denormal _ _` denormal_def
  \\ TOP_CASE_TAC
  \\ fs[]
  \\ rw_thm_asm `abs _ < _` float_to_real_def
  \\ fs[]
  \\ `ff.Exponent <> 0w` by fs[]
  \\ fs[]
  \\ Cases_on `ff` \\ fs[]
  \\ `w2n (-1w:word11) = 2047`  by EVAL_TAC
  \\ `w2n c0 = 2047` by fs[]
  \\ fs[]
  \\ TOP_CASE_TAC \\ fs[minValue_pos_def, minExponentPos_def]
  \\ fs[REAL_ABS_MUL, POW_M1]
  >- (`44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <=  inv 1`
        by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
      \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
    by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
  \\ fs[REAL_INV1])
  >- (Cases_on `c1` \\ fs[]
      \\ `1 < abs (1 + &n / 4503599627370496)`
        by (fs[abs]
            \\ `0:real <= 1 + &n / 4503599627370496`
                by (irule REAL_LE_TRANS
                    \\ qexists_tac `1` \\ fs[]
                    \\ once_rewrite_tac [GSYM REAL_ADD_RID]
                    \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
                    \\ irule REAL_LE_LADD_IMP
                    \\ fs[REAL_ADD_RID, real_div]
                    \\ irule REAL_LE_MUL \\ fs[]
                    \\ irule REAL_LE_INV \\ fs[])
                \\ fs[]
                \\ once_rewrite_tac [GSYM REAL_ADD_RID]
                \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
                \\ irule REAL_LT_IADD
                \\ fs[REAL_ADD_RID, real_div]
                \\ irule REAL_LT_MUL \\ fs[]
                \\ irule REAL_INV_POS \\ fs[])
              \\ `44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <=  inv 1`
                by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
               \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
    by (irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ fs[]
        \\ qmatch_goalsub_abbrev_tac `cst1 < cst2`
        \\ irule REAL_LT_TRANS \\ qexists_tac `cst1 * abs (1 + &n / 4503599627370496)`
        \\ fs[]
        \\ once_rewrite_tac [GSYM REAL_MUL_RID]
        \\ once_rewrite_tac [GSYM REAL_MUL_ASSOC] \\ irule REAL_LT_LMUL_IMP
        \\ fs[]
        \\ unabbrev_all_tac \\ fs[])
  \\ fs[REAL_INV1]));

val validValue_gives_float_value = store_thm ("validValue_gives_float_value",
  ``!ff:(52,11) float.
      validFloatValue (float_to_real ff) M64 ==>
      float_value ff = Float (float_to_real ff)``,
  rpt strip_tac \\ fs[validFloatValue_def]
  >- (irule normal_value_is_float_value \\ fs[])
  >- (irule denormal_value_is_float_value \\ fs[])
  \\ fs[GSYM float_is_zero_to_real, float_is_zero_def]
  \\ every_case_tac \\ fs[]);

val normalTranslatedValue_implies_finiteness = store_thm ("normalTranslatedValue_implies_finiteness",
  ``!ff:double.
      normal (float_to_real ff) M64 ==>
      float_is_finite ff``,
  rpt strip_tac
  \\ fs[float_is_finite_def]
  \\ qspec_then `ff` impl_subgoal_tac normal_value_is_float_value
  \\ fs[]);

val denormalTranslatedValue_implies_finiteness = store_thm (
  "denormalTranslatedValue_implies_finiteness",
  ``!ff:double.
       denormal (float_to_real ff) M64 ==>
       float_is_finite ff``,
  rpt strip_tac
  \\ fs[float_is_finite_def]
  \\ qspec_then `ff` impl_subgoal_tac denormal_value_is_float_value
  \\ fs[]);

val zero_value_implies_finiteness = store_thm ("zero_value_implies_finiteness",
  ``!v. v= 0 ==> float_is_finite ((real_to_float dmode v))``,
  rpt strip_tac \\ rveq
  \\ fs[real_to_float_def, dmode_def]
  \\ irule float_round_finite
  \\ fs[threshold_is_positive]
);

(* val validFPRanges_implies_finiteness = store_thm ("validFPRanges_gives_finiteness", *)
(*   ``!v. *)
(*       validFloatValue v M64 ==> *)
(*       fp64_isFinite (float_to_fp64 (real_to_float dmode v))``, *)
(*   rpt strip_tac *)
(*   \\ fs[validFloatValue_def, fp64_isFinite_def, fp64_to_float_float_to_fp64, *)
(*         zero_value_implies_finiteness, normalValue_implies_finiteness]); *)

val finite_float_implies_threshold = Q.prove (
  `!f:(α , β) float.
      float_is_finite f ==>
      ~(float_to_real f ≤ -threshold (:α # β)) /\
      ~(float_to_real f ≥ threshold (:α # β)) `,
  rpt strip_tac
  \\ drule lift_ieeeTheory.float_to_real_threshold
  \\ simp[realTheory.abs]
  \\ every_case_tac
  \\ strip_tac \\ RealArith.REAL_ASM_ARITH_TAC);

val round_float_to_real_id = Q.prove(
  `!f.
     float_is_finite f /\
     float_is_normal f /\
     ~ float_is_zero f ==>
     round roundTiesToEven (float_to_real f) = f`,
  rw[]
  \\ qpat_assum `float_is_finite _` mp_tac
  \\ qpat_assum `float_is_normal _` mp_tac
  \\ rewrite_tac [float_is_finite_def, float_is_normal_def]
  \\ rewrite_tac [float_value_def]
  \\ simp[]
  \\ strip_tac
  \\ once_rewrite_tac [round_def]
  \\ fs[finite_float_implies_threshold]
  \\ once_rewrite_tac [closest_such_def]
  \\ SELECT_ELIM_TAC
  \\ rw[]
  >- (qexists_tac `f`
      \\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS]
      \\ Cases_on `f = b` \\ fs[]
      \\ first_x_assum (qspec_then `f` mp_tac)
      \\ fs[realTheory.REAL_SUB_REFL]
      \\ strip_tac
      \\ fs[float_to_real_eq]
      \\ rfs[])
  \\ CCONTR_TAC
  \\ fs[is_closest_def, IN_DEF]
  \\ qpat_x_assum `!x._ ` mp_tac
  \\ first_x_assum (qspec_then `f` mp_tac)
  \\ fs[realTheory.REAL_SUB_REFL]
  \\ rpt strip_tac
  \\ fs[float_to_real_eq]
  \\ rfs[]);

val real_to_float_id = Q.store_thm ("real_to_float_id",
  `!f.
     float_is_finite f /\
     float_is_normal f /\
     ~ float_is_zero f ==>
     real_to_float dmode (float_to_real f) = f`,
rpt strip_tac
\\ fs[dmode_def, real_to_float_def, float_round_def, round_float_to_real_id]);

val real_to_float_float_id = Q.prove (
  `!f.
     fp64_isFinite f /\
     fp64_isNormal f /\
     ~ fp64_isZero f ==>
     float_to_fp64 (real_to_float dmode (float_to_real (fp64_to_float f))) = f`,
rpt strip_tac
\\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
\\ fs[real_to_float_id]
\\ fs[float_to_fp64_fp64_to_float]);

val float_to_real_real_to_float_zero_id = store_thm ("float_to_real_real_to_float_zero_id",
  ``float_to_real (real_to_float roundTiesToEven 0) = 0``,
  once_rewrite_tac[real_to_float_def]
  \\ `float_round roundTiesToEven F 0 = (float_plus_zero(:α#β))`
       by  (irule round_roundTiesToEven_is_plus_zero
            \\ fs[ulp_def, ULP_def])
  \\ fs[float_to_real_def, float_plus_zero_def]);

val div_eq0_general = store_thm ("div_eq0_general",
  ``!a b:real. b <> 0 ==> (a / b = 0 <=> a = 0)``,
  rpt strip_tac \\ Cases_on `0 < b` \\ fs[div_eq0]
  \\ `0 < -b` by RealArith.REAL_ASM_ARITH_TAC
  \\ `a/ -b = 0 <=> a = 0` by fs[div_eq0]
  \\ fs[real_div]
  \\ Cases_on `a = 0` \\ fs[]
  \\ Cases_on `inv b = 0` \\ fs[REAL_INV_NZ]);

val float_to_real_round_zero_is_zero = store_thm (
  "float_to_real_round_zero_is_zero",
  ``!ff P.
      2 * abs ff <=  ulp ((:α#β) :(α#β) itself) ==>
      float_to_real ((float_round roundTiesToEven P ff):(α, β) float) = 0``,
  rpt strip_tac \\ Cases_on `P`
  \\ fs [round_roundTiesToEven_is_plus_zero,
         round_roundTiesToEven_is_minus_zero, zero_to_real]);

val noDowncast_def = Define `
  (noDowncast (Var v) = T) /\
  (noDowncast (Const _ _) = T) /\
  (noDowncast (Unop _ e) = noDowncast e) /\
  (noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
  (noDowncast (Fma e1 e2 e3) = (noDowncast e1 /\ noDowncast e2 /\ noDowncast e3)) /\
  (noDowncast (Downcast _ _) = F)`;

val noDowncastFun_def = Define `
  (noDowncastFun (Let m x e g) = (noDowncast e /\ noDowncastFun g)) /\
  (noDowncastFun (Ret e) = noDowncast e)`;

(* val noDenormalCst_def = Define ` *)
(*   (noDenormalCst (Const m v) = ~ denormal (float_to_real (fp64_to_float v)) m) /\ *)
(*   (noDenormalCst (Var v) = T) /\ *)
(*   (noDenormalCst (Unop _ e) = noDenormalCst e) /\ *)
(*   (noDenormalCst (Binop _ e1 e2) = (noDenormalCst e1 /\ noDenormalCst e2)) /\ *)
(*   (noDenormalCst (Downcast _ e) = noDenormalCst e)`; *)

val is64BitEval_def = Define `
  (is64BitEval ((Const m c):real exp) = (m = M64)) /\
  (is64BitEval (Unop _ e) = is64BitEval e) /\
  (is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\
  (is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\
  (is64BitEval (Downcast m e) = is64BitEval e) /\
  (is64BitEval ((Var v):real exp) = T)`;

val is64BitBstep_def = Define `
  (is64BitBstep (Let m x e g) = ((m = M64) /\ is64BitEval e /\ is64BitBstep g)) /\
  (is64BitBstep (Ret e) = is64BitEval e)`;

(* val typeMap_eq_typeExp = Q.prove(` *)
(*   !e. *)
(*     FloverMapTree_find e (typeMap Gamma e (FloverMapTree_empty)) *)
(*     = typeExpression Gamma e`, *)
(*   Induct  *)
(*   \\ fs[Once typeMap_def] \\ rpt strip_tac *)
(*   \\ fs[FloverMapTree_empty_def, Once typeExpression_def] *)
(*   \\ rpt strip_tac  *)
(*   \\ Flover_compute ``typeExpression_def`` fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] ); *)

val typing_exp_64bit = store_thm("typing_exp_64bit",
  ``!e Gamma tMap.
      noDowncast e /\ is64BitEval e /\
      typeCheck e Gamma tMap /\
      (!v. v IN domain(usedVars e) ==> Gamma v = SOME M64) ==>
       FloverMapTree_find e tMap = SOME M64``,
  Induct
  \\ rpt strip_tac \\ Flover_compute ``typeCheck`` \\ fs[noDowncast_def]
  >- (fs[usedVars_def])
  >- (fs[]  \\ rveq \\ fs[is64BitEval_def])
  >- (fs[]
      \\ `FloverMapTree_find e tMap = SOME M64`
            by (first_x_assum irule
                >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
                \\ qexists_tac `Gamma`
                \\ rpt strip_tac
                >- (first_x_assum irule \\ simp[Once usedVars_def])
                \\ fs[])
      \\ fs[])
  >- (rename1 `Binop b e1 e2`
      \\ fs[]
      \\ `FloverMapTree_find e2 tMap = SOME M64`
            by (first_x_assum irule
                >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
                \\ qexists_tac `Gamma` \\ rpt strip_tac
                >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
                \\ fs[])
      \\ `FloverMapTree_find e1 tMap = SOME M64`
            by (first_x_assum irule
                >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
                \\ qexists_tac `Gamma` \\ rpt strip_tac
                >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
                \\ fs[])
      \\ fs[join_def])
  \\ rename1 `Fma e1 e2 e3`
  \\ fs[]
  \\ `FloverMapTree_find e3 tMap = SOME M64`
        by (first_x_assum irule
            >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
            \\ qexists_tac `Gamma` \\ rpt strip_tac
            >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
            \\ fs[])
  \\ `FloverMapTree_find e2 tMap = SOME M64`
        by (first_x_assum irule
            >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
            \\ qexists_tac `Gamma` \\ rpt strip_tac
            >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
            \\ fs[])
  \\ `FloverMapTree_find e1 tMap = SOME M64`
        by (first_x_assum irule
            >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
            \\ qexists_tac `Gamma` \\ rpt strip_tac
            >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
            \\ fs[])
  \\ fs[join3_def, join_def]);

val typing_cmd_64bit = store_thm (
  "typing_cmd_64bit",
  ``!f Gamma tMap.
       noDowncastFun f /\
       is64BitBstep f /\
       typeCheckCmd f Gamma tMap /\
       (!v. v IN domain (freeVars f) ==> Gamma v = SOME M64) ==>
       FloverMapTree_find (getRetExp f) tMap = SOME M64``,
  Induct \\ rpt strip_tac
  \\ Flover_compute ``typeCheckCmd``
  \\ fs[]
  >- (rveq \\ once_rewrite_tac [getRetExp_def]
      \\ fs[]
      \\ first_x_assum irule
      \\ fs[Once is64BitBstep_def, Once noDowncastFun_def]
      \\ qexists_tac `updDefVars n m Gamma`
      \\ fs[]
      \\ rpt strip_tac
      \\ fs[updDefVars_def] \\ IF_CASES_TAC \\ fs[]
      \\ first_x_assum irule
      \\ simp[Once freeVars_def, domain_union])
  \\ fs [getRetExp_def, freeVars_def]
  \\ irule typing_exp_64bit
  \\ fs[Once is64BitBstep_def, Once noDowncastFun_def]
  \\ asm_exists_tac \\ fs[]);

val typing_agrees_exp = store_thm (
  "typing_agrees_exp",
  ``!e E Gamma tMap v m1 m2 .
      typeCheck e Gamma tMap /\
      eval_exp E Gamma e v m1 /\
      FloverMapTree_find e tMap = SOME m2 ==>
      m1 = m2``,
  rpt strip_tac
  \\ drule  typingSoundnessExp
  \\ disch_then drule
  \\ disch_then assume_tac
  \\ fs[FloverMapTree_find_injective]);

val typing_agrees_cmd = store_thm (
  "typing_agrees_cmd",
  ``!f E Gamma v m1 m2 tMap.
       typeCheckCmd f Gamma tMap /\
       bstep f E Gamma v m1 /\
       FloverMapTree_find (getRetExp f) tMap = SOME m2 ==>
       m1 = m2``,
  rpt strip_tac
  \\ drule typingSoundnessCmd
  \\ disch_then drule
  \\ disch_then assume_tac
  \\ fs[FloverMapTree_find_injective]);

val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE",
  ``!(e:word64 exp) E1 E2 E2_real Gamma tMap vR A P fVars dVars .
      (!x. (toREnv E2) x = E2_real x) /\
      typeCheck (toRExp e) Gamma tMap /\
      approxEnv E1 Gamma A fVars dVars E2_real /\
      validIntervalbounds (toRExp e) A P dVars /\
      validErrorbound (toRExp e) tMap A dVars /\
      FPRangeValidator (toRExp e) A tMap dVars /\
      eval_exp (toREnv E2) Gamma (toRExp e) vR M64 /\
      domain (usedVars (toRExp e)) DIFF domain dVars ⊆ domain fVars ∧
      is64BitEval (toRExp e) /\
      noDowncast (toRExp e) /\
      eval_exp_valid e E2 /\
      dVars_range_valid dVars E1 A /\
      fVars_P_sound fVars E1 P /\
      vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
      (∀v.
        v ∈ domain dVars ⇒
        ∃vF m.
        (E2_real v = SOME vF ∧ FloverMapTree_find (Var v) tMap = SOME m ∧
        validFloatValue vF m)) /\
      (!v. v IN domain (usedVars (toRExp e)) ==> Gamma v = SOME M64) ==>
      ?v.
        eval_exp_float e E2 = SOME v /\
        eval_exp (toREnv E2) Gamma (toRExp e) (float_to_real (fp64_to_float v)) M64``,
  Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
  \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
  \\ once_rewrite_tac [eval_exp_float_def]
  \\ fs[eval_exp_valid_def, isValid_def, noDowncast_def]
  >- (once_rewrite_tac [toREnv_def]
      \\ fs[validFloatValue_def]
      \\ rveq
      \\ fs[eval_exp_cases, fp64_to_float_float_to_fp64, dmode_def,
            float_to_real_real_to_float_zero_id]
      \\ fs[toREnv_def]
      \\ fs[eval_exp_float_def, optionLift_def]
      \\ Cases_on `E2 n` \\ fs[optionLift_def, normal_or_zero_def])
  >- (rveq \\ fs[eval_exp_cases]
      \\ fs[optionLift_def, normal_or_zero_def, minValue_pos_def,
            minExponentPos_def, REAL_LT_INV_EQ]
      \\ qexists_tac `0:real`
      \\ fs[mTypeToR_pos, perturb_def, fp64_to_float_float_to_fp64,
            zero_to_real])
  >- (fs[eval_exp_float_def, optionLift_def]
      \\ first_x_assum (qspecl_then [`E1`, `E2`, `E2_real`, `Gamma`, `tMap`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (fs[]
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
          \\ rveq \\ fs[]
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
          \\ fs[]
          \\ rveq
          \\ rw_asm_star `FloverMapTree_find (Unop _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Unop _ _) tMap = _`
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
      \\ fs[fp64_negate_def, fp64_to_float_float_to_fp64]
      \\ once_rewrite_tac [float_to_real_negate]
      \\ once_rewrite_tac [eval_exp_cases]
      \\ fs[] \\ once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac
      \\ fs[evalUnop_def])
  >- (Flover_compute ``validErrorbound``
      \\ rveq \\ fs[])
  >- (rename1 `Binop b (toRExp e1) (toRExp e2)`
      \\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
      \\ `FloverMapTree_find (toRExp e1) tMap = SOME M64 /\
          FloverMapTree_find (toRExp e2) tMap = SOME M64 /\
          FloverMapTree_find (Binop b (toRExp e1) (toRExp e2)) tMap = SOME M64`
          by (rpt conj_tac \\ irule typing_exp_64bit \\ fs[is64BitEval_def, noDowncast_def]
              \\ qexists_tac `Gamma` \\ fs[]
              \\ Flover_compute ``typeCheck``
              \\ rpt strip_tac \\ first_x_assum irule
              \\ simp[Once usedVars_def, domain_union])
      \\ `m1 = M64 /\ m2 = M64`
           by (conj_tac
               \\ Flover_compute ``typeCheck``
               \\ irule typing_agrees_exp
               \\ qexistsl_tac [`toREnv E2`, `Gamma`]
               THENL [qexists_tac `toRExp e1`, qexists_tac `toRExp e2`]
               \\ qexistsl_tac [`tMap`]
               THENL [qexists_tac `v1`, qexists_tac `v2`]
               \\ fs[])
      \\ rveq
      \\ ntac 2 (first_x_assum (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`, `tMap`] assume_tac))
      \\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (fs[]
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
          \\ rveq \\ fs[]
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
          \\ fs[]
          \\ rveq
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, Once usedVars_def]
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
      \\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (fs[]
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
          \\ rveq \\ fs[]
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
          \\ fs[]
          \\ rveq
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def]
          \\ fs[domain_union])
      \\ fs[]
      \\ rename1 `eval_exp_float e1 _ = SOME vF1`
      \\ rename1 `eval_exp_float e2 _ = SOME vF2`
      \\ `?iv err nR2. FloverMapTree_find (toRExp e2) A = SOME (iv, err) /\
            eval_exp E1 (toRMap Gamma) (toREval (toRExp e2)) nR2 REAL /\
            FST iv <= nR2 /\ nR2 <= SND iv`
           by (irule validIntervalbounds_sound
               \\ qexistsl_tac [`P`, `dVars`, `fVars`]
               \\ Flover_compute ``validIntervalbounds``
               \\ fs [DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac \\ first_x_assum irule
               \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
      \\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)`
      (* Obtain evaluation for E2_real*)
      \\ `!vF2 m2. eval_exp E2_real Gamma (toRExp e2) vF2 m2 ==>
            abs (nR2 - vF2) <= err2`
            by (qspecl_then [`toRExp e2`, `E1`, `E2_real`, `A`,`nR2`,
                             `err2`, `P`, `FST iv2`, `SND iv2`, `fVars`,
                             `dVars`, `tMap`, `Gamma`] destruct validErrorbound_sound
                \\ Flover_compute ``typeCheck``
                \\ Flover_compute ``validErrorbound``
                \\ Flover_compute ``validIntervalbounds``
                \\ fs[] \\ rveq \\ fs[]
                \\ fs [DIFF_DEF, SUBSET_DEF]
                \\ rpt strip_tac \\ first_x_assum irule
                \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
      \\ `contained (float_to_real (fp64_to_float vF2))
                    (widenInterval (FST iv2, SND iv2) err2)`
           by (irule distance_gives_iv
               \\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def]
               \\ first_x_assum irule
               \\ qexists_tac `M64`
               \\ drule eval_eq_env
               \\ rpt (disch_then drule) \\ fs[])
      \\ `b = Div ==> float_to_real (fp64_to_float vF2) <> 0`
           by (strip_tac \\ rveq
               \\ Flover_compute ``validErrorbound``
               \\ fs[IVhi_def, IVlo_def, widenInterval_def, contained_def,
                     noDivzero_def]
               >- (CCONTR_TAC \\ fs[] \\ rveq
                   \\ `0 < 0:real`
                        by (irule REAL_LET_TRANS
                            \\ qexists_tac `SND iv2 + err2` \\ fs[])
                   \\ fs[])
               \\ CCONTR_TAC \\ fs[] \\ rveq
               \\ `0 < 0:real`
                    by (irule REAL_LTE_TRANS
                        \\ qexists_tac `FST iv2 - err2` \\ fs[])
               \\ fs[])
      \\ `validFloatValue
            (evalBinop b (float_to_real (fp64_to_float vF1))
             (float_to_real (fp64_to_float vF2))) M64`
          by (drule FPRangeValidator_sound
              \\ disch_then
                   (qspecl_then
                     [`(Binop b (toRExp e1) (toRExp e2))`,
                      `evalBinop b (float_to_real (fp64_to_float vF1))
                        (float_to_real (fp64_to_float vF2))`,
                      `M64`, `tMap`, `P`] irule)
               \\ fs[]
               \\ qexistsl_tac [`P`, `e1`, `e2`, `tMap`]
               \\ fs[]
               \\ irule eval_eq_env
               \\ asm_exists_tac \\ fs[eval_exp_cases]
               \\ rewrite_tac [CONJ_ASSOC]
               \\ rpt (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
               \\ qexists_tac ` 0:real`
               \\ Cases_on `b`
               \\ fs[perturb_def, evalBinop_def, mTypeToR_pos, join_def])
      \\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
           by (drule FPRangeValidator_sound
               \\ disch_then
                    (qspecl_then
                       [`toRExp e1`,
                        `float_to_real (fp64_to_float vF1)`,
                         `M64`, `tMap`, `P`] irule)
               \\ fs[]
               \\ qexistsl_tac [`P`, `e1`, `tMap`] \\ fs[]
               \\ Flover_compute ``typeCheck``
               \\ Flover_compute ``validIntervalbounds``
               \\ Flover_compute ``validErrorbound``
               \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
               \\ rewrite_tac [CONJ_ASSOC] \\ conj_tac
               >- (fs[] \\ rveq \\ fs[]
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
                   \\ fs[SUBSET_DEF, DIFF_DEF]
                   \\ rpt strip_tac \\ first_x_assum irule
                   \\ simp[Once usedVars_def, domain_union] \\ fs[])
               \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
      \\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
           by (drule FPRangeValidator_sound
               \\ disch_then
                    (qspecl_then
                       [`toRExp e2`,
                        `float_to_real (fp64_to_float vF2)`,
                         `M64`, `tMap`, `P`] irule)
               \\ fs[]
               \\ qexistsl_tac [`P`, `e2`, `tMap`] \\ fs[]
               \\ Flover_compute ``typeCheck``
               \\ Flover_compute ``validIntervalbounds``
               \\ Flover_compute ``validErrorbound``
               \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
               \\ rewrite_tac [CONJ_ASSOC] \\ conj_tac
               >- (fs[] \\ rveq \\ fs[]
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
                   \\ fs[SUBSET_DEF, DIFF_DEF]
                   \\ rpt strip_tac \\ first_x_assum irule
                   \\ simp[Once usedVars_def, domain_union] \\ fs[])
               \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
      \\ simp[eval_exp_cases]
      (** Case distinction for operator **)
      \\ Cases_on `b` \\ fs[optionLift_def, PULL_EXISTS, normal_or_zero_def]
      (* Addition, result normal *)
      >- (fs[fp64_add_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ `normal (evalBinop Plus (float_to_real (fp64_to_float vF1))
                     (float_to_real (fp64_to_float vF2))) M64`
                by (rw_thm_asm `validFloatValue (_ + _) _` validFloatValue_def
                    \\ fs[normal_def, denormal_def, evalBinop_def]
                    >- (`abs (float_to_real (fp64_to_float vF1) +
                              float_to_real (fp64_to_float vF2)) <
                         abs (float_to_real (fp64_to_float vF1) +
                              float_to_real (fp64_to_float vF2))`
                           suffices_by (fs[])
                        \\ irule REAL_LTE_TRANS
                        \\ asm_exists_tac \\ fs[])
                    \\ qpat_x_assum `_ + _ = 0` (fn thm => fs[thm])
                    \\ fs[maxValue_def, maxExponent_def])
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                            `(fp64_to_float vF2):(52,11) float`]
               impl_subgoal_tac
               float_add_relative
           >- (rpt conj_tac
               \\ fs[validFloatValue_def,
                     normalTranslatedValue_implies_finiteness,
                     denormalTranslatedValue_implies_finiteness,
                     normalValue_implies_normalization,
                     GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
           \\ fs[dmode_def]
           \\ rename1 `abs err <= _`
           \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                           `float_to_real (fp64_to_float vF2)`, `err`]
           \\ fs[perturb_def, evalBinop_def]
           \\ fs[mTypeToR_def, join_def, perturb_def])
      (* result = 0 *)
      >- (IMP_RES_TAC validValue_gives_float_value
          \\ fs[REAL_LNEG_UNIQ, evalBinop_def]
          \\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64]
          \\ fs[float_add_def, float_round_with_flags_def]
          \\ fs[join_def]
          \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                           `float_to_real (fp64_to_float vF2)`, `0:real`]
          \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
          \\ `2 * abs (0:real) <= ulp (:52 #11)`
                by (fs[ulp_def, ULP_def])
          \\ fs[float_to_real_round_zero_is_zero])
      (* Subtraction, normal value *)
      >- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ `normal (evalBinop Sub (float_to_real (fp64_to_float vF1))
                     (float_to_real (fp64_to_float vF2))) M64`
                by (rw_thm_asm `validFloatValue (_ - _) _` validFloatValue_def
                    \\ fs[normal_def, denormal_def, evalBinop_def]
                    >- (`abs (float_to_real (fp64_to_float vF1) -
                              float_to_real (fp64_to_float vF2)) <
                         abs (float_to_real (fp64_to_float vF1) -
                              float_to_real (fp64_to_float vF2))`
                           suffices_by (fs[])
                        \\ irule REAL_LTE_TRANS
                        \\ asm_exists_tac \\ fs[])
                    \\ qpat_x_assum `float_to_real (fp64_to_float _) = _`
                         (fn thm => fs[thm])
                    \\ fs[maxValue_def, maxExponent_def])
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                               `(fp64_to_float vF2):(52,11) float`]
                 impl_subgoal_tac
                 float_sub_relative
               >- (rpt conj_tac
                       \\ fs[validFloatValue_def,
                             normalTranslatedValue_implies_finiteness,
                             denormalTranslatedValue_implies_finiteness,
                             normalValue_implies_normalization,
                             GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
               \\ fs[dmode_def]
               \\ rename1 `abs err <= _`
               \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                    `float_to_real (fp64_to_float vF2)`, `err`]
               \\ fs[perturb_def, evalBinop_def]
               \\ fs[mTypeToR_def, join_def, perturb_def])
      >- (fs[evalBinop_def]
          \\ qpat_x_assum `float_to_real (fp64_to_float _) = _` MP_TAC
          \\ simp[real_sub, REAL_LNEG_UNIQ, evalBinop_def]
          \\ fs[fp64_sub_def, dmode_def, fp64_to_float_float_to_fp64]
          \\ fs[float_sub_def]
          \\ fs[join_def]
          \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
          \\ fs[validValue_gives_float_value, float_round_with_flags_def]
          \\ strip_tac
          \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`]
          \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
          \\ fs[validValue_gives_float_value, float_round_with_flags_def]
          \\ `2 * abs (0:real) <= ulp (:52 #11)`
                by (fs[ulp_def, ULP_def])
          \\ fs[ float_to_real_round_zero_is_zero])
      (* Multiplication *)
      >- (fs[fp64_mul_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ `normal (evalBinop Mult (float_to_real (fp64_to_float vF1))
                     (float_to_real (fp64_to_float vF2))) M64`
                by (rw_thm_asm `validFloatValue (_ * _) _` validFloatValue_def
                    \\ fs[normal_def, denormal_def, evalBinop_def]
                    >- (`abs (float_to_real (fp64_to_float vF1) *
                              float_to_real (fp64_to_float vF2)) <
                         abs (float_to_real (fp64_to_float vF1) *
                              float_to_real (fp64_to_float vF2))`
                           suffices_by (fs[])
                        \\ irule REAL_LTE_TRANS
                        \\ asm_exists_tac \\ fs[])
                    >- (qpat_x_assum `float_to_real (fp64_to_float _) = _`
                          (fn thm => fs[thm])
                        \\ fs[maxValue_def, maxExponent_def])
                    \\ qpat_x_assum `float_to_real (fp64_to_float _) = _`
                         (fn thm => fs[thm])
                    \\ fs[maxValue_def, maxExponent_def])
          \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                            `(fp64_to_float vF2):(52,11) float`]
               impl_subgoal_tac
               float_mul_relative
           >- (rpt conj_tac
               \\ fs[validFloatValue_def,
                             normalTranslatedValue_implies_finiteness,
                             denormalTranslatedValue_implies_finiteness,
                             normalValue_implies_normalization,
                             GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
               \\ fs[dmode_def]
               \\ rename1 `abs err <= _`
               \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                    `float_to_real (fp64_to_float vF2)`, `err`]
               \\ fs[perturb_def, evalBinop_def]
               \\ fs[mTypeToR_def, join_def, perturb_def])
      >- (fs[evalBinop_def, REAL_ENTIRE, fp64_mul_def, float_mul_def,
             GSYM float_is_zero_to_real, float_is_zero_def]
            THENL [ Cases_on `float_value (fp64_to_float vF1)`,
                    Cases_on `float_value (fp64_to_float vF2)`]
             \\ fs[validValue_gives_float_value]
             \\ fs[float_round_with_flags_def, dmode_def,
                   fp64_to_float_float_to_fp64, perturb_def]
             \\ Cases_on `(fp64_to_float vF1).Sign ≠ (fp64_to_float vF2).Sign`
             \\ `2 * abs (0:real) <= ulp (:52#11)`
               by (fs[ulp_def, ULP_def])
             \\ fs [round_roundTiesToEven_is_plus_zero,
                    round_roundTiesToEven_is_minus_zero, zero_to_real]
             \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                    `float_to_real (fp64_to_float vF2)`, `0:real`]
             \\ rveq
             \\ fs[GSYM float_is_zero_to_real, float_is_zero_def, join_def, mTypeToR_pos, perturb_def])
      (* Division *)
      >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
          \\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1))
                     (float_to_real (fp64_to_float vF2))) M64`
                by (rw_thm_asm `validFloatValue (_ / _) _` validFloatValue_def
                    \\ fs[normal_def, denormal_def, evalBinop_def]
                    >- (`abs (float_to_real (fp64_to_float vF1) /
                              float_to_real (fp64_to_float vF2)) <
                         abs (float_to_real (fp64_to_float vF1) /
                              float_to_real (fp64_to_float vF2))`
                           suffices_by (fs[])
                        \\ irule REAL_LTE_TRANS
                        \\ asm_exists_tac \\ fs[])
                    \\ qpat_x_assum `_ = 0` (fn thm => fs[thm])
                    \\ fs[maxValue_def, maxExponent_def])
             \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
                               `(fp64_to_float vF2):(52,11) float`]
                 impl_subgoal_tac
                 float_div_relative
               >- (rpt conj_tac
                       \\ fs[validFloatValue_def,
                             normalTranslatedValue_implies_finiteness,
                             denormalTranslatedValue_implies_finiteness,
                             normalValue_implies_normalization,
                             GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
               \\ fs[dmode_def]
               \\ rename1 `abs err <= _`
               \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                    `float_to_real (fp64_to_float vF2)`, `err`]
               \\ fs[perturb_def, evalBinop_def]
               \\ fs[mTypeToR_def, join_def, perturb_def])
      >- (fs[fp64_div_def, dmode_def, fp64_to_float_float_to_fp64,
             float_div_def, evalBinop_def]
          \\ `float_to_real (fp64_to_float vF1) = 0`
               by (fs[div_eq0_general])
         \\ rw_thm_asm `float_to_real (fp64_to_float vF1) = 0` (GSYM float_is_zero_to_real)
         \\ fs[float_is_zero_def]
         \\ Cases_on `float_value (fp64_to_float vF1)`
         \\ fs[validValue_gives_float_value]
         \\ simp [float_round_with_flags_def]
         \\ Cases_on `(fp64_to_float vF1).Sign ≠ (fp64_to_float vF2).Sign`
         \\ `2 * abs (0:real) <= ulp (:52#11)`
                 by (fs[ulp_def, ULP_def])
         \\ fs [round_roundTiesToEven_is_plus_zero,
                 round_roundTiesToEven_is_minus_zero, zero_to_real]
         \\ rveq
         \\ `float_to_real (fp64_to_float vF1) = 0:real`
               by (fs[GSYM float_is_zero_to_real, float_is_zero_def])
         \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                    `float_to_real (fp64_to_float vF2)`, `0:real`]
         \\  fs[perturb_def, join_def, mTypeToR_pos]))
  >- (rename1 `Fma (toRExp e1) (toRExp e2) (toRExp e3)`
      \\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
      \\ `FloverMapTree_find (toRExp e1) tMap = SOME M64 /\
          FloverMapTree_find (toRExp e2) tMap = SOME M64 /\
          FloverMapTree_find (toRExp e3) tMap = SOME M64 /\
          FloverMapTree_find (Fma (toRExp e1) (toRExp e2) (toRExp e3)) tMap = SOME M64`
          by (rpt conj_tac \\ irule typing_exp_64bit \\ fs[is64BitEval_def, noDowncast_def]
              \\ qexists_tac `Gamma` \\ fs[]
              \\ Flover_compute ``typeCheck`` \\ fs[] \\ rveq \\ fs[]
              \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union])
      \\ `m1 = M64 /\ m2 = M64 /\ m3 = M64`
           by (rpt conj_tac
               \\ Flover_compute ``typeCheck``
               \\ irule typing_agrees_exp
               \\ qexistsl_tac [`toREnv E2`, `Gamma`]
               THENL [qexists_tac `toRExp e1`, qexists_tac `toRExp e2`, qexists_tac `toRExp e3`]
               \\ qexistsl_tac [`tMap`]
               THENL [qexists_tac `v1`, qexists_tac `v2`, qexists_tac `v3`]
               \\ fs[])
      \\ rveq
      \\ ntac 3 (first_x_assum (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`, `tMap`] assume_tac))
      \\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (fs[]
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
          \\ rveq \\ fs[]
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
          \\ fs[]
          \\ rveq
          \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) tMap = _`
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def]
          \\ fs[domain_union])
      \\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (fs[]
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
          \\ rveq \\ fs[]
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
          \\ fs[]
          \\ rveq
          \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) tMap = _`
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def]
          \\ fs[domain_union])
      \\ first_x_assum (qspecl_then [`v3`, `A`, `P`, `fVars`, `dVars`] destruct)
      >- (fs[]
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
          \\ rveq \\ fs[]
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
          \\ fs[]
          \\ rveq
          \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) tMap = _`
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def]
          \\ fs[domain_union])
      \\ fs[optionLift_def]));

val bstep_gives_IEEE = store_thm (
  "bstep_gives_IEEE",
  ``!(f:word64 cmd) E1 E2 E2_real Gamma tMap vR vF A P fVars dVars outVars.
      (!x. (toREnv E2) x = E2_real x) /\
      approxEnv E1 Gamma A fVars dVars E2_real /\
      ssa (toRCmd f) (union fVars dVars) outVars /\
      typeCheckCmd (toRCmd f) Gamma tMap /\
      validIntervalboundsCmd (toRCmd f) A P dVars /\
      validErrorboundCmd (toRCmd f) tMap A dVars /\
      FPRangeValidatorCmd (toRCmd f) A tMap dVars /\
      bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR REAL /\
      bstep (toRCmd f) (toREnv E2) Gamma vF M64 /\
      domain (freeVars (toRCmd f)) DIFF domain dVars ⊆ domain fVars ∧
      is64BitBstep (toRCmd f) /\
      noDowncastFun (toRCmd f) /\
      bstep_valid f E2 /\
      dVars_range_valid dVars E1 A /\
      fVars_P_sound fVars E1 P /\
      vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
      (∀v.
        v ∈ domain dVars ⇒
        ∃vF m.
        (E2_real v = SOME vF ∧ FloverMapTree_find (Var v) tMap = SOME m ∧
        validFloatValue vF m)) /\
      (!v. v IN domain (freeVars (toRCmd f)) ==> Gamma v = SOME M64) ==>
      ?v.
        bstep_float f E2 = SOME v /\
        bstep (toRCmd f) (toREnv E2) Gamma (float_to_real (fp64_to_float v)) M64``,
  Induct_on `f`
  \\ simp [toRCmd_def, Once toREvalCmd_def, is64BitBstep_def,
                 noDowncastFun_def, bstep_valid_def]
  \\ rpt strip_tac
  \\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
  \\ inversion `ssa _ _ _` ssa_cases
  \\ once_rewrite_tac [bstep_float_def]
  \\ fs[bstep_valid_def, noDowncast_def]
  \\ Flover_compute ``validIntervalboundsCmd``
  \\ Flover_compute ``typeCheckCmd``
  \\ Flover_compute ``validErrorboundCmd``
  \\ fs[] \\ rveq \\ fs[]
  >- (`?v_e. eval_exp_float e E2 = SOME v_e /\
         eval_exp (toREnv E2) Gamma (toRExp e) (float_to_real (fp64_to_float v_e)) M64`
        by (irule eval_exp_gives_IEEE \\ fs[]
            >- (rpt strip_tac \\ first_x_assum irule
                \\ fs[Once freeVars_def, domain_union]
                \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
                \\ fs[SUBSET_DEF, domain_union]
                \\ `n IN domain fVars \/ n IN domain dVars`
                    by (first_x_assum irule \\ fs[]))
            >- (rveq \\ asm_exists_tac \\ fs[])
            \\ qexistsl_tac [`A`, `E1`, `E2_real`, `P`, `dVars`, `fVars`, `tMap`]
            \\ Flover_compute ``validIntervalboundsCmd``
            \\ Flover_compute ``validErrorboundCmd``
            \\ Flover_compute ``typeCheckCmd``
            \\ fs [Once FPRangeValidatorCmd_def]
            \\ rpt conj_tac \\ fs[] \\ rpt strip_tac
            \\ fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]
            \\ rveq \\ fs[]
            \\ rpt strip_tac
            \\ `x IN domain fVars \/  x IN domain dVars`
                 by (first_x_assum irule \\ fs[]))
        \\ qspecl_then [`(toRExp e)`, `A`, `P`, `fVars`, `dVars`, `E1`, `Gamma`]
             destruct validIntervalbounds_sound
        >- (fs[DIFF_DEF, SUBSET_DEF]
            \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def, domain_union]
            \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
            \\ `n IN domain fVars \/ n IN domain dVars`
                 by (first_x_assum irule \\ fs[]))
        \\ qspecl_then [`toRCmd f`, `A`, `updEnv n v' E1`, `fVars`, `insert n () dVars`, `outVars`,
                        `P`, `updDefVars n M64 Gamma`] destruct validIntervalboundsCmd_sound
        >- (fs[] \\ rpt conj_tac
            >- (irule ssa_equal_set
                \\ qexists_tac `insert n () (union fVars dVars)`
                \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
                \\ rewrite_tac [domain_union, domain_insert]
                \\ rewrite_tac [UNION_DEF, INSERT_DEF]
                \\ fs[EXTENSION]
                \\ rpt strip_tac
                \\ metis_tac[])
            >- (fs[dVars_range_valid_def, DIFF_DEF, domain_insert, SUBSET_DEF]
                \\ rpt strip_tac \\ fs[]
                >- (rveq \\ metis_tac [meps_0_deterministic])
                \\ IF_CASES_TAC
                >- (rveq \\ metis_tac [meps_0_deterministic])
                \\ first_x_assum irule \\ fs [])
            >- (fs[fVars_P_sound_def]
                \\ rpt strip_tac
                \\ IF_CASES_TAC
                >- (rveq \\ fs[DIFF_DEF, SUBSET_DEF, domain_union])
                \\ first_x_assum irule \\ fs[])
            >- (fs[vars_typed_def]
                \\ rpt strip_tac
                \\ TRY (first_x_assum irule \\ fs[domain_union] \\ rveq)
                \\ IF_CASES_TAC \\ fs[])
            \\ fs [domain_union, Once freeVars_def, DIFF_DEF, SUBSET_DEF]
            \\ rpt strip_tac \\ first_x_assum irule \\ fs[]
            \\ simp[Once freeVars_def])
        (* prove validity of errorbound for floating-point value *)
        \\ qspecl_then
             [`toRExp e`, `E1`, `E2_real`, `A`, `v'`, `err_e`, `P`,
              `FST iv_e`, `SND iv_e`, `fVars`, `dVars`, `tMap`, `Gamma`]
             impl_subgoal_tac
             validErrorbound_sound
        >- (fs[DIFF_DEF, SUBSET_DEF]
            \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def, domain_union]
            \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
            \\ `n IN domain fVars \/ n IN domain dVars`
                 by (first_x_assum irule \\ fs[]))
        \\ fs[]
        \\ `abs (v' - (float_to_real (fp64_to_float v_e))) <= err_e`
             by (first_x_assum irule \\ fs[]
                 \\ qexists_tac `M64` \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
        \\ rename1 `FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv_f, err_f)`
        (* Now construct a new evaluation according to our big-step semantics
           using lemma validErrorboundCmd_gives_eval *)
        \\ qspecl_then
             [ `toRCmd f`, `A`, `updEnv n v' E1`,
               `updEnv n (float_to_real (fp64_to_float v_e)) E2_real`,
               `outVars`, `fVars`, `insert n () dVars`, `vR`, `FST iv_f`, `SND iv_f`,
               `err_f`, `P`, `M64`, `tMap`, `updDefVars n M64 Gamma`]
             impl_subgoal_tac
             validErrorboundCmd_gives_eval
        >- (fs[] \\ rpt conj_tac
            >- (irule approxUpdBound
                \\ fs[lookup_NONE_domain])
            >- (irule ssa_equal_set
                \\ qexists_tac `insert n () (union fVars dVars)`
                \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
                \\ rewrite_tac [domain_union, domain_insert]
                \\ rewrite_tac [UNION_DEF, INSERT_DEF]
                \\ fs[EXTENSION]
                \\ rpt strip_tac
                \\ metis_tac[])
            >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
                \\ rpt strip_tac \\ first_x_assum irule
                \\ fs[Once freeVars_def]
                \\ simp[Once freeVars_def, domain_union])
            >- (irule swap_Gamma_bstep
                \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[]
                \\ strip_tac
                \\ qspecl_then [`Gamma`, `n`, `M64`, `n'`] assume_tac Rmap_updVars_comm
                \\ fs[updDefVars_def])
            >- (fs[dVars_range_valid_def] \\ rpt strip_tac \\ simp[updEnv_def]
                \\ rveq \\ fs[]
                >- (drule validIntervalbounds_sound
                    \\ rpt (disch_then drule)
                    \\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`] impl_subgoal_tac)
                    >- (fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
                        \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, dVars_range_valid_def]
                        \\ rpt strip_tac \\ first_x_assum irule
                        \\ simp[Once freeVars_def, domain_union]
                        \\ CCONTR_TAC \\ fs[]
                        \\ rveq
                        \\ `n IN domain fVars \/ n IN domain dVars`
                             by (first_x_assum irule \\ fs[]))
                    \\ fs[]
                    \\ metis_tac [meps_0_deterministic])
                \\ IF_CASES_TAC \\ fs[]
                \\ rveq
                \\ fs[domain_union])
            >- (fs[fVars_P_sound_def] \\ rpt strip_tac \\ simp[updEnv_def]
                \\ IF_CASES_TAC \\ fs[]
                \\ rveq
                \\ fs[domain_union])
            \\ fs[vars_typed_def] \\ rpt strip_tac \\ fs[updDefVars_def]
            \\ IF_CASES_TAC \\ fs[]
            \\ first_x_assum irule \\ fs[])
        \\ fs[optionLift_def]
        \\ `FloverMapTree_find (getRetExp (toRCmd f)) tMap= SOME M64`
              by (irule typingSoundnessCmd
                  \\ qexistsl_tac [`updEnv n v (toREnv E2)`, `updDefVars n M64 Gamma`, `vF`]
                  \\ fs[]
                  \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
                  \\ EVERY_CASE_TAC \\ fs[]\\ rveq \\ fs[])
        \\ `m' = M64`
             by (irule typing_agrees_cmd
                 \\ rewrite_tac [CONJ_ASSOC] \\ once_rewrite_tac[CONJ_COMM]
                 \\ rpt (asm_exists_tac \\ fs[])
                 \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
                 \\ EVERY_CASE_TAC \\ fs[] \\ rveq \\ fs[])
        \\ rveq \\ fs[bstep_cases, PULL_EXISTS]
        (* Instantiate IH with newly obtained evaluation, to get the conclusion *)
        \\ first_x_assum
             (qspecl_then [`updEnv n v' E1`, `updFlEnv n v_e E2`,
                           `updEnv n (float_to_real (fp64_to_float v_e)) E2_real`,
                           `updDefVars n M64 Gamma`, `tMap`, `vR`, `vF'`, `A`,
                           `P`, `fVars`, `insert n () dVars`, `outVars`]
             impl_subgoal_tac)
        >- (simp[Once validErrorboundCmd_def, Once validIntervalboundsCmd_def]
            \\ fs [Once FPRangeValidatorCmd_def]
            \\ rveq \\ fs[]
            \\ rpt conj_tac
            >- (strip_tac \\ fs[updFlEnv_def, updEnv_def, toREnv_def]
                \\ IF_CASES_TAC \\ fs[])
            >- (drule approxUpdBound
                \\ disch_then
                     (qspecl_then
                        [`M64`, `v'`, `float_to_real (fp64_to_float v_e)`, `n`]
                        irule)
                \\ fs[domain_lookup, lookup_NONE_domain])
            >- (irule ssa_equal_set
                \\ qexists_tac `insert n () (union fVars dVars)`
                \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
                \\ rewrite_tac [domain_union, domain_insert]
                \\ rewrite_tac [UNION_DEF, INSERT_DEF]
                \\ fs[EXTENSION]
                \\ rpt strip_tac
                \\ metis_tac[])
            >- (irule swap_Gamma_bstep
                \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[]
                \\ rpt strip_tac
                \\ qspecl_then [`Gamma`, `n`, `M64`, `n'`] assume_tac Rmap_updVars_comm
                \\ fs[updDefVars_def])
            >- (irule bstep_eq_env
                \\ qexists_tac `updEnv n (float_to_real (fp64_to_float v_e)) E2_real`
                \\ fs[]
                \\ strip_tac \\ fs[updEnv_def, toREnv_def, updFlEnv_def]
                \\ IF_CASES_TAC \\ fs[])
            >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
                \\ rpt strip_tac \\ first_x_assum irule
                \\ fs[Once freeVars_def]
                \\ simp[Once freeVars_def, domain_union])
            >- (fs[dVars_range_valid_def] \\ rpt strip_tac \\ simp[updEnv_def]
                >- (rveq  \\ metis_tac [meps_0_deterministic])
                \\ IF_CASES_TAC \\ fs[]
                \\ rveq
                \\ fs[domain_union])
            >- (fs[fVars_P_sound_def] \\ rpt strip_tac \\ simp[updEnv_def]
                \\ rveq \\ fs[]
                \\ IF_CASES_TAC \\ rveq \\ fs[]
                \\ fs[DIFF_DEF, SUBSET_DEF, domain_union])
            >- (fs[vars_typed_def] \\ rpt strip_tac \\ simp[updDefVars_def]
                \\ IF_CASES_TAC \\ fs[])
            >- (rpt strip_tac \\ simp[updEnv_def]
                \\ rveq \\ fs[]
                >- (irule FPRangeValidator_sound
                    \\ qexistsl_tac [`A`, `E1`, `E2_real`, `Gamma`, `P`, `dVars`,
                                     `toRExp e`, `fVars`, `tMap`]
                    \\ fs[]
                    \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
                    >- (fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]
                        \\ rpt strip_tac \\ first_x_assum irule \\ fs[]
                        \\ CCONTR_TAC \\ fs[]
                        \\ rveq \\ fs[]
                        \\ metis_tac [])
                    \\ irule eval_eq_env
                    \\ asm_exists_tac \\ fs[])
                \\ IF_CASES_TAC \\ fs[]
                \\ irule FPRangeValidator_sound
                \\ qexistsl_tac [`A`, `E1`, `E2_real`, `Gamma`, `P`, `dVars`,
                                `toRExp e`, `fVars`, `tMap`]
                \\ fs[]
                \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
                >- (fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]
                    \\ rpt strip_tac \\ first_x_assum irule \\ fs[]
                    \\ CCONTR_TAC \\ fs[]
                    \\ rveq \\ fs[]
                    \\ metis_tac [])
                \\ irule eval_eq_env
                \\ asm_exists_tac \\ fs[])
            \\ rpt strip_tac \\ simp [updDefVars_def]
            \\ IF_CASES_TAC \\ fs[]
            \\ first_x_assum irule \\ fs[]
            \\ simp[Once freeVars_def, domain_union])
        \\ fs[]
        \\ qexists_tac `float_to_real (fp64_to_float v_e)` \\ fs[]
        \\ irule bstep_eq_env \\ once_rewrite_tac[CONJ_COMM]
        \\ asm_exists_tac \\ fs[]
        \\ strip_tac \\ fs[toREnv_def, updEnv_def, updFlEnv_def]
        \\ IF_CASES_TAC \\ fs[])
  >- (fs[bstep_cases] \\ irule eval_exp_gives_IEEE
      \\ fs[]
      >- (rpt strip_tac \\ first_x_assum irule
          \\ fs[freeVars_def] \\ fs[])
      >- (rveq \\ asm_exists_tac \\ fs[])
      \\ rewrite_tac [CONJ_ASSOC]
      \\ rpt (once_rewrite_tac [CONJ_COMM]
              \\ asm_exists_tac \\ fs[])
      \\ fs [Once validIntervalboundsCmd_def, Once validErrorboundCmd_def,
             Once typeCheckCmd_def, Once FPRangeValidatorCmd_def]
      \\ rpt conj_tac \\ fs[] \\ rpt strip_tac
      >- (qpat_x_assum `!v. _ ==> ?vF m. _` (qspec_then `v` destruct)
          \\ fs[freeVars_def])
      \\ fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]));

val IEEE_connection_exp = store_thm (
  "IEEE_connection_exp",
  ``!(e:word64 exp) (A:analysisResult) (P:precond) E1 E2 defVars fVars.
      approxEnv E1 defVars A fVars LN (toREnv E2) /\
      is64BitEval (toRExp e) /\
      noDowncast (toRExp e) /\
      eval_exp_valid e E2 /\
      fVars_P_sound fVars E1 P /\
      (domain (usedVars (toRExp e))) SUBSET (domain fVars) /\
      (!v. v IN domain fVars ==> ?m. defVars v = SOME m) /\
      (!v. v IN domain (usedVars (toRExp e)) ==> defVars v = SOME M64) /\
      CertificateChecker (toRExp e) A P defVars ==>
      ?iv err vR vF. (* m, currently = M64 *)
        FloverMapTree_find (toRExp e) A = SOME (iv, err) /\
        eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
       eval_exp_float e E2 = SOME vF /\
       eval_exp (toREnv E2) defVars (toRExp e) (float_to_real (fp64_to_float vF)) M64 /\
       abs (vR - (float_to_real (fp64_to_float vF))) <= err``,
  rpt strip_tac
  \\ drule Certificate_checking_is_sound
  \\ rpt (disch_then drule)
  \\ disch_then (qspecl_then [`toRExp e`, `P`] destruct)
  \\ fs[fVars_P_sound_def]
  \\ rpt strip_tac \\ asm_exists_tac
  \\ fs[CertificateChecker_def]
  \\ qspecl_then [`e`, `E1`, `E2`, `toREnv E2`, `defVars`,
                  `typeMap defVars (toRExp e) FloverMapTree_empty`, `vF`, `A`, `P`, `fVars`,
                  `LN`]
       destruct
       eval_exp_gives_IEEE
  >- (rpt conj_tac \\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
      \\ `FloverMapTree_find (toRExp e) (typeMap defVars (toRExp e) FloverMapTree_empty)  = SOME M64`
           by (drule typing_exp_64bit
               \\ rpt (disch_then drule)
               \\ fs[])
      \\ `m = M64`
           by (drule typing_agrees_exp
               \\ rpt (disch_then drule)
               \\ fs[])
      \\ fs[])
  \\ res_tac \\ fs[]);

val IEEE_connection_cmds = store_thm (
  "IEEE_connection_cmds",
  ``!(f:word64 cmd) (A:analysisResult) (P:precond) E1 E2 defVars (fVars:num_set).
      approxEnv E1 defVars A (freeVars (toRCmd f)) LN (toREnv E2) /\
      is64BitBstep (toRCmd f) /\
      noDowncastFun (toRCmd f) /\
      bstep_valid f E2 /\
      fVars_P_sound fVars E1 P /\
      (∀v. v ∈ domain (freeVars (toRCmd f)) ⇒ defVars v = SOME M64) /\
      (domain (freeVars (toRCmd f))) SUBSET (domain fVars) /\
      (!v. v IN domain fVars ==> ?m. defVars v = SOME m) /\
      CertificateCheckerCmd (toRCmd f) A P defVars ==>
      ?iv err vR vF. (* m, currently = M64 *)
        FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv, err) /\
        bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
        bstep_float f E2 = SOME vF /\
        bstep (toRCmd f) (toREnv E2) defVars (float_to_real (fp64_to_float vF)) M64 /\
        abs (vR - (float_to_real (fp64_to_float vF))) <= err``,
  rpt strip_tac
  \\ qspecl_then
       [`toRCmd f`, `A`, `P`, `defVars`, `E1`, `toREnv E2`, `fVars`]
       impl_subgoal_tac
       CertificateCmd_checking_is_sound
  >- (fs[fVars_P_sound_def]
      \\ rpt strip_tac \\ first_x_assum irule
      \\ fs[SUBSET_DEF])
  \\ fs[CertificateCheckerCmd_def]
  \\ `?outVars. ssa (toRCmd f) (freeVars (toRCmd f)) outVars`
        by (drule validSSA_sound
            \\ rpt (disch_then drule)
            \\ fs[])
  \\ qspecl_then [`f`, `E1`, `E2`, `toREnv E2`, `defVars`,
                  `typeMapCmd defVars (toRCmd f) FloverMapTree_empty`, `vR`, `vF`, `A`, `P`,
                  `freeVars (toRCmd f)`, `LN`, `outVars`]
       destruct
       bstep_gives_IEEE
  >- (rpt conj_tac \\ fs[dVars_range_valid_def, fVars_P_sound_def, vars_typed_def]
      >-(`FloverMapTree_find (getRetExp (toRCmd f))
            (typeMapCmd defVars (toRCmd f) FloverMapTree_empty) = SOME M64`
           by (drule typing_cmd_64bit
               \\ rpt (disch_then drule)
               \\ fs[])
          \\ `m = M64`
                by (drule typing_agrees_cmd
                    \\ rpt (disch_then drule)
                    \\ fs[])
          \\ fs[])
      \\ rpt strip_tac
      \\ first_x_assum irule
      \\ fs[SUBSET_DEF])
  \\ qexistsl_tac [`vR`, `v`]
  \\ fs[]
  \\ first_x_assum irule
  \\ asm_exists_tac \\ fs[]);

val _ = export_theory ();