IEEE rounding modes for Model #
This type provides the five rounding-direction attributes of IEEE 754-2019: the two nearest modes,
which differ only at an exact tie, and the three directed modes. It also provides rounding away
from zero, GNU MPFR's MPFR_RNDA, which IEEE 754 does not define. The broader quantization-policy
vocabulary Numerics.RoundingMode also contains stochastic rounding.
This is the shared mode definition for executable rounding and its proofs. The helpers beside it
state how each direction treats the magnitude of a result, overflow, negation, and an exactly
cancelling sum. IEEERoundingMode.magnitudeRounding names the Numerics.MagnitudeRounding rule
that a direction applies to the magnitude of a result of known sign.
The constructors are nearest (ties to even), nearestAway, towardZero, up, down, and
away. Library code writes them with a leading dot, as in .up, and user code can
open FloatLib.Rounding to write the bare names.
References #
- IEEE Std 754-2019, "IEEE Standard for Floating-Point Arithmetic", Sections 4.3 and 6.3.
- The GNU MPFR Library manual, Section 4.4, "Rounding": https://www.mpfr.org/mpfr-current/mpfr.html#Rounding.
Deterministic rounding direction: the five IEEE 754-2019 rounding-direction attributes and rounding away from zero.
Operations take a direction as the option (mode := .up), nearest-even by default. After
open FloatLib.Rounding, user code can write the six constructors without the leading dot, as in
(mode := up).
- nearest : IEEERoundingMode
Round to the nearest representable value, breaking ties toward an even significand. This is IEEE 754-2019 roundTiesToEven.
- nearestAway : IEEERoundingMode
Round to the nearest representable value, breaking ties toward the neighbour of larger magnitude. This is IEEE 754-2019 roundTiesToAway.
- towardZero : IEEERoundingMode
Round toward zero.
- up : IEEERoundingMode
Round toward positive infinity.
- down : IEEERoundingMode
Round toward negative infinity.
- away : IEEERoundingMode
Round away from zero, to the neighbour of larger magnitude whenever the result is inexact. This is GNU MPFR's
MPFR_RNDA, which is not an IEEE 754 rounding-direction attribute.
Instances For
All constructors of IEEERoundingMode, in their shared traversal order.
Callers use it instead of repeating the enumeration, so update it when adding a constructor.
Instances For
A concise, stable name for diagnostics and interchange files.
These strings are a file format read by the MPFR oracle drivers, so they do not follow the
constructor names: nearest is "nearestEven", up is "towardPositive", down is
"towardNegative", and away is "awayFromZero". toString prints the constructor names.
Instances For
Print a mode as its constructor name, the spelling user code writes after (mode := ...).
The quantization-policy rounding mode with the same direction.
Numerics.RoundingMode also contains stochastic rounding, which has no constructor in
IEEERoundingMode, so this map is an embedding, not a bijection.
Instances For
Whether this mode, read as a directed rounding, moves an inexact result of the given sign away from zero.
This is the directed magnitude-up predicate. Rounding toward positive infinity increases the
magnitude of positive results, rounding toward negative infinity that of negative results,
rounding away from zero that of every result, and rounding toward zero never does. The two nearest
modes are not directed and give false for both signs. Tininess detection relies on that answer
at the midpoint just below the smallest normal number, which both nearest modes take up to the
normal number.
Instances For
Whether an overflowing result of the given sign takes the format's native overflow value instead
of saturating at the largest finite magnitude, as directedOverflow reads it.
Both nearest modes always do. A directed mode, rounding away from zero included, does so exactly
when it rounds that sign away from zero (IEEE 754-2019 Section 7.4). The native overflow value is
the signed infinity in IEEE encodings, a NaN in finite encodings that have one, and the largest
finite value otherwise (nativeOverflow).
Instances For
The mode that mirrors this one under negation: rounding -x with mode gives the negation of
rounding x with mode.negate.
Negation exchanges the two infinity directions and fixes the other four modes, whose choice depends only on the magnitude.
Instances For
Negation fixes nearest-away rounding.
Negation fixes rounding toward zero.
Sign that IEEE 754 gives the zero of an exactly cancelling sum whose operands have the signs
leftSign and rightSign.
IEEE 754-2019 Section 6.3 makes an exact zero sum of operands with opposite signs positive in every rounding direction except toward negative infinity, where it is negative. A sum of two zeros with the same sign keeps that sign in every direction. Rounding away from zero follows the rule of the other directions, as MPFR does: its exact cancellation gives positive zero.
zero keeps a negative sign only in formats with a signed zero.
Instances For
The magnitude rounding rule that this mode applies to a result of the given sign.
The nearest modes round the magnitude to nearest with the same tie rule, toward-zero truncates it, and away-from-zero rounds it up. The two infinity directions round the magnitude up when they move the result away from zero and truncate it otherwise.
Instances For
Negating twice returns the original mode.
The negated mode rounds a result away from zero exactly when this mode rounds its negation.
The negated mode carries an overflow upward exactly when this mode carries its negation.
The negated mode treats a magnitude of one sign as this mode treats the opposite sign.
A mode rounds a magnitude up exactly when it moves a result of that sign away from zero.
Bare rounding-mode names #
open FloatLib.Rounding brings the type IEEERoundingMode and its six constructors into scope
without a namespace or a leading dot, so a directed or status operation can name its mode directly
and user code can take a mode as a parameter:
open FloatLib.Rounding
Model.sqrt x (mode := up) (status := true)
def third (mode : IEEERoundingMode) : Binary32 := ExecFloat.Binary.div 1 3 (mode := mode)
The names are opt-in because they are short words: in a scope that opens this namespace, a
pattern variable spelled up or down is read as the constructor, so bind such values under
other names, such as upper and lower. Library code never opens it and writes .up.
Numerics.RoundingMode, which also has stochastic rounding, has no bare names here.