Reversible controlled addition — the quantum×quantum primitive (ECDLP Phase 2, Stage S2)

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

The Tranche-3 multiplier (ModMul.lean) is quantum×classical: it multiplies a classical constant a = ∑ 2^sh (fixed shifts) by the quantum register Y. Squaring Y² and, more importantly, the field multiplications inside an elliptic-curve point operation are quantum×quantum (both factors are registers): bit i of one factor must control whether the other, shifted, is added. That needs a controlled adder, the primitive built here.

The obstacle: a control-wire-ctrled full adder needs ctrl ANDed with the adder's two inputs — i.e. 3-control gates — while the DSL tops out at CCX (2 controls). We use the standard clean-ancilla decomposition CCCX ctrl x y z = [CCX ctrl x anc, CCX anc y z, CCX ctrl x anc] (anc init false, restored to false), so one shared ancilla suffices and the controlled full adder stays inside the 2-control DSL.

What is proved here (Stage S2.1 — the gadget)

• cfullAdder — the controlled full adder on (ctrl, a, b, cin, cout, anc) (with cout, anc initialised false), eight CCX gates: each gate of fullAdder controlled on ctrl via the ancilla decomposition.
• cfullAdder_correct — full all-inputs correctness (decide over State 6): when ctrl is set it computes the full-adder sum/carry (b ← a⊕b⊕cin, cout ← majority, a/cin preserved); when ctrl is clear it is the identity; either way anc is restored to false.
• cfullAdder_cost — derived toffoli = 8, everything else 0: a controlled add is 4× the uncontrolled full adder's two Toffolis, plus one ancilla. The honest quantum×quantum overhead.

def Reversible.cfullAdder {n : ℕ} (ctrl a b cin cout anc : Fin n) : Circuit n

The controlled full adder on wires ctrl a b cin cout anc (with cout, anc initialised false): when ctrl is set it acts as fullAdder a b cin cout; when ctrl is clear it is the identity. Each of fullAdder's four gates is controlled on ctrl: the two CCXs become 3-control gates realised by the clean-ancilla decomposition CCX ctrl · anc ; CCX anc · cout ; CCX ctrl · anc, and the two CXs become CCX ctrl · ·. Eight CCXs; anc is borrowed clean and returned clean.

Equations

• One or more equations did not get rendered due to their size.

theorem Reversible.cfullAdder_correct (s : State 6) : s 4 = false → s 5 = false → (denote (cfullAdder 0 1 2 3 4 5) s 2 = if s 0 = true then s 1 ^^ s 2 ^^ s 3 else s 2) ∧ (denote (cfullAdder 0 1 2 3 4 5) s 4 = if s 0 = true then majority (s 1) (s 2) (s 3) else false) ∧ denote (cfullAdder 0 1 2 3 4 5) s 5 = false ∧ denote (cfullAdder 0 1 2 3 4 5) s 0 = s 0 ∧ denote (cfullAdder 0 1 2 3 4 5) s 1 = s 1 ∧ denote (cfullAdder 0 1 2 3 4 5) s 3 = s 3

Controlled-full-adder correctness — genuine all-inputs coverage. On the concrete State 6 layout (wires 0..5 = ctrl, a, b, cin, cout, anc), with cout and anc initialised false: if ctrl (wire 0) is set the gadget computes the sum bit on b (wire 2), the carry-out on cout (wire 4), and preserves a, cin; if ctrl is clear it preserves b and leaves cout false; the ancilla (wire 5) is restored to false in both cases. Proved by decide over State 6 (the 2^6 inputs with cout, anc fixed false).

theorem Reversible.cfullAdder_cost {n : ℕ} (ctrl a b cin cout anc : Fin n) : (circuitCost (cfullAdder ctrl a b cin cout anc)).toffoli = 8

Derived Toffoli cost of the controlled full adder (from the gate list, via circuitCost): eight Toffolis. Read off the eight CCXs. The uncontrolled fullAdder is 2 Toffolis + 2 CNOTs; the controlled gadget is 8 Toffolis + 0 CNOTs (cfullAdder_cnot) — the two CXs are promoted to CCX ctrl · · (absorbing the CNOTs into Toffolis) and the two CCXs expand to ancilla-mediated CCCX. Plus one designated clean ancilla wire (not billed by gateCost). The honest quantum×quantum overhead.

theorem Reversible.cfullAdder_cnot {n : ℕ} (ctrl a b cin cout anc : Fin n) : (circuitCost (cfullAdder ctrl a b cin cout anc)).cnot = 0

The controlled full adder uses no CNOTs (cnot = 0): every gate is a CCX, the two CXs of the uncontrolled fullAdder having been promoted to controlled CCXs. Derived from the gate list.

theorem Reversible.cfullAdder_apply_of_ne {n : ℕ} {ctrl a b cin cout anc w : Fin n} (hctrl : w ≠ ctrl) (ha : w ≠ a) (hb : w ≠ b) (hcin : w ≠ cin) (hcout : w ≠ cout) (hanc : w ≠ anc) (s : State n) : denote (cfullAdder ctrl a b cin cout anc) s w = s w

