Exponent-operation contracts

scaleB changes an exact binary exponent before one rounding step; logB reports the leading binary exponent. The finite contracts reduce each operation to the shared dyadic rounder and status calculation. Separate equations give the value and flags for zero, infinity, and NaNs.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleB_eq_value {fmt : FloatFormat} (value : Model fmt) (scale : ℤ) (mode : IEEERoundingMode) : value.scaleB scale mode = (value.scaleBWithStatus scale mode).value

scaleB is exactly the value component of its status-bearing operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleBWithStatus_of_finite {fmt : FloatFormat} (value : Model fmt) (scale : ℤ) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : value.scaleBWithStatus scale mode = have scaled := { negative := exact.negative, significand := exact.significand, exponent := exact.exponent + scale }; have rounded := roundDyadicWithRounding fmt mode scaled; { value := rounded, status := dyadicRoundingStatus fmt mode scaled rounded }

On finite input, scaleB changes only the exact power-of-two exponent before the one selected rounding operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleBWithStatus_zero_of_finite {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : value.scaleBWithStatus 0 mode = have rounded := roundDyadicWithRounding fmt mode exact; { value := rounded, status := dyadicRoundingStatus fmt mode exact rounded }

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleBWithStatus_of_infinity {fmt : FloatFormat} (value : Model fmt) (scale : ℤ) (mode : IEEERoundingMode) (negative : Bool) (hvalue : value.exactValue = ExactValue.infinity negative) : value.scaleBWithStatus scale mode = { value := value, status := IEEEStatus.clear }

scaleB preserves either infinity and raises no exception.

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

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

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.logB_eq_value {fmt : FloatFormat} (value : Model fmt) : value.logB = value.logBWithStatus.value

logB is exactly the value component of its status-bearing operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.logBWithStatus_of_finite_nonzero {fmt : FloatFormat} (value : Model fmt) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) (hsignificand : exact.significand ≠ 0) : value.logBWithStatus = 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.nearestEven exactResult rounded }

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

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

logB 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.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.logBWithStatus_of_infinity {fmt : FloatFormat} (value : Model fmt) (negative : Bool) (hvalue : value.exactValue = ExactValue.infinity negative) : value.logBWithStatus = { value := nativeOverflow fmt false, status := IEEEStatus.clear }

logB of either infinity returns nativeOverflow fmt false and raises no exception. For IEEE encodings this is positive infinity.

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

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