1module Float32Model
2
3import FloatLiteralSpec
4
5-- The N7 SOFTWARE MODEL of binary32 arithmetic (Language & Testing Evolution
6-- L13, PRD 08 N7 / PRD 17 H2): add, subtract, multiply, divide and the ordered
7-- comparisons over BIT PATTERNS (naturals below 2^32), deliberately slow and
8-- exact, for the differential lane. The reference evaluator has no float; this
9-- model IS the declared expectation the native x86-64 lowering (profile
10-- x86-64-sse-scalar-strict) is compared against, next to the independent
11-- known-answer table reference/numeric/float-arith-kat.tsv.
12--
13-- Shared dependency (DIFF-001, recorded): rounding (round-to-nearest, ties to
14-- even; subnormals; overflow) is FloatLiteralSpec's specRound/specAssemble —
15-- the L12 literal converter's owner — applied to the EXACT rational result of
16-- each operation. Everything else (decoding, classification, the special-value
17-- rules) is written here.
18--
19-- Special values follow the x86 SSE scalar rules the profile declares:
20-- - a NaN operand propagates QUIETED (bit 22 set); with two NaN operands the
21-- result is the first operand, quieted -- a signalling second operand has
22-- no priority (what addss/subss/mulss/divss do);
23-- - an invalid operation (inf - inf, 0 x inf, 0 / 0, inf / inf) produces the
24-- default NaN 0xffc00000 ("real indefinite");
25-- - signed zeros: x + (-x) = +0; (-0) + (-0) = -0; a zero product or
26-- quotient carries the XOR of the operand signs;
27-- - rounding overflow gives the signed infinity; subnormals are preserved
28-- (FTZ/DAZ clear); x / 0 for finite nonzero x is the signed infinity.
29-- Every conversion costs a few seconds on the evaluator lane (specRound's
30-- two-level bit length); the model is a specification, never a runtime.
31
32-- a signed exact magnitude (sign, N) with the common denominator 2^150
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
52family ModelSigned : Type 0
53constructor ModelSignedOf
54field unrestricted modelSignedSign : Nat
55field unrestricted modelSignedMagnitude : Nat
56end-family
57
58def modelPow2Twenty2 : Nat = 4194304
59def modelPow2Twenty3 : Nat = 8388608
60def modelPow2Thirty1 : Nat = 2147483648
61def modelPow2Hundred50 : Nat = 1427247692705959881058285969449495136382746624
62def modelPow2Three00 : Nat = 2037035976334486086268445688409378161051468393665936250636140449354381299763336706183397376
63def modelInfinityBits : Nat = 2139095040
64def modelDefaultNaN : Nat = 4290772992
65
66def modelOr =
67 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a 1 b)))
68def modelAnd =
69 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a b 0)))
70def modelXor =
71 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a (specNot b) b)))
72
73-- decoding
74def modelSign = (lambda unrestricted bits : Nat . (nat-divide bits modelPow2Thirty1))
75def modelExponent = (lambda unrestricted bits : Nat . (nat-modulo (nat-divide bits modelPow2Twenty3) 256))
76def modelFraction = (lambda unrestricted bits : Nat . (nat-modulo bits modelPow2Twenty3))
77def modelMagnitudeBits = (lambda unrestricted bits : Nat . (nat-modulo bits modelPow2Thirty1))
78
79-- classification (flags)
80def modelExponentAllOnes = (lambda unrestricted bits : Nat . (specEqual (modelExponent bits) 255))
81def modelIsNaN =
82 (lambda unrestricted bits : Nat . (modelAnd (modelExponentAllOnes bits) (specNot (specIsZero (modelFraction bits)))))
83def modelIsInfinite =
84 (lambda unrestricted bits : Nat . (modelAnd (modelExponentAllOnes bits) (specIsZero (modelFraction bits))))
85def modelIsZero = (lambda unrestricted bits : Nat . (specIsZero (modelMagnitudeBits bits)))
86def modelIsSignalling =
87 (lambda unrestricted bits : Nat . (modelAnd (modelIsNaN bits) (nat-less-than (modelFraction bits) modelPow2Twenty2)))
88
89-- construction
90def modelZeroOf = (lambda unrestricted sign : Nat . (nat-multiply sign modelPow2Thirty1))
91def modelInfinityOf = (lambda unrestricted sign : Nat . (nat-add (nat-multiply sign modelPow2Thirty1) modelInfinityBits))
92def modelQuiet =
93 (lambda unrestricted bits : Nat .
94 (specSelect (nat-less-than (modelFraction bits) modelPow2Twenty2) (nat-add bits modelPow2Twenty2) bits))
95def modelNegate =
96 (lambda unrestricted bits : Nat .
97 (specSelect (modelSign bits) (nat-subtract bits modelPow2Thirty1) (nat-add bits modelPow2Thirty1)))
98
99-- the NaN result of an operation with at least one NaN operand
100def modelNaNResult =
101 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
102 (specSelect (modelIsNaN a) (modelQuiet a) (modelQuiet b))))
103
104-- the exact magnitude of a FINITE value as N / 2^150 (subnormal: 2f / 2^150;
105-- normal: (2^23 + f) x 2^e / 2^150)
106def modelScaledMagnitude =
107 (lambda unrestricted bits : Nat .
108 (specSelect (specIsZero (modelExponent bits))
109 (nat-multiply 2 (modelFraction bits))
110 (nat-multiply (nat-add modelPow2Twenty3 (modelFraction bits)) (specPow2 (modelExponent bits)))))
111
112-- round an exact signed rational sign x N/M to the format; N = 0 is the signed zero
113def modelRoundBits =
114 (lambda unrestricted sign : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
115 (specSelect (specIsZero numerator)
116 (modelZeroOf sign)
117 (eliminate SpecResult (lambda unrestricted current : (family SpecResult) . Nat)
118 (specAssemble 8 23 127 sign (specRound 23 127 numerator denominator))
119 (branch SpecBits n . n)
120 (branch SpecOverflow . (modelInfinityOf sign)))))))
121
122def modelSelectSigned =
123 (lambda unrestricted condition : Nat . (lambda unrestricted whenTrue : (family ModelSigned) . (lambda unrestricted whenFalse : (family ModelSigned) .
124 (nat-eliminate (lambda unrestricted current : Nat . (family ModelSigned)) whenFalse
125 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ModelSigned) . whenTrue)) condition))))
126
127-- the exact signed sum of two FINITE values: same signs add the magnitudes, different
128-- signs subtract the smaller from the larger and take its sign (equal magnitudes give
129-- N = 0, which modelRoundBits makes the signed zero: +0 by the sign chosen below).
130-- Until 2026-09-22 the larger-first case took sign 0, so -3.0 + 1.0 gave +2.0
131-- while 1.0 + -3.0 gave -2.0; the known-answer table had no such row. Found by
132-- the checked learning step's fused multiply-add, which shares the rule.
133-- Exact opposite-sign cancellation must choose +0 even when the first
134-- operand is negative. Preserving that operand's sign made -2+2 disagree
135-- with native round-to-nearest arithmetic; the singleton normalized-
136-- exponential pullback exposed it. Same-sign negative zeros stay negative.
137def modelSumSigned =
138 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
139 (modelSelectSigned (specEqual (modelSign a) (modelSign b))
140 (constructor ModelSigned ModelSignedOf (modelSign a) (nat-add (modelScaledMagnitude a) (modelScaledMagnitude b)))
141 (modelSelectSigned (nat-less-than (modelScaledMagnitude a) (modelScaledMagnitude b))
142 (constructor ModelSigned ModelSignedOf (modelSign b) (nat-subtract (modelScaledMagnitude b) (modelScaledMagnitude a)))
143 (constructor ModelSigned ModelSignedOf
144 (specSelect (nat-less-than (modelScaledMagnitude b) (modelScaledMagnitude a)) (modelSign a) 0)
145 (nat-subtract (modelScaledMagnitude a) (modelScaledMagnitude b)))))))
146
147-- addition of two FINITE values: ONE rounding (the strong normalizer normalizes
148-- every branch of a select, so the rounding must sit outside the selects)
149def modelAddFinite =
150 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
151 (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
152 (modelZeroOf (modelAnd (modelSign a) (modelSign b)))
153 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat) (modelSumSigned a b)
154 (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Hundred50))))))
155
156def modelF32Add =
157 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
158 (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
159 (modelNaNResult a b)
160 (specSelect (modelIsInfinite a)
161 (specSelect (modelAnd (modelIsInfinite b) (specNot (specEqual (modelSign a) (modelSign b))))
162 modelDefaultNaN
163 a)
164 (specSelect (modelIsInfinite b)
165 b
166 (modelAddFinite a b))))))
167
168def modelF32Subtract =
169 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
170 (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
171 (modelNaNResult a b)
172 (modelF32Add a (modelNegate b)))))
173
174def modelF32Multiply =
175 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
176 (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
177 (modelNaNResult a b)
178 (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsZero b)) (modelAnd (modelIsZero a) (modelIsInfinite b)))
179 modelDefaultNaN
180 (specSelect (modelOr (modelIsInfinite a) (modelIsInfinite b))
181 (modelInfinityOf (modelXor (modelSign a) (modelSign b)))
182 (specSelect (modelOr (modelIsZero a) (modelIsZero b))
183 (modelZeroOf (modelXor (modelSign a) (modelSign b)))
184 (modelRoundBits (modelXor (modelSign a) (modelSign b))
185 (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b))
186 modelPow2Three00)))))))
187
188def modelF32Divide =
189 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
190 (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
191 (modelNaNResult a b)
192 (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsInfinite b)) (modelAnd (modelIsZero a) (modelIsZero b)))
193 modelDefaultNaN
194 (specSelect (modelOr (modelIsInfinite a) (modelIsZero b))
195 (modelInfinityOf (modelXor (modelSign a) (modelSign b)))
196 (specSelect (modelOr (modelIsInfinite b) (modelIsZero a))
197 (modelZeroOf (modelXor (modelSign a) (modelSign b)))
198 (modelRoundBits (modelXor (modelSign a) (modelSign b))
199 (modelScaledMagnitude a)
200 (modelScaledMagnitude b))))))))
201
202-- fused multiply-add a x b + c with ONE rounding, as SM86's FFMA performs it:
203-- the exact product (scale 2^300) and the exact addend (scale 2^150, raised to
204-- 2^300) are summed as signed exact magnitudes and rounded once. Special
205-- values: any NaN operand quiets; inf x 0 is invalid; an infinite product or
206-- addend with a finite partner gives that infinity; opposite infinities are
207-- invalid. A zero exact sum carries the sign the sum rule gives (+0 unless
208-- both are negative zero).
209def modelSignedScale =
210 (lambda unrestricted value : (family ModelSigned) . (lambda unrestricted factor : Nat .
211 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) value
212 (branch ModelSignedOf sign magnitude .
213 (constructor ModelSigned ModelSignedOf sign (nat-multiply magnitude factor))))))
214
215def modelSumSignedValues =
216 (lambda unrestricted a : (family ModelSigned) . (lambda unrestricted b : (family ModelSigned) .
217 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) a
218 (branch ModelSignedOf signA magnitudeA .
219 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) b
220 (branch ModelSignedOf signB magnitudeB .
221 (modelSelectSigned (specEqual signA signB)
222 (constructor ModelSigned ModelSignedOf signA (nat-add magnitudeA magnitudeB))
223 (modelSelectSigned (nat-less-than magnitudeA magnitudeB)
224 (constructor ModelSigned ModelSignedOf signB (nat-subtract magnitudeB magnitudeA))
225 (constructor ModelSigned ModelSignedOf
226 (specSelect (nat-less-than magnitudeB magnitudeA) signA 0)
227 (nat-subtract magnitudeA magnitudeB))))))))))
228
229def modelFusedFinite =
230 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
231 (specSelect (modelAnd (modelOr (modelIsZero a) (modelIsZero b)) (modelIsZero c))
232 (modelZeroOf (modelAnd (modelXor (modelSign a) (modelSign b)) (modelSign c)))
233 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat)
234 (modelSumSignedValues
235 (constructor ModelSigned ModelSignedOf (modelXor (modelSign a) (modelSign b))
236 (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b)))
237 (modelSignedScale
238 (constructor ModelSigned ModelSignedOf (modelSign c) (modelScaledMagnitude c))
239 modelPow2Hundred50))
240 (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Three00)))))))
241
242def modelF32FusedMultiplyAdd =
243 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
244 (specSelect (modelOr (modelIsNaN a) (modelOr (modelIsNaN b) (modelIsNaN c)))
245 (specSelect (modelIsNaN a) (modelQuiet a) (specSelect (modelIsNaN b) (modelQuiet b) (modelQuiet c)))
246 (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsZero b)) (modelAnd (modelIsZero a) (modelIsInfinite b)))
247 modelDefaultNaN
248 (specSelect (modelOr (modelIsInfinite a) (modelIsInfinite b))
249 (specSelect (modelAnd (modelIsInfinite c) (specNot (specEqual (modelXor (modelSign a) (modelSign b)) (modelSign c))))
250 modelDefaultNaN
251 (modelInfinityOf (modelXor (modelSign a) (modelSign b))))
252 (specSelect (modelIsInfinite c)
253 c
254 (modelFusedFinite a b c))))))))
255
256-- square root: NaN quieted; signed zero preserved; +inf; a negative operand is
257-- invalid. A finite value is M / 2^150 with M the scaled magnitude, so its
258-- root is sqrt(M * 2^150) / 2^150 with an integer radicand of even scale; the
259-- floor root q is exact when q*q = N, and otherwise (2q+1)/2^151 lies on the
260-- same side of every rounding boundary as the true root.
261def modelIntegerRoot =
262 (lambda unrestricted value : Nat .
263 (app
264 (nat-eliminate
265 (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)))
266 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low))
267 (lambda unrestricted predecessor : Nat .
268 (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) .
269 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
270 (specSelect (nat-less-than (nat-add low 1) high)
271 (specSelect (nat-less-than value (nat-multiply (nat-divide (nat-add low high) 2) (nat-divide (nat-add low high) 2)))
272 (induction low (nat-divide (nat-add low high) 2))
273 (induction (nat-divide (nat-add low high) 2) high))
274 low)))))
275 200)
276 zero (specPow2 (nat-add (nat-divide (specBitLength value) 2) 2))))
277def modelF32SquareRoot =
278 (lambda unrestricted a : Nat .
279 (specSelect (modelIsNaN a)
280 (modelQuiet a)
281 (specSelect (modelIsZero a)
282 a
283 (specSelect (modelSign a)
284 modelDefaultNaN
285 (specSelect (modelIsInfinite a)
286 modelInfinityBits
287 (app (lambda unrestricted n : Nat .
288 (app (lambda unrestricted q : Nat .
289 (modelRoundBits 0
290 (specSelect (specEqual (nat-multiply q q) n) (nat-multiply 2 q) (nat-add (nat-multiply 2 q) 1))
291 (nat-multiply 2 modelPow2Hundred50)))
292 (modelIntegerRoot n)))
293 (nat-multiply (modelScaledMagnitude a) modelPow2Hundred50)))))))
294
295-- ordered comparisons (NaN: never less, never equal; -0 = +0); an infinity's
296-- key is above every finite scaled magnitude (2^300 > 2^278)
297def modelOrderKey =
298 (lambda unrestricted bits : Nat . (specSelect (modelIsInfinite bits) modelPow2Three00 (modelScaledMagnitude bits)))
299def modelF32Less =
300 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
301 (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
302 0
303 (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
304 0
305 (specSelect (modelSign a)
306 (specSelect (modelSign b) (nat-less-than (modelOrderKey b) (modelOrderKey a)) 1)
307 (specSelect (modelSign b) 0 (nat-less-than (modelOrderKey a) (modelOrderKey b))))))))
308def modelF32EqualValue =
309 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
310 (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
311 0
312 (specSelect (modelAnd (modelIsZero a) (modelIsZero b)) 1 (specEqual a b)))))
313
314-- FMNMX: the larger (smaller) of two values; a NaN operand gives the other,
315-- two give the canonical NaN; -0 is below +0. (What the argmax realizations
316-- use it for -- a running maximum and the smaller token of a tie -- does not
317-- depend on the zeros' order; it is ASSUMED, not yet held to a card.)
318def modelF32ExtremumNaN : Nat = 2147483647
319def modelF32Below =
320 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
321 (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
322 (modelAnd (modelSign a) (specNot (modelSign b)))
323 (modelF32Less a b))))
324def modelF32Maximum =
325 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
326 (specSelect (modelIsNaN a)
327 (specSelect (modelIsNaN b) modelF32ExtremumNaN b)
328 (specSelect (modelIsNaN b) a (specSelect (modelF32Below a b) b a)))))
329def modelF32Minimum =
330 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
331 (specSelect (modelIsNaN a)
332 (specSelect (modelIsNaN b) modelF32ExtremumNaN b)
333 (specSelect (modelIsNaN b) a (specSelect (modelF32Below a b) a b)))))
334
335-- I2FP.F32.S32: the 32-bit word read as a signed integer, rounded to binary32
336def modelF32FromSigned32 =
337 (lambda unrestricted word : Nat .
338 (specSelect (nat-less-than word modelPow2Thirty1)
339 (modelRoundBits 0 word 1)
340 (modelRoundBits 1 (nat-subtract (nat-multiply 2 modelPow2Thirty1) word) 1)))
341
342def f32ApproximateReciprocal : Nat = 4
343def f32ApproximateReciprocalSquareRoot : Nat = 5
344def f32ApproximateSquareRoot : Nat = 6
345
346-- The model's approximations: the correctly rounded reciprocal and square
347-- root (and the reciprocal of the rounded square root) -- NOT the MUFU
348-- unit's results, which are within a few units in the last place of them;
349-- the trigonometric, exponential, logarithmic and tanh approximations are
350-- not modelled (the default NaN). A statement at the model that uses them
351-- is a statement about this choice; the checked paths state theirs for
352-- every choice.
353def modelF32Approximate =
354 (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat .
355 (specSelect (specEqual operation f32ApproximateReciprocal)
356 (modelF32Divide 1065353216 value)
357 (specSelect (specEqual operation f32ApproximateSquareRoot)
358 (modelF32SquareRoot value)
359 (specSelect (specEqual operation f32ApproximateReciprocalSquareRoot)
360 (modelF32Divide 1065353216 (modelF32SquareRoot value))
361 modelDefaultNaN)))))
362
363def modelF32Operations : (family Float32Operations) =
364 (constructor Float32Operations Float32OperationsValue modelF32Add modelF32Multiply modelF32FusedMultiplyAdd modelNegate modelF32Approximate)
365
366def f32Add =
367 (lambda unrestricted operations : (family Float32Operations) .
368 (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))) operations
369 (branch Float32OperationsValue add multiply fused negate approximate . add)))
370def f32Multiply =
371 (lambda unrestricted operations : (family Float32Operations) .
372 (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))) operations
373 (branch Float32OperationsValue add multiply fused negate approximate . multiply)))
374def f32FusedMultiplyAdd =
375 (lambda unrestricted operations : (family Float32Operations) .
376 (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted a : Nat . (pi unrestricted b : Nat . (pi unrestricted c : Nat . Nat)))) operations
377 (branch Float32OperationsValue add multiply fused negate approximate . fused)))
378def f32Negate =
379 (lambda unrestricted operations : (family Float32Operations) .
380 (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted value : Nat . Nat)) operations
381 (branch Float32OperationsValue add multiply fused negate approximate . negate)))
382
383def f32Approximate =
384 (lambda unrestricted operations : (family Float32Operations) .
385 (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted operation : Nat . (pi unrestricted value : Nat . Nat))) operations
386 (branch Float32OperationsValue add multiply fused negate approximate . approximate)))
387
388-- A value as the 32-bit word a register or memory holds, and operations
389-- whose every result is taken to a word: the arithmetic a 32-bit machine
390-- performs with them. For the model the words change nothing (its results
391-- are bit patterns); for operations in general, this is what a machine
392-- that masks each write computes.
393def f32Word = (lambda unrestricted value : Nat . (nat-modulo value 4294967296))
394
395def f32OperationsOnWords =
396 (lambda unrestricted operations : (family Float32Operations) .
397 (constructor Float32Operations Float32OperationsValue
398 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (f32Word (f32Add operations left right))))
399 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (f32Word (f32Multiply operations left right))))
400 (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat . (f32Word (f32FusedMultiplyAdd operations a b c)))))
401 (lambda unrestricted value : Nat . (f32Word (f32Negate operations value)))
402 (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat . (f32Word (f32Approximate operations operation value))))))
403
404-- The binary32 operations as a 32-bit machine and the specifications use
405-- them: the model's, each result taken as the word it is. A binary32 result
406-- IS a word, so on words these are the model's values exactly; with them the
407-- statements proved for every choice of operations hold for the model with
408-- no side condition (Proof.LinearStepCorrectForEveryShape, WarpSumCorrect,
409-- HMMATileCorrect).
410def modelF32WordOperations : (family Float32Operations) = (f32OperationsOnWords modelF32Operations)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.