Typed Boolean circuits

This file defines the library's typed Boolean circuits. A Circuit B N M G is a circuit over the basis B with N primary inputs, M output gates, and G internal gates; its wiring makes it acyclic by construction. The file also defines evaluation, depth, the size measure G + M, and complete bases.

Main definitions

• Gate — a gate over a basis, with a free negation flag on each input
• Circuit — an acyclic Boolean circuit (well-formedness by construction)
• Circuit.wireValue, Circuit.eval — evaluation of wires and outputs
• Circuit.wireDepth — depth of a wire in the circuit DAG
• Circuit.outputDepth — depth of a single output gate
• Circuit.depth — depth of a (possibly multi-output) circuit
• Circuit.size — the number of internal and output gates
• CompleteBasis — typeclass for functionally complete bases

Main results

• CompleteBasis.of_simulation — completeness transfers to any basis that can simulate the circuits of a complete basis

structure Complexity.Gate (B : Basis) (W : ℕ) : Type

A gate in a circuit over basis B with W wires available as inputs. The gate's fan-in must satisfy the arity constraint of its operation, and each input is wired to one of the W available wires.

• op : B.Op

  The basis operation this gate computes.

• fanIn : ℕ

  The number of inputs this gate reads.

• arityOk : (B.arity self.op).satisfiedBy self.fanIn

  Proof that fanIn satisfies the arity constraint of op.

• inputs : Fin self.fanIn → Fin W

  The wire each of the gate's fanIn inputs is connected to.

• negated : Fin self.fanIn → Bool

  Per-input negation flag. Negations are free under this library's size convention.

def Complexity.Gate.eval {B : Basis} {W : ℕ} (g : Gate B W) (wireVal : BitString W) : Bool

Evaluate a gate given a wire-value assignment.

Equations

• g.eval wireVal = B.eval g.op g.fanIn ⋯ fun (i : Fin g.fanIn) => g.negated i ^^ wireVal (g.inputs i)

structure Complexity.Circuit (B : Basis) (N M G : ℕ) [NeZero N] [NeZero M] : Type

A Boolean circuit over basis B with N inputs, M outputs, and G internal gates.

All gates reference wires from Fin (N + G). The acyclic field ensures that internal gate i only reads wires 0, …, N + i − 1, preventing cycles.

• gates : Fin G → Gate B (N + G)

  The internal gates; gate i drives wire N + i.

• outputs : Fin M → Gate B (N + G)

  The output gates; output bit j is the value of gate outputs j.

• acyclic (i : Fin G) (k : Fin (self.gates i).fanIn) : ↑((self.gates i).inputs k) < N + ↑i

  Acyclicity: internal gate i only reads wires 0, …, N + i − 1.

@[irreducible]

def Complexity.Circuit.wireValue {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) (w : Fin (N + G)) : Bool

Value of wire w when the circuit is fed input.

The first N wires carry the primary inputs. Wire N + i carries the output of internal gate i.

Equations

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

theorem Complexity.Circuit.wireValue_of_lt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) (w : Fin (N + G)) (h : ↑w < N) : c.wireValue input w = input ⟨↑w, h⟩

On primary input wires (index < N), wireValue is the corresponding input bit.

theorem Complexity.Circuit.wireValue_of_not_lt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) (w : Fin (N + G)) (h : ¬↑w < N) : c.wireValue input w = (c.gates ⟨↑w - N, ⋯⟩).eval (c.wireValue input)

On internal gate wires (index ≥ N), wireValue is the evaluation of gate w − N on the values of its input wires.

@[irreducible]

def Complexity.Circuit.wireDepth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (w : Fin (N + G)) : ℕ

Depth of wire w in the circuit DAG.

Primary inputs have depth 0. Wire N + i (internal gate i) has depth 1 + max over input wires.

Equations

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

@[simp]

theorem Complexity.Circuit.wireDepth_of_lt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (w : Fin (N + G)) (h : ↑w < N) : c.wireDepth w = 0

Primary input wires (index < N) have depth 0.

theorem Complexity.Circuit.wireDepth_of_not_lt {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (w : Fin (N + G)) (h : ¬↑w < N) : c.wireDepth w = 1 + Fin.foldl (c.gates ⟨↑w - N, ⋯⟩).fanIn (fun (acc : ℕ) (k : Fin (c.gates ⟨↑w - N, ⋯⟩).fanIn) => max acc (c.wireDepth ((c.gates ⟨↑w - N, ⋯⟩).inputs k))) 0

Internal gate wires (index ≥ N) have depth 1 + max over their input wires. Unfolds one step of wireDepth for the gate case.

def Complexity.Circuit.outputDepth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (j : Fin M) : ℕ

Depth contributed by a single output gate: one layer for the gate itself plus the maximum wireDepth of its inputs. Always ≥ 1.

Equations

• c.outputDepth j = 1 + Fin.foldl (c.outputs j).fanIn (fun (acc : ℕ) (k : Fin (c.outputs j).fanIn) => max acc (c.wireDepth ((c.outputs j).inputs k))) 0

def Complexity.Circuit.depth {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : ℕ

Depth of a circuit: the maximum outputDepth over all output gates.

Equations

• c.depth = Fin.foldl M (fun (acc : ℕ) (j : Fin M) => max acc (c.outputDepth j)) 0

def Complexity.Circuit.eval {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) (input : BitString N) : BitString M

Evaluate a circuit: map an N-bit input to an M-bit output.

Equations

• c.eval input j = (c.outputs j).eval (c.wireValue input)

def Complexity.Circuit.size {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] : Circuit B N M G → ℕ

The library's circuit size: internal gates plus output gates.

Primary input vertices are not counted, and the negation flags on gate inputs have zero cost. Some texts instead count input vertices and explicit NOT gates; those conventions agree only up to additive/linear overhead, not on exact size bounds.

Equations

• x✝.size = G + M

class Complexity.CompleteBasis (B : Basis) : Prop

A basis is complete if every Boolean function can be computed by some circuit over it.

• complete {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) : ∃ (G : ℕ), ∃ (c : Circuit B N M G), c.eval = f

  Every function BitString N → BitString M is the evaluation of some circuit over B.

theorem Complexity.CompleteBasis.of_simulation (B₁ B₂ : Basis) [CompleteBasis B₁] (sim : ∀ {N M G : ℕ} [inst : NeZero N] [inst_1 : NeZero M] (c : Circuit B₁ N M G), ∃ (G' : ℕ), ∃ (c' : Circuit B₂ N M G'), c'.eval = c.eval) : CompleteBasis B₂

If every circuit over B₁ can be simulated by a circuit over B₂ (possibly with a different number of internal gates), then completeness of B₁ implies completeness of B₂.

This is the generic tool for proving new bases complete: show you can compile each gate of a known-complete basis into a subcircuit of the new basis.