Division-free arithmetic programs over a field and their operation counts.

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.mapRegister {F : Type u_1} {Input : Type u_2} {R : Type u_3} {S : Type u_4} (f : R → S) : Gate F Input R → Gate F Input S

Relabel a gate's register references without changing its input wires.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval_mapRegister {F : Type u_1} [Field F] {Input : Type u_2} {R : Type u_3} {S : Type u_4} (g : Gate F Input R) (f : R → S) (inputs : Input → F) (registers : S → F) : eval inputs registers (mapRegister f g) = eval inputs (fun (i : R) => registers (f i)) g

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.cost_mapRegister {F : Type u_1} {Input : Type u_2} {R : Type u_3} {S : Type u_4} (g : Gate F Input R) (f : R → S) : (mapRegister f g).cost = g.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.oldIndex (r s : ℕ) (i : Fin r) : Fin (r + s)

Locate an earlier program's registers after appending a second program.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.oldIndex r s i = ⟨s + ↑i, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.newIndex (r s : ℕ) (i : Fin s) : Fin (r + s)

Locate the appended program's registers in the combined register space.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.newIndex r s i = ⟨↑i, ⋯⟩

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.oldIndex_zero (r : ℕ) (i : Fin r) : oldIndex r 0 i = i

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.oldIndex_succ (r s : ℕ) (i : Fin r) : oldIndex r (s + 1) i = (oldIndex r s i).succ

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.newIndex_zero (r s : ℕ) : newIndex r (s + 1) 0 = 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.newIndex_succ (r s : ℕ) (i : Fin s) : newIndex r (s + 1) i.succ = (newIndex r s i).succ

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.append {F : Type u_1} {Input : Type u_2} {r : ℕ} (p : Program F Input r) {s : ℕ} : Program F Input s → Program F Input (r + s)

Concatenate independent programs, relabelling the second program's register references.

Equations

• One or more equations did not get rendered due to their size.
• p.append MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.nil = p

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_append_new {F : Type u_1} [Field F] {Input : Type u_2} {r s : ℕ} (p : Program F Input r) (q : Program F Input s) (inputs : Input → F) (i : Fin s) : (p.append q).eval inputs (newIndex r s i) = q.eval inputs i

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_append_old {F : Type u_1} [Field F] {Input : Type u_2} {r s : ℕ} (p : Program F Input r) (q : Program F Input s) (inputs : Input → F) (i : Fin r) : (p.append q).eval inputs (oldIndex r s i) = p.eval inputs i

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.cost_append {F : Type u_1} {Input : Type u_2} {r s : ℕ} (p : Program F Input r) (q : Program F Input s) : (p.append q).cost = p.cost + q.cost

inductive MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression (F : Type u_2) (Input : Type u_3) : Type (max u_2 u_3)

Division-free arithmetic expressions built from inputs, scalars, addition, subtraction and multiplication.

• literal {F : Type u_2} {Input : Type u_3} : F → Expression F Input
• input {F : Type u_2} {Input : Type u_3} : Input → Expression F Input
• add {F : Type u_2} {Input : Type u_3} : Expression F Input → Expression F Input → Expression F Input
• sub {F : Type u_2} {Input : Type u_3} : Expression F Input → Expression F Input → Expression F Input
• mul {F : Type u_2} {Input : Type u_3} : Expression F Input → Expression F Input → Expression F Input

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.eval {F : Type u_1} [Field F] {Input : Type u_2} (inputs : Input → F) : Expression F Input → F

Interpret an arithmetic expression at the supplied input values.

Equations

• One or more equations did not get rendered due to their size.
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.eval inputs (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.literal z) = z
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.eval inputs (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.input i) = inputs i

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.cost {F : Type u_1} {Input : Type u_2} : Expression F Input → ℕ

Count arithmetic operations, treating input and literal loading as free.

Equations

• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.literal z).cost = 0
• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.input i).cost = 0
• (e.add f).cost = e.cost + f.cost + 1
• (e.sub f).cost = e.cost + f.cost + 1
• (e.mul f).cost = e.cost + f.cost + 1

structure MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.Compiled {F : Type u_1} [Field F] {Input : Type u_2} (e : Expression F Input) : Type (max u_1 u_2)

A compiled expression with certified semantics and exact operation count.

• registers : ℕ

  Number of registers allocated for the compiled expression.

• program : Program F Input self.registers

  The straight-line program computing the expression.

• output : Fin self.registers

  Register containing the expression's value.

• correct (inputs : Input → F) : self.program.eval inputs self.output = eval inputs e
• cost_eq : self.program.cost = e.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Expression.compile {F : Type u_1} [Field F] {Input : Type u_2} (e : Expression F Input) : e.Compiled

Compile an expression while certifying its evaluation and operation count.

Equations

• One or more equations did not get rendered due to their size.