Native binary32 words and the generic model

Field packing, decoding, and rounding of native binary32 words agree with the generic Model FloatFormat.binary32 representation. The operation proofs build on these facts, and Narrow.Agreement combines them into agreement of the finite operations.

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_canonicalNaN : ofUInt32 2143289344 = canonicalNaN FloatFormat.binary32

The native canonical NaN word is the model's canonical NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_signedZero (sign : Bool) : ofUInt32 (if sign = true then 2147483648 else 0) = if sign = true then negZero FloatFormat.binary32 else posZero FloatFormat.binary32

The native signed-zero word is the model's signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_signedInf (sign : Bool) : ofUInt32 (if sign = true then 4286578688 else 2139095040) = if sign = true then negInf FloatFormat.binary32 else posInf FloatFormat.binary32

The native signed-infinity word is the model's signed infinity.

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.