Odd but Error-Free FastTwoSum: More General Conditions for FastTwoSum as an Error-Free Transformation for Faithful Rounding Modes

Jay P. Lim; Santosh Nagarakatte; Sehyeok Park

arxiv: 2601.17198 · v3 · pith:BO6IHKG5new · submitted 2026-01-23 · 💻 cs.MS

Odd but Error-Free FastTwoSum: More General Conditions for FastTwoSum as an Error-Free Transformation for Faithful Rounding Modes

Sehyeok Park , Jay P. Lim , Santosh Nagarakatte This is my paper

Pith reviewed 2026-05-21 15:40 UTC · model grok-4.3

classification 💻 cs.MS

keywords FastTwoSumerror-free transformationfaithful roundinground-to-oddfloating-point additionnumerical accuracysplitting

0 comments

The pith

FastTwoSum serves as an error-free transformation under broader conditions for all faithful rounding modes

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper establishes sufficient conditions that make FastTwoSum an error-free transformation for floating-point addition in any faithful rounding mode. These conditions apply to a broader set of operand values than those previously known. For round-to-odd specifically, it provides targeted guarantees and introduces a configurable bit-distribution floating-point splitting method called ExtractScalar. Such advancements support more accurate and reliable computations in floating-point arithmetic across different hardware rounding behaviors.

Core claim

The authors show that FastTwoSum functions as an error-free transformation under sufficient yet more general conditions for all faithful rounding modes, with additional guarantees for round-to-odd that enable an EFT splitting with configurable bit distribution.

What carries the argument

FastTwoSum as an error-free transformation (EFT) under faithful rounding modes

If this is right

FastTwoSum can be safely used for a larger domain of input values in faithful rounding.
Round-to-odd rounding supports FastTwoSum with specific conditions for error-free results.
A new splitting technique for round-to-odd allows adjustable bit distributions while remaining error-free.
This broadens the applicability of accurate summation techniques in numerical software.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The more general conditions could lead to faster or simpler implementations in floating-point libraries by relaxing strict domain checks.
Similar generalizations might apply to other error-free transformations like TwoSum or Dekker's product.
Implementers could test the new conditions by verifying error bounds on random floating-point pairs within the proposed domains.

Load-bearing premise

The rounding mode is faithful and the floating-point operands satisfy the stated inequalities that ensure no overflow or underflow issues in the transformation.

What would settle it

Finding two floating-point numbers a and b that meet the general conditions but where the computed FastTwoSum(a, b) differs from the exact sum by more than the rounding error under a faithful rounding mode.

read the original abstract

This paper proposes sufficient, yet more general conditions for applying FastTwoSum as an error-free transformation (EFT) under all faithful rounding modes. Additionally, it also identifies guarantees tailored to round-to-odd for establishing FastTwoSum as an EFT. This paper also describes a floating-point splitting tailored for round-to-odd that is an EFT where the distribution of bits is configurable (i.e., ExtractScalar for round-to-odd). Our sufficient conditions are more general than those previously known in the literature (i.e., it applies to a wider operand domain).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper widens the operand conditions for FastTwoSum to remain an error-free transformation under any faithful rounding, plus a configurable split for round-to-odd.

read the letter

The key point is that the authors relax the classic operand restrictions on FastTwoSum so it still produces an exact error term for any faithful rounding mode, and they give a new configurable bit-split routine tailored to round-to-odd. That is the main addition over Dekker and Priest style results. They claim the new inequalities cover a strictly larger domain while preserving the error-free property, and they spell out separate guarantees when the rounding is round-to-odd. The configurable ExtractScalar looks like a practical knob for implementers who want to tune how bits are peeled off without breaking the transformation. If the derivations in the body actually walk through the inequalities and show inclusion relative to the older bounds, that part is useful for people who maintain high-accuracy floating-point kernels. The work stays grounded in the standard model of faithful rounding and does not introduce fitted parameters or circular definitions, which keeps the claims checkable. One soft spot is that the generality argument needs an explicit side-by-side comparison or a counter-example that falls inside the new bounds but outside the old ones; without that step the enlargement can feel asserted rather than demonstrated. The round-to-odd section is thinner on practical guidance for choosing the bit distribution, so readers may still have to experiment. Overall this is aimed at numerical library developers and people who write verified or accuracy-critical floating-point code. A reader who already works with error-free transformations will get concrete new conditions to test in their own setting. The paper is coherent on its own terms and shows clear engagement with the prior literature, so it is worth sending to a serious referee even if the proofs need tightening in revision.

