Correctly rounded binary reductions

sum decodes every operand exactly, adds in the shared dyadic domain, and rounds once into the requested destination format. dot does the same with exact products. Source and destination formats may differ, so the operations cover ordinary uniform reductions and mixed-precision accumulation with one API.

Exceptional inputs are deterministic:

• the first signaling NaN in traversal order is selected and quieted, ahead of every quiet NaN;
• otherwise the first quiet NaN is selected;
• opposite-signed infinities and 0 * ∞ raise invalid, even when a quiet NaN supplies the result;
• one infinity sign is preserved; and
• finite inputs are accumulated exactly and rounded once.

NaN payloads are preserved when source and destination formats agree. Cross-format NaNs follow the ordinary Model.cast policy. An infinite result follows the destination's native overflow rule, matching casts: IEEE encodings preserve infinity, finite-with-NaN encodings return NaN, and fully finite encodings return the same-sign maximum. A destination without infinity raises overflow and inexact, and the ternary value is .lt for +∞ and .gt for -∞. Empty reductions return positive zero. A sum of zeros with the same sign keeps that sign, and cancellation and mixed-sign zeros are negative only under rounding toward negative infinity. FNUZ destinations use positive zero.

There is no initial-addend argument. One product plus an addend is already IEEE FMA, and larger finite algebraic expressions can use ExecFloat.roundOnce. A repeated FMA chain is a different operation because it rounds every prefix. It agrees with dot only when those intermediate roundings are exact and the exceptional and signed-zero rules also agree.

The binary reducer and a posit quire share the useful idea “exact products, then one final round,” but not the same machine model. This reducer uses an unbounded software dyadic accumulator and IEEE NaN, infinity, signed-zero, and status semantics. A posit quire is a fixed 16n-bit accumulator with NaR and a coefficient-range condition.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State (destination : FloatFormat) : Type

Accumulator state used by the transparent reduction kernels.

The state records exact finite contributions separately from exceptional inputs, so NaN priority and infinity cancellation can be resolved after traversal.

• exact : Numerics.Dyadic

  Exact finite contribution accumulated so far.

• sawFiniteTerm : Bool

  Whether the reduction has consumed at least one finite term.

• allTermsNegativeZero : Bool

  Whether every consumed finite term was a negative zero.

• allTermsPositiveZero : Bool

  Whether every consumed finite term was a positive zero.

• positiveInfinity : Bool

  Whether a positive infinity has occurred.

• negativeInfinity : Bool

  Whether a negative infinity has occurred.

• signalingNaN : Option (Model destination)

  First signaling NaN in traversal order, quieted into the destination format.

• quietNaN : Option (Model destination)

  First quiet NaN in traversal order, converted into the destination format.

• generatedInvalid : Bool

  Whether a product generated an invalid operation such as 0 * ∞.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.captureNaN {destination source : FloatFormat} (state : State destination) (value : Model source) : State destination

Record the first NaN of each class while preserving signaling-NaN priority.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushExact {destination : FloatFormat} (state : State destination) (value : Numerics.Dyadic) : State destination

Add one exact finite term to the shared dyadic accumulator.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushInfinity {destination : FloatFormat} (state : State destination) (negative : Bool) : State destination

Record an infinity sign without discarding a possible opposing infinity.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushValue {destination source : FloatFormat} (state : State destination) (value : Model source) : State destination

Consume one summand according to the reduction's exceptional-value policy.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushProduct {destination leftFormat rightFormat : FloatFormat} (state : State destination) (left : Model leftFormat) (right : Model rightFormat) : State destination

Consume one exact product while detecting NaNs, infinities, and 0 * ∞.

@[irreducible]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotStateLoop {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (state : State destination) (index remaining : ℕ) (hleft : index + remaining ≤ left.size) (hright : index + remaining ≤ right.size) : State destination

Accumulate a contiguous dot-product slice without allocating a zipped collection.

index is the first pair to consume and remaining is the number of pairs. The size proofs are erased after compilation, and they make every array access bounds-safe without a default value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotState {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (hsize : left.size = right.size) : State destination

Accumulate every pair in two equal-sized arrays in left-to-right traversal order.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.finish {destination : FloatFormat} (state : State destination) (mode : IEEERoundingMode) : IEEEOutcome destination

Resolve exceptional values or round the exact finite result once.

The ternary value compares a rounded finite result with the exact sum. An exact zero sum, a NaN, and an invalid result have .eq. An infinite result uses exactInfinityTernary, which is .eq when the destination keeps the infinity.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.finishValue {destination : FloatFormat} (state : State destination) (mode : IEEERoundingMode) : Model destination

The value of State.finish.

The finisher is inlined here, so the compiled value-only reductions compute neither flags nor the ternary value of the final rounding.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.sum (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode) : IEEEOutcome destination

Correctly rounded sum of an array with its IEEE status, the kernel of Model.sum destination values (mode := mode) (status := true).

Every finite source value is decoded exactly, the exact dyadic sum is formed without intermediate rounding, and the result is rounded once into destination.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.sum (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode) : Model destination

Correctly rounded sum of an array, the kernel of Model.sum destination values (mode := mode).

The accumulation is that of Status.sum, and the final rounding goes through State.finishValue, so no flags or ternary value are computed.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.dot (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) : Except Numerics.ReductionError (IEEEOutcome destination)

Correctly rounded dot product of two arrays with its IEEE status, the kernel of Model.dot destination left right (mode := mode) (status := true).

Each finite pair is multiplied in the exact dyadic domain, all products are added exactly, and the result is rounded once into destination. Unequal lengths are rejected before any arithmetic occurs.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Value.dot (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) : Except Numerics.ReductionError (Model destination)

Correctly rounded dot product of two arrays, the kernel of Model.dot destination left right (mode := mode).

The length check and the accumulation are those of Status.dot, and the final rounding goes through State.finishValue, so no flags or ternary value are computed.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sum (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome destination | false => Model destination

Correctly rounded sum of an array in mode (nearest-even by default).

Every finite source value is decoded exactly, the exact dyadic sum is formed without intermediate rounding, and the result is rounded once into destination. With status := true the result is the IEEEOutcome carrying the exception flags and the ternary value of that one rounding. Reduction.value_sum states that its value is the sum, so every theorem about the status form describes the value.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sumList (destination : FloatFormat) {source : FloatFormat} (values : List (Model source)) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome destination | false => Model destination

List entry point for correctly rounded summation, with the options of sum.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.dot (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : Except Numerics.ReductionError (match status with | true => IEEEOutcome destination | false => Model destination)

Correctly rounded dot product of two arrays in mode (nearest-even by default).

Each finite pair is multiplied in the exact dyadic domain, all products are added exactly, and the result is rounded once into destination. Unequal lengths are rejected before any arithmetic occurs. With status := true the successful result is the IEEEOutcome carrying the exception flags and the ternary value. Reduction.map_value_dot states that its value and its errors are those of the value form.

@[macro_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.dotList (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : List (Model leftFormat)) (right : List (Model rightFormat)) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : Except Numerics.ReductionError (match status with | true => IEEEOutcome destination | false => Model destination)

List entry point for a correctly rounded dot product, with the options of dot.