The carry-clean (Θ(n)-qubit) MODULAR MULTIPLY X·Y mod N (ECDLP Phase 2, Stage 2b)

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

Stage 2 (CuccaroModAdd.lean) delivered the carry-clean modular ADDER cuccaroModAdd (Acc ← (a + b) mod N, every scratch wire restored). This module folds it into the carry-clean modular MULTIPLY X · Y mod N with ONE reused scratch bank (Θ(n) qubits), versus the dirty ModularMulLoop.mulLoop's Θ(n²) fresh-ancilla model.

Acc = 0; for each bit i of X MSB-first: Acc ← (2·Acc) mod N; Acc ← (Acc + X_i·Y) mod N.

The two clean sub-gadgets (each reuses the SAME scratch bank, re-cleaned per step)

1. cuccaroModDouble — clean Acc ← (2·Acc) mod N. Realised as an in-place shift + conditional subtract (Beauregard), NOT copy-add-uncopy. The copy-add-uncopy route is not clean: the copy register holds a, which cannot be uncomputed once Acc becomes 2a mod N (no register then holds a, and a = halve(2a mod N) needs a halver). The shift rotChain doubles by an information-preserving wire rotation (new[i] = old[i-1], new[0] = old[n] = 0), so there is no scratch to clean from the doubling itself; the mod N reduce reuses the Stage-2 pieces (cuccaroSub, maskCopy, cuccaroAdd). The comparison flag is uncomputed by parity: for odd N (the ECDLP prime case), [2a < N] = ¬(2a mod N) mod 2, so a CX (Acc 0) flag ; X clears it. Load-bearing hypothesis: N odd.
2. cuccaroCModAdd — clean bit-gated Acc ← (Acc + X_i·Y) mod N. The masked-operand trick: Mask2 ^= X_i·Y (maskCopyCtrl, n CCXs), run cuccaroModAdd with addend Mask2, then uncompute Mask2 ^= X_i·Y. Because X_i and Y are preserved by the modular add, the mask uncomputes cleanly. This avoids a controlled adder.

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

• cuccaroModDouble_correct / _clean / _preserves_Nreg / _toffoli (= 6n + 4).
• cuccaroCModAdd_correct / _clean / _preserves_operand / _toffoli (= 14n + 10).
• cuccaroModMul_correct — general n: Acc ← (X · Yval) mod N.
• cuccaroModMul_clean — the shared scratch bank restored (so the Θ(n) reuse is real).
• cuccaroModMul_preserves_XY — X, Y intact.
• cuccaroModMul_toffoli — (20n + 14)·n = 20n² + 14n (the headline; per-step 20n + 14).

Honest cost / scope

Per-multiply Toffoli 20n² + 14n (NOT the ~2n² of a non-modular multiply: the mod N reduce per step is irreducible in this measurement-free CCX-only DSL). The prize is Θ(n) reusable qubits (ONE shared scratch bank mod) vs the dirty mulLoop's Θ(n²) fresh ancilla; the per-multiply Toffoli is also ~1.5× better than the dirty 30n². This is the verified modular field-multiply atom; the elliptic-curve point op is a later stage. Load-bearing hypothesis: N odd (the parity flag-uncompute in the doubler), which holds for the ECDLP prime field.

The in-place left-shift (doubling) rotation rotChain

rotChain f k is the top-down adjacent-swap chain swap(f k, f(k-1)) :: ... :: swap(f 1, f 0). It realises the cyclic up-rotation of the block [0, k]: new[i] = old[i-1] for 1 ≤ i ≤ k, new[0] = old[k]. With old[k] = false this is multiplication by 2 of the low k bits.

def Reversible.rotChain {m : ℕ} (f : ℕ → Fin m) : ℕ → Circuit m

Top-down adjacent-swap chain on register f (length k).

Equations

• Reversible.rotChain f 0 = []
• Reversible.rotChain f k.succ = Reversible.Gate.swap (f (k + 1)) (f k) :: Reversible.rotChain f k

theorem Reversible.rotChain_external {m : ℕ} (f : ℕ → Fin m) (k : ℕ) (s : State m) (w : Fin m) (hw : ∀ j ≤ k, w ≠ f j) : denote (rotChain f k) s w = s w

A wire distinct from every f j (j ≤ k) survives rotChain f k.

theorem Reversible.rotChain_apply {m : ℕ} (f : ℕ → Fin m) (k : ℕ) (s : State m) : (∀ (i j : ℕ), i ≤ k → j ≤ k → f i = f j → i = j) → denote (rotChain f k) s (f 0) = s (f k) ∧ ∀ (i : ℕ), 1 ≤ i → i ≤ k → denote (rotChain f k) s (f i) = s (f (i - 1))

