Standard operations beyond basic arithmetic

Remainder, integral rounding, and exponent operations use exact dyadics and the same rounding modes, format policies, and exception status as the arithmetic primitives. Status wrappers also report signaling NaNs for adjacent-value and number-preferring minimum/maximum operations.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt (mode : IEEERoundingMode) (value : Numerics.Dyadic) : ℤ

Round an exact dyadic to an integer in the selected IEEE direction.

The result is an unbounded Int; conversion back to a floating-point format is a separate, explicit boundary. Large negative exponents are handled by right shifts, so this operation does not construct a power of two merely to discard fractional bits.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral (value : Numerics.Dyadic) : Bool

Whether an exact dyadic already denotes an integer.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Operations.Internal.remainderFromDivision (dividendNegative quotientOdd : Bool) (remainder denominator : ℕ) (exponent : ℤ) : Numerics.Dyadic

Construct an exact dyadic remainder from the division facts needed by nearest-even rounding.

The caller supplies the truncated quotient's parity and the ordinary nonnegative remainder. Keeping this decision in one helper makes direct division and logarithmic modular reduction share the same sign, tie, and signed-zero behavior.

def FloatLib.Floats.Formats.BinaryInterchange.Model.remainderDyadic (dividend divisor : Numerics.Dyadic) (_hdivisor : divisor.significand ≠ 0) : Numerics.Dyadic

Exact IEEE remainder of two finite dyadics with a nonzero divisor.

The selected integer quotient is nearest to dividend / divisor, with ties to even. When the dividend has the larger binary exponent, its shifted significand is reduced modulo twice the divisor by logarithmic modular exponentiation. This avoids constructing a natural number whose size is proportional to an arbitrary exponent gap.

def FloatLib.Floats.Formats.BinaryInterchange.Model.remainderWithStatus {fmt : FloatFormat} (dividend divisor : Model fmt) : IEEEOutcome fmt

IEEE remainder with explicit exception status.

For finite IEEE operands with a nonzero divisor, the remainder is exactly representable (remainderWithStatus_exact), and this branch returns clear status. NaNs propagate with signaling operands first, then the left operand. Otherwise, a zero divisor or infinite dividend raises invalid, while a finite dividend modulo infinity is unchanged.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.remainder {fmt : FloatFormat} (dividend divisor : Model fmt) : Model fmt

Value projection of remainderWithStatus.

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

IEEE 754-2019 §5.9 roundToIntegralExact under an explicit rounding direction.

The exact dyadic is rounded to an integer, then encoded in the same direction. Zero preserves the input sign when the format supports signed zero. A signaling NaN raises invalid; a fractional finite input raises inexact.

overflow is raised only for descriptors whose finite range ends below the rounded integer; every IEEE interchange format satisfies fmt.fracWidth ≤ fmt.maxNormalExponent, and roundToIntegralExactWithStatus_overflow_eq_false shows that no overflow is possible there. A custom descriptor uses its declared overflow behavior, so an overflow result need not be integral.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : Model fmt

Integral rounding selected by mode, returning only the value.

This projects the value of roundToIntegralExactWithStatus and discards all status flags. Use that operation when the caller needs signaling-NaN or fractional-input status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.scaleBWithStatus {fmt : FloatFormat} (value : Model fmt) (scale : ℤ) (mode : IEEERoundingMode := IEEERoundingMode.nearestEven) : IEEEOutcome fmt

Multiply a value by 2^scale and round once in the selected direction.

Scaling changes the exact dyadic exponent without constructing 2^scale; the shared rounder then applies the destination format and rounding direction.

@[inline]

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

Value projection of scaleBWithStatus.

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

Round the exponent of the value's leading binary digit into the same format, using nearest-even.

For a nonzero finite dyadic ±m * 2^e with m > 0, the exact result is floor(log₂ m) + e. Either infinity returns nativeOverflow fmt false, the format's positive overflow value. NaNs are quiet-propagated, with invalid raised only for a signaling NaN.

Zero returns nativeOverflow fmt true and raises divideByZero, following IEEE 754-2019 §5.3.3. What that value is depends on the encoding:

• IEEE encodings deliver negative infinity, as the standard specifies.
• finiteMaxNaN and finiteUnsignedZero (FNUZ) return their NaN word with the same divideByZero flag for the zero input.
• finite (signed zero, no NaN) saturates to the most negative finite value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.logB {fmt : FloatFormat} (value : Model fmt) : Model fmt

Value projection of logBWithStatus.

Status-bearing forms of the quiet operations

nextUp, nextDown, minimumNumber, and maximumNumber are value-only in Model. IEEE 754-2019 §5.3.1 and §9.6 still require a signaling NaN operand to raise invalid; the wrappers below add exactly that indicator and change nothing else.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.nextUpWithStatus {fmt : FloatFormat} (x : Model fmt) : IEEEOutcome fmt

nextUp with invalid set exactly for a signaling NaN input.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.nextDownWithStatus {fmt : FloatFormat} (x : Model fmt) : IEEEOutcome fmt

nextDown with invalid set exactly for a signaling NaN input.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumberWithStatus {fmt : FloatFormat} (x y : Model fmt) : IEEEOutcome fmt

IEEE 754-2019 §9.6 minimumNumber with status. A signaling NaN raises invalid, including when the other operand is a number and supplies the result.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumberWithStatus {fmt : FloatFormat} (x y : Model fmt) : IEEEOutcome fmt

IEEE 754-2019 §9.6 maximumNumber with status. A signaling NaN raises invalid, including when the other operand is a number and supplies the result.