When Double Rounding is Correct

1 Introduction

• Specialized machine-learning formats complicate software simulation, while traditional library extensions require implementations for each format, operation, and rounding mode.These formats include 8-, 6-, and 4-bit floating point.Source: §1 · pp. 1–2
• Correct double rounding reduces to format containment, with sufficient conditions depending on the intermediate format and rounding modes.The paper also gives an efficient, complete containment check and mechanizes the results in Lean 4.Source: §1 · p. 2
• Format inference bounds intermediate computations so containment and correct double rounding can justify semantics-preserving rewrites to available operations.This addresses accelerator computations whose intermediate values may require far more precision than their small-format inputs.Source: §1 · p. 2
• MPFX’s correctly-rounded operations run up to 13.5× faster than MPFR and 0.44×–1.62× as fast as SoftFloat.The SoftFloat comparison uses only formats it supports; MPFX supports many more.Source: §1 · p. 2
• The MPFX-based simulation of an OCP MX standard algorithm is up to 13.3× faster than its SoftFloat version.Both implementations use available primitives to implement the specification.Source: §1 · p. 3

2 Overview

• The OCP MX standard specifies small formats and high-level algorithms but leaves implementation formats and rounding modes to the implementer.Different choices trade numerical accuracy for chip area and power.Source: §2 · p. 3
• The overview’s MX dot product combines blocks from A and B with a running accumulator C to update C in each loop iteration.The blocks encode elements using a shared scale factor and block elements.Source: Figure 1 · p. 3
• The specification uses infinitely precise operations, while the programming environment offers rounded operations in a handful of formats, so simulation requires semantics-preserving rewrites.Format inference identifies intermediate formats, and correct double rounding helps determine when replacements preserve behavior.Source: §2 · p. 4
• A dot-product accumulator for small MX inputs can require 69 bits of precision, beyond double precision, and each choice of formats and rounding modes defines another candidate to model.The overview notes that libraries support only a fixed handful of formats, leaving other candidates to bespoke implementations.Source: §2 · p. 4
• MPFX reuses high-precision kernels and re-rounds their results across formats, provided the required intermediate fits in double precision.The library is designed for instances of the abstract format meeting that intermediate-precision condition.Source: §2 · p. 4
• The paper maps the dot-product specification to SoftFloat and MPFX primitives, with both implementations semantically equivalent to the specification.The MPFX implementation uses operations available in the programming environment.Source: §2 · p. 4

3 What is a Number Library?

• Number libraries implement formats and their operations in software, supporting numerical-error analysis, implementation trade-offs, and verification of numerical software and hardware.The section organizes their common foundations around representable values, rounding, and correctness.Source: §3 · pp. 4–5

3.1 Number Formats

• The paper restricts its analysis to dyadic-number formats, which include common floating-point, fixed-point, and integer formats.Dyadic values have the form (−1)^s × c × 2^exp.Source: §3.1 · p. 5

3.2 Rounding

• Rounding maps a real value between adjacent representable values to one of them, with the rounding mode determining the choice.The paper focuses on RNE, RTZ, RAZ, and RTO because the other discussed modes do not add distinct behavior to its analysis.Source: §3.2 · pp. 5–6

3.3 Correct Rounding

• A correctly-rounded implementation applies an exact operation and then rounds its result to the target format and mode.Correct rounding gives a clear behavioral specification, reproducibility across implementations, and consistent bounds on rounding error.Source: §3.3 · p. 6

3.4 Double Rounding

• Double rounding is correct when an intermediate rounding leaves the final result unchanged; it is not always correct, as an RNE example demonstrates.For E2M1 and E4M3, rounding 1.26 directly gives 1.5, while rounding first to E4M3 and then E2M1 gives 1; with RTZ, both expressions give 1.Source: §3.4 · pp. 6–7

3.5 A Brief Survey of Number Libraries

• The surveyed libraries make different choices about supported formats, rounding modes, and correctness guarantees.SoftFloat models IEEE arithmetic using integers, FloppyFloat uses host floating-point operations and EFTs, and MPFR offers arbitrary-precision correctly-rounded operations.Source: §3.5 · p. 7

4.2 Abstract Number Format

• A unifies fixed- and floating-point formats by parameterizing their structured sets of representable values, enabling efficient format-containment reasoning.The generators differ mainly in whether the quantum increases; setting floating-point precision to infinity recovers fixed-point generation.Source: §4 · p. 7, §4.2 · pp. 9–10

4.1 Generating Number Formats

