Packing correctness for configured binary values

The storage-independent constructors form a lossless equivalence with the exact-width binary model and with every in-range complete interchange word. This module depends only on the representation interface; importing these proofs does not register arithmetic backends.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Formats.BinaryInterchange.Model format) : toModel (ofModel value) = value

Decoding immediately after packing a binary proof model returns the original model.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.ofModel_toModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : ofModel (toModel value) = value

Packing immediately after decoding a configured binary value returns the original value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.ofNatBits_toNatBits {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : ofNatBits (toNatBits value) = value

Reconstructing a configured binary value from its complete word is lossless.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toNatBits_ofNatBits_of_lt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (bits : ℕ) (bits_lt : bits < 2 ^ format.bitWidth) : toNatBits (ofNatBits bits) = bits

Reading an in-range complete word immediately after constructing it returns that word.