Correctness of normalization through Lean's logical float model #
The executable rounding primitives in ModelRounding.Runtime agree with Lean 4's
width-parameterized Float.Model.UnpackedFloat.round. The normalization theorem is generic in
the model format. Lemmas using FloatFormat.toModel use the conventional IEEE bias at the
descriptor's field widths.
The model represents discarded information with a round bit and a sticky bit. Model uses an
integer shift followed by nearest-even rounding. The main result,
round_exact_eq_finishRoundedMantissa, proves that these two representations compute the same
rounded mantissa and target exponent.
References #
- IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, Section 4.3.1.
- Lean 4,
Init.Data.Float.Model.Unpacked.Round. - S. Boldo and G. Melquiond, "Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq," ARITH 2011. https://doi.org/10.1109/ARITH.2011.40
Lean's quotient-plus-accuracy representation makes the same nearest-even choice as
Numerics.roundQuotientEven.
Shifting an exact mantissa and rounding its discarded bits agrees with the executable nearest-even shift for every shift distance.
Adding a remainder below half an ulp to a left-shifted mantissa does not change nearest-even rounding.
Subtracting a remainder below half an ulp from a positive left-shifted mantissa does not change nearest-even rounding.
A nonzero mantissa rounded to leading position p is at least 2^p.
Rounding to leading position p can produce at most the one-bit carry 2^(p+1).
Rounding at the exponent that places the leading bit at leadingBit is direct shift-round.
Lean's logical model and FloatFormat compute the same minimum dyadic exponent.
Removing the model precision from a total exponent leaves the usual normal scale.
Below the normal range, every exact dyadic is rounded on the subnormal exponent grid.
In the normal range, the target exponent places the leading bit at fmt.fracWidth.
A nonzero mantissa at most 2^fmt.fracWidth stays on the minimum-exponent grid.
No bits move when a fitting mantissa is already represented at the minimum exponent.
A mantissa between 2^p and 2^(p+1) has leading bit exactly at position p.
A normalized mantissa at leading exponent k needs no second normalization shift.
The only extra bit produced by nearest-even normalization is shifted away exactly.
An exact dyadic below the normal range rounds to at most 2^p units of the minimum exponent.
Here p = fmt.fracWidth; equality is the carry from the largest subnormal neighborhood to the
smallest normal value.
Lean's decrease-then-shift normalization agrees with direct nearest-even rounding.
Decreasing an exact dyadic exponent preserves the leading binary position.
The first exact model-rounding stage uses the original dyadic's target exponent.
A zero rounded mantissa remains signed zero, independently of the provisional exponent.
A nonzero rounded mantissa on the minimum-exponent grid, up to the smallest normal value, needs no second shift.
A normalized rounded mantissa remains unchanged in the second rounding stage.
A one-bit normalization carry becomes 2^p at the next exponent.
The final stage of roundWithAccuracy is finishRoundedMantissa.
roundWithAccuracy agrees with unrestricted rounding when no preliminary left shift is needed.
Exact dyadic model rounding factors through the direct target-exponent rounder.