The carry-clean (Cuccaro) ripple-carry adder — in-place, ancilla-restoring (ECDLP Phase 2, Stage 1)

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

The single highest-leverage reversible gadget the corpus lacked: an in-place, ancilla-restoring ripple-carry adder (Cuccaro, Draper, Kutin, Moulton 2004). Unlike rippleCirc / cRippleCirc (which thread an explicit Θ(n)-wire carry chain C and leave its top carry dirty), the Cuccaro adder stores the carries inside the preserved addend register during the computation and restores them, needing only one clean ancilla Z (the low carry, init false, returned false). This collapses the fresh-ancilla penalty that every prior ECDLP adder (ModularAdd, ModularAddCtrl, DoublingAssembly) carried as a named residue, and brings the per-multiply Toffoli cost from ~30n² toward ~2n².

The construction (standard Cuccaro, mod 2ⁿ, no output carry, one ancilla)

Two three-gate blocks on (c, b, a) (carry-in, sum register, addend register):

• maj c b a := [CX a b, CX a c, CCX c b a] — folds the carry-out into a: a ← majority(a, b, c), b ← b ⊕ a, c ← c ⊕ a (the (b,c) side effects are undone by uma).
• uma c b a := [CCX c b a, CX a c, CX c b] — writes the sum bit and restores: applied to a post-maj state it gives b ← a ⊕ b ⊕ c (the sum), a ← a (restored), c ← c (restored).

The circuit is a forward maj chain then a backward uma chain, with the carry threading through the addend register's wires. Equivalently — and this is the formulation proved here — it is the recursive maj c b₀ a₀ ++ (adder on the high bits with carry-in a₀) ++ uma c b₀ a₀, which makes the compute / uncompute correctness a clean induction on the bit count (cuccaroRec_correct).

What is proved here

• maj / uma with per-block all-inputs decide correctness (maj_correct / uma_correct on the concrete State 3) and the general Fin m lifts (maj_correct_general / uma_correct_general).
• cuccaroAdd_correct — general n, in-place sum: register A ends holding (A + B) mod 2ⁿ.
• cuccaroAdd_preserves_B — register B (the addend) is returned untouched.
• cuccaroAdd_ancilla_clean — the carry-clean property: the ancilla Z returns to false, so the adder is reusable in place with no fresh ancilla. This is what distinguishes it from rippleCirc / cRippleCirc.
• cuccaroAdd_toffoli — derived 2n Toffolis (n maj + n uma, each one CCX).

Scope (honest): this is the value-correct, in-place, ancilla-restoring adder modulo 2ⁿ. It does no modular (mod N) reduction — a carry-clean modular adder / multiply is Stage 2. The n=3 witness (cuccaroLayout3, 5 + 6 mod 8 = 3) is #eval/decide-cross-checked through the strict Array evaluator runArr.

Arithmetic helpers

theorem Reversible.regValRange_succ' {m : ℕ} (f : ℕ → Fin m) (s : State m) (k : ℕ) : regValRange f s (k + 1) = (s (f 0)).toNat + 2 * regValRange (fun (i : ℕ) => f (i + 1)) s k

Bottom-bit split of a place-value readout: peel index 0 off regValRange and factor 2 out of the remaining (shifted) register. The recursion's per-step accounting primitive.

theorem Reversible.nat_lowbit_carry (lowbit X P : ℕ) (hlb : lowbit < 2) (hP : 0 < P) : (lowbit + 2 * X) % (2 * P) = lowbit + 2 * (X % P)

The carry-propagation modular identity: a low bit plus twice a value, reduced mod 2P, is the low bit plus twice the value reduced mod P. The arithmetic core of the per-slice carry step.

The MAJ / UMA blocks

def Reversible.maj {m : ℕ} (c b a : Fin m) : Circuit m

The maj (majority) block on wires c b a (carry-in, sum register, addend register): [CX a b, CX a c, CCX c b a]. Folds the carry-out into a.

