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.

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. Besides documenting the quarter-subnormal offset used by nearest-even, the equalities 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.nearestEven => { 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.towardPositiveInfinity => if roundsAwayFromZero mode 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.towardNegativeInfinity => if roundsAwayFromZero mode 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 nearest-even uses 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.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.nearestEven => scaledRatToReal numerator denominator exponent < (underflowMidpoint fmt).toReal | IEEERoundingMode.towardZero => scaledRatToReal numerator denominator exponent < (minNormalDyadic fmt).toReal | IEEERoundingMode.towardPositiveInfinity => if roundsAwayFromZero mode sign = true then scaledRatToReal numerator denominator exponent ≤ (underflowPredecessor fmt).toReal else scaledRatToReal numerator denominator exponent < (minNormalDyadic fmt).toReal | IEEERoundingMode.towardNegativeInfinity => if roundsAwayFromZero mode 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 exactly 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.

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.

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

After-rounding rational underflow implies inexactness.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatus_overflow {fmt : FloatFormat} (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (rounded : Model fmt) : (rationalRoundingStatus fmt mode sign numerator denominator rounded).overflow = (rationalRoundingOverflows fmt mode sign numerator denominator || !rounded.isFinite && rounded.isInf)

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.rationalRoundingStatus_overflow_of_isFinite {fmt : FloatFormat} (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (rounded : Model fmt) (hfinite : rounded.isFinite = true) : (rationalRoundingStatus fmt mode sign numerator denominator rounded).overflow = rationalRoundingOverflows fmt mode sign numerator denominator

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

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

Rational overflow always raises inexact.

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

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addWithStatus_value {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.addWithStatus y mode).value = addWithRounding mode x y

Status-bearing addition returns the same value as value-only directed addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.subWithStatus_value {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.subWithStatus y mode).value = subWithRounding mode x y

Status-bearing subtraction returns the same value as value-only directed subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulWithStatus_value {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.mulWithStatus y mode).value = mulWithRounding mode x y

Status-bearing multiplication returns the same value as value-only directed multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.divWithStatus_value {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.divWithStatus y mode).value = divWithRounding mode x y

Status-bearing division returns the same value as value-only directed division.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fmaWithStatus_value {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode) : (x.fmaWithStatus y z mode).value = fmaWithRounding mode x y z

Status-bearing FMA returns the same value as value-only directed FMA.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtWithStatus_value {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode) : (x.sqrtWithStatus mode).value = sqrtWithRounding mode x

Status-bearing square root returns the same value as value-only directed square root.

Operation-specific exceptional status

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addWithStatus_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.addWithStatus y mode = have exact := addDyadic dx dy; have value := addWithRounding mode x y; { value := value, status := dyadicRoundingStatus fmt mode exact value }

Finite addition exposes exactly its dyadic rounding status.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addWithStatus_invalid {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.addWithStatus y mode).status.invalid = match x.toDyadic?, y.toDyadic? with | some dx, some dy => have exact := addDyadic dx dy; have value := addWithRounding mode x y; !dyadicRoundingOverflows fmt mode exact && !value.isFinite && !value.isInf | 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 expose the rounded result's classification directly. Exceptional operands raise invalid exactly for a signaling NaN or opposite-signed infinities when no NaN was supplied.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulWithStatus_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.mulWithStatus y mode = have exact := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; have value := mulWithRounding mode x y; { value := value, status := dyadicRoundingStatus fmt mode exact value }

Finite multiplication exposes exactly its dyadic rounding status.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulWithStatus_invalid {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.mulWithStatus y mode).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 := mulWithRounding mode x y; !dyadicRoundingOverflows fmt mode exact && !value.isFinite && !value.isInf | 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 expose the rounded result's classification directly. 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.fmaWithStatus_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.fmaWithStatus y z mode = have product := { negative := dx.negative ^^ dy.negative, significand := dx.significand * dy.significand, exponent := dx.exponent + dy.exponent }; have exact := addDyadic product dz; have value := fmaWithRounding mode x y z; { value := value, status := dyadicRoundingStatus fmt mode exact value }

Finite FMA exposes exactly its dyadic rounding status.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fmaWithStatus_invalid {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode) : (x.fmaWithStatus y z mode).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 := fmaWithRounding mode x y z; !dyadicRoundingOverflows fmt mode exact && !value.isFinite && !value.isInf | 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 expose the singly rounded result's classification directly. 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; an input NaN suppresses the opposite-infinity condition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.divWithStatus_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.divWithStatus y mode = have sign := dx.negative ^^ dy.negative; have exponentDifference := dx.exponent - dy.exponent; have value := roundRatWithRoundingScaled fmt mode sign dx.significand dy.significand exponentDifference; { value := value, status := rationalRoundingStatusScaled fmt mode sign dx.significand dy.significand exponentDifference value }

Finite nonzero division exposes exactly its scaled-rational rounding status.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.divWithStatus_invalid {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.divWithStatus y mode).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 := roundRatWithRoundingScaled 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.divWithStatus_divideByZero {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : (x.divWithStatus y mode).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.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtWithStatus_invalid {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode) : (x.sqrtWithStatus mode).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.divWithStatus_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.divWithStatus y mode).status.invalid = true

Dividing two finite zeros raises invalid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.divWithStatus_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.divWithStatus y mode).status.divideByZero = true

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

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

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