Proof-carrying program compaction

Programs are rebuilt from left to right. A source gate is either copied to the new program or identified with an existing wire. The constructors hide all dependent Fin transport and preserve the complete source trace.

structure Cslib.Circuits.Program.Compaction {σ : Signature} {n g : ℕ} {U : Type u_2} (source : Program σ n g) (interpretation : Interpretation σ U) : Type u_1

A semantics-preserving rebuilding of a program with no additional gates.

• gateCount : ℕ

  Number of gates in the rebuilt program.

• result : Program σ n self.gateCount

  Rebuilt program.

• wireMap : Wire.Renaming n g self.gateCount

  Translation of every source wire to its representative.

• trace_eq (input : Fin n → U) (wire : Wire n g) : self.result.trace interpretation input (self.wireMap.apply wire) = source.trace interpretation input wire

  Every translated wire computes its original value.

• gateCount_le : self.gateCount ≤ g

  The rebuilt program has no more gates than the source.

• cost_le (operationCost : Algebraic.OperationCost σ) : cost operationCost self.result ≤ cost operationCost source

  Compaction does not increase any nonnegative operation cost.

structure Cslib.Circuits.Circuit.Compaction {σ : Signature} {n m : ℕ} {U : Type u_2} (source : Circuit σ n m) (interpretation : Interpretation σ U) : Type u_1

A semantics-preserving circuit compaction that does not increase cost.

• result : Circuit σ n m

  Rebuilt circuit.

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

  Pointwise semantic preservation.

• gateCount_le : self.result.size ≤ source.size

  The rebuilt circuit has no more internal gates than the source.

• cost_le (operationCost : Algebraic.OperationCost σ) : self.result.cost operationCost ≤ source.cost operationCost

  Compaction does not increase any nonnegative operation cost.

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.Compaction.gateCount {σ : Signature} {n m : ℕ} {U : Type u_2} {source : Circuit σ n m} {interpretation : Interpretation σ U} (compaction : source.Compaction interpretation) : ℕ

Number of internal gates in the rebuilt circuit.

Equations

• compaction.gateCount = compaction.result.size

def Cslib.Circuits.Program.Compaction.empty {σ : Signature} {n : ℕ} {U : Type u} (interpretation : Interpretation σ U) : Program.empty.Compaction interpretation

The empty program compacts to itself.

Equations

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

theorem Cslib.Circuits.Program.Compaction.mapLine_eval {σ : Signature} {n g : ℕ} {U : Type u} {source : Program σ n g} {interpretation : Interpretation σ U} (compaction : source.Compaction interpretation) (line : Line σ n g) (input : Fin n → U) : (line.mapWires compaction.wireMap.apply).eval interpretation input (compaction.result.eval interpretation input) = line.eval interpretation input (source.eval interpretation input)

Evaluation of a line is preserved after mapping it through a compaction.

def Cslib.Circuits.Program.Compaction.copy {σ : Signature} {n g : ℕ} {U : Type u} {source : Program σ n g} {interpretation : Interpretation σ U} (compaction : source.Compaction interpretation) (line : Line σ n g) : (source.gate line).Compaction interpretation

Retain the new last source gate in the rebuilt program.

Equations

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

def Cslib.Circuits.Program.Compaction.eliminate {σ : Signature} {n g : ℕ} {U : Type u} {source : Program σ n g} {interpretation : Interpretation σ U} (compaction : source.Compaction interpretation) (line : Line σ n g) (replacement : Wire n compaction.gateCount) (replacement_eq : ∀ (input : Fin n → U), compaction.result.trace interpretation input replacement = (line.mapWires compaction.wireMap.apply).eval interpretation input (compaction.result.eval interpretation input)) : (source.gate line).Compaction interpretation

Replace the new last source gate by an existing rebuilt wire.

Equations

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

def Cslib.Circuits.Program.Compaction.toCircuit {σ : Signature} {n m : ℕ} {U : Type u} {interpretation : Interpretation σ U} {circuit : Circuit σ n m} (compaction : circuit.program.Compaction interpretation) : circuit.Compaction interpretation

Lift a program compaction to a circuit by renaming its output wires.

Equations

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

def Cslib.Circuits.Circuit.Compaction.toReduction {σ : Signature} {n m : ℕ} {U : Type u} {source : Circuit σ n m} {interpretation : Interpretation σ U} (compaction : source.Compaction interpretation) (operationCost : Algebraic.OperationCost σ) : Reduction operationCost source interpretation Algebraic.InputSubstitution.id

View a compaction as a certified identity-substitution reduction.

Equations

• compaction.toReduction operationCost = { result := compaction.result, eval_eq := ⋯, saving := source.cost operationCost - compaction.result.cost operationCost, saving_le := ⋯ }