Equations

• Reversible.maj c b a = [Reversible.Gate.CX a b, Reversible.Gate.CX a c, Reversible.Gate.CCX c b a]

def Reversible.uma {m : ℕ} (c b a : Fin m) : Circuit m

The uma (un-majority-and-add) block on wires c b a: [CCX c b a, CX a c, CX c b]. Applied to a post-maj state, writes the sum into b and restores a, c.

Equations

• Reversible.uma c b a = [Reversible.Gate.CCX c b a, Reversible.Gate.CX a c, Reversible.Gate.CX c b]

theorem Reversible.maj_correct (s : State 3) : denote (maj 0 1 2) s 2 = majority (s 2) (s 1) (s 0) ∧ denote (maj 0 1 2) s 1 = (s 1 ^^ s 2) ∧ denote (maj 0 1 2) s 0 = (s 0 ^^ s 2)

maj correctness — all-inputs decide. On State 3 (wires 0,1,2 = c,b,a): a ← majority, b ← b ⊕ a, c ← c ⊕ a.

theorem Reversible.uma_correct (s : State 3) : denote (uma 0 1 2) s 2 = (s 2 ^^ s 0 && s 1) ∧ denote (uma 0 1 2) s 0 = (s 0 ^^ (s 2 ^^ s 0 && s 1)) ∧ denote (uma 0 1 2) s 1 = (s 1 ^^ (s 0 ^^ (s 2 ^^ s 0 && s 1)))

uma correctness — all-inputs decide. On State 3 (wires 0,1,2 = c,b,a), the raw gate action: a ← a ⊕ (c ∧ b), then c ← c ⊕ a', then b ← b ⊕ c'.

theorem Reversible.maj_apply_of_ne {m : ℕ} {c b a w : Fin m} (hc : w ≠ c) (hb : w ≠ b) (ha : w ≠ a) (s : State m) : denote (maj c b a) s w = s w

Frame lemma for maj. A wire distinct from c, b, a is untouched.

theorem Reversible.uma_apply_of_ne {m : ℕ} {c b a w : Fin m} (hc : w ≠ c) (hb : w ≠ b) (ha : w ≠ a) (s : State m) : denote (uma c b a) s w = s w

Frame lemma for uma. A wire distinct from c, b, a is untouched.

theorem Reversible.maj_correct_general {m : ℕ} {c b a : Fin m} (hcb : c ≠ b) (hca : c ≠ a) (hba : b ≠ a) (s : State m) : denote (maj c b a) s a = majority (s a) (s b) (s c) ∧ denote (maj c b a) s b = (s b ^^ s a) ∧ denote (maj c b a) s c = (s c ^^ s a)

maj correctness, general Fin m wires. For pairwise-distinct c, b, a: a ← majority(a,b,c), b ← b ⊕ a, c ← c ⊕ a.

theorem Reversible.uma_correct_general {m : ℕ} {c b a : Fin m} (hcb : c ≠ b) (hca : c ≠ a) (hba : b ≠ a) (s : State m) : denote (uma c b a) s a = (s a ^^ s c && s b) ∧ denote (uma c b a) s c = (s c ^^ (s a ^^ s c && s b)) ∧ denote (uma c b a) s b = (s b ^^ (s c ^^ (s a ^^ s c && s b)))

uma correctness, general Fin m wires. For pairwise-distinct c, b, a, the raw gate action (in terms of the input bits). Composed with the post-maj relation it yields the sum / restoration.

Derived block costs

@[simp]

theorem Reversible.maj_toffoli {m : ℕ} (c b a : Fin m) : (circuitCost (maj c b a)).toffoli = 1

@[simp]

theorem Reversible.uma_toffoli {m : ℕ} (c b a : Fin m) : (circuitCost (uma c b a)).toffoli = 1

The Cuccaro layout and recursive circuit

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

