Error bounds for mixed-precision accumulation

Real-error decompositions and absolute bounds for mulAcc and dotSequential. Each step's bound accounts for both input casts, multiplication, the cast to the accumulator, and addition. The dot bound also includes the final output cast. The bounds assume IEEE encodings and finite values throughout; their local half-ULP terms cover subnormals as well as normal values.

def FloatLib.Floats.Formats.BinaryInterchange.Model.MulAccFinite (p : SitePolicy) (a b : Model p.storage) (acc : Model p.accumulator) : Prop

All values encountered by one unfused mixed-precision multiply-accumulate are finite.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.mulAccErrorBudget (p : SitePolicy) (a b : Model p.storage) (acc : Model p.accumulator) : ℝ

Sum of the local half-ULP budgets in one mixed-precision multiply-accumulate.

The input-cast terms include the factors introduced when the rounded operands are multiplied.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.mulAccError (p : SitePolicy) (a b : Model p.storage) (acc : Model p.accumulator) : ℝ

Real error introduced by one mixed-precision multiply-accumulate step.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulAccError_eq_site_residuals (p : SitePolicy) (a b : Model p.storage) (acc : Model p.accumulator) : have aP := cast p.storage p.product a; have bP := cast p.storage p.product b; have product := aP.mul bP; have productA := cast p.product p.accumulator product; mulAccError p a b acc = (aP.toReal - a.toReal) * b.toReal + aP.toReal * (bP.toReal - b.toReal) + (product.toReal - aP.toReal * bP.toReal) + (productA.toReal - product.toReal) + ((productA.add acc).toReal - (productA.toReal + acc.toReal))

The error of one mixed-precision multiply-accumulate is exactly the sum of its five site residuals.

This algebraic identity needs no finiteness hypotheses. To interpret the residuals as rounding errors, use the finiteness premises of mulAcc_abs_error_le_budget: toReal maps exceptional values to zero and does not describe their NaN or infinity behavior.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulAcc_abs_error_le_budget (p : SitePolicy) (a b : Model p.storage) (acc : Model p.accumulator) (hstorage : p.storage.isIEEE = true) (hproduct : p.product.isIEEE = true) (haccumulator : p.accumulator.isIEEE = true) (hfinite : MulAccFinite p a b acc) : |mulAccError p a b acc| ≤ mulAccErrorBudget p a b acc

One finite mixed-precision multiply-accumulate differs from the exact source-value operation by at most the sum of the local cast, multiply, cast, and add budgets.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sequentialAccumulator (p : SitePolicy) (xs ys : Array (Model p.storage)) (count : ℕ) : Model p.accumulator

Accumulator state after the first count sequential product-add sites.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.sequentialDotReal (p : SitePolicy) (xs ys : Array (Model p.storage)) (count : ℕ) : ℝ

Exact real dot product of the first count source-value pairs.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.sequentialErrorBudget (p : SitePolicy) (xs ys : Array (Model p.storage)) (count : ℕ) : ℝ

Sum of the local error budgets along the actual sequential accumulator path.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sequentialAccumulator_error_eq_sum (p : SitePolicy) (xs ys : Array (Model p.storage)) (count : ℕ) (haccumulator : p.accumulator.isIEEE = true) : (sequentialAccumulator p xs ys count).toReal - sequentialDotReal p xs ys count = ∑ i ∈ Finset.range count, mulAccError p xs[i]! ys[i]! (sequentialAccumulator p xs ys i)

The executable accumulator's error is the sum of its local errors, evaluated at the successive accumulator states.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sequentialAccumulator_abs_error_le_budget (p : SitePolicy) (xs ys : Array (Model p.storage)) (count : ℕ) (hstorage : p.storage.isIEEE = true) (hproduct : p.product.isIEEE = true) (haccumulator : p.accumulator.isIEEE = true) (hfinite : ∀ i < count, MulAccFinite p xs[i]! ys[i]! (sequentialAccumulator p xs ys i)) : |(sequentialAccumulator p xs ys count).toReal - sequentialDotReal p xs ys count| ≤ sequentialErrorBudget p xs ys count

The absolute error of a finite sequential accumulator is bounded by the sum of its local budgets. Finiteness is required along the executed prefix states; storage, product, and accumulator may use different IEEE formats.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dotSequential_eq_cast_sequentialAccumulator (p : SitePolicy) (xs ys : Array (Model p.storage)) (hsize : xs.size = ys.size) : dotSequential p xs ys = Except.ok (cast p.accumulator p.output (sequentialAccumulator p xs ys xs.size))

The executable dot loop is the prefix accumulator followed by its one output cast.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dotSequential_abs_error_le_budget (p : SitePolicy) (xs ys : Array (Model p.storage)) (result : Model p.output) (hsize : xs.size = ys.size) (hstorage : p.storage.isIEEE = true) (hproduct : p.product.isIEEE = true) (haccumulator : p.accumulator.isIEEE = true) (houtput : p.output.isIEEE = true) (hfinite : ∀ i < xs.size, MulAccFinite p xs[i]! ys[i]! (sequentialAccumulator p xs ys i)) (haccFinite : (sequentialAccumulator p xs ys xs.size).isFinite = true) (hresultFinite : result.isFinite = true) (hresult : dotSequential p xs ys = Except.ok result) : |result.toReal - sequentialDotReal p xs ys xs.size| ≤ epsilonAt p.output (sequentialAccumulator p xs ys xs.size).toReal + sequentialErrorBudget p xs ys xs.size

A successful finite mixed-precision dot product is bounded by all per-step budgets plus the final accumulator-to-output cast budget, following the reduction order of dotSequential.