Binary-interchange conversion proofs #
Every configured and static-byte carrier adapter shares these conversion equations and numerical contract. For default IEEE finite rounding, the nearest-value clause follows from the real rounding bridge and the generic nearest-point theorem. Complete outcome equality keeps all word, status, and policy guarantees.
For a rounding mode with an IEEERoundingMode direction,
finiteStatus_of_ieeeRoundingMode?_eq_some gives the conversion status from that direction's exact
classifiers. For nearest-away rounding, finiteStatus_of_nearestAway names them:
rationalNearestAwayOverflowsScaled and rationalIsTinyAfterRoundingScaled with the nearest-even
tininess boundary.
The significand-based calculation roundedSignificandStatus serves stochastic rounding. For
nearest-away rounding, roundedSignificandStatus_nearestAway shows that it matches the
nearest-away overflow classifier
and the comparison with underflowMidpoint. The tininess classifier also counts a tiny delivered
value, so finiteStatus_eq_roundedSignificandStatus_of_nearestAway adds the engine's result: for
the value that Policy.roundRat delivers, the two calculations give the same status under every
overflow and underflow policy.
The context changes only a possible zero sign, never the exact rational sum.
The context changes only a possible zero sign, never the exact rational difference.
The default context uses the ordinary nearest-even sign rule of SignedRat.
Default-context subtraction is ordinary SignedRat subtraction.
Rounding to nearest gives the canonical context, so (mode := .nearest) changes nothing.
Downward exact cancellation uses the disjunction of the operand signs.
Finite observations use the exact rational binary quantizer.
Infinity observations are governed by the infinity policy alone.
Exceptional observations are governed by the exceptional policy alone.
The canonical IEEE rational rounder selects a nearest finite value whenever its result is finite.
This includes signed zero. The independent real grid has no infinity, so nonfinite results are
covered by the complete outcome clause of specWith.
Descriptor rounding semantics establish the nearest clause for every carrier adapter.
An outcome satisfies specWith exactly when it is the outcome of runWith.
Rejecting infinity fails with the source infinity and its sign, for every carrier.
Rejecting an exceptional observation preserves its complete common classification.
Default conversion of an observed binary NaN agrees with Model.cast in value and in
the invalid flag, for every rounding mode and for equal or unequal descriptors.
The sign and signaling class travel with the observation, and the destination NaN is
Model.propagatedNaN on the IEEE payload, as IEEE 754-2019 §6.2.3 and §7.2 require. A destination
with no NaN encoding is excluded here and covered by runWith_default_nan_of_encoding_finite:
conversion then fails, while Model.cast returns positive zero and raises invalid.
Default conversion of an observed binary NaN into a destination with no NaN encoding fails with
the source NaN as the reported exceptional value, and Model.cast on the same source
raises invalid.
The two paths agree that the conversion is invalid. ExecFloat reports a failure, while the
descriptor model delivers positive zero and sets the invalid flag.
Significand-based status of nearest-away rounding #
With nearest-away rounding, the significand-based status calculation matches the nearest-away
overflow classifier and the comparison with underflowMidpoint: a nonzero magnitude overflows
exactly when rationalNearestAwayOverflowsScaled says so, at or above the top finite midpoint, and
it is tiny exactly below underflowMidpoint.
finiteStatus sends nearest-away rounding to the classifiers, as finiteStatus_of_nearestAway
states. The tininess classifier also counts a tiny delivered value, and
finiteStatus_eq_roundedSignificandStatus_of_nearestAway uses this theorem to show that both
give the same status for the value that Policy.roundRat delivers.
Conversion status of the rounding directions #
For a rounding mode with an IEEERoundingMode direction, conversion status is built from the
exact classifiers of that direction: rationalRoundingOverflows for overflow and
rationalIsTinyAfterRoundingScaled for tininess, under every overflow and underflow policy.
Nearest-away conversion status is the status of the nearest-away classifiers.
The top finite midpoint overflows, and a magnitude is tiny exactly below underflowMidpoint or
when the delivered value is tiny, as for nearest-even rounding. This holds under every overflow and
underflow policy.
For the value that Policy.roundRat delivers, nearest-away conversion status is the status
assembled from roundedSignificandStatus, the significand rounded with an unbounded exponent range,
with the same inexactness, flush-to-zero underflow, and saturation as finiteStatus.
This holds under every overflow and underflow policy. The two tininess bits differ only when the
delivered value is tiny and the exact magnitude is zero or at least underflowMidpoint. The engine
never delivers a tiny value at or above underflowMidpoint, and at an exact zero the result is
exact, so the underflow flag agrees.