• Fixed-point formats generate zero and then positive and negative multiples of a power-of-two quantum, producing evenly spaced values.The section focuses on ordinary representable values; special values such as signed zero, infinity, and NaN are handled separately.Source: Fixed-Point Number Formats · pp. 7–8, §4.1 · p. 7, Figure 3 · p. 8
• Floating-point formats filter dyadic values by a maximum significand precision, with spacing increasing by powers of two while remaining constant below magnitude one.A generator can produce these values without rejection by doubling the quantum at successive power-of-two cutoffs.Source: Floating-Point Number Formats · p. 8
• Bounded formats restrict positive and negative magnitudes, and rounding handles overflow by choosing infinity or the corresponding signed bound.The model omits special values and imposes quantization-or-precision, nontriviality, and parity-related parameter restrictions.Source: §4.1 · p. 7, Bounded Formats · p. 9, §4.2 · p. 10

4.2 Abstract Number Format

• A is parameterized by maximum precision, minimum-quantum exponent, and maximum representable value, which together determine its representable values.Its parameters reduce containment checking to comparisons, including the bound.Source: §4.2 · p. 10, Comparison to Flocq · p. 11
• The abstraction covers common floating-point, fixed-point, integer, and arbitrary-precision formats, while excluding formats that are neither quantized nor precision-bound.Posits fall outside the parameterization because their precision varies with magnitude; two other unrepresented classes are absent from real-world usage.Source: §4.2 · pp. 9–10
• Different parameter choices can describe the same values: bounded fixed-point formats may equal infinitely many degenerate floating-point formats.As bitwidths shrink, some machine-learning floating-point formats approach fixed-point representations.Source: Format Redundancy · p. 11
• The containment rules use a general precision-based test for most cases and an alternative test for degenerate floating-point formats.The precision-based rule is too restrictive for those degenerate cases, which are equivalent to bounded fixed-point formats.Source: Figure 7 · p. 12

5.1 Format Containment

• Containment has a constant-time, complete parameter test: A-Contains-Prec handles most cases, while A-Contains-Sub covers degenerate formats.The two rules together apply if and only if F1⊆F2.Source: §5.1 · pp. 12–13
• A-Contains-Prec requires p1≤p2, exp1≥exp2, and b1≤b2; degenerate cases instead use b1≤2^(exp1+p2).The first rule checks precision, minimum quantum, and bound; the alternative handles formats where maximum precision does not affect representable values.Source: §5.1 · p. 12

5.2 Correct Double Rounding

• Retained width depends on format parameters and input, not rounding mode; RTO padding preserves representability, with one extra bit for directed finals and two for RNE.The RNE premise preserves halfway cases.Source: §5.2 · pp. 13–14
• The rules assume the first rounding does not overflow; their bounds prevent intermediate overflow, and valid adjacent double-rounding rules compose across longer chains.Source: Figure 8 · p. 14, §5.2 · p. 14
• Ten other mode pairings can fail even when F1⊆F2; making F2 larger does not fix them.The counterexample construction approaches the even representable value as the intermediate format grows.Source: §5.2 · p. 15
• RTO intermediates support all four final modes with at most two extra bits; RTZ and RAZ work only when modes match, while RNE works only in trivial cases.The RNE restriction holds even when the intermediate format is made arbitrarily large.Source: §5.2 · pp. 14–15

5.3 Modular Number Libraries

• Correct double rounding separates arithmetic from rounding: reuse a correctly rounded high-precision implementation meeting the premises, with RTO as the natural intermediate.The approach can use hardware, existing libraries, or custom kernels.Source: §5.3 · pp. 15–16

6.1 Format Inference

• Format inference analyzes assignments in execution order and tracks representable-value spacing as well as range, making it more precise than interval analysis.Correctly-rounded operations inherit their target format; bounds for unrounded operations can be tightened from their arguments.Source: §6.1 · p. 16

6.2 Introducing & Eliminating Roundings

• When an unrounded result is already contained in a target format, its rounding changes nothing, justifying either removing that rounding or inserting an equivalent one.Correct double-rounding checks similarly justify merging a rounding sequence or expanding a correctly-rounded operation into higher-precision computation and re-rounding.Source: §6.2 · p. 17

6.3 A Rewriting Strategy

• A three-phase strategy infers expression formats, removes unnecessary roundings, then promotes unrounded operations to available formats, yielding an equivalent executable program.The inferred format may not itself be available, so finitization can choose a larger available format.Source: §6.3 · p. 17, Figure 9 · p. 17
• Exact splitting rewrites an expression as a truncated high part plus a remainder, preserving its value and allowing smaller formats for consumers of fixed-point parts.The high part is truncated to a multiple of 2^(exp+k), and the low part is the remainder.Source: §6.3 · p. 18
• Automating the choice among possible lowerings remains future work, although the format checks and bounded search space are described as straightforward.The authors apply the strategy manually to the MX dot product example.Source: §6.3 · p. 18

7.1 Implementation

