Bounding the complete binary encoding of a circuit

A circuit's typed wires bound every binary reference by its input and gate counts. This gives a polynomial bound on its complete serialized code, including gate tags, outputs and framing. It is useful for certifying circuit-construction loops whose intermediate circuits have bounded size, without making a claim about the complexity of the functions those circuits compute.

Main results

• Cslib.Circuits.Boolean.length_encCode_le: a bound in the input, output and gate counts.

theorem Cslib.Circuits.Boolean.length_encCode_le {n m : ℕ} (c : Circuit signature n m) : (encCode c.code).length ≤ 2 * c.size * (23 + 8 * (n + c.size)) + 1 + m * (2 * (n + c.size) + 1)

The full code of a typed De Morgan circuit has polynomially bounded encoded length.