CSLib De Morgan circuits as Complexitylib circuits

CSLib's circuit model (Cslib.Circuits.Circuit) is a straight-line program over a signature, with designated output wires. Its De Morgan basis (Cslib.Circuits.Boolean.signature) has constants, negation, and binary conjunction and disjunction, and every gate counts toward size. A circuit carries its gate count as the field size.

A CSLib wire (Cslib.Circuits.Wire N g) is either an input Wire.input i or a gate Wire.gate j. Our circuits number their wires Fin (N + g), the inputs first and gate j driving wire N + j, which is exactly CSLib's numbering Wire.index. This file translates a CSLib De Morgan circuit gate for gate into a fan-in-two AND/OR circuit over Basis.andOr2, whose negations are free:

• a negation ¬w becomes ¬w ∧ ¬w;
• a constant becomes x₀ ∧ ¬x₀ or x₀ ∨ ¬x₀ on the first input;
• conjunction and disjunction are unchanged;
• an output wire w becomes the output gate w ∧ w.

So the translated circuit has exactly the CSLib circuit's gates as internal gates, plus one output gate per output.

Main definitions

• Complexity.Circuit.ofCslibGate — the gate simulating one CSLib line
• Complexity.Circuit.ofCslib — the circuit simulating a CSLib circuit

def Complexity.Circuit.firstWire {N g : ℕ} [NeZero N] : Fin (N + g)

The first input wire, read by the gates simulating constants.

Equations

• Complexity.Circuit.firstWire = ⟨0, ⋯⟩

def Complexity.Circuit.ofCslibGate {N g : ℕ} [NeZero N] (l : Cslib.Circuits.Line Cslib.Circuits.Boolean.signature N g) : Gate Basis.andOr2 (N + g)

The fan-in-two AND/OR gate computing a CSLib De Morgan line.

Equations

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

theorem Complexity.Circuit.ofCslibGate_inputs_lt {N g : ℕ} [NeZero N] (l : Cslib.Circuits.Line Cslib.Circuits.Boolean.signature N g) {bound : ℕ} (hN : N ≤ bound) (hl : ∀ (a : Fin (Cslib.Circuits.Boolean.signature.Arity l.op)), ↑(l.wires a).index < bound) (k : Fin (ofCslibGate l).fanIn) : ↑((ofCslibGate l).inputs k) < bound

The gate simulating a line reads only the first input and the line's own wires.

def Complexity.Circuit.ofCslib {N M : ℕ} [NeZero N] [NeZero M] (c : Cslib.Circuits.Circuit Cslib.Circuits.Boolean.signature N M) : Circuit Basis.andOr2 N M c.size

The fan-in-two AND/OR circuit simulating a CSLib De Morgan circuit. Its internal gates are the CSLib circuit's gates, and output j is the gate w ∧ w on CSLib's output wire w.

Equations

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