A Cuccaro-adder layout on m wires for n-bit registers: the sum register A (overwritten with the sum), the addend register B (preserved; also holds the carry chain internally during the run), and a single clean ancilla Z (the low carry, init/returned false). The two register images are pairwise disjoint, disjoint from Z, and each injective on its used index range.

• A : ℕ → Fin m

  Wires of the sum register A (overwritten with (A + B) mod 2ⁿ).

• B : ℕ → Fin m

  Wires of the addend register B (preserved; carries threaded through and restored).

• Z : Fin m

  The single clean ancilla (low carry; init/returned false).

• hAB (i j : ℕ) : self.A i ≠ self.B j
• hAZ (i : ℕ) : self.A i ≠ self.Z
• hBZ (i : ℕ) : self.B i ≠ self.Z
• hAinj (i j : ℕ) : i < n → j < n → self.A i = self.A j → i = j
• hBinj (i j : ℕ) : i < n → j < n → self.B i = self.B j → i = j

def Reversible.cuccaroRec {m n : ℕ} (L : CuccaroLayout m n) : Fin m → ℕ → ℕ → Circuit m

The recursive Cuccaro adder on the len bits start .. start + len - 1 with carry-in wire carry: maj carry A_start B_start ++ (recurse on the high bits, carry-in B_start) ++ uma carry A_start B_start. The carry-out of the low slice (majority, stored in B start) is the carry-in of the recursive remainder; the outer uma writes the low sum bit and restores.

Equations

• Reversible.cuccaroRec L x✝¹ x✝ 0 = []
• Reversible.cuccaroRec L x✝¹ x✝ len.succ = Reversible.maj x✝¹ (L.A x✝) (L.B x✝) ++ Reversible.cuccaroRec L (L.B x✝) (x✝ + 1) len ++ Reversible.uma x✝¹ (L.A x✝) (L.B x✝)

def Reversible.cuccaroAdd {m n : ℕ} (L : CuccaroLayout m n) : Circuit m

The full Cuccaro adder: all n bits, carry-in the ancilla Z.

Equations

• Reversible.cuccaroAdd L = Reversible.cuccaroRec L L.Z 0 n

theorem Reversible.denote_cuccaroRec_succ {m n : ℕ} (L : CuccaroLayout m n) (carry : Fin m) (start len : ℕ) (s : State m) : denote (cuccaroRec L carry start (len + 1)) s = denote (uma carry (L.A start) (L.B start)) (denote (cuccaroRec L (L.B start) (start + 1) len) (denote (maj carry (L.A start) (L.B start)) s))

Recursive correctness invariant

theorem Reversible.cuccaroRec_correct {m n : ℕ} (L : CuccaroLayout m n) (len start : ℕ) (carry : Fin m) (s : State m) : start + len ≤ n → (∀ i < len, carry ≠ L.A (start + i)) → (∀ i < len, carry ≠ L.B (start + i)) → regValRange (fun (i : ℕ) => L.A (start + i)) (denote (cuccaroRec L carry start len) s) len = ((s carry).toNat + regValRange (fun (i : ℕ) => L.A (start + i)) s len + regValRange (fun (i : ℕ) => L.B (start + i)) s len) % 2 ^ len ∧ (∀ i < len, denote (cuccaroRec L carry start len) s (L.B (start + i)) = s (L.B (start + i))) ∧ denote (cuccaroRec L carry start len) s carry = s carry ∧ ∀ (w : Fin m), w ≠ carry → (∀ i < len, w ≠ L.A (start + i)) → (∀ i < len, w ≠ L.B (start + i)) → denote (cuccaroRec L carry start len) s w = s w

The Cuccaro carry-chain invariant. For the len-bit recursive adder with carry-in carry (disjoint from the register range): register A ends holding (carry + A + B) mod 2^len (P1); register B is restored (P2); the carry-in wire is restored (P3); any external wire is preserved (P4). By induction on len, peeling one maj/uma pair per step.

Headline theorems

