An adder-parametric modular multiplier — the substitution keystone (ECDLP Phase 2, Stage S6.3-36a)

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

This module turns re-costing the modular multiplier with a different (cheaper) per-bit step from a per-circuit re-proof into an instantiation. It bundles the multiplier fold's consumption surface into a structure VerifiedAdder, proves the multiply correct + cost it once, parametric over any conforming step, and exhibits the existing corpus multiplier (mulLoop, S6.3d-2b) as the faithfulness instance — recovering its proven (X · Y) mod N correctness and 30 · n² Toffoli figure exactly.

Interface level (the scout-chosen granularity)

The Horner loop body is hornerStep = modDouble ++ cModAdd (S6.3d-2a). The multiplier fold (mulLoop_invariant) consumes each bank as a black box through exactly four facts:

• value correctness acc ← (2·acc + [bit]·Y) mod N (hornerStep_correct),
• multiplicand persistence Y ← Y (hornerStep_preserves_Y),
• an inter-bank frame: bank j leaves bank k's clean / preset wires untouched (k ≠ j) (notTouches_preserved + hInter),
• a derived per-step Toffoli cost (hornerStep_toffoli).

So the interface is placed at the per-bit Horner-step level (the substitutable atom whose cost is adder-dominated), NOT one level finer at the bare controlled adder. Placing it at the step level is the least-refactor non-lossy choice: the existing modular stack (modReduce / modDouble / cModAdd) is reused wholesale inside the faithfulness instance, with zero re-derivation. The doubling is absorbed into the step's cost, so the cost recurrence is n · step.toffoli with no separate overhead term.

What is proved

• VerifiedAdder — the structure with exactly the four consumed fields (+ digit, clean, hNpos).
• genMul / genMul_correct — the multiplier fold + its correctness acc = (accVal digit · Y) mod N, the SAME induction as mulLoop_invariant, now citing the abstract fields (genuine, parametric).
• genMul_toffoli — the cost recurrence n · step.toffoli (derived from the gate-list sum).
• corpusAdder — the faithfulness instance built from a MulLoopLayout and the existing hornerStep lemmas; genMul corpusAdder = mulLoop (definitionally), genMul_corpusAdder_correct reproduces mulLoop_correct's (X · Y) mod N statement, and genMul_corpusAdder_toffoli = 30 · n² recovers mulLoop_toffoli. The abstraction is non-lossy.

Carve line (what this is, and is NOT)

This is the keystone abstraction: interface + parametric multiplier + faithfulness. It is reusable; every future fresh-ancilla step is one VerifiedAdder instance. No ECDSA score change is claimed.

Deferred and the precise propagation cost:

1. 36b (carry-clean Cuccaro multiply). A cheaper BASE (ripple) adder does NOT propagate to the score by instantiation alone. The modular wrappers modAdd / cModAdd / modDouble sit between the ripple adder and the step; a new base adder forces re-deriving them to build a new step. 36b inherits the arithmetic core (accVal / accVal_mod_step) and the cost-recurrence shape, but must build the new step (the modular wrappers on the Cuccaro base) before instantiating. Moreover the Cuccaro multiply reuses a SINGLE scratch bank (carry-clean, Θ(n) qubits), so its frame discipline is a global restored-clean invariant carried per step, NOT this module's per-bank disjoint clean. Serving it therefore needs a carry-clean variant of VerifiedAdder (a clean restored by every step, consuming the value precondition), not this fresh-ancilla signature. That variant is 36b's to build; what it reuses unchanged is accVal / accVal_mod_step and the genMul_toffoli shape.
2. 36c (generic inverter / safegcd). Same pattern one layer up.
3. 36d (Gidney measurement adder). Amplitude-gated per #21 / #31.

Honest cost

genMul_toffoli A derives n · A.toffoli; the corpus instance has A.toffoli = 30 · n (hornerStep_toffoli), so genMul_corpusAdder_toffoli = 30 · n² — equal to mulLoop_toffoli. This is the Θ(n²)-qubit fresh-ancilla figure inherited from the corpus step.

The abstract accumulator value and its modular step

