Reversible modular reduction — the complete single-step reduce circuit (ECDLP Phase 2, Stage S6.3a)

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

S4 (ModReduce.lean) verified the comparison-as-carry-out primitive and the x ≥ N reduce value (rippleCirc_modReduce_ge), but left the flag-controlled wrapper and the x < N branch as documented cost, not as an exhibited circuit (ResourceBounds.modReduceToffoli is a documented estimate, not derived from a reduce circuit). This module closes that residue: it exhibits and proves the complete single-step modular reduction circuit, both branches, from already-verified primitives only.

The circuit (modReduce)

For x in register B with x < 2N (and x < 2ⁿ, N ≤ 2ⁿ):

modReduce L = rippleCirc L1 ++ [Gate.X flag] ++ cRippleCirc L2

• Step 1 rippleCirc L1 (A1 preset to 2ⁿ − N, B, fresh carry chain C1): adds the complement constant, so B ← (x + 2ⁿ − N) mod 2ⁿ, and flag := C1 n (the carry-out) becomes decide (N ≤ x) (rippleCirc_correct + rippleCirc_carryout).
• Step 2 X flag: flips the flag to decide (x < N) = ¬ decide (N ≤ x).
• Step 3 cRippleCirc L2 (A2 preset to N, same B, second fresh carry chain C2, ctrl := flag, fresh ancilla anc): controlled add-back of N, conditional on x < N (cRippleCirc_correct).

The arithmetic (verified in modReduce_correct):

