Resource-accounted circuit composition

This module exposes serial composition of two circuits over the same basis. The construction shares every inner output and therefore has exact additive size, rather than duplicating the inner circuit once per outer use.

Main results

• Circuit.eval_compose -- exact functional composition.
• Circuit.size_compose -- exact additive size.
• Circuit.depth_compose_le -- depth is at most the sum of source depths.
• Circuit.eval_parallel -- parallel composition appends output tuples.
• Circuit.size_parallel -- parallel composition also has exact additive size.

theorem Complexity.Gate.eval_rewire {B : Basis} {W W' : ℕ} (gate : Gate B W) (mapWire : Fin W → Fin W') (wireValue : BitString W') : (gate.rewire mapWire).eval wireValue = gate.eval fun (wire : Fin W) => wireValue (mapWire wire)

Rewiring a gate composes its wire-value assignment with the wire map.

theorem Complexity.Circuit.wireValue_compose_inner {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₁) (input : BitString N) (wire : Fin (N + G₁)) : (outer.compose inner).wireValue input (embedInnerWire wire) = inner.wireValue input wire

Composition preserves each original inner wire value.

theorem Complexity.Circuit.wireValue_compose_innerOutput {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₁) (input : BitString N) (output : Fin K) : (outer.compose inner).wireValue input (embedInnerOutput output) = inner.eval input output

A materialized inner-output wire carries the corresponding inner result.

theorem Complexity.Circuit.wireValue_compose_outer {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₁) (input : BitString N) (wire : Fin (K + G₂)) : (outer.compose inner).wireValue input (embedOuterWire wire) = outer.wireValue (inner.eval input) wire

Composition preserves outer wire semantics after feeding the inner circuit's result to the outer circuit.

theorem Complexity.Circuit.wireDepth_compose_inner {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₁) (wire : Fin (N + G₁)) : (outer.compose inner).wireDepth (embedInnerWire wire) = inner.wireDepth wire

Composition preserves the depth of every original inner wire.

theorem Complexity.Circuit.wireDepth_compose_innerOutput {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₁) (output : Fin K) : (outer.compose inner).wireDepth (embedInnerOutput output) = inner.outputDepth output

A materialized inner output has exactly its original output depth.

theorem Complexity.Circuit.wireDepth_compose_outer_le {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₁) (wire : Fin (K + G₂)) : (outer.compose inner).wireDepth (embedOuterWire wire) ≤ inner.depth + outer.wireDepth wire

Every embedded outer wire has depth at most the inner circuit depth plus its original outer-circuit wire depth.

@[simp]

theorem Complexity.Circuit.eval_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₁) (input : BitString N) : (outer.compose inner).eval input = outer.eval (inner.eval input)

Serial circuit composition agrees exactly with function composition.

@[simp]

theorem Complexity.Circuit.size_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₁) : (outer.compose inner).size = inner.size + outer.size

Serial composition has exactly additive size under the library convention. The K inner output gates become internal gates, so no output gate is lost or double-counted.

theorem Complexity.Circuit.depth_compose_le {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₁) : (outer.compose inner).depth ≤ inner.depth + outer.depth

Serial composition adds at most the two source depths.

Parallel composition

theorem Complexity.Circuit.wireValue_parallel_left {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) (input : BitString N) (wire : Fin (N + G₁)) : (left.parallel right).wireValue input (embedParallelLeftWire wire) = left.wireValue input wire

Parallel composition preserves every left-component wire value.

theorem Complexity.Circuit.wireValue_parallel_right {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) (input : BitString N) (wire : Fin (N + G₂)) : (left.parallel right).wireValue input (embedParallelRightWire wire) = right.wireValue input wire

Parallel composition preserves every right-component wire value after shifting its internal-gate block past the left component.

@[simp]

theorem Complexity.Circuit.eval_parallel {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) (input : BitString N) : (left.parallel right).eval input = Fin.append (left.eval input) (right.eval input)

Parallel circuit composition appends the two source output tuples.

@[simp]

theorem Complexity.Circuit.size_parallel {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) : (left.parallel right).size = left.size + right.size

Parallel composition has exactly additive size: it shares primary inputs and otherwise preserves every internal and output gate.

theorem Complexity.Circuit.exists_parallelFamily {B : Basis} {N : ℕ} [NeZero N] {count : ℕ} [NeZero count] (circuits : Fin count → (internalGates : ℕ) × Circuit B N 1 internalGates) : ∃ (internalGates : ℕ) (packed : Circuit B N count internalGates), packed.size = ∑ i : Fin count, (circuits i).snd.size ∧ ∀ (input : BitString N) (i : Fin count), packed.eval input i = (circuits i).snd.eval input 0

Any positive finite family of single-output circuits with shared primary inputs can be packed into one multi-output circuit. Its size is exactly the sum of the source sizes, and output i is the output of source circuit i.