Block-valued circuit translations

A width-k block translation implements each scalar source operation by a target circuit with k output wires and one k-wire block for every source argument. Compilation maps n source inputs to n * k target inputs and m source outputs to m * k target outputs while retaining one shared gadget per source gate.

def Algebraic.Block.flatten {n k : ℕ} {U : Sort u_1} (values : Fin n → Fin k → U) : Fin (n * k) → U

Flatten an indexed family of width-k blocks.

Equations

• Algebraic.Block.flatten values index = values (finProdFinEquiv.symm index).1 (finProdFinEquiv.symm index).2

def Algebraic.Block.unflatten {n k : ℕ} {U : Sort u_1} (values : Fin (n * k) → U) : Fin n → Fin k → U

Split a flat vector into width-k blocks.

Equations

• Algebraic.Block.unflatten values block component = values (finProdFinEquiv (block, component))

@[simp]

theorem Algebraic.Block.flatten_apply {n k : ℕ} {U : Sort u_1} (values : Fin n → Fin k → U) (block : Fin n) (component : Fin k) : flatten values (finProdFinEquiv (block, component)) = values block component

@[simp]

theorem Algebraic.Block.unflatten_apply {n k : ℕ} {U : Sort u_1} (values : Fin (n * k) → U) (block : Fin n) (component : Fin k) : unflatten values block component = values (finProdFinEquiv (block, component))

@[simp]

theorem Algebraic.Block.unflatten_flatten {n k : ℕ} {U : Sort u_1} (values : Fin n → Fin k → U) : unflatten (flatten values) = values

@[simp]

theorem Algebraic.Block.flatten_unflatten {n k : ℕ} {U : Sort u_1} (values : Fin (n * k) → U) : flatten (unflatten values) = values

def Algebraic.Block.inputWire {n k g : ℕ} (input : Fin n) (component : Fin k) : Wire (n * k) g

The target input wire carrying one component of one source input.

Equations

• Algebraic.Block.inputWire input component = Cslib.Circuits.Wire.input (finProdFinEquiv (input, component))

structure Algebraic.BlockTranslation (σ : Signature) (τ : Signature) (k : ℕ) : Type (max u_1 u_2)

An implementation of every source operation by a width-k, multi-output target circuit.

• operation (op : σ.Op) : Circuit τ (σ.Arity op * k) k

  A gadget receives one target block per source argument and returns one target block.

@[reducible, inline]

abbrev Algebraic.BlockTranslation.gateCount {σ : Signature} {τ : Signature} {k : ℕ} (translation : BlockTranslation σ τ k) (op : σ.Op) : ℕ

Number of target gates used by each operation gadget.

Equations

• translation.gateCount op = (translation.operation op).size

def Algebraic.BlockTranslation.pull {σ : Signature} {τ : Signature} {k : ℕ} {U : Type u_3} (translation : BlockTranslation σ τ k) (interpretation : Interpretation τ U) : Interpretation σ (Fin k → U)

Pull a target interpretation back to an interpretation on width-k blocks.

Equations

• translation.pull interpretation op input = (translation.operation op).eval interpretation (Algebraic.Block.flatten input)

def Algebraic.BlockTranslation.pullCost {σ : Signature} {τ : Signature} {k : ℕ} (translation : BlockTranslation σ τ k) (operationCost : OperationCost τ) : OperationCost σ

Charge each source operation by the exact target cost of its block gadget.

Equations

• translation.pullCost operationCost op = (translation.operation op).cost operationCost

structure Algebraic.BlockTranslation.ProgramCompilation {σ : Signature} {τ : Signature} {k n g : ℕ} (translation : BlockTranslation σ τ k) (source : Program σ n g) : Type u_2

A compiled target program together with the target block representing every source wire.

• gateCount : ℕ

  The number of target gates in the compiled program.

• program : Program τ (n * k) self.gateCount

  The compiled target program, over k target inputs per source input.

• wires : Wire n g → Fin k → Wire (n * k) self.gateCount

  The block of k target wires representing each source wire.

def Algebraic.BlockTranslation.compileProgram {σ : Signature} {τ : Signature} {k n g : ℕ} (translation : BlockTranslation σ τ k) (source : Program σ n g) : translation.ProgramCompilation source

Compile a source program through a block translation.

Equations

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

def Algebraic.BlockTranslation.compiledGateCount {σ : Signature} {τ : Signature} {k n m : ℕ} (translation : BlockTranslation σ τ k) (circuit : Circuit σ n m) : ℕ

Number of target gates produced by block compilation.

Equations

• translation.compiledGateCount circuit = (translation.compileProgram circuit.program).gateCount

def Algebraic.BlockTranslation.compile {σ : Signature} {τ : Signature} {k n m : ℕ} (translation : BlockTranslation σ τ k) (circuit : Circuit σ n m) : Circuit τ (n * k) (m * k)

Compile a source circuit, flattening its input and output blocks.

Equations

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