The rotation action. With f injective on [0, k]: after rotChain f k, wire f 0 holds s (f k) and wire f i (for 1 ≤ i ≤ k) holds s (f (i-1)).

theorem Reversible.rotChain_value {m : ℕ} (f : ℕ → Fin m) (s : State m) (k : ℕ) (hinj : ∀ (i j : ℕ), i ≤ k → j ≤ k → f i = f j → i = j) (htop : s (f k) = false) : regValRange f (denote (rotChain f k) s) (k + 1) = 2 * regValRange f s k

The rotation doubles. With f injective on [0, k] and s (f k) = false: regValRange f (denote (rotChain f k) s) (k+1) = 2 * regValRange f s k.

theorem Reversible.rotChain_toffoli {m : ℕ} (f : ℕ → Fin m) (k : ℕ) : (circuitCost (rotChain f k)).toffoli = 0

Cost of the rotation: zero Toffoli (it is k swaps, each 3 CNOTs).

The clean modular doubler cuccaroModDouble

Reuses the Stage-2 layout CuccaroModLayout (register B is unused by the doubler). The reduce pieces (cuccaroSub L.layN, maskCopy L, cuccaroAdd L.layM) are exactly those of cuccaroModAdd. The flag uncompute is CX (Acc 0) flag ; X flag (parity, odd N).

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

The carry-clean modular doubler Acc ← (2·Acc) mod N. Seven stages: rotate (×2), subtract N, copy sign to flag, mask N, add back, unmask, parity-uncompute the flag.

Equations

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

theorem Reversible.cuccaroModDouble_spec {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc 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 : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hAcc : regValRange L.Acc s n = a) (hN : regValRange L.Nreg s n = N) (haN : a < N) : regValRange L.Acc (denote (cuccaroModDouble L) s) n = 2 * a % N ∧ denote (cuccaroModDouble L) s L.flag = false ∧ (∀ j < n + 1, denote (cuccaroModDouble L) s (L.Mask j) = false) ∧ denote (cuccaroModDouble L) s L.Z = false ∧ denote (cuccaroModDouble L) s (L.Acc n) = false ∧ regValRange L.Nreg (denote (cuccaroModDouble L) s) n = N ∧ denote (cuccaroModDouble L) s (L.Nreg n) = s (L.Nreg n)

The full doubler spec (value + every scratch wire clean + Nreg preserved).

theorem Reversible.cuccaroModDouble_correct {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc 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 : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hAcc : regValRange L.Acc s n = a) (hN : regValRange L.Nreg s n = N) (haN : a < N) : regValRange L.Acc (denote (cuccaroModDouble L) s) n = 2 * a % N

Correctness. cuccaroModDouble leaves Acc = (2·a) mod N.

theorem Reversible.cuccaroModDouble_clean {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc 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 : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hAcc : regValRange L.Acc s n = a) (hN : regValRange L.Nreg s n = N) (haN : a < N) : denote (cuccaroModDouble L) s L.flag = false ∧ denote (cuccaroModDouble L) s (L.Acc n) = false ∧ (∀ j < n + 1, denote (cuccaroModDouble L) s (L.Mask j) = false) ∧ denote (cuccaroModDouble L) s L.Z = false

The doubler is carry-clean. Flag, carry-out Acc[n], every Mask, and Z restored.