theorem Reversible.cuccaroAdd_correct {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (hZ : s L.Z = false) : regValRange L.A (denote (cuccaroAdd L) s) n = (regValRange L.A s n + regValRange L.B s n) % 2 ^ n

Cuccaro adder correctness (in-place sum). For a disjoint-wire layout with the ancilla Z initialised false, the Cuccaro adder leaves register A holding (A + B) mod 2ⁿ — in place, with no carry chain, one ancilla.

theorem Reversible.cuccaroAdd_preserves_B {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (hZ : s L.Z = false) (k : ℕ) : k < n → denote (cuccaroAdd L) s (L.B k) = s (L.B k)

Register B is preserved. The addend register is returned untouched (carries threaded through it during the run are restored). The ancilla hypothesis hZ is taken for API uniformity with the other headlines; B-preservation does not actually consume it.

theorem Reversible.cuccaroAdd_ancilla_clean {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (hZ : s L.Z = false) : denote (cuccaroAdd L) s L.Z = false

The carry-clean property. The ancilla Z returns to false: the Cuccaro adder borrows the low-carry wire clean and returns it clean, so it is reusable in place with no fresh ancilla. This is what distinguishes it from rippleCirc / cRippleCirc (which leave the top carry dirty).

theorem Reversible.cuccaroAdd_preserves_Z {m n : ℕ} (L : CuccaroLayout m n) (s : State m) : denote (cuccaroAdd L) s L.Z = s L.Z

The carry-in wire is restored unconditionally. The ancilla Z is returned to its input value for every input state (not only false): clause P3 of cuccaroRec_correct carries no hypothesis on s Z. This is the lemma the clean subtractor (cuccaroSub) needs to pin the ancilla of an inverse-image state. cuccaroAdd_ancilla_clean is the s Z = false specialisation.

theorem Reversible.cuccaroAdd_preserves_external {m n : ℕ} (L : CuccaroLayout m n) (s : State m) (w : Fin m) (hwZ : w ≠ L.Z) (hwA : ∀ i < n, w ≠ L.A i) (hwB : ∀ i < n, w ≠ L.B i) : denote (cuccaroAdd L) s w = s w

External wires are preserved unconditionally. A wire distinct from the ancilla Z and from every used wire of registers A, B (indices < n) is left unchanged, for every input state (clause P4 of cuccaroRec_correct carries no s Z hypothesis). The frame lemma that lets a clean modular adder thread several Cuccaro passes past its constant / work / flag registers.

Derived cost: 2n Toffolis

theorem Reversible.cuccaroRec_toffoli {m n : ℕ} (L : CuccaroLayout m n) (carry : Fin m) (start len : ℕ) : (circuitCost (cuccaroRec L carry start len)).toffoli = 2 * len

theorem Reversible.cuccaroAdd_toffoli {m n : ℕ} (L : CuccaroLayout m n) : (circuitCost (cuccaroAdd L)).toffoli = 2 * n

Derived Toffoli cost: 2n. n maj blocks + n uma blocks, each exactly one CCX; the CXs are CNOTs (zero Toffoli). The honest in-place carry-clean overhead — half the ~30n²-per-multiply fresh-ancilla cost the corpus adders carried.

Non-vacuity witness + #eval / decide cross-check

A concrete 3-bit layout on Fin 7 (A → {0,1,2}, B → {3,4,5}, Z → 6). The headline applies, and the strict Array evaluator runArr (with the proven bridge regValRangeArr_eq back to denote) witnesses 5 + 6 mod 8 = 3, the ancilla returning false, and B intact.

def Reversible.cuccaroLayout3 : CuccaroLayout 7 3

A concrete 3-bit Cuccaro layout on Fin 7.

Equations

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

def Reversible.cuccaroWitness3 : State 7

Witness state: A = 5 (wires 0,1,2 = 1,0,1), B = 6 (wires 3,4,5 = 0,1,1), Z = 6 = false.

Equations

• Reversible.cuccaroWitness3 = ![true, false, true, false, true, true, false]