Basic posit functions

Absolute value, sign, integer rounding, and representation successor/predecessor from Section 5.2 of the 2022 Posit Standard. Negation is defined with the model.

next and prior wrap over the complete bit vector, including NaR, as specified by the standard. Other posit-valued functions preserve NaR. Integer rounding uses exact rational decoding, Rat.floor or Rat.ceil, and the shared posit rounder.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 5.1--5.2, https://posithub.org/docs/posit_standard-2.pdf.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.next {format : Format} (value : Model format) : Model format

Lexicographic successor of the complete representation, wrapping modulo 2 ^ format.bits.

Unlike ordinary real-valued functions, next does not propagate NaR: it advances from the NaR word to the following encoded word.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.prior {format : Format} (value : Model format) : Model format

Lexicographic predecessor of the complete representation, wrapping modulo 2 ^ format.bits.

As required by the standard, this is the exact inverse of next, including at zero, NaR, and the unsigned wrap boundary.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.prior_next {format : Format} (value : Model format) : value.next.prior = value

Taking the predecessor after the successor recovers every encoded word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.next_prior {format : Format} (value : Model format) : value.prior.next = value

Taking the successor after the predecessor recovers every encoded word.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.abs {format : Format} (value : Model format) : Model format

Standard absolute value.

The encoded order places NaR below zero, but whole-word negation fixes NaR, so this definition also has the required NaR propagation without assigning NaR a numerical sign.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.abs_zero (format : Format) : (zero format).abs = zero format

Absolute value fixes zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.abs_nar (format : Format) : (nar format).abs = nar format

Absolute value propagates NaR.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.sign {format : Format} (value : Model format) : Model format

Standard sign function.

NaR is checked before encoded comparisons because NaR is the least word but has no numerical sign. Positive and negative results are created by exact rounding of ±1.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.sign_zero (format : Format) : (zero format).sign = zero format

The standard sign function fixes the canonical zero word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.sign_nar (format : Format) : (nar format).sign = nar format

The standard sign function propagates NaR.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Model.nearestEvenInteger (value : ℚ) : ℤ

The shared exact nearest-even integer rounder, exposed through the posit API.

theorem FloatLib.Floats.Formats.Posit.Model.nearestEvenInteger_int (value : ℤ) : nearestEvenInteger ↑value = value

An exact integer is unchanged by nearest-even integer rounding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.nearestInt {format : Format} (value : Model format) : Model format

Nearest integer-valued posit, with an even-integer tie rule and NaR propagation.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.ceil {format : Format} (value : Model format) : Model format

Smallest integer-valued posit greater than or equal to the input, with NaR propagation.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.floor {format : Format} (value : Model format) : Model format

Largest integer-valued posit less than or equal to the input, with NaR propagation.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.nearestInt_nar (format : Format) : (nar format).nearestInt = nar format

Nearest-integer rounding propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ceil_nar (format : Format) : (nar format).ceil = nar format

Ceiling propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.floor_nar (format : Format) : (nar format).floor = nar format

Floor propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.nearestInt_zero (format : Format) : (zero format).nearestInt = zero format

Nearest-integer rounding fixes the canonical zero word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ceil_zero (format : Format) : (zero format).ceil = zero format

Ceiling fixes the canonical zero word.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.floor_zero (format : Format) : (zero format).floor = zero format

Floor fixes the canonical zero word.