Configured binary-family conversion proofs

The configured runtime/model conversions are mutual inverses. Their injectivity and FormatSemantics instance are consequences of the codec laws, independent of the chosen carrier.

@[simp]

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

Decoding immediately after packing through a configured codec is lossless.

@[simp]

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

Packing immediately after decoding a configured value is lossless.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Family.toModel_injective {format : FloatFormat} {plan : StoragePlan format} {code : Type} [codec : ExecFloat.ModelCodec plan (Model format) code] {left right : ExecFloat (Family format code plan)} (equality : toModel left = toModel right) : left = right

Model decoding is injective because packing is its inverse.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.BinaryInterchange.Configured.Family.instFormatSemantics {format : FloatFormat} {plan : StoragePlan format} {code : Type} [codec : ExecFloat.ModelCodec plan (Model format) code] : Numerics.FormatSemantics (Family format code plan)