Correctness of exact rational-to-posit rounding #
The executable rational-to-posit specification in Rounding.Runtime satisfies search,
threshold, round-trip, and sign laws. Import this module for these proofs, or import the
FloatLib.Floats.Formats.Posit family entry point for the complete public interface.
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.
Bounded bisection never reaches its exclusive upper endpoint.
This structural range fact does not require monotonicity of accept; every recursive branch
retains a nonempty half-open interval and eventually returns one of its lower endpoints.
Bounded bisection never returns below its initial lower endpoint.
Bounded bisection is monotone under pointwise inclusion of accepted candidates.
The theorem is independent of monotonicity in the candidate index. It only uses that changing a rejected midpoint to accepted moves the active interval upward.
Bounded bisection depends only on predicate values strictly inside its current interval.
This lets semantic monotonicity replace the exact-rational comparison predicate with a plain code prefix without making any claim about out-of-range natural arguments.
Bounded bisection exactly recovers a cutoff when the accepted codes form a natural-number prefix.
The interval invariant is lower ≤ cutoff < upper. The span bound states that the remaining
interval contains at most 2 ^ fuel unit steps, so every nontrivial midpoint leaves at most half
the old span. This theorem is independent of posit decoding and can therefore be reused by every
exact comparison domain that drives the same search.
The fuel and initial interval used by an n-bit posit search recover every nonnegative finite
code when the comparison predicate is the corresponding code prefix.
A candidate bracketed by its exact value and successor is the reference lower code.
Direct arithmetic packers use this theorem to identify a constructed candidate with the search result by proving bounds against the candidate and its successor.
Once the lower-code search reaches maxPos, positive rounding must return maxPos.
This endpoint fact is independent of how an execution kernel established the lower code. Direct dyadic, quotient, and square-root packers can therefore share the final reference-rounding argument.
Searching for the exact value of a nonnegative finite code recovers that code at every width.
The standard's appended-one rounding boundary is strictly above its retained lower code.
The proof embeds the lower n-bit code as the even (n + 1)-bit code U0, then applies the
global unsigned-code ordering theorem to the adjacent code U1.
Positive-code rounding is a left inverse of exact decoding on the complete nonnegative finite interval.
This is the arbitrary-width encoder round-trip theorem. It combines global decoder monotonicity, exact bisection recovery, and the standard's appended-bit boundary rather than relying on small-width enumeration.
Model-valued positive rounding exactly re-encodes every nonnegative finite code.
The public exact-rational rounding specification re-encodes every nonnegative finite posit.
Together with whole-word two's-complement symmetry, this supplies the canonical arbitrary-width decode/encode round-trip used by optimized backends.
The total positive-code helper preserves exact zero.
The square-root code of zero is the zero code.
The rounded square root of zero is the posit zero.
Rounding a negative rational is encoding-level negation of rounding its magnitude.