The carry-clean (ancilla-restoring) MODULAR adder (ECDLP Phase 2, Stage 2)

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

Stage 1 (CuccaroAdd.lean) delivered the in-place, ancilla-restoring ripple-carry adder cuccaroAdd : A ← (A + B) mod 2ⁿ (B preserved, the single ancilla Z returned false). This module builds, on top of it, the carry-clean MODULAR adder cuccaroModAdd:

Acc ← (a + b) mod N      (a, b < N, 2N ≤ 2ⁿ)

that leaves every flag / scratch / carry wire restored to its input value, so it is reusable in place inside a multiply loop with Θ(n) qubits (versus the Θ(n²) fresh-ancilla penalty the dirty ModularAdd.modAdd carries). This is the qubit collapse that turns the per-multiply Toffoli budget from the fresh-ancilla ~30n² toward ~12n² (an n-fold reuse of a 12n+10-Toffoli clean add).

The construction (clean Beauregard, controlled-add-free)

All arithmetic runs on n+1-bit registers (the extra high wire is the sign / carry-out, which a plain Cuccaro adder does not expose, so it is materialised as register bit n). With 2N ≤ 2ⁿ, all operands have bit n clear and a + b < 2N ≤ 2ⁿ < 2ⁿ⁺¹, so the adds never overflow n+1 bits.

1. Acc += B — cuccaroAdd; Acc = a + b.
2. Acc -= Nreg — cuccaroSub (the inverse adder); Acc = a + b − N (mod 2ⁿ⁺¹).
3. flag ^= Acc[n] — copy the sign bit: flag = [a + b < N].
4. Mask ^= flag·Nreg — n Toffolis: Mask = flag ? N : 0 (the masked constant — this replaces a controlled adder, which the CCX-only gate set cannot build without C³X).
5. Acc += Mask — cuccaroAdd; Acc = (a + b) mod N =: r.
6. Mask ^= flag·Nreg — uncompute the mask: Mask = 0.
7. Acc -= B — cuccaroSub; sign bit Acc[n] = [r < b] = ¬flag.
8. flag ^= Acc[n]; X flag — uncompute the flag: flag = ¬(flag ^^ ¬flag) = 0. THE clean step.
9. Acc += B — cuccaroAdd; restore Acc = r.

The flag uncompute (step 8) is the Beauregard trick: for a, b < N, (a + b mod N) < b ⟺ a + b ≥ N ⟺ ¬flag, so re-deriving the comparison against the preserved addend b recomputes the flag and a CNOT+X clears it. This is what most formalisations stop short of; it is what makes the adder ancilla-restoring.

What is proved (all sorry-free, foundational-triple-only)

