Documentation

CsdLean4.Mathlib.QuantumInfo.Reversible.Circuit

Reversible classical circuits — the gate-list DSL #

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

A minimal, derived-cost abstraction for reversible classical circuits. The design choice is deliberate: a circuit is a list of gates, its action is the fold of the per-gate semantics, and (in Cost.lean) its resource cost is a function of the gate list. Resource bounds are therefore theorems about an exhibited circuit, not numbers annotated onto an opaque Equiv — the prerequisite for cost accounting to be genuinely machine-checked. (The reversible-arithmetic application this substrate was built for lives in the Ecdsafail repository, specs/ecdsa/ecdlp-resource-plan.md there.)

Each primitive gate (X flip, CX = CNOT, CCX = Toffoli, swap) is an involution: degenerate forms (control = target) act as the identity, so every gate is its own inverse unconditionally. Hence a circuit's inverse is the reversed gate list (inverse = List.reverse), and denote is a bijection. State is Fin n → Bool; the bridge to the quantum register QReg n (basis states indexed by Fin n → Fin 2) is kept out of this classical layer — it is the embedding Reversible/Lift.lean provides (basis-state permutation semantics).

source
inductive Reversible.Gate (n : ℕ) :
Type

A reversible classical gate on n wires (state Fin n → Bool).

  • X {n : ℕ} (i : Fin n) : Gate n

    Flip wire i.

  • CX {n : ℕ} (c t : Fin n) : Gate n

    CNOT: if wire c is set, flip wire t. Acts as the identity if c = t.

  • CCX {n : ℕ} (c₁ c₂ t : Fin n) : Gate n

    Toffoli: if wires c₁ and c₂ are both set, flip wire t. Identity if t ∈ {c₁, c₂}.

  • swap {n : ℕ} (i j : Fin n) : Gate n

    Exchange wires i and j.

Instances For
    source
    def Reversible.instDecidableEqGate.decEq {n✝ : ℕ} (x✝ x✝¹ : Gate n✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Reversible.instDecidableEqGate {n✝ : ℕ} :
      DecidableEq (Gate n✝)
      Equations
      source
      @[reducible, inline]
      abbrev Reversible.State (n : ℕ) :
      Type

      The Boolean state of n wires.

      Equations
      Instances For
        source
        def Reversible.denoteGate {n : ℕ} :
        Gate n → State n → State n

        Semantics of a single gate as a state transformation. Degenerate forms (control = target) are the identity, which keeps every gate an involution.

        Equations
        Instances For
          source
          theorem Reversible.denoteGate_involutive {n : ℕ} (g : Gate n) :
          Function.Involutive (denoteGate g)

          Every gate is an involution (its own inverse).

          source
          @[reducible, inline]
          abbrev Reversible.Circuit (n : ℕ) :
          Type

          A reversible circuit on n wires: a list of gates applied left to right.

          Equations
          Instances For
            source
            def Reversible.denote {n : ℕ} (c : Circuit n) (s : State n) :
            State n

            The action of a circuit: fold the per-gate semantics over the list (first gate first).

            Equations
            Instances For
              source
              @[simp]
              theorem Reversible.denote_nil {n : ℕ} (s : State n) :
              denote [] s = s
              source
              theorem Reversible.denote_cons {n : ℕ} (g : Gate n) (c : Circuit n) (s : State n) :
              denote (g :: c) s = denote c (denoteGate g s)
              source
              theorem Reversible.denote_append {n : ℕ} (c₁ c₂ : Circuit n) (s : State n) :
              denote (c₁ ++ c₂) s = denote c₂ (denote c₁ s)

              Composition correctness: running c₁ ++ c₂ is c₁ then c₂.

              source
              theorem Reversible.reversible_comp_correct {n : ℕ} (c₁ c₂ : Circuit n) :
              denote (c₁ ++ c₂) = denote c₂ ∘ denote c₁

              reversible_comp_correct: the denotation of a concatenation is the composition of denotations (c₁ first, then c₂).

              source
              def Reversible.inverse {n : ℕ} (c : Circuit n) :
              Circuit n

              The inverse circuit: the reversed gate list (each gate is its own inverse).

              Equations
              Instances For
                source
                @[simp]
                theorem Reversible.inverse_nil {n : ℕ} :
                inverse [] = []
                source
                theorem Reversible.reversible_inverse_correct {n : ℕ} (c : Circuit n) (s : State n) :
                denote (inverse c) (denote c s) = s

                reversible_inverse_correct (left): the inverse circuit undoes the circuit.

                source
                theorem Reversible.reversible_inverse_correct' {n : ℕ} (c : Circuit n) (s : State n) :
                denote c (denote (inverse c) s) = s

                reversible_inverse_correct (right): the circuit undoes its inverse.

                source
                theorem Reversible.denote_bijective {n : ℕ} (c : Circuit n) :
                Function.Bijective (denote c)

                A circuit's denotation is a bijection (it has the inverse circuit as a two-sided inverse).

                Wire support and the frame (locality) lemma #

                A gate only touches the wires in gateWires; every other wire is preserved. Lifted to circuits, this is the frame lemma denote_apply_of_forall_not_mem — the reusable primitive for transporting a gadget's correctness from a concrete wire layout to arbitrary Fin n wires (consumed by the ModAdd / ModMul arithmetic proofs).

                source
                def Reversible.gateWires {n : ℕ} :
                Gate n → Finset (Fin n)

                The set of wires a gate acts on. A wire outside this set is preserved by denoteGate (denoteGate_apply_of_not_mem).

                Equations
                Instances For

                  Interface lemmas (CONVENTIONS §9.1, F1): per-constructor wire sets, stated once. Not @[simp] — existing proofs unfold by name and must keep their behaviour.

                  source
                  theorem Reversible.gateWires_X {n : ℕ} (i : Fin n) :
                  gateWires (Gate.X i) = {i}

                  The wires of an X gate.

                  source
                  theorem Reversible.gateWires_CX {n : ℕ} (c t : Fin n) :
                  gateWires (Gate.CX c t) = {c, t}

                  The wires of a CX gate.

                  source
                  theorem Reversible.gateWires_CCX {n : ℕ} (c₁ c₂ t : Fin n) :
                  gateWires (Gate.CCX c₁ c₂ t) = {c₁, c₂, t}

                  The wires of a CCX gate.

                  source
                  theorem Reversible.gateWires_swap {n : ℕ} (i j : Fin n) :
                  gateWires (Gate.swap i j) = {i, j}

                  The wires of a swap gate.

                  source
                  theorem Reversible.denoteGate_apply_of_not_mem {n : ℕ} {g : Gate n} {s : State n} {i : Fin n} (hi : i ∉ gateWires g) :
                  denoteGate g s i = s i

                  Frame lemma (single gate). A wire outside gateWires g is left unchanged by denoteGate g.

                  source
                  theorem Reversible.denote_apply_of_forall_not_mem {n : ℕ} {i : Fin n} (c : Circuit n) :
                  (∀ g ∈ c, i ∉ gateWires g) → ∀ (s : State n), denote c s i = s i

                  Frame lemma (circuit). A wire untouched by every gate of c is unchanged by denote c. Stated with the per-gate membership hypothesis (the form the gadget proofs consume).