Mixed-precision matrix multiplication

Each output entry is a left-to-right dotSequential reduction under one SitePolicy. Products round in the product format, additions round in the accumulator format, and the completed entry is cast to the output format.

Matrices are row-major arrays: M[i][j] is row i, column j. matmul checks that both inputs are rectangular and that the left row width equals the number of right rows. An empty matrix has zero columns because this representation carries no width without a row.

For an m × k matrix times a k × n matrix, the implementation extracts the right-hand columns once and computes m * n sequential dots of length k. MatmulProof proves that every successful output has this shape and these entries, then applies the dot-product error bound entrywise.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.Matrix (fmt : FloatFormat) : Type

Row-major matrix of Models: outer array = rows, inner array = entries in that row.

inductive FloatLib.Floats.Formats.BinaryInterchange.Model.MatrixShapeError : Type

Shape failures rejected before matrix multiplication begins.

• raggedLeft (expectedColumns : ℕ) : MatrixShapeError

  Rows of the left input do not all have the first row's width.

• raggedRight (expectedColumns : ℕ) : MatrixShapeError

  Rows of the right input do not all have the first row's width.

• innerDimensionMismatch (leftColumns rightRows : ℕ) : MatrixShapeError

  The left row width differs from the number of right rows.

• dotLengthMismatch (rowLength columnLength : ℕ) : MatrixShapeError

  A checked row and column nevertheless reached the dot kernel with different lengths.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprMatrixShapeError : Repr MatrixShapeError

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprMatrixShapeError.repr : MatrixShapeError → ℕ → Std.Format

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

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqMatrixShapeError : DecidableEq MatrixShapeError

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ncols {fmt : FloatFormat} (M : Matrix fmt) : ℕ

Column count from the first row; 0 if there are no rows.

def FloatLib.Floats.Formats.BinaryInterchange.Model.column {fmt : FloatFormat} (M : Matrix fmt) (j : ℕ) : Array (Model fmt)

Extract column j as a length-M.size vector (one entry per row).

Precondition (unchecked): every row has length > j.

def FloatLib.Floats.Formats.BinaryInterchange.Model.matmul (p : SitePolicy) (A B : Matrix p.storage) : Except MatrixShapeError (Matrix p.output)

Mixed-precision matmul under site policy p:

C[i][j] = dotSequential p (row i of A) (column j of B)

• A, B entries are in p.storage.
• Each inner product uses p.product / p.accumulator as in dotSequential.
• Entries of C are in p.output.

On success, C has A.size rows and ncols B columns. Both inputs must be rectangular and the left row width must equal B.size; otherwise the corresponding MatrixShapeError is returned.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.matmulUniform (fmt : FloatFormat) (A B : Matrix fmt) : Except MatrixShapeError (Matrix fmt)

Matmul with one format in every site role.