• cuccaroSub_correct / _preserves_B / _preserves_Z / _preserves_external — the clean subtractor as the inverse Cuccaro adder, characterised via the bijection (reversible_inverse_correct') and the unconditional cuccaroAdd_preserves_Z / _external.
• cuccaroModAdd_correct — regValRange Acc (denote (cuccaroModAdd L) s) n = (a + b) % N.
• cuccaroModAdd_clean — the point: the flag wire, the carry-out wire Acc[n], every Mask scratch wire, and the ancilla Z are all restored to false. The adder is reusable.
• cuccaroModAdd_preserves_operand — the addend B is intact (and Nreg = N).
• cuccaroModAdd_toffoli — derived 12n + 10 Toffolis (5 carry-out passes at 2(n+1) + two masks at n).

Scope (honest)

This is the carry-clean modular adder (Stage 2): it makes the modular ADD reusable in Θ(n) qubits. The carry-clean modular MULTIPLY (folding this over the multiplicand bits) and the secp256k1 figure re-cost are Stage 2b / Stage 3, not built here.

Small gate-action helpers (single-wire reads of CX / X / CCX)

theorem Reversible.denoteGate_cx_ne {m : ℕ} {c t w : Fin m} (h : w ≠ t) (s : State m) : denoteGate (Gate.CX c t) s w = s w

A wire distinct from the target of a CX is unchanged.

theorem Reversible.denoteGate_cx_target {m : ℕ} {c t : Fin m} (h : c ≠ t) (s : State m) : denoteGate (Gate.CX c t) s t = (s c ^^ s t)

The target of a non-degenerate CX reads s c ^^ s t.

theorem Reversible.denoteGate_x_ne {m : ℕ} {i w : Fin m} (h : w ≠ i) (s : State m) : denoteGate (Gate.X i) s w = s w

A wire distinct from the target of an X is unchanged.

theorem Reversible.denoteGate_x_target {m : ℕ} (i : Fin m) (s : State m) : denoteGate (Gate.X i) s i = !s i

The target of an X is flipped.

theorem Reversible.denoteGate_ccx_ne {m : ℕ} {c₁ c₂ t w : Fin m} (h : w ≠ t) (s : State m) : denoteGate (Gate.CCX c₁ c₂ t) s w = s w

A wire distinct from the target of a CCX is unchanged.

The top (sign) bit of a register as a comparison

theorem Reversible.regValRange_top_bit {m : ℕ} (f : ℕ → Fin m) (s : State m) (k : ℕ) : s (f k) = decide (2 ^ k ≤ regValRange f s (k + 1))

Register bit k is the ≥ 2ᵏ comparison of the low k+1 bits. Reads off regValRange_succ (= low + bit·2ᵏ, low < 2ᵏ): the bit is set iff the k+1-bit value is ≥ 2ᵏ. This materialises the sign / carry-out bit that the carry-clean Cuccaro adder does not expose.

theorem Reversible.rvc {m : ℕ} {f : ℕ → Fin m} {x y : State m} {k : ℕ} (h : ∀ j < k, x (f j) = y (f j)) : regValRange f x k = regValRange f y k

A regValRange-congruence shortcut: equal on the low k wires ⇒ equal readouts.

The clean subtractor: cuccaroSub = inverse cuccaroAdd

cuccaroAdd is a bijection, so its gate-reverse inverse is the exact inverse permutation Acc ← Acc − B (mod 2ⁿ). All four facts are characterised through the bijection identity denote (cuccaroAdd L) (denote (cuccaroSub L) s) = s (reversible_inverse_correct') plus the unconditional forward lemmas cuccaroAdd_preserves_Z / cuccaroAdd_preserves_external.

def Reversible.cuccaroSub {m n : ℕ} (L : CuccaroLayout m n) : Circuit m

The clean ripple-carry subtractor: the gate-reverse of the Cuccaro adder.

Equations

• Reversible.cuccaroSub L = Reversible.inverse (Reversible.cuccaroAdd L)

theorem Reversible.cuccaroSub_preserves_Z {m n : ℕ} (L : CuccaroLayout m n) (s : State m) : denote (cuccaroSub L) s L.Z = s L.Z

The subtractor restores the ancilla Z to its input value, unconditionally.

theorem Reversible.cuccaroSub_preserves_external {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (w : Fin m) (hwZ : w ≠ L.Z) (hwA : ∀ i < n, w ≠ L.A i) (hwB : ∀ i < n, w ≠ L.B i) : denote (cuccaroSub L) s w = s w

The subtractor preserves external wires (distinct from Z and the used A / B wires).

theorem Reversible.cuccaroSub_preserves_B {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (hZ : s L.Z = false) (k : ℕ) (hk : k < n) : denote (cuccaroSub L) s (L.B k) = s (L.B k)

The subtractor preserves the subtrahend register B.

theorem Reversible.cuccaroSub_correct {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (hZ : s L.Z = false) : regValRange L.A (denote (cuccaroSub L) s) n = (regValRange L.A s n + 2 ^ n - regValRange L.B s n) % 2 ^ n

The clean subtractor is value-correct. For s Z = false, register A ends holding (A − B) mod 2ⁿ (in ℕ-truncation-safe form (A + 2ⁿ − B) mod 2ⁿ), in place, with Z restored.

theorem Reversible.cuccaroSub_toffoli {m n : ℕ} (L : CuccaroLayout m n) : (circuitCost (cuccaroSub L)).toffoli = 2 * n

Cost of the subtractor: 2n Toffolis (the gate-reverse of cuccaroAdd).

The modular-adder layout

structure Reversible.CuccaroModLayout (m n : ℕ) : Type

A carry-clean modular-adder layout on m wires for n-bit operands.

• Acc : ℕ → Fin m

  Accumulator / result register (n+1 wires; bit n is the sign / carry-out, kept clean).

• B : ℕ → Fin m

  Addend register (holds b, preserved).

• Nreg : ℕ → Fin m

  Constant register (preset to N, preserved).

• Mask : ℕ → Fin m

  Work register for the masked constant (init/returned 0).

• flag : Fin m

  Comparison flag (init/returned false).

• Z : Fin m

  Cuccaro ancilla (init/returned false).

• hAccB (i j : ℕ) : self.Acc i ≠ self.B j
• hAccN (i j : ℕ) : self.Acc i ≠ self.Nreg j
• hAccM (i j : ℕ) : self.Acc i ≠ self.Mask j
• hBN (i j : ℕ) : self.B i ≠ self.Nreg j
• hBM (i j : ℕ) : self.B i ≠ self.Mask j
• hNM (i j : ℕ) : self.Nreg i ≠ self.Mask j
• hAccflag (i : ℕ) : self.Acc i ≠ self.flag
• hBflag (i : ℕ) : self.B i ≠ self.flag
• hNflag (i : ℕ) : self.Nreg i ≠ self.flag
• hMflag (i : ℕ) : self.Mask i ≠ self.flag
• hAccZ (i : ℕ) : self.Acc i ≠ self.Z
• hBZ (i : ℕ) : self.B i ≠ self.Z
• hNZ (i : ℕ) : self.Nreg i ≠ self.Z
• hMZ (i : ℕ) : self.Mask i ≠ self.Z
• hflagZ : self.flag ≠ self.Z
• hAccinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Acc i = self.Acc j → i = j
• hBinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.B i = self.B j → i = j
• hNinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Nreg i = self.Nreg j → i = j
• hMinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Mask i = self.Mask j → i = j

def Reversible.CuccaroModLayout.layB {m n : ℕ} (L : CuccaroModLayout m n) : CuccaroLayout m (n + 1)

Acc += B Cuccaro layout (width n+1).

Equations

• L.layB = { A := L.Acc, B := L.B, Z := L.Z, hAB := ⋯, hAZ := ⋯, hBZ := ⋯, hAinj := ⋯, hBinj := ⋯ }

def Reversible.CuccaroModLayout.layN {m n : ℕ} (L : CuccaroModLayout m n) : CuccaroLayout m (n + 1)

Acc -= Nreg Cuccaro layout (width n+1).

Equations

• L.layN = { A := L.Acc, B := L.Nreg, Z := L.Z, hAB := ⋯, hAZ := ⋯, hBZ := ⋯, hAinj := ⋯, hBinj := ⋯ }

def Reversible.CuccaroModLayout.layM {m n : ℕ} (L : CuccaroModLayout m n) : CuccaroLayout m (n + 1)

Acc += Mask Cuccaro layout (width n+1).

Equations

• L.layM = { A := L.Acc, B := L.Mask, Z := L.Z, hAB := ⋯, hAZ := ⋯, hBZ := ⋯, hAinj := ⋯, hBinj := ⋯ }

The mask gadget: Mask ^= flag · Nreg

def Reversible.maskCopyPrefix {m n : ℕ} (L : CuccaroModLayout m n) (k : ℕ) : Circuit m

The first k masked-copy gates: CCX flag Nreg[i] Mask[i] for i < k.

Equations

• Reversible.maskCopyPrefix L k = List.map (fun (i : ℕ) => Reversible.Gate.CCX L.flag (L.Nreg i) (L.Mask i)) (List.range k)

def Reversible.maskCopy {m n : ℕ} (L : CuccaroModLayout m n) : Circuit m

The masked copy: all n gates CCX flag Nreg[i] Mask[i]. Self-inverse (applied twice it clears Mask); it realises the conditional reduction without a controlled adder.

Equations

• Reversible.maskCopy L = Reversible.maskCopyPrefix L n

theorem Reversible.maskCopyPrefix_succ {m n : ℕ} (L : CuccaroModLayout m n) (k : ℕ) (s : State m) : denote (maskCopyPrefix L (k + 1)) s = denoteGate (Gate.CCX L.flag (L.Nreg k) (L.Mask k)) (denote (maskCopyPrefix L k) s)

theorem Reversible.maskCopyPrefix_spec {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (k : ℕ) : k ≤ n → (∀ j < k, denote (maskCopyPrefix L k) s (L.Mask j) = (s (L.Mask j) ^^ s L.flag && s (L.Nreg j))) ∧ (∀ (j : ℕ), k ≤ j → j < n + 1 → denote (maskCopyPrefix L k) s (L.Mask j) = s (L.Mask j)) ∧ ∀ (w : Fin m), (∀ j < n, w ≠ L.Mask j) → denote (maskCopyPrefix L k) s w = s w

The mask gadget invariant. After k gates: Mask j (for j < k) holds Mask j ^^ (flag ∧ Nreg j); Mask j for k ≤ j ≤ n is untouched; every non-Mask wire (in particular flag, Nreg, Acc, B, Z) is preserved.

theorem Reversible.maskCopy_Mask {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (j : ℕ) (hj : j < n) : denote (maskCopy L) s (L.Mask j) = (s (L.Mask j) ^^ s L.flag && s (L.Nreg j))

Masked copy, computed clause (j < n).

theorem Reversible.maskCopy_Mask_top {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) : denote (maskCopy L) s (L.Mask n) = s (L.Mask n)

Masked copy, top wire Mask n is untouched.

theorem Reversible.maskCopy_external {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (w : Fin m) (hw : ∀ j < n, w ≠ L.Mask j) : denote (maskCopy L) s w = s w

Masked copy preserves every non-Mask wire.

theorem Reversible.maskCopyPrefix_toffoli {m n : ℕ} (L : CuccaroModLayout m n) (k : ℕ) : (circuitCost (maskCopyPrefix L k)).toffoli = k

theorem Reversible.maskCopy_toffoli {m n : ℕ} (L : CuccaroModLayout m n) : (circuitCost (maskCopy L)).toffoli = n

The modular adder

def Reversible.cuccaroModAdd {m n : ℕ} (L : CuccaroModLayout m n) : Circuit m

The carry-clean modular adder. Nine stages (5 Cuccaro passes + 2 masks + 3 single gates); see the module header for the schematic.

Equations

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

theorem Reversible.cuccaroModAdd_spec {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc n) = false) (hBtop : s (L.B n) = false) (hNtop : s (L.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.Mask j) = false) (hflag : s L.flag = false) (hZ : s L.Z = false) {N a b : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange L.Acc s n = a) (hB : regValRange L.B s n = b) (hN : regValRange L.Nreg s n = N) (haN : a < N) (hbN : b < N) : regValRange L.Acc (denote (cuccaroModAdd L) s) n = (a + b) % N ∧ denote (cuccaroModAdd L) s L.flag = false ∧ (∀ j < n + 1, denote (cuccaroModAdd L) s (L.Mask j) = false) ∧ denote (cuccaroModAdd L) s L.Z = false ∧ denote (cuccaroModAdd L) s (L.Acc n) = false ∧ regValRange L.B (denote (cuccaroModAdd L) s) n = b ∧ regValRange L.Nreg (denote (cuccaroModAdd L) s) n = N ∧ denote (cuccaroModAdd L) s (L.B n) = s (L.B n) ∧ denote (cuccaroModAdd L) s (L.Nreg n) = s (L.Nreg n)

The full nine-stage specification of the carry-clean modular adder: the value Acc = (a + b) mod N, the flag/mask/ancilla/top-bit restorations, and the operand preservations, in one conjunction.

Factoring note (§9.4 review, 2026-08-06). At 313 lines this is the corpus's longest proof, and it was reviewed for stage-lemma extraction under the library-grade standard. Verdict: already maximally factored. Every step is a one-to-three-line citation of a named block lemma (cuccaroAdd_correct, cuccaroSub_correct, maskCopy_*, the *_preserves_* frames); the length is the irreducible bookkeeping of nine stages × five tracked invariants (Acc value, B/Nreg/Mask preservation, flag/ancilla state), organised under the ===== STAGE k ===== banners. Re-packaging into per-stage invariant records was assessed and rejected: the record statements alone would add ~150 lines of boilerplate while every proof step already cites its named lemma — indirection without content.

theorem Reversible.cuccaroModAdd_correct {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc n) = false) (hBtop : s (L.B n) = false) (hNtop : s (L.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.Mask j) = false) (hflag : s L.flag = false) (hZ : s L.Z = false) {N a b : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange L.Acc s n = a) (hB : regValRange L.B s n = b) (hN : regValRange L.Nreg s n = N) (haN : a < N) (hbN : b < N) : regValRange L.Acc (denote (cuccaroModAdd L) s) n = (a + b) % N

Correctness. The carry-clean modular adder leaves Acc = (a + b) mod N.

theorem Reversible.cuccaroModAdd_clean {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc n) = false) (hBtop : s (L.B n) = false) (hNtop : s (L.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.Mask j) = false) (hflag : s L.flag = false) (hZ : s L.Z = false) {N a b : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange L.Acc s n = a) (hB : regValRange L.B s n = b) (hN : regValRange L.Nreg s n = N) (haN : a < N) (hbN : b < N) : denote (cuccaroModAdd L) s L.flag = false ∧ denote (cuccaroModAdd L) s (L.Acc n) = false ∧ (∀ j < n + 1, denote (cuccaroModAdd L) s (L.Mask j) = false) ∧ denote (cuccaroModAdd L) s L.Z = false

The carry-clean property — THE point. Every scratch wire is restored to false: the flag, the carry-out / sign wire Acc[n], every Mask wire, and the Cuccaro ancilla Z. So cuccaroModAdd is ancilla-restoring and reusable in place inside a multiply loop with Θ(n) qubits.

theorem Reversible.cuccaroModAdd_preserves_operand {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc n) = false) (hBtop : s (L.B n) = false) (hNtop : s (L.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.Mask j) = false) (hflag : s L.flag = false) (hZ : s L.Z = false) {N a b : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange L.Acc s n = a) (hB : regValRange L.B s n = b) (hN : regValRange L.Nreg s n = N) (haN : a < N) (hbN : b < N) : regValRange L.B (denote (cuccaroModAdd L) s) n = b ∧ regValRange L.Nreg (denote (cuccaroModAdd L) s) n = N ∧ denote (cuccaroModAdd L) s (L.B n) = s (L.B n) ∧ denote (cuccaroModAdd L) s (L.Nreg n) = s (L.Nreg n)

The addend operand is intact — low value AND top padding wires. B = b and Nreg = N survive the whole circuit (needed for the flag uncompute), and the width-(n+1) top padding wires B[n], Nreg[n] are restored to their input values. The top-wire conclusions are what let a Stage-2b multiply-loop caller re-establish the hBtop : B n = false / hNtop : Nreg n = false preconditions of the next iteration through the public API (F1 repair).

Derived cost: 12n + 10 Toffolis

theorem Reversible.cuccaroModAdd_toffoli {m n : ℕ} (L : CuccaroModLayout m n) : (circuitCost (cuccaroModAdd L)).toffoli = 12 * n + 10

Derived Toffoli cost: 12n + 10. Five carry-out Cuccaro passes at 2(n+1) each (three adds

• two subtractors) plus the two mask gadgets at n each; the three single gates [CX], [CX, X] are free. So 5·2(n+1) + 2n = 12n + 10. The leading 12n matches the dirty ModularAdd.modAdd; the win is the qubit count (Θ(n) reusable, vs Θ(n²) fresh per add), not the Toffoli constant.

Non-vacuity witness + #eval / runArr cross-check (both branches + flag-clean)

A concrete n = 3 layout on Fin 18: Acc → {0,1,2,3} (bit 3 = carry-out), B → {4,5,6,7}, Nreg → {8,9,10,11} (preset N = 3 on wires 8,9), Mask → {12,13,14,15}, flag → 16, Z → 17. n = 3 is forced by 2N ≤ 2ⁿ: for N = 3 that needs 2ⁿ ≥ 6. The strict Array evaluator runArr (with the proven bridge regValRangeArr_eq back to denote) witnesses both branches (1+1 mod 3 = 2, the a+b<N add-back branch; 2+2 mod 3 = 1, the a+b≥N no-add-back branch) and that the flag, the carry-out wire, and the Mask scratch all read clean afterward.

def Reversible.cuccaroModLayout3 : CuccaroModLayout 18 3

A concrete n = 3 carry-clean modular-adder layout on Fin 18.

Equations

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

def Reversible.cuccaroModState3 (a0 a1 a2 b0 b1 b2 : Bool) : State 18

Concrete input state for n = 3, N = 3: Acc = a (wires 0,1,2), B = b (wires 4,5,6), Nreg = 3 (wires 8,9), all scratch / carry-out / flag / ancilla false.

Equations

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

theorem Reversible.cuccaroModState3_pre (a0 a1 a2 b0 b1 b2 : Bool) : cuccaroModState3 a0 a1 a2 b0 b1 b2 (cuccaroModLayout3.Acc 3) = false ∧ cuccaroModState3 a0 a1 a2 b0 b1 b2 (cuccaroModLayout3.B 3) = false ∧ cuccaroModState3 a0 a1 a2 b0 b1 b2 (cuccaroModLayout3.Nreg 3) = false ∧ (∀ j < 3 + 1, cuccaroModState3 a0 a1 a2 b0 b1 b2 (cuccaroModLayout3.Mask j) = false) ∧ cuccaroModState3 a0 a1 a2 b0 b1 b2 cuccaroModLayout3.flag = false ∧ cuccaroModState3 a0 a1 a2 b0 b1 b2 cuccaroModLayout3.Z = false ∧ regValRange cuccaroModLayout3.Nreg (cuccaroModState3 a0 a1 a2 b0 b1 b2) 3 = 3

Structural hypotheses of cuccaroModAdd_correct hold at cuccaroModState3 (clean scratch, Nreg = 3), for any data bits.