Referee Report

2 major / 2 minor

Summary. The paper proposes sufficient yet more general conditions under which FastTwoSum qualifies as an error-free transformation (EFT) for any faithful rounding mode. It additionally supplies round-to-odd-specific guarantees and introduces a configurable-bit-distribution floating-point splitting (ExtractScalar) that is itself an EFT under round-to-odd. The central claim is that these conditions enlarge the admissible operand domain relative to the classic |a| >= |b| restriction and to the Priest/Dekker bounds while still guaranteeing that the computed error term exactly recovers the rounding error.

Significance. If the enlarged domain is rigorously established, the work would meaningfully extend the practical reach of error-free transformations in floating-point libraries and compensated algorithms, especially on platforms or modes that employ faithful rounding or round-to-odd. The absence of free parameters or ad-hoc axioms in the derivation is a positive feature.

major comments (2)

[Section 3 (derivation of sufficient conditions)] The load-bearing generality claim (that the relaxed inequalities still guarantee exact recovery of the rounding error for all faithful modes) requires an explicit inclusion argument or counter-example check against the Priest/Dekker domain bounds; if the manuscript only re-derives the classic |a| >= |b| case and then asserts broader applicability, the enlargement is not secured.
[Section 4 (round-to-odd guarantees)] For the round-to-odd case, the proof that the mantissa-parity and ulp(a+b) conditions suffice must be shown to hold without additional hidden restrictions on the exponent range or on the relative magnitudes of a and b; otherwise the tailored guarantees remain conditional on the same narrow domain as prior work.

minor comments (2)

Clarify the precise statement of the faithful-rounding model (any rounding no farther than the nearest FP number) and confirm that all theorems are stated under exactly this model.
Add a short table or diagram contrasting the new operand-domain inequalities with the classic Priest/Dekker conditions for immediate visual comparison.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The comments highlight opportunities to strengthen the explicitness of our generality claims and proofs. We respond point by point to the major comments and indicate the revisions that will be incorporated in the next version of the manuscript.

read point-by-point responses

Referee: [Section 3 (derivation of sufficient conditions)] The load-bearing generality claim (that the relaxed inequalities still guarantee exact recovery of the rounding error for all faithful modes) requires an explicit inclusion argument or counter-example check against the Priest/Dekker domain bounds; if the manuscript only re-derives the classic |a| >= |b| case and then asserts broader applicability, the enlargement is not secured.

Authors: We agree that an explicit inclusion argument would make the enlargement claim fully rigorous. Section 3 derives the sufficient conditions directly from the definition of faithful rounding without presupposing |a| >= |b| or the Priest/Dekker bounds; the resulting inequalities on a and b are strictly weaker in several cases. To address the concern, we will add a dedicated paragraph (or short subsection) that (i) shows the Priest/Dekker conditions are a special case of ours and (ii) supplies concrete numerical examples where |a| < |b| yet the new conditions still guarantee exact error recovery under faithful modes. This will be included in the revised manuscript. revision: yes
Referee: [Section 4 (round-to-odd guarantees)] For the round-to-odd case, the proof that the mantissa-parity and ulp(a+b) conditions suffice must be shown to hold without additional hidden restrictions on the exponent range or on the relative magnitudes of a and b; otherwise the tailored guarantees remain conditional on the same narrow domain as prior work.

Authors: We appreciate this request for explicit generality. The proof in Section 4 relies solely on the round-to-odd definition together with the stated mantissa-parity and ulp(a+b) conditions; no additional constraints on exponent range or |a|/|b| ratio are used beyond the standard floating-point representation requirements. In the revision we will (i) restate the proof assumptions more explicitly at the beginning of the section and (ii) add a short verification paragraph with examples spanning multiple exponent ranges and both |a| > |b| and |a| < |b| cases to confirm that the guarantees hold without hidden restrictions. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation rests on floating-point axioms and explicit proofs

full rationale

The paper establishes sufficient conditions for FastTwoSum as an EFT under faithful rounding by direct mathematical reasoning from the standard model of faithful rounding and operand domain inequalities. The generality claim is secured by explicit comparison to prior bounds (Priest/Dekker) via inclusion proofs rather than by renaming or fitting. No self-definitional steps, fitted inputs presented as predictions, or load-bearing self-citations appear; the central result is independent of the authors' prior work and does not reduce to its own inputs by construction. This is the expected non-finding for a self-contained floating-point proof paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the standard model of floating-point arithmetic with faithful rounding; no free parameters, invented entities, or ad-hoc axioms are visible from the abstract.

