Mechanizing Olver's Error Arithmetic

TL;DR

The paper addresses certifying rounding errors in floating-point computations by adopting Olver's relative-precision metric and formalizing it in the Rocq proof assistant, establishing connections to the standard rounding model. It provides a rigorous Rp-based framework with a concrete $ρ$-style error model, proves key properties (including symmetry, composition, and triangle inequality), and demonstrates a concrete inner-product error bound $s \sim s̃ ; rp\left(\frac{n u}{1-u}\right)$. It also corrects ill-defined sign-related issues in the original definitions and delivers a runnable Rocq formalization with an inner-product example, released under an open-source license. Collectively, the work enables structured, composable, and certifiable error bounds for numerical algorithms and paves the way for integration with automated verification tools in numerical analysis.

Abstract

We mechanize the fundamental properties of a rounding error model for floating-point arithmetic based on relative precision, a measure of error proposed as a substitute for relative error in rounding error analysis. A key property of relative precision is that it forms a true metric, providing a well-defined measure of distance between exact results and their floating-point approximations while offering a structured approach to propagating error bounds through sequences of computations. Our mechanization formalizes this property, establishes rules for converting between relative precision and relative error, and shows that the rounding error model based on relative precision slightly overapproximates the standard rounding error model. Finally, we demonstrate, with a simple example of the inner product of two vectors, that this alternative model facilitates a tractable approach to developing certified rounding error bounds.

Theorems & Definitions (12)

• Theorem 2.1
• Theorem 3.1
• Definition 3.1: Relative Precision (\repo/\slug/relative_prec.v#L8)
• Theorem 3.2
• Theorem 3.3
• Theorem 3.4
• Corollary 3.4.1
• Definition 3.2: Absolute Precision (\repo/\slug/absolute_prec.v#L8)
• Theorem 3.5
• Theorem 3.6