IEEE_connectionScript.sml 68.1 KB
Newer Older
1
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
Heiko Becker's avatar
Heiko Becker committed
2
open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics
3 4
     CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
     TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
Heiko Becker's avatar
Heiko Becker committed
5
     CommandsTheory ssaPrgsTheory EnvironmentsTheory FloverMapTheory
6
open preamble
7

8
val _ = new_theory "IEEE_connection";
9

Heiko Becker's avatar
Heiko Becker committed
10 11
val _ = temp_overload_on("abs",``real$abs``);

12 13
(** FloVer assumes rounding with ties to even, thus we explicitly define
    a rounding mode here **)
Heiko Becker's avatar
Heiko Becker committed
14
val dmode_def = Define `dmode = roundTiesToEven`;
15

16 17 18 19 20 21 22
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`;

23
val eval_exp_float_def = Define `
24 25
  (eval_exp_float (Var n) E = E n) /\
  (eval_exp_float (Const m v) E = SOME v) /\
26 27
  (eval_exp_float (Unop Neg e) E =
    case eval_exp_float e E of
28
      | SOME v =>  SOME (fp64_negate v)
29 30
      | _ => NONE) /\
  (eval_exp_float (Unop Inv e) E = NONE) /\
Heiko Becker's avatar
Heiko Becker committed
31 32
  (eval_exp_float (Binop b e1 e2) E =
    (case (eval_exp_float e1 E), (eval_exp_float e2 E) of
33
       | SOME v1, SOME v2 =>
34
             (case b of
35 36 37 38 39
                | 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)) /\
40 41 42
  (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)) /\
43 44
  (eval_exp_float (Downcast m e) E = NONE)`;

45 46 47 48 49 50
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)`;
51 52 53

val normal_or_zero_def = Define `
  normal_or_zero (v:real) =
54
    (minValue_pos M64 <= abs v \/ v = 0)`;
55 56 57 58 59 60 61

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 `
62 63
  (eval_exp_valid (Var n) E = T) /\
  (eval_exp_valid (Const m v) E = T) /\
64 65
  (eval_exp_valid (Unop u e) E = eval_exp_valid e E) /\
  (eval_exp_valid (Binop b e1 e2) E =
66 67 68 69 70 71 72 73 74 75 76 77 78
    (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)) /\
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
  (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)) /\
97
  (eval_exp_valid (Downcast m e) E = eval_exp_valid e E)`;
98

99 100
val bstep_valid_def = Define `
  (bstep_valid (Let m x e g) E =
101 102 103 104
   (eval_exp_valid e E /\
      optionLift (eval_exp_float e E)
        (\v_e. bstep_valid g (updFlEnv x v_e E))
        T)) /\
105 106
  (bstep_valid (Ret e) E = eval_exp_valid e E)`;

107 108 109 110 111
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)) /\
112
  (toRExp (Fma e1 e2 e3) = Fma (toRExp e1) (toRExp e2) (toRExp e3)) /\
113 114
  (toRExp (Downcast m e1) = Downcast m (toRExp e1))`;

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

119 120 121 122 123 124
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))`;

Heiko Becker's avatar
Heiko Becker committed
125 126 127 128 129
val toWordEnv_def = Define `
  toWordEnv E = \x. case E x of
                      | SOME v => SOME (float_to_fp64 (real_to_float dmode v))
                      | NONE => NONE`;

130 131 132 133 134 135 136
val Binop_to_Rop_def = Define `
  Binop_to_Rop (b:binop) :real->real->real =
    case b of
      | Plus => $+
      | Sub => $-
      | Mult => $*
      | Div => $/ `;
137

138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
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
158
  \\ fs[normal_def, normalizes_def, wordsTheory.INT_MAX_def, minValue_pos_def,
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
        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]);

Heiko Becker's avatar
Heiko Becker committed
174 175 176 177 178 179 180 181
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
182
  \\ qexists_tac `minValue_pos M64` \\ fs[]
Heiko Becker's avatar
Heiko Becker committed
183
  \\ irule REAL_LET_TRANS \\ qexists_tac `maxValue M64`
184
  \\ `minValue_pos M64 <= 1`
