Reversible controlled modular addition — (ctrl, a, b) ↦ if ctrl then (a+b) mod N else b (ECDLP Phase 2, Stage S6.3c)

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

This module verifies the controlled modular-addition VALUE primitive — the controlled analogue of S6.3b's modAdd — by chaining two already-verified blocks:

cModAdd L = cRippleCirc L.cAddStep ++ modReduce L.reduceStep

• Controlled add step cRippleCirc L.cAddStep (S2): addend Aop (= a, read-only), accumulator B (= b), control wire ctrl, the cRipple carry chain Ccadd, shared ancilla ancC (restored by cRippleCirc_anc_restored). With a + b < 2N ≤ 2ⁿ, cRippleCirc_correct gives B ← if ctrl then (a + b) mod 2ⁿ else b = if ctrl then a + b else b (no wrap). In both branches B < 2N (ctrl: a + b < 2N; ¬ctrl: b < N < 2N).
• Reduce step modReduce L.reduceStep (S6.3a) — UNCONDITIONAL, it always runs: since B < 2N in both branches, modReduce_correct maps B ← B mod N. In the ctrl branch that is (a + b) mod N; in the ¬ctrl branch it is b mod N = b (since b < N). The reduce being unconditional is the whole trick: b is already a valid reduced residue, so reducing it again is the identity.

So the headline value is B ← if ctrl then (a + b) mod N else b.

Carve line (what this is, and is NOT)

This VERIFIES the controlled modular-addition value primitive B ← if ctrl then (a+b) mod N else b by chaining the verified cRippleCirc (S2) with S6.3a's modReduce; the unconditional reduce is correct in both branches because b < N is already a valid residue. This is ℕ / mod N bit arithmetic — NO field / group semantics are in play.

This is the inner-loop primitive of the interleaved MSB-first modular MULTIPLY over 𝔽_p (the next stage, S6.3d), which also needs a modular DOUBLING gadget (2·acc mod N, the register-to-itself add) and the Horner loop invariant. This module is NOT the multiply.

Named residue (same as S6.3b; name it): the carry chains Ccadd, C1, C2 and the comparison flag C1 n are left DIRTY after cModAdd. Correctness holds because the layout supplies fresh wires per use (cModAdd_correct requires C* / anc initialised false). In-place reuse across the many additions of a modular multiply needs carry-clean / ancilla-restoring adders (Cuccaro-style inline carry-uncompute, or reversing carry generation) which the corpus's rippleCirc / cRippleCirc do NOT provide. That carry-clean adder is the genuine orthogonal residue, NOT built here.

Honest cost

