Hardwiring Prefixes of Circuit Inputs

Fix a prefix of a fan-in-two AND/OR circuit's inputs without changing its gate count. This is the circuit-level operation used to turn length-dependent advice or random seeds into nonuniform constants while leaving the ordinary input live.

The live suffix and output tuple have positive arity, matching the typed Circuit convention. Circuit families represent the zero-input member separately with emptyOutput.

Main definitions

• Circuit.castInputArity: transport a circuit across equal input arities.
• Circuit.restrictPrefix: hardwire the first k inputs to a fixed bit string.

Main results

• Circuit.restrictPrefix_eval: evaluation agrees with supplying seed ++ input.
• Circuit.restrictPrefix_size: hardwiring preserves the exact circuit size.

def Complexity.Circuit.castInputArity {B : Basis} {N N' M G : ℕ} [NeZero N] [NeZero N'] [NeZero M] (h : N = N') (circuit : Circuit B N M G) : Circuit B N' M G

Transport a circuit across an equality of input arities.

Equations

• Complexity.Circuit.castInputArity h circuit = Eq.ndrec (motive := fun {N' : ℕ} => [inst : NeZero N'] → Complexity.Circuit B N' M G) (fun [NeZero N] => circuit) h

def Complexity.Circuit.restrictPrefix {m M G : ℕ} [NeZero m] [NeZero M] {k : ℕ} : BitString k → Circuit Basis.andOr2 (k + m) M G → Circuit Basis.andOr2 m M G

Fix the first k inputs of a fan-in-two AND/OR circuit to seed.

The remaining positive number m of inputs retain their order, and the internal gate count G is unchanged. The zero-length prefix is the identity after canonical input-arity transport.

Equations

• Complexity.Circuit.restrictPrefix x_3 circuit = Complexity.Circuit.castInputArity ⋯ circuit
• Complexity.Circuit.restrictPrefix seed circuit = Complexity.Circuit.restrictPrefix (Fin.tail seed) (Complexity.restrictCircuit (seed 0) circuit)

theorem Complexity.Circuit.restrictPrefix_eval {k m M G : ℕ} [NeZero m] [NeZero M] (seed : BitString k) (circuit : Circuit Basis.andOr2 (k + m) M G) (input : BitString m) : (restrictPrefix seed circuit).eval input = circuit.eval (Fin.append seed input)

Prefix hardwiring agrees with evaluating the original circuit on the fixed prefix followed by the live input.

@[simp]

theorem Complexity.Circuit.restrictPrefix_size {k m M G : ℕ} [NeZero m] [NeZero M] (seed : BitString k) (circuit : Circuit Basis.andOr2 (k + m) M G) : (restrictPrefix seed circuit).size = circuit.size

Prefix hardwiring preserves the exact circuit size.