Reconstructing typed circuits from raw circuit syntax

This definitions layer packages a nonempty, topologically ordered CircuitCode.RawCircuit as a typed fan-in-two AND/OR circuit. The final raw gate becomes the sole output gate; every preceding raw gate becomes an internal gate in the same order.

def Complexity.CircuitCode.RawGate.toGate {W : ℕ} (gate : RawGate) (hwell : gate.WellFormedAt W) : Gate Basis.andOr2 W

Restore the dependent wire bounds of a well-formed raw gate.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.RawCircuit.toCircuit (N : ℕ) [NeZero N] (circuit : RawCircuit) (hwell : WellFormed N circuit) : Circuit Basis.andOr2 N 1 (List.length circuit - 1)

Restore the dependent type of a valid raw single-output circuit.

The circuit has one typed gate for each raw gate: the first length - 1 are internal gates and the final gate is the sole output gate.

Equations

• One or more equations did not get rendered due to their size.