Reversible modular addition — the verified value primitive (a, b) ↦ (a, (a+b) mod N) (ECDLP Phase 2, Stage S6.3b)

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

This module verifies the modular-addition VALUE primitive (a, b) ↦ (a, (a + b) mod N) over bit registers, by chaining two already-verified blocks:

modAdd L = rippleCirc L.addStep ++ modReduce L.reduceStep

• Add step rippleCirc L.addStep (Aop = the operand a, read-only addend; B holds b; fresh carry chain Cadd): with a, b < N and 2N ≤ 2ⁿ (so a + b < 2N ≤ 2ⁿ), rippleCirc_correct gives B ← (a + b) mod 2ⁿ = a + b (NO wrap, via Nat.mod_eq_of_lt).
• Reduce step modReduce L.reduceStep (S6.3a): now B holds x = a + b < 2N, so modReduce_correct applies and leaves B ← x mod N = (a + b) mod N.

The single load-bearing range fact is a + b < 2N: it is what makes the single-step S6.3a reduction apply (a 2w-bit product would need the iterated schedule). The add step's carry chain Cadd is disjoint from everything the reduce step touches (A1, A2, C1, C2, anc, B), so after the add: A1/A2 are still at their presets and C1/C2/anc are still false (frame lemmas below). B after the add is exactly a + b.

Carve line (what this is, and is NOT)

This is the value-correct modular-addition atom in the fresh-ancilla model. Group-law / field semantics are NOT in play here: this is ℕ / mod N bit arithmetic.

Named residue (do NOT read this as a clean reusable in-place primitive):

1. Dirty carries / flag (the genuine S6.3b-cleanup residue). The carry chains Cadd, C1, C2 and the comparison flag C1 n are left dirty after modAdd. Correctness holds because the layout supplies fresh wires per use (modAdd_correct requires C* / anc initialised false). In- place reuse across many additions needs carry-clean / ancilla-restoring adders — which the corpus's rippleCirc/cRippleCirc do NOT provide. Closing this needs either Cuccaro-style inline carry-uncompute adders, or reversing the carry generation, or the high-bit self-cleaning modular- adder variant. That is the genuine remaining S6.3b-cleanup work, NOT built here.
2. Uncontrolled only. This is the UNCONTROLLED modular adder. The CONTROLLED version (S6.3b-2) and the interleaved MSB-first double-and-reduce modular MULTIPLY over 𝔽_p (S6.3c) are the subsequent tranches. This module is the arithmetic core a modular multiply iterates.

So: a verified modular-addition value atom with dirty carries (fresh-ancilla model), NOT the modular multiply and NOT a clean in-place adder.

Honest cost

modularAdd_toffoli derives 12n Toffolis from the exhibited gate list: add step 2n (rippleCirc, the rippleAdder-style ripple count) + reduce step 10n (modReduceCtrl_toffoli), composed through cost_comp_toffoli_count.

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

A modular-addition layout on Fin m for n-bit registers. Bundles the operand register Aop (read-only addend a), the accumulator B (holds b, overwritten with (a+b) mod N), the add step's own carry chain Cadd, and the reduce sub-data (A1, A2, C1, C2, anc).

The geometry fields give: (i) addStep : RippleLayout well-formed (Aop, B, Cadd pairwise disjoint + bounded-injective), (ii) reduceStep : ModReduceLayout well-formed, and (iii) Cadd and Aop disjoint from every reduce-step wire so the add step's carries are fresh and the operand survives the whole circuit.

Injectivity fields are bounded (< n for registers, < n + 1 for carry chains), exactly as 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 modAdd).

• B : ℕ → Fin m

  Accumulator: holds b, overwritten with (a + b) mod N.

• Cadd : ℕ → Fin m

  Add-step carry chain (disjoint from the reduce step).

• 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
• hAopCadd (i j : ℕ) : self.Aop i ≠ self.Cadd j
• hBCadd (i j : ℕ) : self.B i ≠ self.Cadd 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
• hCaddinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Cadd i = self.Cadd j → i = j
• 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
• hCaddA1 (i j : ℕ) : self.Cadd i ≠ self.A1 j
• hCaddC1 (i j : ℕ) : self.Cadd i ≠ self.C1 j
• hCaddA2 (i j : ℕ) : self.Cadd i ≠ self.A2 j
• hCaddC2 (i j : ℕ) : self.Cadd i ≠ self.C2 j
• hCaddanc (i : ℕ) : self.Cadd 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

