1module Std.Float
2
3-- IEEE-754 binary32 / binary64 as `Std` vocabulary over the EXISTING bit-pattern
4-- owners (Language & Testing Evolution L12a, PRD 08 N6 / NUM-002 groundwork).
5-- Owners (evidence/language-testing/L12a-float-representation-audit.md):
6-- F32 = Data.Float32Bits.InferenceFloat32 (four bytes, little-endian, byte 3
7-- carries the sign bit; foundation's binary32 home "next to
8-- ModelFloat64Bits", with sign/zero/finite predicates);
9-- F64 = Model.Parameter.ModelFloat64Bits (eight bytes, little-endian).
10-- Alpha.Numeric.AlphaFloat32 (the literal payload of the native-lowering
11-- expression graphs) is the same four bytes under another name; it is kept as
12-- the lowering carrier. RECORDED (L12a): Alpha.Numeric does not parse under the
13-- current parser (ALPHA-PARSE-APP at Numeric.alpha:159:9, outside every gate
14-- closure), so the byte conversion between the two carriers lands with the L13
15-- lowering work, not here. No arithmetic lives here (L13); this module is CONSTRUCTION,
16-- PROJECTION, CLASSIFICATION and EQUALITY at the bits level:
17-- stdF32Equal mathematical equality: NaN never equals anything (not even
18-- itself), +0 equals -0, otherwise the bits decide;
19-- stdF32BitsEqual bit-pattern equality (NaN payloads and signed zeros distinct).
20-- The explicit "bits" form of PRD 08 N3 is NOT new syntax: `(stdF32FromWord32 0x3f800000)`
21-- with the U32 literal typed by its expected type (L11s) is the form.
22-- NaN and the infinities are named constructions, never literals (N6).
23import Std.Byte
24import Std.Natural
25import Std.Foundation
26import Model.Config
27import Model.Parameter
28import Model.Word32
29import Model.Word64
30import Data.Float32Bits
31import Data.Bytes
32import Std.Word
33
34-- REG-003 leading-bit search state: the 24-bit significand shifted left so far
35-- and how many shifts were applied (0..23).
36family StdF32UnitState : Type 0
37constructor StdF32UnitStateOf
38field unrestricted stdF32UnitCurrent : (family ModelWord32)
39field unrestricted stdF32UnitShifts : Nat
40
41end-family
42
43def F32 =
44 (family InferenceFloat32)
45
46def F64 =
47 (family ModelFloat64Bits)
48
49-- F32 construction / projection
50def stdF32FromBytes =
51 inferenceFloat32
52
53def stdF32FromWord32 =
54 (lambda unrestricted word : (family ModelWord32) .
55 (eliminate
56 ModelWord32
57 (lambda unrestricted current : (family ModelWord32) . (family InferenceFloat32))
58 word
59 (branch ModelWord32Value b0 b1 b2 b3 . (inferenceFloat32 b0 b1 b2 b3))))
60
61def stdF32ToWord32 =
62 (lambda unrestricted value : (family InferenceFloat32) .
63 (eliminate
64 InferenceFloat32
65 (lambda unrestricted current : (family InferenceFloat32) . (family ModelWord32))
66 value
67 (branch
68 InferenceFloat32Bits
69 b0
70 b1
71 b2
72 b3
73 .
74 (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))))
75
76-- F32 classification (0/1 flags). The owner's predicates are reused by name.
77def stdF32IsNegative =
78 inferenceFloat32Negative
79
80def stdF32IsZero =
81 inferenceFloat32Zero
82
83def stdF32IsFinite =
84 inferenceFloat32Finite
85
86-- exponent field all ones: byte 3 low seven bits = 0x7f and byte 2 high bit set
87def stdF32ExponentAllOnes =
88 (lambda unrestricted value : (family InferenceFloat32) .
89 (eliminate
90 InferenceFloat32
91 (lambda unrestricted current : (family InferenceFloat32) . Nat)
92 value
93 (branch
94 InferenceFloat32Bits
95 b0
96 b1
97 b2
98 b3
99 .
100 (stdFlagAnd
101 (stdFlagOr (byte-equal b3 (byte 127)) (byte-equal b3 (byte 255)))
102 (stdFlagNot (byte-less-than b2 (byte 128)))))))
103
104-- fraction field nonzero: byte 2 low seven bits, byte 1, byte 0
105def stdF32FractionNonzero =
106 (lambda unrestricted value : (family InferenceFloat32) .
107 (eliminate
108 InferenceFloat32
109 (lambda unrestricted current : (family InferenceFloat32) . Nat)
110 value
111 (branch
112 InferenceFloat32Bits
113 b0
114 b1
115 b2
116 b3
117 .
118 (stdFlagOr
119 (stdFlagNot (byte-equal (byteAnd b2 (byte 127)) (byte 0)))
120 (stdFlagOr (stdFlagNot (byte-equal b1 (byte 0))) (stdFlagNot (byte-equal b0 (byte 0))))))))
121
122def stdF32IsNaN =
123 (lambda unrestricted value : (family InferenceFloat32) .
124 (stdFlagAnd (stdF32ExponentAllOnes value) (stdF32FractionNonzero value)))
125
126def stdF32IsInfinite =
127 (lambda unrestricted value : (family InferenceFloat32) .
128 (stdFlagAnd (stdF32ExponentAllOnes value) (stdFlagNot (stdF32FractionNonzero value))))
129
130-- F32 equality (N6)
131def stdF32BitsEqual =
132 (lambda unrestricted a : (family InferenceFloat32) .
133 (lambda unrestricted b : (family InferenceFloat32) .
134 (stdU32Equal (stdF32ToWord32 a) (stdF32ToWord32 b))))
135
136def stdF32Equal =
137 (lambda unrestricted a : (family InferenceFloat32) .
138 (lambda unrestricted b : (family InferenceFloat32) .
139 (stdFlagAnd
140 (stdFlagNot (stdFlagOr (stdF32IsNaN a) (stdF32IsNaN b)))
141 (stdFlagOr (stdFlagAnd (stdF32IsZero a) (stdF32IsZero b)) (stdF32BitsEqual a b)))))
142
143-- F32 named values (never literals)
144def stdF32Zero =
145 (inferenceFloat32 (byte 0) (byte 0) (byte 0) (byte 0))
146
147def stdF32NegativeZero =
148 (inferenceFloat32 (byte 0) (byte 0) (byte 0) (byte 128))
149
150def stdF32One =
151 (inferenceFloat32 (byte 0) (byte 0) (byte 128) (byte 63))
152
153def stdF32Infinity =
154 (inferenceFloat32 (byte 0) (byte 0) (byte 128) (byte 127))
155
156def stdF32NegativeInfinity =
157 (inferenceFloat32 (byte 0) (byte 0) (byte 128) (byte 255))
158
159def stdF32NaN =
160 (inferenceFloat32 (byte 0) (byte 0) (byte 192) (byte 127))
161
162-- F64 construction / projection
163-- NUM-005 integer <-> binary32 conversions. Every conversion is a named function;
164-- rounding is to nearest, ties to even (IEEE-754 roundTiesToEven); a float that is
165-- NaN or infinite, or whose rounded value does not fit, has no integer (StdNone).
166-- The arithmetic is on naturals, over the existing bit owners (the F32's Word32 and
167-- the I32's Word32), so there is no second representation of either.
168-- A natural's low 32 bits as a Word32, by compile-time division (nat-divide /
169-- nat-modulo fold on closed naturals in one step). Model.Word32's
170-- modelWord32FromNaturalTruncated is the runtime owner and counts through the
171-- value, which a 2^30-sized float bit pattern cannot afford; these conversions
172-- are compile-time arithmetic throughout, so they take this form.
173def stdFloatWord32OfNatural =
174 (lambda unrestricted value : Nat .
175 (constructor
176 ModelWord32
177 ModelWord32Value
178 (nat-to-byte (nat-modulo value 256))
179 (nat-to-byte (nat-modulo (nat-divide value 256) 256))
180 (nat-to-byte (nat-modulo (nat-divide value 65536) 256))
181 (nat-to-byte (nat-modulo (nat-divide value 16777216) 256))))
182
183-- `significand` shifted right by `shift` bits, rounded to nearest, ties to even.
184def stdFloatRoundedShift =
185 (lambda unrestricted significand : Nat .
186 (lambda unrestricted shift : Nat .
187 (nat-eliminate
188 (lambda unrestricted current : Nat . Nat)
189 significand
190 (lambda unrestricted shiftPredecessor : Nat .
191 (lambda unrestricted shiftInduction : Nat .
192 (app
193 (lambda unrestricted scale : Nat .
194 (app
195 (lambda unrestricted quotient : Nat .
196 (app
197 (lambda unrestricted remainder : Nat .
198 (app
199 (lambda unrestricted half : Nat .
200 (nat-add
201 quotient
202 (nat-eliminate
203 (lambda unrestricted current : Nat . Nat)
204 (nat-multiply (naturalEqual remainder half) (nat-modulo quotient 2))
205 (lambda unrestricted abovePredecessor : Nat .
206 (lambda unrestricted aboveInduction : Nat . 1))
207 (nat-less-than half remainder))))
208 (nat-divide scale 2)))
209 (nat-modulo significand scale)))
210 (nat-divide significand scale)))
211 (naturalPowerOfTwo shift))))
212 shift)))
213
214-- The position of the highest set bit of a positive natural below 2^33.
215def stdFloatFloorLog2 =
216 (lambda unrestricted value : Nat .
217 (nat-eliminate
218 (lambda unrestricted current : Nat . Nat)
219 zero
220 (lambda unrestricted position : Nat .
221 (lambda unrestricted count : Nat .
222 (nat-add count (naturalIsZero (nat-less-than value (naturalPowerOfTwo (succ position)))))))
223 32))
224
225-- A binary32 from its sign (0 or 1), unbiased exponent and 24-bit significand
226-- (leading bit set).
227def stdFloatF32Assemble =
228 (lambda unrestricted negative : Nat .
229 (lambda unrestricted exponent : Nat .
230 (lambda unrestricted significand : Nat .
231 (stdF32FromWord32
232 (stdFloatWord32OfNatural
233 (nat-add
234 (nat-multiply negative 2147483648)
235 (nat-add
236 (nat-multiply (nat-add exponent 127) 8388608)
237 (nat-subtract significand 8388608))))))))
238
239-- The nearest binary32 to a positive integer magnitude: exactly when it has at most
240-- 24 significant bits, otherwise its low bits rounded away (a carry to 2^24 moves
241-- the exponent).
242def stdFloatF32FromMagnitude =
243 (lambda unrestricted negative : Nat .
244 (lambda unrestricted magnitude : Nat .
245 (app
246 (lambda unrestricted exponent : Nat .
247 (nat-eliminate
248 (lambda unrestricted current : Nat . (family InferenceFloat32))
249 (app
250 (lambda unrestricted rounded : Nat .
251 (nat-eliminate
252 (lambda unrestricted current : Nat . (family InferenceFloat32))
253 (stdFloatF32Assemble negative exponent rounded)
254 (lambda unrestricted carryPredecessor : Nat .
255 (lambda unrestricted carryInduction : (family InferenceFloat32) .
256 (stdFloatF32Assemble negative (succ exponent) 8388608)))
257 (naturalEqual rounded 16777216)))
258 (stdFloatRoundedShift magnitude (nat-subtract exponent 23)))
259 (lambda unrestricted exactPredecessor : Nat .
260 (lambda unrestricted exactInduction : (family InferenceFloat32) .
261 (stdFloatF32Assemble
262 negative
263 exponent
264 (nat-multiply magnitude (naturalPowerOfTwo (nat-subtract 23 exponent))))))
265 (nat-less-than exponent 24)))
266 (stdFloatFloorLog2 magnitude))))
267
268-- An I32 as the nearest binary32 (ties to even): always defined; zero is +0.
269def stdI32ToF32 : (pi unrestricted value : (family StdI32) . (family InferenceFloat32)) =
270 (lambda unrestricted value : (family StdI32) .
271 (app
272 (lambda unrestricted bits : Nat .
273 (app
274 (lambda unrestricted negative : Nat .
275 (app
276 (lambda unrestricted magnitude : Nat .
277 (nat-eliminate
278 (lambda unrestricted current : Nat . (family InferenceFloat32))
279 stdF32Zero
280 (lambda unrestricted magnitudePredecessor : Nat .
281 (lambda unrestricted magnitudeInduction : (family InferenceFloat32) .
282 (stdFloatF32FromMagnitude negative magnitude)))
283 magnitude))
284 (nat-eliminate
285 (lambda unrestricted current : Nat . Nat)
286 bits
287 (lambda unrestricted signPredecessor : Nat .
288 (lambda unrestricted signInduction : Nat . (nat-subtract 4294967296 bits)))
289 negative)))
290 (naturalIsZero (nat-less-than bits 2147483648))))
291 (modelWord32ToNatural (stdI32ToWord value))))
292
293-- A binary32 as an I32, rounded to nearest (ties to even); NaN, the infinities
294-- and any value whose rounding lies outside [-2^31, 2^31) have none.
295def stdF32ToI32Checked :
296 (pi unrestricted value : (family InferenceFloat32) . (family StdOption (family StdI32))) =
297 (lambda unrestricted value : (family InferenceFloat32) .
298 (app
299 (lambda unrestricted bits : Nat .
300 (app
301 (lambda unrestricted biased : Nat .
302 (app
303 (lambda unrestricted negative : Nat .
304 (nat-eliminate
305 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
306 (app
307 (lambda unrestricted magnitude : Nat .
308 (nat-eliminate
309 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
310 (nat-eliminate
311 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
312 (constructor StdOption StdNone (family StdI32))
313 (lambda unrestricted fitsPredecessor : Nat .
314 (lambda unrestricted fitsInduction : (family StdOption (family StdI32)) .
315 (constructor
316 StdOption
317 StdSome
318 (family StdI32)
319 (stdI32FromWord (stdFloatWord32OfNatural magnitude)))))
320 (nat-less-than magnitude 2147483648))
321 (lambda unrestricted negativePredecessor : Nat .
322 (lambda unrestricted negativeInduction : (family StdOption (family StdI32)) .
323 (nat-eliminate
324 (lambda unrestricted current : Nat .
325 (family StdOption (family StdI32)))
326 (constructor StdOption StdNone (family StdI32))
327 (lambda unrestricted fitsPredecessor : Nat .
328 (lambda unrestricted fitsInduction : (family StdOption (family StdI32)) .
329 (constructor
330 StdOption
331 StdSome
332 (family StdI32)
333 (stdI32FromWord
334 (stdFloatWord32OfNatural (nat-subtract 4294967296 magnitude))))))
335 (nat-less-than magnitude 2147483649))))
336 negative))
337 (nat-eliminate
338 (lambda unrestricted current : Nat . Nat)
339 (stdFloatRoundedShift
340 (nat-add (nat-modulo bits 8388608) 8388608)
341 (nat-subtract 150 biased))
342 (lambda unrestricted largePredecessor : Nat .
343 (lambda unrestricted largeInduction : Nat .
344 (nat-multiply
345 (nat-add (nat-modulo bits 8388608) 8388608)
346 (naturalPowerOfTwo (nat-subtract biased 150)))))
347 (naturalIsZero (nat-less-than biased 150))))
348 (lambda unrestricted specialPredecessor : Nat .
349 (lambda unrestricted specialInduction : (family StdOption (family StdI32)) .
350 (constructor StdOption StdNone (family StdI32))))
351 (naturalEqual biased 255)))
352 (naturalIsZero (nat-less-than bits 2147483648))))
353 (nat-modulo (nat-divide bits 8388608) 256)))
354 (modelWord32ToNatural (stdF32ToWord32 value))))
355
356def stdF64FromBytes =
357 (lambda unrestricted b0 : Byte .
358 (lambda unrestricted b1 : Byte .
359 (lambda unrestricted b2 : Byte .
360 (lambda unrestricted b3 : Byte .
361 (lambda unrestricted b4 : Byte .
362 (lambda unrestricted b5 : Byte .
363 (lambda unrestricted b6 : Byte .
364 (lambda unrestricted b7 : Byte .
365 (constructor ModelFloat64Bits ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7)))))))))
366
367def stdF64FromWord64 =
368 (lambda unrestricted word : (family ModelWord64) .
369 (eliminate
370 ModelWord64
371 (lambda unrestricted current : (family ModelWord64) . (family ModelFloat64Bits))
372 word
373 (branch
374 ModelWord64Value
375 b0
376 b1
377 b2
378 b3
379 b4
380 b5
381 b6
382 b7
383 .
384 (constructor ModelFloat64Bits ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7))))
385
386def stdF64ToWord64 =
387 (lambda unrestricted value : (family ModelFloat64Bits) .
388 (eliminate
389 ModelFloat64Bits
390 (lambda unrestricted current : (family ModelFloat64Bits) . (family ModelWord64))
391 value
392 (branch
393 ModelFloat64BitsValue
394 b0
395 b1
396 b2
397 b3
398 b4
399 b5
400 b6
401 b7
402 .
403 (constructor ModelWord64 ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7))))
404
405-- F64 wire codecs (NUM-008): an F64 is eight little-endian bytes of IEEE-754
406-- binary64, so its encodings are the Data.Bytes Word64 codecs over the same
407-- bits -- no second implementation. Encode takes the F64; the exact decoders
408-- are Data.Bytes' own (exactly eight bytes, short and trailing input rejected)
409-- and answer the ModelWord64, which stdF64FromWord64 makes an F64 -- the same
410-- convention as Data.Float32Bits' F32 codecs.
411def stdF64EncodeLE =
412 (lambda unrestricted value : (family ModelFloat64Bits) .
413 (dataBytesWord64LE (stdF64ToWord64 value)))
414
415def stdF64EncodeBE =
416 (lambda unrestricted value : (family ModelFloat64Bits) .
417 (dataBytesWord64BE (stdF64ToWord64 value)))
418
419def stdF64DecodeLEExact =
420 dataBytesDecodeWord64LEExact
421
422def stdF64DecodeBEExact =
423 dataBytesDecodeWord64BEExact
424
425-- F64 classification: sign = byte 7 high bit; exponent = byte 7 low seven bits
426-- and byte 6 high four bits (eleven bits); fraction = byte 6 low four bits and
427-- bytes 5..0.
428def stdF64IsNegative =
429 (lambda unrestricted value : (family ModelFloat64Bits) .
430 (eliminate
431 ModelFloat64Bits
432 (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
433 value
434 (branch
435 ModelFloat64BitsValue
436 b0
437 b1
438 b2
439 b3
440 b4
441 b5
442 b6
443 b7
444 .
445 (stdFlagNot (byte-less-than b7 (byte 128))))))
446
447def stdF64IsZero =
448 (lambda unrestricted value : (family ModelFloat64Bits) .
449 (eliminate
450 ModelFloat64Bits
451 (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
452 value
453 (branch
454 ModelFloat64BitsValue
455 b0
456 b1
457 b2
458 b3
459 b4
460 b5
461 b6
462 b7
463 .
464 (stdFlagAnd
465 (byte-equal b0 (byte 0))
466 (stdFlagAnd
467 (byte-equal b1 (byte 0))
468 (stdFlagAnd
469 (byte-equal b2 (byte 0))
470 (stdFlagAnd
471 (byte-equal b3 (byte 0))
472 (stdFlagAnd
473 (byte-equal b4 (byte 0))
474 (stdFlagAnd
475 (byte-equal b5 (byte 0))
476 (stdFlagAnd
477 (byte-equal b6 (byte 0))
478 (stdFlagOr (byte-equal b7 (byte 0)) (byte-equal b7 (byte 128)))))))))))))
479
480def stdF64ExponentAllOnes =
481 (lambda unrestricted value : (family ModelFloat64Bits) .
482 (eliminate
483 ModelFloat64Bits
484 (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
485 value
486 (branch
487 ModelFloat64BitsValue
488 b0
489 b1
490 b2
491 b3
492 b4
493 b5
494 b6
495 b7
496 .
497 (stdFlagAnd
498 (byte-equal (byteAnd b7 (byte 127)) (byte 127))
499 (byte-equal (byteAnd b6 (byte 240)) (byte 240))))))
500
501def stdF64FractionNonzero =
502 (lambda unrestricted value : (family ModelFloat64Bits) .
503 (eliminate
504 ModelFloat64Bits
505 (lambda unrestricted current : (family ModelFloat64Bits) . Nat)
506 value
507 (branch
508 ModelFloat64BitsValue
509 b0
510 b1
511 b2
512 b3
513 b4
514 b5
515 b6
516 b7
517 .
518 (stdFlagOr
519 (stdFlagNot (byte-equal (byteAnd b6 (byte 15)) (byte 0)))
520 (stdFlagOr
521 (stdFlagNot (byte-equal b5 (byte 0)))
522 (stdFlagOr
523 (stdFlagNot (byte-equal b4 (byte 0)))
524 (stdFlagOr
525 (stdFlagNot (byte-equal b3 (byte 0)))
526 (stdFlagOr
527 (stdFlagNot (byte-equal b2 (byte 0)))
528 (stdFlagOr
529 (stdFlagNot (byte-equal b1 (byte 0)))
530 (stdFlagNot (byte-equal b0 (byte 0))))))))))))
531
532def stdF64IsFinite =
533 (lambda unrestricted value : (family ModelFloat64Bits) .
534 (stdFlagNot (stdF64ExponentAllOnes value)))
535
536def stdF64IsNaN =
537 (lambda unrestricted value : (family ModelFloat64Bits) .
538 (stdFlagAnd (stdF64ExponentAllOnes value) (stdF64FractionNonzero value)))
539
540def stdF64IsInfinite =
541 (lambda unrestricted value : (family ModelFloat64Bits) .
542 (stdFlagAnd (stdF64ExponentAllOnes value) (stdFlagNot (stdF64FractionNonzero value))))
543
544-- F64 equality (N6)
545def stdF64BitsEqual =
546 (lambda unrestricted a : (family ModelFloat64Bits) .
547 (lambda unrestricted b : (family ModelFloat64Bits) .
548 (stdU64Equal (stdF64ToWord64 a) (stdF64ToWord64 b))))
549
550def stdF64Equal =
551 (lambda unrestricted a : (family ModelFloat64Bits) .
552 (lambda unrestricted b : (family ModelFloat64Bits) .
553 (stdFlagAnd
554 (stdFlagNot (stdFlagOr (stdF64IsNaN a) (stdF64IsNaN b)))
555 (stdFlagOr (stdFlagAnd (stdF64IsZero a) (stdF64IsZero b)) (stdF64BitsEqual a b)))))
556
557-- F64 named values (never literals)
558def stdF64Zero =
559 (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0))
560
561def stdF64NegativeZero =
562 (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 128))
563
564def stdF64One =
565 (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 240) (byte 63))
566
567def stdF64Infinity =
568 (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 240) (byte 127))
569
570def stdF64NegativeInfinity =
571 (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 240) (byte 255))
572
573def stdF64NaN =
574 (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 248) (byte 127))
575
576-- REG-003 (PRD 08 N8): the uniform [0,1) contract. stdF32UnitFromWord32 w is
577-- EXACTLY (w >> 8) x 2^-24 — the 24-bit grid, so the largest input 0xFFFFFFFF
578-- gives (2^24 - 1) x 2^-24 = 1 - 2^-24 = 0x3f7fffff, never 1.0, and 0 gives +0.0.
579-- Bit assembly over U32 (no float arithmetic): m = w >> 8; if m = 0 the value is
580-- +0.0; otherwise the leading bit of m is found by shifting left until bit 23 is
581-- set (k shifts, 0..23), the exponent field is 126 - k (= 127 + (23 - k) - 24)
582-- and the fraction field is the shifted m without its leading bit. Verified on
583-- the native lane (debug/std-word-native-check.py, f32 rows) against an
584-- independent oracle: the evaluator lane runs the word shifts through unary
585-- bytes and is not a routine law here.
586def stdF32UnitLeadingBit =
587 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 128) (byte 0))
588
589def stdF32UnitStep =
590 (lambda unrestricted state : (family StdF32UnitState) .
591 (eliminate
592 StdF32UnitState
593 (lambda unrestricted current : (family StdF32UnitState) . (family StdF32UnitState))
594 state
595 (branch
596 StdF32UnitStateOf
597 current
598 shifts
599 .
600 (nat-eliminate
601 (lambda unrestricted current2 : Nat . (family StdF32UnitState))
602 (constructor StdF32UnitState StdF32UnitStateOf current shifts)
603 (lambda unrestricted predecessor : Nat .
604 (lambda unrestricted induction : (family StdF32UnitState) .
605 (constructor
606 StdF32UnitState
607 StdF32UnitStateOf
608 (stdU32ShiftLeft current (succ zero))
609 (succ shifts))))
610 (stdU32LessThan current stdF32UnitLeadingBit)))))
611
612def stdF32UnitRun =
613 (lambda unrestricted significand : (family ModelWord32) .
614 (nat-eliminate
615 (lambda unrestricted current : Nat . (family StdF32UnitState))
616 (constructor StdF32UnitState StdF32UnitStateOf significand zero)
617 (lambda unrestricted predecessor : Nat .
618 (lambda unrestricted induction : (family StdF32UnitState) . (stdF32UnitStep induction)))
619 (byte-to-nat (byte 23))))
620
621def stdF32UnitAssemble =
622 (lambda unrestricted state : (family StdF32UnitState) .
623 (eliminate
624 StdF32UnitState
625 (lambda unrestricted current : (family StdF32UnitState) . (family InferenceFloat32))
626 state
627 (branch
628 StdF32UnitStateOf
629 current
630 shifts
631 .
632 (stdF32FromWord32
633 (stdU32AddWrapping
634 (stdU32ShiftLeft
635 (constructor
636 ModelWord32
637 ModelWord32Value
638 (nat-to-byte (naturalSaturatingSubtract (byte-to-nat (byte 126)) shifts))
639 (byte 0)
640 (byte 0)
641 (byte 0))
642 (byte-to-nat (byte 23)))
643 (stdU32SubtractWrapping current stdF32UnitLeadingBit))))))
644
645def stdF32UnitFromWord32 =
646 (lambda unrestricted word : (family ModelWord32) .
647 (app
648 (lambda unrestricted significand : (family ModelWord32) .
649 (nat-eliminate
650 (lambda unrestricted current : Nat . (family InferenceFloat32))
651 (stdF32UnitAssemble (stdF32UnitRun significand))
652 (lambda unrestricted predecessor : Nat .
653 (lambda unrestricted induction : (family InferenceFloat32) . stdF32Zero))
654 (stdU32IsZero significand)))
655 (stdU32ShiftRight word (byte-to-nat (byte 8)))))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.