module Float32Model import FloatLiteralSpec -- The N7 SOFTWARE MODEL of binary32 arithmetic (Language & Testing Evolution -- L13, PRD 08 N7 / PRD 17 H2): add, subtract, multiply, divide and the ordered -- comparisons over BIT PATTERNS (naturals below 2^32), deliberately slow and -- exact, for the differential lane. The reference evaluator has no float; this -- model IS the declared expectation the native x86-64 lowering (profile -- x86-64-sse-scalar-strict) is compared against, next to the independent -- known-answer table reference/numeric/float-arith-kat.tsv. -- -- Shared dependency (DIFF-001, recorded): rounding (round-to-nearest, ties to -- even; subnormals; overflow) is FloatLiteralSpec's specRound/specAssemble — -- the L12 literal converter's owner — applied to the EXACT rational result of -- each operation. Everything else (decoding, classification, the special-value -- rules) is written here. -- -- Special values follow the x86 SSE scalar rules the profile declares: -- - a NaN operand propagates QUIETED (bit 22 set); with two NaN operands the -- result is the first operand, quieted -- a signalling second operand has -- no priority (what addss/subss/mulss/divss do); -- - an invalid operation (inf - inf, 0 x inf, 0 / 0, inf / inf) produces the -- default NaN 0xffc00000 ("real indefinite"); -- - signed zeros: x + (-x) = +0; (-0) + (-0) = -0; a zero product or -- quotient carries the XOR of the operand signs; -- - rounding overflow gives the signed infinity; subnormals are preserved -- (FTZ/DAZ clear); x / 0 for finite nonzero x is the signed infinity. -- Every conversion costs a few seconds on the evaluator lane (specRound's -- two-level bit length); the model is a specification, never a runtime. -- a signed exact magnitude (sign, N) with the common denominator 2^150 -- The binary32 operations an arithmetic program is built from, as a value. -- The model above is one instance (modelF32Operations). A program written -- over the record says only WHICH operation is applied to WHAT, so a -- statement proved for every instance -- two programs build the same -- expression of operations -- is decided by comparing those expressions, -- never by computing one, and holds for the model in particular. family Float32Operations : Type 0 constructor Float32OperationsValue field unrestricted f32OperationAdd : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat)) field unrestricted f32OperationMultiply : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat)) field unrestricted f32OperationFusedMultiplyAdd : (pi unrestricted a : Nat . (pi unrestricted b : Nat . (pi unrestricted c : Nat . Nat))) field unrestricted f32OperationNegate : (pi unrestricted value : Nat . Nat) -- the multi-function unit's approximations (MUFU), by operation number: -- 0 cos, 1 sin, 2 ex2, 3 lg2, 4 rcp, 5 rsq, 6 sqrt, 7 tanh -- the hardware's -- results are approximations, not correctly rounded, so a statement over -- every choice of them holds for whatever the unit computes field unrestricted f32OperationApproximate : (pi unrestricted operation : Nat . (pi unrestricted value : Nat . Nat)) end-family family ModelSigned : Type 0 constructor ModelSignedOf field unrestricted modelSignedSign : Nat field unrestricted modelSignedMagnitude : Nat end-family def modelPow2Twenty2 : Nat = 4194304 def modelPow2Twenty3 : Nat = 8388608 def modelPow2Thirty1 : Nat = 2147483648 def modelPow2Hundred50 : Nat = 1427247692705959881058285969449495136382746624 def modelPow2Three00 : Nat = 2037035976334486086268445688409378161051468393665936250636140449354381299763336706183397376 def modelInfinityBits : Nat = 2139095040 def modelDefaultNaN : Nat = 4290772992 def modelOr = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a 1 b))) def modelAnd = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a b 0))) def modelXor = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect a (specNot b) b))) -- decoding def modelSign = (lambda unrestricted bits : Nat . (nat-divide bits modelPow2Thirty1)) def modelExponent = (lambda unrestricted bits : Nat . (nat-modulo (nat-divide bits modelPow2Twenty3) 256)) def modelFraction = (lambda unrestricted bits : Nat . (nat-modulo bits modelPow2Twenty3)) def modelMagnitudeBits = (lambda unrestricted bits : Nat . (nat-modulo bits modelPow2Thirty1)) -- classification (flags) def modelExponentAllOnes = (lambda unrestricted bits : Nat . (specEqual (modelExponent bits) 255)) def modelIsNaN = (lambda unrestricted bits : Nat . (modelAnd (modelExponentAllOnes bits) (specNot (specIsZero (modelFraction bits))))) def modelIsInfinite = (lambda unrestricted bits : Nat . (modelAnd (modelExponentAllOnes bits) (specIsZero (modelFraction bits)))) def modelIsZero = (lambda unrestricted bits : Nat . (specIsZero (modelMagnitudeBits bits))) def modelIsSignalling = (lambda unrestricted bits : Nat . (modelAnd (modelIsNaN bits) (nat-less-than (modelFraction bits) modelPow2Twenty2))) -- construction def modelZeroOf = (lambda unrestricted sign : Nat . (nat-multiply sign modelPow2Thirty1)) def modelInfinityOf = (lambda unrestricted sign : Nat . (nat-add (nat-multiply sign modelPow2Thirty1) modelInfinityBits)) def modelQuiet = (lambda unrestricted bits : Nat . (specSelect (nat-less-than (modelFraction bits) modelPow2Twenty2) (nat-add bits modelPow2Twenty2) bits)) def modelNegate = (lambda unrestricted bits : Nat . (specSelect (modelSign bits) (nat-subtract bits modelPow2Thirty1) (nat-add bits modelPow2Thirty1))) -- the NaN result of an operation with at least one NaN operand def modelNaNResult = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelIsNaN a) (modelQuiet a) (modelQuiet b)))) -- the exact magnitude of a FINITE value as N / 2^150 (subnormal: 2f / 2^150; -- normal: (2^23 + f) x 2^e / 2^150) def modelScaledMagnitude = (lambda unrestricted bits : Nat . (specSelect (specIsZero (modelExponent bits)) (nat-multiply 2 (modelFraction bits)) (nat-multiply (nat-add modelPow2Twenty3 (modelFraction bits)) (specPow2 (modelExponent bits))))) -- round an exact signed rational sign x N/M to the format; N = 0 is the signed zero def modelRoundBits = (lambda unrestricted sign : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (specSelect (specIsZero numerator) (modelZeroOf sign) (eliminate SpecResult (lambda unrestricted current : (family SpecResult) . Nat) (specAssemble 8 23 127 sign (specRound 23 127 numerator denominator)) (branch SpecBits n . n) (branch SpecOverflow . (modelInfinityOf sign))))))) def modelSelectSigned = (lambda unrestricted condition : Nat . (lambda unrestricted whenTrue : (family ModelSigned) . (lambda unrestricted whenFalse : (family ModelSigned) . (nat-eliminate (lambda unrestricted current : Nat . (family ModelSigned)) whenFalse (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ModelSigned) . whenTrue)) condition)))) -- the exact signed sum of two FINITE values: same signs add the magnitudes, different -- signs subtract the smaller from the larger and take its sign (equal magnitudes give -- N = 0, which modelRoundBits makes the signed zero: +0 by the sign chosen below). -- Until 2026-09-22 the larger-first case took sign 0, so -3.0 + 1.0 gave +2.0 -- while 1.0 + -3.0 gave -2.0; the known-answer table had no such row. Found by -- the checked learning step's fused multiply-add, which shares the rule. -- Exact opposite-sign cancellation must choose +0 even when the first -- operand is negative. Preserving that operand's sign made -2+2 disagree -- with native round-to-nearest arithmetic; the singleton normalized- -- exponential pullback exposed it. Same-sign negative zeros stay negative. def modelSumSigned = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (modelSelectSigned (specEqual (modelSign a) (modelSign b)) (constructor ModelSigned ModelSignedOf (modelSign a) (nat-add (modelScaledMagnitude a) (modelScaledMagnitude b))) (modelSelectSigned (nat-less-than (modelScaledMagnitude a) (modelScaledMagnitude b)) (constructor ModelSigned ModelSignedOf (modelSign b) (nat-subtract (modelScaledMagnitude b) (modelScaledMagnitude a))) (constructor ModelSigned ModelSignedOf (specSelect (nat-less-than (modelScaledMagnitude b) (modelScaledMagnitude a)) (modelSign a) 0) (nat-subtract (modelScaledMagnitude a) (modelScaledMagnitude b))))))) -- addition of two FINITE values: ONE rounding (the strong normalizer normalizes -- every branch of a select, so the rounding must sit outside the selects) def modelAddFinite = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelAnd (modelIsZero a) (modelIsZero b)) (modelZeroOf (modelAnd (modelSign a) (modelSign b))) (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat) (modelSumSigned a b) (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Hundred50)))))) def modelF32Add = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelOr (modelIsNaN a) (modelIsNaN b)) (modelNaNResult a b) (specSelect (modelIsInfinite a) (specSelect (modelAnd (modelIsInfinite b) (specNot (specEqual (modelSign a) (modelSign b)))) modelDefaultNaN a) (specSelect (modelIsInfinite b) b (modelAddFinite a b)))))) def modelF32Subtract = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelOr (modelIsNaN a) (modelIsNaN b)) (modelNaNResult a b) (modelF32Add a (modelNegate b))))) def modelF32Multiply = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelOr (modelIsNaN a) (modelIsNaN b)) (modelNaNResult a b) (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsZero b)) (modelAnd (modelIsZero a) (modelIsInfinite b))) modelDefaultNaN (specSelect (modelOr (modelIsInfinite a) (modelIsInfinite b)) (modelInfinityOf (modelXor (modelSign a) (modelSign b))) (specSelect (modelOr (modelIsZero a) (modelIsZero b)) (modelZeroOf (modelXor (modelSign a) (modelSign b))) (modelRoundBits (modelXor (modelSign a) (modelSign b)) (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b)) modelPow2Three00))))))) def modelF32Divide = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelOr (modelIsNaN a) (modelIsNaN b)) (modelNaNResult a b) (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsInfinite b)) (modelAnd (modelIsZero a) (modelIsZero b))) modelDefaultNaN (specSelect (modelOr (modelIsInfinite a) (modelIsZero b)) (modelInfinityOf (modelXor (modelSign a) (modelSign b))) (specSelect (modelOr (modelIsInfinite b) (modelIsZero a)) (modelZeroOf (modelXor (modelSign a) (modelSign b))) (modelRoundBits (modelXor (modelSign a) (modelSign b)) (modelScaledMagnitude a) (modelScaledMagnitude b)))))))) -- fused multiply-add a x b + c with ONE rounding, as SM86's FFMA performs it: -- the exact product (scale 2^300) and the exact addend (scale 2^150, raised to -- 2^300) are summed as signed exact magnitudes and rounded once. Special -- values: any NaN operand quiets; inf x 0 is invalid; an infinite product or -- addend with a finite partner gives that infinity; opposite infinities are -- invalid. A zero exact sum carries the sign the sum rule gives (+0 unless -- both are negative zero). def modelSignedScale = (lambda unrestricted value : (family ModelSigned) . (lambda unrestricted factor : Nat . (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) value (branch ModelSignedOf sign magnitude . (constructor ModelSigned ModelSignedOf sign (nat-multiply magnitude factor)))))) def modelSumSignedValues = (lambda unrestricted a : (family ModelSigned) . (lambda unrestricted b : (family ModelSigned) . (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) a (branch ModelSignedOf signA magnitudeA . (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) b (branch ModelSignedOf signB magnitudeB . (modelSelectSigned (specEqual signA signB) (constructor ModelSigned ModelSignedOf signA (nat-add magnitudeA magnitudeB)) (modelSelectSigned (nat-less-than magnitudeA magnitudeB) (constructor ModelSigned ModelSignedOf signB (nat-subtract magnitudeB magnitudeA)) (constructor ModelSigned ModelSignedOf (specSelect (nat-less-than magnitudeB magnitudeA) signA 0) (nat-subtract magnitudeA magnitudeB)))))))))) def modelFusedFinite = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat . (specSelect (modelAnd (modelOr (modelIsZero a) (modelIsZero b)) (modelIsZero c)) (modelZeroOf (modelAnd (modelXor (modelSign a) (modelSign b)) (modelSign c))) (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat) (modelSumSignedValues (constructor ModelSigned ModelSignedOf (modelXor (modelSign a) (modelSign b)) (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b))) (modelSignedScale (constructor ModelSigned ModelSignedOf (modelSign c) (modelScaledMagnitude c)) modelPow2Hundred50)) (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Three00))))))) def modelF32FusedMultiplyAdd = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat . (specSelect (modelOr (modelIsNaN a) (modelOr (modelIsNaN b) (modelIsNaN c))) (specSelect (modelIsNaN a) (modelQuiet a) (specSelect (modelIsNaN b) (modelQuiet b) (modelQuiet c))) (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsZero b)) (modelAnd (modelIsZero a) (modelIsInfinite b))) modelDefaultNaN (specSelect (modelOr (modelIsInfinite a) (modelIsInfinite b)) (specSelect (modelAnd (modelIsInfinite c) (specNot (specEqual (modelXor (modelSign a) (modelSign b)) (modelSign c)))) modelDefaultNaN (modelInfinityOf (modelXor (modelSign a) (modelSign b)))) (specSelect (modelIsInfinite c) c (modelFusedFinite a b c)))))))) -- square root: NaN quieted; signed zero preserved; +inf; a negative operand is -- invalid. A finite value is M / 2^150 with M the scaled magnitude, so its -- root is sqrt(M * 2^150) / 2^150 with an integer radicand of even scale; the -- floor root q is exact when q*q = N, and otherwise (2q+1)/2^151 lies on the -- same side of every rounding boundary as the true root. def modelIntegerRoot = (lambda unrestricted value : Nat . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat))) (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) . (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . (specSelect (nat-less-than (nat-add low 1) high) (specSelect (nat-less-than value (nat-multiply (nat-divide (nat-add low high) 2) (nat-divide (nat-add low high) 2))) (induction low (nat-divide (nat-add low high) 2)) (induction (nat-divide (nat-add low high) 2) high)) low))))) 200) zero (specPow2 (nat-add (nat-divide (specBitLength value) 2) 2)))) def modelF32SquareRoot = (lambda unrestricted a : Nat . (specSelect (modelIsNaN a) (modelQuiet a) (specSelect (modelIsZero a) a (specSelect (modelSign a) modelDefaultNaN (specSelect (modelIsInfinite a) modelInfinityBits (app (lambda unrestricted n : Nat . (app (lambda unrestricted q : Nat . (modelRoundBits 0 (specSelect (specEqual (nat-multiply q q) n) (nat-multiply 2 q) (nat-add (nat-multiply 2 q) 1)) (nat-multiply 2 modelPow2Hundred50))) (modelIntegerRoot n))) (nat-multiply (modelScaledMagnitude a) modelPow2Hundred50))))))) -- ordered comparisons (NaN: never less, never equal; -0 = +0); an infinity's -- key is above every finite scaled magnitude (2^300 > 2^278) def modelOrderKey = (lambda unrestricted bits : Nat . (specSelect (modelIsInfinite bits) modelPow2Three00 (modelScaledMagnitude bits))) def modelF32Less = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelOr (modelIsNaN a) (modelIsNaN b)) 0 (specSelect (modelAnd (modelIsZero a) (modelIsZero b)) 0 (specSelect (modelSign a) (specSelect (modelSign b) (nat-less-than (modelOrderKey b) (modelOrderKey a)) 1) (specSelect (modelSign b) 0 (nat-less-than (modelOrderKey a) (modelOrderKey b)))))))) def modelF32EqualValue = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelOr (modelIsNaN a) (modelIsNaN b)) 0 (specSelect (modelAnd (modelIsZero a) (modelIsZero b)) 1 (specEqual a b))))) -- FMNMX: the larger (smaller) of two values; a NaN operand gives the other, -- two give the canonical NaN; -0 is below +0. (What the argmax realizations -- use it for -- a running maximum and the smaller token of a tie -- does not -- depend on the zeros' order; it is ASSUMED, not yet held to a card.) def modelF32ExtremumNaN : Nat = 2147483647 def modelF32Below = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelAnd (modelIsZero a) (modelIsZero b)) (modelAnd (modelSign a) (specNot (modelSign b))) (modelF32Less a b)))) def modelF32Maximum = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelIsNaN a) (specSelect (modelIsNaN b) modelF32ExtremumNaN b) (specSelect (modelIsNaN b) a (specSelect (modelF32Below a b) b a))))) def modelF32Minimum = (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (specSelect (modelIsNaN a) (specSelect (modelIsNaN b) modelF32ExtremumNaN b) (specSelect (modelIsNaN b) a (specSelect (modelF32Below a b) a b))))) -- I2FP.F32.S32: the 32-bit word read as a signed integer, rounded to binary32 def modelF32FromSigned32 = (lambda unrestricted word : Nat . (specSelect (nat-less-than word modelPow2Thirty1) (modelRoundBits 0 word 1) (modelRoundBits 1 (nat-subtract (nat-multiply 2 modelPow2Thirty1) word) 1))) def f32ApproximateReciprocal : Nat = 4 def f32ApproximateReciprocalSquareRoot : Nat = 5 def f32ApproximateSquareRoot : Nat = 6 -- The model's approximations: the correctly rounded reciprocal and square -- root (and the reciprocal of the rounded square root) -- NOT the MUFU -- unit's results, which are within a few units in the last place of them; -- the trigonometric, exponential, logarithmic and tanh approximations are -- not modelled (the default NaN). A statement at the model that uses them -- is a statement about this choice; the checked paths state theirs for -- every choice. def modelF32Approximate = (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat . (specSelect (specEqual operation f32ApproximateReciprocal) (modelF32Divide 1065353216 value) (specSelect (specEqual operation f32ApproximateSquareRoot) (modelF32SquareRoot value) (specSelect (specEqual operation f32ApproximateReciprocalSquareRoot) (modelF32Divide 1065353216 (modelF32SquareRoot value)) modelDefaultNaN))))) def modelF32Operations : (family Float32Operations) = (constructor Float32Operations Float32OperationsValue modelF32Add modelF32Multiply modelF32FusedMultiplyAdd modelNegate modelF32Approximate) def f32Add = (lambda unrestricted operations : (family Float32Operations) . (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))) operations (branch Float32OperationsValue add multiply fused negate approximate . add))) def f32Multiply = (lambda unrestricted operations : (family Float32Operations) . (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))) operations (branch Float32OperationsValue add multiply fused negate approximate . multiply))) def f32FusedMultiplyAdd = (lambda unrestricted operations : (family Float32Operations) . (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted a : Nat . (pi unrestricted b : Nat . (pi unrestricted c : Nat . Nat)))) operations (branch Float32OperationsValue add multiply fused negate approximate . fused))) def f32Negate = (lambda unrestricted operations : (family Float32Operations) . (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted value : Nat . Nat)) operations (branch Float32OperationsValue add multiply fused negate approximate . negate))) def f32Approximate = (lambda unrestricted operations : (family Float32Operations) . (eliminate Float32Operations (lambda unrestricted current : (family Float32Operations) . (pi unrestricted operation : Nat . (pi unrestricted value : Nat . Nat))) operations (branch Float32OperationsValue add multiply fused negate approximate . approximate))) -- A value as the 32-bit word a register or memory holds, and operations -- whose every result is taken to a word: the arithmetic a 32-bit machine -- performs with them. For the model the words change nothing (its results -- are bit patterns); for operations in general, this is what a machine -- that masks each write computes. def f32Word = (lambda unrestricted value : Nat . (nat-modulo value 4294967296)) def f32OperationsOnWords = (lambda unrestricted operations : (family Float32Operations) . (constructor Float32Operations Float32OperationsValue (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (f32Word (f32Add operations left right)))) (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (f32Word (f32Multiply operations left right)))) (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat . (f32Word (f32FusedMultiplyAdd operations a b c))))) (lambda unrestricted value : Nat . (f32Word (f32Negate operations value))) (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat . (f32Word (f32Approximate operations operation value)))))) -- The binary32 operations as a 32-bit machine and the specifications use -- them: the model's, each result taken as the word it is. A binary32 result -- IS a word, so on words these are the model's values exactly; with them the -- statements proved for every choice of operations hold for the model with -- no side condition (Proof.LinearStepCorrectForEveryShape, WarpSumCorrect, -- HMMATileCorrect). def modelF32WordOperations : (family Float32Operations) = (f32OperationsOnWords modelF32Operations)