A carry-clean adder-parametric modular multiplier (ECDLP Phase 2, Stage S6.3-36b)

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

This module is the carry-clean (Θ(n)-qubit) counterpart of the fresh-ancilla keystone 36a (VerifiedAdder). It bundles the carry-clean multiplier fold's consumption surface into a structure VerifiedAdderCarryClean, proves the multiply correct + cost it once, parametric over any conforming restored-clean step, and exhibits the existing carry-clean Cuccaro multiply (cuccaroModMul, Stage 2b) as the faithfulness instance — recovering its proven (X · Y) mod N correctness and 20·n² + 14·n Toffoli figure exactly.

The restored-clean discipline (the crux vs 36a)

36a's VerifiedAdder models the FRESH-ANCILLA memory model: each bank has a PRIVATE clean predicate clean k s with a precondition-free inter-bank frame cleanStable (bank j never touches bank k's ancilla). That is exactly wrong for the carry-clean multiply, which reuses ONE scratch bank across all n Horner steps. Modelling that single bank as n independently-fresh banks would make the Θ(n)-qubit win vacuous.

So this variant carries a GLOBAL cleanliness predicate clean : State m → Prop (one bank, no per-bank index) under a restored-clean discipline: each step has clean as a PRECONDITION of both its value correctness and its cleanliness, and RE-ESTABLISHES clean as a POSTCONDITION (cleanRestored). The fold maintains "the bank is clean" as a loop invariant (clean in → step → clean out), threaded step to step — not "all banks independently clean throughout". This is the genuine single-bank-reuse invariant; cf. cuccaroModMul_clean (the all-scratch-restored property that enables the reuse).

What is proved

