Circuit composition -- definitions

Serial composition materializes the K output gates of an inner N → K circuit as internal wires, then rewires every input of an outer K → M circuit to those wires. If the two circuits have G₁ and G₂ internal gates, the composite has exactly G₁ + K + G₂ internal gates. Consequently its library size is the sum of the two source sizes.

def Complexity.Gate.rewire {B : Basis} {W W' : ℕ} (gate : Gate B W) (mapWire : Fin W → Fin W') : Gate B W'

Reindex every input wire of a gate, preserving its operation, arity, and per-edge negation flags.

Equations

• gate.rewire mapWire = { op := gate.op, fanIn := gate.fanIn, arityOk := ⋯, inputs := fun (input : Fin gate.fanIn) => mapWire (gate.inputs input), negated := gate.negated }

def Complexity.Circuit.embedInnerWire {N K G₁ G₂ : ℕ} (wire : Fin (N + G₁)) : Fin (N + (G₁ + K + G₂))

Embed an inner-circuit wire into the initial region of the composite.

Equations

• Complexity.Circuit.embedInnerWire wire = ⟨↑wire, ⋯⟩

def Complexity.Circuit.embedInnerOutput {N K G₁ G₂ : ℕ} (output : Fin K) : Fin (N + (G₁ + K + G₂))

The composite wire driven by one materialized inner output gate.

Equations

• Complexity.Circuit.embedInnerOutput output = ⟨N + G₁ + ↑output, ⋯⟩

def Complexity.Circuit.embedOuterWire {N K G₁ G₂ : ℕ} (wire : Fin (K + G₂)) : Fin (N + (G₁ + K + G₂))

Embed an outer-circuit wire into the composite. Outer primary inputs map to the materialized inner outputs; outer internal wires map after that block.

Equations

• Complexity.Circuit.embedOuterWire wire = if hinput : ↑wire < K then ⟨N + G₁ + ↑wire, ⋯⟩ else ⟨N + G₁ + K + (↑wire - K), ⋯⟩

def Complexity.Circuit.composeGate {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (index : Fin (G₁ + K + G₂)) : { gate : Gate B (N + (G₁ + K + G₂)) // ∀ (input : Fin gate.fanIn), ↑(gate.inputs input) < N + ↑index }

The gate at one flat index of a serially composed circuit, bundled with its acyclicity proof.

Equations

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

def Complexity.Circuit.compose {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) : Circuit B N M (G₁ + K + G₂)

Serially compose outer : K → M after inner : N → K.

The K output gates of inner become internal gates so that they can feed arbitrarily many gates of outer without duplicating computation.

Equations

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