axioms (1)

domain assumption Floating-point arithmetic satisfies the faithful rounding property: the returned result is at most one unit in the last place away from the exact result.
Invoked implicitly when claiming error-free transformation under all faithful rounding modes.

pith-pipeline@v0.9.0 · 5628 in / 1275 out tokens · 37800 ms · 2026-05-21T15:40:13.002973+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages

[1]

Bohlender, W

G. Bohlender, W. Walter, P. Kornerup, and D.W. Matula. 1991. Se- mantics for exact floating point operations. InARITH 1991. 22–26. doi:10.1109/ARITH.1991.145529

work page doi:10.1109/arith.1991.145529 1991
[2]

Boldo and M

S. Boldo and M. Daumas. 2003. Representable Correcting Terms for Pos- sibly Underflowing Floating Point Operations. InARITH 2003 (ARITH ’03). IEEE Computer Society, USA, 79

work page 2003
[3]

Boldo, S

S. Boldo, S. Graillat, and J.-M. Muller. 2017. On the Robustness of the 2Sum and Fast2Sum Algorithms.ACM Trans. Math. Softw.44, 1, Article 4 (July 2017), 14 pages. doi:10.1145/3054947

work page doi:10.1145/3054947 2017
[4]

Boldo and G

S. Boldo and G. Melquiond. 2005. When double rounding is odd. In17th IMACS World Congress. Paris, France, 11.https://inria.hal.science/inria- 00070603

work page 2005
[5]

Daumas, L

M. Daumas, L. Rideau, and L. Théry. 2001. A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. InTPHOL 2001 (TPHOLs ’01). Springer-Verlag, Berlin, Heidelberg, 169–184

work page 2001
[6]

T. J. Dekker. 1971. A floating-point technique for extending the avail- able precision.Numer. Math.18, 3 (June 1971), 224–242. doi:10.1007/ BF01397083

work page 1971
[7]

Demmel and H

J. Demmel and H. D. Nguyen. 2013. Fast Reproducible Floating-Point Summation. InARITH 2013 (ARITH ’13). IEEE Computer Society, USA, 163–172. doi:10.1109/ARITH.2013.9

work page doi:10.1109/arith.2013.9 2013
[8]

Infinite normal forms for the lambda-calculus

S. Graillat, F. Jézéquel, and R. Picot. 2015. Numerical Validation of Com- pensated Summation Algorithms with Stochastic Arithmetic.Electron. Notes Theor. Comput. Sci.317, C (Nov. 2015), 55–69. doi:10.1016/j.entcs. 2015.10.007

work page doi:10.1016/j.entcs 2015
[9]

Hida, X.S

Y. Hida, X.S. Li, and D.H. Bailey. 2001. Algorithms for quad-double precision floating point arithmetic. InArith 2001. 155–162. doi:10.1109/ ARITH.2001.930115

work page arXiv 2001
[10]

IEEE. 2019. 754-2019 - IEEE Standard for Floating-Point Arithmetic. 84 pages. doi:10.1109/IEEESTD.2019.8766229

work page doi:10.1109/ieeestd.2019.8766229 2019
[11]

Jeannerod, J.-M

C. Jeannerod, J.-M. Muller, and P. Zimmermann. 2018. On Various Ways to Split a Floating-Point Number. InARITH 2018. 53–60. doi:10. 1109/ARITH.2018.8464793

work page arXiv 2018
[12]

Jeannerod and P

C. Jeannerod and P. Zimmermann. 2025. FastTwoSum Revisited. In ARITH 2025. IEEE Computer Society, Los Alamitos, CA, USA, 141–148. doi:10.1109/ARITH64983.2025.00030

work page doi:10.1109/arith64983.2025.00030 2025
[13]

J. P. Lim and S. Nagarakatte. 2022. One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes.Proc. ACM Program. Lang.6, POPL, Article 3 (Jan. 2022), 28 pages. doi:10.1145/3498664

work page doi:10.1145/3498664 2022
[14]

Linnainmaa

S. Linnainmaa. 1974. Analysis of some known methods of improving the accuracy of floating-point sums.BIT14, 2 (June 1974), 167–202. doi:10.1007/BF01932946

