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 has 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 G : ℕ} [NeZero m] {k : ℕ} : BitString k → Circuit Basis.andOr2 (k + m) 1 G → Circuit Basis.andOr2 m 1 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 G : ℕ} [NeZero m] (seed : BitString k) (circuit : Circuit Basis.andOr2 (k + m) 1 G) (input : BitString m) : (restrictPrefix seed circuit).eval input 0 = circuit.eval (Fin.append seed input) 0

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 G : ℕ} [NeZero m] (seed : BitString k) (circuit : Circuit Basis.andOr2 (k + m) 1 G) : (restrictPrefix seed circuit).size = circuit.size

Prefix hardwiring preserves the exact circuit size.