Correctness of nearest-even real rounding

For conventional IEEE descriptors, Model.roundDyadic delegates normalization to Lean's generic logical float model. This module relates that executable result to the independent Flocq-style rounded-real semantics in FloatLib.Floats.Formats.Flocq.FloatRep. Exponent and fraction widths remain symbolic. The grid membership and preservation results also cover custom biases and encoding policies, but the executable rounding refinement requires fmt.isIEEE = true.

The rounded-real model has gradual underflow but no infinities. So refinement theorems assume that the executable result is finite, since an overflowing IEEE result cannot equal a real-valued rounding function.

References

• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019, Section 4.3.1.
• 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 4, Init.Data.Float.Model.Unpacked.Round.

def FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf (fmt : FloatFormat) : ℤ → ℤ

Precision and gradual-underflow grid using the descriptor’s declared exponent bias.

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instValidExpFexpOf (fmt : FloatFormat) : Flocq.ValidExp (fexpOf fmt)

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt (fmt : FloatFormat) (x : ℝ) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : ℝ

Rounding of a real onto the precision and gradual-underflow grid of fmt, with the descriptor's bias, in the direction mode, nearest-even by default.

The real grid has no upper exponent bound. Overflow and exceptional encodings belong to the executable operation, and its equality to roundAt needs the corresponding refinement hypotheses. Nearest-even rounding and the two infinity directions unfold to Flocq's round with nearestEven, ceilRound, and floorRound, and every direction is round (roundingFunction mode) (roundAt_eq_round).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_eq_round (fmt : FloatFormat) (x : ℝ) (mode : IEEERoundingMode) : roundAt fmt x mode = Flocq.round (Flocq.roundingFunction mode) x

Rounding in every direction is Flocq's rounding with the direction's integer rule.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_zero (fmt : FloatFormat) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : roundAt fmt 0 mode = 0

Every rounding direction fixes zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_neg (fmt : FloatFormat) (x : ℝ) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : roundAt fmt (-x) mode = -roundAt fmt x mode.negate

Rounding a negated real gives the negation of rounding the real in the mirrored direction mode.negate, which exchanges the two infinity directions and fixes the other four. Nearest-even rounding commutes with negation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_mono (fmt : FloatFormat) {x y : ℝ} (hxy : x ≤ y) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : roundAt fmt x mode ≤ roundAt fmt y mode

Every rounding direction is monotone in the real input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_genericFormat_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hfin : x.isFinite = true) : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) x.toReal

Every finite decoded word belongs to its descriptor's precision and gradual-underflow grid. The result includes custom biases, FNUZ, and finite-only encodings.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_toReal_eq {fmt : FloatFormat} (x : Model fmt) (hfin : x.isFinite = true) : roundAt fmt x.toReal = x.toReal

Rounding a finite decoded value back to its own format is the identity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.abs_toReal (d : Numerics.Dyadic) : |d.toReal| = ↑d.significand * Flocq.bpow Numerics.binaryRadix d.exponent

The absolute value of a dyadic ignores its stored sign bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.magnitude_toReal (d : Numerics.Dyadic) (hm : d.significand ≠ 0) : Flocq.magnitude Numerics.binaryRadix d.toReal = Int.ofNat d.significand.log2 + d.exponent + 1

A nonzero dyadic has the leading exponent predicted by its integer mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cexp_toReal_eq_targetExponent (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) (hm : d.significand ≠ 0) : Flocq.cexp Numerics.binaryRadix (fexpOf fmt) d.toReal = fmt.toModel.targetExponent (Float.Model.totalExponent d.significand d.exponent)

Lean's model and the rounded-real format choose the same exponent for a nonzero dyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledMantissa_toReal (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) (hm : d.significand ≠ 0) : Flocq.scaledMantissa Numerics.binaryRadix (fexpOf fmt) d.toReal = (if d.negative = true then -1 else 1) * ↑d.significand * Flocq.bpow Numerics.binaryRadix (d.exponent - fmt.toModel.targetExponent (Float.Model.totalExponent d.significand d.exponent))