theorem Algebraic.BlockTranslation.compileProgram_trace {σ : Signature} {τ : Signature} {k n g : ℕ} {U : Type u_3} (translation : BlockTranslation σ τ k) (source : Program σ n g) (interpretation : Interpretation τ U) (input : Fin n → Fin k → U) (wire : Wire n g) (component : Fin k) : (translation.compileProgram source).program.trace interpretation (Block.flatten input) ((translation.compileProgram source).wires wire component) = source.trace (translation.pull interpretation) input wire component

Program compilation preserves every component of every source wire.

theorem Algebraic.BlockTranslation.compile_eval {σ : Signature} {τ : Signature} {k n m : ℕ} {U : Type u_3} (translation : BlockTranslation σ τ k) (circuit : Circuit σ n m) (interpretation : Interpretation τ U) (input : Fin n → Fin k → U) : (translation.compile circuit).eval interpretation (Block.flatten input) = Block.flatten (circuit.eval (translation.pull interpretation) input)

Block compilation preserves evaluation exactly after flattening.

theorem Algebraic.BlockTranslation.compileProgram_cost {σ : Signature} {τ : Signature} {k n g : ℕ} (translation : BlockTranslation σ τ k) (source : Program σ n g) (operationCost : OperationCost τ) : Program.cost operationCost (translation.compileProgram source).program = Program.cost (translation.pullCost operationCost) source

Block program compilation preserves pulled-back weighted cost exactly.

theorem Algebraic.BlockTranslation.compile_cost {σ : Signature} {τ : Signature} {k n m : ℕ} (translation : BlockTranslation σ τ k) (circuit : Circuit σ n m) (operationCost : OperationCost τ) : (translation.compile circuit).cost operationCost = circuit.cost (translation.pullCost operationCost)

Block circuit compilation preserves pulled-back weighted cost exactly.

theorem Algebraic.BlockTranslation.compile_size {σ : Signature} {τ : Signature} {k n m : ℕ} (translation : BlockTranslation σ τ k) (circuit : Circuit σ n m) : (translation.compile circuit).size = circuit.cost (translation.pullCost OperationCost.unit)

Block compilation has the exact size obtained by charging every source operation by its gadget gate count.

theorem Algebraic.BlockTranslation.compile_size_le_mul {σ : Signature} {τ : Signature} {k n m K : ℕ} (translation : BlockTranslation σ τ k) (circuit : Circuit σ n m) (bounded : ∀ (op : σ.Op), (translation.operation op).size ≤ K) : (translation.compile circuit).size ≤ K * circuit.size

A uniform local gadget bound gives the usual multiplicative size bound for block compilation.

@[reducible, inline]

abbrev Algebraic.BlockSimulation {σ : Signature} {τ : Signature} {k : ℕ} {U : Type u_3} {V : Type u_4} (translation : BlockTranslation σ τ k) (source : Interpretation σ U) (target : Interpretation τ V) : Type (max u_3 u_4)

A block simulation is a homomorphism into the block interpretation pulled back through a block translation.

Equations

• Algebraic.BlockSimulation translation source target = Cslib.Circuits.Homomorphism source (translation.pull target)

def Algebraic.BlockSimulation.ofPreserves {σ : Signature} {τ : Signature} {k : ℕ} {U : Type u_3} {V : Type u_4} {translation : BlockTranslation σ τ k} {source : Interpretation σ U} {target : Interpretation τ V} (map : U → Fin k → V) (preserves : ∀ (op : σ.Op) (input : Fin (σ.Arity op) → U), map (source op input) = (translation.operation op).eval target (Block.flatten (map ∘ input))) : BlockSimulation translation source target

Construct a block simulation from its operation-gadget preservation law.

Equations

• Algebraic.BlockSimulation.ofPreserves map preserves = { map := map, homomorphic := preserves }

theorem Algebraic.BlockSimulation.preserves {σ : Signature} {τ : Signature} {k : ℕ} {U : Type u_3} {V : Type u_4} {translation : BlockTranslation σ τ k} {source : Interpretation σ U} {target : Interpretation τ V} (simulation : BlockSimulation translation source target) (op : σ.Op) (input : Fin (σ.Arity op) → U) : simulation.map (source op input) = (translation.operation op).eval target (Block.flatten (simulation.map ∘ input))

The homomorphism law exposed directly in block-gadget form.

theorem Algebraic.BlockSimulation.map_compile_eval {σ : Signature} {τ : Signature} {k : ℕ} {U : Type u_3} {V : Type u_4} {n m : ℕ} {translation : BlockTranslation σ τ k} {source : Interpretation σ U} {target : Interpretation τ V} (simulation : BlockSimulation translation source target) (circuit : Circuit σ n m) (input : Fin n → U) : Block.flatten (simulation.map ∘ circuit.eval source input) = (translation.compile circuit).eval target (Block.flatten (simulation.map ∘ input))

Evaluation commutes with block compilation and encoding.