lift_machine_ieeeScript.sml
1Theory lift_machine_ieee
2Ancestors
3 machine_ieee lift_ieee
4Libs
5 wordsLib
6
7(* --------------------------------------------------------------------- *)
8
9Definition interval_def: interval a b = {x : real | a <= x /\ x < b}
10End
11
12val lb = UTF8.chr 0x298B
13 (* square bracket with underbar, reminiscent of the way < gets an underbar
14 to include equality *)
15val cm = UTF8.chr 0x2B1D (* square dot *)
16val rp = UTF8.chr 0x27EF (* "flattened" right parenthesis *)
17
18val _ = add_rule {
19 term_name = "interval" , fixity = Closefix,
20 pp_elements = [TOK lb, PPBlock([TM, HardSpace 1, TOK cm, BreakSpace(1,0), TM],
21 (PP.CONSISTENT, 1)), TOK rp],
22 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
23 paren_style = OnlyIfNecessary};
24
25(* I.e., [1,2) looks like ⦋1 ⬝ 2⟯ *)
26(* which is perhaps a bit gross really *)
27
28(* --------------------------------------------------------------------- *)
29
30val rule =
31 wordsLib.WORD_EVAL_RULE o
32 REWRITE_RULE
33 [normalizes_def, binary_ieeeTheory.threshold_def, realTheory.REAL_INV_1OVER,
34 GSYM (SIMP_CONV (srw_ss()) [interval_def] ``a IN interval x y``)]
35
36Theorem word_msb16[local]:
37 !a: word16. ~word_msb a = ((fp16_to_float a).Sign = 0w)
38Proof
39 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fp16_to_float_def]
40QED
41
42Theorem word_msb32[local]:
43 !a: word32. ~word_msb a = ((fp32_to_float a).Sign = 0w)
44Proof
45 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fp32_to_float_def]
46QED
47
48Theorem word_msb64[local]:
49 !a: word64. ~word_msb a = ((fp64_to_float a).Sign = 0w)
50Proof
51 srw_tac [wordsLib.WORD_BIT_EQ_ss] [fp64_to_float_def]
52QED
53
54val tac =
55 simp_tac std_ss
56 [fp16_to_real_def, fp16_isFinite_def, fp16_isZero_def, word_msb16,
57 fp16_add_def, fp16_sub_def, fp16_mul_def, fp16_div_def, fp16_sqrt_def,
58 fp16_mul_add_def, fp16_mul_sub_def, fp16_to_float_float_to_fp16,
59 fp32_to_real_def, fp32_isFinite_def, fp32_isZero_def, word_msb32,
60 fp32_add_def, fp32_sub_def, fp32_mul_def, fp32_div_def, fp32_sqrt_def,
61 fp32_mul_add_def, fp32_mul_sub_def, fp32_to_float_float_to_fp32,
62 fp64_to_real_def, fp64_isFinite_def,fp64_isZero_def, word_msb64,
63 fp64_add_def, fp64_sub_def, fp64_mul_def, fp64_div_def, fp64_sqrt_def,
64 fp64_mul_add_def, fp64_mul_sub_def, fp64_to_float_float_to_fp64,
65 float_add_relative, float_sub_relative,
66 float_mul_relative, float_div_relative,
67 float_mul_add_relative, float_mul_sub_relative, float_sqrt_relative]
68
69(* --------------------------------------------------------------------- *)
70
71Theorem fp16_float_add_relative[local]:
72 !a b.
73 fp16_isFinite a /\ fp16_isFinite b /\
74 normalizes (:10 # 5) (fp16_to_real a + fp16_to_real b) ==>
75 fp16_isFinite (fp16_add roundTiesToEven a b) /\
76 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
77 (fp16_to_real (fp16_add roundTiesToEven a b) =
78 (fp16_to_real a + fp16_to_real b) * (1 + e))
79Proof
80 tac
81QED
82
83Theorem fp16_float_sub_relative[local]:
84 !a b.
85 fp16_isFinite a /\ fp16_isFinite b /\
86 normalizes (:10 # 5) (fp16_to_real a - fp16_to_real b) ==>
87 fp16_isFinite (fp16_sub roundTiesToEven a b) /\
88 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
89 (fp16_to_real (fp16_sub roundTiesToEven a b) =
90 (fp16_to_real a - fp16_to_real b) * (1 + e))
91Proof
92 tac
93QED
94
95Theorem fp16_float_mul_relative[local]:
96 !a b.
97 fp16_isFinite a /\ fp16_isFinite b /\
98 normalizes (:10 # 5) (fp16_to_real a * fp16_to_real b) ==>
99 fp16_isFinite (fp16_mul roundTiesToEven a b) /\
100 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
101 (fp16_to_real (fp16_mul roundTiesToEven a b) =
102 (fp16_to_real a * fp16_to_real b) * (1 + e))
103Proof
104 tac
105QED
106
107Theorem fp16_float_mul_add_relative[local]:
108 !a b c.
109 fp16_isFinite a /\ fp16_isFinite b /\ fp16_isFinite c /\
110 normalizes (:10 # 5)
111 (fp16_to_real a * fp16_to_real b + fp16_to_real c) ==>
112 fp16_isFinite (fp16_mul_add roundTiesToEven a b c) /\
113 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
114 (fp16_to_real (fp16_mul_add roundTiesToEven a b c) =
115 (fp16_to_real a * fp16_to_real b +
116 fp16_to_real c) * (1 + e))
117Proof
118 tac
119QED
120
121Theorem fp16_float_mul_sub_relative[local]:
122 !a b c.
123 fp16_isFinite a /\ fp16_isFinite b /\ fp16_isFinite c /\
124 normalizes (:10 # 5)
125 (fp16_to_real a * fp16_to_real b - fp16_to_real c) ==>
126 fp16_isFinite (fp16_mul_sub roundTiesToEven a b c) /\
127 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
128 (fp16_to_real (fp16_mul_sub roundTiesToEven a b c) =
129 (fp16_to_real a * fp16_to_real b -
130 fp16_to_real c) * (1 + e))
131Proof
132 tac
133QED
134
135Theorem fp16_float_div_relative[local]:
136 !a b.
137 fp16_isFinite a /\ fp16_isFinite b /\ ~fp16_isZero b /\
138 normalizes (:10 # 5) (fp16_to_real a / fp16_to_real b) ==>
139 fp16_isFinite (fp16_div roundTiesToEven a b) /\
140 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
141 (fp16_to_real (fp16_div roundTiesToEven a b) =
142 (fp16_to_real a / fp16_to_real b) * (1 + e))
143Proof
144 tac
145QED
146
147Theorem fp16_float_sqrt_relative[local]:
148 !a.
149 fp16_isFinite a /\ (~word_msb a \/ a = INT_MINw) /\
150 normalizes (:10 # 5) (sqrt (fp16_to_real a)) ==>
151 fp16_isFinite (fp16_sqrt roundTiesToEven a) /\
152 ?e. abs e <= 1 / 2 pow (dimindex (:10) + 1) /\
153 (fp16_to_real (fp16_sqrt roundTiesToEven a) =
154 (sqrt (fp16_to_real a)) * (1 + e))
155Proof
156 tac >> gen_tac >> strip_tac >> irule float_sqrt_relative >>
157 simp[sqrtable_def] >>
158 simp[fp16_to_float_def, binary_ieeeTheory.float_minus_zero_def,
159 binary_ieeeTheory.float_negate_def, binary_ieeeTheory.float_plus_zero_def]
160QED
161
162Theorem fp16_float_add_relative =
163 rule fp16_float_add_relative
164
165Theorem fp16_float_sub_relative =
166 rule fp16_float_sub_relative
167
168Theorem fp16_float_mul_relative =
169 rule fp16_float_mul_relative
170
171Theorem fp16_float_mul_add_relative =
172 rule fp16_float_mul_add_relative
173
174Theorem fp16_float_mul_sub_relative =
175 rule fp16_float_mul_sub_relative
176
177Theorem fp16_float_div_relative =
178 rule fp16_float_div_relative
179
180Theorem fp16_float_sqrt_relative =
181 rule fp16_float_sqrt_relative
182
183(* --------------------------------------------------------------------- *)
184
185Theorem fp32_float_add_relative[local]:
186 !a b.
187 fp32_isFinite a /\ fp32_isFinite b /\
188 normalizes (:23 # 8) (fp32_to_real a + fp32_to_real b) ==>
189 fp32_isFinite (fp32_add roundTiesToEven a b) /\
190 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
191 (fp32_to_real (fp32_add roundTiesToEven a b) =
192 (fp32_to_real a + fp32_to_real b) * (1 + e))
193Proof
194 tac
195QED
196
197Theorem fp32_float_sub_relative[local]:
198 !a b.
199 fp32_isFinite a /\ fp32_isFinite b /\
200 normalizes (:23 # 8) (fp32_to_real a - fp32_to_real b) ==>
201 fp32_isFinite (fp32_sub roundTiesToEven a b) /\
202 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
203 (fp32_to_real (fp32_sub roundTiesToEven a b) =
204 (fp32_to_real a - fp32_to_real b) * (1 + e))
205Proof
206 tac
207QED
208
209Theorem fp32_float_mul_relative[local]:
210 !a b.
211 fp32_isFinite a /\ fp32_isFinite b /\
212 normalizes (:23 # 8) (fp32_to_real a * fp32_to_real b) ==>
213 fp32_isFinite (fp32_mul roundTiesToEven a b) /\
214 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
215 (fp32_to_real (fp32_mul roundTiesToEven a b) =
216 (fp32_to_real a * fp32_to_real b) * (1 + e))
217Proof
218 tac
219QED
220
221Theorem fp32_float_mul_add_relative[local]:
222 !a b c.
223 fp32_isFinite a /\ fp32_isFinite b /\ fp32_isFinite c /\
224 normalizes (:23 # 8)
225 (fp32_to_real a * fp32_to_real b + fp32_to_real c) ==>
226 fp32_isFinite (fp32_mul_add roundTiesToEven a b c) /\
227 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
228 (fp32_to_real (fp32_mul_add roundTiesToEven a b c) =
229 (fp32_to_real a * fp32_to_real b +
230 fp32_to_real c) * (1 + e))
231Proof
232 tac
233QED
234
235Theorem fp32_float_mul_sub_relative[local]:
236 !a b c.
237 fp32_isFinite a /\ fp32_isFinite b /\ fp32_isFinite c /\
238 normalizes (:23 # 8)
239 (fp32_to_real a * fp32_to_real b - fp32_to_real c) ==>
240 fp32_isFinite (fp32_mul_sub roundTiesToEven a b c) /\
241 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
242 (fp32_to_real (fp32_mul_sub roundTiesToEven a b c) =
243 (fp32_to_real a * fp32_to_real b -
244 fp32_to_real c) * (1 + e))
245Proof
246 tac
247QED
248
249Theorem fp32_float_div_relative[local]:
250 !a b.
251 fp32_isFinite a /\ fp32_isFinite b /\ ~fp32_isZero b /\
252 normalizes (:23 # 8) (fp32_to_real a / fp32_to_real b) ==>
253 fp32_isFinite (fp32_div roundTiesToEven a b) /\
254 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
255 (fp32_to_real (fp32_div roundTiesToEven a b) =
256 (fp32_to_real a / fp32_to_real b) * (1 + e))
257Proof
258 tac
259QED
260
261Theorem fp32_float_sqrt_relative[local]:
262 !a.
263 fp32_isFinite a /\ (~word_msb a \/ a = INT_MINw) /\
264 normalizes (:23 # 8) (sqrt (fp32_to_real a)) ==>
265 fp32_isFinite (fp32_sqrt roundTiesToEven a) /\
266 ?e. abs e <= 1 / 2 pow (dimindex (:23) + 1) /\
267 (fp32_to_real (fp32_sqrt roundTiesToEven a) =
268 (sqrt (fp32_to_real a)) * (1 + e))
269Proof
270 tac >> gen_tac >> strip_tac >> irule float_sqrt_relative >>
271 simp[sqrtable_def] >>
272 simp[fp32_to_float_def, binary_ieeeTheory.float_minus_zero_def,
273 binary_ieeeTheory.float_negate_def, binary_ieeeTheory.float_plus_zero_def]
274QED
275
276Theorem fp32_float_add_relative =
277 rule fp32_float_add_relative
278
279Theorem fp32_float_sub_relative =
280 rule fp32_float_sub_relative
281
282Theorem fp32_float_mul_relative =
283 rule fp32_float_mul_relative
284
285Theorem fp32_float_mul_add_relative =
286 rule fp32_float_mul_add_relative
287
288Theorem fp32_float_mul_sub_relative =
289 rule fp32_float_mul_sub_relative
290
291Theorem fp32_float_div_relative =
292 rule fp32_float_div_relative
293
294Theorem fp32_float_sqrt_relative =
295 rule fp32_float_sqrt_relative
296
297(* --------------------------------------------------------------------- *)
298
299Theorem fp64_float_add_relative[local]:
300 !a b.
301 fp64_isFinite a /\ fp64_isFinite b /\
302 normalizes (:52 # 11) (fp64_to_real a + fp64_to_real b) ==>
303 fp64_isFinite (fp64_add roundTiesToEven a b) /\
304 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
305 (fp64_to_real (fp64_add roundTiesToEven a b) =
306 (fp64_to_real a + fp64_to_real b) * (1 + e))
307Proof
308 tac
309QED
310
311Theorem fp64_float_sub_relative[local]:
312 !a b.
313 fp64_isFinite a /\ fp64_isFinite b /\
314 normalizes (:52 # 11) (fp64_to_real a - fp64_to_real b) ==>
315 fp64_isFinite (fp64_sub roundTiesToEven a b) /\
316 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
317 (fp64_to_real (fp64_sub roundTiesToEven a b) =
318 (fp64_to_real a - fp64_to_real b) * (1 + e))
319Proof
320 tac
321QED
322
323Theorem fp64_float_mul_relative[local]:
324 !a b.
325 fp64_isFinite a /\ fp64_isFinite b /\
326 normalizes (:52 # 11) (fp64_to_real a * fp64_to_real b) ==>
327 fp64_isFinite (fp64_mul roundTiesToEven a b) /\
328 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
329 (fp64_to_real (fp64_mul roundTiesToEven a b) =
330 (fp64_to_real a * fp64_to_real b) * (1 + e))
331Proof
332 tac
333QED
334
335Theorem fp64_float_mul_add_relative[local]:
336 !a b c.
337 fp64_isFinite a /\ fp64_isFinite b /\ fp64_isFinite c /\
338 normalizes (:52 # 11)
339 (fp64_to_real a * fp64_to_real b + fp64_to_real c) ==>
340 fp64_isFinite (fp64_mul_add roundTiesToEven a b c) /\
341 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
342 (fp64_to_real (fp64_mul_add roundTiesToEven a b c) =
343 (fp64_to_real a * fp64_to_real b +
344 fp64_to_real c) * (1 + e))
345Proof
346 tac
347QED
348
349Theorem fp64_float_mul_sub_relative[local]:
350 !a b c.
351 fp64_isFinite a /\ fp64_isFinite b /\ fp64_isFinite c /\
352 normalizes (:52 # 11)
353 (fp64_to_real a * fp64_to_real b - fp64_to_real c) ==>
354 fp64_isFinite (fp64_mul_sub roundTiesToEven a b c) /\
355 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
356 (fp64_to_real (fp64_mul_sub roundTiesToEven a b c) =
357 (fp64_to_real a * fp64_to_real b -
358 fp64_to_real c) * (1 + e))
359Proof
360 tac
361QED
362
363Theorem fp64_float_div_relative[local]:
364 !a b.
365 fp64_isFinite a /\ fp64_isFinite b /\ ~fp64_isZero b /\
366 normalizes (:52 # 11) (fp64_to_real a / fp64_to_real b) ==>
367 fp64_isFinite (fp64_div roundTiesToEven a b) /\
368 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
369 (fp64_to_real (fp64_div roundTiesToEven a b) =
370 (fp64_to_real a / fp64_to_real b) * (1 + e))
371Proof
372 tac
373QED
374
375Theorem fp64_float_sqrt_relative[local]:
376 !a.
377 fp64_isFinite a /\ (~word_msb a \/ a = INT_MINw) /\
378 normalizes (:52 # 11) (sqrt (fp64_to_real a)) ==>
379 fp64_isFinite (fp64_sqrt roundTiesToEven a) /\
380 ?e. abs e <= 1 / 2 pow (dimindex (:52) + 1) /\
381 (fp64_to_real (fp64_sqrt roundTiesToEven a) =
382 (sqrt (fp64_to_real a)) * (1 + e))
383Proof
384 tac >> gen_tac >> strip_tac >> irule float_sqrt_relative >>
385 simp[sqrtable_def] >>
386 simp[fp64_to_float_def, binary_ieeeTheory.float_minus_zero_def,
387 binary_ieeeTheory.float_negate_def,
388 binary_ieeeTheory.float_plus_zero_def]
389QED
390
391Theorem fp64_float_add_relative =
392 rule fp64_float_add_relative
393
394Theorem fp64_float_sub_relative =
395 rule fp64_float_sub_relative
396
397Theorem fp64_float_mul_relative =
398 rule fp64_float_mul_relative
399
400Theorem fp64_float_mul_add_relative =
401 rule fp64_float_mul_add_relative
402
403Theorem fp64_float_mul_sub_relative =
404 rule fp64_float_mul_sub_relative
405
406Theorem fp64_float_div_relative =
407 rule fp64_float_div_relative
408
409Theorem fp64_float_sqrt_relative =
410 rule fp64_float_sqrt_relative
411
412(* --------------------------------------------------------------------- *)