Executable policy-aware binary quantization #
Encoding policy and operation policy are distinct. E4M3FN, for example, has one fixed collection of bit patterns but supports both saturating and non-saturating conversions. Hardware may also flush a subnormal result to zero even though the storage format can represent that subnormal.
QuantizationPolicy records the three choices needed when an exact rational is written into a
binary format:
- integer rounding at the discarded-bit boundary;
- behavior beyond the largest finite magnitude;
- gradual underflow or flush-to-zero after rounding.
The implementation uses natural-number arithmetic only. It never passes through a host float.
The local stochastic choice in roundQuot is deterministic given entropy and is unbiased when
entropy % den is uniform. That statement does not by itself give a global unbiasedness theorem
for quantization with saturation, overflow, or flush-to-zero.
roundDyadicGeneral always executes the rational policy algorithm below. The ordinary
roundDyadic entry point dispatches the four IEEERoundingMode choices with native overflow
and gradual underflow to the shift-based rounders in Rounding.Directed.Dyadic. Every other
policy uses the general engine. Keeping these two implementations independent makes the
agreement theorem in Rounding.Policy.Agreement meaningful rather than a consequence of
delegation.
Both engines resolve overflow through directedOverflow, so a finite-with-NaN encoding such as
E4M3FN saturates to its largest finite value in the truncating direction and produces its NaN word
only when the direction carries the magnitude past that value.
References:
- IEEE 754-2019, Sections 4.3 and 7.4, for directed and nearest rounding and overflow behavior.
- Open Compute Project, 8-bit Floating Point Specification (OFP8), Revision 1.0, Section 5.2, https://www.opencompute.org/documents/ocp-8-bit-floating-point-specification-ofp8-revision-1-0-2023-12-01-pdf-1.
- NVIDIA, CUDA Math API: FP8 Conversion and Data Movement, for
NOSATandSATFINITE, https://docs.nvidia.com/cuda/cuda-math-api/cuda_math_api/group__CUDA__MATH__FP8__MISC.html.
Round num / den to a natural number according to mode.
sign is needed only by directed modes. For stochastic rounding with den > 0,
entropy % den < num % den chooses the upper integer. A uniform entropy % den therefore selects
the upper value with probability equal to the fractional part of num / den.
Instances For
The IEEERoundingMode constructor with the same direction as mode, when available.
This type has no nearest-away or stochastic constructor, so those modes map to none.
Instances For
The IEEE rounding direction that policy reduces to, if any.
This returns a direction when overflow is native, underflow is gradual, and the rounding mode
has an IEEERoundingMode constructor. roundDyadic executes such
policies with the directed rounders instead of the general engine.
Instances For
Whether an overflowing magnitude of sign sign is carried upward under mode.
This is the direction test of IEEE 754-2019 Section 7.4 on the policy vocabulary; see
directedOverflow. Nearest-away and stochastic rounding overflow as the nearest modes do.
Instances For
Whether a positive magnitude below half the least subnormal rounds up to that subnormal.
The answer is none for stochastic rounding, where it depends on the entropy. Nearest modes and
toward-zero rounding take such a magnitude to zero; the two infinity-directed modes take it to the
least subnormal when the direction carries the magnitude away from zero.
Instances For
Result selected by a magnitude overflow.
With .saturate the result is the largest finite value of the requested sign. With .native the
direction rule of directedOverflow applies: a magnitude carried upward becomes the format's
native overflow value (signed infinity for the IEEE encoding, the NaN word for the two
finite-with-NaN encodings, the largest finite value for the fully finite encoding) and a magnitude
carried downward becomes the largest finite value of the requested sign.
Instances For
Apply output flush-to-zero after gradual rounding has selected an encoding.
Instances For
Round the nonnegative rational magnitude num / den into fmt with the requested sign.
This is the statically checked arithmetic core used after a caller has established that den > 0.
A magnitude below half the least subnormal is decided by the rounding direction alone, except
under stochastic rounding, so the subnormal alignment shift is not materialized for such inputs.
Stochastic rounding of a far-below-subnormal quotient does shift num by the full alignment
fmt.exponentBias + fmt.fracWidth - 1, because the exact remainder decides the outcome.
Instances For
Round the nonnegative rational magnitude num / den into fmt with the requested sign.
A zero denominator returns none. Otherwise the function first performs gradual quantization and
then applies policy.underflow; this matters at the normal/subnormal boundary, where a value below
the smallest normal can nevertheless round up to that normal value.
Instances For
Round an exact rational magnitude into fmt under policy.
Nearest-even with native overflow and gradual underflow is the canonical Model.roundRat
operation for every complete format descriptor. Other rounding, overflow, or
underflow policies use the explicit general algorithm above. A zero denominator returns none
uniformly, including for finite-only formats that have no NaN encoding.
Instances For
Round an exact signed dyadic with the independent rational policy algorithm.
This definition deliberately does not dispatch to the directed dyadic rounders. It is the
general implementation used for policies outside the directed dispatch. It is compared
independently with roundDyadicWithRounding in Rounding.Policy.Agreement.
Instances For
Round an exact signed dyadic into a policy-aware format.
IEEE directions with native overflow and gradual underflow use the dedicated directed dyadic
rounders. Other policies use roundDyadicGeneral, including nearest-away, stochastic, saturating,
and flush-to-zero policies.
Instances For
Quantize a finite source value. NaN and infinity require an explicit cast policy.