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 explicit 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. Empty reductions return positive zero. A sum of zeros with the same sign keeps that sign; cancellation and mixed-sign zeros are negative only under rounding toward negative infinity. FNUZ destinations use positive zero.

There is deliberately 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 an explicit 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; 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.

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

Correctly rounded sum of an array.

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

@[inline]

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

Value-only projection of sumWithStatus.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sumListWithStatus (destination : FloatFormat) {source : FloatFormat} (values : List (Model source)) (mode : IEEERoundingMode) : IEEEOutcome destination

List entry point for correctly rounded summation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sumList (destination : FloatFormat) {source : FloatFormat} (values : List (Model source)) (mode : IEEERoundingMode) : Model destination

Value-only list entry point for correctly rounded summation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dotWithStatus (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.

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.dot (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) : Except Numerics.ReductionError (Model destination)

Value-only projection of dotWithStatus.

@[inline]

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

List entry point for a correctly rounded dot product.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.dotList (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : List (Model leftFormat)) (right : List (Model rightFormat)) (mode : IEEERoundingMode) : Except Numerics.ReductionError (Model destination)

Value-only list entry point for a correctly rounded dot product.