IEEE exception status for format-parameterized Model

The value operations remain pure and explicit about their rounding mode. This module pairs those values with the five IEEE exception indicators. Tininess is detected after rounding, and underflow is raised exactly when a tiny result is inexact.

Overflow is classified from the precision-rounded result with an unbounded exponent range, as in IEEE 754-2019 §7.4 and the GNU MPFR manual's exception definition: https://doi.org/10.1109/IEEESTD.2019.8766229 and https://www.mpfr.org/mpfr-current/mpfr.html#Exceptions.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.IEEEStatus : Type

The shared IEEE exception indicators, also used by decimal arithmetic.

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEEStatus.clear : IEEEStatus

No exception was raised.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.IEEEOutcome (fmt : FloatFormat) : Type

A format-parameterized executable value paired with its IEEE exception status.

• value : Model fmt

  Delivered floating-point result.

• status : IEEEStatus

  Exception indicators raised while computing value.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIEEEOutcome {fmt✝ : FloatFormat} : Repr (IEEEOutcome fmt✝)

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIEEEOutcome.repr {fmt✝ : FloatFormat} : IEEEOutcome fmt✝ → ℕ → Std.Format

def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqIEEEOutcome.decEq {fmt✝ : FloatFormat} (x✝ x✝¹ : IEEEOutcome fmt✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqIEEEOutcome {fmt✝ : FloatFormat} : DecidableEq (IEEEOutcome fmt✝)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instInhabitedIEEEOutcome {a✝ : FloatFormat} : Inhabited (IEEEOutcome a✝)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.outcomeWithInvalid {fmt : FloatFormat} (value : Model fmt) (invalid : Bool) : IEEEOutcome fmt

Pair a value with either the invalid-operation flag or a clear status.

Exceptional arithmetic paths share this constructor so the value and the Boolean invalid condition remain visible without duplicating conditional record construction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.isTinyAfterRounding {fmt : FloatFormat} (x : Model fmt) : Bool

Whether a finite rounded result is zero or subnormal.

def FloatLib.Floats.Formats.BinaryInterchange.Model.minNormalDyadic (fmt : FloatFormat) : Numerics.Dyadic

Exact positive value of the smallest normal number in fmt.

def FloatLib.Floats.Formats.BinaryInterchange.Model.underflowPredecessor (fmt : FloatFormat) : Numerics.Dyadic

Largest positive number below minNormalDyadic fmt on the format's precision grid with an unbounded exponent range. Its distance from the smallest normal is half one subnormal step.

def FloatLib.Floats.Formats.BinaryInterchange.Model.underflowMidpoint (fmt : FloatFormat) : Numerics.Dyadic

Positive boundary used by after-rounding tininess detection.

Tininess after rounding is determined by first rounding to the destination precision with an unbounded exponent range. Immediately below the smallest normal value that unbounded grid has half the subnormal spacing, so its midpoint is one quarter of a subnormal step below minNormal. The midpoint itself rounds to the even minNormal significand and is not tiny.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundsAwayFromZero (mode : IEEERoundingMode) (negative : Bool) : Bool

Whether a directed mode rounds a result with this sign away from zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsTinyAfterRounding (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : Bool

Whether a dyadic result is tiny after rounding to the destination precision with an unbounded exponent range.

Most tiny results are visible directly as zero or subnormal encodings. A result delivered as minNormal needs a mode-sensitive boundary:

• nearest-even uses the midpoint between minNormal and its unbounded-grid predecessor;
• rounding away from zero is tiny through that predecessor;
• rounding toward zero is tiny for every magnitude strictly below minNormal.

def FloatLib.Floats.Formats.BinaryInterchange.Model.maxFiniteDyadic (fmt : FloatFormat) : Numerics.Dyadic

Exact positive dyadic value of the largest finite number in fmt.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicMagnitudeOverflows (fmt : FloatFormat) (exact : Numerics.Dyadic) : Bool

Whether an exact dyadic magnitude exceeds the finite range of fmt.

def FloatLib.Floats.Formats.BinaryInterchange.Model.overflowMidpoint (fmt : FloatFormat) : Numerics.Dyadic

Positive midpoint between the largest finite value and the next magnitude on the same binary grid.

Nearest-even overflow is decided at this boundary. The midpoint itself overflows exactly when the largest finite significand is odd, because the conceptual next significand is then even.

def FloatLib.Floats.Formats.BinaryInterchange.Model.overflowLimit (fmt : FloatFormat) : Numerics.Dyadic

First grid magnitude beyond the largest finite value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.maxFiniteMantissaOdd (fmt : FloatFormat) : Bool

Whether the largest finite significand is odd.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicNearestEvenOverflows (fmt : FloatFormat) (exact : Numerics.Dyadic) : Bool

Whether nearest-even rounding of an exact dyadic magnitude signals overflow.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicTruncationOverflows (fmt : FloatFormat) (exact : Numerics.Dyadic) : Bool

Whether truncating an exact dyadic magnitude still exceeds the finite range.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingOverflows (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) : Bool

Whether rounding an exact dyadic signals overflow.

Nearest-even uses the top finite midpoint. A directed mode that increases the magnitude overflows above maxFinite; a mode that decreases the magnitude overflows only at overflowLimit. For conventional IEEE encodings, that limit starts the next binade. For encodings that reserve a terminal fraction pattern, it can lie within the same binade.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicRoundingStatus (fmt : FloatFormat) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (rounded : Model fmt) : IEEEStatus

Classify rounding an exact dyadic to rounded under mode.

Finite results use the proof-guided exact decoder. An exceptional rounded argument is classified explicitly as overflow or invalid; it is never treated as a clear status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalEqualsDyadicScaled (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (value : Numerics.Dyadic) : Bool

Exact equality between (numerator / denominator) * 2^exponent and a signed dyadic.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalMagnitudeOverflowsScaled (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) : Bool

Whether a positive scaled rational magnitude exceeds the finite range of fmt.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalMagnitudeOverflows (fmt : FloatFormat) (numerator denominator : ℕ) : Bool

Whether a positive rational magnitude exceeds the finite range of fmt.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalNearestEvenOverflowsScaled (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) : Bool

Whether nearest-even rounding of a positive scaled rational signals overflow.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalTruncationOverflowsScaled (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) : Bool

Whether truncating a scaled rational magnitude still exceeds the finite range.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOverflowsScaled (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) : Bool

Whether rounding an exact signed scaled rational signals overflow.

The sign determines whether a directed mode increases or decreases magnitude. Magnitude-increasing rounding overflows above maxFinite; truncating rounding uses overflowLimit.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingOverflows (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) : Bool

Whether rounding an exact rational signals overflow.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalIsTinyAfterRoundingScaled (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) : Bool

Whether a scaled rational result is tiny after rounding to the destination precision with an unbounded exponent range.

As with dyadics, an encoded zero or subnormal is tiny. A result delivered as minNormal uses the nearest midpoint, the unbounded-grid predecessor, or minNormal itself according to the rounding direction and sign.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatusScaled (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (rounded : Model fmt) : IEEEStatus

Classify rounding an exact scaled signed rational to rounded under mode.

For a nonzero denominator, finite results are compared with the exact rational. Exceptional results are classified as overflow or invalid, as in dyadicRoundingStatus. Division handles a zero denominator before calling this classifier.

def FloatLib.Floats.Formats.BinaryInterchange.Model.rationalRoundingStatus (fmt : FloatFormat) (mode : IEEERoundingMode) (sign : Bool) (numerator denominator : ℕ) (rounded : Model fmt) : IEEEStatus

Classify rounding an exact signed rational to rounded under mode.

def FloatLib.Floats.Formats.BinaryInterchange.Model.addWithStatus {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Addition with an explicit rounding direction and IEEE exception status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.subWithStatus {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Subtraction with an explicit rounding direction and IEEE exception status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.mulWithStatus {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Multiplication with an explicit rounding direction and IEEE exception status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.divWithStatus {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Division with an explicit rounding direction and IEEE exception status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.fmaWithStatus {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Fused multiply-add with an explicit rounding direction and IEEE exception status.

IEEE 754-2019 Section 7.2 leaves it implementation defined whether fma(0, ∞, c) signals invalid when c is a quiet NaN. This implementation signals invalid for that case: the invalid product 0 × ∞ is reported whether or not the addend is a quiet NaN, whereas addWithStatus and mulWithStatus only report an operand-generated invalid operation when no operand is a NaN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicSquareRootIsExact (exact : Numerics.Dyadic) : Bool

Whether a nonnegative dyadic has an exact dyadic square root.

When the exponent is odd, one factor of two moves into the significand. The square root is dyadic exactly when the resulting significand is a perfect square.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrtWithStatus {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Square root with an explicit rounding direction and IEEE exception status.