Configured unsigned integer semantics

The codec preserves the model's numerical guarantees: exact unsigned decoding after accepted rounding, a half-unit error bound, even halfway results, and the MSB-only sentinel rule including its collision with a valid unsigned integer.

@[simp]

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

Decoding the configured conversion recovers the model result through any lawful codec.

theorem FloatLib.Floats.ExecFloat.Posit.toUnsigned_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) : toUnsigned width value hwidth = Formats.Posit.Model.toUnsigned width (toModel value) hwidth

Storage choice does not change unsigned rounding or sentinel delivery.

theorem FloatLib.Floats.ExecFloat.Posit.toModel_ofUnsigned_intMin {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (hwidth : 0 < width) : toModel (ofUnsigned (BitVec.intMin width) hwidth) = Formats.Posit.Model.nar format

The MSB-only input becomes NaR through every lawful storage codec.

theorem FloatLib.Floats.ExecFloat.Posit.ofUnsigned_eq_roundRat {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] {width : ℕ} (value : BitVec width) (hwidth : 0 < width) (hvalue : value ≠ BitVec.intMin width) : toModel (ofUnsigned value hwidth) = Formats.Posit.Model.roundRat format ↑value.toNat

Outside the reserved MSB-only word, conversion rounds the unsigned natural value by the posit rounding rule.

theorem FloatLib.Floats.ExecFloat.Posit.toUnsigned_eq_intMin_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) : toUnsigned width value hwidth = BitVec.intMin width

NaR converts to the MSB-only output sentinel.

theorem FloatLib.Floats.ExecFloat.Posit.toNat_toUnsigned_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.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : ↑(toUnsigned width value hwidth).toNat = Numerics.roundRatEven q

Accepted output bits denote the exact rounded integer, without modular wraparound.

theorem FloatLib.Floats.ExecFloat.Posit.toUnsigned_eq_intMin_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.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : toUnsigned width value hwidth = BitVec.intMin width

A finite input whose rounded integer is outside the unsigned range delivers the sentinel.

theorem FloatLib.Floats.ExecFloat.Posit.toUnsigned_eq_intMin_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) : toUnsigned width value hwidth = BitVec.intMin width ↔ ¬(Numerics.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q) ∨ Numerics.roundRatEven q = 2 ^ (width - 1)

For finite inputs, the sentinel bits denote either a rejected rounded integer or the successful value 2 ^ (width - 1). These cases cannot be distinguished from the bits alone.

theorem FloatLib.Floats.ExecFloat.Posit.toUnsigned_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.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : |↑(toUnsigned width value hwidth).toNat - q| ≤ 1 / 2

An accepted unsigned conversion differs from the exact posit value by at most half a unit.

theorem FloatLib.Floats.ExecFloat.Posit.toUnsigned_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.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) (hhalf : 2 * (q.num.natAbs % q.den) = q.den) : (toUnsigned width value hwidth).toNat % 2 = 0

An accepted halfway input rounds to an even unsigned integer, including a negative halfway input whose rounded result is zero.