• x ≥ N: flag clears, no add-back; step-1 value (x + 2ⁿ − N) mod 2ⁿ = x − N = x mod N (using N ≤ x < 2ⁿ and S4's mod_eq_sub_of_le_of_lt_two_mul).
• x < N: flag sets; step-1 value is x + 2ⁿ − N (no wrap, since x < N ≤ 2ⁿ), then + N mod 2ⁿ = (x + 2ⁿ) mod 2ⁿ = x = x mod N.

What is NEW vs S4

S4's rippleCirc_modReduce_ge handled only the x ≥ N branch and no control — the reduce was the bare adder, correct only when a subtract was actually needed. This module does both branches in one reversible pass, with the comparison flag controlling the conditional add-back via S2's cRippleCirc. So: comparison VERIFIED (S4), x ≥ N reduce VERIFIED (S4), and now the flag-controlled wrapper + the x < N identity branch are exhibited circuits, VERIFIED (S6.3a) — the documented residue of S4 §"Documented residue" is closed.

Honest cost

modReduceCtrl_toffoli derives 2n + 8n = 10n Toffolis from the exhibited gate list (step-1 ripple 2n, the X flip 0, step-3 controlled ripple 8n via cRippleCirc_toffoli). This is heavier than S4's documented estimate modReduceToffoli n = 4n: the controlled add-back is 8n (the quantum×quantum overhead of S2, 4× the 2n of an uncontrolled add), not the ~2n an idealised in-place subtract would suggest. That is the honest cost of a verified reduction (compare-and- conditional-subtract, both branches, in the 2-control DSL) versus S4's documented uncontrolled-add estimate.

Remaining residue (named, not built)

1. Cleanup / reversibility (S6.3b concern). The comparison flag C1 n is left holding decide (x < N), the step-1 carry chain C1 holds garbage, and C2/anc are restored clean by cRippleCirc but C1/flag are not uncomputed. The value correctness of B holds regardless (modReduce_correct), but in-place reuse inside a multiply needs the standard recompute-and-uncompute of the flag and step-1 carries. Naming, not building, that uncompute pass here.
2. Full product reduction. A 2w-bit product (x up to ~N²) is reduced by the multi-step / interleaved schedule that keeps the accumulator < 2N and applies this primitive each step. This module is the single-step (x < 2N) primitive that schedule iterates; the full modular multiply is S6.3b.

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

A single-step modular-reduction layout on Fin m for n-bit registers. Bundles:

• B — the data register (holds x, overwritten with x mod N);
• A1 — the step-1 constant register (preset to 2ⁿ − N), with fresh carry chain C1 (whose output wire C1 n is the comparison flag);
• A2 — the step-3 constant register (preset to N), with a second fresh carry chain C2;
• anc — the shared clean ancilla for the controlled add-back.

The fields are pure wire geometry (pairwise disjointness + per-range bounded injectivity), mirroring the RippleLayout/CRippleLayout discipline. The injectivity fields are bounded (< n for registers, < n + 1 for carry chains) exactly as MulLayout/CMulLayout — an unbounded ℕ → Fin m injectivity field is uninhabitable and would make the theorem vacuous.

• B : ℕ → Fin m

  Data register: holds x, overwritten with x mod N.

• A1 : ℕ → Fin m

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

• C1 : ℕ → Fin m

  Step-1 carry chain; C1 n is the comparison flag (the control of step 3).

• A2 : ℕ → Fin m

  Step-3 constant register (preset to N).

• C2 : ℕ → Fin m

  Step-3 carry chain (distinct from C1).

• anc : Fin m

  Shared clean ancilla for the controlled add-back.

• 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
• hBinj (i j : ℕ) : i < n → j < n → self.B i = self.B j → i = 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

def Reversible.ModReduceLayout.stepOne {m n : ℕ} (L : ModReduceLayout m n) : RippleLayout m n

Step 1 as a RippleLayout: register A1 + data B + carry chain C1.

Equations

• L.stepOne = { A := L.A1, B := L.B, C := L.C1, hAB := ⋯, hAC := ⋯, hBC := ⋯, hAinj := ⋯, hBinj := ⋯, hCinj := ⋯ }

def Reversible.ModReduceLayout.stepThree {m n : ℕ} (L : ModReduceLayout m n) : CRippleLayout m n

Step 3 as a CRippleLayout: register A2 + data B + carry chain C2, controlled on the flag C1 n, with the shared ancilla.

Equations

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

def Reversible.modReduce {m n : ℕ} (L : ModReduceLayout m n) : Circuit m

The single-step modular-reduction circuit. rippleCirc (add complement 2ⁿ − N, produce the comparison flag) ++ [X flag] (flip flag to x < N) ++ cRippleCirc (controlled add-back of N).

Equations

• Reversible.modReduce L = Reversible.rippleCirc L.stepOne ++ [Reversible.Gate.X (L.C1 n)] ++ Reversible.cRippleCirc L.stepThree

Frame: step-3 inputs survive steps 1 and 2

Step 1 (rippleCirc L.stepOne) touches only {A1 k, B k, C1 k} and step 2 (X (C1 n)) only {C1 n}. The step-3 carry chain C2, constant A2, and ancilla anc are disjoint from those, so their values pass through steps 1 + 2 unchanged.

theorem Reversible.modReduce_stepTwo_preserves_B {m n : ℕ} {L : ModReduceLayout m n} (s : State m) (j : ℕ) : denoteGate (Gate.X (L.C1 n)) s (L.B j) = s (L.B j)

The data-register window B is untouched by the flag flip (step 2): C1 n ≠ B j.

theorem Reversible.modReduce_steps12_preserves_C2 {m n : ℕ} {L : ModReduceLayout m n} (s : State m) (j : ℕ) : denoteGate (Gate.X (L.C1 n)) (denote (rippleCirc L.stepOne) s) (L.C2 j) = s (L.C2 j)

Steps 1 + 2 leave the step-3 carry chain C2 j at its initial value.

theorem Reversible.modReduce_steps12_preserves_A2 {m n : ℕ} {L : ModReduceLayout m n} (s : State m) (j : ℕ) : denoteGate (Gate.X (L.C1 n)) (denote (rippleCirc L.stepOne) s) (L.A2 j) = s (L.A2 j)

Steps 1 + 2 leave the step-3 constant register A2 j at its initial value.

theorem Reversible.modReduce_steps12_preserves_anc {m n : ℕ} {L : ModReduceLayout m n} (s : State m) : denoteGate (Gate.X (L.C1 n)) (denote (rippleCirc L.stepOne) s) L.anc = s L.anc

Steps 1 + 2 leave the shared ancilla anc at its initial value.

Value correctness, both branches

theorem Reversible.modReduce_correct {m n : ℕ} (L : ModReduceLayout m n) (s : State m) (hC1 : ∀ (j : ℕ), s (L.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.C2 j) = false) (hanc : s L.anc = false) {N : ℕ} (hN : N ≤ 2 ^ n) (hA1 : regValRange L.A1 s n = 2 ^ n - N) (hA2 : regValRange L.A2 s n = N) (hx2N : regValRange L.B s n < 2 * N) : regValRange L.B (denote (modReduce L) s) n = regValRange L.B s n % N

The complete single-step modular reduction — both branches, verified from the exhibited circuit. For a disjoint-wire ModReduceLayout with the step-1 carry chain C1, the step-3 carry chain C2, and the ancilla anc all initialised false, register A1 preset to 2ⁿ − N, register A2 preset to N, and data B holding x with N ≤ 2ⁿ, x < 2ⁿ, x < 2N: the circuit modReduce L leaves B holding x mod N.

Proof. Step 1 (rippleCirc_correct) writes (x + 2ⁿ − N) mod 2ⁿ to B and sets the flag C1 n = decide (N ≤ x) (rippleCirc_carryout); step 2 flips it to decide (x < N); step 3 (cRippleCirc_correct) adds N back iff the flag is set. The two branches:

• x ≥ N (flag clear): step-1 value (x + 2ⁿ − N) mod 2ⁿ = x − N (N ≤ x < 2ⁿ), and x − N = x mod N (mod_eq_sub_of_le_of_lt_two_mul); add-back skipped.
• x < N (flag set): step-1 value x + 2ⁿ − N (no wrap, x < N ≤ 2ⁿ), then + N mod 2ⁿ = (x + 2ⁿ) mod 2ⁿ = x = x mod N.

This closes S4's documented residue: comparison + conditional-subtract + both branches, derived from circuits, not documented.

theorem Reversible.modReduce_in_range {m n : ℕ} (L : ModReduceLayout m n) (s : State m) (hC1 : ∀ (j : ℕ), s (L.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.C2 j) = false) (hanc : s L.anc = false) {N : ℕ} (hNpos : 0 < N) (hN : N ≤ 2 ^ n) (hA1 : regValRange L.A1 s n = 2 ^ n - N) (hA2 : regValRange L.A2 s n = N) (hx2N : regValRange L.B s n < 2 * N) : regValRange L.B (denote (modReduce L) s) n < N

The reducer output is a genuine residue in [0, N). A direct corollary of modReduce_correct and Nat.mod_lt: the property a modular reducer must have.

Derived cost

theorem Reversible.modReduceCtrl_toffoli {m n : ℕ} (L : ModReduceLayout m n) : (circuitCost (modReduce L)).toffoli = 10 * n

Derived Toffoli cost of the single-step reduce circuit: 10n Toffolis, from the exhibited gate list. Step 1 (rippleCirc) is 2n (rippleAdder_toffoli-style, here read via the same ripple count), the X flip is 0, and step 3 (cRippleCirc) is 8n (cRippleCirc_toffoli); composed through the Tranche-1 additivity cost_comp_toffoli_count. This is heavier than S4's documented modReduceToffoli n = 4n: the verified controlled add-back costs 8n (the quantum×quantum overhead of S2, 4× an uncontrolled add), the honest price of an exhibited both-branch reduction.

Non-vacuity witness

A concrete 2-bit reduce layout on Fin 13:

• data B → {0,1}, step-1 constant A1 → {2,3}, step-1 carry chain C1 → {4,5,6},
• step-3 constant A2 → {7,8}, step-3 carry chain C2 → {9,10,11}, ancilla 12.

This exhibits that ModReduceLayout is inhabited (the bounded-injectivity bundle is satisfiable), so the headlines are not vacuously quantified. The concrete computations below run the reducer on n = 2, N = 3 at two fully-specified input states, checking x = 3 ↦ 0 (the x ≥ N subtract branch) and x = 2 ↦ 2 (the x < N identity branch). [The spec's illustrative x = 5 ↦ 2 needs n = 3: 5 < 2³ = 8; at n = 2, x < 2² = 4, so 5 is not representable in two wires.]

def Reversible.modReduceLayout2 : ModReduceLayout 13 2

A concrete 2-bit reduce layout on Fin 13.

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.modReduceLayout2_B (i : ℕ) : modReduceLayout2.B i = if i = 0 then 0 else 1

modReduceLayout2's data-register wires.

theorem Reversible.modReduceLayout2_A1 (i : ℕ) : modReduceLayout2.A1 i = if i = 0 then 2 else 3

modReduceLayout2's step-1 constant-register wires.

theorem Reversible.modReduceLayout2_C1 (i : ℕ) : modReduceLayout2.C1 i = if i = 0 then 4 else if i = 1 then 5 else 6

modReduceLayout2's step-1 carry-chain wires.

theorem Reversible.modReduceLayout2_A2 (i : ℕ) : modReduceLayout2.A2 i = if i = 0 then 7 else 8

modReduceLayout2's step-3 constant-register wires.

theorem Reversible.modReduceLayout2_C2 (i : ℕ) : modReduceLayout2.C2 i = if i = 0 then 9 else if i = 1 then 10 else 11

modReduceLayout2's step-3 carry-chain wires.

theorem Reversible.modReduceLayout2_anc : modReduceLayout2.anc = 12

modReduceLayout2's ancilla wire.

def Reversible.modReduceState2 (b0 b1 : Bool) : State 13

Concrete input state for n = 2, N = 3: data B = x (wires 0,1), A1 = 1 = 2² − 3 (wire 2), A2 = 3 (wires 7,8), all carries / ancilla false. Parameterised by the two data bits b0, b1 of x.

Equations

• Reversible.modReduceState2 b0 b1 w = if w = 0 then b0 else if w = 1 then b1 else if w = 2 then true else if w = 7 then true else if w = 8 then true else false

theorem Reversible.modReduceState2_pre (b0 b1 : Bool) : (∀ (j : ℕ), modReduceState2 b0 b1 (modReduceLayout2.C1 j) = false) ∧ (∀ (j : ℕ), modReduceState2 b0 b1 (modReduceLayout2.C2 j) = false) ∧ modReduceState2 b0 b1 modReduceLayout2.anc = false ∧ regValRange modReduceLayout2.A1 (modReduceState2 b0 b1) 2 = 2 ^ 2 - 3 ∧ regValRange modReduceLayout2.A2 (modReduceState2 b0 b1) 2 = 3

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