Uniform instantiation of fixed Boolean formula templates

The formula is fixed, while the target input count and its selected binary input references may vary. The certificate constructs the actual code of the renamed formula. It does not use a finite encoding of circuits at a fixed width. Variable-size families of instances can use appendCodes after providing their uniform scalar generator.

Main definitions

• Cslib.Circuits.Boolean.formulaCode: the actual code of a fixed formula at selected wires.

Main results

• Cslib.Circuits.Boolean.formulaCode_eq_code: exact agreement with typed instantiation.
• Cslib.Circuits.Boolean.computableInPolyTime_formulaCode: instantiate a fixed formula at efficiently computed input wires.

def Cslib.Circuits.Boolean.formulaCode {m : ℕ} (n : ℕ) (F : Formula signature m) (wires : Fin m → ℕ) : List (Op × List ℕ) × List ℕ

Instantiate a formula at raw wire numbers. This algorithm is total even when a selected wire is outside the declared input count; its typed correctness theorem requires valid wires.

theorem Cslib.Circuits.Boolean.formulaCode_eq_code {n m : ℕ} (F : Formula signature m) (wires : Fin m → Fin n) : (formulaCode n F fun (i : Fin m) => ↑(wires i)) = (Formula.rename wires F).toCircuit.code

Instantiating valid input wires constructs exactly the renamed formula's circuit code.

theorem Cslib.Circuits.Boolean.computableInPolyTime_formulaCode {α : Type} {enc : α ↪ List Bool} {n : α → ℕ} {m : ℕ} (F : Formula signature m) {wires : α → Fin m → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hwires : ∀ (i : Fin m), Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => wires a i) enc Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => formulaCode (n a) F (wires a)) enc encCode

A fixed formula's full instantiated code is polynomial-time in the target input count and its selected binary wire numbers. This is uniform in every target width and reference.