Executable standard posit quire operations

Quire arithmetic implements the operations of Posit Standard (2022), §5.11. Every accumulation kernel works on the signed fixed-point coefficient. Posit operands decode to the shared exact dyadic carrier and are shifted directly to the quire's fixed scale. No operation normalizes through Rat.

The standard reserves the most-negative quire word for NaR. Consequently every checked result uses Model.ofCoefficient: NaR propagates, and either signed overflow or a result equal to the reserved word produces quire NaR.

The exact coefficient, dyadic, and rational refinement theorems live in Arithmetic.Proof.

References

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

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.addDyadic {format : Format} (accumulator : Model format) (increment : Numerics.Dyadic) : Model format

Add an exact dyadic increment to an ordinary quire.

This shared integer kernel underlies posit addition and fused product accumulation. The function is total and produces quire NaR in three cases: the accumulator is NaR, the increment's stored exponent is below the quire scale, or the exact coefficient sum is not an ordinary quire coefficient. The exponent check is sufficient for alignment; it can reject an otherwise aligned dyadic with trailing zeros in its significand. Decoded ordinary posits and their exact products always pass this check, so it only restricts direct callers of this kernel.

@[inline]

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

Convert a posit into the exact quire associated with the same descriptor.

@[inline]

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

Negate an ordinary quire; quire NaR remains quire NaR.

@[inline]

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

Absolute value of an ordinary quire; quire NaR remains quire NaR.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.qAddP {format : Format} (accumulator : Model format) (addend : Posit.Model format) : Model format

Add one posit exactly to a quire, producing NaR on exceptional input or quire overflow.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.qSubP {format : Format} (accumulator : Model format) (subtrahend : Posit.Model format) : Model format

Subtract one posit exactly from a quire, producing NaR on exceptional input or quire overflow.

@[inline]

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

Add two quires exactly, returning quire NaR on NaR input or signed overflow.

@[inline]

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

Subtract two quires exactly, returning quire NaR on NaR input or signed overflow.

@[inline]

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

Accumulate one exact posit product with no intermediate rounding.

Both posit operands must use the same format as the quire, enforced by the type.

@[inline]

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

Subtract one exact posit product from a quire with no intermediate rounding.

@[inline]

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

Round a quire once to its associated posit.

The ordinary path turns the fixed-point coefficient into a shared dyadic and applies the Posit Standard (2022) rounder, without constructing a Rat.