Circuits as lists of gates

A circuit is written down as data by listing its gates in program order. Wires are numbered as in Cslib.Circuits.Circuit.trace: input i is wire i and gate j is wire n + j, where n is the number of inputs (Wire.toNat). A line is written as its operation and the numbers of the wires it reads (Line.code), a program as the list of its lines (Program.code), and a circuit as its program and the numbers of its output wires (Circuit.code). The size of a circuit is the length of its gate list (Program.length_code).

Decoding (Program.ofCode, Circuit.ofCode) checks that every line has as many arguments as its operation's arity and reads only inputs and earlier gates, and that the outputs are wires of the circuit. It inverts coding (Circuit.ofCode_code), and every list it accepts is the code of the circuit it returns (Circuit.code_of_ofCode_eq_some); so a list of gates that passes these checks is a circuit, with the usual semantics. The lists it accepts are described by Program.IsCodeFrom (Program.isSome_ofCode_iff, Circuit.isSome_ofCode_iff). All of this is defined for an arbitrary signature.

For the De Morgan basis, an operation is written as its number Boolean.Op.toNat in unary and a wire number in binary (Boolean.encGate). A circuit with n inputs and m outputs is encoded by n in unary, then its framed gates in program order, then its framed output wires (Boolean.encCircuit). Writing n in unary makes the encoding at least as long as the number of inputs, as when inputs are counted as vertices of the circuit Arora and Barak, Section 6.1. Gates may read wires of any number below their own, so wire numbers take logarithmically many bits.

Main definitions

• Cslib.Circuits.Wire.toNat, Cslib.Circuits.Wire.ofNat: wire numbers.
• Cslib.Circuits.Line.code, Cslib.Circuits.Program.code, Cslib.Circuits.Circuit.code: circuits as lists of gates.
• Cslib.Circuits.Line.ofCode, Cslib.Circuits.Program.ofCode, Cslib.Circuits.Circuit.ofCode: decoding, with the well-formedness checks.
• Cslib.Circuits.Program.IsCodeFrom: the lists of gates that are codes of programs.
• Cslib.Circuits.Boolean.encOp, Cslib.Circuits.Boolean.encGate, Cslib.Circuits.Boolean.encCode, Cslib.Circuits.Boolean.encCircuit: binary encodings of De Morgan circuits.

Main results

• Cslib.Circuits.Program.ofCode_code, Cslib.Circuits.Circuit.ofCode_code: decoding inverts coding.
• Cslib.Circuits.Program.code_of_ofCode_eq_some, Cslib.Circuits.Circuit.code_of_ofCode_eq_some: an accepted list is the code of the decoded circuit.
• Cslib.Circuits.Program.isSome_ofCode_iff, Cslib.Circuits.Circuit.isSome_ofCode_iff: the lists that decode.
• Cslib.Circuits.Program.IsCodeFrom.getElem, Cslib.Circuits.Program.isCodeFrom_of_getElem: elementwise characterization of Program.IsCodeFrom.
• Cslib.Circuits.Circuit.code_injective: coding is injective.
• Cslib.Circuits.Boolean.le_length_encCircuit: the encoding is at least as long as the number of inputs.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

Wire numbers

def Cslib.Circuits.Wire.equivFin (inputCount gateCount : ℕ) : Wire inputCount gateCount ≃ Fin (inputCount + gateCount)

Wires numbered inputs first: input i is i and gate j is inputCount + j, the order of Circuit.trace.

@[simp]

theorem Cslib.Circuits.Wire.equivFin_input {n k : ℕ} (i : Fin n) : (equivFin n k) (input i) = Fin.castAdd k i

@[simp]

theorem Cslib.Circuits.Wire.equivFin_gate {n k : ℕ} (j : Fin k) : (equivFin n k) (gate j) = Fin.natAdd n j

def Cslib.Circuits.Wire.toNat {n k : ℕ} (w : Wire n k) : ℕ

The number of a wire: input i is i and gate j is inputCount + j.

@[simp]

theorem Cslib.Circuits.Wire.toNat_input {n k : ℕ} (i : Fin n) : (input i).toNat = ↑i

