Unsigned posit integer conversion guarantees

Accepted outputs denote the nearest-even integer exactly and have at most one-half unit of error. The range test applies to this rounded integer, including small negative inputs that round to zero.

The sentinel characterization includes the in-range integer 2^(width-1); its unsigned encoding is indistinguishable from the NaR or out-of-range result. Input conversion reserves that word before numerical rounding. Representable non-sentinel integers have exact round trips.

theorem FloatLib.Floats.Formats.Posit.Model.unsignedSentinel_toNat {width : ℕ} (hwidth : 0 < width) : (BitVec.intMin width).toNat = 2 ^ (width - 1)

The reserved unsigned word has just its most significant bit set.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ofUnsigned_intMin {width : ℕ} (format : Format) (hwidth : 0 < width) : ofUnsigned format (BitVec.intMin width) hwidth = nar format

theorem FloatLib.Floats.Formats.Posit.Model.ofUnsigned_eq_roundRat {format : Format} {width : ℕ} (value : BitVec width) (hwidth : 0 < width) (hvalue : value ≠ BitVec.intMin width) : ofUnsigned format value hwidth = roundRat format ↑value.toNat

Non-sentinel unsigned inputs use their natural-number value, even when their MSB is set.

theorem FloatLib.Floats.Formats.Posit.Model.ofUnsigned_eq_of_toRat? {format : Format} {width : ℕ} (value : BitVec width) (hwidth : 0 < width) (hvalue : value ≠ BitVec.intMin width) (result : Model format) (hexact : result.toRat? = some ↑value.toNat) : ofUnsigned format value hwidth = result

If a finite posit denotes the unsigned integer exactly, conversion recovers that posit.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_nar {width : ℕ} (format : Format) (hwidth : 0 < width) : toUnsigned width (nar format) hwidth = BitVec.intMin width

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_eq_intMin_of_none {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) (hvalue : value.toRat? = none) : toUnsigned width value hwidth = BitVec.intMin width

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_eq_of_inRange {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : (Numerics.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : toUnsigned width value hwidth = BitVec.ofNat width (Numerics.roundRatEven q).toNat

A rounded integer in the full unsigned range is packed without wraparound.

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_eq_intMin_of_not_inRange {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : ¬(Numerics.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : toUnsigned width value hwidth = BitVec.intMin width

theorem FloatLib.Floats.Formats.Posit.Model.toNat_toUnsigned_of_inRange {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : (Numerics.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : ↑(toUnsigned width value hwidth).toNat = Numerics.roundRatEven q

The output's unsigned numerical interpretation equals the rounded integer.

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_eq_intMin_iff {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) : toUnsigned width value hwidth = BitVec.intMin width ↔ ¬(Numerics.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q) ∨ Numerics.roundRatEven q = 2 ^ (width - 1)

Sentinel output also occurs for the valid unsigned integer sharing those bits.

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_error_le_half {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : (Numerics.IntegerFormat.unsigned width).InRange (Numerics.roundRatEven q)) : |↑(toUnsigned width value hwidth).toNat - q| ≤ 1 / 2

A successful conversion has the nearest-integer error bound.

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_even_of_half {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = 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

Half-integer ties choose an even output, by the shared exact integer rounder.

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_eq_of_nat {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {integer : ℕ} (hvalue : value.toRat? = some ↑integer) (hrange : integer < 2 ^ width) : toUnsigned width value hwidth = BitVec.ofNat width integer

An unsigned integer that is exactly represented by the posit is returned unchanged.

theorem FloatLib.Floats.Formats.Posit.Model.toUnsigned_ofUnsigned {format : Format} {width : ℕ} (value : BitVec width) (hwidth : 0 < width) (hvalue : value ≠ BitVec.intMin width) (hexact : (roundRat format ↑value.toNat).toRat? = some ↑value.toNat) : toUnsigned width (ofUnsigned format value hwidth) hwidth = value

Exact posit representability and a non-sentinel input suffice for an unsigned round trip.