Correctness of standard posit quire operations #
The executable quire operations agree with their exact coefficient, dyadic, and rational semantics. The refinement theorems cover these operations from Posit Standard (2022), §5.11:
pToQ;qNegateandqAbs;qAddPandqSubP;qAddQandqSubQ;qMulAddandqMulSub; andqToP.
The runtime definitions live in Arithmetic.Runtime. Keeping the refinement layer separate lets
execution-only clients use the integer and dyadic kernels without importing the full proof graph.
References #
- Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Section 5.11, https://posithub.org/docs/posit_standard-2.pdf.
Converting posit NaR to a quire produces quire NaR.
Converting posit zero to a quire produces quire zero.
Converting quire NaR back to a posit produces posit NaR.
Converting quire zero back to a posit produces posit zero.
Exact coefficient and rational refinement theorems #
The standard quire scale is no greater than the decoded scale of any nonzero finite posit.
For widths of at least three this follows from the format-wide regime bound. The two-bit standard
format is the only arithmetic boundary case: its two ordinary nonzero words are 1 and -1, both
at scale zero.
Every ordinary posit dyadic aligns exactly with the least-significant bit of its associated quire.
This supplies the conversion kernel's scale condition at every width, including the two-bit boundary format.
Every ordinary decoded posit significand fits below its complete encoded modulus.
The dyadic scale of every ordinary posit is below four times its encoded width.
Aligning an ordinary posit to the quire scale requires at most twelve shift bits per posit bit.
This linear bound suffices to prove that conversion fits in the standard 16n-bit quire.
The magnitude of the integer coefficient produced by posit-to-quire alignment is strictly below the quire's signed half-range.
Every ordinary posit converts to an ordinary quire coefficient without overflow.
Ordinary quire negation stores the exact negated coefficient.
Ordinary quire negation refines exact rational negation.
Successful exact quire addition stores the mathematical coefficient sum.
Successful exact quire addition refines rational addition at the shared fixed scale.
Successful exact quire subtraction stores the mathematical coefficient difference.
Successful exact quire subtraction refines rational subtraction at the shared fixed scale.
The dyadic accumulation kernel propagates quire NaR.
An increment whose stored exponent is below the quire scale produces quire NaR.
Otherwise coefficientOfDyadic would clamp the negative shift to zero. The guard does not inspect
trailing zeros in the significand, so it may reject a dyadic whose value is nevertheless aligned.
Once the accumulator is ordinary and the increment is aligned, the kernel is exactly
ofCoefficient applied to the coefficient sum.
An aligned increment whose exact coefficient sum overflows produces quire NaR.
Successful dyadic accumulation stores the exact coefficient sum.
The shared dyadic accumulation kernel refines exact rational addition whenever the dyadic aligns to the quire scale and the resulting coefficient is ordinary.
Adding an ordinary posit to an ordinary quire refines exact rational addition whenever the resulting fixed-point coefficient remains ordinary.
Decoded posits satisfy the scale condition automatically. The remaining range hypothesis excludes overflow and the reserved NaR coefficient.
Successful posit accumulation stores the exact coefficient sum.
Adding an ordinary posit whose exact coefficient sum overflows the quire produces NaR.
Subtracting an ordinary posit from an ordinary quire refines exact rational subtraction whenever the resulting fixed-point coefficient remains ordinary.
As for addition, decoded posits align with the associated quire. The remaining range hypothesis excludes overflow and the reserved NaR coefficient.
Every ordinary posit dyadic lies at or above the smallest positive posit exponent.
Zero uses the exact carrier's conventional exponent zero. A finite nonzero value uses the global representation bound proved from the mandatory negative-regime terminator.
The associated quire scale is twice the smallest positive posit exponent.
Every exact product of two ordinary posits aligns with the associated quire scale.
Exact fused product accumulation refines rational multiplication followed by exact quire addition whenever the resulting coefficient is ordinary.
Successful fused product accumulation stores the exact coefficient sum.
Accumulating an exact product whose coefficient sum overflows the quire produces NaR.
Together with toRat?_qMulAdd_of_ordinary this characterizes qMulAdd on ordinary inputs: the
result is exact while the coefficient stays ordinary and NaR as soon as it does not.
Exact fused product subtraction refines rational subtraction whenever the resulting coefficient is ordinary.
Posit-to-quire conversion preserves exact rational meaning when the standard scale and quire-range invariants are supplied.
toRat?_pToQ supplies both invariants for every ordinary posit. This local form also allows
specialized decoders to supply their own alignment and range proofs.
Posit-to-quire conversion preserves exact rational meaning for every Posit Standard (2022) value.
NaR maps to quire NaR. Every ordinary value is proved to align with the standard quire scale and to lie strictly inside its signed coefficient range, so this theorem has no caller-supplied side conditions.
Quire-to-posit conversion agrees with Posit Standard (2022) rational rounding.
An ordinary quire rounds its exact rational value once; the reserved quire NaR maps to the unique posit NaR instead of being assigned a finite or infinite numerical value.