module Std.Float -- IEEE-754 binary32 / binary64 as `Std` vocabulary over the EXISTING bit-pattern -- owners (Language & Testing Evolution L12a, PRD 08 N6 / NUM-002 groundwork). -- Owners (evidence/language-testing/L12a-float-representation-audit.md): -- F32 = Data.Float32Bits.InferenceFloat32 (four bytes, little-endian, byte 3 -- carries the sign bit; foundation's binary32 home "next to -- ModelFloat64Bits", with sign/zero/finite predicates); -- F64 = Model.Parameter.ModelFloat64Bits (eight bytes, little-endian). -- Alpha.Numeric.AlphaFloat32 (the literal payload of the native-lowering -- expression graphs) is the same four bytes under another name; it is kept as -- the lowering carrier. RECORDED (L12a): Alpha.Numeric does not parse under the -- current parser (ALPHA-PARSE-APP at Numeric.alpha:159:9, outside every gate -- closure), so the byte conversion between the two carriers lands with the L13 -- lowering work, not here. No arithmetic lives here (L13); this module is CONSTRUCTION, -- PROJECTION, CLASSIFICATION and EQUALITY at the bits level: -- stdF32Equal mathematical equality: NaN never equals anything (not even -- itself), +0 equals -0, otherwise the bits decide; -- stdF32BitsEqual bit-pattern equality (NaN payloads and signed zeros distinct). -- The explicit "bits" form of PRD 08 N3 is NOT new syntax: `(stdF32FromWord32 0x3f800000)` -- with the U32 literal typed by its expected type (L11s) is the form. -- NaN and the infinities are named constructions, never literals (N6). import Std.Byte import Std.Natural import Std.Foundation import Model.Config import Model.Parameter import Model.Word32 import Model.Word64 import Data.Float32Bits import Data.Bytes import Std.Word -- REG-003 leading-bit search state: the 24-bit significand shifted left so far -- and how many shifts were applied (0..23). family StdF32UnitState : Type 0 constructor StdF32UnitStateOf field unrestricted stdF32UnitCurrent : (family ModelWord32) field unrestricted stdF32UnitShifts : Nat end-family def F32 = (family InferenceFloat32) def F64 = (family ModelFloat64Bits) -- F32 construction / projection def stdF32FromBytes = inferenceFloat32 def stdF32FromWord32 = (lambda unrestricted word : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . (family InferenceFloat32)) word (branch ModelWord32Value b0 b1 b2 b3 . (inferenceFloat32 b0 b1 b2 b3)))) def stdF32ToWord32 = (lambda unrestricted value : (family InferenceFloat32) . (eliminate InferenceFloat32 (lambda unrestricted current : (family InferenceFloat32) . (family ModelWord32)) value (branch InferenceFloat32Bits b0 b1 b2 b3 . (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3)))) -- F32 classification (0/1 flags). The owner's predicates are reused by name. def stdF32IsNegative = inferenceFloat32Negative def stdF32IsZero = inferenceFloat32Zero def stdF32IsFinite = inferenceFloat32Finite -- exponent field all ones: byte 3 low seven bits = 0x7f and byte 2 high bit set def stdF32ExponentAllOnes = (lambda unrestricted value : (family InferenceFloat32) . (eliminate InferenceFloat32 (lambda unrestricted current : (family InferenceFloat32) . Nat) value (branch InferenceFloat32Bits b0 b1 b2 b3 . (stdFlagAnd (stdFlagOr (byte-equal b3 (byte 127)) (byte-equal b3 (byte 255))) (stdFlagNot (byte-less-than b2 (byte 128))))))) -- fraction field nonzero: byte 2 low seven bits, byte 1, byte 0 def stdF32FractionNonzero = (lambda unrestricted value : (family InferenceFloat32) . (eliminate InferenceFloat32 (lambda unrestricted current : (family InferenceFloat32) . Nat) value (branch InferenceFloat32Bits b0 b1 b2 b3 . (stdFlagOr (stdFlagNot (byte-equal (byteAnd b2 (byte 127)) (byte 0))) (stdFlagOr (stdFlagNot (byte-equal b1 (byte 0))) (stdFlagNot (byte-equal b0 (byte 0)))))))) def stdF32IsNaN = (lambda unrestricted value : (family InferenceFloat32) . (stdFlagAnd (stdF32ExponentAllOnes value) (stdF32FractionNonzero value))) def stdF32IsInfinite = (lambda unrestricted value : (family InferenceFloat32) . (stdFlagAnd (stdF32ExponentAllOnes value) (stdFlagNot (stdF32FractionNonzero value)))) -- F32 equality (N6) def stdF32BitsEqual = (lambda unrestricted a : (family InferenceFloat32) . (lambda unrestricted b : (family InferenceFloat32) . (stdU32Equal (stdF32ToWord32 a) (stdF32ToWord32 b)))) def stdF32Equal = (lambda unrestricted a : (family InferenceFloat32) . (lambda unrestricted b : (family InferenceFloat32) . (stdFlagAnd (stdFlagNot (stdFlagOr (stdF32IsNaN a) (stdF32IsNaN b))) (stdFlagOr (stdFlagAnd (stdF32IsZero a) (stdF32IsZero b)) (stdF32BitsEqual a b))))) -- F32 named values (never literals) def stdF32Zero = (inferenceFloat32 (byte 0) (byte 0) (byte 0) (byte 0)) def stdF32NegativeZero = (inferenceFloat32 (byte 0) (byte 0) (byte 0) (byte 128)) def stdF32One = (inferenceFloat32 (byte 0) (byte 0) (byte 128) (byte 63)) def stdF32Infinity = (inferenceFloat32 (byte 0) (byte 0) (byte 128) (byte 127)) def stdF32NegativeInfinity = (inferenceFloat32 (byte 0) (byte 0) (byte 128) (byte 255)) def stdF32NaN = (inferenceFloat32 (byte 0) (byte 0) (byte 192) (byte 127)) -- F64 construction / projection -- NUM-005 integer <-> binary32 conversions. Every conversion is a named function; -- rounding is to nearest, ties to even (IEEE-754 roundTiesToEven); a float that is -- NaN or infinite, or whose rounded value does not fit, has no integer (StdNone). -- The arithmetic is on naturals, over the existing bit owners (the F32's Word32 and -- the I32's Word32), so there is no second representation of either. -- A natural's low 32 bits as a Word32, by compile-time division (nat-divide / -- nat-modulo fold on closed naturals in one step). Model.Word32's -- modelWord32FromNaturalTruncated is the runtime owner and counts through the -- value, which a 2^30-sized float bit pattern cannot afford; these conversions -- are compile-time arithmetic throughout, so they take this form. def stdFloatWord32OfNatural = (lambda unrestricted value : Nat . (constructor ModelWord32 ModelWord32Value (nat-to-byte (nat-modulo value 256)) (nat-to-byte (nat-modulo (nat-divide value 256) 256)) (nat-to-byte (nat-modulo (nat-divide value 65536) 256)) (nat-to-byte (nat-modulo (nat-divide value 16777216) 256)))) -- `significand` shifted right by `shift` bits, rounded to nearest, ties to even. def stdFloatRoundedShift = (lambda unrestricted significand : Nat . (lambda unrestricted shift : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) significand (lambda unrestricted shiftPredecessor : Nat . (lambda unrestricted shiftInduction : Nat . (app (lambda unrestricted scale : Nat . (app (lambda unrestricted quotient : Nat . (app (lambda unrestricted remainder : Nat . (app (lambda unrestricted half : Nat . (nat-add quotient (nat-eliminate (lambda unrestricted current : Nat . Nat) (nat-multiply (naturalEqual remainder half) (nat-modulo quotient 2)) (lambda unrestricted abovePredecessor : Nat . (lambda unrestricted aboveInduction : Nat . 1)) (nat-less-than half remainder)))) (nat-divide scale 2))) (nat-modulo significand scale))) (nat-divide significand scale))) (naturalPowerOfTwo shift)))) shift))) -- The position of the highest set bit of a positive natural below 2^33. def stdFloatFloorLog2 = (lambda unrestricted value : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted position : Nat . (lambda unrestricted count : Nat . (nat-add count (naturalIsZero (nat-less-than value (naturalPowerOfTwo (succ position))))))) 32)) -- A binary32 from its sign (0 or 1), unbiased exponent and 24-bit significand -- (leading bit set). def stdFloatF32Assemble = (lambda unrestricted negative : Nat . (lambda unrestricted exponent : Nat . (lambda unrestricted significand : Nat . (stdF32FromWord32 (stdFloatWord32OfNatural (nat-add (nat-multiply negative 2147483648) (nat-add (nat-multiply (nat-add exponent 127) 8388608) (nat-subtract significand 8388608)))))))) -- The nearest binary32 to a positive integer magnitude: exactly when it has at most -- 24 significant bits, otherwise its low bits rounded away (a carry to 2^24 moves -- the exponent). def stdFloatF32FromMagnitude = (lambda unrestricted negative : Nat . (lambda unrestricted magnitude : Nat . (app (lambda unrestricted exponent : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family InferenceFloat32)) (app (lambda unrestricted rounded : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family InferenceFloat32)) (stdFloatF32Assemble negative exponent rounded) (lambda unrestricted carryPredecessor : Nat . (lambda unrestricted carryInduction : (family InferenceFloat32) . (stdFloatF32Assemble negative (succ exponent) 8388608))) (naturalEqual rounded 16777216))) (stdFloatRoundedShift magnitude (nat-subtract exponent 23))) (lambda unrestricted exactPredecessor : Nat . (lambda unrestricted exactInduction : (family InferenceFloat32) . (stdFloatF32Assemble negative exponent (nat-multiply magnitude (naturalPowerOfTwo (nat-subtract 23 exponent)))))) (nat-less-than exponent 24))) (stdFloatFloorLog2 magnitude)))) -- An I32 as the nearest binary32 (ties to even): always defined; zero is +0. def stdI32ToF32 : (pi unrestricted value : (family StdI32) . (family InferenceFloat32)) = (lambda unrestricted value : (family StdI32) . (app (lambda unrestricted bits : Nat . (app (lambda unrestricted negative : Nat . (app (lambda unrestricted magnitude : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family InferenceFloat32)) stdF32Zero (lambda unrestricted magnitudePredecessor : Nat . (lambda unrestricted magnitudeInduction : (family InferenceFloat32) . (stdFloatF32FromMagnitude negative magnitude))) magnitude)) (nat-eliminate (lambda unrestricted current : Nat . Nat) bits (lambda unrestricted signPredecessor : Nat . (lambda unrestricted signInduction : Nat . (nat-subtract 4294967296 bits))) negative))) (naturalIsZero (nat-less-than bits 2147483648)))) (modelWord32ToNatural (stdI32ToWord value)))) -- A binary32 as an I32, rounded to nearest (ties to even); NaN, the infinities -- and any value whose rounding lies outside [-2^31, 2^31) have none. def stdF32ToI32Checked : (pi unrestricted value : (family InferenceFloat32) . (family StdOption (family StdI32))) = (lambda unrestricted value : (family InferenceFloat32) . (app (lambda unrestricted bits : Nat . (app (lambda unrestricted biased : Nat . (app (lambda unrestricted negative : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family StdOption (family StdI32))) (app (lambda unrestricted magnitude : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family StdOption (family StdI32))) (nat-eliminate (lambda unrestricted current : Nat . (family StdOption (family StdI32))) (constructor StdOption StdNone (family StdI32)) (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family StdOption (family StdI32)) . (constructor StdOption StdSome (family StdI32) (stdI32FromWord (stdFloatWord32OfNatural magnitude))))) (nat-less-than magnitude 2147483648)) (lambda unrestricted negativePredecessor : Nat . (lambda unrestricted negativeInduction : (family StdOption (family StdI32)) . (nat-eliminate (lambda unrestricted current : Nat . (family StdOption (family StdI32))) (constructor StdOption StdNone (family StdI32)) (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family StdOption (family StdI32)) . (constructor StdOption StdSome (family StdI32) (stdI32FromWord (stdFloatWord32OfNatural (nat-subtract 4294967296 magnitude)))))) (nat-less-than magnitude 2147483649)))) negative)) (nat-eliminate (lambda unrestricted current : Nat . Nat) (stdFloatRoundedShift (nat-add (nat-modulo bits 8388608) 8388608) (nat-subtract 150 biased)) (lambda unrestricted largePredecessor : Nat . (lambda unrestricted largeInduction : Nat . (nat-multiply (nat-add (nat-modulo bits 8388608) 8388608) (naturalPowerOfTwo (nat-subtract biased 150))))) (naturalIsZero (nat-less-than biased 150)))) (lambda unrestricted specialPredecessor : Nat . (lambda unrestricted specialInduction : (family StdOption (family StdI32)) . (constructor StdOption StdNone (family StdI32)))) (naturalEqual biased 255))) (naturalIsZero (nat-less-than bits 2147483648)))) (nat-modulo (nat-divide bits 8388608) 256))) (modelWord32ToNatural (stdF32ToWord32 value)))) def stdF64FromBytes = (lambda unrestricted b0 : Byte . (lambda unrestricted b1 : Byte . (lambda unrestricted b2 : Byte . (lambda unrestricted b3 : Byte . (lambda unrestricted b4 : Byte . (lambda unrestricted b5 : Byte . (lambda unrestricted b6 : Byte . (lambda unrestricted b7 : Byte . (constructor ModelFloat64Bits ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7))))))))) def stdF64FromWord64 = (lambda unrestricted word : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . (family ModelFloat64Bits)) word (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (constructor ModelFloat64Bits ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7)))) def stdF64ToWord64 = (lambda unrestricted value : (family ModelFloat64Bits) . (eliminate ModelFloat64Bits (lambda unrestricted current : (family ModelFloat64Bits) . (family ModelWord64)) value (branch ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7 . (constructor ModelWord64 ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7)))) -- F64 wire codecs (NUM-008): an F64 is eight little-endian bytes of IEEE-754 -- binary64, so its encodings are the Data.Bytes Word64 codecs over the same -- bits -- no second implementation. Encode takes the F64; the exact decoders -- are Data.Bytes' own (exactly eight bytes, short and trailing input rejected) -- and answer the ModelWord64, which stdF64FromWord64 makes an F64 -- the same -- convention as Data.Float32Bits' F32 codecs. def stdF64EncodeLE = (lambda unrestricted value : (family ModelFloat64Bits) . (dataBytesWord64LE (stdF64ToWord64 value))) def stdF64EncodeBE = (lambda unrestricted value : (family ModelFloat64Bits) . (dataBytesWord64BE (stdF64ToWord64 value))) def stdF64DecodeLEExact = dataBytesDecodeWord64LEExact def stdF64DecodeBEExact = dataBytesDecodeWord64BEExact -- F64 classification: sign = byte 7 high bit; exponent = byte 7 low seven bits -- and byte 6 high four bits (eleven bits); fraction = byte 6 low four bits and -- bytes 5..0. def stdF64IsNegative = (lambda unrestricted value : (family ModelFloat64Bits) . (eliminate ModelFloat64Bits (lambda unrestricted current : (family ModelFloat64Bits) . Nat) value (branch ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7 . (stdFlagNot (byte-less-than b7 (byte 128)))))) def stdF64IsZero = (lambda unrestricted value : (family ModelFloat64Bits) . (eliminate ModelFloat64Bits (lambda unrestricted current : (family ModelFloat64Bits) . Nat) value (branch ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7 . (stdFlagAnd (byte-equal b0 (byte 0)) (stdFlagAnd (byte-equal b1 (byte 0)) (stdFlagAnd (byte-equal b2 (byte 0)) (stdFlagAnd (byte-equal b3 (byte 0)) (stdFlagAnd (byte-equal b4 (byte 0)) (stdFlagAnd (byte-equal b5 (byte 0)) (stdFlagAnd (byte-equal b6 (byte 0)) (stdFlagOr (byte-equal b7 (byte 0)) (byte-equal b7 (byte 128))))))))))))) def stdF64ExponentAllOnes = (lambda unrestricted value : (family ModelFloat64Bits) . (eliminate ModelFloat64Bits (lambda unrestricted current : (family ModelFloat64Bits) . Nat) value (branch ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7 . (stdFlagAnd (byte-equal (byteAnd b7 (byte 127)) (byte 127)) (byte-equal (byteAnd b6 (byte 240)) (byte 240)))))) def stdF64FractionNonzero = (lambda unrestricted value : (family ModelFloat64Bits) . (eliminate ModelFloat64Bits (lambda unrestricted current : (family ModelFloat64Bits) . Nat) value (branch ModelFloat64BitsValue b0 b1 b2 b3 b4 b5 b6 b7 . (stdFlagOr (stdFlagNot (byte-equal (byteAnd b6 (byte 15)) (byte 0))) (stdFlagOr (stdFlagNot (byte-equal b5 (byte 0))) (stdFlagOr (stdFlagNot (byte-equal b4 (byte 0))) (stdFlagOr (stdFlagNot (byte-equal b3 (byte 0))) (stdFlagOr (stdFlagNot (byte-equal b2 (byte 0))) (stdFlagOr (stdFlagNot (byte-equal b1 (byte 0))) (stdFlagNot (byte-equal b0 (byte 0)))))))))))) def stdF64IsFinite = (lambda unrestricted value : (family ModelFloat64Bits) . (stdFlagNot (stdF64ExponentAllOnes value))) def stdF64IsNaN = (lambda unrestricted value : (family ModelFloat64Bits) . (stdFlagAnd (stdF64ExponentAllOnes value) (stdF64FractionNonzero value))) def stdF64IsInfinite = (lambda unrestricted value : (family ModelFloat64Bits) . (stdFlagAnd (stdF64ExponentAllOnes value) (stdFlagNot (stdF64FractionNonzero value)))) -- F64 equality (N6) def stdF64BitsEqual = (lambda unrestricted a : (family ModelFloat64Bits) . (lambda unrestricted b : (family ModelFloat64Bits) . (stdU64Equal (stdF64ToWord64 a) (stdF64ToWord64 b)))) def stdF64Equal = (lambda unrestricted a : (family ModelFloat64Bits) . (lambda unrestricted b : (family ModelFloat64Bits) . (stdFlagAnd (stdFlagNot (stdFlagOr (stdF64IsNaN a) (stdF64IsNaN b))) (stdFlagOr (stdFlagAnd (stdF64IsZero a) (stdF64IsZero b)) (stdF64BitsEqual a b))))) -- F64 named values (never literals) def stdF64Zero = (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0)) def stdF64NegativeZero = (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 128)) def stdF64One = (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 240) (byte 63)) def stdF64Infinity = (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 240) (byte 127)) def stdF64NegativeInfinity = (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 240) (byte 255)) def stdF64NaN = (stdF64FromBytes (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 0) (byte 248) (byte 127)) -- REG-003 (PRD 08 N8): the uniform [0,1) contract. stdF32UnitFromWord32 w is -- EXACTLY (w >> 8) x 2^-24 — the 24-bit grid, so the largest input 0xFFFFFFFF -- gives (2^24 - 1) x 2^-24 = 1 - 2^-24 = 0x3f7fffff, never 1.0, and 0 gives +0.0. -- Bit assembly over U32 (no float arithmetic): m = w >> 8; if m = 0 the value is -- +0.0; otherwise the leading bit of m is found by shifting left until bit 23 is -- set (k shifts, 0..23), the exponent field is 126 - k (= 127 + (23 - k) - 24) -- and the fraction field is the shifted m without its leading bit. Verified on -- the native lane (debug/std-word-native-check.py, f32 rows) against an -- independent oracle: the evaluator lane runs the word shifts through unary -- bytes and is not a routine law here. def stdF32UnitLeadingBit = (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 128) (byte 0)) def stdF32UnitStep = (lambda unrestricted state : (family StdF32UnitState) . (eliminate StdF32UnitState (lambda unrestricted current : (family StdF32UnitState) . (family StdF32UnitState)) state (branch StdF32UnitStateOf current shifts . (nat-eliminate (lambda unrestricted current2 : Nat . (family StdF32UnitState)) (constructor StdF32UnitState StdF32UnitStateOf current shifts) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdF32UnitState) . (constructor StdF32UnitState StdF32UnitStateOf (stdU32ShiftLeft current (succ zero)) (succ shifts)))) (stdU32LessThan current stdF32UnitLeadingBit))))) def stdF32UnitRun = (lambda unrestricted significand : (family ModelWord32) . (nat-eliminate (lambda unrestricted current : Nat . (family StdF32UnitState)) (constructor StdF32UnitState StdF32UnitStateOf significand zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdF32UnitState) . (stdF32UnitStep induction))) (byte-to-nat (byte 23)))) def stdF32UnitAssemble = (lambda unrestricted state : (family StdF32UnitState) . (eliminate StdF32UnitState (lambda unrestricted current : (family StdF32UnitState) . (family InferenceFloat32)) state (branch StdF32UnitStateOf current shifts . (stdF32FromWord32 (stdU32AddWrapping (stdU32ShiftLeft (constructor ModelWord32 ModelWord32Value (nat-to-byte (naturalSaturatingSubtract (byte-to-nat (byte 126)) shifts)) (byte 0) (byte 0) (byte 0)) (byte-to-nat (byte 23))) (stdU32SubtractWrapping current stdF32UnitLeadingBit)))))) def stdF32UnitFromWord32 = (lambda unrestricted word : (family ModelWord32) . (app (lambda unrestricted significand : (family ModelWord32) . (nat-eliminate (lambda unrestricted current : Nat . (family InferenceFloat32)) (stdF32UnitAssemble (stdF32UnitRun significand)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family InferenceFloat32) . stdF32Zero)) (stdU32IsZero significand))) (stdU32ShiftRight word (byte-to-nat (byte 8)))))