Flocq-style rounded-real theory

This umbrella exports the radix-parametric format and rounding theory, exact mantissa/exponent negation and multiplication, and the rounded scalar NF. The theory is independent of concrete IEEE bit encodings. Its main definitions are FloatRep, genericFormat, round, ulp, and bpow.

Import a child module for a smaller dependency set; import this module for the full theory.

Analysis

The Analysis modules provide ULP functions, adjacent representable values, and Sterbenz exact-subtraction results. The representability of the rounded-addition error, which is the specification of the TwoSum and FastTwoSum error-free transformations, is proved in Theory.Error.Addition; the operation-level exactness of those algorithms is not formalized.

Error

The Error modules collect the generic error results used by format-specific BinaryInterchange.Model.roundAt theorems, runtime-refinement proofs, verifier margins, and numerical analyses.

Format

The Format modules develop magnitude, exponent selection, and representability, following Flocq's generic-format organization. A client that only needs a format predicate can import its defining module without the rounding and error theory.

Rounding

The Rounding modules contain rounding functions and their semantic laws: directed modes, nearest choices, order properties, round-to-odd, round-away, and double rounding. A format supplies the representable grid and a rounding policy selects a point on that grid.

Scalar

NF is the scalar-facing interface to generic rounding. This folder keeps the carrier and its representability invariant together. The raw carrier may contain any real value; statements that require membership in the declared grid use NF.IsRepresentable explicitly.

References

• S. Boldo and G. Melquiond, "Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq," IEEE ARITH, 2011, doi:10.1109/ARITH.2011.40.
• IEEE, IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, Sections 4 and 7.
• P. H. Sterbenz, Floating-Point Computation, Prentice-Hall, 1974.
• N. J. Higham, Accuracy and Stability of Numerical Algorithms, second edition, SIAM, 2002.
• D. Goldberg, "What Every Computer Scientist Should Know About Floating-Point Arithmetic," ACM Computing Surveys 23(1), 1991, doi:10.1145/103162.103163.