Combining circuit codes on shared inputs

appendCode n c d runs both codes on the same n inputs, keeping the outputs of c before those of d. It shifts the gate references of d past the gates of c, while preserving its input references. On codes of circuits, the result is the code of Circuit.append. appendCodes combines any list of blocks by repeated append; each block is relocated by the number of preceding gates. bundleCode uses a fixed block size and agrees with appendCodes when its blocks have that size. All three constructors are computable in polynomial time with binary layout parameters.

compCode n d c instead feeds c's output wires to d's inputs. Its polynomial-time constructor performs binary-indexed lookup and gate relocation, and agrees exactly with Circuit.comp.

Main definitions

• Cslib.Circuits.Program.appendWireCode: wire numbers under program continuation.
• Cslib.Circuits.Boolean.appendCode: combine raw codes on shared inputs.
• Cslib.Circuits.Boolean.appendCodes: combine raw blocks of varying sizes on shared inputs.
• Cslib.Circuits.Boolean.bundleCode: combine equal-sized raw blocks on shared inputs.
• Cslib.Circuits.Boolean.compCode: compose raw circuit codes through their output wires.

Main results

• Cslib.Circuits.Program.code_append: code of program continuation.
• Cslib.Circuits.Boolean.appendCode_code: agreement with typed circuit append.
• Cslib.Circuits.Boolean.length_appendCode: additive gate count.
• Cslib.Circuits.Boolean.computableInPolyTime_appendCode: constructor efficiency.
• Cslib.Circuits.Boolean.appendCodes_code: agreement with arbitrary typed output families.
• Cslib.Circuits.Boolean.computableInPolyTime_appendCodes: varying-size constructor efficiency, including arbitrary binary wire indices.
• Cslib.Circuits.Boolean.bundleCode_eq_foldl_appendCode: bundling agrees with repeated append.
• Cslib.Circuits.Boolean.computableInPolyTime_bundleCode: bundling efficiency.
• Cslib.Circuits.Boolean.exists_circuit_bundleCode: raw bundles realize typed output families.
• Cslib.Circuits.Boolean.compCode_code: agreement with typed sequential composition.
• Cslib.Circuits.Boolean.computableInPolyTime_compCode: sequential constructor efficiency.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

def Cslib.Circuits.Program.appendWireCode (n m s : ℕ) (feed : Fin m → Wire n s) (i : ℕ) : ℕ

The wire-number map when continuing a program with another program.

theorem Cslib.Circuits.Program.appendedWire_toNat {n m s t : ℕ} (feed : Fin m → Wire n s) (w : Wire m t) : (appendedWire feed w).toNat = appendWireCode n m s feed w.toNat

Numbering a continued wire agrees with the raw wire-number map.

theorem Cslib.Circuits.Program.code_append {σ : Signature} {n m s t : ℕ} (p : Program σ n s) (feed : Fin m → Wire n s) (q : Program σ m t) : (p.append feed q).code = p.code ++ List.map (fun (g : σ.Op × List ℕ) => (g.1, List.map (appendWireCode n m s feed) g.2)) q.code

Program continuation acts on codes by appending the rewired gate list.

def Cslib.Circuits.Boolean.shiftCodeWire (n offset i : ℕ) : ℕ

Retain an input wire, or shift a gate wire past offset preceding gates.

def Cslib.Circuits.Boolean.appendCode (n : ℕ) (c d : List (Op × List ℕ) × List ℕ) : List (Op × List ℕ) × List ℕ

Run two raw codes on shared inputs, listing the first code's outputs before the second's. Malformed codes are transformed as data; semantic correctness is asserted on typed circuits.

@[simp]

theorem Cslib.Circuits.Boolean.length_appendCode (n : ℕ) (c d : List (Op × List ℕ) × List ℕ) : (appendCode n c d).1.length = c.1.length + d.1.length

@[simp]

theorem Cslib.Circuits.Boolean.length_appendCode_outputs (n : ℕ) (c d : List (Op × List ℕ) × List ℕ) : (appendCode n c d).2.length = c.2.length + d.2.length

theorem Cslib.Circuits.Boolean.appendCode_code {n m p : ℕ} (c : Circuit signature n m) (d : Circuit signature n p) : appendCode n c.code d.code = (c.append d).code

Raw shared-input composition agrees with ordinary typed circuit append.

theorem Cslib.Circuits.Boolean.evalOutput_appendCode_code {n m p : ℕ} (c : Circuit signature n m) (d : Circuit signature n p) (x : Fin n → Bool) : List.map (evalOutput (List.ofFn x) (appendCode n c.code d.code).1) (appendCode n c.code d.code).2 = List.ofFn (c.eval interpretation x) ++ List.ofFn (d.eval interpretation x)