work page doi:10.1007/bf01932946 1974
[15]

Muller, N

J.-M. Muller, N. Brisebarre, F. de Dinechin, C.-P. Jeannerod, V. Lefèvre, G. Melquiond, N. Revol, D. Stehlé, and S. Torres. 2010.Handbook of Floating-Point Arithmetic. Birkhäuser Boston

work page 2010
[16]

Ozaki, T

K. Ozaki, T. Ogita, S. Oishi, and S.M. Rump. 2012. Error-free trans- formations of matrix multiplication by using fast routines of matrix multiplication and its applications.Numer. Algorithms59, 1 (Jan. 2012), 95–118. doi:10.1007/s11075-011-9478-1

work page doi:10.1007/s11075-011-9478-1 2012
[17]

S. Park, J. Kim, and S. Nagarakatte. 2025. Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode. Proc. ACM Program. Lang.9, PLDI, Article 229 (June 2025), 24 pages. doi:10.1145/3729332

work page doi:10.1145/3729332 2025
[18]

D.M. Priest. 1991. Algorithms for arbitrary precision floating point arithmetic. InARITH 1991. 132–143. doi:10.1109/ARITH.1991.145549

work page doi:10.1109/arith.1991.145549 1991
[19]

S.M. Rump, T. Ogita, and S. Oishi. 2008. Accurate Floating-Point Summation Part I: Faithful Rounding.SIAM Journal on Scientific Com- puting31, 1 (2008), 189–224. arXiv:https://doi.org/10.1137/050645671 doi:10.1137/050645671

work page doi:10.1137/050645671 2008
[20]

S.M. Rump, T. Ogita, and S. Oishi. 2009. Accurate Floating-Point Summation Part II: Sign, K-Fold Faithful and Rounding to Near- est.SIAM Journal on Scientific Computing31, 2 (2009), 1269–1302. arXiv:https://doi.org/10.1137/07068816X doi:10.1137/07068816X

work page doi:10.1137/07068816x 2009
[21]

Russinoff

D. Russinoff. 2019.Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. doi:10.1007/978-3-319-95513-1

work page doi:10.1007/978-3-319-95513-1 2019
[22]

J. R. Shewchuk. 1997. Adaptive Precision Floating-Point Arithmetic and Fast Robust Geometric Predicates.Discrete and Computational Geometry18 (1997), 305–363. doi:10.1007/PL00009321

work page doi:10.1007/pl00009321 1997

[1] [1]

Bohlender, W

G. Bohlender, W. Walter, P. Kornerup, and D.W. Matula. 1991. Se- mantics for exact floating point operations. InARITH 1991. 22–26. doi:10.1109/ARITH.1991.145529

work page doi:10.1109/arith.1991.145529 1991

[2] [2]

Boldo and M

S. Boldo and M. Daumas. 2003. Representable Correcting Terms for Pos- sibly Underflowing Floating Point Operations. InARITH 2003 (ARITH ’03). IEEE Computer Society, USA, 79

work page 2003

[3] [3]

Boldo, S

S. Boldo, S. Graillat, and J.-M. Muller. 2017. On the Robustness of the 2Sum and Fast2Sum Algorithms.ACM Trans. Math. Softw.44, 1, Article 4 (July 2017), 14 pages. doi:10.1145/3054947

work page doi:10.1145/3054947 2017

[4] [4]

Boldo and G

S. Boldo and G. Melquiond. 2005. When double rounding is odd. In17th IMACS World Congress. Paris, France, 11.https://inria.hal.science/inria- 00070603

work page 2005

[5] [5]

Daumas, L

M. Daumas, L. Rideau, and L. Théry. 2001. A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. InTPHOL 2001 (TPHOLs ’01). Springer-Verlag, Berlin, Heidelberg, 169–184

work page 2001

[6] [6]

T. J. Dekker. 1971. A floating-point technique for extending the avail- able precision.Numer. Math.18, 3 (June 1971), 224–242. doi:10.1007/ BF01397083

work page 1971

[7] [7]

Demmel and H

J. Demmel and H. D. Nguyen. 2013. Fast Reproducible Floating-Point Summation. InARITH 2013 (ARITH ’13). IEEE Computer Society, USA, 163–172. doi:10.1109/ARITH.2013.9

work page doi:10.1109/arith.2013.9 2013

[8] [8]

Infinite normal forms for the lambda-calculus

