Float32Model

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.

41field unrestricted f32OperationAdd : (pi unrestricted left : Nat . (pi unrestricted right : Nat . Nat))