Dependency support as an abstract interpretation

Each input is initialized with its singleton coordinate and every operation unions the supports of its arguments. Evaluation then reproduces the existing structural support analysis exactly, so translations inherit exact dependency semantics from the general compilation theorem.

def Cslib.Circuits.Signature.supportInterpretation (σ : Signature) (n : ℕ) : Interpretation σ (Finset (Fin n))

The dependency-support interpretation on n original inputs.

Equations

• σ.supportInterpretation n x✝ input = Finset.univ.biUnion input

theorem Cslib.Circuits.Program.eval_supportInterpretation {σ : Signature} {n g : ℕ} (program : Program σ n g) : (program.eval (σ.supportInterpretation n) fun (input : Fin n) => {input}) = program.gateSupport

Evaluating a program in the support interpretation gives exactly its gate supports.

theorem Cslib.Circuits.Program.trace_supportInterpretation {σ : Signature} {n g : ℕ} (program : Program σ n g) : (program.trace (σ.supportInterpretation n) fun (input : Fin n) => {input}) = program.wireSupport

Evaluating all wires in the support interpretation gives exactly the program's wire supports.

theorem Cslib.Circuits.Circuit.eval_supportInterpretation {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) : (circuit.eval (σ.supportInterpretation n) fun (input : Fin n) => {input}) = circuit.outputSupport

Circuit evaluation in the support interpretation gives each designated output's structural support.

theorem Algebraic.Translation.compile_outputSupport {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) : (translation.compile circuit).outputSupport = circuit.eval (translation.pull (τ.supportInterpretation n)) fun (input : Fin n) => {input}

Compiled output support is exact evaluation of the source circuit in the pulled-back target support interpretation.