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. Like the arithmetic operations, each has one name with options: roundToIntegral x (mode := .up), scale x n (mode := .down) (status := true), remainder x y (status := true). Integral rounding and scaling take a rounding direction. The rounded binary exponent always rounds to nearest-even, and remainder, nextUp, nextDown, minimumNumber, and maximumNumber are exact, so they take only status. With status := true, nextUp and its three siblings report the invalid signal that a signaling NaN operand owes.

Each public operation is a small @[macro_inline] selector that tests status before computing anything. The kernels it selects live in Model.Internal.Status and Model.Internal.Value. Integral rounding, scaling, and the rounded binary exponent carry @[specialize fmt]: a module that calls them with a closed format compiles a copy specialized to that descriptor term (calls that spell the same descriptor alike share it), and other callers run the compiled generic body. Their value kernels inline the status body and compute no flags or ternary value.

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

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

The result is an unbounded Int, and converting it back to a floating-point format is a separate step. Large negative exponents are handled by right shifts, so this operation does not construct a power of two merely to discard fractional bits. Nearest-away rounding and rounding away from zero apply Numerics.roundShiftRight to the magnitude. They select the integers of IEEE 754-2019 roundToIntegralTiesToAway and of MPFR's mpfr_rint under MPFR_RNDA.

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. Direct division and logarithmic modular reduction both call it, so they 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.Internal.Status.remainder {fmt : FloatFormat} (dividend divisor : Model fmt) : IEEEOutcome fmt

IEEE remainder with exception status, the kernel of Model.remainder dividend divisor (status := true).

For finite IEEE operands with a nonzero divisor, the remainder is exactly representable (remainder_exact), and this branch returns clear status and the ternary value .eq. 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. Every branch has the ternary value .eq.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.remainder {fmt : FloatFormat} (dividend divisor : Model fmt) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE 754-2019 §5.3.1 remainder: dividend - n * divisor for the integer n nearest to the exact quotient, ties to even. The result is exact, so there is no rounding option. With status := true the result is the IEEEOutcome carrying the invalid flag of a zero divisor, an infinite dividend, or a signaling NaN.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.roundToIntegral {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) : IEEEOutcome fmt

IEEE 754-2019 §5.9 roundToIntegralExact in rounding direction mode, the kernel of Model.roundToIntegral value (mode := mode) (status := true).

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, and 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 roundToIntegral_overflow_eq_false shows that no overflow is possible there, so on an IEEE descriptor with that range the overflow test is skipped. The range test is stated over natural numbers, fmt.fracWidth + fmt.exponentBias ≤ fmt.maxFiniteExpField, so a closed format folds it at compile time. roundToIntegral_status_of_finite states the finite outcome with the encoder's overflow classification. A custom descriptor uses its declared overflow behavior, so an overflow result need not be integral.

The ternary value compares the delivered value with the input, as MPFR's mpfr_rint does. It is therefore not determined by inexact: a saturating descriptor can deliver its own fractional input, with inexact raised and the ternary value .eq.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.scale {fmt : FloatFormat} (value : Model fmt) (n : ℤ) (mode : IEEERoundingMode) : IEEEOutcome fmt

Multiply a value by 2^n, round once, and report exception flags (IEEE 754 scaleB), the kernel of Model.scale value n (mode := mode) (status := true).

Scaling changes the exact dyadic exponent without constructing 2^n, and the shared rounder then applies the destination format and rounding direction. The ternary value compares the delivered value with the exact scaled dyadic.

