Native binary32 field-packing identities

The executable field operations live in Narrow.Base.Runtime. This module proves that extracting and repacking a native binary32 word is lossless, and records the native form of quieting a NaN.

These bit-level identities are shared by addition and fused multiply-add proofs, but do not depend on either arithmetic operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.mkBits_fields (bits : UInt32) : mkBits (signBit bits) (expField bits).toNat (fracField bits).toNat = bits

Repacking the fields extracted from a native binary32 word returns the original word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.ofUInt32_or_quietBit (x : Value) : ofUInt32 (toUInt32 x ||| 4194304) = ofBits (x.bits ||| FloatFormat.binary32.quietBit)

Setting the native quiet-NaN bit agrees with setting the generic binary32 quiet bit.