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

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.mapInput {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} {Register : Type u_4} (f : Input → Input') : Gate F Input Register → Gate F Input' Register

Relabel a gate's input wires while preserving its register references.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval_mapInput {F : Type u_1} [Field F] {Input : Type u_2} {Input' : Type u_3} {Register : Type u_4} (f : Input → Input') (g : Gate F Input Register) (inputs : Input' → F) (registers : Register → F) : eval inputs registers (mapInput f g) = eval (inputs ∘ f) registers g

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.cost_mapInput {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} {Register : Type u_4} (f : Input → Input') (g : Gate F Input Register) : (mapInput f g).cost = g.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.mapSource {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} {Register : Type u_4} (f : Input → Input' ⊕ F) : Gate F Input Register → Gate F Input' Register

Replace input wires by new input wires or literal scalars.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval_mapSource {F : Type u_1} [Field F] {Input : Type u_2} {Input' : Type u_3} {Register : Type u_4} (f : Input → Input' ⊕ F) (g : Gate F Input Register) (inputs : Input' → F) (registers : Register → F) : eval inputs registers (mapSource f g) = eval (fun (i : Input) => Sum.elim inputs id (f i)) registers g

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.cost_mapSource {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} {Register : Type u_4} (f : Input → Input' ⊕ F) (g : Gate F Input Register) : (mapSource f g).cost = g.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.mapInput {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} (f : Input → Input') {r : ℕ} : Program F Input r → Program F Input' r

Relabel every input wire of a straight-line program.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_mapInput {F : Type u_1} [Field F] {Input : Type u_2} {Input' : Type u_3} (f : Input → Input') {r : ℕ} (p : Program F Input r) (inputs : Input' → F) (i : Fin r) : (mapInput f p).eval inputs i = p.eval (inputs ∘ f) i

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.cost_mapInput {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} (f : Input → Input') {r : ℕ} (p : Program F Input r) : (mapInput f p).cost = p.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.mapSource {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} (f : Input → Input' ⊕ F) {r : ℕ} : Program F Input r → Program F Input' r

Specialize a program's inputs to new wires or literal scalars.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval_mapSource {F : Type u_1} [Field F] {Input : Type u_2} {Input' : Type u_3} (f : Input → Input' ⊕ F) {r : ℕ} (p : Program F Input r) (inputs : Input' → F) (i : Fin r) : (mapSource f p).eval inputs i = p.eval (fun (j : Input) => Sum.elim inputs id (f j)) i

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.cost_mapSource {F : Type u_1} {Input : Type u_2} {Input' : Type u_3} (f : Input → Input' ⊕ F) {r : ℕ} (p : Program F Input r) : (mapSource f p).cost = p.cost

structure MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.Substituted {F : Type u_1} [Field F] {Input : Type u_2} {Mid : Type u_4} {r s : ℕ} (p : Program F Input r) (q : Program F Mid s) (wires : Mid → Fin r) : Type (max u_1 u_2)

A composed program with output maps and correctness and cost certificates for both stages.

• registers : ℕ

  Number of registers in the composed program.

• program : Program F Input self.registers

  The straight-line program realizing the composition.

• oldOutput : Fin r → Fin self.registers

  Locations of the first program's outputs in the composed register space.

• output : Fin s → Fin self.registers

  Locations of the second program's outputs in the composed register space.

• correctOld (inputs : Input → F) (i : Fin r) : self.program.eval inputs (self.oldOutput i) = p.eval inputs i
• correct (inputs : Input → F) (i : Fin s) : self.program.eval inputs (self.output i) = q.eval (fun (j : Mid) => p.eval inputs (wires j)) i
• cost_eq : self.program.cost = p.cost + q.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.Substituted.step {F : Type u_1} [Field F] {Input : Type u_2} {Mid : Type u_4} {r s : ℕ} {p : Program F Input r} {q : Program F Mid s} {wires : Mid → Fin r} (a : p.Substituted q wires) (g : Gate F Mid (Fin s)) (h : Gate F Input (Fin a.registers)) (heval : ∀ (inputs : Input → F), Gate.eval inputs (a.program.eval inputs) h = Gate.eval (fun (j : Mid) => p.eval inputs (wires j)) (q.eval fun (j : Mid) => p.eval inputs (wires j)) g) (hcost : h.cost = g.cost) : p.Substituted (q.step g) wires

Extend a certified composition by one gate without changing its cost accounting.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.substitute {F : Type u_1} [Field F] {Input : Type u_2} {Mid : Type u_4} {r : ℕ} (p : Program F Input r) {s : ℕ} (q : Program F Mid s) (wires : Mid → Fin r) : p.Substituted q wires

Substitute the outputs of one program for the input wires of another.

Equations

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