The outputs of combined codes are the two output lists in order, on every input.

theorem Cslib.Circuits.Boolean.computableInPolyTime_shiftCodeWire {α : Type} {enc : α ↪ List Bool} {n offset i : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hoffset : Turing.MultiTapeTM.ComputableInPolyTime offset enc Turing.MultiTapeTM.encNat) (hi : Turing.MultiTapeTM.ComputableInPolyTime i enc Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => shiftCodeWire (n a) (offset a) (i a)) enc Turing.MultiTapeTM.encNat

Shifting wire numbers is polynomial-time with all quantities encoded in binary.

def Cslib.Circuits.Boolean.shiftCode (n offset : ℕ) (code : List (Op × List ℕ) × List ℕ) : List (Op × List ℕ) × List ℕ

Shift the gate references and output references of a raw code. Input wires are preserved.

theorem Cslib.Circuits.Boolean.computableInPolyTime_shiftCode {α : Type} {enc : α ↪ List Bool} {n offset : α → ℕ} {code : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hoffset : Turing.MultiTapeTM.ComputableInPolyTime offset enc Turing.MultiTapeTM.encNat) (hcode : Turing.MultiTapeTM.ComputableInPolyTime code enc encCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => shiftCode (n a) (offset a) (code a)) enc encCode

Relocating a circuit-code block is polynomial-time with binary offsets.

theorem Cslib.Circuits.Boolean.computableInPolyTime_appendCode {α : Type} {enc : α ↪ List Bool} {n : α → ℕ} {c d : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hc : Turing.MultiTapeTM.ComputableInPolyTime c enc encCode) (hd : Turing.MultiTapeTM.ComputableInPolyTime d enc encCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => appendCode (n a) (c a) (d a)) enc encCode

Combining circuit codes is polynomial-time, including binary input and wire counts.

def Cslib.Circuits.Boolean.appendCodes (n : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) : List (Op × List ℕ) × List ℕ

Combine a list of raw codes on shared inputs, preserving block and output order. Blocks may have different gate counts and any number of outputs.

@[simp]

theorem Cslib.Circuits.Boolean.appendCodes_nil (n : ℕ) : appendCodes n [] = ([], [])

theorem Cslib.Circuits.Boolean.appendCodes_append_singleton (n : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) (code : List (Op × List ℕ) × List ℕ) : appendCodes n (codes ++ [code]) = appendCode n (appendCodes n codes) code

Adding a final block is ordinary shared-input append.

@[simp]

theorem Cslib.Circuits.Boolean.length_appendCodes (n : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) : (appendCodes n codes).1.length = (List.flatMap Prod.fst codes).length

The combined code retains every gate, without padding the individual blocks.

@[simp]

theorem Cslib.Circuits.Boolean.length_appendCodes_outputs (n : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) : (appendCodes n codes).2.length = (List.flatMap Prod.snd codes).length

The combined code retains all outputs, including repeated outputs and zero-gate blocks.