Heiko Becker's avatar
Heiko Becker committed
185
        by (once_rewrite_tac [GSYM REAL_INV1]
186
            \\ fs[minValue_pos_def, minExponentPos_def]
Heiko Becker's avatar
Heiko Becker committed
187 188 189 190 191
            \\ 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]);

192 193 194 195 196 197 198 199 200
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]
201
  \\ every_case_tac \\ fs[maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def]
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260
   >-( 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[]));

Heiko Becker's avatar
Heiko Becker committed
261 262 263 264 265 266 267 268 269
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[]
Heiko Becker's avatar
Heiko Becker committed
270
  \\ rw_thm_asm `abs _ < _` float_to_real_def
Heiko Becker's avatar
Heiko Becker committed
271 272 273 274 275 276 277
  \\ fs[]
  \\ `ff.Exponent <> 0w` by fs[]
  \\ fs[]
  \\ Cases_on `ff` \\ fs[]
  \\ `w2n (-1w:word11) = 2047`  by EVAL_TAC
  \\ `w2n c0 = 2047` by fs[]
  \\ fs[]
278
  \\ TOP_CASE_TAC \\ fs[minValue_pos_def, minExponentPos_def]
Heiko Becker's avatar
Heiko Becker committed
279 280 281
  \\ fs[REAL_ABS_MUL, POW_M1]
  >- (`44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <=  inv 1`
        by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
Heiko Becker's avatar
Heiko Becker committed
282 283
      \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
    by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
Heiko Becker's avatar
Heiko Becker committed
284
  \\ fs[REAL_INV1])
Heiko Becker's avatar
Heiko Becker committed
285 286
  >- (Cases_on `c1` \\ fs[]
      \\ `1 < abs (1 + &n / 4503599627370496)`
Heiko Becker's avatar
Heiko Becker committed
287 288 289 290 291 292 293 294 295 296 297 298 299
        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]
Heiko Becker's avatar
Heiko Becker committed
300
                \\ irule REAL_LT_IADD
Heiko Becker's avatar
Heiko Becker committed
301
                \\ fs[REAL_ADD_RID, real_div]
Heiko Becker's avatar
Heiko Becker committed
302 303
                \\ irule REAL_LT_MUL \\ fs[]
                \\ irule REAL_INV_POS \\ fs[])
Heiko Becker's avatar
Heiko Becker committed
304 305
              \\ `44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <=  inv 1`
                by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
Heiko Becker's avatar
Heiko Becker committed
306 307 308 309
               \\ `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)`
Heiko Becker's avatar
Heiko Becker committed
310 311
        \\ fs[]
        \\ once_rewrite_tac [GSYM REAL_MUL_RID]
Heiko Becker's avatar
Heiko Becker committed
312
        \\ once_rewrite_tac [GSYM REAL_MUL_ASSOC] \\ irule REAL_LT_LMUL_IMP
Heiko Becker's avatar
Heiko Becker committed
313 314 315 316
        \\ fs[]
        \\ unabbrev_all_tac \\ fs[])
  \\ fs[REAL_INV1]));

Heiko Becker's avatar
Heiko Becker committed
317 318 319 320 321 322
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[])
Heiko Becker's avatar
Heiko Becker committed
323
  >- (irule denormal_value_is_float_value \\ fs[])
Heiko Becker's avatar
Heiko Becker committed
324 325 326
  \\ fs[GSYM float_is_zero_to_real, float_is_zero_def]
  \\ every_case_tac \\ fs[]);

327 328 329 330 331 332 333 334 335
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[]);

Heiko Becker's avatar
Heiko Becker committed
336 337 338 339 340 341 342 343 344 345
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[]);

346 347 348 349 350 351 352 353
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]
);

Heiko Becker's avatar
Heiko Becker committed
354 355 356 357 358 359 360
(* 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]); *)
361

Heiko Becker's avatar
Heiko Becker committed
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416
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]);

417
val real_to_float_float_id = Q.prove (
Heiko Becker's avatar
Heiko Becker committed
418 419 420 421 422
  `!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`,
423
rpt strip_tac
Heiko Becker's avatar
Heiko Becker committed
424 425 426
\\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
\\ fs[real_to_float_id]
\\ fs[float_to_fp64_fp64_to_float]);
427