theorem Reversible.cuccaroModDouble_preserves_Nreg {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hAccTop : s (L.Acc 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 : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hAcc : regValRange L.Acc s n = a) (hN : regValRange L.Nreg s n = N) (haN : a < N) : regValRange L.Nreg (denote (cuccaroModDouble L) s) n = N ∧ denote (cuccaroModDouble L) s (L.Nreg n) = s (L.Nreg n)

Nreg is preserved (low value and top padding wire).

theorem Reversible.cuccaroModDouble_toffoli {m n : ℕ} (L : CuccaroModLayout m n) : (circuitCost (cuccaroModDouble L)).toffoli = 6 * n + 4

Derived Toffoli cost: 6n + 4. Rotation 0 (swaps, no Toffoli), subtract 2(n+1), mask n, add 2(n+1), mask n, single gates 0: 2(n+1) + n + 2(n+1) + n = 6n + 4.

Two cuccaroModAdd frame lemmas (external wires + per-wire B)

cuccaroModAdd exports only regValRange-level operand preservation; the bit-gated adder needs (a) preservation of wires entirely outside the modular adder (for the read-only Y / ctrl), and (b) per-wire restoration of the addend register B (for the masked-operand uncompute). Both compose the per-stage frame lemmas; the ancilla Z stays clean throughout (the per-stage _preserves_Z lemmas are unconditional).

theorem Reversible.cuccaroModAdd_preserves_external {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (w : Fin m) (hAcc : ∀ (j : ℕ), w ≠ L.Acc j) (hB : ∀ (j : ℕ), w ≠ L.B j) (hNg : ∀ (j : ℕ), w ≠ L.Nreg j) (hM : ∀ (j : ℕ), w ≠ L.Mask j) (hflag : w ≠ L.flag) (hZ : w ≠ L.Z) : denote (cuccaroModAdd L) s w = s w

A wire disjoint from every modular-adder family (Acc, B, Nreg, Mask, flag, Z) survives cuccaroModAdd.

theorem Reversible.cuccaroModAdd_preserves_B_wire {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (hZ : s L.Z = false) (k : ℕ) (hk : k < n + 1) : denote (cuccaroModAdd L) s (L.B k) = s (L.B k)

Per-wire restoration of the addend B. Each B k (k < n + 1) is returned to its input value (the carries threaded through it during the three cuccaroAdd L.layB / two cuccaroSub L.layB passes are restored). Needs only s Z = false.

The control-masked copy maskCopyCtrl

Mask2 ^= ctrl · Y via n Toffolis CCX ctrl (Y i) (B i) (the addend register B plays the role of Mask2). Mirrors maskCopy with (flag, Nreg, Mask) ↦ (ctrl, Y, B).

def Reversible.maskCopyCtrlPrefix {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (k : ℕ) : Circuit m

First k masked-copy gates CCX ctrl (Y i) (B i).

Equations

• Reversible.maskCopyCtrlPrefix L Y ctrl k = List.map (fun (i : ℕ) => Reversible.Gate.CCX ctrl (Y i) (L.B i)) (List.range k)

def Reversible.maskCopyCtrl {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) : Circuit m

The full control-masked copy: Mask2 = B ^= ctrl · Y on all n low wires. Self-inverse.

Equations

• Reversible.maskCopyCtrl L Y ctrl = Reversible.maskCopyCtrlPrefix L Y ctrl n

theorem Reversible.maskCopyCtrlPrefix_succ {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (k : ℕ) (s : State m) : denote (maskCopyCtrlPrefix L Y ctrl (k + 1)) s = denoteGate (Gate.CCX ctrl (Y k) (L.B k)) (denote (maskCopyCtrlPrefix L Y ctrl k) s)

theorem Reversible.maskCopyCtrlPrefix_spec {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (s : State m) (hctrlB : ∀ (j : ℕ), ctrl ≠ L.B j) (hYB : ∀ (i j : ℕ), Y i ≠ L.B j) (k : ℕ) : k ≤ n → (∀ j < k, denote (maskCopyCtrlPrefix L Y ctrl k) s (L.B j) = (s (L.B j) ^^ s ctrl && s (Y j))) ∧ (∀ (j : ℕ), k ≤ j → j < n + 1 → denote (maskCopyCtrlPrefix L Y ctrl k) s (L.B j) = s (L.B j)) ∧ ∀ (w : Fin m), (∀ j < n, w ≠ L.B j) → denote (maskCopyCtrlPrefix L Y ctrl k) s w = s w

The control-masked-copy invariant. After k gates: B j (j < k) holds B j ^^ (ctrl ∧ Y j); B j (k ≤ j ≤ n) is untouched; every non-B wire is preserved.

theorem Reversible.maskCopyCtrl_B {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (s : State m) (hctrlB : ∀ (j : ℕ), ctrl ≠ L.B j) (hYB : ∀ (i j : ℕ), Y i ≠ L.B j) (j : ℕ) (hj : j < n) : denote (maskCopyCtrl L Y ctrl) s (L.B j) = (s (L.B j) ^^ s ctrl && s (Y j))

maskCopyCtrl computed clause (j < n).

theorem Reversible.maskCopyCtrl_B_top {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (s : State m) (hctrlB : ∀ (j : ℕ), ctrl ≠ L.B j) (hYB : ∀ (i j : ℕ), Y i ≠ L.B j) : denote (maskCopyCtrl L Y ctrl) s (L.B n) = s (L.B n)

maskCopyCtrl top wire B n untouched.

theorem Reversible.maskCopyCtrl_external {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (s : State m) (hctrlB : ∀ (j : ℕ), ctrl ≠ L.B j) (hYB : ∀ (i j : ℕ), Y i ≠ L.B j) (w : Fin m) (hw : ∀ j < n, w ≠ L.B j) : denote (maskCopyCtrl L Y ctrl) s w = s w

maskCopyCtrl preserves every non-B wire.

theorem Reversible.maskCopyCtrlPrefix_toffoli {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (k : ℕ) : (circuitCost (maskCopyCtrlPrefix L Y ctrl k)).toffoli = k

theorem Reversible.maskCopyCtrl_toffoli {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) : (circuitCost (maskCopyCtrl L Y ctrl)).toffoli = n

theorem Reversible.maskCopyCtrl_value {m n : ℕ} (L : CuccaroModLayout m n) (Y : ℕ → Fin m) (ctrl : Fin m) (s : State m) (hctrlB : ∀ (j : ℕ), ctrl ≠ L.B j) (hYB : ∀ (i j : ℕ), Y i ≠ L.B j) (hB0 : ∀ j < n, s (L.B j) = false) : regValRange L.B (denote (maskCopyCtrl L Y ctrl) s) n = if s ctrl = true then regValRange Y s n else 0

maskCopyCtrl value: with B initially 0, Mask2 = B ends holding if ctrl then y else 0 where y = regValRange Y s n.

The clean bit-gated modular adder cuccaroCModAdd

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

Bundled layout for the clean conditional modular add: the Stage-2 modular-adder layout mod (its addend register mod.B is the masked operand Mask2), plus the read-only multiplicand Y and the gating bit ctrl, disjoint from everything mod touches.

• mod : CuccaroModLayout m n

  The carry-clean modular-adder layout (mod.B = the masked operand Mask2).

• Y : ℕ → Fin m

  The read-only multiplicand register (n bits).

• ctrl : Fin m

  The gating bit.

• hYAcc (i j : ℕ) : self.Y i ≠ self.mod.Acc j
• hYB (i j : ℕ) : self.Y i ≠ self.mod.B j
• hYN (i j : ℕ) : self.Y i ≠ self.mod.Nreg j
• hYM (i j : ℕ) : self.Y i ≠ self.mod.Mask j
• hYflag (i : ℕ) : self.Y i ≠ self.mod.flag
• hYZ (i : ℕ) : self.Y i ≠ self.mod.Z
• hctrlAcc (j : ℕ) : self.ctrl ≠ self.mod.Acc j
• hctrlB (j : ℕ) : self.ctrl ≠ self.mod.B j
• hctrlN (j : ℕ) : self.ctrl ≠ self.mod.Nreg j
• hctrlM (j : ℕ) : self.ctrl ≠ self.mod.Mask j
• hctrlflag : self.ctrl ≠ self.mod.flag
• hctrlZ : self.ctrl ≠ self.mod.Z

def Reversible.cuccaroCModAdd {m n : ℕ} (K : CuccaroCModLayout m n) : Circuit m

The carry-clean bit-gated modular adder Acc ← (Acc + (if ctrl then Y else 0)) mod N. Mask the operand into Mask2 = mod.B, run cuccaroModAdd, uncompute the mask.

Equations

• Reversible.cuccaroCModAdd K = Reversible.maskCopyCtrl K.mod K.Y K.ctrl ++ Reversible.cuccaroModAdd K.mod ++ Reversible.maskCopyCtrl K.mod K.Y K.ctrl

theorem Reversible.cuccaroCModAdd_spec {m n : ℕ} (K : CuccaroCModLayout m n) (s : State m) (hAccTop : s (K.mod.Acc n) = false) (hBtop : ∀ j < n + 1, s (K.mod.B j) = false) (hNtop : s (K.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (K.mod.Mask j) = false) (hflag : s K.mod.flag = false) (hZ : s K.mod.Z = false) {N a y : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange K.mod.Acc s n = a) (hN : regValRange K.mod.Nreg s n = N) (haN : a < N) (hYval : regValRange K.Y s n = y) (hyN : y < N) : regValRange K.mod.Acc (denote (cuccaroCModAdd K) s) n = (a + if s K.ctrl = true then y else 0) % N ∧ denote (cuccaroCModAdd K) s K.mod.flag = false ∧ denote (cuccaroCModAdd K) s (K.mod.Acc n) = false ∧ (∀ j < n + 1, denote (cuccaroCModAdd K) s (K.mod.Mask j) = false) ∧ (∀ j < n + 1, denote (cuccaroCModAdd K) s (K.mod.B j) = false) ∧ denote (cuccaroCModAdd K) s K.mod.Z = false ∧ regValRange K.Y (denote (cuccaroCModAdd K) s) n = y ∧ denote (cuccaroCModAdd K) s K.ctrl = s K.ctrl ∧ regValRange K.mod.Nreg (denote (cuccaroCModAdd K) s) n = N ∧ denote (cuccaroCModAdd K) s (K.mod.Nreg n) = s (K.mod.Nreg n)

The full bit-gated-adder spec (value + all scratch incl. Mask2 clean + Y / ctrl / Nreg preserved).

theorem Reversible.cuccaroCModAdd_correct {m n : ℕ} (K : CuccaroCModLayout m n) (s : State m) (hAccTop : s (K.mod.Acc n) = false) (hBtop : ∀ j < n + 1, s (K.mod.B j) = false) (hNtop : s (K.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (K.mod.Mask j) = false) (hflag : s K.mod.flag = false) (hZ : s K.mod.Z = false) {N a y : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange K.mod.Acc s n = a) (hN : regValRange K.mod.Nreg s n = N) (haN : a < N) (hYval : regValRange K.Y s n = y) (hyN : y < N) : regValRange K.mod.Acc (denote (cuccaroCModAdd K) s) n = (a + if s K.ctrl = true then y else 0) % N

Correctness. The bit-gated modular adder leaves Acc = (a + (if ctrl then y else 0)) mod N.

theorem Reversible.cuccaroCModAdd_clean {m n : ℕ} (K : CuccaroCModLayout m n) (s : State m) (hAccTop : s (K.mod.Acc n) = false) (hBtop : ∀ j < n + 1, s (K.mod.B j) = false) (hNtop : s (K.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (K.mod.Mask j) = false) (hflag : s K.mod.flag = false) (hZ : s K.mod.Z = false) {N a y : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange K.mod.Acc s n = a) (hN : regValRange K.mod.Nreg s n = N) (haN : a < N) (hYval : regValRange K.Y s n = y) (hyN : y < N) : denote (cuccaroCModAdd K) s K.mod.flag = false ∧ denote (cuccaroCModAdd K) s (K.mod.Acc n) = false ∧ (∀ j < n + 1, denote (cuccaroCModAdd K) s (K.mod.Mask j) = false) ∧ (∀ j < n + 1, denote (cuccaroCModAdd K) s (K.mod.B j) = false) ∧ denote (cuccaroCModAdd K) s K.mod.Z = false

The bit-gated adder is carry-clean, including the masked operand Mask2 = mod.B.

theorem Reversible.cuccaroCModAdd_preserves_operand {m n : ℕ} (K : CuccaroCModLayout m n) (s : State m) (hAccTop : s (K.mod.Acc n) = false) (hBtop : ∀ j < n + 1, s (K.mod.B j) = false) (hNtop : s (K.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (K.mod.Mask j) = false) (hflag : s K.mod.flag = false) (hZ : s K.mod.Z = false) {N a y : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hAcc : regValRange K.mod.Acc s n = a) (hN : regValRange K.mod.Nreg s n = N) (haN : a < N) (hYval : regValRange K.Y s n = y) (hyN : y < N) : regValRange K.Y (denote (cuccaroCModAdd K) s) n = y ∧ denote (cuccaroCModAdd K) s K.ctrl = s K.ctrl ∧ regValRange K.mod.Nreg (denote (cuccaroCModAdd K) s) n = N

The operand is preserved: Y, ctrl, and Nreg survive.

theorem Reversible.cuccaroCModAdd_toffoli {m n : ℕ} (K : CuccaroCModLayout m n) : (circuitCost (cuccaroCModAdd K)).toffoli = 14 * n + 10

Derived Toffoli cost: 14n + 10. Two control-masks (n CCX each) + the modular adder (12n + 10): n + (12n + 10) + n = 14n + 10.

theorem Reversible.cuccaroModDouble_preserves_external {m n : ℕ} (L : CuccaroModLayout m n) (s : State m) (w : Fin m) (hAcc : ∀ (j : ℕ), w ≠ L.Acc j) (hNg : ∀ (j : ℕ), w ≠ L.Nreg j) (hM : ∀ (j : ℕ), w ≠ L.Mask j) (hflag : w ≠ L.flag) (hZ : w ≠ L.Z) : denote (cuccaroModDouble L) s w = s w

A wire disjoint from Acc, Nreg, Mask, flag, Z survives cuccaroModDouble (it touches no other families; the addend register B is not used by the doubler).

theorem Reversible.cuccaroCModAdd_preserves_external {m n : ℕ} (K : CuccaroCModLayout m n) (s : State m) (w : Fin m) (hAcc : ∀ (j : ℕ), w ≠ K.mod.Acc j) (hB : ∀ (j : ℕ), w ≠ K.mod.B j) (hNg : ∀ (j : ℕ), w ≠ K.mod.Nreg j) (hM : ∀ (j : ℕ), w ≠ K.mod.Mask j) (hflag : w ≠ K.mod.flag) (hZ : w ≠ K.mod.Z) : denote (cuccaroCModAdd K) s w = s w

A wire disjoint from Acc, B, Nreg, Mask, flag, Z survives cuccaroCModAdd (the read-only Y and ctrl are never written).

The carry-clean modular multiply: the Horner fold with ONE reused scratch bank

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

An n-bit carry-clean modular-multiply layout on Fin m: a single Stage-2 modular-adder layout mod (its addend register mod.B is the shared masked-operand scratch Mask2), a multiplicand register Y, and a multiplier register X. Both Y and X are disjoint from everything mod touches; X is injective on [0, n). This is ONE shared scratch bank — mod (with its Acc, B, Nreg, Mask, flag, Z) is reused across all n Horner steps (Θ(n) qubits, not Θ(n²)).

• mod : CuccaroModLayout m n

  The shared carry-clean modular-adder layout (mod.B = the reused masked-operand scratch).

• Y : ℕ → Fin m

  The multiplicand register Y (read-only, n bits).

• X : ℕ → Fin m

  The multiplier register X (read-only control bits; bit n-1-j gates step j).

• hYAcc (i j : ℕ) : self.Y i ≠ self.mod.Acc j
• hYB (i j : ℕ) : self.Y i ≠ self.mod.B j
• hYN (i j : ℕ) : self.Y i ≠ self.mod.Nreg j
• hYM (i j : ℕ) : self.Y i ≠ self.mod.Mask j
• hYflag (i : ℕ) : self.Y i ≠ self.mod.flag
• hYZ (i : ℕ) : self.Y i ≠ self.mod.Z
• hXAcc (i j : ℕ) : self.X i ≠ self.mod.Acc j
• hXB (i j : ℕ) : self.X i ≠ self.mod.B j
• hXN (i j : ℕ) : self.X i ≠ self.mod.Nreg j
• hXM (i j : ℕ) : self.X i ≠ self.mod.Mask j
• hXflag (i : ℕ) : self.X i ≠ self.mod.flag
• hXZ (i : ℕ) : self.X i ≠ self.mod.Z

def Reversible.CuccaroMulLayout.cmod {m n : ℕ} (L : CuccaroMulLayout m n) (j : ℕ) : CuccaroCModLayout m n

The bit-gated-adder layout for step j (its gate is bit X (n-1-j), MSB-first).

Equations

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

def Reversible.cuccaroModMulStep {m n : ℕ} (L : CuccaroMulLayout m n) (j : ℕ) : Circuit m

One Horner step on the shared bank: double the accumulator, then bit-gated-add X_{n-1-j}·Y.

Equations

• Reversible.cuccaroModMulStep L j = Reversible.cuccaroModDouble L.mod ++ Reversible.cuccaroCModAdd (L.cmod j)

def Reversible.cuccaroModMul {m n : ℕ} (L : CuccaroMulLayout m n) : Circuit m

The general-n carry-clean modular multiply: fold the Horner step over the n multiplier bits MSB-first, reusing the single scratch bank mod.

Equations

• Reversible.cuccaroModMul L = List.flatMap id (List.map (fun (j : ℕ) => Reversible.cuccaroModMulStep L j) (List.range n))

def Reversible.cuccaroModMulUpto {m n : ℕ} (L : CuccaroMulLayout m n) (k : ℕ) : Circuit m

The first k Horner steps (the induction handle).

Equations

• Reversible.cuccaroModMulUpto L k = List.flatMap id (List.map (fun (j : ℕ) => Reversible.cuccaroModMulStep L j) (List.range k))

theorem Reversible.cuccaroModMul_eq_upto {m n : ℕ} (L : CuccaroMulLayout m n) : cuccaroModMul L = cuccaroModMulUpto L n

theorem Reversible.cuccaroModMulUpto_succ {m n : ℕ} (L : CuccaroMulLayout m n) (k : ℕ) : cuccaroModMulUpto L (k + 1) = cuccaroModMulUpto L k ++ cuccaroModMulStep L k

theorem Reversible.cuccaroModMul_invariant {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) (hAccTop : s (L.mod.Acc n) = false) (hNtop : s (L.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.mod.Mask j) = false) (hB0 : ∀ j < n + 1, s (L.mod.B j) = false) (hflag : s L.mod.flag = false) (hZ : s L.mod.Z = false) {N y : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hNpos : 0 < N) (hyN : y < N) (hAcc0 : regValRange L.mod.Acc s n = 0) (hNval : regValRange L.mod.Nreg s n = N) (hYval : regValRange L.Y s n = y) (k : ℕ) : k ≤ n → regValRange L.mod.Acc (denote (cuccaroModMulUpto L k) s) n = hornerVal (fun (i : ℕ) => if s (L.X i) = true then 1 else 0) n k * y % N ∧ denote (cuccaroModMulUpto L k) s (L.mod.Acc n) = false ∧ denote (cuccaroModMulUpto L k) s L.mod.flag = false ∧ (∀ j < n + 1, denote (cuccaroModMulUpto L k) s (L.mod.Mask j) = false) ∧ (∀ j < n + 1, denote (cuccaroModMulUpto L k) s (L.mod.B j) = false) ∧ denote (cuccaroModMulUpto L k) s L.mod.Z = false ∧ regValRange L.mod.Nreg (denote (cuccaroModMulUpto L k) s) n = N ∧ denote (cuccaroModMulUpto L k) s (L.mod.Nreg n) = false ∧ regValRange L.Y (denote (cuccaroModMulUpto L k) s) n = y ∧ ∀ (i : ℕ), denote (cuccaroModMulUpto L k) s (L.X i) = s (L.X i)

The multiply-loop invariant. After the first k Horner steps from a clean bank (Acc = 0), the accumulator holds (hornerVal bits n k · y) mod N (bits i = [X i]), the whole scratch bank is restored clean, and Nreg, Y, every X bit are intact. By induction on k.

theorem Reversible.cuccaroModMul_correct {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) (hAccTop : s (L.mod.Acc n) = false) (hNtop : s (L.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.mod.Mask j) = false) (hB0 : ∀ j < n + 1, s (L.mod.B j) = false) (hflag : s L.mod.flag = false) (hZ : s L.mod.Z = false) {N Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hNpos : 0 < N) (hyN : Yval < N) (hAcc0 : regValRange L.mod.Acc s n = 0) (hNval : regValRange L.mod.Nreg s n = N) (hYval : regValRange L.Y s n = Yval) : regValRange L.mod.Acc (denote (cuccaroModMul L) s) n = regValRange L.X s n * Yval % N

The verified general-n carry-clean modular multiply. From a clean shared bank (Acc = 0, all scratch false, Nreg = N, Y = Yval < N, 2N ≤ 2ⁿ, N odd), the loop leaves the accumulator holding (X · Yval) mod N, with the multiplier X arbitrary.

theorem Reversible.cuccaroModMul_clean {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) (hAccTop : s (L.mod.Acc n) = false) (hNtop : s (L.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.mod.Mask j) = false) (hB0 : ∀ j < n + 1, s (L.mod.B j) = false) (hflag : s L.mod.flag = false) (hZ : s L.mod.Z = false) {N Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hNpos : 0 < N) (hyN : Yval < N) (hAcc0 : regValRange L.mod.Acc s n = 0) (hNval : regValRange L.mod.Nreg s n = N) (hYval : regValRange L.Y s n = Yval) : denote (cuccaroModMul L) s (L.mod.Acc n) = false ∧ denote (cuccaroModMul L) s L.mod.flag = false ∧ (∀ j < n + 1, denote (cuccaroModMul L) s (L.mod.Mask j) = false) ∧ (∀ j < n + 1, denote (cuccaroModMul L) s (L.mod.B j) = false) ∧ denote (cuccaroModMul L) s L.mod.Z = false

The shared scratch bank is restored clean (so the Θ(n) reuse is real): the carry-out Acc[n], flag, every Mask, every Mask2 = mod.B, and Z all return to false.

theorem Reversible.cuccaroModMul_preserves_XY {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) (hAccTop : s (L.mod.Acc n) = false) (hNtop : s (L.mod.Nreg n) = false) (hMask0 : ∀ j < n + 1, s (L.mod.Mask j) = false) (hB0 : ∀ j < n + 1, s (L.mod.B j) = false) (hflag : s L.mod.flag = false) (hZ : s L.mod.Z = false) {N Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hNpos : 0 < N) (hyN : Yval < N) (hAcc0 : regValRange L.mod.Acc s n = 0) (hNval : regValRange L.mod.Nreg s n = N) (hYval : regValRange L.Y s n = Yval) : (∀ (i : ℕ), denote (cuccaroModMul L) s (L.X i) = s (L.X i)) ∧ regValRange L.Y (denote (cuccaroModMul L) s) n = Yval ∧ regValRange L.mod.Nreg (denote (cuccaroModMul L) s) n = N

X and Y are intact (and Nreg = N): the multiplier / multiplicand survive the multiply.

Derived cost: (20n + 14)·n = 20n² + 14n Toffolis

theorem Reversible.cuccaroModMulStep_toffoli {m n : ℕ} (L : CuccaroMulLayout m n) (j : ℕ) : (circuitCost (cuccaroModMulStep L j)).toffoli = 20 * n + 14

theorem Reversible.cuccaroModMulUpto_toffoli {m n : ℕ} (L : CuccaroMulLayout m n) (k : ℕ) : (circuitCost (cuccaroModMulUpto L k)).toffoli = (20 * n + 14) * k

theorem Reversible.cuccaroModMul_toffoli {m n : ℕ} (L : CuccaroMulLayout m n) : (circuitCost (cuccaroModMul L)).toffoli = (20 * n + 14) * n

Derived Toffoli cost: (20n + 14)·n = 20n² + 14n. n Horner steps, each 20n + 14 (doubler 6n + 4 + bit-gated adder 14n + 10). The prize is the Θ(n) reusable qubit count (one shared scratch bank), not the Toffoli constant (modular reduction per step is irreducible in this measurement-free CCX-only DSL); still ~1.5× better than the dirty mulLoop's 30n².

Non-vacuity witness + #eval / runArr cross-check (n = 3, N = 3)

A concrete CuccaroMulLayout 24 3: Acc → {0,1,2,3}, the shared masked-operand scratch Mask2 = mod.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, multiplicand Y → {18,19,20} (preset 2 on wire 19), multiplier X → {21,22,23}. n = 3 is forced by 2N ≤ 2ⁿ (N = 3 needs 2ⁿ ≥ 6). The witnesses realise X · 2 mod 3: X = 3 ↦ 0, X = 2 ↦ 1, X = 1 ↦ 2, read off the strict Array evaluator (runArr, via regValRangeArr_eq), with the shared scratch reading clean afterward.

def Reversible.cuccaroMulModLayout3 : CuccaroModLayout 24 3

A concrete n = 3 carry-clean modular-adder layout on Fin 24 (the shared bank).

Equations

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

Interface lemmas (CONVENTIONS §9.1, F1): the wire assignments of the concrete layout, one lemma per field.

theorem Reversible.cuccaroMulModLayout3_Acc (i : ℕ) : cuccaroMulModLayout3.Acc i = if i = 0 then 0 else if i = 1 then 1 else if i = 2 then 2 else 3

cuccaroMulModLayout3's accumulator wires.

theorem Reversible.cuccaroMulModLayout3_B (i : ℕ) : cuccaroMulModLayout3.B i = if i = 0 then 4 else if i = 1 then 5 else if i = 2 then 6 else 7

cuccaroMulModLayout3's addend wires.

theorem Reversible.cuccaroMulModLayout3_Nreg (i : ℕ) : cuccaroMulModLayout3.Nreg i = if i = 0 then 8 else if i = 1 then 9 else if i = 2 then 10 else 11

cuccaroMulModLayout3's modulus-register wires.

theorem Reversible.cuccaroMulModLayout3_Mask (i : ℕ) : cuccaroMulModLayout3.Mask i = if i = 0 then 12 else if i = 1 then 13 else if i = 2 then 14 else 15

cuccaroMulModLayout3's mask-register wires.

theorem Reversible.cuccaroMulModLayout3_flag : cuccaroMulModLayout3.flag = 16

cuccaroMulModLayout3's comparison-flag wire.

theorem Reversible.cuccaroMulModLayout3_Z : cuccaroMulModLayout3.Z = 17

cuccaroMulModLayout3's borrow/carry ancilla wire.

def Reversible.cuccaroMulLayout3 : CuccaroMulLayout 24 3

A concrete n = 3 carry-clean modular-multiply layout on Fin 24.

Equations

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

def Reversible.cuccaroMulState3 (x0 x1 x2 : Bool) : State 24

Input state for n = 3, N = 3, Y = 2: Nreg = 3 (wires 8,9), Y = 2 (wire 19), multiplier X bits x0,x1,x2 (wires 21,22,23), all of Acc / Mask2 / Mask / flag / Z clean.

Equations

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

theorem Reversible.cuccaroMulState3_pre (x0 x1 x2 : Bool) : cuccaroMulState3 x0 x1 x2 (cuccaroMulLayout3.mod.Acc 3) = false ∧ cuccaroMulState3 x0 x1 x2 (cuccaroMulLayout3.mod.Nreg 3) = false ∧ (∀ j < 3 + 1, cuccaroMulState3 x0 x1 x2 (cuccaroMulLayout3.mod.Mask j) = false) ∧ (∀ j < 3 + 1, cuccaroMulState3 x0 x1 x2 (cuccaroMulLayout3.mod.B j) = false) ∧ cuccaroMulState3 x0 x1 x2 cuccaroMulLayout3.mod.flag = false ∧ cuccaroMulState3 x0 x1 x2 cuccaroMulLayout3.mod.Z = false ∧ regValRange cuccaroMulLayout3.mod.Acc (cuccaroMulState3 x0 x1 x2) 3 = 0 ∧ regValRange cuccaroMulLayout3.mod.Nreg (cuccaroMulState3 x0 x1 x2) 3 = 3 ∧ regValRange cuccaroMulLayout3.Y (cuccaroMulState3 x0 x1 x2) 3 = 2

The structural preconditions of cuccaroModMul_correct hold at cuccaroMulState3.