Proofs for the CSLib circuit bridge

• Circuit.eval_ofCslib_internal: the translation Circuit.ofCslib computes what the CSLib circuit computes. The proof shows that our wire values satisfy every gate equation of the CSLib program, which determines the program's evaluation (Program.eq_eval_of_forall_lines_eval).
• Circuit.exists_cslib_internal: every fan-in-two AND/OR circuit has a CSLib De Morgan circuit of size at most N + 2G + M computing the same outputs. The proof uses CSLib's synthesis calculus: it keeps every wire and its negation available, spending N gates on negated inputs, two gates per internal gate, and one gate per output.

theorem Complexity.Circuit.ofCslibGate_eval {N g : ℕ} [NeZero N] (l : Cslib.Circuits.Line Cslib.Circuits.Boolean.signature N g) (v : BitString (N + g)) : (ofCslibGate l).eval v = Cslib.Circuits.Boolean.interpretation l.op fun (a : Fin (Cslib.Circuits.Boolean.signature.Arity l.op)) => v (l.wires a).index

The gate simulating a line computes the line's operation.

theorem Complexity.Circuit.wireValue_ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) (x : BitString N) (w : Cslib.Circuits.Wire N c.size) : (ofCslib c).wireValue x w.index = c.program.trace Cslib.Circuits.Boolean.interpretation x w

Our wire values in the translation are the CSLib program's wire values.

theorem Complexity.Circuit.eval_ofCslib_internal {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) (x : BitString N) : (ofCslib c).eval x = c.eval Cslib.Circuits.Boolean.interpretation x

The translation computes what the CSLib circuit computes.

theorem Complexity.Circuit.synthesis_gate {N W : ℕ} (gt : Gate Basis.andOr2 W) (val : BitString N → BitString W) (s : Set (BitString N → Bool)) (hs : ∀ (k : Fin gt.fanIn), (fun (x : BitString N) => gt.negated k ^^ val x (gt.inputs k)) ∈ s) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation s {fun (x : BitString N) => gt.eval (val x)} 1

A fan-in-two AND/OR gate whose two literals are available costs one CSLib gate.

def Complexity.Circuit.litSet {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) (bound : ℕ) : Set (BitString N → Bool)

Literals b ⊕ w of the wires w below bound.

Equations

• c.litSet bound = {f : Complexity.BitString N → Bool | ∃ (b : Bool) (w : Fin (N + G)), ↑w < bound ∧ f = fun (x : Complexity.BitString N) => b ^^ c.wireValue x w}

theorem Complexity.Circuit.synthesis_litSet_zero {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs N) (c.litSet N) N

Spending one negation per input makes every input literal available.

theorem Complexity.Circuit.synthesis_litSet_succ {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) {i : ℕ} (hi : i < G) (h : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs N) (c.litSet (N + i)) (N + 2 * i)) : Cslib.Circuits.Synthesis Cslib.Circuits.Boolean.interpretation (Cslib.Circuits.inputs N) (c.litSet (N + (i + 1))) (N + 2 * (i + 1))

Two more gates make both literals of the next gate wire available.

theorem Complexity.Circuit.exists_cslib_internal {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.andOr2 N M G) : ∃ (c' : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M), c'.size ≤ N + 2 * G + M ∧ ∀ (x : Fin N → Bool) (j : Fin M), c'.eval Cslib.Circuits.Boolean.interpretation x j = c.eval x j

Every fan-in-two AND/OR circuit is a CSLib De Morgan circuit of size at most N + 2G + M computing the same outputs.