Circuit translations with shared context inputs

A contextual translation implements every source operation by a target circuit that receives a fixed block of shared context inputs followed by the ordinary operation arguments. Compilation retains one copy of the context for the whole source circuit.

This is useful when a syntactically nullary source gate denotes an object that depends on shared ambient variables—for example, a dictionary term in a Waring decomposition. Ordinary Translation cannot express that dependency because a nullary operation gadget has no inputs.

structure Algebraic.ContextualTranslation (σ : Signature) (τ : Signature) (q : ℕ) : Type (max u_1 u_2)

An implementation of every source operation by a target circuit with a shared q-input context followed by its ordinary arguments.

• operation (op : σ.Op) : Circuit τ (q + σ.Arity op) 1

  Target circuit implementing a source operation from the shared context and the operation's local arguments.

@[reducible, inline]

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

Number of target gates used to implement a source operation.

Equations

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

def Algebraic.ContextualTranslation.appendInputs {q : ℕ} {U : Sort u_1} {n : ℕ} (context : Fin q → U) (input : Fin n → U) : Fin (q + n) → U

Concatenate the shared context with the ordinary circuit inputs.

Equations

• Algebraic.ContextualTranslation.appendInputs context input i = Fin.addCases context input i

@[simp]

theorem Algebraic.ContextualTranslation.appendInputs_context {q : ℕ} {U : Sort u_1} {n : ℕ} (context : Fin q → U) (input : Fin n → U) (index : Fin q) : appendInputs context input (Fin.castAdd n index) = context index

@[simp]

theorem Algebraic.ContextualTranslation.appendInputs_input {q : ℕ} {U : Sort u_1} {n : ℕ} (context : Fin q → U) (input : Fin n → U) (index : Fin n) : appendInputs context input (Fin.natAdd q index) = input index

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

Pull a target interpretation back after fixing the shared context.

Equations

• translation.pull interpretation context op input = (translation.operation op).eval interpretation (Algebraic.ContextualTranslation.appendInputs context input) 0

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

Charge a source operation by the exact target cost of its contextual implementation.

Equations

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

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

The compiled target program and the image of every source wire.

• gateCount : ℕ

  Number of gates in the compiled target program.

• program : Program τ (q + n) self.gateCount

  Compiled program over the context followed by the source inputs.

• wires : Wire n g → Wire (q + n) self.gateCount

  Image of every source input or gate wire.

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

Compile a source program while sharing one ambient context block across all operation gadgets.

Equations

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

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

Number of target gates produced by contextual compilation.

Equations

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

def Algebraic.ContextualTranslation.compile {σ : Signature} {τ : Signature} {q n m : ℕ} (translation : ContextualTranslation σ τ q) (circuit : Circuit σ n m) : Circuit τ (q + n) m

Compile a circuit, prefixing its source inputs by the shared context.

Equations

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

theorem Algebraic.ContextualTranslation.compileProgram_trace {σ : Signature} {τ : Signature} {q n g : ℕ} {U : Type u_3} (translation : ContextualTranslation σ τ q) (source : Program σ n g) (interpretation : Interpretation τ U) (context : Fin q → U) (input : Fin n → U) (wire : Wire n g) : (translation.compileProgram source).program.trace interpretation (appendInputs context input) ((translation.compileProgram source).wires wire) = source.trace (translation.pull interpretation context) input wire

Contextual program compilation preserves the value of every source wire.

theorem Algebraic.ContextualTranslation.compile_eval {σ : Signature} {τ : Signature} {q n m : ℕ} {U : Type u_3} (translation : ContextualTranslation σ τ q) (circuit : Circuit σ n m) (interpretation : Interpretation τ U) (context : Fin q → U) (input : Fin n → U) : (translation.compile circuit).eval interpretation (appendInputs context input) = circuit.eval (translation.pull interpretation context) input

Contextual circuit compilation preserves evaluation exactly.

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

Contextual program compilation preserves pulled-back weighted cost exactly.

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

Contextual circuit compilation preserves pulled-back weighted cost exactly.

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

The compiled size is source cost under contextual gadget sizes.

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

A uniform contextual gadget-size bound controls compilation size.