The canonical scaled mantissa of a dyadic is its signed magnitude at the target exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_scaledMagnitude (mantissa : ℕ) (exponent targetExponent : ℤ) : Flocq.nearestEven (↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = Int.ofNat (roundMantissaAtExponentEven mantissa exponent targetExponent)

Nearest-even rounding of a nonnegative dyadic agrees with executable shift-and-round.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_scaledDyadic (sign : Bool) (mantissa : ℕ) (exponent targetExponent : ℤ) : Flocq.nearestEven ((if sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = if sign = true then -Int.ofNat (roundMantissaAtExponentEven mantissa exponent targetExponent) else Int.ofNat (roundMantissaAtExponentEven mantissa exponent targetExponent)

Nearest-even rounding commutes with the sign stored in a dyadic value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.natCast_pow2_eq_bpow (exponent : ℕ) : ↑(pow2 exponent) = Flocq.bpow Numerics.binaryRadix ↑exponent

The executable natural power of two has the same real value as the binary radix power.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_dyadic_eq (fmt : FloatFormat) (d : Numerics.Dyadic) (hfmt : fmt.isIEEE = true) (hm : d.significand ≠ 0) : have target := fmt.toModel.targetExponent (Float.Model.totalExponent d.significand d.exponent); have rounded := roundMantissaAtExponentEven d.significand d.exponent target; roundAt fmt d.toReal = ↑(if d.negative = true then -Int.ofNat rounded else Int.ofNat rounded) * Flocq.bpow Numerics.binaryRadix target

Rounded-real semantics of a nonzero dyadic at a conventional IEEE descriptor.

The integer on the right is computed entirely by shifts and nearest-even rounding. The exponent is chosen by Lean's generic logical float model and independently characterized by fexpOf.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_finishRoundedMantissa_minSubnormal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (rounded : ℕ) (hle : rounded ≤ pow2 fmt.fracWidth) : (ofModel fmt (finishRoundedMantissa fmt.toModel sign (rounded, fmt.ieeeMinSubnormalExponent))).toReal = (if modelSignBit sign = true then -1 else 1) * (↑rounded * Flocq.bpow Numerics.binaryRadix fmt.ieeeMinSubnormalExponent)

Real value of a finished rounded mantissa on the subnormal grid.

The mantissa may be zero, in which case the packed value is a signed zero, or reach 2 ^ fracWidth, in which case it is the least normal value. Both have the stated real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_finishRoundedMantissa_normal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (rounded : ℕ) (k : ℤ) (hlow : pow2 fmt.fracWidth ≤ rounded) (hhigh : rounded ≤ pow2 (fmt.fracWidth + 1)) (hk : fmt.ieeeMinNormalExponent ≤ k) (hfin : (ofModel fmt (finishRoundedMantissa fmt.toModel sign (rounded, k - ↑fmt.fracWidth))).isFinite = true) : (ofModel fmt (finishRoundedMantissa fmt.toModel sign (rounded, k - ↑fmt.fracWidth))).toReal = (if modelSignBit sign = true then -1 else 1) * (↑rounded * Flocq.bpow Numerics.binaryRadix (k - ↑fmt.fracWidth))

Real value of a finished normalized rounded mantissa with leading bit at unbiased exponent k.

The mantissa lies in [2 ^ fracWidth, 2 ^ (fracWidth + 1)]. The upper endpoint is the carry that finishRoundedMantissa renormalizes to exponent k + 1. The finiteness hypothesis excludes IEEE overflow, which has no value in ℝ.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundDyadic_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (d : Numerics.Dyadic) (hfin : (roundDyadic fmt d).isFinite = true) : (roundDyadic fmt d).toReal = roundAt fmt d.toReal

Executable dyadic rounding refines the rounded-real semantics for conventional IEEE descriptors.

The finiteness hypothesis excludes the one case that has no value in ℝ: IEEE overflow to infinity. Custom widths are allowed when they satisfy the IEEE-descriptor condition.