Binary-interchange formats #

Descriptors for sign/exponent/fraction encodings, with exact decoding, directed and status-bearing arithmetic, software backends, and refinement proofs. The descriptors cover IEEE layouts and finite-only exceptional-value policies.

Configured supplies the ExecFloat.Binary API. The descriptor-level Model supports bit-level and mathematical proofs. Scalar conversions and finite reductions are included. Reductions accumulate the exact sum or dot product and round the final result once. Square, reciprocal square root, hypotenuse, integer powers, and integer-degree roots also round once, with real-rounding theorems for conventional IEEE descriptors.

References #

IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, https://doi.org/10.1109/IEEESTD.2019.8766229.
Open Compute Project, 8-bit Floating Point Specification, revision 1.0, https://www.opencompute.org/documents/ocp-8-bit-floating-point-specification-ofp8-revision-1-0-2023-12-01-pdf-1.

Runtime #

Public runtime entry point for the generic kernel (Model fmt): layout, the five IEEE rounding directions and rounding away from zero, exception status, dyadic/rational rounding, arithmetic, comparisons, format casts, outward-rounded intervals, mixed-precision mulAcc / dotSequential / matmul, and standard numeric instances.

Elementary functions (exp, log, sin, ...) and Model.pow are not on this import. Import FloatLib.Floats.Formats.BinaryInterchange.Configured.Transcendentals (or the model barrel BinaryInterchange.Transcendentals) by name to install Model.exp, Model.pow, and MathFunctions. These are software approximation kernels without a general accuracy theorem, and they do not call the host FPU. For an IEEE descriptor, Model.pow with a finite nonzero base and a finite integral exponent is correctly rounded whenever its result is finite (Model.Power.toReal_pow_of_eq_intCast), and a finite positive base with any other finite exponent is correctly rounded whenever its certified enclosure search settles (Model.Power.pow_spec_of_certified). Certified sqrt and abs are available here, but their MathFunctions aliases need the elementary-function import.

Import FloatLib.Floats.ExecFloat for the universal capability API, or this module for descriptor-model execution. Import FloatLib.Floats.Formats.BinaryInterchange.Semantics for the descriptor model's real-refinement theorems.