Exact semantics of posit integer conversions

The integer sentinel has only its most significant bit set. Finite posit values first undergo exact nearest-even integer rounding; the signed range is checked on that rounded integer. Within range, decoding the output recovers the rounded integer, with error at most one half. At an exact halfway numerator/denominator remainder, that integer is even.

The sentinel characterization includes an in-range result equal to the signed minimum, whose encoding coincides with the overflow and NaR sentinel.

theorem FloatLib.Floats.Formats.Posit.Model.integerSentinel_toNatBits {width : ℕ} (hwidth : 0 < width) : (Numerics.Representations.FixedInt.minCode width).toNatBits = 2 ^ (width - 1)

The integer conversion sentinel has precisely its most significant bit set.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ofFixedInt_minCode {width : ℕ} (format : Format) (hwidth : 0 < width) : ofFixedInt format (Numerics.Representations.FixedInt.minCode width) hwidth = nar format

The reserved integer word converts to NaR, independently of the posit format.

theorem FloatLib.Floats.Formats.Posit.Model.ofFixedInt_eq_roundRat {format : Format} {width : ℕ} (value : Numerics.Representations.FixedInt width) (hwidth : 0 < width) (hvalue : value ≠ Numerics.Representations.FixedInt.minCode width) : ofFixedInt format value hwidth = roundRat format ↑value.toInt

Every non-sentinel integer undergoes one rounding of its exact signed value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toFixedInt_nar {width : ℕ} (format : Format) (hwidth : 0 < width) : toFixedInt width (nar format) hwidth = Numerics.Representations.FixedInt.minCode width

NaR converts to the reserved integer word at every positive width.

theorem FloatLib.Floats.Formats.Posit.Model.toFixedInt_eq_of_inRange {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) : toFixedInt width value hwidth = Numerics.Representations.FixedInt.ofInt (Numerics.roundRatEven q)

A finite posit whose rounded integer fits is encoded without wraparound.

theorem FloatLib.Floats.Formats.Posit.Model.toFixedInt_eq_minCode_of_not_inRange {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : ¬Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) : toFixedInt width value hwidth = Numerics.Representations.FixedInt.minCode width

A finite posit whose rounded integer is out of range produces the sentinel.

theorem FloatLib.Floats.Formats.Posit.Model.toInt_toFixedInt_of_inRange {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {q : ℚ} (hvalue : value.toRat? = some q) (hrange : Numerics.Representations.FixedInt.InRange width (Numerics.roundRatEven q)) : (toFixedInt width value hwidth).toInt = Numerics.roundRatEven q

Decoding an in-range conversion gives the exact nearest-even integer.

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

For a finite posit, sentinel output means either overflow after rounding or a rounded result equal to the signed minimum. The latter is an in-range integer with the same reserved bits.

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

A finite conversion without rounded overflow has absolute error at most one half.

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

At an exact half-integer, the converted integer is even, provided it is in range. The remainder condition expresses a fractional magnitude of exactly one half, for either sign.

theorem FloatLib.Floats.Formats.Posit.Model.toFixedInt_eq_of_int {format : Format} {width : ℕ} (value : Model format) (hwidth : 0 < width) {integer : ℤ} (hvalue : value.toRat? = some ↑integer) (hrange : Numerics.Representations.FixedInt.InRange width integer) : toFixedInt width value hwidth = Numerics.Representations.FixedInt.ofInt integer

A finite posit that denotes an in-range integer converts to that integer exactly.

theorem FloatLib.Floats.Formats.Posit.Model.toFixedInt_ofFixedInt {format : Format} {width : ℕ} (value : Numerics.Representations.FixedInt width) (hwidth : 0 < width) (hvalue : value ≠ Numerics.Representations.FixedInt.minCode width) (hexact : (roundRat format ↑value.toInt).toRat? = some ↑value.toInt) : toFixedInt width (ofFixedInt format value hwidth) hwidth = value

An integer round trip is exact when its Section 4.1 posit rounding still denotes that integer and its input word is not the sentinel. Representability is essential here.