def Reversible.ModAddLayout.addStep {m n : ℕ} (L : ModAddLayout m n) : RippleLayout m n

The add step as a RippleLayout: operand Aop + accumulator B + add-carry chain Cadd.

Equations

• L.addStep = { A := L.Aop, B := L.B, C := L.Cadd, hAB := ⋯, hAC := ⋯, hBC := ⋯, hAinj := ⋯, hBinj := ⋯, hCinj := ⋯ }

def Reversible.ModAddLayout.reduceStep {m n : ℕ} (L : ModAddLayout 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.modAdd {m n : ℕ} (L : ModAddLayout m n) : Circuit m

The modular-addition circuit. Register add (rippleCirc) followed by the S6.3a single-step modular reduction (modReduce).

Equations

• Reversible.modAdd L = Reversible.rippleCirc L.addStep ++ Reversible.modReduce L.reduceStep

Frame: a wire disjoint from addStep's registers survives the add step

rippleCirc L.addStep touches only the wires {Aop k, B k, Cadd k} (the slices are fullAdder (Aop k) (B k) (Cadd k) (Cadd (k+1))). Any wire distinct from all of those passes through unchanged. This is the generic frame lemma; the four corollaries below specialise it to the reduce step's A1 / A2 / C1 / C2 / anc wires.

theorem Reversible.rippleCirc_addStep_preserves {m n : ℕ} {L : ModAddLayout m n} (s : State m) (w : Fin m) (hA : ∀ (k : ℕ), w ≠ L.Aop k) (hB : ∀ (k : ℕ), w ≠ L.B k) (hC : ∀ (k : ℕ), w ≠ L.Cadd k) : denote (rippleCirc L.addStep) s w = s w

Generic add-step frame. A wire w with w ≠ Aop k, w ≠ B k, w ≠ Cadd k for all k is left unchanged by rippleCirc L.addStep.

theorem Reversible.modAdd_addStep_preserves_A1 {m n : ℕ} {L : ModAddLayout m n} (s : State m) (j : ℕ) : denote (rippleCirc L.addStep) s (L.A1 j) = s (L.A1 j)

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

theorem Reversible.modAdd_addStep_preserves_A2 {m n : ℕ} {L : ModAddLayout m n} (s : State m) (j : ℕ) : denote (rippleCirc L.addStep) s (L.A2 j) = s (L.A2 j)

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

theorem Reversible.modAdd_addStep_preserves_C1 {m n : ℕ} {L : ModAddLayout m n} (s : State m) (j : ℕ) : denote (rippleCirc L.addStep) s (L.C1 j) = s (L.C1 j)

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

theorem Reversible.modAdd_addStep_preserves_C2 {m n : ℕ} {L : ModAddLayout m n} (s : State m) (j : ℕ) : denote (rippleCirc L.addStep) s (L.C2 j) = s (L.C2 j)

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

theorem Reversible.modAdd_addStep_preserves_anc {m n : ℕ} {L : ModAddLayout m n} (s : State m) : denote (rippleCirc L.addStep) s L.anc = s L.anc

After the add step, anc is unchanged.

Frame: the operand Aop survives the reduce step

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

theorem Reversible.modReduce_reduceStep_preserves_Aop {m n : ℕ} {L : ModAddLayout 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.

Value correctness

theorem Reversible.modAdd_correct {m n : ℕ} (L : ModAddLayout m n) (s : State m) (hCadd : ∀ (j : ℕ), s (L.Cadd j) = 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 (modAdd L) s) n = (a + b) % N

The verified modular-addition value primitive. For a disjoint-wire ModAddLayout with all carry chains (Cadd, C1, C2) and the ancilla 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ⁿ (so a + b < 2N ≤ 2ⁿ): modAdd L leaves register B holding (a + b) mod N.

Proof. The add step (rippleCirc_correct) writes (a + b) mod 2ⁿ = a + b to B (no wrap, since a + b < 2N ≤ 2ⁿ), preserving Aop = a (P2 of the ripple invariant) and — via the frame lemmas — the reduce step's presets A1 = 2ⁿ − N, A2 = N and clean carries C1 = C2 = false, anc = false. The reduce step (modReduce_correct, S6.3a) then maps B = a + b < 2N to (a + b) mod N.

The range hypothesis is taken as 2 * N ≤ 2 ^ n directly (the honest load-bearing form; the gloss N ≤ 2^(n-1) is only equivalent for n ≥ 1 and diverges at n = 0, so it is avoided): it forces both a + b < 2ⁿ, so the add does not wrap, and a + b < 2N, so the single-step S6.3a reduction applies.

theorem Reversible.modAdd_preserves_operand {m n : ℕ} (L : ModAddLayout m n) (s : State m) (hCadd : ∀ (j : ℕ), s (L.Cadd j) = false) {a : ℕ} (hAop : regValRange L.Aop s n = a) : regValRange L.Aop (denote (modAdd L) s) n = a

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

theorem Reversible.modAdd_in_range {m n : ℕ} (L : ModAddLayout m n) (s : State m) (hCadd : ∀ (j : ℕ), s (L.Cadd j) = 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 (modAdd L) s) n < N

The modular-addition output is a genuine residue in [0, N). Corollary of modAdd_correct and Nat.mod_lt.

Derived cost

theorem Reversible.modularAdd_toffoli {m n : ℕ} (L : ModAddLayout m n) : (circuitCost (modAdd L)).toffoli = 12 * n

Derived Toffoli cost of the modular adder: 12n Toffolis, from the exhibited gate list. Add step 2n (rippleCirc, the same ripple count as rippleAdder) + reduce step 10n (modReduceCtrl_toffoli), composed through cost_comp_toffoli_count.

Non-vacuity witness

A concrete 3-bit modular-addition layout on Fin 25:

• operand Aop → {0,1,2}, accumulator B → {3,4,5}, add-carry Cadd → {6,7,8,9},
• 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}, ancilla 24.

(n = 3 is needed, not n = 2: the modular adder requires 2N ≤ 2ⁿ so the add does not wrap; for N = 3 that forces 2ⁿ ≥ 6, i.e. n ≥ 3. At n = 2 the case a = b = 2 gives a + b = 4 = 2², which would wrap.) This exhibits that ModAddLayout is inhabited, so the headlines are not vacuously quantified. The concrete runs below add modulo N = 3 at fully specified input states: a = 2, b = 2 ↦ (2 + 2) mod 3 = 1 and a = 1, b = 1 ↦ (1 + 1) mod 3 = 2.

def Reversible.modAddLayout2 : ModAddLayout 25 3

A concrete 3-bit modular-addition layout on Fin 25.

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, so consumers cite these instead of unfolding the whole structure.

theorem Reversible.modAddLayout2_Aop (i : ℕ) : modAddLayout2.Aop i = if i = 0 then 0 else if i = 1 then 1 else 2

modAddLayout2's operand register wires.

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

modAddLayout2's accumulator wires.

theorem Reversible.modAddLayout2_Cadd (i : ℕ) : modAddLayout2.Cadd i = if i = 0 then 6 else if i = 1 then 7 else if i = 2 then 8 else 9

modAddLayout2's add-step carry-chain wires.

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

modAddLayout2's step-1 constant-register wires.

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

modAddLayout2's step-1 carry-chain wires.

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

modAddLayout2's step-3 constant-register wires.

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

modAddLayout2's step-3 carry-chain wires.

theorem Reversible.modAddLayout2_anc : modAddLayout2.anc = 24

modAddLayout2's shared ancilla wire.

def Reversible.modAddState2 (a0 a1 a2 b0 b1 b2 : Bool) : State 25

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

Equations

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

theorem Reversible.modAddState2_pre (a0 a1 a2 b0 b1 b2 : Bool) : (∀ (j : ℕ), modAddState2 a0 a1 a2 b0 b1 b2 (modAddLayout2.Cadd j) = false) ∧ (∀ (j : ℕ), modAddState2 a0 a1 a2 b0 b1 b2 (modAddLayout2.C1 j) = false) ∧ (∀ (j : ℕ), modAddState2 a0 a1 a2 b0 b1 b2 (modAddLayout2.C2 j) = false) ∧ modAddState2 a0 a1 a2 b0 b1 b2 modAddLayout2.anc = false ∧ regValRange modAddLayout2.A1 (modAddState2 a0 a1 a2 b0 b1 b2) 3 = 2 ^ 3 - 3 ∧ regValRange modAddLayout2.A2 (modAddState2 a0 a1 a2 b0 b1 b2) 3 = 3

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