Iterating an endomorphism circuit

Sequentially compose a circuit with itself while retaining exact semantics and cost. This construction is useful for fixed-round arithmetic algorithms such as exponentiation and inversion.

def Cslib.Circuits.Circuit.iterateFunction {A : Sort u} (function : A → A) : ℕ → A → A

Left-associated iteration, universe-polymorphic over Sort.

Equations

• Cslib.Circuits.Circuit.iterateFunction function 0 = id
• Cslib.Circuits.Circuit.iterateFunction function steps.succ = fun (input : A) => function (Cslib.Circuits.Circuit.iterateFunction function steps input)

def Cslib.Circuits.Circuit.iterate {σ : Signature} {n : ℕ} (circuit : Circuit σ n n) (steps : ℕ) : Circuit σ n n

Compose an endomorphism circuit with itself steps times.

Equations

• circuit.iterate 0 = Cslib.Circuits.Circuit.id σ n
• circuit.iterate steps.succ = circuit.comp (circuit.iterate steps)

@[simp]

theorem Cslib.Circuits.Circuit.size_iterate {σ : Signature} {n : ℕ} (circuit : Circuit σ n n) (steps : ℕ) : (circuit.iterate steps).size = steps * circuit.size

Iterating a circuit multiplies its gate count by the round count.

@[simp]

theorem Cslib.Circuits.Circuit.eval_iterate {σ : Signature} {n : ℕ} {U : Type u_2} (circuit : Circuit σ n n) (steps : ℕ) (interpretation : Interpretation σ U) (input : Fin n → U) : (circuit.iterate steps).eval interpretation input = iterateFunction (circuit.eval interpretation) steps input

Iterated circuit evaluation is function iteration.

@[simp]

theorem Cslib.Circuits.Circuit.cost_iterate {σ : Signature} {n : ℕ} (circuit : Circuit σ n n) (steps : ℕ) (operationCost : Algebraic.OperationCost σ) : (circuit.iterate steps).cost operationCost = steps * circuit.cost operationCost

Iterating a circuit multiplies its weighted cost by the round count.