• VerifiedAdderCarryClean — the structure with the restored-clean fields (correct / cleanRestored / presY all gated on clean s, digitStable, digit, toffoli, hNpos, hToffoli).
• genMulCC / genMulCC_correct — the multiplier fold + its correctness acc = (accVal digit · y) mod N, the same induction as cuccaroModMul_invariant, now citing the abstract fields with the restored-clean loop invariant. REUSES accVal / accVal_mod_step / accVal_succ from 36a UNCHANGED.
• genMulCC_clean — the shared bank restored after the full multiply (the Θ(n) reuse is real).
• genMulCC_toffoli — the cost recurrence n · step.toffoli.
• cuccaroAdder — the faithfulness instance from a CuccaroMulLayout and the existing carry-clean Cuccaro step (the REAL cuccaroModMulStep, independently derived; NOT 36a's fresh-ancilla hornerStep); genMulCC cuccaroAdder = cuccaroModMul (definitionally), genMulCC_cuccaroAdder_correct reproduces cuccaroModMul_correct's (X · Y) mod N, and genMulCC_cuccaroAdder_toffoli = 20·n² + 14·n recovers cuccaroModMul_toffoli. The abstraction is non-lossy.

Honest scope

36b validates the keystone generalises across memory models (fresh-ancilla 36a + carry-clean here), and gives the first generic-multiplier instance that moves the cost (20n² + 14n < the fresh-ancilla 30n² for n ≥ 2; equal-order, the genuine prize is the Θ(n)-vs-Θ(n²) qubit collapse below), FULLY Boolean-verified (the whole stack is CCX-circuit denote, no amplitude wall, unlike a measurement adder). This is the MULTIPLY cost; the score-dominant term is the INVERTER (36c, safegcd parametric, the ~67%). No ECDSA score change is claimed yet (still needs 36c + harness #7). The Θ(n)-qubit win is real: the restored-clean invariant (this module's cleanRestored, realised by cuccaroModMul_clean) is exactly what lets the single scratch bank be reused across all n steps. Load-bearing hypothesis: N odd (inherited from the doubler's parity flag-uncompute), which holds for the ECDLP prime field.

The carry-clean variant interface

structure Reversible.VerifiedAdderCarryClean (m n N : ℕ) : Type

A verified carry-clean per-bit modular-multiply step, the substitutable atom of the single-scratch-bank multiplier fold. Bundles exactly the carry-clean fold's consumption surface: a per-step circuit step k over a shared accumulator B and multiplicand Y, the digit digit k s step k folds, a GLOBAL cleanliness predicate clean s (one reused scratch bank, no per-bank index), and the restored-clean facts the fold consumes. Unlike 36a's fresh-ancilla signature, clean is a PRECONDITION of correct / cleanRestored / presY and is RE-ESTABLISHED by cleanRestored; the fold threads "bank clean" as a loop invariant. N is the modulus; hNpos keeps the running residue genuine.

• step : ℕ → Circuit m

  Step k's circuit on the shared bank.

• B : ℕ → Fin m

  The shared accumulator register.

• Y : ℕ → Fin m

  The shared multiplicand register.

• digit : ℕ → State m → ℕ

  The digit (0 / 1) step k folds, read off the state.

• clean : State m → Prop

  The GLOBAL single-bank cleanliness precondition (no per-bank index).

• toffoli : ℕ

  The per-step Toffoli cost.

• hNpos : 0 < N

  The modulus is positive.

• hToffoli (k : ℕ) : (circuitCost (self.step k)).toffoli = self.toffoli

  The step's gate-list Toffoli count is toffoli.

• correct (k : ℕ) (s : State m) (c Yval : ℕ) : k < n → self.clean s → Yval < N → regValRange self.B s n = c → c < N → regValRange self.Y s n = Yval → regValRange self.B (denote (self.step k) s) n = (2 * c + self.digit k s * Yval) % N

  Value correctness (clean PRECONDITION). From a clean bank with B = c < N and Y = Yval < N, step k advances the residue: B ← (2·c + digit·Yval) mod N.

• cleanRestored (k : ℕ) (s : State m) (c Yval : ℕ) : k < n → self.clean s → Yval < N → regValRange self.B s n = c → c < N → regValRange self.Y s n = Yval → self.clean (denote (self.step k) s)

  Cleanliness restoration (the load-bearing POSTCONDITION). From a clean bank with the same value preconditions, step k re-establishes clean on the output state. This is what makes the single-bank reuse sound: each step consumes a clean bank and gives one back.

• presY (k : ℕ) (s : State m) (c Yval : ℕ) : k < n → self.clean s → Yval < N → regValRange self.B s n = c → c < N → regValRange self.Y s n = Yval → regValRange self.Y (denote (self.step k) s) n = Yval

  Multiplicand persistence. Step k leaves Y at its value.

• digitStable (j k : ℕ) (s : State m) : self.digit k (denote (self.step j) s) = self.digit k s

  Digit frame. Step j leaves step k's digit intact (the digit lives on the read-only multiplier register, preserved by every step).

The generic carry-clean multiplier

def Reversible.genMulCC {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) : Circuit m

The adder-parametric carry-clean modular multiplier. Fold the restored-clean step over the n banks on the single shared scratch bank.

Equations

• Reversible.genMulCC A = List.flatMap id (List.map (fun (j : ℕ) => A.step j) (List.range n))

def Reversible.genMulCCUpto {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) (k : ℕ) : Circuit m

The first k steps of the loop (the induction handle).

Equations

• Reversible.genMulCCUpto A k = List.flatMap id (List.map (fun (j : ℕ) => A.step j) (List.range k))

theorem Reversible.genMulCC_eq_upto {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) : genMulCC A = genMulCCUpto A n

theorem Reversible.genMulCCUpto_succ {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) (k : ℕ) : genMulCCUpto A (k + 1) = genMulCCUpto A k ++ A.step k

theorem Reversible.genMulCC_digit_pres {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) (s : State m) (k p : ℕ) : A.digit k (denote (genMulCCUpto A p) s) = A.digit k s

Step k's digit survives the prefix of steps [0, p) (every step preserves all digits, by digitStable).

theorem Reversible.genMulCC_invariant {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) (s : State m) {y : ℕ} (hy : y < N) (hclean : A.clean s) (hB0 : regValRange A.B s n = 0) (hY : regValRange A.Y s n = y) (k : ℕ) : k ≤ n → regValRange A.B (denote (genMulCCUpto A k) s) n = accVal (fun (j : ℕ) => A.digit j s) k * y % N ∧ A.clean (denote (genMulCCUpto A k) s) ∧ regValRange A.Y (denote (genMulCCUpto A k) s) n = y

The generic carry-clean multiply-loop invariant. After the first k steps (k ≤ n) from a clean bank with B = 0, the accumulator holds (accVal digit k · y) mod N, the bank is STILL clean (the restored-clean loop invariant: clean in → correct + cleanRestored → clean out), and Y still holds y. The same induction as cuccaroModMul_invariant, now citing the abstract fields.

theorem Reversible.genMulCC_correct {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) (s : State m) {y : ℕ} (hy : y < N) (hclean : A.clean s) (hB0 : regValRange A.B s n = 0) (hY : regValRange A.Y s n = y) : regValRange A.B (denote (genMulCC A) s) n = accVal (fun (j : ℕ) => A.digit j s) n * y % N

The adder-parametric carry-clean modular multiply (the keystone). For any conforming restored-clean step, with B = 0, Y = y < N, and the bank clean, genMulCC A leaves the accumulator holding (accVal digit n · y) mod N. Proved ONCE, parametric over A.

theorem Reversible.genMulCC_clean {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) (s : State m) {y : ℕ} (hy : y < N) (hclean : A.clean s) (hB0 : regValRange A.B s n = 0) (hY : regValRange A.Y s n = y) : A.clean (denote (genMulCC A) s)

The shared bank is restored clean after the full multiply (so the Θ(n) reuse is real).

theorem Reversible.genMulCC_toffoli {m n N : ℕ} (A : VerifiedAdderCarryClean m n N) : (circuitCost (genMulCC A)).toffoli = n * A.toffoli

Derived cost recurrence: n · A.toffoli. The fold is n copies of the step composed through the concatenation; multiplier_toffoli turns the gate list into the sum of the per-step counts.

The faithfulness instance: the carry-clean Cuccaro multiply (the non-lossy guard)

cuccaroAdder instantiates VerifiedAdderCarryClean with the existing Stage-2b carry-clean Cuccaro step cuccaroModMulStep (= cuccaroModDouble ++ cuccaroCModAdd), reading the proven cuccaroModDouble / cuccaroCModAdd lemmas into the abstract fields via the per-step workhorse cuccaroModMulStep_spec. The generic theorems then recover cuccaroModMul's (X · Y) mod N correctness and 20·n² + 14·n cost exactly.

def Reversible.cuccaroClean {m n : ℕ} (L : CuccaroMulLayout m n) (N : ℕ) (s : State m) : Prop

The GLOBAL single-bank clean precondition for the Cuccaro multiply: every scratch wire of the shared bank mod restored to false, plus the modulus preset Nreg = N. This is the carry-clean "bank ready for a step" predicate; cuccaroModMul_clean is exactly its restoration.

Equations

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

theorem Reversible.cuccaroModMulStep_preserves_X {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) (j i : ℕ) : denote (cuccaroModMulStep L j) s (L.X i) = s (L.X i)

The read-only multiplier register survives one Cuccaro step (both sub-gadgets leave it external).

theorem Reversible.cuccaroModMulStep_spec {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) {N c y : ℕ} (hclean : cuccaroClean L N s) (h2N : 2 * N ≤ 2 ^ n) (hNodd : N % 2 = 1) (hNpos : 0 < N) (hAcc : regValRange L.mod.Acc s n = c) (hcN : c < N) (hY : regValRange L.Y s n = y) (hyN : y < N) (k : ℕ) : regValRange L.mod.Acc (denote (cuccaroModMulStep L k) s) n = (2 * c + (if s (L.X (n - 1 - k)) = true then 1 else 0) * y) % N ∧ cuccaroClean L N (denote (cuccaroModMulStep L k) s) ∧ regValRange L.Y (denote (cuccaroModMulStep L k) s) n = y

The per-step Cuccaro workhorse (clean in → step → clean out). From a clean bank with Acc = c < N and Y = y < N, one Horner step (cuccaroModDouble ++ cuccaroCModAdd) advances the residue to (2·c + [X bit]·y) mod N, restores the whole shared bank clean, and preserves Y. The refactor of the succ case of cuccaroModMul_invariant to consume / produce cuccaroClean.

def Reversible.cuccaroAdder {m n : ℕ} (L : CuccaroMulLayout m n) (N : ℕ) (hNpos : 0 < N) (hNodd : N % 2 = 1) (h2N : 2 * N ≤ 2 ^ n) : VerifiedAdderCarryClean m n N

The faithfulness instance: the carry-clean Cuccaro multiply as a VerifiedAdderCarryClean.

Equations

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

theorem Reversible.genMulCC_cuccaroAdder_eq {m n : ℕ} (L : CuccaroMulLayout m n) (N : ℕ) (hNpos : 0 < N) (hNodd : N % 2 = 1) (h2N : 2 * N ≤ 2 ^ n) : genMulCC (cuccaroAdder L N hNpos hNodd h2N) = cuccaroModMul L

Definitional faithfulness: the generic carry-clean multiplier on the Cuccaro step IS the existing cuccaroModMul.

theorem Reversible.genMulCC_cuccaroAdder_correct {m n : ℕ} (L : CuccaroMulLayout m n) (s : State m) {N Yval : ℕ} (hNpos : 0 < N) (hNodd : N % 2 = 1) (h2N : 2 * N ≤ 2 ^ n) (hyN : Yval < N) (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) (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 (genMulCC (cuccaroAdder L N hNpos hNodd h2N)) s) n = regValRange L.X s n * Yval % N

Correctness faithfulness (the non-lossy guard): genMulCC_correct on the Cuccaro instance recovers cuccaroModMul_correct's (X · Y) mod N statement exactly. The generic accVal digit n lands on regValRange X s n via accVal_eq_hornerVal + regValRange_eq_hornerVal_bits.

theorem Reversible.genMulCC_cuccaroAdder_toffoli {m n : ℕ} (L : CuccaroMulLayout m n) (N : ℕ) (hNpos : 0 < N) (hNodd : N % 2 = 1) (h2N : 2 * N ≤ 2 ^ n) : (circuitCost (genMulCC (cuccaroAdder L N hNpos hNodd h2N))).toffoli = 20 * n ^ 2 + 14 * n

Cost faithfulness (the non-lossy guard): the cost recurrence on the Cuccaro instance recovers cuccaroModMul_toffoli's figure 20·n² + 14·n exactly — the first generic-multiplier instance below the fresh-ancilla 30·n² baseline, fully Boolean-verified.