Agreement between native binary32 words and the generic model

The narrow-word core implements finite binary32 arithmetic with UInt32 and UInt64. This module contains the proof-side bridge back to the generic Model FloatFormat.binary32 representation: field packing, decoding, rounding, and the shared finite-operation specifications.

The operation-specific Addition, Multiplication, and Fma proof modules connect their native implementations to the finite specifications used here. Together, these results connect native arithmetic to the generic binary32 model. Runtime clients can import the corresponding Runtime modules without this proof development.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.toUInt32_ofFields (sign : Bool) (exponent fraction : ℕ) : toUInt32 (ofFields FloatFormat.binary32 sign exponent fraction) = mkBits sign exponent fraction

Native and generic binary32 field packing produce the same storage word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_mkBits (sign : Bool) (exponent fraction : ℕ) : ofUInt32 (mkBits sign exponent fraction) = ofFields FloatFormat.binary32 sign exponent fraction

Rewrapping native field packing equals generic Model.ofFields.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.expField_toNat (x : Value) : (expField (toUInt32 x)).toNat = Model.expField x

Native and generic binary32 exponent extraction have the same natural-number value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fracField_toNat (x : Value) : (fracField (toUInt32 x)).toNat = Model.fracField x

Native and generic binary32 fraction extraction have the same natural-number value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.signBit_eq (x : Value) : signBit (toUInt32 x) = Model.signBit x

Native and generic binary32 sign extraction agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.expField_beq_zero (x : Value) : (expField (toUInt32 x) == 0) = (Model.expField x == 0)

Native and generic binary32 exponent zero tests agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.expField_beq_allOnes (x : Value) : (expField (toUInt32 x) == 255) = (Model.expField x == 255)

Native and generic binary32 exceptional-exponent tests agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fracField_beq_zero (x : Value) : (fracField (toUInt32 x) == 0) = (Model.fracField x == 0)

Native and generic binary32 fraction zero tests agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.toDyadic_eq (x : Value) : toDyadic? (toUInt32 x) = Model.toDyadic? x

Native field extraction decodes the same exact dyadic as generic binary32.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_roundRatScaled (sign : Bool) (num den : ℕ) (exponent : ℤ) : ofUInt32 (roundRatScaled sign num den exponent) = Model.roundRatScaled FloatFormat.binary32 sign num den exponent

Native rational rounding agrees with generic binary32 rational rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_roundDyadic (value : Numerics.Dyadic) : ofUInt32 (roundDyadic value) = Model.roundDyadic FloatFormat.binary32 value

Native dyadic rounding agrees with generic binary32 rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.addFinite_eq (x y : Value) : addFinite? x y = match Model.toDyadic? x, Model.toDyadic? y with | some dx, some dy => some (Model.roundDyadic FloatFormat.binary32 (addDyadic dx dy)) | x, x_1 => none

The native finite add result is exactly the generic finite add result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.mulFinite_eq (x y : Value) : mulFinite? x y = match Model.toDyadic? x, Model.toDyadic? y with | some dx, some dy => have sign := dx.negative ^^ dy.negative; if (dx.significand == 0 || dy.significand == 0) = true then some (if sign = true then negZero FloatFormat.binary32 else posZero FloatFormat.binary32) else some (Model.roundDyadic FloatFormat.binary32 { negative := sign, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }) | x, x_1 => none

The native finite multiply result is exactly the generic finite multiply result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.divFinite_eq (x y : Value) : divFinite? x y = match Model.toDyadic? x, Model.toDyadic? y with | some dx, some dy => have sign := dx.negative ^^ dy.negative; some (if (dy.significand == 0) = true then if (dx.significand == 0) = true then canonicalNaN FloatFormat.binary32 else if sign = true then negInf FloatFormat.binary32 else posInf FloatFormat.binary32 else if (dx.significand == 0) = true then if sign = true then negZero FloatFormat.binary32 else posZero FloatFormat.binary32 else Model.roundRatScaled FloatFormat.binary32 sign dx.significand dy.significand (dx.exponent - dy.exponent)) | x, x_1 => none

The native finite divide result is exactly the generic finite divide result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.fmaFinite_eq (x y z : Value) : fmaFinite? x y z = match Model.toDyadic? x, Model.toDyadic? y, Model.toDyadic? z with | some dx, some dy, some dz => have product := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; some (Model.roundDyadic FloatFormat.binary32 (addDyadic product dz)) | x, x_1, x_2 => none

The native finite fused multiply-add result is exactly the generic finite result.