Correctness of IEEE exception status

The executable status kernels in Status.Runtime satisfy cross-flag invariants and operation-level specifications. Import BinaryInterchange.Status for the combined public interface.

The rounding-status classifiers compare an exact dyadic or scaled rational with the supplied rounded value. Operation wrappers compute that exact witness alongside the value-only operation. This file proves cross-flag invariants, preservation of the ordinary result, real-order tininess boundaries, and operation-specific invalid and divide-by-zero conditions. On a positive finite input, square root raises inexact exactly when its delivered value is not the real square root (sqrt_inexact_iff).

Constructors and rounding-status invariants

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isTinyAfterRounding_eq_true_iff {fmt : FloatFormat} (rounded : Model fmt) : rounded.isTinyAfterRounding = true ↔ rounded.isFinite = true ∧ rounded.expField = 0

The direct result classifier recognizes exactly finite zero and subnormal encodings.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.underflow_boundary_gaps (fmt : FloatFormat) : (underflowMidpoint fmt).toReal - (underflowPredecessor fmt).toReal = Flocq.bpow Numerics.binaryRadix (fmt.minSubnormalExponent - 2) ∧ (minNormalDyadic fmt).toReal - (underflowMidpoint fmt).toReal = Flocq.bpow Numerics.binaryRadix (fmt.minSubnormalExponent - 2)

The underflow midpoint is exactly halfway between the unbounded-grid predecessor and the smallest normal value.