• About 3.17 billion cases across 4,704 configurations were checked bit-for-bit against MPFR for small IEEE 754-style formats.The tests cover six operations, rounding modes, backends, and float or double containers; a separate randomized suite checks unbounded-exponent formats.Source: §7.1 · pp. 18–19
• 2,318 source lines implement MPFX operations correctly rounded for instances of the abstract format whose required intermediate fits in FP64, under all seven rounding modes.The arithmetic and round-to-odd emulation do not depend on the target format; only final re-rounding does.Source: §7.1 · p. 19

7.2 Performance of MPFX

• 0.44×–1.62× as fast as SoftFloat and up to 13.5× faster than MPFR: MPFX’s faster backends span this range across measured operations, datatypes, and rounding modes.The figure compares FP32 and FP16 across six operations and RNE, RTP, and RTZ, with SoftFloat as the baseline.Source: Figure 10 · p. 20, §7.2 · p. 21
• With one element per call, CPFloat is 1.6×–4.7× slower than MPFX on every operation, but batched calls are 4.6×–12.2× faster due to amortized parameter setup.The authors attribute the difference to API granularity rather than rounding cost.Source: §7.2 · p. 21

Case Study: MX Dot Product

• The specification assumes E5M2-representable block elements and power-of-two scale factors in [2^-127, 2^127], with exact local dot products and FP32 RNE accumulation.Accumulation across block pairs is rounded after each step.Source: §8 · p. 21

Discussion

• Uniform FP32 produces incorrect results on roughly 5.2% of one million randomly sampled MX block pairs.The reported disagreements include a dense underflow band and errors distributed across the rest of the input space, excluding the overflow corner.Source: §8 · p. 21, Figure 11 · p. 21

Mapping to SoftFloat

• Format inference bounds intermediates, revealing that the accumulator needs 69 bits of precision and the scaled local dot product exceeds double precision.The inferred accumulator format is propagated through the program to derive bounds for subsequent expressions.Source: Mapping to SoftFloat · p. 22, Figure 12 · p. 22
• SoftFloat mapping promotes operands to supported formats and uses FP128 for the largest intermediate, then correctly double-rounds the final addition to FP32.The inferred multiplication formats fit in FP32, allowing lossless promotion for that operation.Source: Mapping to SoftFloat · pp. 22–23

Going Faster with MPFX

• MPFX replaces FP128 accumulation with fixed-point integer arithmetic and splits the accumulator so the remaining products can use native FP64.A split and a three-argument adder preserve correct final rounding while avoiding SoftFloat’s most expensive operations.Source: Going Faster with MPFX · pp. 23–24

Comparison

• 13.26× speedup for E5M2×E4M3 and 9.99× for E5M2×E5M2; E4M3×E4M3 has a smaller speedup over SoftFloat.The E4M3×E4M3 implementations use double precision throughout the inner dot product, so only the final adder differs.Source: Table 3 · p. 24, Comparison · p. 24

Limitations

• The format treats special values separately, and the authors leave a parameterized treatment of format-specific special values to future work.Emerging formats differ in which special values they support.Source: §9 · p. 25
• The abstract format does not directly represent posits or strictly positive formats such as MX E8M0, and unsigned floating-point support remains unverified.The authors suggest setting b− = 0 for unsigned formats but have not verified that extension.Source: §9 · p. 25
• Correct double-rounding rules guarantee results only when direct rounding to the target format does not overflow.Overflow behavior varies across formats and rounding modes, so extending the rules requires specifying whether overflow rounds to infinity or the maximum value.Source: §9 · p. 25
• Format inference covers straight-line programs; dynamic-bound loops would require widening and may produce impractically wide formats.Statically bounded loops can be unrolled, as in the case study.Source: §9 · p. 25

Future Work

• The authors plan to add transcendental-function support through RLIBM and adopt CPFloat’s optimized rounding algorithms.These are proposed improvements to MPFX, not reported current capabilities.Source: §9 · p. 25

Number libraries

• CPFloat and MXSim use high-precision computation followed by rounding, while FloatX notes that its double roundings may not be correctly rounded [28].CPFloat also offers stochastic rounding, which MPFX lacks.Source: §10 · p. 25
• SoftFloat, FloppyFloat, and SIPE provide uniform-precision operations, while Universal covers many number formats but requires substantial implementation and validation effort.MPFR instead provides correctly rounded operations at arbitrary precision.Source: §10 · p. 26

Floating-point formalization

• Prior formalizations cover floating-point arithmetic, but the paper’s abstract format unifies fixed- and floating-point and adds a bound for containment reasoning.Chang et al. formalize the draft IEEE P3109 standard in Lean, focusing on one standard rather than cross-format containment or double rounding [10].Source: §10 · p. 26

Double rounding and round to odd

• Earlier double-rounding results establish conditions for particular modes or operations, while round-to-odd work supports correctly rounded applications such as RLIBM.Boldo and Melquiond show that round to odd and p+2 digits ensure correct rounding to p digits under RNE.Source: §10 · pp. 26–27

