Explicit encoded size of compiled Boolean circuits

For a circuit with n inputs, s stored gates, m designated outputs and output depth d, write W = n + 3 * s and B = log₂ W + 1. The actual compiled schedule and output selectors have at most

4 * d * (2 * W * (6 * B + 21) + 1) + m * (2 * B + 1) + 1

bits. This includes all node tags, binary references, pair framing, layer framing and repeated selectors. Unused gates contribute to the working width, but only the designated-output depth controls the number of layers. When d = 0, the schedule contributes no nodes or layers.

Main results

• Cslib.Circuits.Boolean.Layered.length_encCompiled_compile_le: the explicit binary size bound.

References

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

theorem Cslib.Circuits.Boolean.Layered.length_encCompiled_compile_le {n m : ℕ} (c : Circuit signature n m) : have width := n + 3 * c.size; have bits := width.log2 + 1; (encCompiled (compile n c.code)).length ≤ 4 * c.depth * (2 * width * (6 * bits + 21) + 1) + m * (2 * bits + 1) + 1

The full compiled artifact has size linear in the number of emitted nodes and selectors, times a logarithmic reference bound. All tags and framing are included.