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.equivFin, 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.pushCode, 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.Circuit.encGate, Cslib.Circuits.Circuit.encCode, Cslib.Circuits.Circuit.encCircuit: binary encodings of circuits over an arbitrary signature given an operation encoding.
• Cslib.Circuits.Boolean.Op.toNat, 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.Circuit.code_wiring, Cslib.Circuits.Circuit.code_wiring_eq_map, Cslib.Circuits.Circuit.code_wiring_id: serialized codes of pure wirings.
• Cslib.Circuits.Circuit.le_length_encCircuit, Cslib.Circuits.Circuit.size_le_length_encCircuit, Cslib.Circuits.Boolean.le_length_encCircuit: the encoding is at least as long as the number of inputs and the gate count.

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

Input wire i maps to Fin.castAdd k i under equivFin.

@[simp]

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

Gate wire j maps to Fin.natAdd n j under equivFin.

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

Input wire i has wire number i.

@[simp]

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

Gate wire j has wire number n + j.

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

Every wire in a circuit with n inputs and k gates has wire number strictly less than 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

Decoding the wire number of w recovers w.

@[simp]

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

The wire number of ofNat i h is i.

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

Wire numbering toNat is injective.

@[simp]

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

Widening a wire by castSucc preserves its wire number.

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

The first component of a line's code is its operation.

@[simp]

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

The wire list in a line's code has length equal to the arity of its operation.

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

Widening the wires of a line by castSucc leaves its code unchanged.

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 = []

The code of the empty program is the empty list.

@[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]

Appending a gate appends its line code to the program's 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)

IsCodeFrom σ n k gates is decidable.

@[simp]

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

The empty gate list satisfies IsCodeFrom σ n k for every starting gate index 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

g :: gates satisfies IsCodeFrom σ n k iff g is a valid line at index k and gates satisfies IsCodeFrom σ n (k + 1).

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'

A concatenation gates ++ gates' satisfies IsCodeFrom σ n k iff gates satisfies IsCodeFrom σ n k and gates' satisfies IsCodeFrom σ n (k + gates.length).

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⟩

Decoding the empty gate list yields the empty program.

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

Decoding gates ++ [g] is equivalent to decoding gates and then pushing 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.

Wiring serialization

theorem Cslib.Circuits.Circuit.code_wiring {σ : Signature} {n m : ℕ} (f : Fin m → Fin n) : (wiring σ f).code = ([], List.ofFn fun (j : Fin m) => ↑(f j))

The serialized code of a pure wiring Circuit.wiring σ f has no gate lines and output wire indices (f j).val.

theorem Cslib.Circuits.Circuit.code_wiring_eq_map {σ : Signature} {n m : ℕ} {f : Fin m → Fin n} {g : ℕ → ℕ} (h : ∀ (j : Fin m), ↑(f j) = g ↑j) : (wiring σ f).code = ([], List.map g (List.range m))

When (f j).val = g j.val for every output wire j, the serialized output list of Circuit.wiring σ f is (List.range m).map g.

@[simp]

theorem Cslib.Circuits.Circuit.code_wiring_id {σ : Signature} {n : ℕ} : (wiring σ _root_.id).code = ([], List.range n)

The serialized code of the identity wiring on n wires is ([], List.range n).

Binary encodings of circuits over an arbitrary signature

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.encGate {Op : Type} (encOp : Op ↪ List Bool) : Op × List ℕ ↪ List Bool

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

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.encCode {Op : Type} (encOp : Op ↪ List Bool) : List (Op × List ℕ) × List ℕ ↪ List Bool

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

def Cslib.Circuits.Circuit.encCircuit {σ : Signature} (encOp : σ.Op ↪ List Bool) (m : ℕ) : (n : ℕ) × Circuit σ n m ↪ List Bool

Binary encoding of circuits with m outputs over an arbitrary signature σ equipped with encOp : σ.Op ↪ List Bool: the input count n in unary, followed by the code of the circuit (encCode encOp).

theorem Cslib.Circuits.Circuit.encCircuit_apply {m : ℕ} {σ : Signature} (encOp : σ.Op ↪ List Bool) (c : (n : ℕ) × Circuit σ n m) : (encCircuit encOp m) c = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (encCode encOp)) (c.fst, c.snd.code)

Unfolding formula for encCircuit encOp m c.

theorem Cslib.Circuits.Circuit.le_length_encCircuit {m : ℕ} {σ : Signature} (encOp : σ.Op ↪ List Bool) (c : (n : ℕ) × Circuit σ n m) : c.fst ≤ ((encCircuit encOp m) c).length

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

theorem Cslib.Circuits.Circuit.size_le_length_encCircuit {m : ℕ} {σ : Signature} (encOp : σ.Op ↪ List Bool) (c : (n : ℕ) × Circuit σ n m) : c.snd.size ≤ ((encCircuit encOp m) c).length

The encoding of a circuit is at least as long as its gate count c.2.size.

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

The numbering Op.toNat of De Morgan operations is injective.

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 of the De Morgan basis 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 De Morgan circuit: its framed gates in program order, then its framed output wires, all wire numbers in binary.

@[reducible, inline]

abbrev 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)

Unfolding formula for encCircuit m c.

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.