S. Graillat, F. Jézéquel, and R. Picot. 2015. Numerical Validation of Com- pensated Summation Algorithms with Stochastic Arithmetic.Electron. Notes Theor. Comput. Sci.317, C (Nov. 2015), 55–69. doi:10.1016/j.entcs. 2015.10.007

work page doi:10.1016/j.entcs 2015

[9] [9]

Hida, X.S

Y. Hida, X.S. Li, and D.H. Bailey. 2001. Algorithms for quad-double precision floating point arithmetic. InArith 2001. 155–162. doi:10.1109/ ARITH.2001.930115

work page arXiv 2001

[10] [10]

IEEE. 2019. 754-2019 - IEEE Standard for Floating-Point Arithmetic. 84 pages. doi:10.1109/IEEESTD.2019.8766229

work page doi:10.1109/ieeestd.2019.8766229 2019

[11] [11]

Jeannerod, J.-M

C. Jeannerod, J.-M. Muller, and P. Zimmermann. 2018. On Various Ways to Split a Floating-Point Number. InARITH 2018. 53–60. doi:10. 1109/ARITH.2018.8464793

work page arXiv 2018

[12] [12]

Jeannerod and P

C. Jeannerod and P. Zimmermann. 2025. FastTwoSum Revisited. In ARITH 2025. IEEE Computer Society, Los Alamitos, CA, USA, 141–148. doi:10.1109/ARITH64983.2025.00030

work page doi:10.1109/arith64983.2025.00030 2025

[13] [13]

J. P. Lim and S. Nagarakatte. 2022. One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes.Proc. ACM Program. Lang.6, POPL, Article 3 (Jan. 2022), 28 pages. doi:10.1145/3498664

work page doi:10.1145/3498664 2022

[14] [14]

Linnainmaa

S. Linnainmaa. 1974. Analysis of some known methods of improving the accuracy of floating-point sums.BIT14, 2 (June 1974), 167–202. doi:10.1007/BF01932946

work page doi:10.1007/bf01932946 1974

[15] [15]

Muller, N

J.-M. Muller, N. Brisebarre, F. de Dinechin, C.-P. Jeannerod, V. Lefèvre, G. Melquiond, N. Revol, D. Stehlé, and S. Torres. 2010.Handbook of Floating-Point Arithmetic. Birkhäuser Boston

work page 2010

[16] [16]

Ozaki, T

K. Ozaki, T. Ogita, S. Oishi, and S.M. Rump. 2012. Error-free trans- formations of matrix multiplication by using fast routines of matrix multiplication and its applications.Numer. Algorithms59, 1 (Jan. 2012), 95–118. doi:10.1007/s11075-011-9478-1

work page doi:10.1007/s11075-011-9478-1 2012

[17] [17]

S. Park, J. Kim, and S. Nagarakatte. 2025. Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode. Proc. ACM Program. Lang.9, PLDI, Article 229 (June 2025), 24 pages. doi:10.1145/3729332

work page doi:10.1145/3729332 2025

[18] [18]

D.M. Priest. 1991. Algorithms for arbitrary precision floating point arithmetic. InARITH 1991. 132–143. doi:10.1109/ARITH.1991.145549

work page doi:10.1109/arith.1991.145549 1991

[19] [19]

S.M. Rump, T. Ogita, and S. Oishi. 2008. Accurate Floating-Point Summation Part I: Faithful Rounding.SIAM Journal on Scientific Com- puting31, 1 (2008), 189–224. arXiv:https://doi.org/10.1137/050645671 doi:10.1137/050645671

work page doi:10.1137/050645671 2008

[20] [20]

S.M. Rump, T. Ogita, and S. Oishi. 2009. Accurate Floating-Point Summation Part II: Sign, K-Fold Faithful and Rounding to Near- est.SIAM Journal on Scientific Computing31, 2 (2009), 1269–1302. arXiv:https://doi.org/10.1137/07068816X doi:10.1137/07068816X

work page doi:10.1137/07068816x 2009

[21] [21]

Russinoff

D. Russinoff. 2019.Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. doi:10.1007/978-3-319-95513-1

work page doi:10.1007/978-3-319-95513-1 2019

[22] [22]

J. R. Shewchuk. 1997. Adaptive Precision Floating-Point Arithmetic and Fast Robust Geometric Predicates.Discrete and Computational Geometry18 (1997), 305–363. doi:10.1007/PL00009321

work page doi:10.1007/pl00009321 1997