Compiling shared Boolean circuits into consecutive layers

Each original depth uses a preparation layer and a finishing layer. Original input and gate values retain their wire numbers. Two further slots per gate hold NAND intermediates, including the two negated operands of OR. Copies carry earlier values between levels. The first layer creates the working slots directly from the original inputs; it requires no padding layer.

Output selection is separate wiring, so an empty schedule preserves depth-zero circuits.

Main definitions

• Cslib.Circuits.Boolean.Layered.prepareLayer: prepare one depth's NAND intermediates.
• Cslib.Circuits.Boolean.Layered.finishLayer: finish gates at that depth and carry older wires.
• Cslib.Circuits.Boolean.Layered.schedule: two consecutive layers per original depth.
• Cslib.Circuits.Boolean.Layered.compile: compute depths, schedule layers, and retain outputs.
• Cslib.Circuits.Boolean.Layered.encCompiled: encode the layers and binary output indices.

Main results

• Cslib.Circuits.Boolean.Layered.length_compile: exactly twice the designated-output depth.

Compile.Correctness proves well-formedness and semantic preservation. Compile.Size bounds the complete encoded result; Compile.PolyTime certifies the actual compiler on all raw codes.

References

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

def Cslib.Circuits.Boolean.Layered.carry (depths : List ℕ) (level wire : ℕ) : Node

Carry an already computed main wire; unused slots contain a constant placeholder.

def Cslib.Circuits.Boolean.Layered.prepareFirst (gate : Op × List ℕ) : Node

The first NAND intermediate, or the value itself for a constant gate.

def Cslib.Circuits.Boolean.Layered.prepareSecond (gate : Op × List ℕ) : Node

OR needs a second negated operand; the other operations need only one intermediate.

def Cslib.Circuits.Boolean.Layered.finish (inputCount gateCount gateIndex : ℕ) : Op → Node

Finish a gate using the two scratch positions allocated after all main wires.

def Cslib.Circuits.Boolean.Layered.prepareLayer (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) : List Node

Keep completed main wires and prepare the active depth in two scratch blocks.

def Cslib.Circuits.Boolean.Layered.finishLayer (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) : List Node

Update the active main slots, retain earlier values, and clear the scratch blocks.

def Cslib.Circuits.Boolean.Layered.schedule (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (depth : ℕ) : List (List Node)

Generate both microlevels at each depth, retaining shared wire slots.

def Cslib.Circuits.Boolean.Layered.compile (inputCount : ℕ) (code : List (Op × List ℕ) × List ℕ) : List (List Node) × List ℕ

Compile raw De Morgan code, retaining its designated outputs as free final wiring. Depths are computed from the code, not supplied as extra input. Malformed codes have total fallback behavior; semantic agreement is specified for well-formed circuits.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Layered.encCompiled : List (List Node) × List ℕ ↪ List Bool

Encode the complete schedule and all binary output selectors.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.compile_outputs (inputCount : ℕ) (code : List (Op × List ℕ) × List ℕ) : (compile inputCount code).2 = code.2

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_prepareLayer (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) : (prepareLayer inputCount gates depths level).length = inputCount + 3 * gates.length

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_finishLayer (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) : (finishLayer inputCount gates depths level).length = inputCount + 3 * gates.length

@[simp]

theorem Cslib.Circuits.Boolean.Layered.schedule_zero (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) : schedule inputCount gates depths 0 = []

theorem Cslib.Circuits.Boolean.Layered.schedule_succ (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (depth : ℕ) : schedule inputCount gates depths (depth + 1) = schedule inputCount gates depths depth ++ [prepareLayer inputCount gates depths (depth + 1), finishLayer inputCount gates depths (depth + 1)]

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_schedule (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (depth : ℕ) : (schedule inputCount gates depths depth).length = 2 * depth

The schedule uses two layers per source depth, irrespective of the number of stored gates.

theorem Cslib.Circuits.Boolean.Layered.length_of_mem_schedule (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (depth : ℕ) {layer : List Node} (h : layer ∈ schedule inputCount gates depths depth) : layer.length = inputCount + 3 * gates.length

Every scheduled layer has the same working width. The empty schedule still has input width.

theorem Cslib.Circuits.Boolean.Layered.getD_eval_prepareLayer_main (inputs : List Bool) (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) {i : ℕ} (hi : i < inputCount + gates.length) : (evalLayer inputs (prepareLayer inputCount gates depths level)).getD i false = Node.eval inputs (carry depths level i)

The preparation layer carries exactly the completed main slots.

theorem Cslib.Circuits.Boolean.Layered.getD_eval_prepareLayer_first (inputs : List Bool) (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) {j : ℕ} (hj : j < gates.length) (hlevel : depths.getD (inputCount + j) 0 = level) : (evalLayer inputs (prepareLayer inputCount gates depths level)).getD (inputCount + gates.length + j) false = Node.eval inputs (prepareFirst (gates.getD j (Op.const false, [])))

The first scratch block stores the first intermediate for an active gate.

theorem Cslib.Circuits.Boolean.Layered.getD_eval_prepareLayer_second (inputs : List Bool) (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) {j : ℕ} (hj : j < gates.length) (hlevel : depths.getD (inputCount + j) 0 = level) : (evalLayer inputs (prepareLayer inputCount gates depths level)).getD (inputCount + 2 * gates.length + j) false = Node.eval inputs (prepareSecond (gates.getD j (Op.const false, [])))

The second scratch block stores OR's second negated operand.

theorem Cslib.Circuits.Boolean.Layered.getD_eval_finishLayer_input (inputs : List Bool) (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) {i : ℕ} (hi : i < inputCount) : (evalLayer inputs (finishLayer inputCount gates depths level)).getD i false = inputs.getD i false

Input wires are copied through the finishing layer.

theorem Cslib.Circuits.Boolean.Layered.getD_eval_finishLayer_gate (inputs : List Bool) (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) {j : ℕ} (hj : j < gates.length) : (evalLayer inputs (finishLayer inputCount gates depths level)).getD (inputCount + j) false = Node.eval inputs (if depths.getD (inputCount + j) 0 = level then finish inputCount gates.length j (gates.getD j (Op.const false, [])).1 else carry depths level (inputCount + j))

A main gate slot is either finished at this level or carried from an earlier one.

theorem Cslib.Circuits.Boolean.Layered.finish_prepare_eq {n g : ℕ} (inputs : List Bool) (gates : List (Op × List ℕ)) (depths : List ℕ) (level : ℕ) {j : ℕ} (hj : j < gates.length) (line : Line signature n g) (hgate : gates.getD j (Op.const false, []) = line.code) (hlevel : depths.getD (n + j) 0 = level) : Node.eval (evalLayer inputs (prepareLayer n gates depths level)) (finish n gates.length j line.op) = interpretation line.op fun (a : Fin (signature.Arity line.op)) => inputs.getD (line.wires a).toNat false

The two microlevels compute one De Morgan operation from its original wire values.

@[simp]

theorem Cslib.Circuits.Boolean.Layered.length_compile {n m : ℕ} (c : Circuit signature n m) : (compile n c.code).1.length = 2 * c.depth

Compiling a typed circuit uses exactly twice its designated-output depth. Dead gates do not extend the schedule.