def Reversible.accVal (d : ℕ → ℕ) : ℕ → ℕ

Process-step accumulator: accVal d 0 = 0, accVal d (k+1) = 2 · accVal d k + d k. The MSB-first Horner reconstruction folded by a multiplier whose bank k contributes digit d k.

Equations

• Reversible.accVal d 0 = 0
• Reversible.accVal d k.succ = 2 * Reversible.accVal d k + d k

@[simp]

theorem Reversible.accVal_zero (d : ℕ → ℕ) : accVal d 0 = 0

theorem Reversible.accVal_succ (d : ℕ → ℕ) (k : ℕ) : accVal d (k + 1) = 2 * accVal d k + d k

theorem Reversible.accVal_mod_step (H y N b : ℕ) : (2 * (H * y % N) + b * y) % N = (2 * H + b) * y % N

The Horner arithmetic step (general digit). (2·((H·y) mod N) + b·y) mod N = ((2·H + b)·y) mod N, absorbing the inner reduction via Nat.mul_mod. The per-step residue advance the fold needs.

theorem Reversible.accVal_eq_hornerVal (bits : ℕ → ℕ) (n k : ℕ) : accVal (fun (j : ℕ) => bits (n - 1 - j)) k = hornerVal bits n k

Bridge to the Horner reconstruction. accVal (fun j => bits (n-1-j)) k = hornerVal bits n k: both satisfy 0 / 2·prev + bits (n-1-k). Lets the faithfulness instance land accVal digit n on regValRange X s n via regValRange_eq_hornerVal_bits.

The interface

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

A verified per-bit modular-multiply step, the substitutable atom of the multiplier fold. Bundles exactly the fold's consumption surface for the fresh-ancilla discipline: a per-bank circuit step k over a shared accumulator B and multiplicand Y, the digit digit k s bank k folds, the per-bank cleanliness predicate clean k s, and the four facts the fold induction consumes (correct, presY, the inter-bank frame cleanStable / digitStable, the cost hToffoli). N is the modulus; hNpos keeps the running residue genuine.

• step : ℕ → Circuit m

  Bank k's step circuit.

• B : ℕ → Fin m

  The shared accumulator register.

• Y : ℕ → Fin m

  The shared multiplicand register.

• digit : ℕ → State m → ℕ

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

• clean : ℕ → State m → Prop

  Bank k's private clean / preset precondition.

• 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 k 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. From a clean bank with B = c < N and Y = Yval < N, bank k advances the residue: B ← (2·c + digit·Yval) mod N.

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

  Multiplicand persistence. Bank k leaves Y at its value.

• cleanStable (j k : ℕ) (s : State m) : j < n → k < n → j ≠ k → self.clean k s → self.clean k (denote (self.step j) s)

  Inter-bank clean frame. Bank j leaves bank k's clean precondition intact (j ≠ k).

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

  Inter-bank digit frame. Bank j leaves bank k's digit intact (j ≠ k).

The generic multiplier

def Reversible.genMul {m n N : ℕ} (A : VerifiedAdder m n N) : Circuit m

The adder-parametric modular multiplier. Fold the verified step over the n banks.

Equations

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

def Reversible.genMulUpto {m n N : ℕ} (A : VerifiedAdder m n N) (k : ℕ) : Circuit m

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

Equations

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

theorem Reversible.genMul_eq_upto {m n N : ℕ} (A : VerifiedAdder m n N) : genMul A = genMulUpto A n

theorem Reversible.genMulUpto_succ {m n N : ℕ} (A : VerifiedAdder m n N) (k : ℕ) : genMulUpto A (k + 1) = genMulUpto A k ++ A.step k

theorem Reversible.genMul_clean_pres {m n N : ℕ} (A : VerifiedAdder m n N) (s : State m) {k : ℕ} (hk : k < n) (hck : A.clean k s) (p : ℕ) : p ≤ k → A.clean k (denote (genMulUpto A p) s)

Bank k's clean precondition survives the prefix of banks [0, p) (p ≤ k): each earlier bank j < p ≤ k has j ≠ k, so cleanStable applies.

