Typed circuits reconstructed from raw circuit syntax

This module exposes the reverse direction of the canonical fan-in-two circuit encoding bridge. A valid raw circuit at positive input arity becomes a typed Circuit Basis.andOr2; reconstruction preserves its ordered raw syntax, Boolean evaluation, and exact gate count.

Main definitions

• CircuitCode.RawGate.toGate: restore a raw gate's dependent wire bounds.
• CircuitCode.RawCircuit.toCircuit: restore a valid raw circuit's dependent circuit type.

Main results

• RawCircuit.ofCircuit_toCircuit: reconstruction is a right inverse to erasure.
• RawCircuit.eval?_toCircuit: iterative raw and typed evaluation agree.
• RawCircuit.size_toCircuit: typed size equals the raw gate count.

theorem Complexity.CircuitCode.RawCircuit.ofCircuit_toCircuit (N : ℕ) [NeZero N] (circuit : RawCircuit) (hwell : WellFormed N circuit) : ofCircuit (toCircuit N circuit hwell) = circuit

Re-erasing a reconstructed typed circuit returns the original raw circuit.

theorem Complexity.CircuitCode.RawCircuit.eval?_toCircuit (N : ℕ) [NeZero N] (circuit : RawCircuit) (hwell : WellFormed N circuit) (input : BitString N) : circuit.eval? input.toList = some ((toCircuit N circuit hwell).eval input 0)

Raw iterative evaluation agrees with the reconstructed typed circuit.

theorem Complexity.CircuitCode.RawCircuit.size_toCircuit (N : ℕ) [NeZero N] (circuit : RawCircuit) (hwell : WellFormed N circuit) : (toCircuit N circuit hwell).size = List.length circuit

Reconstructed typed size is exactly the raw gate count.