Exponent-operation contracts

scale changes the exact binary exponent before rounding, and binaryExponent reports the leading binary exponent. The finite contracts reduce each operation to the shared dyadic rounder and status calculation. Zero, infinity, and NaNs have their own equations.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentInt_of_finite_nonzero {fmt : FloatFormat} (value : Model fmt) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) (hsignificand : exact.significand ≠ 0) : value.binaryExponentInt = { value := ↑exact.significand.log2 + exact.exponent }

A finite nonzero input delivers its exact leading exponent without any exception.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentInt_bounds {fmt : FloatFormat} (value : Model fmt) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) (hsignificand : exact.significand ≠ 0) : 2 ^ value.binaryExponentInt.value ≤ ↑exact.significand * 2 ^ exact.exponent ∧ ↑exact.significand * 2 ^ exact.exponent < 2 ^ (value.binaryExponentInt.value + 1)

The integer answer brackets the exact finite magnitude between consecutive powers of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentSentinel_outside_logBBound (fmt : FloatFormat) : 2 * |logBBound fmt| < binaryExponentSentinel fmt ∧ -binaryExponentSentinel fmt < -(2 * |logBBound fmt|)

The exceptional integer is strictly beyond the IEEE integer-result bound in either sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentInt_of_zero {fmt : FloatFormat} (value : Model fmt) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) (hsignificand : exact.significand = 0) : value.binaryExponentInt = { value := -binaryExponentSentinel fmt, status := { invalid := true } }

An integer-result exponent query signals invalid on zero, rather than divide-by-zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentInt_of_infinity {fmt : FloatFormat} (value : Model fmt) (negative : Bool) (hvalue : value.exactValue = ExactValue.infinity negative) : value.binaryExponentInt = { value := binaryExponentSentinel fmt, status := { invalid := true } }

Either infinity uses the positive exceptional integer and signals invalid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentInt_of_nan {fmt : FloatFormat} (value : Model fmt) (negative signaling : Bool) (payload : ℕ) (hvalue : value.exactValue = ExactValue.nan negative signaling payload) : value.binaryExponentInt = { value := binaryExponentSentinel fmt, status := { invalid := true } }

Both quiet and signaling NaNs signal invalid for an integer-result exponent query.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_scale {fmt : FloatFormat} (value : Model fmt) (n : ℤ) (mode : IEEERoundingMode) : (value.scale n mode true).value = value.scale n mode

Scaling with status := true delivers the value of scaling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scale_status_of_finite {fmt : FloatFormat} (value : Model fmt) (n : ℤ) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : value.scale n mode true = have scaled := { negative := exact.negative, significand := exact.significand, exponent := exact.exponent + n }; have rounded := Internal.Directed.roundDyadic fmt mode scaled; { value := rounded, status := dyadicRoundingStatus fmt mode scaled rounded, ternary := dyadicTernary scaled rounded }

On finite input, scale changes only the exact binary exponent before rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scale_zero_status_of_finite {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : value.scale 0 mode true = have rounded := Internal.Directed.roundDyadic fmt mode exact; { value := rounded, status := dyadicRoundingStatus fmt mode exact rounded, ternary := dyadicTernary exact rounded }

Scaling by zero uses the ordinary one-round exact-dyadic path.

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

scale returns either infinity unchanged and raises no exception.

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

scale quiets a NaN and raises invalid exactly for a signaling NaN.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_binaryExponent {fmt : FloatFormat} (value : Model fmt) : (value.binaryExponent true).value = value.binaryExponent

binaryExponent with status := true delivers the value of binaryExponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponent_status_of_finite_nonzero {fmt : FloatFormat} (value : Model fmt) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) (hsignificand : exact.significand ≠ 0) : value.binaryExponent true = have exponent := Int.ofNat exact.significand.log2 + exact.exponent; have exactResult := Numerics.Dyadic.ofScaledInt exponent 0; have rounded := roundDyadic fmt exactResult; { value := rounded, status := dyadicRoundingStatus fmt IEEERoundingMode.nearest exactResult rounded, ternary := dyadicTernary exactResult rounded }

For a nonzero finite dyadic ±m * 2^e with m > 0, binaryExponent returns the rounded encoding of the integer floor(log₂ m) + e.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponent_status_of_zero {fmt : FloatFormat} (value : Model fmt) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) (hsignificand : exact.significand = 0) : value.binaryExponent true = { value := nativeOverflow fmt true, status := { divideByZero := true }, ternary := exactInfinityTernary true (nativeOverflow fmt true) }

binaryExponent of finite zero raises divideByZero and returns nativeOverflow fmt true.

For IEEE encodings that value is negative infinity, as IEEE 754-2019 §5.3.3 requires. For the finiteMaxNaN and finiteUnsignedZero encodings, which have no infinity, it is the encoding's NaN word, with the same divideByZero flag for the zero input. The finite encoding saturates to its most negative finite value. The ternary value compares that delivery with the exact -∞.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponent_status_of_infinity {fmt : FloatFormat} (value : Model fmt) (negative : Bool) (hvalue : value.exactValue = ExactValue.infinity negative) : value.binaryExponent true = { value := nativeOverflow fmt false, status := Numerics.IEEEStatus.clear, ternary := exactInfinityTernary false (nativeOverflow fmt false) }

binaryExponent of either infinity returns nativeOverflow fmt false and raises no exception. For IEEE encodings this is positive infinity. The ternary value compares that delivery with the exact +∞.

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

binaryExponent quiets a NaN and raises invalid exactly for a signaling NaN.