Reversible modular doubling — the verified value primitive a ↦ 2a mod N (ECDLP Phase 2, Stage S6.3d-1)

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

This module verifies the modular-doubling VALUE primitive a ↦ 2a mod N over bit registers, the acc ← 2·acc mod N step of the interleaved MSB-first modular multiply. It is realised as a copy followed by the already-verified S6.3b modular adder:

modDouble L = copyReg L ++ modAdd L.addLayout

• Copy step copyReg L (the only genuinely new gadget): with B holding a and the operand register Aop initially 0 on [0, n), n CNOTs CX (B i) (Aop i) copy B into Aop. Each Aop i ← Aop i ⊕ B i = 0 ⊕ B i = B i; B is the control, so it is preserved. After the copy: Aop = a, B = a.
• Add step modAdd L.addLayout (S6.3b, modAdd_correct): with Aop = a, B = a (both < N), presets A1 = 2ⁿ − N, A2 = N, carries / ancilla clean, 2N ≤ 2ⁿ, leaves B ← (a + a) mod N, and a + a = 2 * a gives 2a mod N.

The copy step touches only the wires {B i, Aop i}. So it WRITES Aop (from 0 to a, exactly the operand the add step wants), PRESERVES B (control), and leaves the add step's presets / carries (A1, A2, Cadd, C1, C2, anc) untouched — re-establishing modAdd_correct's hypotheses with a := a, b := a.

Carve line (what this is, and is NOT)

This is 2a mod N realised as copy ++ modAdd, reusing wholesale the verified S6.3b modAdd. The only new verified content is the copyReg CNOT-copy gadget (copyReg_correct). This is ℕ / mod N bit arithmetic; no group-law / field semantics are in play.

Named residue (same fresh-ancilla model as S6.3b; do NOT read as a clean in-place primitive):

1. Operand copy left dirty. After modDouble, the operand register Aop is left holding a (not restored to 0), and — inherited from modAdd — the carry chains Cadd, C1, C2 and the comparison flag are dirty. Correctness holds because the layout supplies fresh wires per use. In- place reuse across many doublings needs the carry-clean / ancilla-restoring adders the corpus does NOT yet provide (Cuccaro-style inline uncompute, or the self-cleaning high-bit modular adder).
2. This is the doubling PRIMITIVE, not the multiply. The full interleaved MSB-first modular MULTIPLY over 𝔽_p (the Horner loop of modDouble + cModAdd with the running acc < N invariant) is the subsequent tranche (S6.3d-2). This module is the acc ← 2·acc mod N atom that loop iterates.

Honest cost

modDouble_toffoli derives 12n Toffolis: copy step 0 (n CNOTs, no Toffoli) + add step 12n (modularAdd_toffoli), composed through cost_comp_toffoli_count. The copy contributes n CNOTs (modDouble_cnot_copy), which do not add Toffolis.

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

A modular-doubling layout on Fin m for n-bit registers. It is exactly a ModAddLayout: the copy step reuses the same two registers the add step uses — B (holds a, the doubled accumulator) and Aop (the operand, initially 0, copied to a). No new wire families are needed. All disjointness / bounded-injectivity facts come for free from the bundled ModAddLayout.

• addLayout : ModAddLayout m n

  The bundled S6.3b modular-addition layout (supplies every register + geometry fact).

def Reversible.ModDoubleLayout.B {m n : ℕ} (L : ModDoubleLayout m n) : ℕ → Fin m

The doubled accumulator register (B of the bundled add layout); holds a, overwritten with 2a mod N.

Equations

• L.B = L.addLayout.B

def Reversible.ModDoubleLayout.Aop {m n : ℕ} (L : ModDoubleLayout m n) : ℕ → Fin m

The operand register (Aop of the bundled add layout); initially 0, copied to a.

Equations

• L.Aop = L.addLayout.Aop

The copy gadget

def Reversible.copyReg {m n : ℕ} (L : ModDoubleLayout m n) : Circuit m

The copy circuit: n CNOTs CX (B i) (Aop i), copying register B into register Aop.