theorem Reversible.genMul_digit_pres {m n N : ℕ} (A : VerifiedAdder m n N) (s : State m) {k : ℕ} (hk : k < n) (p : ℕ) : p ≤ k → A.digit k (denote (genMulUpto A p) s) = A.digit k s

Bank k's digit survives the prefix of banks [0, p) (p ≤ k), by digitStable.

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

The generic multiply-loop invariant. After the first k banks (k ≤ n) from B = 0, the accumulator holds (accVal digit k · y) mod N and Y still holds y. The SAME induction as mulLoop_invariant, now citing the abstract VerifiedAdder fields: the prefix preserves bank k's clean precondition (genMul_clean_pres) and its digit (genMul_digit_pres); correct advances the residue (accVal_mod_step); presY keeps y.

theorem Reversible.genMul_correct {m n N : ℕ} (A : VerifiedAdder m n N) (s : State m) {y : ℕ} (hy : y < N) (hclean : ∀ k < n, A.clean k s) (hB0 : regValRange A.B s n = 0) (hY : regValRange A.Y s n = y) : regValRange A.B (denote (genMul A) s) n = accVal (fun (j : ℕ) => A.digit j s) n * y % N

The adder-parametric modular multiply (the keystone). For any conforming step, with B = 0, Y = y < N, and every bank clean, genMul A leaves the accumulator holding (accVal digit n · y) mod N. Specialised from genMul_invariant at k = n. Proved ONCE, parametric over A.