@[simp]

theorem Cslib.Circuits.Wire.toNat_gate {n k : ℕ} (j : Fin k) : (gate j).toNat = n + ↑j

theorem Cslib.Circuits.Wire.toNat_lt {n k : ℕ} (w : Wire n k) : w.toNat < n + k

def Cslib.Circuits.Wire.ofNat {n k : ℕ} (i : ℕ) (h : i < n + k) : Wire n k

The wire with number i, for i < inputCount + gateCount.

@[simp]

theorem Cslib.Circuits.Wire.ofNat_toNat {n k : ℕ} (w : Wire n k) : ofNat w.toNat ⋯ = w

@[simp]

theorem Cslib.Circuits.Wire.toNat_ofNat {n k : ℕ} (i : ℕ) (h : i < n + k) : (ofNat i h).toNat = i

theorem Cslib.Circuits.Wire.toNat_injective {n k : ℕ} : Function.Injective toNat

@[simp]

theorem Cslib.Circuits.Wire.toNat_castSucc {n k : ℕ} (w : Wire n k) : w.castSucc.toNat = w.toNat

Lines

def Cslib.Circuits.Line.code {σ : Signature} {n k : ℕ} (line : Line σ n k) : σ.Op × List ℕ

A line as data: its operation and the numbers of the wires it reads.

@[simp]

theorem Cslib.Circuits.Line.code_fst {σ : Signature} {n k : ℕ} (line : Line σ n k) : line.code.1 = line.op

@[simp]

theorem Cslib.Circuits.Line.length_code_snd {σ : Signature} {n k : ℕ} (line : Line σ n k) : line.code.2.length = σ.Arity line.op

theorem Cslib.Circuits.Line.code_mapWires_castSucc {σ : Signature} {n k : ℕ} (line : Line σ n k) : (line.mapWires Wire.Renaming.castSucc.apply).code = line.code

def Cslib.Circuits.Line.ofCode {σ : Signature} (n k : ℕ) (g : σ.Op × List ℕ) : Option (Line σ n k)

The line performing g.1 on the wires numbered g.2, when g.2 has as many entries as the arity of g.1 and numbers only inputs and the k earlier gates.

@[simp]

theorem Cslib.Circuits.Line.ofCode_code {σ : Signature} {n k : ℕ} (line : Line σ n k) : ofCode n k line.code = some line

Decoding inverts coding.

theorem Cslib.Circuits.Line.code_of_ofCode_eq_some {σ : Signature} {n k : ℕ} {g : σ.Op × List ℕ} {line : Line σ n k} (h : ofCode n k g = some line) : line.code = g

A list accepted by decoding is the code of the decoded line.

theorem Cslib.Circuits.Line.isSome_ofCode_iff {σ : Signature} {n k : ℕ} {g : σ.Op × List ℕ} : (ofCode n k g).isSome = true ↔ g.2.length = σ.Arity g.1 ∧ ∀ i ∈ g.2, i < n + k

A line code decodes exactly when it has the arity of its operation and reads only the first n + k wires.

Programs

def Cslib.Circuits.Program.code {σ : Signature} {n k : ℕ} : Program σ n k → List (σ.Op × List ℕ)

A program as data: the codes of its lines in program order.

@[simp]

theorem Cslib.Circuits.Program.code_empty {σ : Signature} {n : ℕ} : empty.code = []

@[simp]

theorem Cslib.Circuits.Program.code_gate {σ : Signature} {n k : ℕ} (p : Program σ n k) (line : Line σ n k) : (p.gate line).code = p.code ++ [line.code]

@[simp]

theorem Cslib.Circuits.Program.length_code {σ : Signature} {n k : ℕ} (p : Program σ n k) : p.code.length = k

The code of a program lists one entry per gate.

theorem Cslib.Circuits.Program.code_eq_ofFn_lines {σ : Signature} {n k : ℕ} (p : Program σ n k) : p.code = List.ofFn fun (j : Fin k) => (p.lines j).code

The code of a program is the list of codes of its widened lines.

