Floating-Point Operation Accuracy

This file establishes accuracy lemmas for the basic floating-point operations BPLUS, BMINUS, BMULT, and BFMA as defined in the VCFloat library. Each operation is analyzed in the round-to-nearest-even (RNE) rounding mode. The central results take the form of the standard rounding error model: given that a floating-point operation does not overflow, its result fl(op) satisfies a bound of the form \[ \mathtt{fl}(a \mathbin{\mathrm{op}} b) = (a \mathbin{\mathrm{op}} b)(1 + \delta) + \varepsilon \] where the relative error \(\delta\) and absolute error \(\varepsilon\) satisfy \[ |\delta| \leq \mathbf{u}, \qquad |\varepsilon| \leq \eta, \qquad \delta \cdot \varepsilon = 0 \] and where \(\mathbf{u}\) denotes the unit roundoff and \(\eta\) denotes the underflow threshold for the given floating-point type t . The mutual exclusion condition \(\delta \cdot \varepsilon = 0\) reflects the standard decomposition: in the normal range only relative error is incurred, while in the subnormal range only absolute error is incurred. For BPLUS and BMINUS the error model simplifies to \(\mathtt{fl}(a \mathbin{\mathrm{op}} b) = (a \mathbin{\mathrm{op}} b)(1 + \delta)\), since addition and subtraction on floating-point numbers that are already representable incur only relative error.

Structure

The file is organized as follows:

• Signed zero lemmas: behavior of operations when one argument is zero.
• Signed zero facts: FT2R evaluations at signed zeros.
• No-overflow predicates: fma_no_overflow, Bmult_no_overflow, Bplus_no_overflow, Bminus_no_overflow.
• Generic rounding lemma: generic_round_property, which extracts the \((\delta, \varepsilon)\) decomposition from the Flocq library for an arbitrary real number.
• Per-operation accuracy and finiteness lemmas for BFMA, BMULT, BPLUS, and BMINUS, each in two forms:
  • a form assuming a no-overflow hypothesis on real-valued arguments;
  • a primed form (fma_accurate', BMULT_accurate', etc.) assuming only that the floating-point result is finite, from which the no-overflow condition is derived automatically.
• Correctness lemmas (BFMA_correct, BMULT_correct, BPLUS_correct): these combine the finiteness of inputs and the rounding identity into a single conclusion.

Signed Zero Lemmas

Behavior of BMULT, BPLUS, and BFMA when one operand evaluates to zero under FT2R. These are used in higher-level proofs to eliminate zero-valued terms from error bounds.

Signed Zero Values

Signed zeros are finite, and their real-valued interpretations and that of Zconst t 0 under FT2R are all zero. These are used directly in arithmetic simplifications.

No-Overflow Predicates

Each predicate asserts that the RNE-rounded exact result of the corresponding operation has absolute value strictly less than fmax, i.e., the result falls within the normal floating-point range. These are the preconditions for the main accuracy lemmas and are derived automatically in the primed variants.

Generic Rounding Error Decomposition

The lemma below is the shared foundation for all per-operation accuracy results. It packages the Flocq error_N_FLT theorem into the \((\delta, \varepsilon)\) form used throughout this library. generic_round_property is the fundamental \((\delta,\varepsilon)\) decomposition of RNE rounding error in the Flocq FLT format. The condition \(\delta * \varepsilon = 0\) asserts that exactly one of the two error terms is zero, reflecting the fact that the two sources of rounding error are mutually exclusive:

• In the normal range, error is purely relative: \(\varepsilon = 0\).
• In the subnormal range, error is purely absolute: \(\delta = 0\)

No rounding event can simultaneously be in both regimes, so the two error terms never both appear at once.

Fused Multiply-Add

fma_accurate establishes the standard rounding error model for the fused multiply-add operation.

is_finite_fma_no_overflow shows that finiteness of the result of an FMA implies the no-overflow condition on the exact value \(x \cdot y + z\). This allows the primed form fma_accurate' to work directly from a finiteness hypothesis.

BFMA_finite_e extracts finiteness of each individual argument from finiteness of the FMA result. This is a standard regularity property: the IEEE 754 FMA result is non-finite if any input is non-finite (with the exception of a zero-times-infinity addend, which produces a NaN).

is_finite_fma_no_overflow': If all three inputs to an FMA are finite and no overflow occurs, then the FMA result is finite.

fma_accurate' is the finiteness-hypothesis form of fma_accurate: it requires only that the result is finite, deriving the no-overflow condition and input finiteness internally.

BFMA_correct combines BFMA_finite_e and is_finite_fma_no_overflow to give the full correctness statement: finiteness of the result implies finiteness of all inputs and a rounding identity.

Floating-Point Multiplication

BMULT_accurate establishes the rounding error model for multiplication, which computes \(\mathtt{fl}(x \cdot y)\) under RNE rounding.

is_finite_BMULT_no_overflow shows that finiteness of BMULT x y implies that the exact product \(x \cdot y\) does not overflow.

BMULT_accurate' is the finiteness-hypothesis form of BMULT_accurate.

BMULT_finite_e extracts finiteness of each factor from finiteness of the product.

BMULT_correct gives the full correctness statement for multiplication: finiteness of the result implies finiteness of the operands and a rounding identity.

Floating-Point Addition

BPLUS_B2R_zero is a special case: adding the zero constant to a finite value returns a result with the same real value.

BPLUS_accurate establishes the standard relative rounding error model for floating-point addition BPLUS x y.

is_finite_sum_no_overflow shows that finiteness of the result implies the no-overflow condition on the exact sum \(x + y\).

no_overflow_sum_is_finite is the converse direction: if both summands are finite and the exact sum does not overflow, then the result is finite.

BPLUS_accurate' is the finiteness-hypothesis form of BPLUS_accurate.

BPLUS_finite_e extracts finiteness of each summand from finiteness of the sum.

BPLUS_correct gives the full correctness statement for floating-point addition: finiteness of the result implies finiteness of each summand and relates the floating-point result to the rounded real result.

Floating-Point Subtraction

BMINUS_accurate establishes the pure relative rounding error model for floating-point subtraction.

is_finite_minus_no_overflow shows that finiteness of the floating-point result implies that the exact difference does not overflow.

no_overflow_minus_is_finite is the converse direction for subtraction: if both operands are finite and the exact difference does not overflow, then the result is finite.

BMINUS_accurate' is the finiteness-hypothesis form of BMINUS_accurate.

BMINUS_finite_sub extracts finiteness of each operand from finiteness of the difference.