Float32Model

1module Float32Model
2
3import FloatLiteralSpec
4import BinaryFloatModel
5
6-- The N7 SOFTWARE MODEL of binary32 arithmetic (Language & Testing Evolution
7-- L13, PRD 08 N7 / PRD 17 H2): add, subtract, multiply, divide and the ordered
8-- comparisons over BIT PATTERNS (naturals below 2^32), deliberately slow and
9-- exact, for the differential lane. The reference evaluator has no float; this
10-- model IS the declared expectation the native x86-64 lowering (profile
11-- x86-64-sse-scalar-strict) is compared against, next to the independent
12-- known-answer table reference/numeric/float-arith-kat.tsv.
13--
14-- Shared dependency (DIFF-001, recorded): rounding (round-to-nearest, ties to
15-- even; subnormals; overflow) is FloatLiteralSpec's specRound/specAssemble —
16-- the L12 literal converter's owner — applied to the EXACT rational result of
17-- each operation. BinaryFloatModel owns decoding, classification and the
18-- shared arithmetic; this module specializes it and owns binary32-only forms.
19--
20-- Special values follow the x86 SSE scalar rules the profile declares:
21--   - a NaN operand propagates QUIETED (bit 22 set); with two NaN operands the
22--     result is the first operand, quieted -- a signalling second operand has
23--     no priority (what addss/subss/mulss/divss do);
24--   - an invalid operation (inf - inf, 0 x inf, 0 / 0, inf / inf) produces the
25--     default NaN 0xffc00000 ("real indefinite");
26--   - signed zeros: x + (-x) = +0; (-0) + (-0) = -0; a zero product or
27--     quotient carries the XOR of the operand signs;
28--   - rounding overflow gives the signed infinity; subnormals are preserved
29--     (FTZ/DAZ clear); x / 0 for finite nonzero x is the signed infinity.
30-- Every conversion costs a few seconds on the evaluator lane (specRound's
31-- two-level bit length); the model is a specification, never a runtime.
32
33-- The binary32 operations an arithmetic program is built from, as a value.
34-- The model above is one instance (modelF32Operations).  A program written
35-- over the record says only WHICH operation is applied to WHAT, so a
36-- statement proved for every instance -- two programs build the same
37-- expression of operations -- is decided by comparing those expressions,
38-- never by computing one, and holds for the model in particular.
39family Float32Operations : Type 0
40constructor Float32OperationsValue
41field unrestricted f32OperationAdd : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))
42field unrestricted f32OperationMultiply : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))
43field unrestricted f32OperationFusedMultiplyAdd : (pi unrestricted a : Nat . (pi unrestricted b : Nat . (pi unrestricted c : Nat . Nat)))
44field unrestricted f32OperationNegate : (pi unrestricted value : Nat . Nat)
45-- the multi-function unit's approximations (MUFU), by operation number:
46-- 0 cos, 1 sin, 2 ex2, 3 lg2, 4 rcp, 5 rsq, 6 sqrt, 7 tanh -- the hardware's
47-- results are approximations, not correctly rounded, so a statement over
48-- every choice of them holds for whatever the unit computes
49field unrestricted f32OperationApproximate : (pi unrestricted operation : Nat . (pi unrestricted value : Nat . Nat))
50end-family
51
52def modelPow2Twenty2 : Nat = (binaryFloatQuietBit binary32Format)
53def modelPow2Twenty3 : Nat = (binaryFloatFractionBase binary32Format)
54def modelPow2Thirty1 : Nat = (binaryFloatSignBase binary32Format)
55def modelPow2Hundred50 : Nat = (binaryFloatDenominator binary32Format)
56def modelPow2Three00 : Nat = (binaryFloatProductDenominator binary32Format)
57def modelInfinityBits : Nat = (binaryFloatInfinityBits binary32Format)
58def modelDefaultNaN : Nat = (binaryFloatDefaultNaN binary32Format)
59
60-- Binary32 specialization of the shared exact arithmetic reference.
61-- Classification and separate add/subtract/multiply/divide have one owner.
62-- decoding
63def modelSign = (binaryFloatSign binary32Format)
64def modelExponent = (binaryFloatExponent binary32Format)
65def modelFraction = (binaryFloatFraction binary32Format)
66def modelMagnitudeBits = (binaryFloatMagnitudeBits binary32Format)
67
68-- classification (flags)
69def modelExponentAllOnes = (binaryFloatExponentAllOnes binary32Format)
70def modelIsNaN = (binaryFloatIsNaN binary32Format)
71def modelIsInfinite = (binaryFloatIsInfinite binary32Format)
72def modelIsZero = (binaryFloatIsZero binary32Format)
73def modelIsSignalling = (binaryFloatIsSignalling binary32Format)
74
75-- construction
76def modelZeroOf = (binaryFloatZeroOf binary32Format)
77def modelInfinityOf = (binaryFloatInfinityOf binary32Format)
78def modelQuiet = (binaryFloatQuiet binary32Format)
79def modelNegate = (binaryFloatNegate binary32Format)
80
81-- the NaN result of an operation with at least one NaN operand
82def modelNaNResult = (binaryFloatNaNResult binary32Format)
83
84-- the exact magnitude of a FINITE value as N / 2^150 (subnormal: 2f / 2^150;
85-- normal: (2^23 + f) x 2^e / 2^150)
86def modelScaledMagnitude = (binaryFloatScaledMagnitude binary32Format)
87
88-- round an exact signed rational sign x N/M to the format; N = 0 is the signed zero
89def modelRoundBits = (binaryFloatRoundBits binary32Format)
90
91-- the exact signed sum of two FINITE values: same signs add the magnitudes, different
92-- signs subtract the smaller from the larger and take its sign (equal magnitudes give
93-- N = 0, which modelRoundBits makes the signed zero: +0 by the sign chosen below).
94-- Until 2026-09-22 the larger-first case took sign 0, so -3.0 + 1.0 gave +2.0
95-- while 1.0 + -3.0 gave -2.0; the known-answer table had no such row.  Found by
96-- the checked learning step's fused multiply-add, which shares the rule.
97-- Exact opposite-sign cancellation must choose +0 even when the first
98-- operand is negative. Preserving that operand's sign made -2+2 disagree
99-- with native round-to-nearest arithmetic; the singleton normalized-
100-- exponential pullback exposed it. Same-sign negative zeros stay negative.
101def modelSumSigned = (binaryFloatSumSigned binary32Format)
102
103-- addition of two FINITE values: ONE rounding (the strong normalizer normalizes
104-- every branch of a select, so the rounding must sit outside the selects)
105def modelAddFinite = (binaryFloatAddFinite binary32Format)
106
107def modelF32Add = (binaryFloatAdd binary32Format)
108
109def modelF32Subtract = (binaryFloatSubtract binary32Format)
110
111def modelF32Multiply = (binaryFloatMultiply binary32Format)
112
113def modelF32Divide = (binaryFloatDivide binary32Format)
114
115-- fused multiply-add a x b + c with ONE rounding, as SM86's FFMA performs it:
116-- the exact product (scale 2^300) and the exact addend (scale 2^150, raised to
117-- 2^300) are summed as signed exact magnitudes and rounded once.  Special
118-- values: any NaN operand quiets; inf x 0 is invalid; an infinite product or
119-- addend with a finite partner gives that infinity; opposite infinities are
120-- invalid.  A zero exact sum carries the sign the sum rule gives (+0 unless
121-- both are negative zero).
122
123def modelFusedFinite =
124  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
125    (specSelect (modelAnd (modelOr (modelIsZero a) (modelIsZero b)) (modelIsZero c))
126      (modelZeroOf (modelAnd (modelXor (modelSign a) (modelSign b)) (modelSign c)))
127      (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat)
128        (modelSumSignedValues
129          (constructor ModelSigned ModelSignedOf (modelXor (modelSign a) (modelSign b))
130            (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b)))
131          (modelSignedScale
132            (constructor ModelSigned ModelSignedOf (modelSign c) (modelScaledMagnitude c))
133            modelPow2Hundred50))
134        (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Three00)))))))
135
136def modelF32FusedMultiplyAdd =
137  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
138    (specSelect (modelOr (modelIsNaN a) (modelOr (modelIsNaN b) (modelIsNaN c)))
139      (specSelect (modelIsNaN a) (modelQuiet a) (specSelect (modelIsNaN b) (modelQuiet b) (modelQuiet c)))
140      (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsZero b)) (modelAnd (modelIsZero a) (modelIsInfinite b)))
141        modelDefaultNaN
142        (specSelect (modelOr (modelIsInfinite a) (modelIsInfinite b))
143          (specSelect (modelAnd (modelIsInfinite c) (specNot (specEqual (modelXor (modelSign a) (modelSign b)) (modelSign c))))
144            modelDefaultNaN
145            (modelInfinityOf (modelXor (modelSign a) (modelSign b))))
146          (specSelect (modelIsInfinite c)
147            c
148            (modelFusedFinite a b c))))))))
149
150-- square root: NaN quieted; signed zero preserved; +inf; a negative operand is
151-- invalid. A finite value is M / 2^150 with M the scaled magnitude, so its
152-- root is sqrt(M * 2^150) / 2^150 with an integer radicand of even scale; the
153-- floor root q is exact when q*q = N, and otherwise (2q+1)/2^151 lies on the
154-- same side of every rounding boundary as the true root.
155def modelIntegerRoot =
156  (lambda unrestricted value : Nat .
157    (app
158      (nat-eliminate
159        (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)))
160        (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low))
161        (lambda unrestricted predecessor : Nat .
162          (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) .
163            (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
164              (specSelect (nat-less-than (nat-add low 1) high)
165                (specSelect (nat-less-than value (nat-multiply (nat-divide (nat-add low high) 2) (nat-divide (nat-add low high) 2)))
166                  (induction low (nat-divide (nat-add low high) 2))
167                  (induction (nat-divide (nat-add low high) 2) high))
168                low)))))
169        200)
170      zero (specPow2 (nat-add (nat-divide (specBitLength value) 2) 2))))
171def modelF32SquareRoot =
172  (lambda unrestricted a : Nat .
173    (specSelect (modelIsNaN a)
174      (modelQuiet a)
175      (specSelect (modelIsZero a)
176        a
177        (specSelect (modelSign a)
178          modelDefaultNaN
179          (specSelect (modelIsInfinite a)
180            modelInfinityBits
181            (app (lambda unrestricted n : Nat .
182              (app (lambda unrestricted q : Nat .
183                (modelRoundBits 0
184                  (specSelect (specEqual (nat-multiply q q) n) (nat-multiply 2 q) (nat-add (nat-multiply 2 q) 1))
185                  (nat-multiply 2 modelPow2Hundred50)))
186              (modelIntegerRoot n)))
187            (nat-multiply (modelScaledMagnitude a) modelPow2Hundred50)))))))
188
189-- ordered comparisons (NaN: never less, never equal; -0 = +0); an infinity's
190-- key is above every finite scaled magnitude (2^300 > 2^278)
191def modelOrderKey =
192  (lambda unrestricted bits : Nat . (specSelect (modelIsInfinite bits) modelPow2Three00 (modelScaledMagnitude bits)))
193def modelF32Less =
194  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
195    (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
196      0
197      (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
198        0
199        (specSelect (modelSign a)
200          (specSelect (modelSign b) (nat-less-than (modelOrderKey b) (modelOrderKey a)) 1)
201          (specSelect (modelSign b) 0 (nat-less-than (modelOrderKey a) (modelOrderKey b))))))))
202def modelF32EqualValue =
203  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
204    (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
205      0
206      (specSelect (modelAnd (modelIsZero a) (modelIsZero b)) 1 (specEqual a b)))))
207
208-- FMNMX: the larger (smaller) of two values; a NaN operand gives the other,
209-- two give the canonical NaN; -0 is below +0.  (What the argmax realizations
210-- use it for -- a running maximum and the smaller token of a tie -- does not
211-- depend on the zeros' order; it is ASSUMED, not yet held to a card.)
212def modelF32ExtremumNaN : Nat = 2147483647
213def modelF32Below =
214  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
215    (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
216      (modelAnd (modelSign a) (specNot (modelSign b)))
217      (modelF32Less a b))))
218def modelF32Maximum =
219  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
220    (specSelect (modelIsNaN a)
221      (specSelect (modelIsNaN b) modelF32ExtremumNaN b)
222      (specSelect (modelIsNaN b) a (specSelect (modelF32Below a b) b a)))))
223def modelF32Minimum =
224  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
225    (specSelect (modelIsNaN a)
226      (specSelect (modelIsNaN b) modelF32ExtremumNaN b)
227      (specSelect (modelIsNaN b) a (specSelect (modelF32Below a b) a b)))))
228
229-- I2FP.F32.S32: the 32-bit word read as a signed integer, rounded to binary32
230def modelF32FromSigned32 =
231  (lambda unrestricted word : Nat .
232    (specSelect (nat-less-than word modelPow2Thirty1)
233      (modelRoundBits 0 word 1)
234      (modelRoundBits 1 (nat-subtract (nat-multiply 2 modelPow2Thirty1) word) 1)))
235
236def f32ApproximateReciprocal : Nat = 4
237def f32ApproximateReciprocalSquareRoot : Nat = 5
238def f32ApproximateSquareRoot : Nat = 6
239
240-- The model's approximations: the correctly rounded reciprocal and square
241-- root (and the reciprocal of the rounded square root) -- NOT the MUFU
242-- unit's results, which are within a few units in the last place of them;
243-- the trigonometric, exponential, logarithmic and tanh approximations are
244-- not modelled (the default NaN).  A statement at the model that uses them
245-- is a statement about this choice; the checked paths state theirs for
246-- every choice.
247def modelF32Approximate =
248  (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat .
249    (specSelect (specEqual operation f32ApproximateReciprocal)
250      (modelF32Divide 1065353216 value)
251      (specSelect (specEqual operation f32ApproximateSquareRoot)
252        (modelF32SquareRoot value)
253        (specSelect (specEqual operation f32ApproximateReciprocalSquareRoot)
254          (modelF32Divide 1065353216 (modelF32SquareRoot value))
255          modelDefaultNaN)))))
256
257def modelF32Operations : (family Float32Operations) =
258  (constructor Float32Operations Float32OperationsValue modelF32Add modelF32Multiply modelF32FusedMultiplyAdd modelNegate modelF32Approximate)
259
260def f32Add =
261  (lambda unrestricted operations : (family Float32Operations) .
262    (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))) operations
263      (branch Float32OperationsValue add multiply fused negate approximate . add)))
264def f32Multiply =
265  (lambda unrestricted operations : (family Float32Operations) .
266    (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))) operations
267      (branch Float32OperationsValue add multiply fused negate approximate . multiply)))
268def f32FusedMultiplyAdd =
269  (lambda unrestricted operations : (family Float32Operations) .
270    (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted a : Nat . (pi unrestricted b : Nat . (pi unrestricted c : Nat . Nat)))) operations
271      (branch Float32OperationsValue add multiply fused negate approximate . fused)))
272def f32Negate =
273  (lambda unrestricted operations : (family Float32Operations) .
274    (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted value : Nat . Nat)) operations
275      (branch Float32OperationsValue add multiply fused negate approximate . negate)))
276
277def f32Approximate =
278  (lambda unrestricted operations : (family Float32Operations) .
279    (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted operation : Nat . (pi unrestricted value : Nat . Nat))) operations
280      (branch Float32OperationsValue add multiply fused negate approximate . approximate)))
281
282-- A value as the 32-bit word a register or memory holds, and operations
283-- whose every result is taken to a word: the arithmetic a 32-bit machine
284-- performs with them.  For the model the words change nothing (its results
285-- are bit patterns); for operations in general, this is what a machine
286-- that masks each write computes.
287def f32Word = (lambda unrestricted value : Nat . (nat-modulo value 4294967296))
288
289def f32OperationsOnWords =
290  (lambda unrestricted operations : (family Float32Operations) .
291    (constructor Float32Operations Float32OperationsValue
292      (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (f32Word (f32Add operations left right))))
293      (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (f32Word (f32Multiply operations left right))))
294      (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat . (f32Word (f32FusedMultiplyAdd operations a b c)))))
295      (lambda unrestricted value : Nat . (f32Word (f32Negate operations value)))
296      (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat . (f32Word (f32Approximate operations operation value))))))
297
298-- The binary32 operations as a 32-bit machine and the specifications use
299-- them: the model's, each result taken as the word it is.  A binary32 result
300-- IS a word, so on words these are the model's values exactly; with them the
301-- statements proved for every choice of operations hold for the model with
302-- no side condition (Proof.LinearStepCorrectForEveryShape, WarpSumCorrect,
303-- HMMATileCorrect).
304def modelF32WordOperations : (family Float32Operations) = (f32OperationsOnWords modelF32Operations)