Arithmetic expressions compiled to circuits

This module supplies a small reusable expression language for arithmetic circuits. Compilation is tree-shaped: the left subtree is emitted first, the right subtree is instantiated after it over the same original inputs, and the root operation is appended last. The result is a circuit whose bundled size is definitionally the expression gate count.

inductive Algebraic.Arithmetic.Expression (C : Type u) (n : ℕ) : Type u

Tree-shaped arithmetic expressions with named constants.

• input {C : Type u} {n : ℕ} (index : Fin n) : Expression C n
• constant {C : Type u} {n : ℕ} (value : C) : Expression C n
• add {C : Type u} {n : ℕ} (left right : Expression C n) : Expression C n
• mul {C : Type u} {n : ℕ} (left right : Expression C n) : Expression C n

@[reducible]

def Algebraic.Arithmetic.Expression.gateCount {C : Type u_1} {n : ℕ} : Expression C n → ℕ

Number of gates emitted by tree compilation. Inputs are free.

Equations

• (Algebraic.Arithmetic.Expression.input index).gateCount = 0
• (Algebraic.Arithmetic.Expression.constant value).gateCount = 1
• (left.add right).gateCount = left.gateCount + right.gateCount + 1
• (left.mul right).gateCount = left.gateCount + right.gateCount + 1

@[reducible]

def Algebraic.Arithmetic.Expression.weightedCost {C : Type u_1} {n : ℕ} (addition multiplication : ℕ) : Expression C n → ℕ

Weighted number of binary arithmetic nodes. Constants are free, matching Arithmetic.weightedCost; tree compilation realizes this cost exactly.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Arithmetic.Expression.weightedCost addition multiplication (Algebraic.Arithmetic.Expression.input index) = 0
• Algebraic.Arithmetic.Expression.weightedCost addition multiplication (Algebraic.Arithmetic.Expression.constant value) = 0

@[reducible]

def Algebraic.Arithmetic.Expression.multiplicationCount {C : Type u_1} {n : ℕ} : Expression C n → ℕ

Number of multiplication nodes in an expression.

Equations

• Algebraic.Arithmetic.Expression.multiplicationCount = Algebraic.Arithmetic.Expression.weightedCost 0 1

@[reducible]

def Algebraic.Arithmetic.Expression.additionCount {C : Type u_1} {n : ℕ} : Expression C n → ℕ

Number of addition nodes in an expression.

Equations

• Algebraic.Arithmetic.Expression.additionCount = Algebraic.Arithmetic.Expression.weightedCost 1 0

def Algebraic.Arithmetic.Expression.eval {R : Type u_1} {C : Type u_2} {n : ℕ} [Add R] [Mul R] (constant : C → R) (input : Fin n → R) : Expression C n → R

Evaluate an expression in an arbitrary arithmetic carrier.

Equations

• Algebraic.Arithmetic.Expression.eval constant input (Algebraic.Arithmetic.Expression.input index) = input index
• Algebraic.Arithmetic.Expression.eval constant input (Algebraic.Arithmetic.Expression.constant value) = constant value
• Algebraic.Arithmetic.Expression.eval constant input (left.add right) = Algebraic.Arithmetic.Expression.eval constant input left + Algebraic.Arithmetic.Expression.eval constant input right
• Algebraic.Arithmetic.Expression.eval constant input (left.mul right) = Algebraic.Arithmetic.Expression.eval constant input left * Algebraic.Arithmetic.Expression.eval constant input right

structure Algebraic.Arithmetic.Expression.Compilation {C : Type u_1} {n : ℕ} (expression : Expression C n) : Type u_1

A compiled expression program together with its result wire.

• program : Program (signature C) n expression.gateCount

  Emitted straight-line program.

• output : Wire n expression.gateCount

  Wire carrying the expression value.

def Algebraic.Arithmetic.Expression.compile {C : Type u_1} {n : ℕ} (expression : Expression C n) : expression.Compilation

Compile an arithmetic expression to a straight-line program.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.Arithmetic.Expression.input index).compile = { program := Cslib.Circuits.Program.empty, output := Cslib.Circuits.Wire.input index }

def Algebraic.Arithmetic.Expression.circuit {C : Type u_1} {n : ℕ} (expression : Expression C n) : Circuit (signature C) n 1

The one-output circuit emitted for an expression.

Equations

• expression.circuit = { size := expression.gateCount, program := expression.compile.program, outputs := fun (x : Fin 1) => expression.compile.output }

@[simp]

theorem Algebraic.Arithmetic.Expression.size_circuit {C : Type u_1} {n : ℕ} (expression : Expression C n) : expression.circuit.size = expression.gateCount

The circuit emitted for an expression has exactly the expression gate count.

theorem Algebraic.Arithmetic.Expression.compile_weightedCost {C : Type u_1} {n : ℕ} (addition multiplication : ℕ) (expression : Expression C n) : Program.cost (Arithmetic.weightedCost addition multiplication) expression.compile.program = weightedCost addition multiplication expression

Tree compilation preserves every binary arithmetic weighting exactly.

@[simp]

theorem Algebraic.Arithmetic.Expression.circuit_multiplicationCost {C : Type u_1} {n : ℕ} (expression : Expression C n) : expression.circuit.cost multiplicationCost = expression.multiplicationCount

Exact multiplicative complexity of a compiled expression.

@[simp]

theorem Algebraic.Arithmetic.Expression.circuit_additionCost {C : Type u_1} {n : ℕ} (expression : Expression C n) : expression.circuit.cost additionCost = expression.additionCount

Exact additive complexity of a compiled expression.

theorem Algebraic.Arithmetic.Expression.compile_trace {R : Type u_1} {C : Type u_2} {n : ℕ} [Add R] [Mul R] (constant : C → R) (input : Fin n → R) (expression : Expression C n) : expression.compile.program.trace (interpretation constant) input expression.compile.output = eval constant input expression

Tree compilation preserves expression evaluation.

theorem Algebraic.Arithmetic.Expression.circuit_eval {R : Type u_1} {C : Type u_2} {n : ℕ} [Add R] [Mul R] (constant : C → R) (input : Fin n → R) (expression : Expression C n) : expression.circuit.eval (interpretation constant) input 0 = eval constant input expression

Circuit evaluation of a compiled expression is its direct evaluation.