428 429 430 431 432 433 434 435
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]);

Heiko Becker's avatar
Heiko Becker committed
436 437 438 439 440 441 442 443 444
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]);

445 446 447 448 449 450 451 452
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]);
Heiko Becker's avatar
Heiko Becker committed
453

Heiko Becker's avatar
Heiko Becker committed
454 455 456 457 458
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)) /\
459
  (noDowncast (Fma e1 e2 e3) = (noDowncast e1 /\ noDowncast e2 /\ noDowncast e3)) /\
Heiko Becker's avatar
Heiko Becker committed
460 461
  (noDowncast (Downcast _ _) = F)`;

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

466 467 468 469 470 471
(* 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)`; *)
Heiko Becker's avatar
Heiko Becker committed
472

Heiko Becker's avatar
Heiko Becker committed
473 474 475 476
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)) /\
477
  (is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\
Heiko Becker's avatar
Heiko Becker committed
478 479 480
  (is64BitEval (Downcast m e) = is64BitEval e) /\
  (is64BitEval ((Var v):real exp) = T)`;

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

485 486
(* val typeMap_eq_typeExp = Q.prove(` *)
(*   !e. *)
Heiko Becker's avatar
Heiko Becker committed
487
(*     FloverMapTree_find e (typeMap Gamma e (FloverMapTree_empty)) *)
488 489 490
(*     = typeExpression Gamma e`, *)
(*   Induct  *)
(*   \\ fs[Once typeMap_def] \\ rpt strip_tac *)
Heiko Becker's avatar
Heiko Becker committed
491
(*   \\ fs[FloverMapTree_empty_def, Once typeExpression_def] *)
492
(*   \\ rpt strip_tac  *)
Heiko Becker's avatar
Heiko Becker committed
493
(*   \\ Flover_compute ``typeExpression_def`` fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] ); *)
Heiko Becker's avatar
Heiko Becker committed
494

495
val typing_exp_64bit = store_thm("typing_exp_64bit",
496
  ``!e Gamma tMap.
Heiko Becker's avatar
Heiko Becker committed
497 498 499
      noDowncast e /\ is64BitEval e /\
      typeCheck e Gamma tMap /\
      (!v. v IN domain(usedVars e) ==> Gamma v = SOME M64) ==>
Heiko Becker's avatar
Heiko Becker committed
500
       FloverMapTree_find e tMap = SOME M64``,
501
  Induct
Heiko Becker's avatar
Heiko Becker committed
502
  \\ rpt strip_tac \\ Flover_compute ``typeCheck`` \\ fs[noDowncast_def]
503 504 505
  >- (fs[usedVars_def])
  >- (fs[]  \\ rveq \\ fs[is64BitEval_def])
  >- (fs[]
Heiko Becker's avatar
Heiko Becker committed
506
      \\ `FloverMapTree_find e tMap = SOME M64`
507 508 509 510 511 512 513 514 515
            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[]
Heiko Becker's avatar
Heiko Becker committed
516
      \\ `FloverMapTree_find e2 tMap = SOME M64`
517 518 519 520 521
            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[])
Heiko Becker's avatar
Heiko Becker committed
522
      \\ `FloverMapTree_find e1 tMap = SOME M64`
523 524 525 526 527 528 529 530
            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[]
Heiko Becker's avatar
Heiko Becker committed
531
  \\ `FloverMapTree_find e3 tMap = SOME M64`
532 533 534 535 536
        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[])
Heiko Becker's avatar
Heiko Becker committed
537
  \\ `FloverMapTree_find e2 tMap = SOME M64`
538 539 540 541 542
        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[])
Heiko Becker's avatar
Heiko Becker committed
543
  \\ `FloverMapTree_find e1 tMap = SOME M64`
544 545 546 547 548 549
        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]);
Heiko Becker's avatar
WIP  
Heiko Becker committed
550

551 552 553 554 555 556 557
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) ==>
Heiko Becker's avatar
Heiko Becker committed
558
       FloverMapTree_find (getRetExp f) tMap = SOME M64``,
559
  Induct \\ rpt strip_tac
Heiko Becker's avatar
Heiko Becker committed
560
  \\ Flover_compute ``typeCheckCmd``
561
  \\ fs[]
562
  >- (rveq \\ once_rewrite_tac [getRetExp_def]
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578
      \\ 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",
Heiko Becker's avatar
Heiko Becker committed
579 580 581
  ``!e E Gamma tMap v m1 m2 .
      typeCheck e Gamma tMap /\
      eval_exp E Gamma e v m1 /\
Heiko Becker's avatar
Heiko Becker committed
582
      FloverMapTree_find e tMap = SOME m2 ==>
Heiko Becker's avatar
Heiko Becker committed
583
      m1 = m2``,
584 585 586 587
  rpt strip_tac
  \\ drule  typingSoundnessExp
  \\ disch_then drule
  \\ disch_then assume_tac
Heiko Becker's avatar
Heiko Becker committed
588
  \\ fs[FloverMapTree_find_injective]);
Heiko Becker's avatar
Heiko Becker committed
589

590 591 592 593 594
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 /\
Heiko Becker's avatar
Heiko Becker committed
595
       FloverMapTree_find (getRetExp f) tMap = SOME m2 ==>
596
       m1 = m2``,
597 598 599 600
  rpt strip_tac
  \\ drule typingSoundnessCmd
  \\ disch_then drule
  \\ disch_then assume_tac
Heiko Becker's avatar
Heiko Becker committed
601
  \\ fs[FloverMapTree_find_injective]);
Heiko Becker's avatar
Heiko Becker committed
602

603 604 605
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) /\
Heiko Becker's avatar
Heiko Becker committed
606
      typeCheck (toRExp e) Gamma tMap /\
607
      approxEnv E1 Gamma A fVars dVars E2_real /\
608
      validIntervalbounds (toRExp e) A P dVars /\
Heiko Becker's avatar
Heiko Becker committed
609
      validErrorbound (toRExp e) tMap A dVars /\
610
      FPRangeValidator (toRExp e) A tMap dVars /\
611 612
      eval_exp (toREnv E2) Gamma (toRExp e) vR M64 /\
      domain (usedVars (toRExp e)) DIFF domain dVars  domain fVars 
Heiko Becker's avatar
WIP  
Heiko Becker committed
613
      is64BitEval (toRExp e) /\
Heiko Becker's avatar
Heiko Becker committed
614
      noDowncast (toRExp e) /\
615
      eval_exp_valid e E2 /\
616 617 618
      dVars_range_valid dVars E1 A /\
      fVars_P_sound fVars E1 P /\
      vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
619 620 621
      (v.
        v  domain dVars 
        vF m.
Heiko Becker's avatar
Heiko Becker committed
622
        (E2_real v = SOME vF  FloverMapTree_find (Var v) tMap = SOME m 
623
        validFloatValue vF m)) /\
Heiko Becker's avatar
Heiko Becker committed
624
      (!v. v IN domain (usedVars (toRExp e)) ==> Gamma v = SOME M64) ==>
625 626 627
      ?v.
        eval_exp_float e E2 = SOME v /\
        eval_exp (toREnv E2) Gamma (toRExp e) (float_to_real (fp64_to_float v)) M64``,
Heiko Becker's avatar
Heiko Becker committed
628
  Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
629
  \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
630
  \\ once_rewrite_tac [eval_exp_float_def]
631
  \\ fs[eval_exp_valid_def, isValid_def, noDowncast_def]
632
  >- (once_rewrite_tac [toREnv_def]
633
      \\ fs[validFloatValue_def]
Heiko Becker's avatar
Heiko Becker committed
634
      \\ rveq
635 636 637
      \\ fs[eval_exp_cases, fp64_to_float_float_to_fp64, dmode_def,
            float_to_real_real_to_float_zero_id]
      \\ fs[toREnv_def]
638 639
      \\ fs[eval_exp_float_def, optionLift_def]
      \\ Cases_on `E2 n` \\ fs[optionLift_def, normal_or_zero_def])
640
  >- (rveq \\ fs[eval_exp_cases]
641
      \\ fs[optionLift_def, normal_or_zero_def, minValue_pos_def,
Heiko Becker's avatar
Heiko Becker committed
642 643
            minExponentPos_def, REAL_LT_INV_EQ]
      \\ qexists_tac `0:real`
644
      \\ fs[mTypeToR_pos, perturb_def, fp64_to_float_float_to_fp64,
Heiko Becker's avatar
Heiko Becker committed
645
            zero_to_real])
646
  >- (fs[eval_exp_float_def, optionLift_def]
647
      \\ first_x_assum (qspecl_then [`E1`, `E2`, `E2_real`, `Gamma`, `tMap`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
648
      >- (fs[]
Heiko Becker's avatar
Heiko Becker committed
649 650 651
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
652
          \\ rveq \\ fs[]
653
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
Heiko Becker's avatar
Heiko Becker committed
654
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
655
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
656
          \\ fs[]
657
          \\ rveq
Heiko Becker's avatar
Heiko Becker committed
658 659
          \\ rw_asm_star `FloverMapTree_find (Unop _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Unop _ _) tMap = _`
Heiko Becker's avatar
Heiko Becker committed
660
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
661
      \\ fs[fp64_negate_def, fp64_to_float_float_to_fp64]
662 663 664 665
      \\ 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])
Heiko Becker's avatar
Heiko Becker committed
666
  >- (Flover_compute ``validErrorbound``
667
      \\ rveq \\ fs[])
668
  >- (rename1 `Binop b (toRExp e1) (toRExp e2)`
669
      \\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
Heiko Becker's avatar
Heiko Becker committed
670 671 672
      \\ `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`
673
          by (rpt conj_tac \\ irule typing_exp_64bit \\ fs[is64BitEval_def, noDowncast_def]
Heiko Becker's avatar
Heiko Becker committed
674
              \\ qexists_tac `Gamma` \\ fs[]
Heiko Becker's avatar
Heiko Becker committed
675
              \\ Flover_compute ``typeCheck``
676 677
              \\ rpt strip_tac \\ first_x_assum irule
              \\ simp[Once usedVars_def, domain_union])
Heiko Becker's avatar
Heiko Becker committed
678 679
      \\ `m1 = M64 /\ m2 = M64`
           by (conj_tac
Heiko Becker's avatar
Heiko Becker committed
680
               \\ Flover_compute ``typeCheck``
681
               \\ irule typing_agrees_exp
Heiko Becker's avatar
Heiko Becker committed
682 683 684 685
               \\ qexistsl_tac [`toREnv E2`, `Gamma`]
               THENL [qexists_tac `toRExp e1`, qexists_tac `toRExp e2`]
               \\ qexistsl_tac [`tMap`]
               THENL [qexists_tac `v1`, qexists_tac `v2`]
686
               \\ fs[])
687
      \\ rveq
688
      \\ ntac 2 (first_x_assum (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`, `tMap`] assume_tac))
