Integral-rounding contracts

The unbounded dyadic-to-integer kernel is related to the usual nearest-even, nearest-away, floor, ceiling, truncation, and away-from-zero semantics. The floating-point wrapper then records exactly when fractional bits were discarded and exposes the exceptional branches.

For IEEE encodings with fmt.fracWidth ≤ fmt.maxNormalExponent, the selected integer is exactly representable. This condition holds for the IEEE interchange formats. On finite inputs, roundToIntegral then denotes the integer selected by the rounding direction and reports no overflow. Truncation toward zero needs no such range condition: its result cannot exceed the input magnitude. Nearest-away rounding is roundToIntegralTiesToAway of IEEE 754-2019, Section 5.9, and it is Flocq's nearestChoice with the tie choice nearestAwayChoice.

References

• IEEE 754-2019, Sections 4.3.2 and 5.9 (directed and integral rounding). https://doi.org/10.1109/IEEESTD.2019.8766229

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_zero (mode : IEEERoundingMode) : roundDyadicToInt mode Numerics.Dyadic.zero = 0

Exact zero rounds to integer zero in every direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_nearest (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.nearest value = Flocq.nearestEven value.toReal

Nearest-even integer rounding has its usual mathematical meaning, independently of the stored dyadic exponent or magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_up (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.up value = ⌈value.toReal⌉

Rounding toward positive infinity computes the mathematical ceiling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_down (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.down value = ⌊value.toReal⌋

Rounding toward negative infinity computes the mathematical floor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_towardZero (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.towardZero value = if 0 ≤ value.toReal then ⌊value.toReal⌋ else ⌈value.toReal⌉

Rounding toward zero truncates the exact dyadic: nonnegative values use floor and negative values use ceiling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_nearestAway (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.nearestAway value = Flocq.nearestChoice Flocq.nearestAwayChoice value.toReal

Nearest-away integer rounding is Flocq's nearest rounding with ties away from zero, independently of the stored dyadic exponent or magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_away (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.away value = if 0 ≤ value.toReal then ⌈value.toReal⌉ else ⌊value.toReal⌋

Rounding away from zero takes the ceiling of a nonnegative exact dyadic and the floor of a negative one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral_ofNat (negative : Bool) (significand exponent : ℕ) : dyadicIsIntegral { negative := negative, significand := significand, exponent := Int.ofNat exponent } = true

A dyadic with a nonnegative exponent is already an integer.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral_zero (negative : Bool) (exponent : ℤ) : dyadicIsIntegral { negative := negative, significand := 0, exponent := exponent } = true

Dyadic zero is integral independently of its stored sign and exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral_iff (value : Numerics.Dyadic) : dyadicIsIntegral value = true ↔ match value.exponent with | Int.ofNat a => True | Int.negSucc shift => 2 ^ (shift + 1) ∣ value.significand

An exact dyadic is integral exactly when no negative binary exponent leaves a fractional bit.

For exponent -(shift + 1), this says that 2^(shift + 1) divides the significand. A nonnegative exponent is always integral.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_roundToIntegral {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) : (value.roundToIntegral mode true).value = value.roundToIntegral mode

Integral rounding with status := true delivers the value of integral rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_inexact_iff {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : (value.roundToIntegral mode true).status.inexact = true ↔ match exact.exponent with | Int.ofNat a => False | Int.negSucc shift => ¬2 ^ (shift + 1) ∣ exact.significand

On finite input, roundToIntegral raises inexact exactly when a negative binary exponent leaves at least one fractional bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_status_of_infinity {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (negative : Bool) (hvalue : value.exactValue = ExactValue.infinity negative) : value.roundToIntegral mode true = { value := value, status := Numerics.IEEEStatus.clear, ternary := Ordering.eq }

roundToIntegral returns either infinity unchanged, with clear status.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_status_of_nan {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (negative signaling : Bool) (payload : ℕ) (hvalue : value.exactValue = ExactValue.nan negative signaling payload) : value.roundToIntegral mode true = { value := value.quietNaN, status := { invalid := signaling }, ternary := Ordering.eq }

roundToIntegral quiets a NaN and raises invalid exactly when it was signaling.

Representability of the rounded integer

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_le_roundDyadicToInt (mode : IEEERoundingMode) (value : Numerics.Dyadic) : ⌊value.toReal⌋ ≤ roundDyadicToInt mode value

Every rounding direction lands at or above the floor of the exact value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_le_ceil (mode : IEEERoundingMode) (value : Numerics.Dyadic) : roundDyadicToInt mode value ≤ ⌈value.toReal⌉

Every rounding direction lands at or below the ceiling of the exact value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_roundDyadicToInt_le_two_pow_of_exponent_neg (mode : IEEERoundingMode) (value : Numerics.Dyadic) (fracWidth : ℕ) (hsig : value.significand < 2 ^ (fracWidth + 1)) (hexp : value.exponent < 0) : |roundDyadicToInt mode value| ≤ 2 ^ fracWidth

If the significand is below 2^(fracWidth + 1) and the binary exponent is negative, the rounded integer has magnitude at most 2^fracWidth.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_ofScaledInt_zero (c : ℤ) : (Numerics.Dyadic.ofScaledInt c 0).toReal = ↑c

An integer placed at exponent zero denotes itself.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_status_of_finite {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : value.roundToIntegral mode true = have coefficient := roundDyadicToInt mode exact; have rounded := if (coefficient == 0) = true then zero fmt exact.negative else Internal.Directed.roundDyadic fmt mode (Numerics.Dyadic.ofScaledInt coefficient 0); have encodingStatus := dyadicRoundingStatus fmt mode (Numerics.Dyadic.ofScaledInt coefficient 0) rounded; { value := rounded, status := { overflow := encodingStatus.overflow, inexact := !dyadicIsIntegral exact }, ternary := dyadicTernary exact rounded }

On finite input, roundToIntegral rounds the exact dyadic to an unbounded integer, then encodes that integer in the selected direction. The status records discarded fractional bits and the encoder's overflow classification, and the ternary value compares the delivered value with the input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_finite_exact {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : isFinite (value.roundToIntegral mode) = true ∧ toReal (value.roundToIntegral mode) = ↑(roundDyadicToInt mode exact) ∧ (value.roundToIntegral mode true).status.overflow = false

On a finite input of an IEEE format whose exponent range reaches the precision, the selected integer is represented exactly and reports no overflow. Fractional input can still set inexact. The range condition holds for IEEE 754's standard binary interchange formats.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_roundDyadicToInt_towardZero_le (value : Numerics.Dyadic) : |↑(roundDyadicToInt IEEERoundingMode.towardZero value)| ≤ |value.toReal|

Truncation toward zero cannot increase the magnitude of an exact dyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_roundToIntegral_towardZero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : isFinite (value.roundToIntegral IEEERoundingMode.towardZero) = true

Truncating a finite IEEE value toward zero is finite, for any exponent range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_towardZero_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : toReal (value.roundToIntegral IEEERoundingMode.towardZero) = if 0 ≤ value.toReal then ↑⌊value.toReal⌋ else ↑⌈value.toReal⌉

Truncation toward zero computes floor or ceiling without an exponent-range restriction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_towardZero_overflow_eq_false {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : (value.roundToIntegral IEEERoundingMode.towardZero true).status.overflow = false

Truncation toward zero of a finite IEEE value never signals overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_overflow_eq_false {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (hfinite : value.isFinite = true) : (value.roundToIntegral mode true).status.overflow = false

Integral rounding of a finite IEEE value never overflows when fmt.fracWidth ≤ fmt.maxNormalExponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_roundToIntegral {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (hfinite : value.isFinite = true) : isFinite (value.roundToIntegral mode) = true

Integral rounding of a finite IEEE value is finite when the exponent range reaches the precision.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hd : value.toDyadic? = some exact) : toReal (value.roundToIntegral mode) = ↑(roundDyadicToInt mode exact)

The real value of a finite integral rounding is the integer selected by roundDyadicToInt.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exists_int_toReal_roundToIntegral {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (hfinite : value.isFinite = true) : ∃ (n : ℤ), toReal (value.roundToIntegral mode) = ↑n

The result of integral rounding is an integer.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_down {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : toReal (value.roundToIntegral IEEERoundingMode.down) = ↑⌊value.toReal⌋

Rounding toward negative infinity computes the floor of the real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_up {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : toReal (value.roundToIntegral IEEERoundingMode.up) = ↑⌈value.toReal⌉

Rounding toward positive infinity computes the ceiling of the real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_towardZero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : toReal (value.roundToIntegral IEEERoundingMode.towardZero) = if 0 ≤ value.toReal then ↑⌊value.toReal⌋ else ↑⌈value.toReal⌉

Rounding toward zero truncates the real value: floor when nonnegative, ceiling otherwise.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_nearestAway {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : toReal (value.roundToIntegral IEEERoundingMode.nearestAway) = ↑(Flocq.nearestChoice Flocq.nearestAwayChoice value.toReal)

Rounding to nearest with ties away from zero computes the nearest integer and resolves a tie toward the integer of larger magnitude, roundToIntegralTiesToAway of IEEE 754-2019. This is Flocq's nearestChoice nearestAwayChoice.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_away {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : toReal (value.roundToIntegral IEEERoundingMode.away) = if 0 ≤ value.toReal then ↑⌈value.toReal⌉ else ↑⌊value.toReal⌋

Rounding away from zero computes the ceiling of a nonnegative value and the floor of a negative one, as MPFR's mpfr_rint does under MPFR_RNDA.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_nearest {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : toReal value.roundToIntegral = ↑(Flocq.nearestEven value.toReal)

Rounding to nearest computes the nearest integer with ties to even, nearestEven from the Flocq theory. Mathlib's round resolves ties toward positive infinity.