Executable exact rational-to-posit rounding

The width-generic reference conversion searches the monotone positive encoding with at most format.bits bisection comparisons. Between adjacent n-bit codes U and W, the standard's exact boundary is the (n + 1)-bit posit whose encoding is U1; this is not generally the arithmetic midpoint of the decoded values. A tie at that boundary is resolved by the low bit of U. Negative inputs use whole-word two's-complement symmetry.

This implementation is the executable rounding specification. Packed word and limb kernels are proved equal to it. Search and round-trip theorems live in Rounding.Proof.

The Posit Standard (2022) also gives the extreme intervals explicit behavior: magnitudes above maxPos saturate to signed maxPos, while every nonzero magnitude below minPos rounds to signed minPos. Zero is represented exactly.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Section 4, https://posithub.org/docs/posit_standard-2.pdf.
• John L. Gustafson, Standard Posit Arithmetic, Supercomputing Frontiers and Innovations 9(1), 2022, https://doi.org/10.14529/jsfi220102.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.lowerCodeByBisection (accept : ℕ → Bool) : ℕ → ℕ → ℕ → ℕ

Shared bounded bisection over an unsigned code interval.

accept code states that code is still on the lower side of the target boundary. Separating the search from the comparison domain lets the exact-rational specification and certified integer implementations follow literally the same control flow.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.lowerCodeForPositive (format : Format) (target : ℚ) : ℕ

Greatest candidate code found below an exclusive upper bound.

The initial interval is [0, signMaskNat). Its size is a power of two, so format.bits bisections are sufficient to isolate adjacent codes. Exact rational comparison avoids host-float double-rounding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.minPositiveRat (format : Format) : ℚ

Exact smallest positive value of a posit format.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundingThreshold (format : Format) (lowerCode : ℕ) : ℚ

Exact standard rounding boundary above an n-bit lower code.

If U is the lower code, Section 4.1 defines the boundary as the value of the (n + 1)-bit word U1. Numerically that word has unsigned code 2 * U + 1.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundPositiveCode (format : Format) (target : ℚ) : ℕ

Round a nonnegative exact rational to a nonnegative posit code.

This helper is total, returning zero for nonpositive input. Its intended positive-input behavior matches Section 4.1 exactly: nonzero underflow selects minPos, overflow selects maxPos, and each interior interval uses the appended-bit boundary with ties to an even retained low bit.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundPositiveRat (format : Format) (target : ℚ) : Model format

Round a positive rational to a nonnegative posit model.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.lowerSqrtCode (format : Format) (radicand : ℚ) : ℕ

For a nonnegative radicand, the greatest nonnegative code whose squared value does not exceed it.

Comparing squares is enough because positive posit codes are ordered by their unsigned word. It also keeps square-root rounding fully executable over exact rationals: no approximate real square root or host floating-point operation enters the specification.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundSqrtCode (format : Format) (radicand : ℚ) : ℕ

Round the nonnegative square root of an exact rational to a nonnegative posit code.

The comparisons square each exact standard threshold. This decides the rounding of irrational roots without introducing an approximate square-root oracle.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundSqrtRat (format : Format) (radicand : ℚ) : Model format

Round the nonnegative square root of an exact rational using only rational comparisons.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundRat (format : Format) (value : ℚ) : Model format

Round an exact rational to the configured posit using the Posit Standard rule.

This conversion does not pass through Float, Float32, MPFR, or another destination format.