Mixed-precision multiply-accumulate

SitePolicy assigns a format to each of four roles: input storage, multiplication, the running accumulator, and final output. For example, inputs and products can use bf16 while accumulation and output use binary32. The product is rounded before it reaches the accumulator.

mulAcc performs one unfused step:

storage inputs → cast each to product → multiply in product
                                     → cast to accumulator → add to accumulator

Each step has five possible rounding errors: two input casts, multiplication, the product cast, and addition. Finite casts between identical formats are exact. The result stays in the accumulator format; the output format is used only when a reduction finishes.

dotSequential starts at positive zero, applies mulAcc from left to right, then casts once to the output format. Different reduction orders can produce different bits. Unequal input lengths return an error; empty inputs return positive zero cast to the output format.

Matmul applies the same dot kernel to rows and columns. Proof and MatmulProof give error bounds for IEEE encodings when the inputs, intermediate values, and results are finite.

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

Formats used by input storage, an unfused multiply-accumulate step, and the final output cast.

• storage : FloatFormat

  Format of input operands.

• product : FloatFormat

  Format in which the product is formed.

• accumulator : FloatFormat

  Format holding the running sum.

• output : FloatFormat

  Format of the final write after a reduction (dotSequential ends with a cast here).

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqSitePolicy : DecidableEq SitePolicy

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

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprSitePolicy : Repr SitePolicy

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprSitePolicy.repr : SitePolicy → ℕ → Std.Format

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SitePolicy.uniform (fmt : FloatFormat) : SitePolicy

Every role uses the same format (classic single-dtype path).

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.SitePolicy.mixedStoreProductAcc (storeProd accOut : FloatFormat) : SitePolicy

Store and multiply in storeProd, then accumulate and write the reduction result in accOut.

@[inline]

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

One unfused mixed-precision step: acc ← cast(mul(cast a, cast b)) + acc.

• Inputs a, b are in p.storage.
• Product is computed in p.product (after casting inputs into that format).
• Product is cast into p.accumulator and added to acc.
• Returns the new accumulator value (still p.accumulator).

To produce an output value, apply cast p.accumulator p.output to the result.

def FloatLib.Floats.Formats.BinaryInterchange.Model.dotSequential (p : SitePolicy) (xs ys : Array (Model p.storage)) : Except Numerics.ReductionError (Model p.output)

Sequential mixed-precision dot product under site policy p.

Each product-add uses mulAcc (storage → product → accumulator), and the completed accumulator is cast once into p.output. The reduction visits indices from left to right; rounded addition is not associative, so another parenthesization can change the result.

The inputs must have equal lengths. A mismatch returns ReductionError.lengthMismatch; empty inputs return +0 cast from the accumulator format into p.output.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.dotSequentialUniform (fmt : FloatFormat) (xs ys : Array (Model fmt)) : Except Numerics.ReductionError (Model fmt)

Sequential dot product with a single format in every arithmetic role.