Reversible quantum×quantum multiplication — controlled shift-and-add (ECDLP Phase 2, Stage S2.3)

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

The Tranche-3 multiplier (ModMul.lean) is quantum×classical (a·Y, a a classical constant fixing which shifts appear). A genuine quantum×quantum multiply X·Y (both factors registers — what squaring and elliptic-curve field multiplication need) controls each partial-product add on a register bit X_i. This module folds the controlled ripple adder (CtrlAdd.lean, cRippleCirc_correct) over the bits of X, with the per-bit control wire bound to X_i and a shared ancilla re-cleaned between steps (cRippleCirc_anc_restored).

What is proved here

• cAccStep — the controlled accumulation step: one controlled full-window ripple add of the multiplicand Y (value Yv) into the accumulator window Acc[i, W), controlled on ctrl, increases the accumulator by if ctrl then 2^i · Yv else 0. The controlled analogue of ModMul.accStep, routed through cRippleCirc_correct (so the ctrl-clear case adds nothing) — the heart of the quantum×quantum multiply.

theorem Reversible.cAccStep {m w : ℕ} (L : CRippleLayout m w) (Acc : ℕ → Fin m) (s : State m) (i W : ℕ) (hw : w = W - i) (hiW : i ≤ W) (hB : ∀ (k : ℕ), L.B k = Acc (i + k)) (hAccinj : ∀ (j k : ℕ), j < W → k < W → Acc j = Acc k → j = k) (hAccA : ∀ j < i, ∀ (k : ℕ), Acc j ≠ L.A k) (hAccC : ∀ j < i, ∀ (k : ℕ), Acc j ≠ L.C k) (hAccctrl : ∀ j < i, Acc j ≠ L.ctrl) (hAccanc : ∀ j < i, Acc j ≠ L.anc) (hcarry : ∀ (j : ℕ), s (L.C j) = false) (hanc0 : s L.anc = false) (Yv : ℕ) (hYv : regValRange L.A s w = Yv) (hno : Yv + regValRange (fun (k : ℕ) => Acc (i + k)) s w < 2 ^ w) : regValRange Acc (denote (cRippleCirc L) s) W = regValRange Acc s W + if s L.ctrl = true then 2 ^ i * Yv else 0

Controlled accumulation step. One controlled full-remaining-width ripple add of the multiplicand (value Yv, read by L.A) into the accumulator window Acc[i, W), controlled on L.ctrl: it increases the full accumulator value by 2^i · Yv when the control is set and leaves it unchanged when clear — + (if ctrl then 2^i · Yv else 0). The carry propagates through the whole upper accumulator (width w = W - i); the low i bits are preserved (they are external to the slice); the add must not overflow the window. The controlled analogue of ModMul.accStep.

The quantum×quantum multiplier and its correctness

A CMulLayout lays out, on Fin M: the accumulator Acc (W wires), the control register X (the first factor, whose bit sh controls partial product sh), the multiplicand Y (W wires, high bits held zero), a per-shift carry chain Carry, and the shared ancilla anc. The multiplier is the concatenation, over the shift list, of one controlled full-window ripple add of Y into Acc[sh, W) controlled on X sh. Folding cAccStep gives Acc ← Acc + (∑ sh, [X_sh] · 2^sh) · Y = Acc + X·Y.

structure Reversible.CMulLayout (M n W : ℕ) : Type

A quantum×quantum multiplier layout on Fin M: accumulator Acc, control register X, multiplicand Y (high bits zero), per-shift carry chain Carry, shared ancilla anc. The fields are pure wire geometry (disjointness + injectivity).

• Acc : ℕ → Fin M

  Accumulator wires (indices [0, W)).

• X : ℕ → Fin M

  Control-register wires (the first factor X; bit sh controls partial product sh).

• Y : ℕ → Fin M

  Multiplicand wires (W-wire register; values in [0, n), high bits held zero).

• Carry : ℕ → ℕ → Fin M

  Carry chain for the partial-product add at shift sh.

