Reversible interleaved modular multiply — the verified Horner LOOP BODY (ECDLP Phase 2, Stage S6.3d-2a)

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

This module verifies the loop body of the interleaved MSB-first modular multiply over 𝔽_p, acc ← (2·acc + [X_i]·Y) mod N, by chaining the two already-verified blocks one tranche below:

hornerStep L = modDouble L.dbl ++ cModAdd L.add

• modDouble modDouble L.dbl (S6.3d-1, modDouble_correct / modDouble_in_range): with the accumulator B holding c < N, its scratch operand dbl.Aop initialised 0, presets A1 = 2ⁿ − N, A2 = N, clean carries / ancilla, and 2N ≤ 2ⁿ, it leaves B ← (2c) mod N, with (2c) mod N < N. It touches only its own wires {B, dbl.Aop, dbl.Cadd, dbl.A1, dbl.C1, dbl.A2, dbl.C2, dbl.anc}, so the multiplicand Y = add.Aop, the control bit X_i = add.ctrl, and the controlled-add step's fresh carries / presets / ancilla all survive it (the frame lemmas modDouble_preserves_external and corollaries below).
• cModAdd cModAdd L.add (S6.3c, cModAdd_correct): now B = d := (2c) mod N < N, operand Aop = Y (Yval < N), control ctrl = X_i. It leaves B ← if X_i then (Yval + d) mod N else d.

Composition (the loop-body identity, absorbing the inner mod N via Nat.add_mod / Nat.mod_add_mod):

• X_i set: (Yval + (2c mod N)) mod N = (Yval + 2c) mod N = (2c + Yval) mod N.
• X_i clear: (2c) mod N = (2c + 0) mod N.

So hornerStep_correct gives B ← (2*c + (if X_i then Yval else 0)) mod N.

Carve line (what this is, and is NOT)

This is the verified LOOP BODY of the interleaved MSB-first modular multiply, acc ← (2·acc + [X_i]·Y) mod N, composing the verified modDouble (S6.3d-1) and cModAdd (S6.3c). The 2-step composition is delivered two ways: (i) the proven mulStep2_correct, which chains hornerStep_correct twice over two banks sharing B and Y with fresh per-bank wires, concluding acc = (X · Yval) mod N for the 2-bit multiplier X = 2·X₁ + X₀; and (ii) a concrete Fin 92 instance (mulCircuit2 / mulState2) whose three #eval / decide witnesses realise X = 3 ↦ 0, X = 2 ↦ 1, X = 1 ↦ 2 at Y = 2, N = 3 (the verified n = 2 modular multiply).

This is NOT the general-n multiply. The general-n Horner loop — the induction folding hornerStep over all n bits of X with the invariant acc = (X ≫ i)·Y mod N — is the subsequent tranche S6.3d-2b, NOT built here — it lives in ModularMulLoop.lean (mulLoop_correct).

The fresh-ancilla / dirty-carry model (inherited from S6.3d-1 and S6.3c):

1. Fresh per-iteration wires (O(n²) qubits). Each Horner step is supplied its OWN doubling scratch / carries / ancilla and its OWN controlled-add carries / ancilla, disjoint from the previous step's. The 2-step demo exhibits exactly this: two banks, fresh wires each. Across n steps this is Θ(n²) ancilla. In-place reuse (Θ(n) qubits) needs a carry-clean / ancilla-restoring adder — supplied by CuccaroModAdd.lean (cuccaroModAdd_clean) and folded into the Θ(n)-qubit multiply in CuccaroModMul.lean; NOT built here.
2. Only the multiplicand Y must persist across steps. The loop reads each X_i once (the bit wire of step i is dead after step i), but Y = add.Aop must survive every step; this is the load-bearing hornerStep_preserves_Y.

Honest cost

hornerStep_toffoli derives 30n Toffolis from the exhibited gate list: modDouble 12n (modDouble_toffoli) + cModAdd 18n (cModularAdd_toffoli), composed through cost_comp_toffoli_count.

Generic frame: a wire external to modReduce / modAdd / modDouble survives