theorem Reversible.genMul_toffoli {m n N : ℕ} (A : VerifiedAdder m n N) : (circuitCost (genMul 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 corpus mulLoop (the non-lossy guard)

corpusAdder instantiates VerifiedAdder with the existing S6.3d-2b multiplier's per-bit Horner step, reading the proven hornerStep_* lemmas into the abstract fields. The generic theorems then recover the corpus's (X · Y) mod N correctness and 30 · n² cost exactly.

def Reversible.corpusClean {m n : ℕ} (L : MulLoopLayout m n) (N k : ℕ) (s : State m) : Prop

Bank k's clean / preset precondition for the corpus Horner step (the 14 facts hornerStep_correct consumes about bank k's private wires: 10 clean carries / ancilla false, 4 reduce presets).

Equations

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

theorem Reversible.corpus_step_pres {m n : ℕ} (L : MulLoopLayout m n) {j k : ℕ} (hj : j < n) (hk : k < n) (hjk : j ≠ k) (s : State m) (w : Fin m) (hw : Clean L.bank k w) : denote (hornerStep (L.bank j)) s w = s w

A wire of bank k's clean set survives bank j's Horner step (j ≠ k): hInter + frame.

theorem Reversible.corpus_step_pres_reg {m n : ℕ} (L : MulLoopLayout m n) {j k : ℕ} (hj : j < n) (hk : k < n) (hjk : j ≠ k) (s : State m) (f : ℕ → Fin m) (hf : ∀ (i : ℕ), Clean L.bank k (f i)) (q : ℕ) : regValRange f (denote (hornerStep (L.bank j)) s) q = regValRange f s q

A register over bank k's clean wires survives bank j's Horner step (j ≠ k).

theorem Reversible.corpusAdder_correct {m n : ℕ} (L : MulLoopLayout m n) (N : ℕ) (h2N : 2 * N ≤ 2 ^ n) (k : ℕ) (s : State m) (c Yval : ℕ) : k < n → corpusClean L N k s → Yval < N → regValRange L.B s n = c → c < N → regValRange L.Y s n = Yval → regValRange L.B (denote (hornerStep (L.bank k)) s) n = (2 * c + (if s (L.X (n - 1 - k)) = true then 1 else 0) * Yval) % N

Corpus correct field: hornerStep_correct with the digit read as [X_{n-1-k}]·Y.

theorem Reversible.corpusAdder_presY {m n : ℕ} (L : MulLoopLayout m n) (N k : ℕ) (s : State m) (Yval : ℕ) : k < n → corpusClean L N k s → regValRange L.Y s n = Yval → regValRange L.Y (denote (hornerStep (L.bank k)) s) n = Yval

Corpus presY field: hornerStep_preserves_Y.

theorem Reversible.corpusAdder_cleanStable {m n : ℕ} (L : MulLoopLayout m n) (N j k : ℕ) (s : State m) : j < n → k < n → j ≠ k → corpusClean L N k s → corpusClean L N k (denote (hornerStep (L.bank j)) s)

Corpus cleanStable field: each clean wire / preset survives bank j via corpus_step_pres.

theorem Reversible.corpusAdder_digitStable {m n : ℕ} (L : MulLoopLayout m n) (j k : ℕ) (s : State m) : j < n → k < n → j ≠ k → (if denote (hornerStep (L.bank j)) s (L.X (n - 1 - k)) = true then 1 else 0) = if s (L.X (n - 1 - k)) = true then 1 else 0

Corpus digitStable field: the control bit X (n-1-k) survives bank j (hCtrlTouch).

def Reversible.corpusAdder {m n : ℕ} (L : MulLoopLayout m n) (N : ℕ) (hNpos : 0 < N) (h2N : 2 * N ≤ 2 ^ n) : VerifiedAdder m n N

The faithfulness instance: the corpus S6.3d-2b multiplier as a VerifiedAdder.

Equations

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

theorem Reversible.genMul_corpusAdder_eq {m n : ℕ} (L : MulLoopLayout m n) (N : ℕ) (hNpos : 0 < N) (h2N : 2 * N ≤ 2 ^ n) : genMul (corpusAdder L N hNpos h2N) = mulLoop L

Definitional faithfulness: the generic multiplier on the corpus step IS the corpus mulLoop.

theorem Reversible.genMul_corpusAdder_correct {m n : ℕ} (L : MulLoopLayout m n) (s : State m) {N Yval : ℕ} (hNpos : 0 < N) (h2N : 2 * N ≤ 2 ^ n) (hYN : Yval < N) (hB0 : regValRange L.B s n = 0) (hYv : regValRange L.Y s n = Yval) (hcleanAop : ∀ (j i : ℕ), j < n → i < n → s ((L.bank j).dbl.Aop i) = false) (hcleanCadd : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.Cadd i) = false) (hcleandC1 : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.C1 i) = false) (hcleandC2 : ∀ (j i : ℕ), j < n → s ((L.bank j).dbl.addLayout.C2 i) = false) (hcleandanc : ∀ j < n, s (L.bank j).dbl.addLayout.anc = false) (hcleanCcadd : ∀ (j i : ℕ), j < n → s ((L.bank j).add.Ccadd i) = false) (hcleanancC : ∀ j < n, s (L.bank j).add.ancC = false) (hcleanC1 : ∀ (j i : ℕ), j < n → s ((L.bank j).add.C1 i) = false) (hcleanC2 : ∀ (j i : ℕ), j < n → s ((L.bank j).add.C2 i) = false) (hcleananc : ∀ j < n, s (L.bank j).add.anc = false) (hA1dbl : ∀ j < n, regValRange (L.bank j).dbl.addLayout.A1 s n = 2 ^ n - N) (hA2dbl : ∀ j < n, regValRange (L.bank j).dbl.addLayout.A2 s n = N) (hA1add : ∀ j < n, regValRange (L.bank j).add.A1 s n = 2 ^ n - N) (hA2add : ∀ j < n, regValRange (L.bank j).add.A2 s n = N) : regValRange L.B (denote (genMul (corpusAdder L N hNpos h2N)) s) n = regValRange L.X s n * Yval % N

Correctness faithfulness (the non-lossy guard): genMul_correct on the corpus instance recovers mulLoop_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.genMul_corpusAdder_toffoli {m n : ℕ} (L : MulLoopLayout m n) (N : ℕ) (hNpos : 0 < N) (h2N : 2 * N ≤ 2 ^ n) : (circuitCost (genMul (corpusAdder L N hNpos h2N))).toffoli = 30 * n ^ 2

Cost faithfulness (the non-lossy guard): the cost recurrence on the corpus instance recovers mulLoop_toffoli's figure 30 · n².