Equations

• Reversible.copyReg L = List.map (fun (i : ℕ) => Reversible.Gate.CX (L.B i) (L.Aop i)) (List.range n)

def Reversible.modDouble {m n : ℕ} (L : ModDoubleLayout m n) : Circuit m

The modular-doubling circuit. Copy B into Aop, then add (modAdd): 2a = a + a.

Equations

• Reversible.modDouble L = Reversible.copyReg L ++ Reversible.modAdd L.addLayout

Copy-step frame: a wire disjoint from {B i, Aop i} survives

copyReg L touches only the wires {B k, Aop k} (the k-th gate is CX (B k) (Aop k), whose gateWires is {B k, Aop k}). Any wire distinct from all of those passes through unchanged.

theorem Reversible.copyReg_preserves {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (w : Fin m) (hB : ∀ (k : ℕ), w ≠ L.B k) (hA : ∀ (k : ℕ), w ≠ L.Aop k) : denote (copyReg L) s w = s w

Generic copy-step frame. A wire w with w ≠ B k, w ≠ Aop k for all k is left unchanged by copyReg L.

Copy-step value correctness

The CNOTs have pairwise-disjoint targets (Aop injective on [0, n)) and never target a control (hAopB), so each Aop i is touched by exactly its own CNOT, and B is never a target. We prove the prefix invariant by induction: after the first k copies, Aop i = B i for i < k, Aop i unchanged for k ≤ i, and B everywhere preserved.

def Reversible.copyPrefix {m n : ℕ} (L : ModDoubleLayout m n) (k : ℕ) : Circuit m

The circuit of the first k copies.

Equations

• Reversible.copyPrefix L k = List.map (fun (i : ℕ) => Reversible.Gate.CX (L.B i) (L.Aop i)) (List.range k)

theorem Reversible.copyReg_eq_prefix {m n : ℕ} (L : ModDoubleLayout m n) : copyReg L = copyPrefix L n

theorem Reversible.denote_copyPrefix_succ {m n : ℕ} (L : ModDoubleLayout m n) (k : ℕ) (s : State m) : denote (copyPrefix L (k + 1)) s = denoteGate (Gate.CX (L.B k) (L.Aop k)) (denote (copyPrefix L k) s)

theorem Reversible.copyPrefix_preserves {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (w : Fin m) (k : ℕ) (hB : ∀ (j : ℕ), w ≠ L.B j) (hA : ∀ (j : ℕ), w ≠ L.Aop j) : denote (copyPrefix L k) s w = s w

A wire disjoint from {B i, Aop i} survives the first k copies (the prefix frame).

theorem Reversible.copyReg_invariant {m n : ℕ} (L : ModDoubleLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.Aop i) = false) (k : ℕ) : k ≤ n → (∀ i < k, denote (copyPrefix L k) s (L.Aop i) = s (L.B i)) ∧ (∀ (i : ℕ), k ≤ i → i < n → denote (copyPrefix L k) s (L.Aop i) = s (L.Aop i)) ∧ ∀ (j : ℕ), denote (copyPrefix L k) s (L.B j) = s (L.B j)

The copy invariant. Assuming Aop is initially 0 on [0, n), after the first k copies: Aop i = B i for i < k, Aop i is unchanged for k ≤ i < n, and B j is preserved for all j. The B preservation holds because B is never a CNOT target (hAopB); the Aop clauses hold because the targets are pairwise disjoint (Aop injective).

theorem Reversible.copyReg_correct_operand {m n : ℕ} (L : ModDoubleLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.Aop i) = false) : regValRange L.Aop (denote (copyReg L) s) n = regValRange L.B s n

Copy correctness — operand. With Aop initially 0, after the copy the operand register reads the value B held: regValRange Aop (denote (copyReg L) s) n = regValRange B s n.

theorem Reversible.copyReg_correct_B {m n : ℕ} (L : ModDoubleLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.Aop i) = false) : regValRange L.B (denote (copyReg L) s) n = regValRange L.B s n

