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.

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.