modDouble L = copyReg L ++ modAdd L.addLayout and modAdd L = rippleCirc L.addStep ++ modReduce L.reduceStep. Each block is a frame lemma over its wire families; the three lemmas below compose them so that a wire disjoint from every modDouble-touched family passes through unchanged. These are the only genuinely new structural lemmas of this tranche.

theorem Reversible.modReduce_preserves_external {m n : ℕ} (L : ModReduceLayout m n) (s : State m) (w : Fin m) (hB : ∀ (j : ℕ), w ≠ L.B j) (hA1 : ∀ (j : ℕ), w ≠ L.A1 j) (hC1 : ∀ (j : ℕ), w ≠ L.C1 j) (hA2 : ∀ (j : ℕ), w ≠ L.A2 j) (hC2 : ∀ (j : ℕ), w ≠ L.C2 j) (hanc : w ≠ L.anc) : denote (modReduce L) s w = s w

modReduce frame. A wire w disjoint from every reduce-step family (B, A1, C1, A2, C2, anc) is left unchanged by modReduce L. Mirrors modReduce_reduceStep_preserves_Aop but abstracted to an arbitrary external wire and a bare ModReduceLayout.

theorem Reversible.modAdd_preserves_external {m n : ℕ} (L : ModAddLayout m n) (s : State m) (w : Fin m) (hAop : ∀ (j : ℕ), w ≠ L.Aop j) (hB : ∀ (j : ℕ), w ≠ L.B j) (hCadd : ∀ (j : ℕ), w ≠ L.Cadd j) (hA1 : ∀ (j : ℕ), w ≠ L.A1 j) (hC1 : ∀ (j : ℕ), w ≠ L.C1 j) (hA2 : ∀ (j : ℕ), w ≠ L.A2 j) (hC2 : ∀ (j : ℕ), w ≠ L.C2 j) (hanc : w ≠ L.anc) : denote (modAdd L) s w = s w

modAdd frame. A wire w disjoint from every modAdd-touched family (Aop, B, Cadd, A1, C1, A2, C2, anc) is left unchanged by modAdd L. Composes rippleCirc_addStep_preserves (add step) with modReduce_preserves_external (reduce step).

theorem Reversible.modDouble_preserves_external {m n : ℕ} (L : ModDoubleLayout m n) (s : State m) (w : Fin m) (hB : ∀ (j : ℕ), w ≠ L.B j) (hAop : ∀ (j : ℕ), w ≠ L.Aop j) (hCadd : ∀ (j : ℕ), w ≠ L.addLayout.Cadd j) (hA1 : ∀ (j : ℕ), w ≠ L.addLayout.A1 j) (hC1 : ∀ (j : ℕ), w ≠ L.addLayout.C1 j) (hA2 : ∀ (j : ℕ), w ≠ L.addLayout.A2 j) (hC2 : ∀ (j : ℕ), w ≠ L.addLayout.C2 j) (hanc : w ≠ L.addLayout.anc) : denote (modDouble L) s w = s w