Copy correctness — accumulator preserved. The copy leaves register B unchanged (it is the control, never a CNOT target). Note B is NOT disjoint from the gate wires (each B k is a control wire), so this is read off the invariant's B-preservation clause, not the generic frame lemma.

Copy-step frame for the add-step presets / carries

The add step (modAdd L.addLayout) reads A1, A2, Cadd, C1, C2, anc. Each is disjoint from both B and Aop (the only wires copyReg touches), so all survive the copy and modAdd's preset / clean-carry hypotheses re-establish. The hAop* / hB* fields of ModAddLayout supply the disjointness; the helper below packages the per-wire frame for each.

theorem Reversible.copyReg_preserves_A1 {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (j : ℕ) : denote (copyReg L) s (L.addLayout.A1 j) = s (L.addLayout.A1 j)

After the copy, A1 is unchanged on every wire.

theorem Reversible.copyReg_preserves_A2 {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (j : ℕ) : denote (copyReg L) s (L.addLayout.A2 j) = s (L.addLayout.A2 j)

After the copy, A2 is unchanged on every wire.

theorem Reversible.copyReg_preserves_Cadd {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (j : ℕ) : denote (copyReg L) s (L.addLayout.Cadd j) = s (L.addLayout.Cadd j)

After the copy, the add-carry chain Cadd is unchanged on every wire.

theorem Reversible.copyReg_preserves_C1 {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (j : ℕ) : denote (copyReg L) s (L.addLayout.C1 j) = s (L.addLayout.C1 j)

After the copy, the reduce step-1 carry C1 is unchanged on every wire.

theorem Reversible.copyReg_preserves_C2 {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) (j : ℕ) : denote (copyReg L) s (L.addLayout.C2 j) = s (L.addLayout.C2 j)

After the copy, the reduce step-3 carry C2 is unchanged on every wire.

theorem Reversible.copyReg_preserves_anc {m n : ℕ} {L : ModDoubleLayout m n} (s : State m) : denote (copyReg L) s L.addLayout.anc = s L.addLayout.anc

After the copy, the shared ancilla anc is unchanged.

Value correctness of the modular doubler

theorem Reversible.modDouble_correct {m n : ℕ} (L : ModDoubleLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.Aop i) = false) (hCadd : ∀ (j : ℕ), s (L.addLayout.Cadd j) = false) (hC1 : ∀ (j : ℕ), s (L.addLayout.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.addLayout.C2 j) = false) (hanc : s L.addLayout.anc = false) {N a : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hA1 : regValRange L.addLayout.A1 s n = 2 ^ n - N) (hA2 : regValRange L.addLayout.A2 s n = N) (hB : regValRange L.B s n = a) (haN : a < N) : regValRange L.B (denote (modDouble L) s) n = 2 * a % N

The verified modular-doubling value primitive. For a ModDoubleLayout with operand register Aop initially 0 on [0, n), accumulator B holding a < N, with 2N ≤ 2ⁿ, presets A1 = 2ⁿ − N, A2 = N, and all carries (Cadd, C1, C2) and ancilla anc clean: modDouble L leaves register B holding (2 * a) mod N.

Proof. The copy step (copyReg_correct_operand / copyReg_correct_B) writes a to Aop and preserves B = a, and (copyReg_preserves_*) leaves the add step's presets A1 = 2ⁿ − N, A2 = N and clean carries Cadd = C1 = C2 = false, anc = false. So modAdd_correct applies with a := a, b := a, giving B ← (a + a) mod N; rewriting a + a = 2 * a finishes.

theorem Reversible.modDouble_in_range {m n : ℕ} (L : ModDoubleLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.Aop i) = false) (hCadd : ∀ (j : ℕ), s (L.addLayout.Cadd j) = false) (hC1 : ∀ (j : ℕ), s (L.addLayout.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.addLayout.C2 j) = false) (hanc : s L.addLayout.anc = false) {N a : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hA1 : regValRange L.addLayout.A1 s n = 2 ^ n - N) (hA2 : regValRange L.addLayout.A2 s n = N) (hB : regValRange L.B s n = a) (haN : a < N) : regValRange L.B (denote (modDouble L) s) n < N

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

Derived cost

theorem Reversible.copyReg_cnot {m n : ℕ} (L : ModDoubleLayout m n) : (circuitCost (copyReg L)).cnot = n

Copy-step CNOT count: n CNOTs (and zero Toffoli). The copy is n CX gates.

theorem Reversible.copyReg_toffoli {m n : ℕ} (L : ModDoubleLayout m n) : (circuitCost (copyReg L)).toffoli = 0

Copy-step Toffoli count: zero — the copy is n CNOTs, no Toffoli.

theorem Reversible.modDouble_toffoli {m n : ℕ} (L : ModDoubleLayout m n) : (circuitCost (modDouble L)).toffoli = 12 * n

Derived Toffoli cost of the modular doubler: 12n Toffolis, from the exhibited gate list. Copy step 0 (copyReg_toffoli, the n CNOTs carry no Toffoli) + add step 12n (modularAdd_toffoli), composed through cost_comp_toffoli_count.

theorem Reversible.modDouble_cnot_copy {m n : ℕ} (L : ModDoubleLayout m n) : (circuitCost (modDouble L)).cnot = n + (circuitCost (modAdd L.addLayout)).cnot

Copy contributes n CNOTs to the doubler (reported separately; they do not add Toffolis).

Non-vacuity witness

A concrete 3-bit modular-doubling layout on Fin 25, reusing the S6.3b modAddLayout2 (operand Aop → {0,1,2}, accumulator B → {3,4,5}, add-carry Cadd → {6..9}, reduce presets / carries A1,C1,A2,C2,anc → {10..24}). n = 3 is needed (not n = 2): the modular adder requires 2N ≤ 2ⁿ, so for N = 3 that forces 2ⁿ ≥ 6, i.e. n ≥ 3.

The concrete runs double modulo N = 3: a = 2 ↦ (2 * 2) mod 3 = 1 and a = 1 ↦ (2 * 1) mod 3 = 2, with the operand Aop initialised 0 (so the copy seeds it from B = a).

def Reversible.modDoubleLayout2 : ModDoubleLayout 25 3

A concrete 3-bit modular-doubling layout on Fin 25, bundling modAddLayout2.

Equations

• Reversible.modDoubleLayout2 = { addLayout := Reversible.modAddLayout2 }

def Reversible.modDoubleState2 (b0 b1 b2 : Bool) : State 25

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

Equations

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

theorem Reversible.modDoubleState2_pre (b0 b1 b2 : Bool) : (∀ i < 3, modDoubleState2 b0 b1 b2 (modDoubleLayout2.Aop i) = false) ∧ (∀ (j : ℕ), modDoubleState2 b0 b1 b2 (modDoubleLayout2.addLayout.Cadd j) = false) ∧ (∀ (j : ℕ), modDoubleState2 b0 b1 b2 (modDoubleLayout2.addLayout.C1 j) = false) ∧ (∀ (j : ℕ), modDoubleState2 b0 b1 b2 (modDoubleLayout2.addLayout.C2 j) = false) ∧ modDoubleState2 b0 b1 b2 modDoubleLayout2.addLayout.anc = false ∧ regValRange modDoubleLayout2.addLayout.A1 (modDoubleState2 b0 b1 b2) 3 = 2 ^ 3 - 3 ∧ regValRange modDoubleLayout2.addLayout.A2 (modDoubleState2 b0 b1 b2) 3 = 3

The hypotheses of modDouble_correct hold at modDoubleState2 (operand 0, carries / ancilla clear, A1 = 5, A2 = 3), for any data bits.

Fast #eval cross-check (Eval harness)

runArr / regValRangeArr (Eval.lean) compute the same denote / regValRange value the theorems are stated about (regValRangeArr_eq), but on a strict Array Bool — instant, no lazy Function.update blowup. The #evals below print 2a mod N off register B for the two witnesses; the decide examples confirm the printed numbers (kernel-reduced through the bridge).