cModularAdd_toffoli derives 18n Toffolis from the exhibited gate list: controlled add step 8n (cRippleCirc_toffoli, the quantum×quantum overhead) + reduce step 10n (modReduceCtrl_toffoli), composed through cost_comp_toffoli_count. (Heavier than S6.3b's uncontrolled 12n precisely by the 4× quantum×quantum cost of the controlled add, 8n vs 2n.)

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

A controlled-modular-addition layout on Fin m for n-bit registers. Like ModAddLayout but the add step is a CRippleLayout: it bundles the operand register Aop (read-only addend a), the accumulator B (holds b, overwritten with if ctrl then (a+b) mod N else b), the controlled-add step's own carry chain Ccadd, the control wire ctrl, the cRipple shared ancilla ancC, and the reduce sub-data (A1, A2, C1, C2, anc).

The geometry fields give: (i) cAddStep : CRippleLayout well-formed (Aop, B, Ccadd, ctrl, ancC pairwise disjoint + bounded-injective), (ii) reduceStep : ModReduceLayout well-formed, and (iii) Ccadd, Aop, ctrl, ancC all disjoint from every reduce-step wire so the controlled-add step's carries / ancilla are fresh and the operand + control bit survive the whole circuit.

Injectivity fields are bounded (< n for registers, < n + 1 for carry chains), exactly as ModAddLayout / ModReduceLayout / MulLayout: an unbounded ℕ → Fin m injectivity field is uninhabitable and would make the theorems vacuous.

• Aop : ℕ → Fin m

  Operand register: holds a, read-only addend (preserved by cModAdd).

• B : ℕ → Fin m

  Accumulator: holds b, overwritten with if ctrl then (a + b) mod N else b.

• Ccadd : ℕ → Fin m

  Controlled-add-step carry chain (disjoint from the reduce step).

• ctrl : Fin m

  The control wire (set ⇒ add a; clear ⇒ leave b). Read, never written.

• ancC : Fin m

  The controlled-add-step shared clean ancilla (CCCX decomposition; restored false).

• A1 : ℕ → Fin m

  Reduce step-1 constant register (preset to 2ⁿ − N).

• C1 : ℕ → Fin m

  Reduce step-1 carry chain; C1 n is the comparison flag.

• A2 : ℕ → Fin m

  Reduce step-3 constant register (preset to N).

• C2 : ℕ → Fin m

  Reduce step-3 carry chain.

• anc : Fin m

  Reduce shared clean ancilla.

• hAopB (i j : ℕ) : self.Aop i ≠ self.B j
• hAopCcadd (i j : ℕ) : self.Aop i ≠ self.Ccadd j
• hBCcadd (i j : ℕ) : self.B i ≠ self.Ccadd j
• hAopinj (i j : ℕ) : i < n → j < n → self.Aop i = self.Aop j → i = j
• hBinj (i j : ℕ) : i < n → j < n → self.B i = self.B j → i = j
• hCcaddinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Ccadd i = self.Ccadd j → i = j
• hctrlAop (i : ℕ) : self.ctrl ≠ self.Aop i
• hctrlB (i : ℕ) : self.ctrl ≠ self.B i
• hctrlCcadd (i : ℕ) : self.ctrl ≠ self.Ccadd i
• hctrlancC : self.ctrl ≠ self.ancC
• hancCAop (i : ℕ) : self.ancC ≠ self.Aop i
• hancCB (i : ℕ) : self.ancC ≠ self.B i
• hancCCcadd (i : ℕ) : self.ancC ≠ self.Ccadd i
• hBA1 (i j : ℕ) : self.B i ≠ self.A1 j
• hBC1 (i j : ℕ) : self.B i ≠ self.C1 j
• hA1C1 (i j : ℕ) : self.A1 i ≠ self.C1 j
• hA1inj (i j : ℕ) : i < n → j < n → self.A1 i = self.A1 j → i = j
• hC1inj (i j : ℕ) : i < n + 1 → j < n + 1 → self.C1 i = self.C1 j → i = j
• hBA2 (i j : ℕ) : self.B i ≠ self.A2 j
• hBC2 (i j : ℕ) : self.B i ≠ self.C2 j
• hA2C2 (i j : ℕ) : self.A2 i ≠ self.C2 j
• hA2inj (i j : ℕ) : i < n → j < n → self.A2 i = self.A2 j → i = j
• hC2inj (i j : ℕ) : i < n + 1 → j < n + 1 → self.C2 i = self.C2 j → i = j
• hflagA2 (j : ℕ) : self.C1 n ≠ self.A2 j
• hflagB (j : ℕ) : self.C1 n ≠ self.B j
• hflagC2 (j : ℕ) : self.C1 n ≠ self.C2 j
• hflaganc : self.C1 n ≠ self.anc
• hancA2 (j : ℕ) : self.anc ≠ self.A2 j
• hancB (j : ℕ) : self.anc ≠ self.B j
• hancC2 (j : ℕ) : self.anc ≠ self.C2 j
• hA2A1 (i j : ℕ) : self.A2 i ≠ self.A1 j
• hA2C1 (i j : ℕ) : self.A2 i ≠ self.C1 j
• hC2A1 (i j : ℕ) : self.C2 i ≠ self.A1 j
• hC2C1 (i j : ℕ) : self.C2 i ≠ self.C1 j
• hancA1 (j : ℕ) : self.anc ≠ self.A1 j
• hancC1 (j : ℕ) : self.anc ≠ self.C1 j
• hCcaddA1 (i j : ℕ) : self.Ccadd i ≠ self.A1 j
• hCcaddC1 (i j : ℕ) : self.Ccadd i ≠ self.C1 j
• hCcaddA2 (i j : ℕ) : self.Ccadd i ≠ self.A2 j
• hCcaddC2 (i j : ℕ) : self.Ccadd i ≠ self.C2 j
• hCcaddanc (i : ℕ) : self.Ccadd i ≠ self.anc
• hAopA1 (i j : ℕ) : self.Aop i ≠ self.A1 j
• hAopC1 (i j : ℕ) : self.Aop i ≠ self.C1 j
• hAopA2 (i j : ℕ) : self.Aop i ≠ self.A2 j
• hAopC2 (i j : ℕ) : self.Aop i ≠ self.C2 j
• hAopanc (i : ℕ) : self.Aop i ≠ self.anc
• hctrlA1 (j : ℕ) : self.ctrl ≠ self.A1 j
• hctrlC1 (j : ℕ) : self.ctrl ≠ self.C1 j
• hctrlA2 (j : ℕ) : self.ctrl ≠ self.A2 j
• hctrlC2 (j : ℕ) : self.ctrl ≠ self.C2 j
• hctrlanc : self.ctrl ≠ self.anc
• hancCA1 (j : ℕ) : self.ancC ≠ self.A1 j
• hancCC1 (j : ℕ) : self.ancC ≠ self.C1 j
• hancCA2 (j : ℕ) : self.ancC ≠ self.A2 j
• hancCC2 (j : ℕ) : self.ancC ≠ self.C2 j
• hancCanc : self.ancC ≠ self.anc

def Reversible.CModAddLayout.cAddStep {m n : ℕ} (L : CModAddLayout m n) : CRippleLayout m n

The controlled add step as a CRippleLayout: operand Aop + accumulator B + add-carry chain Ccadd, controlled on ctrl, with shared ancilla ancC.

Equations

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

def Reversible.CModAddLayout.reduceStep {m n : ℕ} (L : CModAddLayout m n) : ModReduceLayout m n

The reduce step as a ModReduceLayout (S6.3a).

Equations

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

def Reversible.cModAdd {m n : ℕ} (L : CModAddLayout m n) : Circuit m

The controlled modular-addition circuit. Controlled register add (cRippleCirc) followed by the S6.3a single-step modular reduction (modReduce), the latter run unconditionally.

Equations

• Reversible.cModAdd L = Reversible.cRippleCirc L.cAddStep ++ Reversible.modReduce L.reduceStep

Frame: a wire disjoint from cAddStep's wires survives the controlled add step

cRippleCirc L.cAddStep touches only {ctrl, ancC} ∪ {Aop k, B k, Ccadd k}. Any wire distinct from all of those passes through unchanged (cRippleCirc_preserves_external). The four corollaries below specialise it to the reduce step's A1 / A2 / C1 / C2 / anc wires.

theorem Reversible.cModAdd_cAddStep_preserves_A1 {m n : ℕ} {L : CModAddLayout m n} (s : State m) (j : ℕ) : denote (cRippleCirc L.cAddStep) s (L.A1 j) = s (L.A1 j)

After the controlled add step, A1 is unchanged on every wire (disjoint from the add step).

theorem Reversible.cModAdd_cAddStep_preserves_A2 {m n : ℕ} {L : CModAddLayout m n} (s : State m) (j : ℕ) : denote (cRippleCirc L.cAddStep) s (L.A2 j) = s (L.A2 j)

After the controlled add step, A2 is unchanged on every wire.

theorem Reversible.cModAdd_cAddStep_preserves_C1 {m n : ℕ} {L : CModAddLayout m n} (s : State m) (j : ℕ) : denote (cRippleCirc L.cAddStep) s (L.C1 j) = s (L.C1 j)

After the controlled add step, C1 is unchanged on every wire.

theorem Reversible.cModAdd_cAddStep_preserves_C2 {m n : ℕ} {L : CModAddLayout m n} (s : State m) (j : ℕ) : denote (cRippleCirc L.cAddStep) s (L.C2 j) = s (L.C2 j)

After the controlled add step, C2 is unchanged on every wire.

theorem Reversible.cModAdd_cAddStep_preserves_anc {m n : ℕ} {L : CModAddLayout m n} (s : State m) : denote (cRippleCirc L.cAddStep) s L.anc = s L.anc

After the controlled add step, anc is unchanged.

Frame: the operand Aop and the control bit ctrl survive the reduce step

modReduce L.reduceStep touches only {A1, A2, C1, C2, anc, B} (and the flag C1 n). Since Aop and ctrl are disjoint from all of these, they pass through the reduce step unchanged.

theorem Reversible.cModAdd_reduceStep_preserves_Aop {m n : ℕ} {L : CModAddLayout m n} (s : State m) (j : ℕ) : denote (modReduce L.reduceStep) s (L.Aop j) = s (L.Aop j)

Operand frame through the reduce step. Aop j is untouched by modReduce L.reduceStep.

theorem Reversible.cModAdd_reduceStep_preserves_ctrl {m n : ℕ} {L : CModAddLayout m n} (s : State m) : denote (modReduce L.reduceStep) s L.ctrl = s L.ctrl

Control frame through the reduce step. ctrl is untouched by modReduce L.reduceStep.

Value correctness

theorem Reversible.cModAdd_correct {m n : ℕ} (L : CModAddLayout m n) (s : State m) (hCcadd : ∀ (j : ℕ), s (L.Ccadd j) = false) (hancC : s L.ancC = false) (hC1 : ∀ (j : ℕ), s (L.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.C2 j) = false) (hanc : s L.anc = false) {N a b : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hA1 : regValRange L.A1 s n = 2 ^ n - N) (hA2 : regValRange L.A2 s n = N) (hAop : regValRange L.Aop s n = a) (hB : regValRange L.B s n = b) (haN : a < N) (hbN : b < N) : regValRange L.B (denote (cModAdd L) s) n = if s L.ctrl = true then (a + b) % N else b

The verified controlled modular-addition value primitive. For a disjoint-wire CModAddLayout with all carry chains (Ccadd, C1, C2) and both ancillas (ancC, anc) initialised false, register A1 preset to 2ⁿ − N, register A2 preset to N, operand register Aop holding a, accumulator B holding b, with a < N, b < N, 2N ≤ 2ⁿ: cModAdd L leaves register B holding if ctrl then (a + b) mod N else b.

Proof. The controlled add step (cRippleCirc_correct) writes if ctrl then (a + b) mod 2ⁿ else b = if ctrl then a + b else b to B (no wrap, since a + b < 2N ≤ 2ⁿ), preserving Aop = a and — via the frame lemmas — the reduce step's presets A1 = 2ⁿ − N, A2 = N and clean carries C1 = C2 = false, anc = false. In both control branches B < 2N (ctrl: a + b < 2N; ¬ctrl: b < N < 2N), so the unconditional reduce step (modReduce_correct, S6.3a) maps B to B mod N: (a + b) mod N in the ctrl branch, and b mod N = b in the ¬ctrl branch (b < N, Nat.mod_eq_of_lt). The reduce being unconditional is the whole trick: b is already a valid residue.

theorem Reversible.cModAdd_preserves_operand {m n : ℕ} (L : CModAddLayout m n) (s : State m) (hCcadd : ∀ (j : ℕ), s (L.Ccadd j) = false) (hancC : s L.ancC = false) {a : ℕ} (hAop : regValRange L.Aop s n = a) : regValRange L.Aop (denote (cModAdd L) s) n = a

The operand register is intact. cModAdd L leaves Aop holding a (read-only addend). The controlled add step preserves Aop (P2 of the controlled-ripple invariant) and the reduce step is disjoint from Aop.

theorem Reversible.cModAdd_preserves_ctrl {m n : ℕ} (L : CModAddLayout m n) (s : State m) (hCcadd : ∀ (j : ℕ), s (L.Ccadd j) = false) (hancC : s L.ancC = false) : denote (cModAdd L) s L.ctrl = s L.ctrl

The control bit is preserved. cModAdd L leaves ctrl at its initial value (it is read by the controlled add step, never written, and the reduce step is disjoint from it). The interleaved modular multiply needs this to keep each partial-product's control bit equal to the original register bit across the accumulation loop.

theorem Reversible.cModAdd_in_range {m n : ℕ} (L : CModAddLayout m n) (s : State m) (hCcadd : ∀ (j : ℕ), s (L.Ccadd j) = false) (hancC : s L.ancC = false) (hC1 : ∀ (j : ℕ), s (L.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.C2 j) = false) (hanc : s L.anc = false) {N a b : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hA1 : regValRange L.A1 s n = 2 ^ n - N) (hA2 : regValRange L.A2 s n = N) (hAop : regValRange L.Aop s n = a) (hB : regValRange L.B s n = b) (haN : a < N) (hbN : b < N) : regValRange L.B (denote (cModAdd L) s) n < N

The controlled modular-addition output is a genuine residue in [0, N). In both branches: (a + b) % N < N (ctrl set) and b < N (ctrl clear). Corollary of cModAdd_correct.

Derived cost

theorem Reversible.cModularAdd_toffoli {m n : ℕ} (L : CModAddLayout m n) : (circuitCost (cModAdd L)).toffoli = 18 * n

Derived Toffoli cost of the controlled modular adder: 18n Toffolis, from the exhibited gate list. Controlled add step 8n (cRippleCirc_toffoli, the quantum×quantum overhead) + reduce step 10n (modReduceCtrl_toffoli), composed through cost_comp_toffoli_count. Heavier than S6.3b's uncontrolled 12n precisely by the 4× cost of the controlled add (8n vs 2n).

Non-vacuity witness

A concrete 3-bit controlled-modular-addition layout on Fin 27:

• operand Aop → {0,1,2}, accumulator B → {3,4,5}, controlled-add carry Ccadd → {6,7,8,9}, control 25, cRipple ancilla 26,
• reduce step-1 constant A1 → {10,11,12}, step-1 carry C1 → {13,14,15,16},
• reduce step-3 constant A2 → {17,18,19}, step-3 carry C2 → {20,21,22,23}, reduce ancilla 24.

(n = 3 is needed, as in S6.3b: the modular adder requires 2N ≤ 2ⁿ so the controlled add does not wrap; for N = 3 that forces 2ⁿ ≥ 6, i.e. n ≥ 3.) This exhibits that CModAddLayout is inhabited, so the headlines are not vacuously quantified. The concrete runs below exercise both control branches at fully-specified input states: a = 2, b = 2, N = 3, ctrl = true ↦ (2+2) mod 3 = 1, and the same a, b with ctrl = false ↦ B stays b = 2.

def Reversible.cModAddLayout2 : CModAddLayout 27 3

A concrete 3-bit controlled-modular-addition layout on Fin 27.

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.cModAddLayout2_Aop (i : ℕ) : cModAddLayout2.Aop i = if i = 0 then 0 else if i = 1 then 1 else 2

cModAddLayout2's operand register wires.

theorem Reversible.cModAddLayout2_B (i : ℕ) : cModAddLayout2.B i = if i = 0 then 3 else if i = 1 then 4 else 5

cModAddLayout2's accumulator wires.

theorem Reversible.cModAddLayout2_Ccadd (i : ℕ) : cModAddLayout2.Ccadd i = if i = 0 then 6 else if i = 1 then 7 else if i = 2 then 8 else 9

cModAddLayout2's controlled-add carry-chain wires.

theorem Reversible.cModAddLayout2_ctrl : cModAddLayout2.ctrl = 25

cModAddLayout2's control wire.

theorem Reversible.cModAddLayout2_ancC : cModAddLayout2.ancC = 26

cModAddLayout2's controlled-add clean-ancilla wire.

theorem Reversible.cModAddLayout2_A1 (i : ℕ) : cModAddLayout2.A1 i = if i = 0 then 10 else if i = 1 then 11 else 12

cModAddLayout2's step-1 constant-register wires.

theorem Reversible.cModAddLayout2_C1 (i : ℕ) : cModAddLayout2.C1 i = if i = 0 then 13 else if i = 1 then 14 else if i = 2 then 15 else 16

cModAddLayout2's step-1 carry-chain wires.

theorem Reversible.cModAddLayout2_A2 (i : ℕ) : cModAddLayout2.A2 i = if i = 0 then 17 else if i = 1 then 18 else 19

cModAddLayout2's step-3 constant-register wires.

theorem Reversible.cModAddLayout2_C2 (i : ℕ) : cModAddLayout2.C2 i = if i = 0 then 20 else if i = 1 then 21 else if i = 2 then 22 else 23

cModAddLayout2's step-3 carry-chain wires.

theorem Reversible.cModAddLayout2_anc : cModAddLayout2.anc = 24

cModAddLayout2's reduce-step ancilla wire.

def Reversible.cModAddState2 (a0 a1 a2 b0 b1 b2 c : Bool) : State 27

Concrete input state for n = 3, N = 3: operand Aop = a (wires 0,1,2), accumulator B = b (wires 3,4,5), control wire 25 = ctrl, A1 = 5 = 2³ − 3 (wires 10,12), A2 = 3 (wires 17,18), all carries / ancillas false. Parameterised by the data bits of a, b, and the control bit.

Equations

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

theorem Reversible.cModAddState2_apply (a0 a1 a2 b0 b1 b2 c : Bool) (w : Fin 27) : cModAddState2 a0 a1 a2 b0 b1 b2 c w = if w = 0 then a0 else if w = 1 then a1 else if w = 2 then a2 else if w = 3 then b0 else if w = 4 then b1 else if w = 5 then b2 else if w = 10 then true else if w = 12 then true else if w = 17 then true else if w = 18 then true else if w = 25 then c else false

The concrete input state at a wire, as its defining case chain (interface lemma, §9.1).

theorem Reversible.cModAddState2_pre (a0 a1 a2 b0 b1 b2 c : Bool) : (∀ (j : ℕ), cModAddState2 a0 a1 a2 b0 b1 b2 c (cModAddLayout2.Ccadd j) = false) ∧ cModAddState2 a0 a1 a2 b0 b1 b2 c cModAddLayout2.ancC = false ∧ (∀ (j : ℕ), cModAddState2 a0 a1 a2 b0 b1 b2 c (cModAddLayout2.C1 j) = false) ∧ (∀ (j : ℕ), cModAddState2 a0 a1 a2 b0 b1 b2 c (cModAddLayout2.C2 j) = false) ∧ cModAddState2 a0 a1 a2 b0 b1 b2 c cModAddLayout2.anc = false ∧ regValRange cModAddLayout2.A1 (cModAddState2 a0 a1 a2 b0 b1 b2 c) 3 = 2 ^ 3 - 3 ∧ regValRange cModAddLayout2.A2 (cModAddState2 a0 a1 a2 b0 b1 b2 c) 3 = 3

The hypotheses of cModAdd_correct hold at cModAddState2 (carries/ancillas clear, A1 = 5, A2 = 3), for any data / control bits. The regValRange register-value preconditions are concrete sums, discharged by decide.