IEEE exception status for format-parameterized Model #
The value operations are pure and take their rounding mode as an argument. This module pairs their results with the five IEEE exception indicators and a ternary value. Tininess is detected after rounding, and underflow is raised exactly when a tiny result is inexact.
Overflow is classified from the precision-rounded result with an unbounded exponent range, as in IEEE 754-2019 §7.4 and the GNU MPFR manual's exception definition: https://doi.org/10.1109/IEEESTD.2019.8766229 and https://www.mpfr.org/mpfr-current/mpfr.html#Exceptions.
The ternary value follows MPFR's return-value convention
(https://www.mpfr.org/mpfr-current/mpfr.html#Rounding-Modes): it compares the delivered value
with the exact result, so .lt means the delivered value is below it. Each producer computes it
by an exact comparison with the exact witness its status uses, and integral rounding compares with
its input, as mpfr_rint does. For the producers built on dyadicRoundingOutcome and
rationalRoundingOutcomeScaled, compiled code makes that comparison once and, below the overflow
threshold, reads the inexact flag from it (dyadicRoundingOutcome_eq_internal,
rationalRoundingOutcomeScaled_eq_internal). Square root reads inexact from its own squared-root
comparison (sqrt_inexact_iff). Only integral rounding computes inexact apart from its
ternary value.
The arithmetic producers are the status kernels Model.Internal.Status.add through
Model.Internal.Status.sqrt, and user code calls them as Model.add x y (status := true) and its
siblings in Arithmetic.Runtime. Results without an exact real counterpart have fixed
conventions, documented at IEEEOutcome.ternary.
A format-parameterized executable value paired with its IEEE exception status and its ternary value.
- value : Model fmt
Delivered floating-point result.
- status : Numerics.IEEEStatus
Exception indicators raised while computing
value. - ternary : Ordering
The delivered value compared with the exact result, as MPFR's ternary value:
.ltwhen the delivered value is below the exact result,.eqwhen they are equal,.gtwhen it is above.Results that have no exact real counterpart follow fixed conventions. A NaN from a NaN operand or an invalid operation, an exceptional placeholder such as the positive zero that a fully finite format delivers for an invalid operation, and an infinity that is itself the exact result all have
.eq. A finite exact value delivered as an overflow infinity has.gtwhen it is positive and.ltwhen it is negative. The NaN that replaces the infinity in a format without one gets the same value by convention. An exact infinity delivered as a saturated finite value has.ltfor+∞and.gtfor-∞, and so, by convention, has an exact infinity delivered as that overflow NaN. These NaN conventions do not order the NaN itself.The structure does not tie inexactness to a nonzero ternary value. A saturated integral rounding can return its own input with
inexactraised, and a division by zero that delivers a saturated value raises onlydivideByZero, so any relation between the two holds only for particular operations.
Instances For
Instances For
The default outcome is an exact +0 with a clear status: its value is the default all-zero word
and its ternary value is .eq.
Pair a value with the ternary value .eq and a status that is clear or raises only invalid
operation.
Exceptional arithmetic paths use it for NaNs, exact infinities and placeholders, whose
IEEEOutcome.ternary convention is .eq, and for exact finite results such as an exact zero sum.
The constructor proves nothing about exactness. For a remainder, remainder_exact proves it on
IEEE descriptors.
Instances For
Whether a finite rounded result is zero or subnormal.
Instances For
Exact positive value of the smallest normal number in fmt.
Instances For
Largest positive number below minNormalDyadic fmt on the format's precision grid with an
unbounded exponent range. Its distance from the smallest normal is half one subnormal step.
Instances For
Positive boundary used by after-rounding tininess detection.
Tininess after rounding is determined by first rounding to the destination precision with an
unbounded exponent range. Immediately below the smallest normal value, that unbounded grid has
half the subnormal spacing, so the midpoint between minNormal and its predecessor is one quarter
of a subnormal step below minNormal. Both nearest modes take the midpoint itself to minNormal,
whose significand is even and whose magnitude is the larger one, so it is not tiny.
Instances For
Whether a dyadic result is tiny after rounding to the destination precision with an unbounded exponent range.
Most tiny results show up as zero or subnormal encodings. A result delivered as minNormal
needs a mode-sensitive boundary:
- both nearest modes use the midpoint between
minNormaland its unbounded-grid predecessor, which itself rounds tominNormal; - a direction that rounds the magnitude up is tiny up to and including that predecessor;
- a direction that truncates the magnitude is tiny for every magnitude strictly below
minNormal.
Instances For
Exact positive dyadic value of the largest finite number in fmt.
Instances For
Whether an exact dyadic magnitude exceeds the finite range of fmt.
Instances For
Positive midpoint between the largest finite value and the next magnitude on the same binary grid.
Nearest-even overflow is decided at this boundary. The midpoint itself overflows exactly when the largest finite significand is odd, because the conceptual next significand is then even.
Instances For
First grid magnitude beyond the largest finite value.
Instances For
Whether the largest finite significand is odd.
Instances For
Whether nearest-even rounding of an exact dyadic magnitude signals overflow.
Instances For
Whether nearest-away rounding of an exact dyadic magnitude signals overflow.
Nearest-away rounding is decided at the same top finite midpoint as nearest-even rounding, but the midpoint itself always overflows: a tie rounds away from zero whatever the parity of the largest finite significand.
Instances For
Whether truncating an exact dyadic magnitude still exceeds the finite range.
Instances For
Whether rounding an exact dyadic signals overflow.
The nearest modes use the top finite midpoint, which overflows under nearest-away rounding and
under nearest-even rounding only when the largest finite significand is odd. A directed mode that
increases the magnitude overflows above maxFinite, while a mode that decreases the magnitude
overflows only from overflowLimit on. For conventional IEEE encodings, that limit starts the next
binade. For
encodings that reserve a terminal fraction pattern, it can lie within the same binade.
Instances For
Classify rounding an exact dyadic to rounded under mode.
Finite results use the proof-guided exact decoder. An exceptional rounded argument is classified
as overflow or invalid, never as a clear status.
Instances For
Ternary value of delivering rounded for the exact dyadic result exact.
A finite delivery is compared exactly with exact by cmpDyadic, the bounded comparison that
dyadicRoundingStatus uses for inexactness. A non-finite delivery stands for the overflow of a
finite exact value and gets the sign of exact: .gt for a positive and .lt for a negative
value. For an infinity this is the order, and for the NaN that replaces the infinity in a format
without one it is the convention of IEEEOutcome.ternary.
Instances For
The outcome of delivering value for the exact dyadic result exact.
Its status is dyadicRoundingStatus and its ternary value is dyadicTernary. Compiled code uses
Internal.Status.dyadicRoundingOutcome, which builds the same record with one comparison of the
delivered value against exact.
Instances For
The status and the ternary value of delivering value for exact, from one comparison.
A finite delivery is decoded once and compared with exact once, and that comparison is the
ternary value of dyadicTernary. In the finite branch without overflow, inexactness is its
difference from .eq: dyadicRoundingStatus compares in the other orientation, and the two tests
agree by cmpDyadic_swap. The overflow test still comes first in the status and raises inexact
by itself, the non-finite branch is that of dyadicRoundingStatus and dyadicTernary, and
tininess is computed only for an inexact result.
Instances For
Compiled form of dyadicRoundingOutcome, built from one
Internal.Status.dyadicRoundingClassification call.
The record is built outside every branch, so a caller that keeps only the value lets the compiler drop the classification call altogether. Classification is a separate function for the same reason: its branches, inlined into such a caller, would survive as dead tests.
Instances For
Compiled code builds every dyadic rounding outcome with one delivered-versus-exact comparison on the finite branch.
The equality holds for every exact value and every delivered value, finite or not. It is registered before every producer in this module and in importing modules, so each of them is compiled with the shared comparison.
Ternary value of delivering value when the exact result is the infinity with sign negative.
The infinity itself has .eq. Any other delivery has .lt for +∞ and .gt for -∞. For the
saturated finite value of a fully finite format this is the order, and for the NaN that a format
without infinities returns instead it is the convention of IEEEOutcome.ternary, chosen so that
the value agrees with the overflow and inexact flags that casts and reductions raise there.
Instances For
Exact equality between (numerator / denominator) * 2^exponent and a signed dyadic.
Instances For
Whether a positive scaled rational magnitude exceeds the finite range of fmt.
Instances For
Whether nearest-even rounding of a positive scaled rational signals overflow.
Instances For
Whether nearest-away rounding of a positive scaled rational signals overflow.
As for dyadics, the top finite midpoint itself overflows whatever the parity of the largest finite significand.
Instances For
Whether truncating a scaled rational magnitude still exceeds the finite range.
Instances For
Whether rounding an exact signed scaled rational signals overflow.
The nearest modes use the top finite midpoint, as for dyadics. The sign determines whether an
infinity-directed mode increases or decreases magnitude. Magnitude-increasing rounding, rounding
away from zero included, overflows above maxFinite, while truncating rounding uses
overflowLimit.
Instances For
Whether rounding an exact rational signals overflow.
Instances For
Whether a scaled rational result is tiny after rounding to the destination precision with an unbounded exponent range.
As with dyadics, an encoded zero or subnormal is tiny. A result delivered as minNormal uses the
nearest midpoint, the unbounded-grid predecessor, or minNormal itself according to the rounding
direction and sign.
Instances For
Classify rounding an exact scaled signed rational to rounded under mode.
For a nonzero denominator, finite results are compared with the exact rational. Exceptional
results are classified as overflow or invalid, as in dyadicRoundingStatus. Division handles a
zero denominator before calling this classifier.
Instances For
Ternary value of delivering rounded for the exact signed rational
±(numerator / denominator) * 2^exponent, where sign is the sign.
A finite delivery is compared exactly with the rational by compareDyadicScaled?, the comparison
that rationalRoundingStatusScaled uses for inexactness, with its orientation reversed: that
comparator orders the rational before the delivered value. A non-finite delivery gets the sign,
as in dyadicTernary. With a zero denominator, which no operation passes, a finite delivery gives
.eq.
Instances For
The outcome of delivering value for the exact signed rational
±(numerator / denominator) * 2^exponent, where sign is the sign.
Its status is rationalRoundingStatusScaled and its ternary value is rationalTernaryScaled.
Compiled code uses Internal.Status.rationalRoundingOutcomeScaled, which builds the same record
with one comparison of the delivered value against the rational.
Instances For
The status and the ternary value of delivering value for the exact scaled rational, from one
comparison.
A finite delivery is decoded once and compared with the rational by compareDyadicScaled? once.
Inexactness is whether that comparison differs from some .eq, as in
rationalRoundingStatusScaled, and the ternary value reverses its orientation, as in
rationalTernaryScaled. Inexactness is not read off the ternary value: with a zero denominator the
comparator returns none, which is inexact and still has the ternary value .eq. The overflow
test still comes first in the status, the non-finite branch is that of both classifiers, and
tininess is computed only for an inexact result.
Instances For
Compiled form of rationalRoundingOutcomeScaled, built from one
Internal.Status.rationalRoundingClassificationScaled call.
As for Internal.Status.dyadicRoundingOutcome, the record is built outside every branch, so a
caller that keeps only the value lets the compiler drop the classification call altogether.
Instances For
Compiled code builds every scaled rational rounding outcome with one delivered-versus-exact comparison on the finite branch.
The equality holds for every numerator and denominator, a zero denominator included, and every delivered value. It is registered before every producer in this module and in importing modules, so each of them is compiled with the shared comparison.
Addition in rounding direction mode, with IEEE exception status and ternary value: the kernel
of Model.add x y (mode := mode) (status := true).
Finite operands compare the delivered value with their exact dyadic sum. An infinite or NaN
operand gives an exact infinity or a NaN, with the ternary value .eq.
Instances For
Subtraction in rounding direction mode, with IEEE exception status and ternary value: the
kernel of Model.sub x y (mode := mode) (status := true).
Instances For
Multiplication in rounding direction mode, with IEEE exception status and ternary value: the
kernel of Model.mul x y (mode := mode) (status := true).
Finite operands compare the delivered value with their exact dyadic product. An infinite or NaN
operand gives an exact infinity or a NaN, with the ternary value .eq.
Instances For
Division in rounding direction mode, with IEEE exception status and ternary value: the kernel
of Model.div x y (mode := mode) (status := true).
A finite nonzero quotient compares the delivered value with the exact rational quotient. A finite
nonzero value over zero has an exact infinity, so the ternary value is exactInfinityTernary of
the delivered overflow result. Zero over a nonzero finite value is exact, and invalid or NaN
operands give the ternary value .eq.
Instances For
Fused multiply-add in rounding direction mode, with IEEE exception status and ternary value:
the kernel of Model.fma x y z (mode := mode) (status := true).
Finite operands compare the delivered value with the exact dyadic x * y + z. An infinite or NaN
operand gives an exact infinity or a NaN, with the ternary value .eq.
IEEE 754-2019 Section 7.2 leaves it implementation defined whether fma(0, ∞, c) signals invalid
when c is a quiet NaN. This implementation signals invalid for that case: the invalid product
0 × ∞ is reported whether or not the addend is a quiet NaN, whereas add and mul only
report an operand-generated invalid operation when no operand is a NaN.
Instances For
Ternary value of delivering rounded for the square root of the nonnegative dyadic radicand.
For nonnegative a and b, a < √b holds exactly when a * a < b, and likewise for equality.
So the delivery, which is the rounded root, is decoded once and squared exactly, and the square is
compared with radicand: the comparison is exact and never evaluates the square root of
radicand. It is meaningful only for a nonnegative radicand and a nonnegative delivery, which
Internal.Status.sqrt ensures before calling it. A non-finite delivery gets .gt, the overflow
convention of dyadicTernary for a positive exact value.
Instances For
Whether the square root of the dyadic radicand, taken as a magnitude, lies below the
after-rounding tininess boundary of mode.
The boundaries are those of dyadicIsTinyAfterRounding: the underflow midpoint for both nearest
modes, minNormal for the directions that truncate a positive value, and the unbounded-grid
predecessor for the directions that round it up. On nonnegative values, comparing √radicand with
a positive boundary is equivalent to comparing radicand with its square, so the radicand is
compared with the squared boundary and no approximate square root enters the test.
Instances For
Square root in rounding direction mode, with IEEE exception status and ternary value: the
kernel of Model.sqrt x (mode := mode) (status := true).
A NaN raises invalid only when it is signaling. Among the other inputs with a set sign bit, a
zero raises nothing and every other value raises invalid. An input with a clear sign bit is
decoded once: +∞ and +0 raise nothing, and a positive finite input compares the delivered root
through its exact square with dyadicSqrtTernary. That comparison is the ternary value, and
the result is inexact exactly when it is not .eq, that is, when the delivered value is not the
real square root (sqrt_inexact_iff). Tininess is tested only for an inexact result:
a zero or subnormal delivery is tiny, and otherwise dyadicSqrtIsTinyAfterRounding
decides. That comparison is skipped when fmt.fracWidth + 1 < fmt.exponentBias, because then the
least positive radicand already exceeds the square of every boundary
(dyadicSqrtIsTinyAfterRounding_eq_false). NaNs, zeros, +∞, and the invalid square
root of a negative value have the ternary value .eq. sqrt_status_of_toDyadic and its
siblings restate the outcome case by case.
A module that calls it with a closed format compiles a copy specialized to that descriptor term by
@[specialize fmt] (calls that spell the same descriptor alike share it), and other callers run the
compiled generic body.