Internal: Typed Circuits as Circuit Descriptors

This internal module connects the typed Circuit model over Basis.andOr2 to the fixed-size CircDesc counting model. It contains only the encoding, its orderedness proof, and its semantic-correctness proof, so clients that need this bridge do not also acquire the lower-bound and padding machinery from Internal.Bridge.

Encoding

def Complexity.encodeGate {W W' : ℕ} (g : Gate Basis.andOr2 W) (hW : W ≤ W') : GateSlot W'

Encode a Basis.andOr2 gate as a GateSlot.

Equations

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

def Complexity.circuitToDesc {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : CircDesc N (G + 1)

Encode a circuit over Basis.andOr2 as a circuit descriptor. Internal gates map to positions 0..G-1; the output gate to position G.

Equations

• Complexity.circuitToDesc c i = if h : ↑i < G then Complexity.encodeGate (c.gates ⟨↑i, h⟩) ⋯ else Complexity.encodeGate (c.outputs 0) ⋯

theorem Complexity.circuitToDesc_ordered {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : (circuitToDesc c).Ordered

Descriptors obtained from typed circuits only refer to primary inputs or strictly earlier gates.

Semantic Equivalence

theorem Complexity.wireValue_eq_wireVal {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (input : BitString N) (w : Fin (N + G)) : c.wireValue input w = (circuitToDesc c).wireVal input ⟨↑w, ⋯⟩

Wire values agree between Circuit.wireValue and wireVal for wires in the range 0..N+G-1.

theorem Complexity.circuit_eval_eq_eval {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : (fun (x : BitString N) => c.eval x 0) = CircDesc.eval ⋯ (circuitToDesc c)

Circuit evaluation agrees with descriptor evaluation.