Native-word comparison of exact dyadic fields #
Fixed-width numerical formats frequently decode a finite value to a machine-word significand and
an unbounded exponent. Converting that significand to Nat before every candidate comparison is
unnecessary when the one required alignment shift still fits in a word.
The recognizer is representation-independent:
- execute the comparison with
UInt64shifts when the aligned operand provably fits; - otherwise call the arbitrary-precision exact comparator.
The arbitrary-precision branch is part of the algorithm, not an exceptional or unverified path.
Consequently every format can reuse this primitive. Significand alignment and comparison use
native words whenever the capacity guards hold. The refinement theorem lives in
DyadicCompare.Proof.
Whether shifting a nonnegative word significand left by shift preserves its exact value.
For a nonzero word, log2 + shift < 64 is precisely the capacity condition needed by the native
left shift. The proposition is decidable from machine-word data; its proof is erased after
compilation.
Instances For
Whether shifting a two-limb significand left by shift preserves its exact value.
For a nonzero significand, log2 + shift < 128 ensures that the shifted value fits in two limbs.
The proof argument is erased after compilation.
Instances For
Compare two nonnegative exact dyadics whose significands are native words.
Only the operand with the larger dyadic exponent needs alignment. If that shift stays within one
word, significand alignment and comparison use native operations. Large exponent gaps and
over-wide aligned values use the exact Nat implementation; exponent arithmetic uses Int.
Instances For
Compare a nonnegative two-word dyadic with a nonnegative one-word dyadic.
Values whose high limb is zero reuse compareNonnegative. For a nonzero high limb in the left
significand, the only possible alignment into the wider carrier is a shift of the right word.
The leading-bit capacity test recognizes exactly when that shift fits in 128 bits. If it does not
fit, the shifted right operand is necessarily larger than every UInt128; if the left exponent
is larger, the already-wide left operand is necessarily larger than the word target. Thus the
wide path keeps significands in fixed limbs. Exponent arithmetic still uses Int.
Instances For
Test whether a nonnegative word dyadic is strictly below an integral power of two.
For a nonzero significand, exponent + log2 significand is the exponent of its leading bit.
Comparing that scalar exponent avoids both alignment shifts and the arbitrary-precision branch
that a generic dyadic comparison needs when the exponent gap exceeds one machine word.