Configured posit-family conversion proofs

The configured runtime/model conversions are mutual inverses. The same codec laws yield injectivity, ordinary numerical semantics, and format-indexed exact decoding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.Family.decode_eq_codeToModel {format : Format} {plan : StoragePlan format} (value : ExecFloat (Family format (Code plan) plan)) : ExecFloat.ModelCodec.decode value = Code.toModel value.raw

For the built-in storage family, codec decoding is exactly the constructor-indexed Code.toModel function.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.Family.toModel_ofModel {format : Format} {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 posit codec is lossless.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Configured.Family.ofModel_toModel {format : Format} {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 posit is lossless.

theorem FloatLib.Floats.Formats.Posit.Configured.Family.toModel_injective {format : Format} {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]

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

@[instance_reducible]

instance FloatLib.Floats.Formats.Posit.Configured.Family.instHasExactSemantics {format : Format} {plan : StoragePlan format} {code : Type} [codec : ExecFloat.ModelCodec plan (Model format) code] : Numerics.HasExactSemantics (Family format code plan)