theorem Cslib.Circuits.Program.getD_code {σ : Signature} {n k : ℕ} (p : Program σ n k) (j : Fin k) (d : σ.Op × List ℕ) : p.code.getD (↑j) d = (p.lines j).code

Reading an existing encoded gate returns the code of its widened program line.

def Cslib.Circuits.Program.IsCodeFrom (σ : Signature) (n : ℕ) : ℕ → List (σ.Op × List ℕ) → Prop

IsCodeFrom σ n k gates: every entry of gates has the arity of its operation and reads only the n inputs and the gates before it, the first entry being gate k. Such lists, with k = 0, are exactly the codes of programs (Program.isSome_ofCode_iff).

@[instance_reducible]

instance Cslib.Circuits.Program.instDecidableIsCodeFrom {σ : Signature} {n : ℕ} (k : ℕ) (gates : List (σ.Op × List ℕ)) : Decidable (IsCodeFrom σ n k gates)

@[simp]

theorem Cslib.Circuits.Program.isCodeFrom_nil {σ : Signature} {n : ℕ} (k : ℕ) : IsCodeFrom σ n k []

@[simp]

theorem Cslib.Circuits.Program.isCodeFrom_cons {σ : Signature} {n : ℕ} (k : ℕ) (g : σ.Op × List ℕ) (gates : List (σ.Op × List ℕ)) : IsCodeFrom σ n k (g :: gates) ↔ (g.2.length = σ.Arity g.1 ∧ ∀ i ∈ g.2, i < n + k) ∧ IsCodeFrom σ n (k + 1) gates

theorem Cslib.Circuits.Program.isCodeFrom_append {σ : Signature} {n : ℕ} (k : ℕ) (gates gates' : List (σ.Op × List ℕ)) : IsCodeFrom σ n k (gates ++ gates') ↔ IsCodeFrom σ n k gates ∧ IsCodeFrom σ n (k + gates.length) gates'

theorem Cslib.Circuits.Program.IsCodeFrom.getElem {σ : Signature} {n k : ℕ} {gates : List (σ.Op × List ℕ)} (h : IsCodeFrom σ n k gates) (j : ℕ) (hj : j < gates.length) : gates[j].2.length = σ.Arity gates[j].1 ∧ ∀ i ∈ gates[j].2, i < n + k + j

In a list satisfying IsCodeFrom σ n k, entry j has the arity of its operation and reads only the first n + k + j wires.

theorem Cslib.Circuits.Program.isCodeFrom_of_getElem {σ : Signature} {n k : ℕ} {gates : List (σ.Op × List ℕ)} (h : ∀ (j : ℕ) (hj : j < gates.length), gates[j].2.length = σ.Arity gates[j].1 ∧ ∀ i ∈ gates[j].2, i < n + k + j) : IsCodeFrom σ n k gates

A list of gates satisfies IsCodeFrom σ n k when every entry j has the arity of its operation and reads only the first n + k + j wires.

def Cslib.Circuits.Program.pushCode {σ : Signature} (n : ℕ) (p : Option ((k : ℕ) × Program σ n k)) (g : σ.Op × List ℕ) : Option ((k : ℕ) × Program σ n k)

Extend a decoded program by the line with code g, when g reads only earlier wires.

def Cslib.Circuits.Program.ofCode {σ : Signature} (n : ℕ) (gates : List (σ.Op × List ℕ)) : Option ((k : ℕ) × Program σ n k)

The program on n inputs whose lines have the codes gates, when every entry is the code of a line reading only inputs and earlier gates.

@[simp]

theorem Cslib.Circuits.Program.ofCode_nil {σ : Signature} {n : ℕ} : ofCode n [] = some ⟨0, empty⟩

theorem Cslib.Circuits.Program.ofCode_append_singleton {σ : Signature} {n : ℕ} (gates : List (σ.Op × List ℕ)) (g : σ.Op × List ℕ) : ofCode n (gates ++ [g]) = pushCode n (ofCode n gates) g

@[simp]

theorem Cslib.Circuits.Program.ofCode_code {σ : Signature} {n k : ℕ} (p : Program σ n k) : ofCode n p.code = some ⟨k, p⟩

