CSLib formula normalization preserves values, depths, and size bounds

The adapter preserves every program wire's evaluation and depth. The existing typed wire normalizer therefore gives the same bounds for CSLib's selected output wire.

theorem Complexity.CslibAC0.wireValue_asTyped {n g : ℕ} [NeZero n] (p : Cslib.Circuits.Program Basis.unboundedAndOr.signature n g) (x : BitString n) (w : Cslib.Circuits.Wire n g) : (asTyped p).wireValue x w.index = p.trace Basis.unboundedAndOr.interpretation x w

theorem Complexity.CslibAC0.wireDepth_asTyped {n g : ℕ} [NeZero n] (p : Cslib.Circuits.Program Basis.unboundedAndOr.signature n g) (w : Cslib.Circuits.Wire n g) : (asTyped p).wireDepth w.index = p.wireDepths w

theorem Complexity.CslibAC0.outputFormula_spec_proof {n : ℕ} [NeZero n] (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1) : (∀ (x : BitString n), AC0Formula.eval x (outputFormula c) = c.eval Basis.unboundedAndOr.interpretation x 0) ∧ (outputFormula c).depth ≤ c.depth ∧ (outputFormula c).size ≤ (2 * (n + c.size) + 1) ^ (c.depth + 1)