Reversible modular reduction — comparison via carry-out, single-step reduce (ECDLP Phase 2, Stage S4)

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

The resource figures so far (ResourceBounds.lean) cost multiply-and-accumulate but omit the modular reduction that keeps the accumulator bounded — a real completeness gap in the Toffoli count (mulCircuit_correct_zmod discharges the reduction semantically, by reading the register in ZMod N, but exhibits no reduction circuit, so its cost is unaccounted). This module closes the gap on the verified side as far as a measurement-free, control-light gate DSL honestly allows, and names the documented residue.

Modular reduction of x (with x < 2N) is compare-and-conditional-subtract: if x ≥ N return x − N, else return x. Two facts make this cheap to verify by reusing the Tranche-2 ripple adder:

• The comparison is the carry-out. Adding the complement constant 2ⁿ − N to x overflows (carry-out = 1) iff x ≥ N. The carry-out wire C n of rippleCirc already carries this bit; rippleCirc_carryout reads it off the existing rippleCirc_invariant — no new circuit.
• The subtract is that same add. When x ≥ N (and x < 2N), rippleCirc with register A preset to 2ⁿ − N leaves register B holding (2ⁿ − N + x) mod 2ⁿ = x − N = x mod N (rippleCirc_modReduce_ge), a corollary of rippleCirc_correct.

What is proved here (verified)

• rippleCirc_carryout — the ripple adder's carry-out wire is the comparison flag decide (2ⁿ ≤ A + B). The verified core of modular reduction.
• rippleCirc_modReduce_ge — for N ≤ x < 2N and register A preset to 2ⁿ − N, the ripple adder computes x mod N into register B. A verified single-step modular reduction (the x ≥ N branch).
• mod_eq_sub_of_le_of_lt_two_mul — the ℕ spec the circuit realises: N ≤ x < 2N ⇒ x mod N = x − N.

Residue — now CLOSED by S6.3a (ModReduceCtrl.lean)

The flag-controlled conditional subtract (so the x < N branch is left untouched) was originally left as documented cost here, because it needs a controlled adder (CX→CCX, CCX→ 3-control). That wrapper is now built and verified in Reversible/ModReduceCtrl.lean (Stage S6.3a): modReduce composes this comparison core with S2's cRippleCirc (controlled add-back of N gated on the flipped flag), and modReduce_correct verifies the complete single-step reduction for both branches (regValRange B = x mod N for x < 2N), at a derived 10n Toffolis (vs the 4n documented estimate below). So rippleCirc_modReduce_ge here remains the x ≥ N corollary; the both-branch reducer is S6.3a. The original documented-cost note (kept for the historical estimate): the conditional-subtract cost lives in ResourceBounds.lean (modReduceToffoli/modMultToffoli), composed over this verified comparison core; that estimate is now superseded by the exhibited-circuit cost modReduceCtrl_toffoli = 10n.

theorem Reversible.mod_eq_sub_of_le_of_lt_two_mul {x N : ℕ} (hle : N ≤ x) (hlt : x < 2 * N) : x % N = x - N

ℕ spec of single-step reduction. For N ≤ x < 2N, the modulus is one subtraction: x mod N = x − N. The arithmetic fact the comparison-and-subtract circuit realises.

theorem Reversible.rippleCirc_carryout {m n : ℕ} (L : RippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) : denote (rippleCirc L) s (L.C n) = decide (2 ^ n ≤ regValRange L.A s n + regValRange L.B s n)

The carry-out is the comparison flag. For a disjoint-wire layout with all carries initialised false, the ripple adder's output carry wire C n holds decide (2ⁿ ≤ A + B) — it is set exactly when the addition overflows n bits, i.e. when A + B ≥ 2ⁿ. Read off rippleCirc_invariant (clause P1) together with regValRange_lt; no new circuit. This is the comparison primitive of modular reduction: preset A := 2ⁿ − N and the carry-out becomes decide (N ≤ x).

theorem Reversible.rippleCirc_modReduce_ge {m n : ℕ} (L : RippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) {N : ℕ} (hN : N ≤ 2 ^ n) (hA : regValRange L.A s n = 2 ^ n - N) (hge : N ≤ regValRange L.B s n) (hx2N : regValRange L.B s n < 2 * N) : regValRange L.B (denote (rippleCirc L) s) n = regValRange L.B s n % N

Verified single-step modular reduction (the x ≥ N branch). With register A preset to the complement constant 2ⁿ − N and register B holding x with N ≤ x < 2N, the ripple adder leaves B holding x mod N. Proof: rippleCirc_correct gives B ← (2ⁿ − N + x) mod 2ⁿ; since N ≤ x < 2ⁿ the sum is 2ⁿ + (x − N) with x − N < 2ⁿ, so the mod yields x − N, which equals x mod N by Nat.mod_eq_sub_of_le_of_lt_two_mul. The reduction value is therefore verified for the case that actually needs reducing; the flag-controlled wrapper (so the x < N case is left untouched) is now built and verified in ModReduceCtrl.lean (modReduce_correct, both branches) — S6.3a.

Non-vacuity

rippleCirc_carryout and rippleCirc_modReduce_ge inherit inhabitation of RippleLayout from rippleLayout2 (Tranche 2). The example below pins the comparison primitive at the concrete 2-bit layout, confirming the headlines are not vacuously quantified.