Correctness of depth-bounded Boolean circuit compilation

After the two microlevels for depth k, every original wire of depth at most k is available at its original position and has its original value. Deeper gates may remain placeholders. This invariant covers unused gates and the input-only initial row.

Main results

• Cslib.Circuits.Boolean.Layered.getD_eval_schedule: every ready wire has its original value.
• Cslib.Circuits.Boolean.Layered.wellFormed_compile: every scheduled reference is valid.
• Cslib.Circuits.Boolean.Layered.outputs_valid_compile: output indices address the final row.
• Cslib.Circuits.Boolean.Layered.select_eval_compile: the ordered outputs equal the original circuit evaluation, including depth-zero wiring and repeated outputs.

theorem Cslib.Circuits.Boolean.Layered.length_eval_schedule (inputs : List Bool) (inputCount : ℕ) (gates : List (Op × List ℕ)) (depths : List ℕ) (k : ℕ) : (eval inputs (schedule inputCount gates depths (k + 1))).length = inputCount + 3 * gates.length

Once a positive number of rounds has run, the row has the full working width.

theorem Cslib.Circuits.Boolean.Layered.toNat_lt_length_eval_schedule {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (k : ℕ) (w : Wire n g) (hw : p.wireDepths w ≤ k) : w.toNat < (eval (List.ofFn x) (schedule n p.code (wireDepthsCode n p.code) k)).length

Every original wire of depth at most the completed level is available at its original index.

theorem Cslib.Circuits.Boolean.Layered.getD_eval_schedule {n g : ℕ} (p : Program signature n g) (x : Fin n → Bool) (k : ℕ) (w : Wire n g) (hw : p.wireDepths w ≤ k) : (eval (List.ofFn x) (schedule n p.code (wireDepthsCode n p.code) k)).getD w.toNat false = p.trace interpretation x w

The schedule preserves each completed original wire's value; deeper unused gates need not have been computed.

theorem Cslib.Circuits.Boolean.Layered.wellFormed_compile {n m : ℕ} (c : Circuit signature n m) : WellFormed n (compile n c.code).1

The actual compiler produces a well-formed layered schedule for every typed circuit.

theorem Cslib.Circuits.Boolean.Layered.outputs_valid_compile {n m : ℕ} (c : Circuit signature n m) (i : ℕ) : i ∈ (compile n c.code).2 → i < outputWidth n (compile n c.code).1

All designated outputs select existing final wires. This also covers an empty schedule with dead gates, whose available final wires are only the original inputs.

theorem Cslib.Circuits.Boolean.Layered.select_eval_compile {n m : ℕ} (c : Circuit signature n m) (x : Fin n → Bool) : select (eval (List.ofFn x) (compile n c.code).1) (compile n c.code).2 = List.ofFn (c.eval interpretation x)

Compilation preserves every output's Boolean value, in order and with repetitions.