Exactly rounded posit algebraic functions

Reciprocal square root, hypotenuse, and fused triple multiplication evaluate their rational intermediates exactly and round only the final result. In particular, an intermediate product cannot overflow or underflow the posit format. Square roots use exact comparisons with squared posit rounding boundaries, including the standard's appended-bit tie rule.

Reference

• Posit Standard (2022), §§4.1–4.2 and 5.5–5.7

@[inline]

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

Reciprocal square root, rounded once. Nonpositive inputs and NaR produce NaR.

The exact identity 1 / sqrt x = sqrt (1 / x) reduces this operation to rational square-root rounding without first rounding either the reciprocal or the square root.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.hypot {format : Format} (left right : Model format) : Model format

Hypotenuse sqrt (a² + b²), rounded once; either NaR input produces NaR.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.fMM {format : Format} (left right third : Model format) : Model format

Fused triple multiplication a * b * c, rounded once; any NaR input produces NaR.