689
      \\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct)
690
      >- (fs[]
Heiko Becker's avatar
Heiko Becker committed
691 692 693
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
694
          \\ rveq \\ fs[]
695
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
Heiko Becker's avatar
Heiko Becker committed
696
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
697
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
698
          \\ fs[]
699
          \\ rveq
Heiko Becker's avatar
Heiko Becker committed
700 701
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
702 703
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, Once usedVars_def]
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
704
      \\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct)
705
      >- (fs[]
Heiko Becker's avatar
Heiko Becker committed
706 707 708
          \\ Flover_compute ``validErrorbound``
          \\ Flover_compute ``validIntervalbounds``
          \\ Flover_compute ``typeCheck``
709
          \\ rveq \\ fs[]
710
          \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
Heiko Becker's avatar
Heiko Becker committed
711
          \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
712
          \\ rw_thm_asm `is64BitEval _` is64BitEval_def
713
          \\ fs[]
714
          \\ rveq
Heiko Becker's avatar
Heiko Becker committed
715 716
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
          \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
Heiko Becker's avatar
Heiko Becker committed
717
          \\ fs[domain_union, DIFF_DEF, SUBSET_DEF]
718 719
          \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def]
          \\ fs[domain_union])
Heiko Becker's avatar
Heiko Becker committed
720
      \\ fs[]
