Internal correctness of raw-to-typed circuit reconstruction

This proof layer shows that restoring dependent wire bounds and then erasing them is an exact round trip. Semantic correctness is consequently inherited from the existing typed-to-raw evaluator theorem rather than reproved.

@[simp]

theorem Complexity.CircuitCode.RawGate.ofGate_toGate_internal {W : ℕ} (gate : RawGate) (hwell : gate.WellFormedAt W) : ofGate (gate.toGate hwell) = gate

Restoring and then erasing a well-formed raw gate is the identity.

theorem Complexity.CircuitCode.RawCircuit.ofCircuit_toCircuit_internal (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 list exactly, including its gate order and designated final output gate.

theorem Complexity.CircuitCode.RawCircuit.eval?_toCircuit_internal (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 exactly with evaluation of the reconstructed typed circuit.

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

Reconstruction preserves the raw gate count under the library's circuit size convention, which counts internal and output gates.