• anc : Fin M

  The shared clean ancilla.

• hYAcc (i j : ℕ) : self.Y i ≠ self.Acc j
• hYCarry (i sh j : ℕ) : self.Y i ≠ self.Carry sh j
• hAccCarry (i sh j : ℕ) : self.Acc i ≠ self.Carry sh j
• hCarryCross (sh sh' i j : ℕ) : sh ≤ W → sh' ≤ W → sh ≠ sh' → self.Carry sh i ≠ self.Carry sh' j
• hAccInj (i j : ℕ) : i < W → j < W → self.Acc i = self.Acc j → i = j
• hYInj (i j : ℕ) : i < W → j < W → self.Y i = self.Y j → i = j
• hCarryInj (sh i j : ℕ) : i ≤ W → j ≤ W → self.Carry sh i = self.Carry sh j → i = j
• hXAcc (i j : ℕ) : self.X i ≠ self.Acc j
• hXY (i j : ℕ) : self.X i ≠ self.Y j
• hXCarry (i sh j : ℕ) : self.X i ≠ self.Carry sh j
• hXanc (i : ℕ) : self.X i ≠ self.anc
• hXInj (i j : ℕ) : i < W → j < W → self.X i = self.X j → i = j
• hAncAcc (j : ℕ) : self.anc ≠ self.Acc j
• hAncY (j : ℕ) : self.anc ≠ self.Y j
• hAncCarry (sh j : ℕ) : self.anc ≠ self.Carry sh j

def Reversible.cStepLayout {m n W : ℕ} (L : CMulLayout m n W) (sh : ℕ) : CRippleLayout m (W - sh)

The controlled-ripple layout for the partial product at shift sh: controlled on X sh, add the multiplicand Y into the accumulator window Acc[sh, W) (width W - sh), carry chain Carry sh, shared ancilla anc.

Equations

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

def Reversible.cMulCircuit {m n W : ℕ} (L : CMulLayout m n W) (shifts : List ℕ) : Circuit m

The quantum×quantum multiplier circuit: one controlled partial-product ripple add per shift.

Equations

• Reversible.cMulCircuit L shifts = Reversible.multiplier (List.map (fun (sh : ℕ) => Reversible.cRippleCirc (Reversible.cStepLayout L sh)) shifts)

theorem Reversible.cStepLayout_preserves_Y {m n W : ℕ} (L : CMulLayout m n W) (sh : ℕ) (s : State m) (hcarry : ∀ (k : ℕ), s (L.Carry sh k) = false) (hanc : s L.anc = false) (j : ℕ) (hj : j < W) : denote (cRippleCirc (cStepLayout L sh)) s (L.Y j) = s (L.Y j)

A partial-product step preserves the multiplicand Y (addend wires are read-only).

theorem Reversible.cStepLayout_preserves_carry {m n W : ℕ} (L : CMulLayout m n W) (sh sh' : ℕ) (hshW : sh ≤ W) (hsh'W : sh' ≤ W) (hne : sh' ≠ sh) (s : State m) (k : ℕ) : denote (cRippleCirc (cStepLayout L sh)) s (L.Carry sh' k) = s (L.Carry sh' k)

A partial-product step at shift sh preserves the carry chain of any other shift sh' ≠ sh.

theorem Reversible.cStepLayout_preserves_X {m n W : ℕ} (L : CMulLayout m n W) (sh : ℕ) (s : State m) (hcarry : ∀ (k : ℕ), s (L.Carry sh k) = false) (hanc : s L.anc = false) (j : ℕ) (hjW : j < W) (hshW : sh < W) : denote (cRippleCirc (cStepLayout L sh)) s (L.X j) = s (L.X j)

A partial-product step preserves every control bit X j (the control register is read-only).

theorem Reversible.cMulCircuit_correct {m n W : ℕ} (L : CMulLayout m n W) (shifts : List ℕ) : shifts.Nodup → (∀ sh ∈ shifts, sh + n ≤ W) → (∀ sh ∈ shifts, sh < W) → ∀ (s : State m) (Yv : ℕ), (∀ sh ∈ shifts, ∀ (k : ℕ), s (L.Carry sh k) = false) → s L.anc = false → (∀ (j : ℕ), n ≤ j → j < W → s (L.Y j) = false) → regValRange L.Y s n = Yv → regValRange L.Acc s W + (List.map (fun (sh : ℕ) => 2 ^ sh * Yv) shifts).sum < 2 ^ W → regValRange L.Acc (denote (cMulCircuit L shifts) s) W = regValRange L.Acc s W + (List.map (fun (sh : ℕ) => if s (L.X sh) = true then 2 ^ sh * Yv else 0) shifts).sum

Quantum×quantum multiplier correctness (the S2.3 headline). The controlled shift-and-add multiplier over shifts leaves the accumulator holding Acc + (∑ sh ∈ shifts, [X_sh] · 2^sh) · Y, where [X_sh] is 0/1 for the control bit — provided the carries and ancilla start false, Y's high bits are zero, and no step overflows. With shifts = [0, …, n-1] and Acc initialised 0 this is Acc = X · Y (both factors quantum).

theorem Reversible.ctrlSum_eq {m : ℕ} (s : State m) (X : ℕ → Fin m) (Yv n : ℕ) : (List.map (fun (sh : ℕ) => if s (X sh) = true then 2 ^ sh * Yv else 0) (List.range n)).sum = regValRange X s n * Yv

The sum of controlled partial products over [0, n) is exactly X · Y: each set control bit X_sh contributes 2^sh · Yv, so the total is (∑ 2^sh·[X_sh]) · Yv = regValRange X · Yv.

theorem Reversible.cMulCircuit_eq_mul {m n W : ℕ} (L : CMulLayout m n W) (s : State m) (Yv : ℕ) (hshn : ∀ sh ∈ List.range n, sh + n ≤ W) (hshW : ∀ sh ∈ List.range n, sh < W) (hcarry : ∀ sh ∈ List.range n, ∀ (k : ℕ), s (L.Carry sh k) = false) (hanc : s L.anc = false) (hYhigh : ∀ (j : ℕ), n ≤ j → j < W → s (L.Y j) = false) (hYv : regValRange L.Y s n = Yv) (hbound : regValRange L.Acc s W + (List.map (fun (sh : ℕ) => 2 ^ sh * Yv) (List.range n)).sum < 2 ^ W) : regValRange L.Acc (denote (cMulCircuit L (List.range n)) s) W = regValRange L.Acc s W + regValRange L.X s n * Yv

Quantum×quantum multiply, X · Y form. Over the full shift list [0, n), the controlled shift-and-add multiplier leaves the accumulator holding Acc + (regValRange X) · Y. With Acc initialised 0 this is Acc = X · Y (both factors quantum); with X preset to a copy of Y it is Acc = Y² (squaring). The ctrlSum_eq rewrite collapses the per-bit controlled sum to the product.

The overflow hypothesis hbound is the worst-case-over-X condition Acc + (∑ 2^sh)·Yv < 2^W = Acc + (2ⁿ−1)·Yv < 2^W, with no if: because X is a quantum register, a sound circuit must not overflow on any branch of a superposition, so the design-time bound must hold for the maximal X. (For squaring, the copy gadget X := Y is a precondition supplied by the caller as regValRange X s n = regValRange Y s n; the copy CNOT fan-out is not built here.)

Non-vacuity witness

A concrete 1-bit quantum×quantum multiplier layout on Fin 8: accumulator 0, control register X on 1, multiplicand Y on 2, carry banks {3,4} (shift 0) / {5,6} (shift 1), shared ancilla 7 — exhibiting that CMulLayout is inhabited and cMulCircuit_eq_mul applies.

def Reversible.cMulLayout1 : CMulLayout 8 1 1

A concrete 1-bit (n = W = 1) quantum×quantum multiplier layout on Fin 8.

Equations

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