Typed circuits as CSLib straight-line programs

This file proves that Circuit.toStraightLine, which turns a typed circuit over a basis B into a CSLib circuit over B.signature, preserves the computed function, the size, and the total fan-in, and that its outputs are gates (Cslib.Circuits.Circuit.GatedOutputs). It is the correspondence on which the move of Complexitylib's circuit developments to CSLib's model rests (see ROADMAP.md, item 7). The correspondence proved here runs one way, from typed circuits to CSLib circuits; the translation back is not yet formalized.

Main results

• Complexity.Basis.interpretation_kind — the interpretation of a gate's kind is the gate's evaluation
• Complexity.StraightLine.eval_ofLines — each gate of a program built from lines evaluates its line on the values of the earlier gates
• Complexity.StraightLine.index_wireOfIndex — the wire with index w in the typed layout has CSLib index w
• Complexity.Circuit.eval_toStraightLine — the translation computes what the typed circuit computes
• Complexity.Circuit.size_toStraightLine — the translation has the typed circuit's size
• Complexity.Circuit.gatedOutputs_toStraightLine — every output of the translation is an internal gate
• Complexity.Circuit.totalFanIn_toStraightLine — the translation has the typed circuit's total fan-in

theorem Complexity.Basis.interpretation_kind {B : Basis} {W : ℕ} (g : Gate B W) (v : BitString W) : B.interpretation g.kind (v ∘ g.inputs) = g.eval v

The interpretation of a gate's kind, applied to the values of the gate's input wires, is the gate's evaluation: Basis.interpretation negates the flagged inputs and applies the operation exactly as Gate.eval does.

@[simp]

theorem Complexity.StraightLine.index_wireOfIndex {N j : ℕ} (w : ℕ) (hw : w < N + j) : (wireOfIndex w hw).index = ⟨w, hw⟩

The wire with index w in the layout of typed circuits has CSLib index w.

theorem Complexity.StraightLine.eval_ofLines {σ : Cslib.Circuits.Signature} {N : ℕ} {U : Type u_1} (I : Cslib.Circuits.Interpretation σ U) (x : Fin N → U) (g : ℕ) (lines : (j : Fin g) → Cslib.Circuits.Line σ N ↑j) (j : Fin g) : (Cslib.Circuits.Program.ofLines g lines).eval I x j = (lines j).eval I x fun (k : Fin ↑j) => (Cslib.Circuits.Program.ofLines g lines).eval I x (Fin.castLE ⋯ k)

Each gate of Program.ofLines g lines evaluates its line on the values of the earlier gates.

theorem Complexity.Circuit.eval_toStraightLine {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (x : BitString N) : c.toStraightLine.eval B.interpretation x = c.eval x

The straight-line form computes what the typed circuit computes.

theorem Complexity.Circuit.size_toStraightLine {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.toStraightLine.size = c.size

The straight-line form has the typed circuit's size.

theorem Complexity.Circuit.gatedOutputs_toStraightLine {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.toStraightLine.GatedOutputs

The straight-line form has gated outputs. Its outputs are the last M gates, the typed circuit's output gates, never an original input.

theorem Complexity.Circuit.totalFanIn_toStraightLine {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.toStraightLine.totalFanIn = c.totalFanIn

The straight-line form has the typed circuit's total fan-in. CSLib's Circuit.totalFanIn of the translation, the sum of the arities of its lines, equals the typed circuit's Circuit.totalFanIn, the sum of the fan-ins of its internal and output gates.