721
      \\ rename1 `eval_exp_float e1 _ = SOME vF1`
722
      \\ rename1 `eval_exp_float e2 _ = SOME vF2`
Heiko Becker's avatar
Heiko Becker committed
723
      \\ `?iv err nR2. FloverMapTree_find (toRExp e2) A = SOME (iv, err) /\
724
            eval_exp E1 (toRMap Gamma) (toREval (toRExp e2)) nR2 REAL /\
725
            FST iv <= nR2 /\ nR2 <= SND iv`
726 727
           by (irule validIntervalbounds_sound
               \\ qexistsl_tac [`P`, `dVars`, `fVars`]
Heiko Becker's avatar
Heiko Becker committed
728
               \\ Flover_compute ``validIntervalbounds``
729 730 731
               \\ fs [DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac \\ first_x_assum irule
               \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
Heiko Becker's avatar
Heiko Becker committed
732
      \\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)`
733 734
      (* Obtain evaluation for E2_real*)
      \\ `!vF2 m2. eval_exp E2_real Gamma (toRExp e2) vF2 m2 ==>
735
            abs (nR2 - vF2) <= err2`
736
            by (qspecl_then [`toRExp e2`, `E1`, `E2_real`, `A`,`nR2`,
737 738
                             `err2`, `P`, `FST iv2`, `SND iv2`, `fVars`,
                             `dVars`, `tMap`, `Gamma`] destruct validErrorbound_sound
Heiko Becker's avatar
Heiko Becker committed
739 740 741
                \\ Flover_compute ``typeCheck``
                \\ Flover_compute ``validErrorbound``
                \\ Flover_compute ``validIntervalbounds``
742
                \\ fs[] \\ rveq \\ fs[]
743 744 745
                \\ fs [DIFF_DEF, SUBSET_DEF]
                \\ rpt strip_tac \\ first_x_assum irule
                \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
746
      \\ `contained (float_to_real (fp64_to_float vF2))
747
                    (widenInterval (FST iv2, SND iv2) err2)`
748 749 750
           by (irule distance_gives_iv
               \\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def]
               \\ first_x_assum irule
751 752 753
               \\ qexists_tac `M64`
               \\ drule eval_eq_env
               \\ rpt (disch_then drule) \\ fs[])
754
      \\ `b = Div ==> float_to_real (fp64_to_float vF2) <> 0`
755
           by (strip_tac \\ rveq
Heiko Becker's avatar
Heiko Becker committed
756
               \\ Flover_compute ``validErrorbound``
757 758
               \\ fs[IVhi_def, IVlo_def, widenInterval_def, contained_def,
                     noDivzero_def]
759 760 761
               >- (CCONTR_TAC \\ fs[] \\ rveq
                   \\ `0 < 0:real`
                        by (irule REAL_LET_TRANS
762
                            \\ qexists_tac `SND iv2 + err2` \\ fs[])
763 764 765 766
                   \\ fs[])
               \\ CCONTR_TAC \\ fs[] \\ rveq
               \\ `0 < 0:real`
                    by (irule REAL_LTE_TRANS
767
                        \\ qexists_tac `FST iv2 - err2` \\ fs[])
768
               \\ fs[])
769 770 771
      \\ `validFloatValue
            (evalBinop b (float_to_real (fp64_to_float vF1))
             (float_to_real (fp64_to_float vF2))) M64`
772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
          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])
789
      \\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
790 791 792 793 794
           by (drule FPRangeValidator_sound
               \\ disch_then
                    (qspecl_then
                       [`toRExp e1`,
                        `float_to_real (fp64_to_float vF1)`,
Heiko Becker's avatar
Heiko Becker committed
795
                         `M64`, `tMap`, `P`] irule)
796
               \\ fs[]
797
               \\ qexistsl_tac [`P`, `e1`, `tMap`] \\ fs[]
Heiko Becker's avatar
Heiko Becker committed
798 799 800
               \\ Flover_compute ``typeCheck``
               \\ Flover_compute ``validIntervalbounds``
               \\ Flover_compute ``validErrorbound``
801
               \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
802 803
               \\ rewrite_tac [CONJ_ASSOC] \\ conj_tac
               >- (fs[] \\ rveq \\ fs[]
Heiko Becker's avatar
Heiko Becker committed
804 805
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
806 807 808 809
                   \\ 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[])
810
      \\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
Heiko Becker's avatar
Heiko Becker committed
811
           by (drule FPRangeValidator_sound
812 813 814
               \\ disch_then
                    (qspecl_then
                       [`toRExp e2`,
815
                        `float_to_real (fp64_to_float vF2)`,
Heiko Becker's avatar
Heiko Becker committed
816
                         `M64`, `tMap`, `P`] irule)
817
               \\ fs[]
818
               \\ qexistsl_tac [`P`, `e2`, `tMap`] \\ fs[]
Heiko Becker's avatar
Heiko Becker committed
819 820 821
               \\ Flover_compute ``typeCheck``
               \\ Flover_compute ``validIntervalbounds``
               \\ Flover_compute ``validErrorbound``
822
               \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
823 824
               \\ rewrite_tac [CONJ_ASSOC] \\ conj_tac
               >- (fs[] \\ rveq \\ fs[]
Heiko Becker's avatar
Heiko Becker committed
825 826
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
                   \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) tMap = _`
827 828 829 830
                   \\ 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[])
