1module BinaryFloatModel
2
3import FloatLiteralSpec
4
5-- Exact binary floating arithmetic for the reference lane. A format owns its
6-- exponent/fraction widths, bias and rational scale. The operations round once
7-- through the maintained literal-rounding specification, preserving subnormals
8-- and signed zero. NaN selection is the reference policy (quiet first operand,
9-- negative quiet NaN for invalid operations); it is not a hardware attestation.
10-- This module is never part of a production device execution path.
11-- The admitted reference formats are binary32Format and binary64Format;
12-- new widths need their own rational-exponent bound and known-answer rows.
13family BinaryFloatFormat : Type 0
14constructor BinaryFloatFormatOf
15field unrestricted binaryFloatExponentWidth : Nat
16field unrestricted binaryFloatFractionWidth : Nat
17field unrestricted binaryFloatExponentBias : Nat
18
19end-family
20
21family ModelSigned : Type 0
22constructor ModelSignedOf
23field unrestricted modelSignedSign : Nat
24field unrestricted modelSignedMagnitude : Nat
25
26end-family
27
28def binary32Format =
29 (constructor BinaryFloatFormat BinaryFloatFormatOf 8 23 127)
30
31def binary64Format =
32 (constructor BinaryFloatFormat BinaryFloatFormatOf 11 52 1023)
33
34def binaryFloatExponentBits =
35 (lambda unrestricted format : (family BinaryFloatFormat) .
36 (eliminate
37 BinaryFloatFormat
38 (lambda unrestricted value : (family BinaryFloatFormat) . Nat)
39 format
40 (branch BinaryFloatFormatOf e f b . e)))
41
42def binaryFloatFractionBits =
43 (lambda unrestricted format : (family BinaryFloatFormat) .
44 (eliminate
45 BinaryFloatFormat
46 (lambda unrestricted value : (family BinaryFloatFormat) . Nat)
47 format
48 (branch BinaryFloatFormatOf e f b . f)))
49
50def binaryFloatBias =
51 (lambda unrestricted format : (family BinaryFloatFormat) .
52 (eliminate
53 BinaryFloatFormat
54 (lambda unrestricted value : (family BinaryFloatFormat) . Nat)
55 format
56 (branch BinaryFloatFormatOf e f b . b)))
57
58def binaryFloatFractionBase =
59 (lambda unrestricted format : (family BinaryFloatFormat) .
60 (specPow2 (binaryFloatFractionBits format)))
61
62def binaryFloatSignBase =
63 (lambda unrestricted format : (family BinaryFloatFormat) .
64 (specPow2 (nat-add (binaryFloatExponentBits format) (binaryFloatFractionBits format))))
65
66def binaryFloatExponentBase =
67 (lambda unrestricted format : (family BinaryFloatFormat) .
68 (specPow2 (binaryFloatExponentBits format)))
69
70def binaryFloatExponentMask =
71 (lambda unrestricted format : (family BinaryFloatFormat) .
72 (nat-subtract (binaryFloatExponentBase format) 1))
73
74def binaryFloatQuietBit =
75 (lambda unrestricted format : (family BinaryFloatFormat) .
76 (nat-divide (binaryFloatFractionBase format) 2))
77
78def binaryFloatInfinityBits =
79 (lambda unrestricted format : (family BinaryFloatFormat) .
80 (nat-multiply (binaryFloatExponentMask format) (binaryFloatFractionBase format)))
81
82def binaryFloatDefaultNaN =
83 (lambda unrestricted format : (family BinaryFloatFormat) .
84 (nat-add
85 (binaryFloatSignBase format)
86 (nat-add (binaryFloatInfinityBits format) (binaryFloatQuietBit format))))
87
88def binaryFloatDenominator =
89 (lambda unrestricted format : (family BinaryFloatFormat) .
90 (specPow2 (nat-add (binaryFloatBias format) (binaryFloatFractionBits format))))
91
92def binaryFloatProductDenominator =
93 (lambda unrestricted format : (family BinaryFloatFormat) .
94 (nat-multiply (binaryFloatDenominator format) (binaryFloatDenominator format)))
95
96-- A finite significand scaled to this denominator has at most fractionBits
97-- + exponentMask bits; an exact product has at most twice that. Include one
98-- complete chunk beyond integer division, before the residual bit scan.
99def binaryFloatRoundingChunks =
100 (lambda unrestricted format : (family BinaryFloatFormat) .
101 (nat-add
102 1
103 (nat-divide
104 (nat-multiply 2 (nat-add (binaryFloatFractionBits format) (binaryFloatExponentMask format)))
105 64)))
106
107-- Signed exact magnitudes are independent of any floating format.
108def modelOr =
109 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a 1 b)))
110
111def modelAnd =
112 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a b 0)))
113
114def modelXor =
115 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a (specNot b) b)))
116
117def modelSelectSigned =
118 (lambda unrestricted condition : Nat .
119 (lambda unrestricted whenTrue : (family ModelSigned) .
120 (lambda unrestricted whenFalse : (family ModelSigned) .
121 (nat-eliminate
122 (lambda unrestricted current : Nat . (family ModelSigned))
123 whenFalse
124 (lambda unrestricted predecessor : Nat .
125 (lambda unrestricted induction : (family ModelSigned) . whenTrue))
126 condition))))
127
128def modelSignedScale =
129 (lambda unrestricted value : (family ModelSigned) .
130 (lambda unrestricted factor : Nat .
131 (eliminate
132 ModelSigned
133 (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
134 value
135 (branch
136 ModelSignedOf
137 sign
138 magnitude
139 .
140 (constructor ModelSigned ModelSignedOf sign (nat-multiply magnitude factor))))))
141
142def modelSumSignedValues =
143 (lambda unrestricted a : (family ModelSigned) .
144 (lambda unrestricted b : (family ModelSigned) .
145 (eliminate
146 ModelSigned
147 (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
148 a
149 (branch
150 ModelSignedOf
151 signA
152 magnitudeA
153 .
154 (eliminate
155 ModelSigned
156 (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
157 b
158 (branch
159 ModelSignedOf
160 signB
161 magnitudeB
162 .
163 (modelSelectSigned
164 (specEqual signA signB)
165 (constructor ModelSigned ModelSignedOf signA (nat-add magnitudeA magnitudeB))
166 (modelSelectSigned
167 (nat-less-than magnitudeA magnitudeB)
168 (constructor ModelSigned ModelSignedOf signB (nat-subtract magnitudeB magnitudeA))
169 (constructor
170 ModelSigned
171 ModelSignedOf
172 (specSelect (nat-less-than magnitudeB magnitudeA) signA 0)
173 (nat-subtract magnitudeA magnitudeB))))))))))
174
175def binaryFloatSign =
176 (lambda unrestricted format : (family BinaryFloatFormat) .
177 (lambda unrestricted bits : Nat . (nat-divide bits (binaryFloatSignBase format))))
178
179def binaryFloatExponent =
180 (lambda unrestricted format : (family BinaryFloatFormat) .
181 (lambda unrestricted bits : Nat .
182 (nat-modulo
183 (nat-divide bits (binaryFloatFractionBase format))
184 (binaryFloatExponentBase format))))
185
186def binaryFloatFraction =
187 (lambda unrestricted format : (family BinaryFloatFormat) .
188 (lambda unrestricted bits : Nat . (nat-modulo bits (binaryFloatFractionBase format))))
189
190def binaryFloatMagnitudeBits =
191 (lambda unrestricted format : (family BinaryFloatFormat) .
192 (lambda unrestricted bits : Nat . (nat-modulo bits (binaryFloatSignBase format))))
193
194def binaryFloatExponentAllOnes =
195 (lambda unrestricted format : (family BinaryFloatFormat) .
196 (lambda unrestricted bits : Nat .
197 (specEqual (binaryFloatExponent format bits) (binaryFloatExponentMask format))))
198
199def binaryFloatIsNaN =
200 (lambda unrestricted format : (family BinaryFloatFormat) .
201 (lambda unrestricted bits : Nat .
202 (modelAnd
203 (binaryFloatExponentAllOnes format bits)
204 (specNot (specIsZero (binaryFloatFraction format bits))))))
205
206def binaryFloatIsInfinite =
207 (lambda unrestricted format : (family BinaryFloatFormat) .
208 (lambda unrestricted bits : Nat .
209 (modelAnd
210 (binaryFloatExponentAllOnes format bits)
211 (specIsZero (binaryFloatFraction format bits)))))
212
213def binaryFloatIsZero =
214 (lambda unrestricted format : (family BinaryFloatFormat) .
215 (lambda unrestricted bits : Nat . (specIsZero (binaryFloatMagnitudeBits format bits))))
216
217def binaryFloatIsSignalling =
218 (lambda unrestricted format : (family BinaryFloatFormat) .
219 (lambda unrestricted bits : Nat .
220 (modelAnd
221 (binaryFloatIsNaN format bits)
222 (nat-less-than (binaryFloatFraction format bits) (binaryFloatQuietBit format)))))
223
224def binaryFloatZeroOf =
225 (lambda unrestricted format : (family BinaryFloatFormat) .
226 (lambda unrestricted sign : Nat . (nat-multiply sign (binaryFloatSignBase format))))
227
228def binaryFloatInfinityOf =
229 (lambda unrestricted format : (family BinaryFloatFormat) .
230 (lambda unrestricted sign : Nat .
231 (nat-add (nat-multiply sign (binaryFloatSignBase format)) (binaryFloatInfinityBits format))))
232
233def binaryFloatQuiet =
234 (lambda unrestricted format : (family BinaryFloatFormat) .
235 (lambda unrestricted bits : Nat .
236 (specSelect
237 (nat-less-than (binaryFloatFraction format bits) (binaryFloatQuietBit format))
238 (nat-add bits (binaryFloatQuietBit format))
239 bits)))
240
241def binaryFloatNegate =
242 (lambda unrestricted format : (family BinaryFloatFormat) .
243 (lambda unrestricted bits : Nat .
244 (specSelect
245 (binaryFloatSign format bits)
246 (nat-subtract bits (binaryFloatSignBase format))
247 (nat-add bits (binaryFloatSignBase format)))))
248
249def binaryFloatNaNResult =
250 (lambda unrestricted format : (family BinaryFloatFormat) .
251 (lambda unrestricted a : Nat .
252 (lambda unrestricted b : Nat .
253 (specSelect
254 (binaryFloatIsNaN format a)
255 (binaryFloatQuiet format a)
256 (binaryFloatQuiet format b)))))
257
258def binaryFloatScaledMagnitude =
259 (lambda unrestricted format : (family BinaryFloatFormat) .
260 (lambda unrestricted bits : Nat .
261 (specSelect
262 (specIsZero (binaryFloatExponent format bits))
263 (nat-multiply 2 (binaryFloatFraction format bits))
264 (nat-multiply
265 (nat-add (binaryFloatFractionBase format) (binaryFloatFraction format bits))
266 (specPow2 (binaryFloatExponent format bits))))))
267
268def binaryFloatRoundBitsWithLimit =
269 (lambda unrestricted chunks : Nat .
270 (lambda unrestricted format : (family BinaryFloatFormat) .
271 (lambda unrestricted sign : Nat .
272 (lambda unrestricted numerator : Nat .
273 (lambda unrestricted denominator : Nat .
274 (specSelect
275 (specIsZero numerator)
276 (binaryFloatZeroOf format sign)
277 (eliminate
278 SpecResult
279 (lambda unrestricted current : (family SpecResult) . Nat)
280 (specAssemble
281 (binaryFloatExponentBits format)
282 (binaryFloatFractionBits format)
283 (binaryFloatBias format)
284 sign
285 (specRoundWithLimit
286 chunks
287 (binaryFloatFractionBits format)
288 (binaryFloatBias format)
289 numerator
290 denominator))
291 (branch SpecBits n . n)
292 (branch SpecOverflow . (binaryFloatInfinityOf format sign)))))))))
293
294def binaryFloatRoundBits =
295 (lambda unrestricted format : (family BinaryFloatFormat) .
296 (binaryFloatRoundBitsWithLimit (binaryFloatRoundingChunks format) format))
297
298def binaryFloatSumSigned =
299 (lambda unrestricted format : (family BinaryFloatFormat) .
300 (lambda unrestricted a : Nat .
301 (lambda unrestricted b : Nat .
302 (modelSelectSigned
303 (specEqual (binaryFloatSign format a) (binaryFloatSign format b))
304 (constructor
305 ModelSigned
306 ModelSignedOf
307 (binaryFloatSign format a)
308 (nat-add (binaryFloatScaledMagnitude format a) (binaryFloatScaledMagnitude format b)))
309 (modelSelectSigned
310 (nat-less-than
311 (binaryFloatScaledMagnitude format a)
312 (binaryFloatScaledMagnitude format b))
313 (constructor
314 ModelSigned
315 ModelSignedOf
316 (binaryFloatSign format b)
317 (nat-subtract
318 (binaryFloatScaledMagnitude format b)
319 (binaryFloatScaledMagnitude format a)))
320 (constructor
321 ModelSigned
322 ModelSignedOf
323 (specSelect
324 (nat-less-than
325 (binaryFloatScaledMagnitude format b)
326 (binaryFloatScaledMagnitude format a))
327 (binaryFloatSign format a)
328 0)
329 (nat-subtract
330 (binaryFloatScaledMagnitude format a)
331 (binaryFloatScaledMagnitude format b))))))))
332
333def binaryFloatAddFinite =
334 (lambda unrestricted format : (family BinaryFloatFormat) .
335 (lambda unrestricted a : Nat .
336 (lambda unrestricted b : Nat .
337 (specSelect
338 (modelAnd (binaryFloatIsZero format a) (binaryFloatIsZero format b))
339 (binaryFloatZeroOf
340 format
341 (modelAnd (binaryFloatSign format a) (binaryFloatSign format b)))
342 (eliminate
343 ModelSigned
344 (lambda unrestricted current : (family ModelSigned) . Nat)
345 (binaryFloatSumSigned format a b)
346 (branch
347 ModelSignedOf
348 sign
349 magnitude
350 .
351 (binaryFloatRoundBits format sign magnitude (binaryFloatDenominator format))))))))
352
353def binaryFloatAdd =
354 (lambda unrestricted format : (family BinaryFloatFormat) .
355 (lambda unrestricted a : Nat .
356 (lambda unrestricted b : Nat .
357 (specSelect
358 (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
359 (binaryFloatNaNResult format a b)
360 (specSelect
361 (binaryFloatIsInfinite format a)
362 (specSelect
363 (modelAnd
364 (binaryFloatIsInfinite format b)
365 (specNot (specEqual (binaryFloatSign format a) (binaryFloatSign format b))))
366 (binaryFloatDefaultNaN format)
367 a)
368 (specSelect (binaryFloatIsInfinite format b) b (binaryFloatAddFinite format a b)))))))
369
370def binaryFloatSubtract =
371 (lambda unrestricted format : (family BinaryFloatFormat) .
372 (lambda unrestricted a : Nat .
373 (lambda unrestricted b : Nat .
374 (specSelect
375 (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
376 (binaryFloatNaNResult format a b)
377 (binaryFloatAdd format a (binaryFloatNegate format b))))))
378
379def binaryFloatMultiply =
380 (lambda unrestricted format : (family BinaryFloatFormat) .
381 (lambda unrestricted a : Nat .
382 (lambda unrestricted b : Nat .
383 (specSelect
384 (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
385 (binaryFloatNaNResult format a b)
386 (specSelect
387 (modelOr
388 (modelAnd (binaryFloatIsInfinite format a) (binaryFloatIsZero format b))
389 (modelAnd (binaryFloatIsZero format a) (binaryFloatIsInfinite format b)))
390 (binaryFloatDefaultNaN format)
391 (specSelect
392 (modelOr (binaryFloatIsInfinite format a) (binaryFloatIsInfinite format b))
393 (binaryFloatInfinityOf
394 format
395 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
396 (specSelect
397 (modelOr (binaryFloatIsZero format a) (binaryFloatIsZero format b))
398 (binaryFloatZeroOf
399 format
400 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
401 (binaryFloatRoundBits
402 format
403 (modelXor (binaryFloatSign format a) (binaryFloatSign format b))
404 (nat-multiply
405 (binaryFloatScaledMagnitude format a)
406 (binaryFloatScaledMagnitude format b))
407 (binaryFloatProductDenominator format)))))))))
408
409def binaryFloatDivide =
410 (lambda unrestricted format : (family BinaryFloatFormat) .
411 (lambda unrestricted a : Nat .
412 (lambda unrestricted b : Nat .
413 (specSelect
414 (modelOr (binaryFloatIsNaN format a) (binaryFloatIsNaN format b))
415 (binaryFloatNaNResult format a b)
416 (specSelect
417 (modelOr
418 (modelAnd (binaryFloatIsInfinite format a) (binaryFloatIsInfinite format b))
419 (modelAnd (binaryFloatIsZero format a) (binaryFloatIsZero format b)))
420 (binaryFloatDefaultNaN format)
421 (specSelect
422 (modelOr (binaryFloatIsInfinite format a) (binaryFloatIsZero format b))
423 (binaryFloatInfinityOf
424 format
425 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
426 (specSelect
427 (modelOr (binaryFloatIsInfinite format b) (binaryFloatIsZero format a))
428 (binaryFloatZeroOf
429 format
430 (modelXor (binaryFloatSign format a) (binaryFloatSign format b)))
431 (binaryFloatRoundBits
432 format
433 (modelXor (binaryFloatSign format a) (binaryFloatSign format b))
434 (binaryFloatScaledMagnitude format a)
435 (binaryFloatScaledMagnitude format b)))))))))
436
437-- Conversion rounds the exact source rational once. Its scan bound comes from
438-- the SOURCE width: using the destination's binary32 bound for a binary64
439-- numerator silently loses large exponents. NaN payload mapping is a reference
440-- policy; finite device conversion must be qualified separately on silicon.
441def binaryFloatConvert =
442 (lambda unrestricted source : (family BinaryFloatFormat) .
443 (lambda unrestricted destination : (family BinaryFloatFormat) .
444 (lambda unrestricted bits : Nat .
445 (let unrestricted sign =
446 (binaryFloatSign source bits)
447 in
448 (specSelect
449 (binaryFloatIsNaN source bits)
450 (binaryFloatQuiet
451 destination
452 (nat-add
453 (binaryFloatInfinityOf destination sign)
454 (nat-divide
455 (nat-multiply
456 (binaryFloatFraction source bits)
457 (binaryFloatFractionBase destination))
458 (binaryFloatFractionBase source))))
459 (specSelect
460 (binaryFloatIsInfinite source bits)
461 (binaryFloatInfinityOf destination sign)
462 (binaryFloatRoundBitsWithLimit
463 (binaryFloatRoundingChunks source)
464 destination
465 sign
466 (binaryFloatScaledMagnitude source bits)
467 (binaryFloatDenominator source))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.