Documentation

Complexity.Computability.Circuit.Boolean.CodeSubstitution

Hardwiring a prefix of a Boolean circuit code #

prefixCode r n code replaces the first r.length inputs by r and leaves n live inputs. Two shared constant gates precede the original gates. The transformation is the raw code of ordinary circuit composition, with exactly two additional gates. Its constructor runs in polynomial time, with n in binary and all wire numbers in binary.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.prefixWire (r : List Bool) (n i : ℕ) :
ℕ

Map an old wire to a live suffix input, a shared constant, or a shifted gate.

Instances For
    source
    def Cslib.Circuits.Boolean.prefixCode (r : List Bool) (n : ℕ) (code : List (Op × List ℕ) × List ℕ) :
    List (Op × List ℕ) × List ℕ

    Hardwire a prefix, sharing two constant gates and retaining all original gates and outputs. Malformed codes are transformed as data; correctness is asserted on codes of typed circuits.

    Instances For
      source
      def Cslib.Circuits.Boolean.prefixInputs (r : List Bool) (n : ℕ) :
      Fin (r.length + n) → Fin n ⊕ Bool

      Feed the fixed prefix bits followed by the live suffix inputs.

      Instances For
        source
        def Cslib.Circuits.Boolean.prefixCircuit {n m : ℕ} (r : List Bool) (c : Circuit signature (r.length + n) m) :
        Circuit signature n m

        Hardwire a prefix using the existing shared-constant substitution circuit.

        Instances For
          source
          theorem Cslib.Circuits.Boolean.code_prefixCircuit {n m : ℕ} (r : List Bool) (c : Circuit signature (r.length + n) m) :
          (prefixCircuit r c).code = prefixCode r n c.code

          The raw hardwiring transformation is exactly the code of typed circuit composition.

          source
          @[simp]
          theorem Cslib.Circuits.Boolean.ofCode_prefixCode {n m : ℕ} (r : List Bool) (c : Circuit signature (r.length + n) m) :
          Circuit.ofCode n m (prefixCode r n c.code) = some (prefixCircuit r c)

          Decoding the hardwired code produces the corresponding typed circuit.

          source
          theorem Cslib.Circuits.Boolean.isSome_ofCode_prefixCode {n m : ℕ} (r : List Bool) (code : List (Op × List ℕ) × List ℕ) (h : (Circuit.ofCode (r.length + n) m code).isSome = true) :
          (Circuit.ofCode n m (prefixCode r n code)).isSome = true

          A valid circuit code remains valid after hardwiring its input prefix.

          source
          @[simp]
          theorem Cslib.Circuits.Boolean.eval_prefixCircuit {n m : ℕ} (r : List Bool) (c : Circuit signature (r.length + n) m) (x : Fin n → Bool) :
          (prefixCircuit r c).eval interpretation x = c.eval interpretation (Fin.append (fun (i : Fin r.length) => r[↑i]) x)

          Hardwiring a prefix supplies its bits before the live inputs.

          source
          theorem Cslib.Circuits.Boolean.evalOutputs_prefixCode {n m : ℕ} (r : List Bool) (c : Circuit signature (r.length + n) m) (x : Fin n → Bool) :
          List.map (evalOutput (List.ofFn x) (prefixCode r n c.code).1) (prefixCode r n c.code).2 = List.ofFn (c.eval interpretation (Fin.append (fun (i : Fin r.length) => r[↑i]) x))

          Reading the hardwired raw code's output wires gives the original circuit's outputs.

          source
          @[simp]
          theorem Cslib.Circuits.Boolean.size_prefixCircuit {n m : ℕ} (r : List Bool) (c : Circuit signature (r.length + n) m) :
          (prefixCircuit r c).size = 2 + c.size

          Exactly two gates are added, even if the constants or all outputs are unused.

          source
          @[simp]
          theorem Cslib.Circuits.Boolean.length_prefixCode (r : List Bool) (n : ℕ) (code : List (Op × List ℕ) × List ℕ) :
          (prefixCode r n code).1.length = 2 + code.1.length ∧ (prefixCode r n code).2.length = code.2.length

          Hardwiring adds two gates and retains every designated output.

          source
          theorem Cslib.Circuits.Boolean.computableInPolyTime_prefixWire {α : Type} {encIn : α ↪ List Bool} {r : α → List Bool} {n i : α → ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encBits) (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encNat) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encNat) :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => prefixWire (r a) (n a) (i a)) encIn Turing.MultiTapeTM.encNat

          Rewriting one wire is polynomial-time even when wire numbers and n are binary.

          source
          theorem Cslib.Circuits.Boolean.computableInPolyTime_prefixCode {α : Type} {encIn : α ↪ List Bool} {r : α → List Bool} {n : α → ℕ} {code : α → List (Op × List ℕ) × List ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encBits) (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encNat) (hcode : Turing.MultiTapeTM.ComputableInPolyTime code encIn encCode) :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => prefixCode (r a) (n a) (code a)) encIn encCode

          Construct hardwired raw codes in polynomial time, with binary live-input and wire counts.