Configured binary-interchange conversion proofs #
Configured conversion inherits the descriptor's default IEEE nearest-value contract and preserves the complete outcome for every context.
It is the final transport layer between descriptor-level conversion semantics and the public packed carrier. The statements do not mention storage selection: every configured backend must decode to the same converted value and status, so moving from a native word to arbitrary-width storage cannot change the numerical contract.
Finite observations are handled by the configured binary finite quantizer.
Infinity observations are handled by the infinity policy alone.
Exceptional observations are handled by the exceptional policy alone.
The configured carrier inherits the descriptor's nearest-value and complete-outcome clauses.
An outcome satisfies the semantic contract exactly when it is the outcome of run, configured
word and status fields included.
A successful default IEEE conversion satisfies the nearest-value predicate after decoding.
The installed exact decoder is the public signed-rational decoder.
A default-context finite conversion is the canonical nearest-even rational rounder applied to the sign bit and magnitude of the signed rational.
The delivered value is Model.roundRat. For conventional IEEE destinations and finite results,
Model.toReal_roundRatScaled_eq_roundAt relates that rounder to nearest-even rounding over ℝ.
Converting an exact negative zero preserves its sign when the destination supports negative zero.
For an encoding with one unsigned zero, zero true is that encoding's positive zero, so the
statement also covers FNUZ destinations.
Rejecting infinity fails with the source infinity and its sign.
Rejecting an exceptional observation preserves its complete common classification.
A configured NaN decodes to its diagnostic payload without the quiet bit, sign, and class.
Default conversion of a decoded configured NaN is Model.cast on the source model.
An IEEE destination keeps the sign and any payload that fits, and an oversized payload becomes zero.
Maximum-NaN encodings keep only the sign, while FNUZ has a single NaN. Invalid is raised exactly
for a signaling source. The destination must have a NaN encoding. When it has none,
run_default_decode_of_isNaN_of_encoding_finite shows that conversion fails while
Model.cast raises invalid.
Default conversion of a decoded configured 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.
ExecFloat reports a failure because the destination has no NaN to deliver, while the descriptor
model returns positive zero with the invalid flag set. Both paths classify the conversion as
invalid.