Error analyzers

• Error analyzers use exactness to tighten error bounds, whereas this work uses format containment to drop or insert roundings while preserving correct rounding.The cited tools reason about exact operations such as Sterbenz subtraction and multiplication by powers of two.Source: §10 · p. 27

Rewriting numerical programs and precision tuning

• Verified rewriting preserves exact correctly-rounded results here, unlike RealCake’s error-bounded transformations; precision tuners instead search assignments under an accuracy bound.The paper describes precision tuning and its rewriting strategy as complementary.Source: §10 · p. 27

Conclusion

• The paper gives format-based sufficient conditions for correct double rounding across rounding-mode pairings, using abstract format A and an efficient, complete containment check.The abstract format parameterizes fixed- and floating-point formats.Source: §11 · p. 27
• Format containment supports both checking individual operations and rewriting whole programs to available library or hardware primitives while preserving correct rounding.The conclusion reports MPFX as competitive with MPFR and SoftFloat despite supporting a broader class of formats, and says the case study’s MPFX-targeted implementation is faster.Source: §11 · p. 27
• The authors present correct double rounding as a principled, scalable path for software support as hardware number formats diversify.Source: §11 · p. 27

• The appendix contains proofs for the format-containment rules and correct-double-rounding rules.Source: A Proofs · p. 31
• The proofs are mechanized in Lean.Source: A Proofs · p. 31
• Table 4 maps principal rules and lemmas from Sections 5 and 6 to their Lean theorems.Source: Table 4 · p. 31, A Proofs · p. 31

• The two rules are sound and complete for containment, with A-Contains-Sub covering degenerate floating-point formats and bounded fixed-point formats beyond A-Contains-Prec.Source: §A.1 · p. 31
• A-Contains-Prec transfers precision, magnitude, and quantum constraints when the source precision, exponent, and bound satisfy the stated containment inequalities.The proof handles an unconstrained target quantum separately; otherwise the source exponent condition ensures the value is a multiple of the target quantum.Source: §A.1 · p. 31
• A-Contains-Sub establishes containment when the source bound is at most 2^(exp1+p2) and the target exponent is no greater than the source exponent.The bound limits the integer significand to at most p2 digits, even when p1 exceeds p2.Source: §A.1 · p. 31
• For non-trivial formats with a representable bound, containment requires the source bound and exponent conditions used by the rules.The appendix gives examples showing that omitting either the representable-bound or non-triviality restriction can leave equal value sets while neither rule applies.Source: §A.1 · p. 32

A.2 Correct Double Rounding

• The number of digits retained when rounding depends on format precision, exponent, and input, not on the rounding mode or bound.The appendix derives the retained-digit position for fixed-point, floating-point, and combined formats.Source: §A.2 · p. 32
• For k≥1, round-to-odd at precision w+k leaves values representable at w unchanged and keeps unrepresentable values between their two nearest w-precision neighbors.The proof also establishes that an unrepresentable input remains unrepresentable after round-to-odd.Source: §A.2 · p. 33
• Round-to-zero followed by round-to-zero and round-away-from-zero followed by round-away-from-zero preserve the direct result when the first format is contained in the second.The proofs characterize each mode as selecting the largest representable value below, or smallest representable value above, the input; they also check overflow.Source: §A.2 · pp. 33–34
• Round-to-odd followed by round-to-odd preserves the direct result when the first format is contained in the second and the second precision is at least 2.If the two roundings use different digit positions, Lemma 5.4 keeps the intermediate value between the same first-format neighbors; the proof also treats overflow according to the bound's parity.Source: §A.2 · p. 34
• Round-to-odd followed by toward-zero or away-from-zero rounding is correct when the second format contains the widened source format; the widened precision separates the intermediate value from the source-format neighbors.The toward-zero rule uses A(p1+1, exp1−1, next(b1)); the away-from-zero rule uses the corresponding bounded format.Source: §A.2 · pp. 34–35
• Round-to-odd followed by round-to-nearest-even is correct when the second format contains A(p1+2, exp1−2, b1), preserving the side of the midpoint or the exact tie.The proof also handles overflow using the halfway bound and its containment in the second format.Source: §A.2 · p. 35

A.3 Format Inference

• Multiplication inference bounds the result by adding input precisions and exponents and multiplying their magnitude bounds.The proof applies the precision, quantum, and magnitude constraints to the product.Source: §A.3 · p. 35
• Addition inference uses the finer input quantum and summed magnitude bounds to derive a precision sufficient to contain the sum.Its precision bound is P=max(1, ceil(log2(N+1))) for N=floor((b1+b2)/2^m), where m is the finer exponent.Source: §A.3 · pp. 35–36