BinaryFloatModel

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))))))))