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; the executable rounding refinement requires fmt.isIEEE = true.

The rounded-real model has gradual underflow but no infinities. Consequently refinement theorems carry an explicit hypothesis that the executable result is finite; 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)

@[reducible, inline]

noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt (fmt : FloatFormat) (x : ℝ) : ℝ

Nearest-even rounding with the descriptor's precision, bias, and gradual underflow.

The real grid has no upper exponent bound. Overflow and exceptional encodings belong to the executable operation; its equality to roundAt needs the corresponding refinement hypotheses.

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

Nearest-even rounding on a binary format fixes zero.

@[simp]

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

Nearest-even rounding on a binary format commutes with negation.

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

Nearest-even rounding is monotone on the exact 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 an exact 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. Both the IEEE-descriptor condition and result finiteness are explicit hypotheses; custom widths are allowed when they satisfy that descriptor condition.