Refinement of configured posit integer conversions

Both adapters refine the model conversions for arbitrary positive integer widths and lawful posit codecs. The semantic theorems expose the exact once-rounded integer input and nearest-even integer output, including the signed-minimum sentinel collision.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_ofFixedInt {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (value : Numerics.Representations.FixedInt width) (hwidth : 0 < width) : toModel (ofFixedInt value hwidth) = Formats.Posit.Model.ofFixedInt format value hwidth

Packing the integer conversion preserves the model result exactly.

theorem FloatLib.Floats.ExecFloat.Posit.toFixedInt_eq_model {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) : toFixedInt width value hwidth = Formats.Posit.Model.toFixedInt width (toModel value) hwidth

Converting a configured posit to an integer is conversion of its exact model value.

theorem FloatLib.Floats.ExecFloat.Posit.toModel_ofFixedInt_minCode {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (hwidth : 0 < width) : toModel (ofFixedInt (Numerics.Representations.FixedInt.minCode width) hwidth) = Formats.Posit.Model.nar format

The reserved integer word becomes the posit NaR encoding through every lawful codec.

theorem FloatLib.Floats.ExecFloat.Posit.ofFixedInt_eq_roundRat {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (value : Numerics.Representations.FixedInt width) (hwidth : 0 < width) (hvalue : value ≠ Numerics.Representations.FixedInt.minCode width) : toModel (ofFixedInt value hwidth) = Formats.Posit.Model.roundRat format ↑value.toInt

Non-sentinel integer inputs receive exactly one posit rounding of their signed values.

theorem FloatLib.Floats.ExecFloat.Posit.toFixedInt_eq_minCode_of_none {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) (hvalue : toRat? value = none) : toFixedInt width value hwidth = Numerics.Representations.FixedInt.minCode width

A configured NaR observation converts to the MSB-only integer sentinel.

theorem FloatLib.Floats.ExecFloat.Posit.toInt_toFixedInt_of_inRange {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) {q : ℚ} (hvalue : toRat? value = some q) (hrange : Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) : (toFixedInt width value hwidth).toInt = Numerics.roundRatEven q

An in-range configured conversion decodes to the exact nearest-even integer.

theorem FloatLib.Floats.ExecFloat.Posit.toFixedInt_eq_minCode_of_not_inRange {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) {q : ℚ} (hvalue : toRat? value = some q) (hrange : ¬Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) : toFixedInt width value hwidth = Numerics.Representations.FixedInt.minCode width

Out-of-range rounded integers produce the sentinel through every configured carrier.

theorem FloatLib.Floats.ExecFloat.Posit.toFixedInt_eq_minCode_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) {q : ℚ} (hvalue : toRat? value = some q) : toFixedInt width value hwidth = Numerics.Representations.FixedInt.minCode width ↔ ¬Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q) ∨ Numerics.roundRatEven q = Numerics.Representations.FixedInt.minValue width

Finite sentinel output includes both overflow and a rounded result at the signed minimum.

theorem FloatLib.Floats.ExecFloat.Posit.toFixedInt_error_le_half {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) {q : ℚ} (hvalue : toRat? value = some q) (hrange : Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) : |↑(toFixedInt width value hwidth).toInt - q| ≤ 1 / 2

The absolute conversion error is at most one half when the rounded integer fits.

theorem FloatLib.Floats.ExecFloat.Posit.toFixedInt_even_of_half {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (width : ℕ) (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hwidth : 0 < width) {q : ℚ} (hvalue : toRat? value = some q) (hrange : Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) (hhalf : 2 * (q.num.natAbs % q.den) = q.den) : (toFixedInt width value hwidth).toInt % 2 = 0

Exact halfway values convert to even integers, provided their rounded values fit.