Decoding inverts coding.

theorem Cslib.Circuits.Program.code_of_ofCode_eq_some {σ : Signature} {n : ℕ} {gates : List (σ.Op × List ℕ)} {p : (k : ℕ) × Program σ n k} (h : ofCode n gates = some p) : p.snd.code = gates

A list accepted by decoding is the code of the decoded program.

theorem Cslib.Circuits.Program.isSome_ofCode_iff {σ : Signature} {n : ℕ} {gates : List (σ.Op × List ℕ)} : (ofCode n gates).isSome = true ↔ IsCodeFrom σ n 0 gates

The codes of programs: a list of gates decodes to a program exactly when every entry has the arity of its operation and reads only the inputs and the gates before it.

Circuits

def Cslib.Circuits.Circuit.code {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : List (σ.Op × List ℕ) × List ℕ

A circuit as data: the code of its program and the numbers of its output wires.

def Cslib.Circuits.Circuit.ofCode {σ : Signature} (n m : ℕ) (code : List (σ.Op × List ℕ) × List ℕ) : Option (Circuit σ n m)

The circuit on n inputs with m outputs whose program and outputs have the code code, when the program decodes and code.2 lists m wires of it.

@[simp]

theorem Cslib.Circuits.Circuit.ofCode_code {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ofCode n m c.code = some c

Decoding inverts coding.

theorem Cslib.Circuits.Circuit.code_of_ofCode_eq_some {σ : Signature} {n m : ℕ} {code : List (σ.Op × List ℕ) × List ℕ} {c : Circuit σ n m} (h : ofCode n m code = some c) : c.code = code

A code accepted by decoding is the code of the decoded circuit.

theorem Cslib.Circuits.Circuit.isSome_ofCode_iff {σ : Signature} {n m : ℕ} {code : List (σ.Op × List ℕ) × List ℕ} : (ofCode n m code).isSome = true ↔ Program.IsCodeFrom σ n 0 code.1 ∧ code.2.length = m ∧ ∀ i ∈ code.2, i < n + code.1.length

The codes of circuits: a code decodes to a circuit with m outputs exactly when its gate list is the code of a program (Program.IsCodeFrom) and it lists m output wires of that program.

theorem Cslib.Circuits.Circuit.code_injective {σ : Signature} {n m : ℕ} : Function.Injective code

Different circuits have different codes.

@[simp]

theorem Cslib.Circuits.Circuit.length_code_fst {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.code.1.length = c.size

The code of a circuit lists one entry per gate.

Encodings of De Morgan circuits

def Cslib.Circuits.Boolean.Op.toNat : Op → ℕ

The number of an operation of the De Morgan basis: 0 and 1 for the constants false and true, then 2, 3, 4 for NOT, AND, OR.

theorem Cslib.Circuits.Boolean.Op.toNat_injective : Function.Injective toNat

def Cslib.Circuits.Boolean.encOp : Op ↪ List Bool

Operations of the De Morgan basis encoded by their number Op.toNat in unary.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.encGate : Op × List ℕ ↪ List Bool

A gate as data: its operation by encOp, then the framed binary numbers of the wires it reads.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.encCode : List (Op × List ℕ) × List ℕ ↪ List Bool

The code of a circuit: its framed gates in program order, then its framed output wires, all wire numbers in binary.

def Cslib.Circuits.Boolean.encCircuit (m : ℕ) : (n : ℕ) × Circuit signature n m ↪ List Bool

Binary encoding of De Morgan circuits with m outputs and any number n of inputs: n in unary, then the code of the circuit (encCode), that is, its gates in program order and its output wires, with wire numbers in binary.

theorem Cslib.Circuits.Boolean.encCircuit_apply {m : ℕ} (c : (n : ℕ) × Circuit signature n m) : (encCircuit m) c = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encCode) (c.fst, c.snd.code)

theorem Cslib.Circuits.Boolean.le_length_encCircuit {m : ℕ} (c : (n : ℕ) × Circuit signature n m) : c.fst ≤ ((encCircuit m) c).length

The encoding of a circuit is at least as long as its number of inputs.