Both gaps are one 2^(minSubnormalExponent - 2) step. The equalities pin down the quarter-subnormal offset used by nearest-even and rule out an off-by-one significand or exponent in the three executable boundary constants.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsTinyAfterRounding_eq_true_iff (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : dyadicIsTinyAfterRounding fmt mode exact rounded = true ↔ rounded.isTinyAfterRounding = true ∨ rounded.isTinyAfterRounding = false ∧ match mode with | IEEERoundingMode.nearest => { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal < (underflowMidpoint fmt).toReal | IEEERoundingMode.nearestAway => { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal < (underflowMidpoint fmt).toReal | IEEERoundingMode.towardZero => { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal < (minNormalDyadic fmt).toReal | IEEERoundingMode.up => if mode.roundsAwayFromZero exact.negative = true then { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal ≤ (underflowPredecessor fmt).toReal else { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal < (minNormalDyadic fmt).toReal | IEEERoundingMode.down => if mode.roundsAwayFromZero exact.negative = true then { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal ≤ (underflowPredecessor fmt).toReal else { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal < (minNormalDyadic fmt).toReal | IEEERoundingMode.away => if mode.roundsAwayFromZero exact.negative = true then { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal ≤ (underflowPredecessor fmt).toReal else { negative := false, significand := exact.significand, exponent := exact.exponent }.toReal < (minNormalDyadic fmt).toReal

Real-order specification of after-rounding dyadic tininess.

An already tiny encoding is accepted immediately. Otherwise both nearest modes use the underflow midpoint, rounding toward zero uses the smallest normal, and a directed mode uses either the unbounded-grid predecessor or the smallest normal according to whether it rounds this sign away from zero. This theorem is the semantic boundary for the executable comparisons in dyadicIsTinyAfterRounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsTinyAfterRounding_nearestAway (fmt : FloatFormat) (exact : Numerics.Dyadic) (rounded : Model fmt) : dyadicIsTinyAfterRounding fmt IEEERoundingMode.nearestAway exact rounded = dyadicIsTinyAfterRounding fmt IEEERoundingMode.nearest exact rounded

Nearest-away rounding detects tininess at the same boundary as nearest-even rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsTinyAfterRoundingScaled_nearestAway (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) : rationalIsTinyAfterRoundingScaled fmt IEEERoundingMode.nearestAway sign numerator denominator exponent rounded = rationalIsTinyAfterRoundingScaled fmt IEEERoundingMode.nearest sign numerator denominator exponent rounded

Nearest-away rounding detects tininess at the same boundary as nearest-even rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsTinyAfterRoundingScaled_eq_true_iff (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) (hdenominator : denominator ≠ 0) : rationalIsTinyAfterRoundingScaled fmt mode sign numerator denominator exponent rounded = true ↔ rounded.isTinyAfterRounding = true ∨ rounded.isTinyAfterRounding = false ∧ match mode with | IEEERoundingMode.nearest => scaledRatToReal numerator denominator exponent < (underflowMidpoint fmt).toReal | IEEERoundingMode.nearestAway => scaledRatToReal numerator denominator exponent < (underflowMidpoint fmt).toReal | IEEERoundingMode.towardZero => scaledRatToReal numerator denominator exponent < (minNormalDyadic fmt).toReal | IEEERoundingMode.up => if mode.roundsAwayFromZero sign = true then scaledRatToReal numerator denominator exponent ≤ (underflowPredecessor fmt).toReal else scaledRatToReal numerator denominator exponent < (minNormalDyadic fmt).toReal | IEEERoundingMode.down => if mode.roundsAwayFromZero sign = true then scaledRatToReal numerator denominator exponent ≤ (underflowPredecessor fmt).toReal else scaledRatToReal numerator denominator exponent < (minNormalDyadic fmt).toReal | IEEERoundingMode.away => if mode.roundsAwayFromZero sign = true then scaledRatToReal numerator denominator exponent ≤ (underflowPredecessor fmt).toReal else scaledRatToReal numerator denominator exponent < (minNormalDyadic fmt).toReal

Real-order specification of after-rounding tininess for scaled rationals.

The denominator premise excludes the malformed representation for which the executable comparator returns none. For every valid rational, the optimized leading-exponent comparison has the same mode-sensitive boundaries as the dyadic classifier above.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsTinyAfterRoundingScaled_eq_dyadic (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : rationalIsTinyAfterRoundingScaled fmt mode exact.negative exact.significand 1 exact.exponent rounded = dyadicIsTinyAfterRounding fmt mode exact rounded

The dyadic and scaled-rational tininess classifiers agree when the rational has denominator one.

This bridge lets operation proofs choose the representation natural to their exact arithmetic without creating two notions of IEEE underflow.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.outcomeWithInvalid_value {fmt : FloatFormat} (value : Model fmt) (invalid : Bool) : (value.outcomeWithInvalid invalid).value = value

outcomeWithInvalid preserves its supplied floating-point value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.outcomeWithInvalid_invalid {fmt : FloatFormat} (value : Model fmt) (invalid : Bool) : (value.outcomeWithInvalid invalid).status.invalid = invalid

outcomeWithInvalid records its supplied invalid-operation condition.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.outcomeWithInvalid_divideByZero {fmt : FloatFormat} (value : Model fmt) (invalid : Bool) : (value.outcomeWithInvalid invalid).status.divideByZero = false

outcomeWithInvalid never raises divide-by-zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.outcomeWithInvalid_ternary {fmt : FloatFormat} (value : Model fmt) (invalid : Bool) : (value.outcomeWithInvalid invalid).ternary = Ordering.eq

outcomeWithInvalid carries the exceptional-result ternary convention .eq.

This is a convention for NaNs, exact infinities, and placeholders, not a statement that the value equals an exact real result.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingOutcome_value (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (value : Model fmt) : (dyadicRoundingOutcome fmt mode exact value).value = value

A dyadic rounding outcome delivers the value it was given.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingOutcome_status (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (value : Model fmt) : (dyadicRoundingOutcome fmt mode exact value).status = dyadicRoundingStatus fmt mode exact value

The status of a dyadic rounding outcome is dyadicRoundingStatus.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingOutcome_ternary (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (value : Model fmt) : (dyadicRoundingOutcome fmt mode exact value).ternary = dyadicTernary exact value

The ternary value of a dyadic rounding outcome is dyadicTernary.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOutcomeScaled_value (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (value : Model fmt) : (rationalRoundingOutcomeScaled fmt mode sign numerator denominator exponent value).value = value

A scaled rational rounding outcome delivers the value it was given.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOutcomeScaled_status (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (value : Model fmt) : (rationalRoundingOutcomeScaled fmt mode sign numerator denominator exponent value).status = rationalRoundingStatusScaled fmt mode sign numerator denominator exponent value

The status of a scaled rational rounding outcome is rationalRoundingStatusScaled.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOutcomeScaled_ternary (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (value : Model fmt) : (rationalRoundingOutcomeScaled fmt mode sign numerator denominator exponent value).ternary = rationalTernaryScaled sign numerator denominator exponent value

The ternary value of a scaled rational rounding outcome is rationalTernaryScaled.

Ternary values

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_eq_toReal_finiteDyadic {fmt : FloatFormat} {x : Model fmt} (hfinite : x.isFinite = true) : x.toReal = (x.finiteDyadic hfinite).toReal

A finite value denotes the real value of its decoded dyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicTernary_eq_compare {fmt : FloatFormat} (exact : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = true) : dyadicTernary exact rounded = Ord.compare rounded.toReal exact.toReal

For a finite delivery, the dyadic ternary value is the real comparison with the exact value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicTernary_eq_lt_iff {fmt : FloatFormat} (exact : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = true) : dyadicTernary exact rounded = Ordering.lt ↔ rounded.toReal < exact.toReal

A finite delivery has the dyadic ternary value .lt exactly when it is below the exact one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicTernary_eq_eq_iff {fmt : FloatFormat} (exact : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = true) : dyadicTernary exact rounded = Ordering.eq ↔ rounded.toReal = exact.toReal

A finite delivery has the dyadic ternary value .eq exactly when it equals the exact value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicTernary_eq_gt_iff {fmt : FloatFormat} (exact : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = true) : dyadicTernary exact rounded = Ordering.gt ↔ exact.toReal < rounded.toReal

A finite delivery has the dyadic ternary value .gt exactly when it is above the exact one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicTernary_of_isFinite_eq_false {fmt : FloatFormat} (exact : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = false) : dyadicTernary exact rounded = if exact.negative = true then Ordering.lt else Ordering.gt

A non-finite delivery has the ternary value given by the sign of the exact value, the overflow convention of dyadicTernary.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_compare {fmt : FloatFormat} (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) {rounded : Model fmt} (hdenominator : denominator ≠ 0) (hfinite : rounded.isFinite = true) : rationalTernaryScaled sign numerator denominator exponent rounded = Ord.compare rounded.toReal (signedScaledRatToReal sign numerator denominator exponent)

For a finite delivery and a nonzero denominator, the rational ternary value is the real comparison with the exact signed rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_lt_iff {fmt : FloatFormat} (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) {rounded : Model fmt} (hdenominator : denominator ≠ 0) (hfinite : rounded.isFinite = true) : rationalTernaryScaled sign numerator denominator exponent rounded = Ordering.lt ↔ rounded.toReal < signedScaledRatToReal sign numerator denominator exponent

A finite delivery has the rational ternary value .lt exactly when it is below the rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_eq_iff {fmt : FloatFormat} (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) {rounded : Model fmt} (hdenominator : denominator ≠ 0) (hfinite : rounded.isFinite = true) : rationalTernaryScaled sign numerator denominator exponent rounded = Ordering.eq ↔ rounded.toReal = signedScaledRatToReal sign numerator denominator exponent

A finite delivery has the rational ternary value .eq exactly when it equals the rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_gt_iff {fmt : FloatFormat} (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) {rounded : Model fmt} (hdenominator : denominator ≠ 0) (hfinite : rounded.isFinite = true) : rationalTernaryScaled sign numerator denominator exponent rounded = Ordering.gt ↔ signedScaledRatToReal sign numerator denominator exponent < rounded.toReal

A finite delivery has the rational ternary value .gt exactly when it is above the rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_of_isFinite_eq_false {fmt : FloatFormat} (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) {rounded : Model fmt} (hfinite : rounded.isFinite = false) : rationalTernaryScaled sign numerator denominator exponent rounded = if sign = true then Ordering.lt else Ordering.gt

A non-finite delivery has the rational ternary value given by the sign of the exact rational, the overflow convention of rationalTernaryScaled.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTernaryScaled_eq_dyadicTernary {fmt : FloatFormat} (exact : Numerics.Dyadic) (rounded : Model fmt) : rationalTernaryScaled exact.negative exact.significand 1 exact.exponent rounded = dyadicTernary exact rounded

With denominator one, the rational ternary value is the dyadic ternary value of the same exact number, so operations may use either representation of their exact result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactInfinityTernary_eq_eq_iff {fmt : FloatFormat} (negative : Bool) (value : Model fmt) : exactInfinityTernary negative value = Ordering.eq ↔ value.isInf = true ∧ value.signBit = negative

The exact-infinity ternary value is .eq exactly for the infinity itself.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactInfinityTernary_of_not_infinity {fmt : FloatFormat} (negative : Bool) {value : Model fmt} (hvalue : ¬(value.isInf = true ∧ value.signBit = negative)) : exactInfinityTernary negative value = if negative = true then Ordering.gt else Ordering.lt

Any delivery other than the exact infinity itself has the exact-infinity ternary value .lt for +∞ and .gt for -∞. For a saturated finite value this is the order, and for the overflow NaN of a format without infinities it is the convention of IEEEOutcome.ternary.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicSqrtTernary_of_isFinite {fmt : FloatFormat} (radicand : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = true) : dyadicSqrtTernary radicand rounded = cmpDyadic { negative := false, significand := (rounded.finiteDyadic hfinite).significand * (rounded.finiteDyadic hfinite).significand, exponent := (rounded.finiteDyadic hfinite).exponent + (rounded.finiteDyadic hfinite).exponent } radicand

A finite delivery is compared with the radicand through the exact square of its decoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicSqrtTernary_of_isFinite_eq_false {fmt : FloatFormat} (radicand : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = false) : dyadicSqrtTernary radicand rounded = Ordering.gt

A non-finite delivery has the square-root ternary value .gt.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicSqrtTernary_eq_compare {fmt : FloatFormat} (radicand : Numerics.Dyadic) {rounded : Model fmt} (hfinite : rounded.isFinite = true) (hrounded : 0 ≤ rounded.toReal) (hradicand : 0 ≤ radicand.toReal) : dyadicSqrtTernary radicand rounded = Ord.compare rounded.toReal √radicand.toReal

For a finite nonnegative delivery and a nonnegative radicand, the square-root ternary value is the real comparison of the delivered value with the exact square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_inexact_of_underflow {fmt : FloatFormat} {mode : IEEERoundingMode} {exact : Numerics.Dyadic} {rounded : Model fmt} (h : (dyadicRoundingStatus fmt mode exact rounded).underflow = true) : (dyadicRoundingStatus fmt mode exact rounded).inexact = true

After-rounding dyadic underflow implies inexactness.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_overflow {fmt : FloatFormat} (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : (dyadicRoundingStatus fmt mode exact rounded).overflow = (dyadicRoundingOverflows fmt mode exact || !rounded.isFinite && rounded.isInf)

Dyadic rounding reports overflow when rounding crosses the format's overflow threshold or when the supplied rounded result is an infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_overflow_of_isFinite {fmt : FloatFormat} (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) (hfinite : rounded.isFinite = true) : (dyadicRoundingStatus fmt mode exact rounded).overflow = dyadicRoundingOverflows fmt mode exact

For a finite result, dyadic overflow is exactly the exact-value overflow classification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_inexact_of_overflow {fmt : FloatFormat} {mode : IEEERoundingMode} {exact : Numerics.Dyadic} {rounded : Model fmt} (h : (dyadicRoundingStatus fmt mode exact rounded).overflow = true) : (dyadicRoundingStatus fmt mode exact rounded).inexact = true

Dyadic rounding overflow always raises inexact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_not_underflow_of_overflow {fmt : FloatFormat} {mode : IEEERoundingMode} {exact : Numerics.Dyadic} {rounded : Model fmt} (h : (dyadicRoundingStatus fmt mode exact rounded).overflow = true) : (dyadicRoundingStatus fmt mode exact rounded).underflow = false

A dyadic rounding result cannot simultaneously signal overflow and underflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_inexact_of_underflow {fmt : FloatFormat} {mode : IEEERoundingMode} {sign : Bool} {numerator denominator : ℕ} {exponent : ℤ} {rounded : Model fmt} (h : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).underflow = true) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).inexact = true

After-rounding scaled rational underflow implies inexactness.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_overflow {fmt : FloatFormat} (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).overflow = (rationalRoundingOverflowsScaled fmt mode sign numerator denominator exponent || !rounded.isFinite && rounded.isInf)

Scaled rational rounding reports overflow when rounding crosses the format's overflow threshold or when the supplied rounded result is an infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_overflow_of_isFinite {fmt : FloatFormat} (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) (hfinite : rounded.isFinite = true) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).overflow = rationalRoundingOverflowsScaled fmt mode sign numerator denominator exponent

For a finite result, scaled rational overflow is exactly the exact-value overflow classification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_inexact_of_overflow {fmt : FloatFormat} {mode : IEEERoundingMode} {sign : Bool} {numerator denominator : ℕ} {exponent : ℤ} {rounded : Model fmt} (h : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).overflow = true) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).inexact = true

Scaled rational overflow always raises inexact.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_not_underflow_of_overflow {fmt : FloatFormat} {mode : IEEERoundingMode} {sign : Bool} {numerator denominator : ℕ} {exponent : ℤ} {rounded : Model fmt} (h : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).overflow = true) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).underflow = false

Scaled rational rounding cannot signal overflow and underflow together.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_invalid (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : (dyadicRoundingStatus fmt mode exact rounded).invalid = (!dyadicRoundingOverflows fmt mode exact && !rounded.isFinite && !rounded.isInf)

Dyadic rounding is invalid exactly for an unclassified non-finite, non-infinite result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_invalid_false_of_isFinite (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) (hfinite : rounded.isFinite = true) : (dyadicRoundingStatus fmt mode exact rounded).invalid = false

A finite dyadic rounding result cannot raise invalid.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus_divideByZero_false (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : (dyadicRoundingStatus fmt mode exact rounded).divideByZero = false

Rounding an exact dyadic never raises divideByZero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_invalid (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).invalid = (!rationalRoundingOverflowsScaled fmt mode sign numerator denominator exponent && !rounded.isFinite && !rounded.isInf)

Scaled rational rounding is invalid exactly for an unclassified non-finite, non-infinite result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_invalid_false_of_isFinite (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) (hfinite : rounded.isFinite = true) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).invalid = false

A finite scaled rational rounding result cannot raise invalid.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled_divideByZero_false (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) : (rationalRoundingStatusScaled fmt mode sign numerator denominator exponent rounded).divideByZero = false

Rounding an exact scaled rational never raises divideByZero.

Result projection

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_add {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.add y mode true).value = x.add y mode

Addition with status := true delivers the value of addition in the same direction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_sub {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.sub y mode true).value = x.sub y mode

Subtraction with status := true delivers the value of subtraction in the same direction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_mul {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.mul y mode true).value = x.mul y mode

Multiplication with status := true delivers the value of multiplication in the same direction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_div {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.div y mode true).value = x.div y mode

Division with status := true delivers the value of division in the same direction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_fma {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode) : (x.fma y z mode true).value = x.fma y z mode

FMA with status := true delivers the value of FMA in the same direction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.value_sqrt {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode) : (x.sqrt mode true).value = x.sqrt mode

Square root with status := true delivers the value of square root in the same direction.

Operation-specific exceptional status

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_status_of_toDyadic {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (mode : IEEERoundingMode) (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.add y mode true = have exact := addDyadic dx dy; have value := x.add y mode; { value := value, status := dyadicRoundingStatus fmt mode exact value, ternary := dyadicTernary exact value }

Finite addition reports its dyadic rounding status and ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_invalid {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.add y mode true).status.invalid = match x.toDyadic?, y.toDyadic? with | some dx, some dy => have exact := addDyadic dx dy; have value := x.add y mode; !dyadicRoundingOverflows fmt mode exact && !isFinite value && !isInf value | x_1, x_2 => x.isSNaN || y.isSNaN || !(x.isNaN || y.isNaN) && (x.isInf && y.isInf && x.signBit != y.signBit)

Complete invalid-status classification for addition.

Finite operands take the rounded result's classification. Exceptional operands raise invalid exactly for a signaling NaN or opposite-signed infinities when no NaN was supplied.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mul_status_of_toDyadic {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (mode : IEEERoundingMode) (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.mul y mode true = have exact := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; have value := x.mul y mode; { value := value, status := dyadicRoundingStatus fmt mode exact value, ternary := dyadicTernary exact value }

Finite multiplication reports its dyadic rounding status and ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mul_invalid {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.mul y mode true).status.invalid = match x.toDyadic?, y.toDyadic? with | some dx, some dy => have exact := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; have value := x.mul y mode; !dyadicRoundingOverflows fmt mode exact && !isFinite value && !isInf value | x_1, x_2 => x.isSNaN || y.isSNaN || !(x.isNaN || y.isNaN) && (x.isInf && y.isZero || y.isInf && x.isZero)

Complete invalid-status classification for multiplication.

Finite operands take the rounded result's classification. Exceptional operands raise invalid exactly for a signaling NaN or an infinity-times-zero operation without an input NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fma_status_of_toDyadic {fmt : FloatFormat} {x y z : Model fmt} {dx dy dz : Numerics.Dyadic} (mode : IEEERoundingMode) (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hz : z.toDyadic? = some dz) : x.fma y z mode true = have product := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; have exact := addDyadic product dz; have value := x.fma y z mode; { value := value, status := dyadicRoundingStatus fmt mode exact value, ternary := dyadicTernary exact value }

Finite FMA reports its dyadic rounding status and ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fma_invalid {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode) : (x.fma y z mode true).status.invalid = match x.toDyadic?, y.toDyadic?, z.toDyadic? with | some dx, some dy, some dz => have product := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; have exact := addDyadic product dz; have value := x.fma y z mode; !dyadicRoundingOverflows fmt mode exact && !isFinite value && !isInf value | x_1, x_2, x_3 => have hasNaN := x.isNaN || y.isNaN || z.isNaN; have invalidProduct := (x.isInf || y.isInf) && (x.isZero || y.isZero); have productIsInf := (x.isInf || y.isInf) && !(x.isZero || y.isZero); have oppositeInfiniteAddend := productIsInf && z.isInf && z.signBit != (x.signBit ^^ y.signBit); x.isSNaN || y.isSNaN || z.isSNaN || invalidProduct || !hasNaN && oppositeInfiniteAddend

Complete invalid-status classification for fused multiply-add.

Finite operands take the singly rounded result's classification. Exceptional operands use the IEEE signaling-NaN, infinity-times-zero, and opposite-infinity rules. For the implementation-defined quiet-NaN case, this library raises invalid for infinity times zero even when the addend is a quiet NaN, while an input NaN suppresses the opposite-infinity condition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_status_of_toDyadic_nonzero {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} (mode : IEEERoundingMode) (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hxnonzero : dx.significand ≠ 0) (hynonzero : dy.significand ≠ 0) : x.div y mode true = have sign := dx.negative ^^ dy.negative; have exponentDifference := dx.exponent - dy.exponent; have value := Internal.Directed.roundRatScaled fmt mode sign dx.significand dy.significand exponentDifference; { value := value, status := rationalRoundingStatusScaled fmt mode sign dx.significand dy.significand exponentDifference value, ternary := rationalTernaryScaled sign dx.significand dy.significand exponentDifference value }

Finite nonzero division reports its scaled-rational rounding status and ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_invalid {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.div y mode true).status.invalid = match x.toDyadic?, y.toDyadic? with | some dx, some dy => have sign := dx.negative ^^ dy.negative; if (dy.significand == 0) = true then dx.significand == 0 else if (dx.significand == 0) = true then false else have exponentDifference := dx.exponent - dy.exponent; have value := Internal.Directed.roundRatScaled fmt mode sign dx.significand dy.significand exponentDifference; !rationalRoundingOverflowsScaled fmt mode sign dx.significand dy.significand exponentDifference && !value.isFinite && !value.isInf | x_1, x_2 => x.isSNaN || y.isSNaN || !(x.isNaN || y.isNaN) && (x.isInf && y.isInf)

Complete invalid-status classification for division.

The finite branch distinguishes zero-over-zero, exact zero, and nonzero rational rounding. Exceptional operands use the signaling-NaN and infinity-over-infinity rules.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_divideByZero {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.div y mode true).status.divideByZero = match x.toDyadic?, y.toDyadic? with | some dx, some dy => dx.significand != 0 && dy.significand == 0 | x, x_1 => false

Division raises divide-by-zero exactly for a finite nonzero numerator over finite zero.

Square-root cases

Square root with status := true tests the sign bit first and decodes an input with a clear sign bit once. The next theorems restate its outcome on NaNs, zeros, negative values, +∞, and positive finite values. These cases cover every input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicSqrtIsTinyAfterRounding_eq_false {fmt : FloatFormat} (mode : IEEERoundingMode) (hformat : fmt.fracWidth + 1 < fmt.exponentBias) {x : Model fmt} {radicand : Numerics.Dyadic} (hx : x.toDyadic? = some radicand) (hzero : radicand.significand ≠ 0) : dyadicSqrtIsTinyAfterRounding fmt mode radicand = false

When fmt.fracWidth + 1 < fmt.exponentBias, the square root of a nonzero decoded radicand never lies below an underflow boundary. The least positive magnitude 2^minSubnormalExponent exceeds the square of minNormal, 2^(2 * minNormalExponent), and every boundary is at most minNormal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_status_of_isNaN {fmt : FloatFormat} {x : Model fmt} (mode : IEEERoundingMode) (hnan : x.isNaN = true) : x.sqrt mode true = outcomeWithInvalid (x.sqrt mode) x.isSNaN

A NaN delivers the square-root value and raises invalid only when it is signaling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_status_of_isZero {fmt : FloatFormat} {x : Model fmt} (mode : IEEERoundingMode) (hzero : x.isZero = true) : x.sqrt mode true = outcomeWithInvalid (x.sqrt mode) false

A zero of either sign delivers the square-root value and raises nothing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_status_of_signBit {fmt : FloatFormat} {x : Model fmt} (mode : IEEERoundingMode) (hnan : x.isNaN = false) (hzero : x.isZero = false) (hsign : x.signBit = true) : x.sqrt mode true = outcomeWithInvalid (x.sqrt mode) true

A negative value that is neither a NaN nor a zero, -∞ included, raises invalid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_status_of_isInf {fmt : FloatFormat} {x : Model fmt} (mode : IEEERoundingMode) (hinf : x.isInf = true) (hsign : x.signBit = false) : x.sqrt mode true = outcomeWithInvalid (x.sqrt mode) false

+∞ delivers the square-root value and raises nothing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_status_of_toDyadic {fmt : FloatFormat} {x : Model fmt} {exact : Numerics.Dyadic} (mode : IEEERoundingMode) (hx : x.toDyadic? = some exact) (hzero : exact.significand ≠ 0) (hsign : exact.negative = false) : x.sqrt mode true = have value := x.sqrt mode; have ternary := dyadicSqrtTernary exact value; have inexact := ternary != Ordering.eq; { value := value, status := { underflow := inexact && (isTinyAfterRounding value || dyadicSqrtIsTinyAfterRounding fmt mode exact), inexact := inexact }, ternary := ternary }

On a positive finite input, the ternary value compares the squared delivery with the radicand, the result is inexact exactly when that comparison is not .eq, and an inexact result underflows when its encoding is zero or subnormal or its exact root lies below the underflow boundary.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_invalid {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode) : (x.sqrt mode true).status.invalid = (x.isSNaN || !x.isNaN && x.signBit && !x.isZero)

Square root raises invalid exactly for an sNaN or a negative nonzero non-NaN input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_invalid_of_zero_div_zero {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} {mode : IEEERoundingMode} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hxzero : dx.significand = 0) (hyzero : dy.significand = 0) : (x.div y mode true).status.invalid = true

Dividing two finite zeros raises invalid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_divideByZero_of_nonzero_div_zero {fmt : FloatFormat} {x y : Model fmt} {dx dy : Numerics.Dyadic} {mode : IEEERoundingMode} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hxnonzero : dx.significand ≠ 0) (hyzero : dy.significand = 0) : (x.div y mode true).status.divideByZero = true

Dividing a finite nonzero value by a finite zero raises divide-by-zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_invalid_of_negative_nonzero {fmt : FloatFormat} {x : Model fmt} {mode : IEEERoundingMode} (hnan : x.isNaN = false) (hnegative : x.signBit = true) (hnonzero : x.isZero = false) : (x.sqrt mode true).status.invalid = true

The square root of a negative nonzero non-NaN value raises invalid.

Square-root inexactness

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_inexact_eq_ternary_bne_eq {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode) : (x.sqrt mode true).status.inexact = ((x.sqrt mode true).ternary != Ordering.eq)

Square root raises inexact exactly when its ternary value is not .eq, on every input. The flag is computed from that value on a positive finite input, and the other cases raise neither.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_inexact_of_underflow {fmt : FloatFormat} {x : Model fmt} {mode : IEEERoundingMode} (h : (x.sqrt mode true).status.underflow = true) : (x.sqrt mode true).status.inexact = true

Square-root underflow implies inexactness.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_inexact_iff {fmt : FloatFormat} (mode : IEEERoundingMode) {x : Model fmt} (hfinite : x.isFinite = true) (hzero : x.isZero = false) (hsign : x.signBit = false) : (x.sqrt mode true).status.inexact = true ↔ (x.sqrt mode true).value.toReal ≠ √x.toReal

On a positive finite input, square root raises inexact exactly when the delivered value is not the real square root of the input, in every rounding direction and for every descriptor.

The flag is computed as the ternary value's difference from .eq (sqrt_inexact_eq_ternary_bne_eq), so on such an input the ternary value is .eq exactly when the delivered value is the real square root.