theorem Cslib.Circuits.Boolean.computableInPolyTime_appendCodes {α : Type} {enc : α ↪ List Bool} {n : α → ℕ} {codes : α → List (List (Op × List ℕ) × List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hcodes : Turing.MultiTapeTM.ComputableInPolyTime codes enc (Turing.MultiTapeTM.encList encCode)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => appendCodes (n a) (codes a)) enc encCode

Combining arbitrary raw blocks is polynomial-time in their complete encodings. Input and wire numbers are binary; no uniform block-size or well-formedness premise is needed.

theorem Cslib.Circuits.Boolean.appendCodes_code {k n : ℕ} (cs : Fin k → Circuit signature n 1) : appendCodes n (List.ofFn fun (j : Fin k) => (cs j).code) = (Circuit.pi cs).code

Combining single-output circuit codes agrees exactly with Circuit.pi, with no restriction on the gate counts of its components.

def Cslib.Circuits.Boolean.bundleCode (n blockSize : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) : List (Op × List ℕ) × List ℕ

Combine equal-sized gate blocks on shared inputs. Block j is relocated by j * blockSize. The construction is total on raw data; its append semantics requires the stated block sizes.

theorem Cslib.Circuits.Boolean.computableInPolyTime_bundleCode {α : Type} {enc : α ↪ List Bool} {n blockSize : α → ℕ} {codes : α → List (List (Op × List ℕ) × List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hblock : Turing.MultiTapeTM.ComputableInPolyTime blockSize enc Turing.MultiTapeTM.encNat) (hcodes : Turing.MultiTapeTM.ComputableInPolyTime codes enc (Turing.MultiTapeTM.encList encCode)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => bundleCode (n a) (blockSize a) (codes a)) enc encCode

Bundling raw blocks is polynomial-time in their encodings and binary layout parameters.

theorem Cslib.Circuits.Boolean.length_bundleCode (n blockSize : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) (hlen : ∀ c ∈ codes, c.1.length = blockSize) : (bundleCode n blockSize codes).1.length = codes.length * blockSize

Equal-sized blocks occupy exactly their number times their common gate count.

theorem Cslib.Circuits.Boolean.bundleCode_append_singleton (n blockSize : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) (code : List (Op × List ℕ) × List ℕ) (hlen : ∀ c ∈ codes, c.1.length = blockSize) : bundleCode n blockSize (codes ++ [code]) = appendCode n (bundleCode n blockSize codes) code

Adding the next equal-sized block is shared-input append.

theorem Cslib.Circuits.Boolean.bundleCode_eq_foldl_appendCode (n blockSize : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) (hlen : ∀ c ∈ codes, c.1.length = blockSize) : bundleCode n blockSize codes = List.foldl (appendCode n) ([], []) codes

For equal-sized blocks, direct relocation agrees with repeated shared-input append.

theorem Cslib.Circuits.Boolean.bundleCode_eq_appendCodes (n blockSize : ℕ) (codes : List (List (Op × List ℕ) × List ℕ)) (hlen : ∀ c ∈ codes, c.1.length = blockSize) : bundleCode n blockSize codes = appendCodes n codes

Fixed-size bundling is a specialization of the varying-size constructor.

theorem Cslib.Circuits.Boolean.bundleCode_code {k n : ℕ} (cs : Fin k → Circuit signature n 1) (blockSize : ℕ) (hs : ∀ (j : Fin k), (cs j).size = blockSize) : bundleCode n blockSize (List.ofFn fun (j : Fin k) => (cs j).code) = (Circuit.pi cs).code

The typed and raw bundles have exactly the same code when component sizes agree.

theorem Cslib.Circuits.Boolean.exists_circuit_bundleCode {k n : ℕ} (cs : Fin k → Circuit signature n 1) (blockSize : ℕ) (hs : ∀ (j : Fin k), (cs j).size = blockSize) : ∃ (c : Circuit signature n k), bundleCode n blockSize (List.ofFn fun (j : Fin k) => (cs j).code) = c.code ∧ ∀ (x : Fin n → Bool) (j : Fin k), c.eval interpretation x j = (cs j).eval interpretation x 0

Equal-sized single-output codes form one typed circuit with the corresponding output order.

def Cslib.Circuits.Boolean.compCodeWire (n : ℕ) (c : List (Op × List ℕ) × List ℕ) (i : ℕ) : ℕ

Route a later circuit's inputs through c's outputs and shift its gates past c's gates.

def Cslib.Circuits.Boolean.compCode (n : ℕ) (d c : List (Op × List ℕ) × List ℕ) : List (Op × List ℕ) × List ℕ

Feed the outputs of c to the inputs of d, matching the argument order of Circuit.comp. The constructor is total on raw data, including malformed circuit codes.

theorem Cslib.Circuits.Boolean.compCode_code {n m p : ℕ} (d : Circuit signature m p) (c : Circuit signature n m) : compCode n d.code c.code = (d.comp c).code

Raw sequential composition is exactly the code of typed circuit composition.

@[simp]

theorem Cslib.Circuits.Boolean.length_compCode (n : ℕ) (d c : List (Op × List ℕ) × List ℕ) : (compCode n d c).1.length = c.1.length + d.1.length

Sequential composition retains both gate lists.

@[simp]

theorem Cslib.Circuits.Boolean.length_compCode_outputs (n : ℕ) (d c : List (Op × List ℕ) × List ℕ) : (compCode n d c).2.length = d.2.length

Sequential composition retains the later circuit's number of outputs.

theorem Cslib.Circuits.Boolean.computableInPolyTime_compCodeWire {α : Type} {enc : α ↪ List Bool} {n i : α → ℕ} {c : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hc : Turing.MultiTapeTM.ComputableInPolyTime c enc encCode) (hi : Turing.MultiTapeTM.ComputableInPolyTime i enc Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => compCodeWire (n a) (c a) (i a)) enc Turing.MultiTapeTM.encNat

Resolve a composed wire in polynomial time, including binary output lookup and offsets.

theorem Cslib.Circuits.Boolean.computableInPolyTime_compCode {α : Type} {enc : α ↪ List Bool} {n : α → ℕ} {d c : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hd : Turing.MultiTapeTM.ComputableInPolyTime d enc encCode) (hc : Turing.MultiTapeTM.ComputableInPolyTime c enc encCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => compCode (n a) (d a) (c a)) enc encCode

Construct sequential circuit codes in polynomial time. All wire indices and input counts are binary; list lengths, input lookup, gate relocation and the whole output code are charged.