@[specialize #[0]]

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

The value of Status.roundToIntegral, the kernel of Model.roundToIntegral value (mode := mode). The status body is inlined here, so the compiled kernel computes neither flags nor the ternary value.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.scale {fmt : FloatFormat} (value : Model fmt) (n : ℤ) (mode : IEEERoundingMode) : Model fmt

The value of Status.scale, the kernel of Model.scale value n (mode := mode), with the status body inlined as in Internal.Value.roundToIntegral.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE 754-2019 §5.9 integral rounding in mode (nearest-even by default).

The value is roundToIntegral: the input rounded to an integer and encoded in the same direction. With status := true the result is the IEEEOutcome of roundToIntegralExact: a signaling NaN raises invalid and a fractional finite input raises inexact, and the ternary value compares the delivered value with the input.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.scale {fmt : FloatFormat} (value : Model fmt) (n : ℤ) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

Multiply by 2^n and round once in mode (nearest-even by default), IEEE 754 scaleB. With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.IntegerExponentOutcome : Type

Integer result and default exception indicators for IEEE logB.

• value : ℤ

  Exact leading exponent, or a format-dependent exceptional sentinel.

• status : Numerics.IEEEStatus

  Exceptional integer results signal invalid, and finite nonzero inputs raise no flags.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqIntegerExponentOutcome : DecidableEq IntegerExponentOutcome

def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqIntegerExponentOutcome.decEq (x✝ x✝¹ : IntegerExponentOutcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIntegerExponentOutcome : Repr IntegerExponentOutcome

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIntegerExponentOutcome.repr : IntegerExponentOutcome → ℕ → Std.Format

def FloatLib.Floats.Formats.BinaryInterchange.Model.logBBound (fmt : FloatFormat) : ℤ

The IEEE integer logB exceptional-result bound emax + p - 1.

def FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponentSentinel (fmt : FloatFormat) : ℤ

Exceptional integer outside the finite exponent range and the IEEE logB bound.

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

Exact IEEE 754-2019 §5.3.3 logB with an unbounded integer result format.

For nonzero finite ±m * 2^e, return floor(log₂ m) + e with clear status. Zero returns the negative exceptional sentinel, and infinity and either kind of NaN return the positive one. All exceptional integer results signal invalid, as required for an integer logBFormat. No rounding of the exponent occurs, including for low-precision source descriptors.

@[specialize #[0]]

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

Return the leading binary exponent rounded into the same format, with exception flags, the kernel of Model.binaryExponent value (status := true).

This convenience operation uses nearest-even. It agrees with floating-result IEEE logB only when the source format can represent the exponent exactly, and binaryExponentInt provides the exact integer-result operation for every descriptor.

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.

The ternary value compares the delivered value with the exact exponent, so a low-precision format that rounds the exponent reports the direction: in ieee 5 1 the exponent 13 of 2^13 is delivered as 12 with .lt. The exact infinities of zero and infinite inputs use exactInfinityTernary, which is .eq for IEEE encodings and records the saturated or NaN replacement elsewhere.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.binaryExponent {fmt : FloatFormat} (value : Model fmt) : Model fmt

The value of Status.binaryExponent, the kernel of Model.binaryExponent value, with the status body inlined as in Internal.Value.roundToIntegral.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.binaryExponent {fmt : FloatFormat} (value : Model fmt) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

Leading binary exponent rounded into the source format, always to nearest-even. binaryExponentInt is the exact integer version. With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value.

Status of the quiet operations

nextUp, nextDown, minimumNumber, and maximumNumber compute exact results without a status. IEEE 754-2019 §5.3.1 and §9.6 still require a signaling NaN operand to raise invalid, so with status := true each operation adds that indicator and changes nothing else. Their results are exact, so the ternary value is .eq.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.nextUp {fmt : FloatFormat} (x : Model fmt) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

The next representable value strictly greater than x, IEEE 754-2019 §5.3.1 nextUp. With status := true the result is the IEEEOutcome with invalid set exactly for a signaling NaN.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.nextDown {fmt : FloatFormat} (x : Model fmt) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

The next representable value strictly less than x, IEEE 754-2019 §5.3.1 nextDown. With status := true the result is the IEEEOutcome with invalid set exactly for a signaling NaN.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.minimumNumber {fmt : FloatFormat} (x y : Model fmt) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE 754-2019 §9.6 minimumNumber. With status := true the result is the IEEEOutcome: a signaling NaN raises invalid, including when the other operand is a number and supplies the result.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.maximumNumber {fmt : FloatFormat} (x y : Model fmt) (status : Bool := false) : match status with | true => IEEEOutcome fmt | false => Model fmt

IEEE 754-2019 §9.6 maximumNumber. With status := true the result is the IEEEOutcome: a signaling NaN raises invalid, including when the other operand is a number and supplies the result.