1open HolKernel Parse boolLib bossLib 2open machine_ieeeTheory lift_ieeeTheory wordsLib; 3 4val () = new_theory "lift_machine_ieee"; 5 6(* --------------------------------------------------------------------- *) 7 8val interval_def = Define `interval a b = {x : real | a <= x /\ x < b}` 9 10val () = ( Parse.add_infix ("..", 350, HOLgrammars.NONASSOC) 11 ; Parse.overload_on ("..", ``interval``) 12 ) 13 14(* --------------------------------------------------------------------- *) 15 16val rule = 17 wordsLib.WORD_EVAL_RULE o 18 REWRITE_RULE 19 [normalizes_def, binary_ieeeTheory.threshold_def, realTheory.REAL_INV_1OVER, 20 GSYM (SIMP_CONV (srw_ss()) [interval_def] ``a IN (x .. y)``)] 21 22val word_msb16 = Q.prove( 23 `!a: word16. ~word_msb a = ((fp16_to_float a).Sign = 0w)`, 24 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fp16_to_float_def]) 25 26val word_msb32 = Q.prove( 27 `!a: word32. ~word_msb a = ((fp32_to_float a).Sign = 0w)`, 28 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fp32_to_float_def]) 29 30val word_msb64 = Q.prove( 31 `!a: word64. ~word_msb a = ((fp64_to_float a).Sign = 0w)`, 32 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fp64_to_float_def]) 33 34val tac = 35 simp_tac std_ss 36 [fp16_to_real_def, fp16_isFinite_def, fp16_isZero_def, word_msb16, 37 fp16_add_def, fp16_sub_def, fp16_mul_def, fp16_div_def, fp16_sqrt_def, 38 fp16_mul_add_def, fp16_mul_sub_def, fp16_to_float_float_to_fp16, 39 fp32_to_real_def, fp32_isFinite_def, fp32_isZero_def, word_msb32, 40 fp32_add_def, fp32_sub_def, fp32_mul_def, fp32_div_def, fp32_sqrt_def, 41 fp32_mul_add_def, fp32_mul_sub_def, fp32_to_float_float_to_fp32, 42 fp64_to_real_def, fp64_isFinite_def,fp64_isZero_def, word_msb64, 43 fp64_add_def, fp64_sub_def, fp64_mul_def, fp64_div_def, fp64_sqrt_def, 44 fp64_mul_add_def, fp64_mul_sub_def, fp64_to_float_float_to_fp64, 45 float_add_relative, float_sub_relative, 46 float_mul_relative, float_div_relative, 47 float_mul_add_relative, float_mul_sub_relative, float_sqrt_relative] 48 49(* --------------------------------------------------------------------- *) 50 51val fp16_float_add_relative = Q.prove( 52 `!a b. 53 fp16_isFinite a /\ fp16_isFinite b /\ 54 normalizes (:10 # 5) (fp16_to_real a + fp16_to_real b) ==> 55 fp16_isFinite (fp16_add roundTiesToEven a b) /\ 56 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 57 (fp16_to_real (fp16_add roundTiesToEven a b) = 58 (fp16_to_real a + fp16_to_real b) * (1 + e))`, 59 tac 60 ) 61 62val fp16_float_sub_relative = Q.prove( 63 `!a b. 64 fp16_isFinite a /\ fp16_isFinite b /\ 65 normalizes (:10 # 5) (fp16_to_real a - fp16_to_real b) ==> 66 fp16_isFinite (fp16_sub roundTiesToEven a b) /\ 67 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 68 (fp16_to_real (fp16_sub roundTiesToEven a b) = 69 (fp16_to_real a - fp16_to_real b) * (1 + e))`, 70 tac 71 ) 72 73val fp16_float_mul_relative = Q.prove( 74 `!a b. 75 fp16_isFinite a /\ fp16_isFinite b /\ 76 normalizes (:10 # 5) (fp16_to_real a * fp16_to_real b) ==> 77 fp16_isFinite (fp16_mul roundTiesToEven a b) /\ 78 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 79 (fp16_to_real (fp16_mul roundTiesToEven a b) = 80 (fp16_to_real a * fp16_to_real b) * (1 + e))`, 81 tac 82 ) 83 84val fp16_float_mul_add_relative = Q.prove( 85 `!a b c. 86 fp16_isFinite a /\ fp16_isFinite b /\ fp16_isFinite c /\ 87 normalizes (:10 # 5) 88 (fp16_to_real a * fp16_to_real b + fp16_to_real c) ==> 89 fp16_isFinite (fp16_mul_add roundTiesToEven a b c) /\ 90 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 91 (fp16_to_real (fp16_mul_add roundTiesToEven a b c) = 92 (fp16_to_real a * fp16_to_real b + 93 fp16_to_real c) * (1 + e))`, 94 tac 95 ) 96 97val fp16_float_mul_sub_relative = Q.prove( 98 `!a b c. 99 fp16_isFinite a /\ fp16_isFinite b /\ fp16_isFinite c /\ 100 normalizes (:10 # 5) 101 (fp16_to_real a * fp16_to_real b - fp16_to_real c) ==> 102 fp16_isFinite (fp16_mul_sub roundTiesToEven a b c) /\ 103 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 104 (fp16_to_real (fp16_mul_sub roundTiesToEven a b c) = 105 (fp16_to_real a * fp16_to_real b - 106 fp16_to_real c) * (1 + e))`, 107 tac 108 ) 109 110val fp16_float_div_relative = Q.prove( 111 `!a b. 112 fp16_isFinite a /\ fp16_isFinite b /\ ~fp16_isZero b /\ 113 normalizes (:10 # 5) (fp16_to_real a / fp16_to_real b) ==> 114 fp16_isFinite (fp16_div roundTiesToEven a b) /\ 115 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 116 (fp16_to_real (fp16_div roundTiesToEven a b) = 117 (fp16_to_real a / fp16_to_real b) * (1 + e))`, 118 tac 119 ) 120 121val fp16_float_sqrt_relative = Q.prove( 122 `!a. 123 fp16_isFinite a /\ ~word_msb a /\ 124 normalizes (:10 # 5) (sqrt (fp16_to_real a)) ==> 125 fp16_isFinite (fp16_sqrt roundTiesToEven a) /\ 126 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\ 127 (fp16_to_real (fp16_sqrt roundTiesToEven a) = 128 (sqrt (fp16_to_real a)) * (1 + e))`, 129 tac 130 ) 131 132val fp16_float_add_relative = save_thm("fp16_float_add_relative", 133 rule fp16_float_add_relative) 134 135val fp16_float_sub_relative = save_thm("fp16_float_sub_relative", 136 rule fp16_float_sub_relative) 137 138val fp16_float_mul_relative = save_thm("fp16_float_mul_relative", 139 rule fp16_float_mul_relative) 140 141val fp16_float_mul_add_relative = save_thm("fp16_float_mul_add_relative", 142 rule fp16_float_mul_add_relative) 143 144val fp16_float_mul_sub_relative = save_thm("fp16_float_mul_sub_relative", 145 rule fp16_float_mul_sub_relative) 146 147val fp16_float_div_relative = save_thm("fp16_float_div_relative", 148 rule fp16_float_div_relative) 149 150val fp16_float_sqrt_relative = save_thm("fp16_float_sqrt_relative", 151 rule fp16_float_sqrt_relative) 152 153(* --------------------------------------------------------------------- *) 154 155val fp32_float_add_relative = Q.prove( 156 `!a b. 157 fp32_isFinite a /\ fp32_isFinite b /\ 158 normalizes (:23 # 8) (fp32_to_real a + fp32_to_real b) ==> 159 fp32_isFinite (fp32_add roundTiesToEven a b) /\ 160 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 161 (fp32_to_real (fp32_add roundTiesToEven a b) = 162 (fp32_to_real a + fp32_to_real b) * (1 + e))`, 163 tac 164 ) 165 166val fp32_float_sub_relative = Q.prove( 167 `!a b. 168 fp32_isFinite a /\ fp32_isFinite b /\ 169 normalizes (:23 # 8) (fp32_to_real a - fp32_to_real b) ==> 170 fp32_isFinite (fp32_sub roundTiesToEven a b) /\ 171 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 172 (fp32_to_real (fp32_sub roundTiesToEven a b) = 173 (fp32_to_real a - fp32_to_real b) * (1 + e))`, 174 tac 175 ) 176 177val fp32_float_mul_relative = Q.prove( 178 `!a b. 179 fp32_isFinite a /\ fp32_isFinite b /\ 180 normalizes (:23 # 8) (fp32_to_real a * fp32_to_real b) ==> 181 fp32_isFinite (fp32_mul roundTiesToEven a b) /\ 182 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 183 (fp32_to_real (fp32_mul roundTiesToEven a b) = 184 (fp32_to_real a * fp32_to_real b) * (1 + e))`, 185 tac 186 ) 187 188val fp32_float_mul_add_relative = Q.prove( 189 `!a b c. 190 fp32_isFinite a /\ fp32_isFinite b /\ fp32_isFinite c /\ 191 normalizes (:23 # 8) 192 (fp32_to_real a * fp32_to_real b + fp32_to_real c) ==> 193 fp32_isFinite (fp32_mul_add roundTiesToEven a b c) /\ 194 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 195 (fp32_to_real (fp32_mul_add roundTiesToEven a b c) = 196 (fp32_to_real a * fp32_to_real b + 197 fp32_to_real c) * (1 + e))`, 198 tac 199 ) 200 201val fp32_float_mul_sub_relative = Q.prove( 202 `!a b c. 203 fp32_isFinite a /\ fp32_isFinite b /\ fp32_isFinite c /\ 204 normalizes (:23 # 8) 205 (fp32_to_real a * fp32_to_real b - fp32_to_real c) ==> 206 fp32_isFinite (fp32_mul_sub roundTiesToEven a b c) /\ 207 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 208 (fp32_to_real (fp32_mul_sub roundTiesToEven a b c) = 209 (fp32_to_real a * fp32_to_real b - 210 fp32_to_real c) * (1 + e))`, 211 tac 212 ) 213 214val fp32_float_div_relative = Q.prove( 215 `!a b. 216 fp32_isFinite a /\ fp32_isFinite b /\ ~fp32_isZero b /\ 217 normalizes (:23 # 8) (fp32_to_real a / fp32_to_real b) ==> 218 fp32_isFinite (fp32_div roundTiesToEven a b) /\ 219 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 220 (fp32_to_real (fp32_div roundTiesToEven a b) = 221 (fp32_to_real a / fp32_to_real b) * (1 + e))`, 222 tac 223 ) 224 225val fp32_float_sqrt_relative = Q.prove( 226 `!a. 227 fp32_isFinite a /\ ~word_msb a /\ 228 normalizes (:23 # 8) (sqrt (fp32_to_real a)) ==> 229 fp32_isFinite (fp32_sqrt roundTiesToEven a) /\ 230 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\ 231 (fp32_to_real (fp32_sqrt roundTiesToEven a) = 232 (sqrt (fp32_to_real a)) * (1 + e))`, 233 tac 234 ) 235 236val fp32_float_add_relative = save_thm("fp32_float_add_relative", 237 rule fp32_float_add_relative) 238 239val fp32_float_sub_relative = save_thm("fp32_float_sub_relative", 240 rule fp32_float_sub_relative) 241 242val fp32_float_mul_relative = save_thm("fp32_float_mul_relative", 243 rule fp32_float_mul_relative) 244 245val fp32_float_mul_add_relative = save_thm("fp32_float_mul_add_relative", 246 rule fp32_float_mul_add_relative) 247 248val fp32_float_mul_sub_relative = save_thm("fp32_float_mul_sub_relative", 249 rule fp32_float_mul_sub_relative) 250 251val fp32_float_div_relative = save_thm("fp32_float_div_relative", 252 rule fp32_float_div_relative) 253 254val fp32_float_sqrt_relative = save_thm("fp32_float_sqrt_relative", 255 rule fp32_float_sqrt_relative) 256 257(* --------------------------------------------------------------------- *) 258 259val fp64_float_add_relative = Q.prove( 260 `!a b. 261 fp64_isFinite a /\ fp64_isFinite b /\ 262 normalizes (:52 # 11) (fp64_to_real a + fp64_to_real b) ==> 263 fp64_isFinite (fp64_add roundTiesToEven a b) /\ 264 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 265 (fp64_to_real (fp64_add roundTiesToEven a b) = 266 (fp64_to_real a + fp64_to_real b) * (1 + e))`, 267 tac 268 ) 269 270val fp64_float_sub_relative = Q.prove( 271 `!a b. 272 fp64_isFinite a /\ fp64_isFinite b /\ 273 normalizes (:52 # 11) (fp64_to_real a - fp64_to_real b) ==> 274 fp64_isFinite (fp64_sub roundTiesToEven a b) /\ 275 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 276 (fp64_to_real (fp64_sub roundTiesToEven a b) = 277 (fp64_to_real a - fp64_to_real b) * (1 + e))`, 278 tac 279 ) 280 281val fp64_float_mul_relative = Q.prove( 282 `!a b. 283 fp64_isFinite a /\ fp64_isFinite b /\ 284 normalizes (:52 # 11) (fp64_to_real a * fp64_to_real b) ==> 285 fp64_isFinite (fp64_mul roundTiesToEven a b) /\ 286 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 287 (fp64_to_real (fp64_mul roundTiesToEven a b) = 288 (fp64_to_real a * fp64_to_real b) * (1 + e))`, 289 tac 290 ) 291 292val fp64_float_mul_add_relative = Q.prove( 293 `!a b c. 294 fp64_isFinite a /\ fp64_isFinite b /\ fp64_isFinite c /\ 295 normalizes (:52 # 11) 296 (fp64_to_real a * fp64_to_real b + fp64_to_real c) ==> 297 fp64_isFinite (fp64_mul_add roundTiesToEven a b c) /\ 298 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 299 (fp64_to_real (fp64_mul_add roundTiesToEven a b c) = 300 (fp64_to_real a * fp64_to_real b + 301 fp64_to_real c) * (1 + e))`, 302 tac 303 ) 304 305val fp64_float_mul_sub_relative = Q.prove( 306 `!a b c. 307 fp64_isFinite a /\ fp64_isFinite b /\ fp64_isFinite c /\ 308 normalizes (:52 # 11) 309 (fp64_to_real a * fp64_to_real b - fp64_to_real c) ==> 310 fp64_isFinite (fp64_mul_sub roundTiesToEven a b c) /\ 311 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 312 (fp64_to_real (fp64_mul_sub roundTiesToEven a b c) = 313 (fp64_to_real a * fp64_to_real b - 314 fp64_to_real c) * (1 + e))`, 315 tac 316 ) 317 318val fp64_float_div_relative = Q.prove( 319 `!a b. 320 fp64_isFinite a /\ fp64_isFinite b /\ ~fp64_isZero b /\ 321 normalizes (:52 # 11) (fp64_to_real a / fp64_to_real b) ==> 322 fp64_isFinite (fp64_div roundTiesToEven a b) /\ 323 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 324 (fp64_to_real (fp64_div roundTiesToEven a b) = 325 (fp64_to_real a / fp64_to_real b) * (1 + e))`, 326 tac 327 ) 328 329val fp64_float_sqrt_relative = Q.prove( 330 `!a. 331 fp64_isFinite a /\ ~word_msb a /\ 332 normalizes (:52 # 11) (sqrt (fp64_to_real a)) ==> 333 fp64_isFinite (fp64_sqrt roundTiesToEven a) /\ 334 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\ 335 (fp64_to_real (fp64_sqrt roundTiesToEven a) = 336 (sqrt (fp64_to_real a)) * (1 + e))`, 337 tac 338 ) 339 340val fp64_float_add_relative = save_thm("fp64_float_add_relative", 341 rule fp64_float_add_relative) 342 343val fp64_float_sub_relative = save_thm("fp64_float_sub_relative", 344 rule fp64_float_sub_relative) 345 346val fp64_float_mul_relative = save_thm("fp64_float_mul_relative", 347 rule fp64_float_mul_relative) 348 349val fp64_float_mul_add_relative = save_thm("fp64_float_mul_add_relative", 350 rule fp64_float_mul_add_relative) 351 352val fp64_float_mul_sub_relative = save_thm("fp64_float_mul_sub_relative", 353 rule fp64_float_mul_sub_relative) 354 355val fp64_float_div_relative = save_thm("fp64_float_div_relative", 356 rule fp64_float_div_relative) 357 358val fp64_float_sqrt_relative = save_thm("fp64_float_sqrt_relative", 359 rule fp64_float_sqrt_relative) 360 361(* --------------------------------------------------------------------- *) 362 363val () = export_theory () 364