Configured posit conversion refinement

The conversion equations hold for every width, storage plan and lawful codec. Encoding and decoding add no rounding.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromConfiguredPosit_eq {format : Posit.Format} {plan : Posit.Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Posit.Model format) code] (target : Format) (mode : RoundingMode) (x : ExecFloat (Posit.Configured.Family format code plan)) : fromConfiguredPosit target mode x = fromPosit target mode (ExecFloat.Posit.toModel x)

Configured posit-to-decimal conversion is exactly the model conversion.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toModel_toConfiguredPosit {format : Posit.Format} {plan : Posit.Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Posit.Model format) code] (x : Datum) : ExecFloat.Posit.toModel (toConfiguredPosit x) = toPosit format x

The encoded result decodes exactly to the model decimal-to-posit conversion.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toConfiguredPosit_eq_real {format : Posit.Format} {plan : Posit.Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Posit.Model format) code] (x : Datum) {a : ℚ} (hx : x.toRat? = some a) : ExecFloat.Posit.toModel (toConfiguredPosit x) = Posit.Model.RealRounding.round format ↑a

A finite decimal input rounds once by the Posit Standard rule, for any lawful carrier.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromConfiguredPosit_eq_project {format : Posit.Format} {plan : Posit.Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Posit.Model format) code] (target : Format) (mode : RoundingMode) (x : ExecFloat (Posit.Configured.Family format code plan)) {a : ℚ} (hx : ExecFloat.Posit.toRat? x = some a) : fromConfiguredPosit target mode x = project target mode a 0

A finite configured posit is projected from its exact rational value.