831
      \\ simp[eval_exp_cases]
Heiko Becker's avatar
Heiko Becker committed
832
      (** Case distinction for operator **)
833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863
      \\ 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]
864
           \\ fs[mTypeToR_def, join_def, perturb_def])
865
      (* result = 0 *)
866 867
      >- (IMP_RES_TAC validValue_gives_float_value
          \\ fs[REAL_LNEG_UNIQ, evalBinop_def]
868
          \\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64]
869
          \\ fs[float_add_def, float_round_with_flags_def]
870
          \\ fs[join_def]
871 872
          \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                           `float_to_real (fp64_to_float vF2)`, `0:real`]
873
          \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
874 875
          \\ `2 * abs (0:real) <= ulp (:52 #11)`
                by (fs[ulp_def, ULP_def])
876
          \\ fs[float_to_real_round_zero_is_zero])
877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893
      (* 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`,
894 895 896 897 898 899 900 901
                               `(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,
902
                             GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
903 904 905 906 907
               \\ 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]
908
               \\ fs[mTypeToR_def, join_def, perturb_def])
909 910
      >- (fs[evalBinop_def]
          \\ qpat_x_assum `float_to_real (fp64_to_float _) = _` MP_TAC
911 912 913 914
          \\ 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]
915
          \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
916 917 918
          \\ 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`]
919
          \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
920 921 922 923 924
          \\ 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 *)
925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948
      >- (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,
949 950 951
                             normalTranslatedValue_implies_finiteness,
                             denormalTranslatedValue_implies_finiteness,
                             normalValue_implies_normalization,
952
                             GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
953 954 955 956 957
               \\ 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]
958
               \\ fs[mTypeToR_def, join_def, perturb_def])
959
      >- (fs[evalBinop_def, REAL_ENTIRE, fp64_mul_def, float_mul_def,
960
             GSYM float_is_zero_to_real, float_is_zero_def]
Heiko Becker's avatar
Heiko Becker committed
961 962 963 964 965
            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]
966
             \\ Cases_on `(fp64_to_float vF1).Sign  (fp64_to_float vF2).Sign`
Heiko Becker's avatar
Heiko Becker committed
967 968 969 970
             \\ `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]
971 972 973
             \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
                    `float_to_real (fp64_to_float vF2)`, `0:real`]
             \\ rveq
974
             \\ fs[GSYM float_is_zero_to_real, float_is_zero_def, join_def, mTypeToR_pos, perturb_def])
975
      (* Division *)
976 977 978 979 980 981 982 983 984 985 986 987 988 989
      >- (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])
990 991 992 993 994 995 996 997 998
             \\ 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,
999
                             GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
1000 1001 1002