Data.Float32Bits

1module Data.Float32Bits
2
3import Data.Bytes
4import Model.Config
5import Std.Flag
6import Std.Natural
7
8-- The IEEE-754 binary32 bit pattern as four bytes (little-endian: byte3 holds
9-- the sign bit) with its sign / zero / finite predicates as Nat flags. Lifted
10-- VERBATIM out of Inference.Candidate by the R4b reroute (2026-09-09,
11-- tools/refactor/extract_contract.py, reconstruction proof): the SM86 sampling
12-- realization consumes a temperature as this pattern and the sampling-mode
13-- contract carries it, so it belongs in foundation (RFC S2 standard = numbers),
14-- next to ModelFloat64Bits. The `InferenceFloat32`/`inferenceFloat32*` names are
15-- the lifted identity — renaming is the later namespace chunk.
16-- Inference.Candidate imports this module (its comparison defs eliminate the
17-- family here) and never redeclares it. Imports only Std.Flag.
18family InferenceFloat32 : Type 0
19constructor InferenceFloat32Bits
20field unrestricted inferenceFloat32Byte0 : Byte
21field unrestricted inferenceFloat32Byte1 : Byte
22field unrestricted inferenceFloat32Byte2 : Byte
23field unrestricted inferenceFloat32Byte3 : Byte
24
25end-family
26
27def inferenceFloat32 =
28  (lambda unrestricted byte0 : Byte .
29    (lambda unrestricted byte1 : Byte .
30      (lambda unrestricted byte2 : Byte .
31        (lambda unrestricted byte3 : Byte .
32          (constructor InferenceFloat32 InferenceFloat32Bits byte0 byte1 byte2 byte3)))))
33
34def inferenceFloat32Negative =
35  (lambda unrestricted value : (family InferenceFloat32) .
36    (eliminate
37      InferenceFloat32
38      (lambda unrestricted current : (family InferenceFloat32) . Nat)
39      value
40      (branch
41        InferenceFloat32Bits
42        byte0
43        byte1
44        byte2
45        byte3
46        .
47        (inferenceFlagNot (byte-less-than byte3 (byte 128))))))
48
49def inferenceFloat32Zero =
50  (lambda unrestricted value : (family InferenceFloat32) .
51    (eliminate
52      InferenceFloat32
53      (lambda unrestricted current : (family InferenceFloat32) . Nat)
54      value
55      (branch
56        InferenceFloat32Bits
57        byte0
58        byte1
59        byte2
60        byte3
61        .
62        (inferenceFlagAnd
63          (inferenceFlagAnd
64            (inferenceFlagAnd
65              (inferenceByteEqual byte0 (byte 0))
66              (inferenceByteEqual byte1 (byte 0)))
67            (inferenceByteEqual byte2 (byte 0)))
68          (inferenceFlagOr
69            (inferenceByteEqual byte3 (byte 0))
70            (inferenceByteEqual byte3 (byte 128)))))))
71
72def inferenceFloat32Finite =
73  (lambda unrestricted value : (family InferenceFloat32) .
74    (eliminate
75      InferenceFloat32
76      (lambda unrestricted current : (family InferenceFloat32) . Nat)
77      value
78      (branch
79        InferenceFloat32Bits
80        byte0
81        byte1
82        byte2
83        byte3
84        .
85        (inferenceFlagNot
86          (inferenceFlagAnd
87            (inferenceFlagOr
88              (inferenceByteEqual byte3 (byte 127))
89              (inferenceByteEqual byte3 (byte 255)))
90            (inferenceFlagNot (byte-less-than byte2 (byte 128))))))))
91
92-- CODECS (NUM-008). InferenceFloat32 and ModelWord32 are structurally the
93-- same 4-byte record (this family's own docstring: "lifted VERBATIM ...
94-- next to ModelFloat64Bits"), but Alpha families are nominal, so the two
95-- conversions below are the only glue needed to reuse Data.Bytes' single,
96-- KAT-proven Word32 codec (evidence/language-testing/L11n-codec-owner-audit.md)
97-- for float bits -- never a second byte-assembly/decode implementation.
98def inferenceFloat32AsModelWord32 =
99  (lambda unrestricted value : (family InferenceFloat32) .
100    (eliminate
101      InferenceFloat32
102      (lambda unrestricted current : (family InferenceFloat32) . (family ModelWord32))
103      value
104      (branch InferenceFloat32Bits byte0 byte1 byte2 byte3 . (modelWord32 byte0 byte1 byte2 byte3))))
105
106def modelWord32AsInferenceFloat32 =
107  (lambda unrestricted value : (family ModelWord32) .
108    (eliminate
109      ModelWord32
110      (lambda unrestricted current : (family ModelWord32) . (family InferenceFloat32))
111      value
112      (branch ModelWord32Value byte0 byte1 byte2 byte3 . (inferenceFloat32 byte0 byte1 byte2 byte3))))
113
114-- Encode*: value -> Bytes (byte assembly; LE = byte 0 first, BE = last).
115def dataFloat32EncodeLE =
116  (lambda unrestricted value : (family InferenceFloat32) .
117    (dataBytesWord32LE (inferenceFloat32AsModelWord32 value)))
118
119def dataFloat32EncodeBE =
120  (lambda unrestricted value : (family InferenceFloat32) .
121    (dataBytesWord32BE (inferenceFloat32AsModelWord32 value)))
122
123-- Decode*Exact: canonical decode -> value only when the input is EXACTLY 4
124-- bytes (short AND trailing input rejected). Same result family as
125-- stdU32DecodeLEExact (DataBytesWord32ExactDecodeResult, carrying a
126-- ModelWord32 on success) -- callers needing an InferenceFloat32 value
127-- apply modelWord32AsInferenceFloat32 to the decoded value, the same way a
128-- caller of stdU32DecodeLEExact already gets a ModelWord32 back.
129def dataFloat32DecodeLEExact =
130  dataBytesDecodeWord32LEExact
131
132def dataFloat32DecodeBEExact =
133  dataBytesDecodeWord32BEExact
134
135-- Bounded integer ordering for already-admitted finite binary32 words.
136-- Positive encodings increase with magnitude; negative encodings reverse
137-- that order. This total order places -0 below +0, useful for extrema. It
138-- does not specify NaN comparison and is not IEEE's signed-zero equality.
139-- Unlike an exact rational reference comparator, it needs no large integers
140-- or float instruction, so both the checker and native code can execute it.
141def dataFloat32FiniteWordBelow =
142  (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
143    (let unrestricted leftSign = (nat-divide left 2147483648) in
144      (let unrestricted rightSign = (nat-divide right 2147483648) in
145        (naturalSelect (naturalEqual leftSign rightSign)
146          (naturalSelect leftSign (nat-less-than right left) (nat-less-than left right))
147          leftSign)))))
148def dataFloat32FiniteWordMaximum =
149  (lambda unrestricted left : Nat . (lambda unrestricted right : Nat .
150    (naturalSelect (dataFloat32FiniteWordBelow left right) right left)))