Certified circuit reductions

A reduction packages a semantics-preserving circuit transformation under an input substitution together with a certified cost saving. The construction of the residual circuit is deliberately basis-specific; consumers need only this common certificate.

def Cslib.Circuits.Circuit.CostMinimal {σ : Signature} {n m : ℕ} {U : Type u_2} (operationCost : Algebraic.OperationCost σ) (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) : Prop

A circuit has minimum weighted cost among all circuits computing a target.

Equations

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

structure Cslib.Circuits.Circuit.CostSizeMinimal {σ : Signature} {n m : ℕ} {U : Type u_2} (operationCost : Algebraic.OperationCost σ) (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) : Prop

A circuit is lexicographically minimal by weighted cost and then by internal gate count. The tie-break excludes gratuitous zero-cost internal structure.

• cost : CostMinimal operationCost circuit interpretation target

  No implementation has lower weighted cost.

• gateCount (competitor : Circuit σ n m) : competitor.ComputesWith interpretation target → competitor.cost operationCost = circuit.cost operationCost → circuit.size ≤ competitor.size

  Among equal-cost implementations, none has fewer internal gates.

structure Cslib.Circuits.Circuit.Minimum {σ : Signature} {U : Type u_2} {n m : ℕ} (operationCost : Algebraic.OperationCost σ) (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) : Type u_1

A minimum-cost implementation of a target, including its proof.

• circuit : Circuit σ n m

  Chosen implementation.

• computes : self.circuit.ComputesWith interpretation target

  The implementation computes the requested target.

• minimal : CostSizeMinimal operationCost self.circuit interpretation target

  The implementation is cost-minimal with a gate-count tie-break.

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.Minimum.gateCount {σ : Signature} {U : Type u_2} {n m : ℕ} {operationCost : Algebraic.OperationCost σ} {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} (minimum : Minimum operationCost interpretation target) : ℕ

Number of internal gates in the chosen implementation.

Equations

• minimum.gateCount = minimum.circuit.size

noncomputable def Cslib.Circuits.Circuit.minimum {σ : Signature} {n m : ℕ} {U : Type u_2} (operationCost : Algebraic.OperationCost σ) (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (computes : circuit.ComputesWith interpretation target) : Minimum operationCost interpretation target

Choose a minimum-cost implementation of a target from any supplied implementation. This uses only well-ordering of natural-valued costs; the collection of circuits need not be finite. The chosen implementation is a classical proof witness, not an executable circuit optimizer.

Equations

• Cslib.Circuits.Circuit.minimum operationCost circuit interpretation target computes = { circuit := Classical.choose ⋯, computes := ⋯, minimal := ⋯ }

structure Cslib.Circuits.Circuit.Reduction {σ : Signature} {n m : ℕ} {U : Type u_2} {k : ℕ} (operationCost : Algebraic.OperationCost σ) (source : Circuit σ n m) (interpretation : Interpretation σ U) (substitution : Algebraic.InputSubstitution U n k) : Type u_1

A circuit reduction under an input substitution with certified cost saving.

• result : Circuit σ k m

  The residual circuit on the new inputs.

• eval_eq (input : Fin k → U) : self.result.eval interpretation input = source.eval interpretation (substitution.apply input)

  The residual circuit agrees with the source under the substitution.

• saving : ℕ

  Certified amount by which the chosen cost decreases.

• saving_le : self.saving + self.result.cost operationCost ≤ source.cost operationCost

  The residual cost plus the saving is bounded by the source cost.

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.Reduction.gateCount {σ : Signature} {n m : ℕ} {U : Type u_2} {k : ℕ} {operationCost : Algebraic.OperationCost σ} {source : Circuit σ n m} {interpretation : Interpretation σ U} {substitution : Algebraic.InputSubstitution U n k} (reduction : Reduction operationCost source interpretation substitution) : ℕ

Number of internal gates in the residual circuit.

Equations

• reduction.gateCount = reduction.result.size

def Cslib.Circuits.Circuit.Reduction.refl {σ : Signature} {n m : ℕ} {U : Type u_2} (operationCost : Algebraic.OperationCost σ) (circuit : Circuit σ n m) (interpretation : Interpretation σ U) : Reduction operationCost circuit interpretation Algebraic.InputSubstitution.id

The identity circuit reduction.

Equations

• Cslib.Circuits.Circuit.Reduction.refl operationCost circuit interpretation = { result := circuit, eval_eq := ⋯, saving := 0, saving_le := ⋯ }

def Cslib.Circuits.Circuit.Reduction.rebaseSource {σ : Signature} {n m : ℕ} {U : Type u_2} {k : ℕ} {operationCost : Algebraic.OperationCost σ} {interpretation : Interpretation σ U} {source replacement : Circuit σ n m} {target : Algebraic.Target U n m} {substitution : Algebraic.InputSubstitution U n k} (reduction : Reduction operationCost replacement interpretation substitution) (sourceComputes : source.ComputesWith interpretation target) (replacementComputes : replacement.ComputesWith interpretation target) (cost_le : replacement.cost operationCost ≤ source.cost operationCost) : Reduction operationCost source interpretation substitution

Rebase a reduction from a cheaper implementation of the same target onto the original source circuit. This is the bridge from optimal-circuit elimination arguments to lower bounds for arbitrary circuits.

Equations

• reduction.rebaseSource sourceComputes replacementComputes cost_le = { result := reduction.result, eval_eq := ⋯, saving := reduction.saving, saving_le := ⋯ }

def Cslib.Circuits.Circuit.Reduction.trans {U : Type u_1} {n k : ℕ} {σ✝ : Signature} {operationCost : Algebraic.OperationCost σ✝} {outputCount✝ : ℕ} {source : Circuit σ✝ n outputCount✝} {interpretation : Interpretation σ✝ U} {l : ℕ} {firstSubstitution : Algebraic.InputSubstitution U n k} (first : Reduction operationCost source interpretation firstSubstitution) {secondSubstitution : Algebraic.InputSubstitution U k l} (second : Reduction operationCost first.result interpretation secondSubstitution) : Reduction operationCost source interpretation (firstSubstitution.comp secondSubstitution)

Compose certified circuit reductions.

Equations

• first.trans second = { result := second.result, eval_eq := ⋯, saving := first.saving + second.saving, saving_le := ⋯ }

theorem Cslib.Circuits.Circuit.Reduction.computes {U : Type u_1} {n m : ℕ} {σ✝ : Signature} {operationCost : Algebraic.OperationCost σ✝} {source : Circuit σ✝ n m} {interpretation : Interpretation σ✝ U} {k✝ : ℕ} {substitution : Algebraic.InputSubstitution U n k✝} {target : Algebraic.Target U n m} (reduction : Reduction operationCost source interpretation substitution) (computes : source.ComputesWith interpretation target) : reduction.result.ComputesWith interpretation (target.substitute substitution)

A reduction of a computing circuit computes the restricted target.