Frame lemma for the controlled gadget. A wire distinct from all six of ctrl, a, b, cin, cout, anc is untouched by cfullAdder (every gate's wires lie in that set). Lets the controlled carry-chain lift the gadget over a register.

theorem Reversible.cfullAdder_correct_general {n : ℕ} {ctrl a b cin cout anc : Fin n} (hctrla : ctrl ≠ a) (hctrlb : ctrl ≠ b) (hctrlcin : ctrl ≠ cin) (hctrlcout : ctrl ≠ cout) (hctrlanc : ctrl ≠ anc) (hab : a ≠ b) (hacin : a ≠ cin) (hacout : a ≠ cout) (haanc : a ≠ anc) (hbcin : b ≠ cin) (hbcout : b ≠ cout) (hbanc : b ≠ anc) (hcincout : cin ≠ cout) (hcinanc : cin ≠ anc) (hcoutanc : cout ≠ anc) {s : State n} (hcout : s cout = false) (hanc : s anc = false) : (denote (cfullAdder ctrl a b cin cout anc) s b = if s ctrl = true then s a ^^ s b ^^ s cin else s b) ∧ (denote (cfullAdder ctrl a b cin cout anc) s cout = if s ctrl = true then majority (s a) (s b) (s cin) else false) ∧ denote (cfullAdder ctrl a b cin cout anc) s anc = false ∧ denote (cfullAdder ctrl a b cin cout anc) s a = s a ∧ denote (cfullAdder ctrl a b cin cout anc) s cin = s cin ∧ denote (cfullAdder ctrl a b cin cout anc) s ctrl = s ctrl

Controlled-full-adder correctness, general Fin n wires. For pairwise-distinct wires ctrl, a, b, cin, cout, anc with cout and anc initialised false: when ctrl is set the gadget writes the sum bit to b, the carry-out to cout, and preserves a, cin; when ctrl is clear it preserves b and leaves cout false; the ancilla anc is restored to false in both cases. This is the slice the controlled ripple carry-chain iterates.

The controlled ripple adder (general n): correctness

A CRippleLayout is a RippleLayout (registers A, B, carry chain C) plus a control wire ctrl and a shared clean ancilla anc, both disjoint from the registers. The controlled ripple adder is one cfullAdder per slice, all sharing ctrl and anc. The headline: it leaves register B holding (A + B) mod 2^n when ctrl is set, and B unchanged when ctrl is clear.

structure Reversible.CRippleLayout (m n : ℕ) extends Reversible.RippleLayout m n : Type

A controlled ripple-adder layout: a RippleLayout plus a control wire and a shared ancilla, both disjoint from registers A, B and the carry chain C.

• A : ℕ → Fin m
• B : ℕ → Fin m
• C : ℕ → Fin m
• hAB (i j : ℕ) : self.A i ≠ self.B j
• hAC (i j : ℕ) : self.A i ≠ self.C j
• hBC (i j : ℕ) : self.B i ≠ self.C j
• hAinj (i j : ℕ) : i < n → j < n → self.A i = self.A j → i = j
• hBinj (i j : ℕ) : i < n → j < n → self.B i = self.B j → i = j
• hCinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.C i = self.C j → i = j
• ctrl : Fin m

  The control wire (set ⇒ add, clear ⇒ identity).

• anc : Fin m

  The shared clean ancilla for the CCCX decomposition (borrowed and returned false).

• hctrlA (i : ℕ) : self.ctrl ≠ self.A i
• hctrlB (i : ℕ) : self.ctrl ≠ self.B i
• hctrlC (i : ℕ) : self.ctrl ≠ self.C i
• hctrlanc : self.ctrl ≠ self.anc
• hancA (i : ℕ) : self.anc ≠ self.A i
• hancB (i : ℕ) : self.anc ≠ self.B i
• hancC (i : ℕ) : self.anc ≠ self.C i

def Reversible.cRippleSlice {n m : ℕ} (L : CRippleLayout m n) (i : ℕ) : Circuit m

One controlled ripple slice: a controlled full adder on (A i, B i, C i, C (i+1)) with the shared control and ancilla.

Equations

• Reversible.cRippleSlice L i = Reversible.cfullAdder L.ctrl (L.A i) (L.B i) (L.C i) (L.C (i + 1)) L.anc

def Reversible.cRipplePrefix {n m : ℕ} (L : CRippleLayout m n) (k : ℕ) : Circuit m

The circuit of the first k controlled slices.

Equations

• Reversible.cRipplePrefix L k = List.flatMap (Reversible.cRippleSlice L) (List.range k)

def Reversible.cRippleCirc {n m : ℕ} (L : CRippleLayout m n) : Circuit m

The full controlled ripple adder: all n slices.

Equations

• Reversible.cRippleCirc L = Reversible.cRipplePrefix L n

theorem Reversible.denote_cRipplePrefix_succ {n m : ℕ} (L : CRippleLayout m n) (k : ℕ) (s : State m) : denote (cRipplePrefix L (k + 1)) s = denote (cRippleSlice L k) (denote (cRipplePrefix L k) s)

theorem Reversible.cRippleCirc_invariant {n m : ℕ} (L : CRippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) (hanc0 : s L.anc = false) (k : ℕ) : k ≤ n → regValRange L.B (denote (cRipplePrefix L k) s) k + (denote (cRipplePrefix L k) s (L.C k)).toNat * 2 ^ k = (if s L.ctrl = true then regValRange L.A s k else 0) + regValRange L.B s k ∧ (∀ j < n, denote (cRipplePrefix L k) s (L.A j) = s (L.A j)) ∧ (∀ (j : ℕ), k ≤ j → j < n → denote (cRipplePrefix L k) s (L.B j) = s (L.B j)) ∧ (∀ (j : ℕ), k < j → j < n + 1 → denote (cRipplePrefix L k) s (L.C j) = s (L.C j)) ∧ denote (cRipplePrefix L k) s L.anc = false ∧ denote (cRipplePrefix L k) s L.ctrl = s L.ctrl ∧ (s L.ctrl = false → denote (cRipplePrefix L k) s (L.C k) = false)

The controlled carry-chain invariant. After the first k slices: B's low k bits plus the carry into bit k equal (if ctrl then A else 0) + B over the low k bits (P1 — unified: ctrl clear ⇒ added value 0, carry stays false, B unchanged; ctrl set ⇒ the ripple sum); A untouched (P2); high B (P4) and high carries (P5) preserved; ancilla restored to false (P6); the control bit preserved (P0c); and — the clause that closes the ctrl-clear case — the working carry stays false when ctrl is clear (P7). By induction on k, lifting cfullAdder_correct_general through cfullAdder_apply_of_ne.

theorem Reversible.cRippleCirc_correct {n m : ℕ} (L : CRippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) (hanc0 : s L.anc = false) : regValRange L.B (denote (cRippleCirc L) s) n = if s L.ctrl = true then (regValRange L.A s n + regValRange L.B s n) % 2 ^ n else regValRange L.B s n

Controlled ripple-adder correctness (the S2 headline). For a disjoint-wire layout with all carries and the ancilla initialised false, the controlled ripple adder leaves register B holding (A + B) mod 2^n when the control wire ctrl is set, and B unchanged when ctrl is clear. The quantum×quantum-ready conditional add, derived from the exhibited circuit cRippleCirc.

theorem Reversible.cRippleCirc_toffoli {n m : ℕ} (L : CRippleLayout m n) : (circuitCost (cRippleCirc L)).toffoli = 8 * n

Derived cost of the controlled ripple adder: 8n Toffolis (eight per slice, cfullAdder_cost), composed through the Tranche-1 cost_comp_toffoli_count — 4× the uncontrolled ripple adder's 2n, the honest quantum×quantum overhead.

theorem Reversible.cRippleCirc_anc_restored {n m : ℕ} (L : CRippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) (hanc0 : s L.anc = false) : denote (cRippleCirc L) s L.anc = false

The shared ancilla is returned clean. After the whole controlled ripple adder the ancilla is false again (it is borrowed and restored within each slice). The hygiene fact a multi-step consumer needs to reuse the ancilla between successive controlled adds.

theorem Reversible.cRippleCirc_ctrl_preserved {n m : ℕ} (L : CRippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) (hanc0 : s L.anc = false) : denote (cRippleCirc L) s L.ctrl = s L.ctrl

The control wire is preserved by the controlled ripple adder (it is read, never written). The consumer needs this to keep each partial-product's control bit equal to the original register bit across the accumulation loop.

theorem Reversible.cRippleCirc_preserves_external {n m : ℕ} (L : CRippleLayout m n) (s : State m) (x : Fin m) (hctrl : x ≠ L.ctrl) (hanc : x ≠ L.anc) (hA : ∀ k < n, x ≠ L.A k) (hB : ∀ k < n, x ≠ L.B k) (hC : ∀ k < n + 1, x ≠ L.C k) : denote (cRippleCirc L) s x = s x

The controlled ripple adder preserves any external wire (distinct from ctrl, anc, and every register/carry wire A k, B k, C k). The frame lemma at circuit granularity: every gate of cRippleCirc L has wires among {ctrl, anc} ∪ {A k, B k, C k}.

Non-vacuity witness

A concrete 2-bit controlled ripple layout on Fin 9 (registers A → {0,1}, B → {2,3}, carry chain C → {4,5,6}, control 7, ancilla 8), exhibiting that CRippleLayout is inhabited and the headline applies.

def Reversible.cRippleLayout2 : CRippleLayout 9 2

A concrete 2-bit controlled adder layout on Fin 9.

Equations

• One or more equations did not get rendered due to their size.