modDouble frame. A wire w disjoint from every modDouble-touched family (B, the scratch operand dbl.Aop, and the bundled add layout's Cadd, A1, C1, A2, C2, anc) is left unchanged by modDouble L. Composes copyReg_preserves (copy step) with modAdd_preserves_external (the bundled modAdd).

theorem Reversible.cModAdd_preserves_external {m n : ℕ} (L : CModAddLayout m n) (s : State m) (w : Fin m) (hAop : ∀ k < n, w ≠ L.Aop k) (hB : ∀ (k : ℕ), w ≠ L.B k) (hctrl : w ≠ L.ctrl) (hCcadd : ∀ k < n + 1, w ≠ L.Ccadd k) (hancC : w ≠ L.ancC) (hA1 : ∀ (j : ℕ), w ≠ L.A1 j) (hC1 : ∀ (j : ℕ), w ≠ L.C1 j) (hA2 : ∀ (j : ℕ), w ≠ L.A2 j) (hC2 : ∀ (j : ℕ), w ≠ L.C2 j) (hanc : w ≠ L.anc) : denote (cModAdd L) s w = s w

cModAdd frame. A wire w disjoint from every cModAdd-touched family (Aop, B, Ccadd, ctrl, ancC of the controlled add, and A1, C1, A2, C2, anc of the reduce) is left unchanged by cModAdd L. Composes cRippleCirc_preserves_external (controlled add step) with modReduce_preserves_external (reduce step). Register hyps are bounded (< n / < n + 1), as in cRippleCirc_preserves_external.

The Horner-step layout

A HornerStepLayout bundles the S6.3d-1 doubling sub-layout dbl and the S6.3c controlled-add sub-layout add, sharing the accumulator (dbl.B = add.B, the running acc), with the doubling's wires (scratch operand + carries + ancilla) and the controlled-add's wires (carries + ancilla) fresh and disjoint from each other, from the multiplicand Y = add.Aop, and from the control bit X_i = add.ctrl. The cross-disjointness fields are exactly what modDouble_preserves_external needs to re-establish every cModAdd_correct hypothesis through the doubling.

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

A Horner-step layout for n-bit registers on Fin m. The two sub-layouts share the accumulator B; everything else of the doubling block is disjoint from everything the controlled-add block reads or carries.

• dbl : ModDoubleLayout m n

  The S6.3d-1 doubling sub-layout (its B is the shared accumulator).

• add : CModAddLayout m n

  The S6.3c controlled-add sub-layout (add.Aop = Y, add.ctrl = X_i, add.B the shared acc).

• hBshared : self.dbl.B = self.add.B

  Sharing: the two blocks act on the same accumulator register B.

• hAopAop (i j : ℕ) : self.dbl.Aop i ≠ self.add.Aop j
• hAopctrl (i : ℕ) : self.dbl.Aop i ≠ self.add.ctrl
• hAopCcadd (i j : ℕ) : self.dbl.Aop i ≠ self.add.Ccadd j
• hAopancC (i : ℕ) : self.dbl.Aop i ≠ self.add.ancC
• hAopA1 (i j : ℕ) : self.dbl.Aop i ≠ self.add.A1 j
• hAopC1 (i j : ℕ) : self.dbl.Aop i ≠ self.add.C1 j
• hAopA2 (i j : ℕ) : self.dbl.Aop i ≠ self.add.A2 j
• hAopC2 (i j : ℕ) : self.dbl.Aop i ≠ self.add.C2 j
• hAopanc (i : ℕ) : self.dbl.Aop i ≠ self.add.anc
• hCaddAop (i j : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.Aop j
• hCaddctrl (i : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.ctrl
• hCaddCcadd (i j : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.Ccadd j
• hCaddancC (i : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.ancC
• hCaddA1 (i j : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.A1 j
• hCaddC1 (i j : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.C1 j
• hCaddA2 (i j : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.A2 j
• hCaddC2 (i j : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.C2 j
• hCaddanc (i : ℕ) : self.dbl.addLayout.Cadd i ≠ self.add.anc
• hdA1Aop (i j : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.Aop j
• hdA1ctrl (i : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.ctrl
• hdA1Ccadd (i j : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.Ccadd j
• hdA1ancC (i : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.ancC
• hdA1A1 (i j : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.A1 j
• hdA1C1 (i j : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.C1 j
• hdA1A2 (i j : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.A2 j
• hdA1C2 (i j : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.C2 j
• hdA1anc (i : ℕ) : self.dbl.addLayout.A1 i ≠ self.add.anc
• hdC1Aop (i j : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.Aop j
• hdC1ctrl (i : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.ctrl
• hdC1Ccadd (i j : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.Ccadd j
• hdC1ancC (i : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.ancC
• hdC1A1 (i j : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.A1 j
• hdC1C1 (i j : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.C1 j
• hdC1A2 (i j : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.A2 j
• hdC1C2 (i j : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.C2 j
• hdC1anc (i : ℕ) : self.dbl.addLayout.C1 i ≠ self.add.anc
• hdA2Aop (i j : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.Aop j
• hdA2ctrl (i : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.ctrl
• hdA2Ccadd (i j : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.Ccadd j
• hdA2ancC (i : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.ancC
• hdA2A1 (i j : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.A1 j
• hdA2C1 (i j : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.C1 j
• hdA2A2 (i j : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.A2 j
• hdA2C2 (i j : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.C2 j
• hdA2anc (i : ℕ) : self.dbl.addLayout.A2 i ≠ self.add.anc
• hdC2Aop (i j : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.Aop j
• hdC2ctrl (i : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.ctrl
• hdC2Ccadd (i j : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.Ccadd j
• hdC2ancC (i : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.ancC
• hdC2A1 (i j : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.A1 j
• hdC2C1 (i j : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.C1 j
• hdC2A2 (i j : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.A2 j
• hdC2C2 (i j : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.C2 j
• hdC2anc (i : ℕ) : self.dbl.addLayout.C2 i ≠ self.add.anc
• hdancAop (j : ℕ) : self.dbl.addLayout.anc ≠ self.add.Aop j
• hdancctrl : self.dbl.addLayout.anc ≠ self.add.ctrl
• hdancCcadd (j : ℕ) : self.dbl.addLayout.anc ≠ self.add.Ccadd j
• hdancancC : self.dbl.addLayout.anc ≠ self.add.ancC
• hdancA1 (j : ℕ) : self.dbl.addLayout.anc ≠ self.add.A1 j
• hdancC1 (j : ℕ) : self.dbl.addLayout.anc ≠ self.add.C1 j
• hdancA2 (j : ℕ) : self.dbl.addLayout.anc ≠ self.add.A2 j
• hdancC2 (j : ℕ) : self.dbl.addLayout.anc ≠ self.add.C2 j
• hdancanc : self.dbl.addLayout.anc ≠ self.add.anc

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

The shared accumulator register (acc), the B of both sub-layouts.

Equations

• L.B = L.add.B

def Reversible.HornerStepLayout.ctrl {m n : ℕ} (L : HornerStepLayout m n) : Fin m

The control wire X_i for this Horner step (the controlled-add's ctrl).

Equations

• L.ctrl = L.add.ctrl

def Reversible.HornerStepLayout.Y {m n : ℕ} (L : HornerStepLayout m n) : ℕ → Fin m

The multiplicand register Y (the controlled-add's read-only operand).

Equations

• L.Y = L.add.Aop

def Reversible.hornerStep {m n : ℕ} (L : HornerStepLayout m n) : Circuit m

The Horner-step circuit. Double the accumulator (modDouble), then conditionally add the multiplicand Y controlled on the bit X_i (cModAdd).

Equations

• Reversible.hornerStep L = Reversible.modDouble L.dbl ++ Reversible.cModAdd L.add

modDouble preserves the controlled-add block's external wires

Each corollary specialises modDouble_preserves_external to one controlled-add family, feeding the eight cross-disjointness fields for that family. These re-establish cModAdd_correct's hypotheses at the post-doubling state.

theorem Reversible.modDouble_pres_addAop {m n : ℕ} {L : HornerStepLayout m n} (s : State m) (j : ℕ) : denote (modDouble L.dbl) s (L.add.Aop j) = s (L.add.Aop j)

theorem Reversible.modDouble_pres_addctrl {m n : ℕ} {L : HornerStepLayout m n} (s : State m) : denote (modDouble L.dbl) s L.add.ctrl = s L.add.ctrl

theorem Reversible.modDouble_pres_addCcadd {m n : ℕ} {L : HornerStepLayout m n} (s : State m) (j : ℕ) : denote (modDouble L.dbl) s (L.add.Ccadd j) = s (L.add.Ccadd j)

theorem Reversible.modDouble_pres_addancC {m n : ℕ} {L : HornerStepLayout m n} (s : State m) : denote (modDouble L.dbl) s L.add.ancC = s L.add.ancC

theorem Reversible.modDouble_pres_addA1 {m n : ℕ} {L : HornerStepLayout m n} (s : State m) (j : ℕ) : denote (modDouble L.dbl) s (L.add.A1 j) = s (L.add.A1 j)

theorem Reversible.modDouble_pres_addC1 {m n : ℕ} {L : HornerStepLayout m n} (s : State m) (j : ℕ) : denote (modDouble L.dbl) s (L.add.C1 j) = s (L.add.C1 j)

theorem Reversible.modDouble_pres_addA2 {m n : ℕ} {L : HornerStepLayout m n} (s : State m) (j : ℕ) : denote (modDouble L.dbl) s (L.add.A2 j) = s (L.add.A2 j)

theorem Reversible.modDouble_pres_addC2 {m n : ℕ} {L : HornerStepLayout m n} (s : State m) (j : ℕ) : denote (modDouble L.dbl) s (L.add.C2 j) = s (L.add.C2 j)

theorem Reversible.modDouble_pres_addanc {m n : ℕ} {L : HornerStepLayout m n} (s : State m) : denote (modDouble L.dbl) s L.add.anc = s L.add.anc

theorem Reversible.hornerStep_preserves_external {m n : ℕ} (L : HornerStepLayout m n) (s : State m) (w : Fin m) (hB : ∀ (j : ℕ), w ≠ L.dbl.B j) (hdAop : ∀ (j : ℕ), w ≠ L.dbl.Aop j) (hdCadd : ∀ (j : ℕ), w ≠ L.dbl.addLayout.Cadd j) (hdA1 : ∀ (j : ℕ), w ≠ L.dbl.addLayout.A1 j) (hdC1 : ∀ (j : ℕ), w ≠ L.dbl.addLayout.C1 j) (hdA2 : ∀ (j : ℕ), w ≠ L.dbl.addLayout.A2 j) (hdC2 : ∀ (j : ℕ), w ≠ L.dbl.addLayout.C2 j) (hdanc : w ≠ L.dbl.addLayout.anc) (hAop : ∀ k < n, w ≠ L.add.Aop k) (haddB : ∀ (j : ℕ), w ≠ L.add.B j) (hctrl : w ≠ L.add.ctrl) (hCcadd : ∀ k < n + 1, w ≠ L.add.Ccadd k) (hancC : w ≠ L.add.ancC) (hA1 : ∀ (j : ℕ), w ≠ L.add.A1 j) (hC1 : ∀ (j : ℕ), w ≠ L.add.C1 j) (hA2 : ∀ (j : ℕ), w ≠ L.add.A2 j) (hC2 : ∀ (j : ℕ), w ≠ L.add.C2 j) (hanc : w ≠ L.add.anc) : denote (hornerStep L) s w = s w

hornerStep frame. A wire w disjoint from every wire of BOTH blocks survives the whole Horner step (modDouble L.dbl ++ cModAdd L.add). Used by the 2-step demo to transport bank 2's clean presets / scratch / carries through bank 1. The modDouble families are {B, dbl.Aop, dbl.Cadd, dbl.A1, dbl.C1, dbl.A2, dbl.C2, dbl.anc}; the cModAdd families are {add.Aop, add.B, add.Ccadd, add.ctrl, add.ancC, add.A1, add.C1, add.A2, add.C2, add.anc}.

Value correctness of the Horner step

theorem Reversible.hornerStep_correct {m n : ℕ} (L : HornerStepLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.dbl.Aop i) = false) (hCadd_dbl : ∀ (j : ℕ), s (L.dbl.addLayout.Cadd j) = false) (hC1_dbl : ∀ (j : ℕ), s (L.dbl.addLayout.C1 j) = false) (hC2_dbl : ∀ (j : ℕ), s (L.dbl.addLayout.C2 j) = false) (hanc_dbl : s L.dbl.addLayout.anc = false) (hCcadd : ∀ (j : ℕ), s (L.add.Ccadd j) = false) (hancC : s L.add.ancC = false) (hC1 : ∀ (j : ℕ), s (L.add.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.add.C2 j) = false) (hanc : s L.add.anc = false) {N c Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hA1_dbl : regValRange L.dbl.addLayout.A1 s n = 2 ^ n - N) (hA2_dbl : regValRange L.dbl.addLayout.A2 s n = N) (hA1 : regValRange L.add.A1 s n = 2 ^ n - N) (hA2 : regValRange L.add.A2 s n = N) (hB : regValRange L.B s n = c) (hcN : c < N) (hY : regValRange L.Y s n = Yval) (hYN : Yval < N) : regValRange L.B (denote (hornerStep L) s) n = (2 * c + if s L.add.ctrl = true then Yval else 0) % N

The verified Horner loop body acc ← (2·acc + [X_i]·Y) mod N. For a HornerStepLayout with the accumulator B holding c < N, the multiplicand register Y = add.Aop holding Yval < N, 2N ≤ 2ⁿ, both sub-layouts' presets (A1 = 2ⁿ − N, A2 = N), all carries / ancillas clean, and the scratch operands of the doubling zeroed, hornerStep L leaves register B holding (2·c + (if X_i then Yval else 0)) mod N.

Proof. The doubling step (modDouble_correct / modDouble_in_range) writes (2c) mod N < N to B, preserves Y, X_i, and the controlled-add block's presets / clean carries / ancillas (modDouble_pres_add*). The controlled add (cModAdd_correct) then writes if X_i then (Yval + (2c mod N)) mod N else (2c mod N). In the set branch Nat.add_mod_mod absorbs the inner reduction: (Yval + (2c mod N)) mod N = (Yval + 2c) mod N = (2c + Yval) mod N; in the clear branch (2c) mod N = (2c + 0) mod N.

theorem Reversible.hornerStep_in_range {m n : ℕ} (L : HornerStepLayout m n) (s : State m) (hAop0 : ∀ i < n, s (L.dbl.Aop i) = false) (hCadd_dbl : ∀ (j : ℕ), s (L.dbl.addLayout.Cadd j) = false) (hC1_dbl : ∀ (j : ℕ), s (L.dbl.addLayout.C1 j) = false) (hC2_dbl : ∀ (j : ℕ), s (L.dbl.addLayout.C2 j) = false) (hanc_dbl : s L.dbl.addLayout.anc = false) (hCcadd : ∀ (j : ℕ), s (L.add.Ccadd j) = false) (hancC : s L.add.ancC = false) (hC1 : ∀ (j : ℕ), s (L.add.C1 j) = false) (hC2 : ∀ (j : ℕ), s (L.add.C2 j) = false) (hanc : s L.add.anc = false) {N c Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hA1_dbl : regValRange L.dbl.addLayout.A1 s n = 2 ^ n - N) (hA2_dbl : regValRange L.dbl.addLayout.A2 s n = N) (hA1 : regValRange L.add.A1 s n = 2 ^ n - N) (hA2 : regValRange L.add.A2 s n = N) (hB : regValRange L.B s n = c) (hcN : c < N) (hY : regValRange L.Y s n = Yval) (hYN : Yval < N) (hNpos : 0 < N) : regValRange L.B (denote (hornerStep L) s) n < N

The Horner-step output is a genuine residue in [0, N). Corollary of hornerStep_correct and Nat.mod_lt.

theorem Reversible.hornerStep_preserves_Y {m n : ℕ} (L : HornerStepLayout m n) (s : State m) (hCcadd : ∀ (j : ℕ), s (L.add.Ccadd j) = false) (hancC : s L.add.ancC = false) {Yval : ℕ} (hY : regValRange L.Y s n = Yval) : regValRange L.Y (denote (hornerStep L) s) n = Yval

The multiplicand Y is preserved. hornerStep L leaves Y = add.Aop at its initial value: the doubling block is disjoint from Y (modDouble_pres_addAop), and the controlled add reads Y read-only (cModAdd_preserves_operand). This is the load-bearing persistence: the loop reuses the SAME Y across all bit positions.

Derived cost

theorem Reversible.hornerStep_toffoli {m n : ℕ} (L : HornerStepLayout m n) : (circuitCost (hornerStep L)).toffoli = 30 * n

Derived Toffoli cost of the Horner step: 30n Toffolis, from the exhibited gate list. Doubling step 12n (modDouble_toffoli) + controlled add step 18n (cModularAdd_toffoli), composed through cost_comp_toffoli_count.

2-step composition: the verified n = 2 modular multiply

Two Horner-step banks L1 (high bit X₁) then L2 (low bit X₀) sharing the accumulator B and the multiplicand Y, with fresh per-bank scratch / carries / ancilla. Starting from acc = 0:

• step 1 leaves acc₁ = (X₁·Yval) mod N (hornerStep_correct L1, c = 0);
• step 2 leaves acc₂ = (2·acc₁ + X₀·Yval) mod N = ((2·X₁ + X₀)·Yval) mod N = (X·Yval) mod N (hornerStep_correct L2, c = acc₁), where X = 2·X₁ + X₀ is the 2-bit multiplier.

The load-bearing inter-bank obligation is that bank 1 leaves bank 2's clean presets / scratch / carries / ancilla and the low control bit X₀ UNTOUCHED — taken here as the hp_* hypotheses, each dischargeable from inter-bank disjointness via hornerStep_preserves_external (the fresh-wire model; see the mulCircuit2 #eval cross-check for a concrete instance that satisfies them). This exhibits that the loop body composes; the general-n Horner induction is S6.3d-2b, NOT proved here.

theorem Reversible.mulStep2_correct {m n : ℕ} (L1 L2 : HornerStepLayout m n) (s : State m) (hBshare : L2.B = L1.B) (hYshare : L2.Y = L1.Y) (h1Aop0 : ∀ i < n, s (L1.dbl.Aop i) = false) (h1Cadd_dbl : ∀ (j : ℕ), s (L1.dbl.addLayout.Cadd j) = false) (h1C1_dbl : ∀ (j : ℕ), s (L1.dbl.addLayout.C1 j) = false) (h1C2_dbl : ∀ (j : ℕ), s (L1.dbl.addLayout.C2 j) = false) (h1anc_dbl : s L1.dbl.addLayout.anc = false) (h1Ccadd : ∀ (j : ℕ), s (L1.add.Ccadd j) = false) (h1ancC : s L1.add.ancC = false) (h1C1 : ∀ (j : ℕ), s (L1.add.C1 j) = false) (h1C2 : ∀ (j : ℕ), s (L1.add.C2 j) = false) (h1anc : s L1.add.anc = false) (h2Aop0 : ∀ i < n, s (L2.dbl.Aop i) = false) (h2Cadd_dbl : ∀ (j : ℕ), s (L2.dbl.addLayout.Cadd j) = false) (h2C1_dbl : ∀ (j : ℕ), s (L2.dbl.addLayout.C1 j) = false) (h2C2_dbl : ∀ (j : ℕ), s (L2.dbl.addLayout.C2 j) = false) (h2anc_dbl : s L2.dbl.addLayout.anc = false) (h2Ccadd : ∀ (j : ℕ), s (L2.add.Ccadd j) = false) (h2ancC : s L2.add.ancC = false) (h2C1 : ∀ (j : ℕ), s (L2.add.C1 j) = false) (h2C2 : ∀ (j : ℕ), s (L2.add.C2 j) = false) (h2anc : s L2.add.anc = false) {N Yval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (hNpos : 0 < N) (h1A1_dbl : regValRange L1.dbl.addLayout.A1 s n = 2 ^ n - N) (h1A2_dbl : regValRange L1.dbl.addLayout.A2 s n = N) (h1A1 : regValRange L1.add.A1 s n = 2 ^ n - N) (h1A2 : regValRange L1.add.A2 s n = N) (h2A1_dbl : regValRange L2.dbl.addLayout.A1 s n = 2 ^ n - N) (h2A2_dbl : regValRange L2.dbl.addLayout.A2 s n = N) (h2A1 : regValRange L2.add.A1 s n = 2 ^ n - N) (h2A2 : regValRange L2.add.A2 s n = N) (hB0 : regValRange L1.B s n = 0) (hY : regValRange L1.Y s n = Yval) (hYN : Yval < N) (hp_2Aop : ∀ (i : ℕ), denote (hornerStep L1) s (L2.dbl.Aop i) = s (L2.dbl.Aop i)) (hp_2dCadd : ∀ (j : ℕ), denote (hornerStep L1) s (L2.dbl.addLayout.Cadd j) = s (L2.dbl.addLayout.Cadd j)) (hp_2dC1 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.dbl.addLayout.C1 j) = s (L2.dbl.addLayout.C1 j)) (hp_2dC2 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.dbl.addLayout.C2 j) = s (L2.dbl.addLayout.C2 j)) (hp_2danc : denote (hornerStep L1) s L2.dbl.addLayout.anc = s L2.dbl.addLayout.anc) (hp_2dA1 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.dbl.addLayout.A1 j) = s (L2.dbl.addLayout.A1 j)) (hp_2dA2 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.dbl.addLayout.A2 j) = s (L2.dbl.addLayout.A2 j)) (hp_2Ccadd : ∀ (j : ℕ), denote (hornerStep L1) s (L2.add.Ccadd j) = s (L2.add.Ccadd j)) (hp_2ancC : denote (hornerStep L1) s L2.add.ancC = s L2.add.ancC) (hp_2C1 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.add.C1 j) = s (L2.add.C1 j)) (hp_2C2 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.add.C2 j) = s (L2.add.C2 j)) (hp_2anc : denote (hornerStep L1) s L2.add.anc = s L2.add.anc) (hp_2A1 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.add.A1 j) = s (L2.add.A1 j)) (hp_2A2 : ∀ (j : ℕ), denote (hornerStep L1) s (L2.add.A2 j) = s (L2.add.A2 j)) (hp_2ctrl : denote (hornerStep L1) s L2.add.ctrl = s L2.add.ctrl) (h1Ccadd' : ∀ (j : ℕ), s (L1.add.Ccadd j) = false) (h1ancC' : s L1.add.ancC = false) : regValRange L2.B (denote (hornerStep L2) (denote (hornerStep L1) s)) n = ((2 * if s L1.add.ctrl = true then 1 else 0) + if s L2.add.ctrl = true then 1 else 0) * Yval % N

Concrete #eval cross-check: the verified n = 2 modular multiply on Fin 92

Two Horner-step banks laid out on Fin 92, n = 3 register width (forced by 2N ≤ 2ⁿ for N = 3), sharing the accumulator B → {0,1,2} and the multiplicand Y → {3,4,5}, with a 2-bit multiplier X on the dedicated control wires {6, 7} (wire 6 = bank-1 control X₁, the HIGH bit; wire 7 = bank-2 control X₀, the LOW bit). Every other wire family is FRESH per bank (the Θ(n²)-ancilla fresh-wire model): bank 1 on {8..49}, bank 2 on {50..91}.

The full circuit is modDouble dbl1 ++ cModAdd add1 ++ modDouble dbl2 ++ cModAdd add2 — exactly hornerStep (bank 1) followed by hornerStep (bank 2). Reading register B (low 3 bits) off the strict Array Bool evaluator (runArr, via the proven bridge regValRangeArr_eq) gives the value the chained hornerStep_correct / mulStep2_correct constrain, computed instantly. The three witnesses below realise X · Yval mod N for Yval = 2, N = 3: X = 3 ↦ 0, X = 2 ↦ 1, X = 1 ↦ 2.

def Reversible.dbl1 : ModDoubleLayout 92 3

Bank-1 doubling sub-layout (scratch {8,9,10}, carries/presets {11..29}).

Equations

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

def Reversible.add1 : CModAddLayout 92 3

Bank-1 controlled-add sub-layout (Aop = Y → {3,4,5}, ctrl = 6, carries/presets {30..49}).

Equations

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

def Reversible.dbl2 : ModDoubleLayout 92 3

Bank-2 doubling sub-layout (scratch {50,51,52}, carries/presets {53..71}).

Equations

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

def Reversible.add2 : CModAddLayout 92 3

Bank-2 controlled-add sub-layout (Aop = Y → {3,4,5}, ctrl = 7, carries/presets {72..91}).

Equations

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

def Reversible.mulCircuit2 : Circuit 92

The full 2-step modular-multiply circuit: bank-1 Horner step then bank-2 Horner step.

Equations

• Reversible.mulCircuit2 = Reversible.modDouble Reversible.dbl1 ++ Reversible.cModAdd Reversible.add1 ++ Reversible.modDouble Reversible.dbl2 ++ Reversible.cModAdd Reversible.add2

def Reversible.mulState2 (y0 y1 y2 x1 x0 : Bool) : State 92

Concrete input state on Fin 92: shared accumulator B = 0 (wires {0,1,2}), multiplicand Y = (y0,y1,y2) (wires {3,4,5}), 2-bit multiplier X = high bit x1 (wire 6) + low bit x0 (wire 7); both banks' presets A1 = 5 = 2³ − 3 and A2 = 3; all scratch / carries / ancillas false. Parameterised by the data bits.

Equations

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