The minimal 1-Toffoli-per-carry (Gidney) reversible adder (Tier-X / Build #35)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Pure Boolean-DSL value-correctness; the amplitude / measurement re-cost is Empirical/QM/MeasurementGidneyAdder.lean.

Why this file exists

#30 (AndAdd.lean) computes each carry into a fresh ancilla with a 3-Toffoli preserving-majority cell (andCarryCell), so its adder costs 6n Toffoli. The Cuccaro adder (CuccaroAdd.lean) restores the carries in place with 2n Toffoli but exposes no fresh-AND attachment point (its uma is a unitary in-place restore), so the measurement-uncomputation gadget (#31) cannot drop its Toffolis.

This file supplies the competitive adder: the Gidney carry cell folds the carry into a fresh ancilla with a single Toffoli (the addend bits are XOR-shifted by the carry-in and restored on the reverse pass), and the reverse pass's per-carry Toffoli is a genuine andUncompute-shaped block — the attachment point the measurement gadget eliminates. The unitary cost is 2n; the measurement re-cost (in MeasurementGidneyAdder.lean) drops the reverse pass to 0, giving n.

The carry cell (Gidney, one Toffoli)

c_{i+1} = MAJ(a_i, b_i, c_i) = c_i ⊕ ((a_i ⊕ c_i) ∧ (b_i ⊕ c_i)). The cell on (a, b, cin, cout) (cout a fresh runway ancilla, init false) is majCell a b cin cout := [CX cin a, CX cin b, CCX a b cout, CX cin cout]:

• CX cin a / CX cin b shift a ← a ⊕ cin, b ← b ⊕ cin;
• the single CCX a b cout writes cout ← (a ⊕ cin) ∧ (b ⊕ cin) (the fresh-AND temporary);
• CX cin cout adds the cin term, giving cout = MAJ(a, b, cin).

majCell_toffoli : … = 1 is the cost win. majCell_correct proves the Boolean semantics.

The adder + correctness (the anti-hollow requirement)

gidneyAdd L := gidneyForward L ++ andSumPass L.toAnd ++ inverse (gidneyForward L) on a GidneyLayout (addends A, B, sum register S, fresh carry chain G). The forward pass computes every carry into G (XOR-shifting A, B); the sum pass writes S i ← A i ⊕ B i ⊕ G i (= a_i ⊕ b_i ⊕ c_i, since the two c_i shifts cancel one); the reverse pass uncomputes the carries and restores A, B, G.

• gidneyAdd_correct : regValRange L.S (denote (gidneyAdd L) s) n = (A + B) % 2 ^ n — general n.
• gidneyAdd_ancilla_clean / gidneyAdd_preserves_A / _preserves_B — the reverse pass restores the carry chain to false and the addends to their inputs.
• gidneyAdd_toffoli : … = 2 * n — n forward + n reverse, sum pass CNOT-only.

The sum-pass machinery, the carry arithmetic (carryOf, adder_sum_identity), and the circuit locality lemmas (denote_apply_of_forall_not_mem_target, denote_agree_on) are reused from #30 via the projection GidneyLayout.toAnd.

Honest scope

Value-correct + ancilla-clean over regVal, Boolean DSL only, general n. The Toffoli win over #30 (6n) is at the unitary level; the win over Cuccaro (2n) requires the measurement re-cost (MeasurementGidneyAdder.lean), which inherits #31's cell-granularity amplitude bridge. No amplitudes, no measurement, no ECDSA resource claim here.

Space tradeoff (honest). The Toffoli parity (and the measurement-level advantage over Cuccaro) is bought with O(n) extra space: a separate sum register S (n wires) and an (n+1)-wire fresh carry runway G, against Cuccaro's single in-place ancilla. The win is on the Toffoli axis only. The count is also Toffoli-only (the dominant fault-tolerant cost); Cliffords / measurements are not counted.

The Gidney carry cell (one Toffoli)

def Reversible.majCell {m : ℕ} (a b cin cout : Fin m) : Circuit m

The Gidney carry cell on (a, b, cin, cout) with cout a fresh runway ancilla: [CX cin a, CX cin b, CCX a b cout, CX cin cout]. The single CCX folds the fresh-AND (a ⊕ cin) ∧ (b ⊕ cin) into cout; the surrounding CNOTs shift a, b by cin and add the cin term, giving cout = MAJ(a, b, cin). Deviates from Cuccaro's 3-wire in-place maj by using a fresh cout (the attachment point the measurement gadget needs). One Toffoli per carry.

Equations

• Reversible.majCell a b cin cout = [Reversible.Gate.CX cin a, Reversible.Gate.CX cin b, Reversible.Gate.CCX a b cout, Reversible.Gate.CX cin cout]

theorem Reversible.majCell_toffoli {m : ℕ} (a b cin cout : Fin m) : (circuitCost (majCell a b cin cout)).toffoli = 1

Cell Toffoli cost = 1 (the single CCX; the other three gates are CNOTs). The key cost win over #30's 3-Toffoli andCarryCell.

theorem Reversible.majCell_correct {m : ℕ} {a b cin cout : Fin m} (hab : a ≠ b) (hca : cin ≠ a) (hcb : cin ≠ b) (hcc : cin ≠ cout) (hoa : cout ≠ a) (hob : cout ≠ b) {s : State m} (h0 : s cout = false) : denote (majCell a b cin cout) s cout = majority (s a) (s b) (s cin) ∧ denote (majCell a b cin cout) s a = (s a ^^ s cin) ∧ denote (majCell a b cin cout) s b = (s b ^^ s cin) ∧ denote (majCell a b cin cout) s cin = s cin

Cell correctness. For pairwise-distinct wires and a fresh cout = false, the cell writes cout = MAJ(a, b, cin), shifts a ← a ⊕ cin and b ← b ⊕ cin, and preserves cin. The fresh-AND temporary (a ⊕ cin) ∧ (b ⊕ cin) is computed by the single Toffoli and completed to the majority by the final CNOT.

The Gidney adder layout (addend registers injective; A, B are modified and restored)

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

The Gidney-adder wire geometry on m wires for n-bit registers: addends A, B (XOR-shifted during the forward pass, restored by the reverse pass), a separate sum register S, and a fresh per-carry ancilla chain G (G 0 the input carry, G (i+1) the carry out of bit i, all init false). Unlike AndAddLayout, A and B carry their own injectivity (hAinj / hBinj) because the forward pass writes them. The four images are pairwise disjoint.

• A : ℕ → Fin m

  First addend (shifted then restored).

• B : ℕ → Fin m

  Second addend (shifted then restored).

• S : ℕ → Fin m

  Sum output register ((A + B) mod 2 ^ n).

• G : ℕ → Fin m

  Fresh per-carry ancilla chain (G i = carry into bit i; init/returned false).

• hAB (i j : ℕ) : self.A i ≠ self.B j
• hAS (i j : ℕ) : self.A i ≠ self.S j
• hAG (i j : ℕ) : self.A i ≠ self.G j
• hBS (i j : ℕ) : self.B i ≠ self.S j
• hBG (i j : ℕ) : self.B i ≠ self.G j
• hSG (i j : ℕ) : self.S i ≠ self.G j
• 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
• hSinj (i j : ℕ) : i < n → j < n → self.S i = self.S j → i = j
• hGinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.G i = self.G j → i = j

def Reversible.GidneyLayout.toAnd {m n : ℕ} (L : GidneyLayout m n) : AndAddLayout m n

The #30 AndAddLayout underlying a GidneyLayout (drops the addend injectivity). Lets the Gidney adder reuse #30's sum-pass machinery and carry arithmetic verbatim.

Equations

• L.toAnd = { A := L.A, B := L.B, S := L.S, G := L.G, hAB := ⋯, hAS := ⋯, hAG := ⋯, hBS := ⋯, hBG := ⋯, hSG := ⋯, hSinj := ⋯, hGinj := ⋯ }

Forward carry pass

def Reversible.gidneyForwardSlice {m n : ℕ} (L : GidneyLayout m n) (i : ℕ) : Circuit m

The carry compute for bit i: the Gidney cell on (A i, B i, G i, G (i+1)).

Equations

• Reversible.gidneyForwardSlice L i = Reversible.majCell (L.A i) (L.B i) (L.G i) (L.G (i + 1))

def Reversible.gidneyForwardPrefix {m n : ℕ} (L : GidneyLayout m n) (k : ℕ) : Circuit m

The forward carry pass over the first k bits.

Equations

• Reversible.gidneyForwardPrefix L k = List.flatMap (Reversible.gidneyForwardSlice L) (List.range k)

def Reversible.gidneyForward {m n : ℕ} (L : GidneyLayout m n) : Circuit m

The full forward carry pass (all n bits).

Equations

• Reversible.gidneyForward L = Reversible.gidneyForwardPrefix L n

def Reversible.gidneyAdd {m n : ℕ} (L : GidneyLayout m n) : Circuit m

The Gidney adder. Compute all carries into G (gidneyForward, n Toffoli, XOR-shifting A, B), write the sums into S (andSumPass, CNOT-only, reused from #30), then uncompute every carry and restore A, B, G via the reverse pass inverse (gidneyForward L). The reverse pass's per-carry Toffoli is an andUncompute-shaped block — the measurement-gadget attachment point.

Equations

• Reversible.gidneyAdd L = Reversible.gidneyForward L ++ Reversible.andSumPass L.toAnd ++ Reversible.inverse (Reversible.gidneyForward L)

Membership / wire / target characterisation

theorem Reversible.mem_gidneyForwardPrefix {m n : ℕ} {L : GidneyLayout m n} {k : ℕ} {g : Gate m} (hg : g ∈ gidneyForwardPrefix L k) : ∃ j < k, g ∈ gidneyForwardSlice L j

theorem Reversible.gidneyForwardSlice_wires {m n : ℕ} {L : GidneyLayout m n} {j : ℕ} {g : Gate m} (hg : g ∈ gidneyForwardSlice L j) {w : Fin m} (hw : w ∈ gateWires g) : w = L.A j ∨ w = L.B j ∨ w = L.G j ∨ w = L.G (j + 1)

theorem Reversible.gidneyForwardSlice_target {m n : ℕ} {L : GidneyLayout m n} {j : ℕ} {g : Gate m} (hg : g ∈ gidneyForwardSlice L j) {w : Fin m} (hw : w ∈ gateTarget g) : w = L.A j ∨ w = L.B j ∨ w = L.G (j + 1)

Preservation lemmas (target-frame)

theorem Reversible.gidneyForwardPrefix_preserves_S {m n : ℕ} (L : GidneyLayout m n) (s : State m) (k i : ℕ) : denote (gidneyForwardPrefix L k) s (L.S i) = s (L.S i)

The forward prefix preserves the sum register (S is never a target).

theorem Reversible.gidneyForwardSlice_preserves {m n : ℕ} (L : GidneyLayout m n) (s : State m) (k : ℕ) {w : Fin m} (hA : w ≠ L.A k) (hB : w ≠ L.B k) (hG : w ≠ L.G (k + 1)) : denote (gidneyForwardSlice L k) s w = s w

The forward slice for bit k preserves any wire outside {A k, B k, G (k+1)}.

The forward carry invariant

theorem Reversible.gidneyForward_invariant {m n : ℕ} (L : GidneyLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (k : ℕ) : k ≤ n → (∀ i ≤ k, denote (gidneyForwardPrefix L k) s (L.G i) = carryOf (fun (i : ℕ) => s (L.A i)) (fun (i : ℕ) => s (L.B i)) i) ∧ (∀ (i : ℕ), k < i → i ≤ n → denote (gidneyForwardPrefix L k) s (L.G i) = false) ∧ (∀ i < k, denote (gidneyForwardPrefix L k) s (L.A i) = (s (L.A i) ^^ carryOf (fun (i : ℕ) => s (L.A i)) (fun (i : ℕ) => s (L.B i)) i)) ∧ (∀ i < k, denote (gidneyForwardPrefix L k) s (L.B i) = (s (L.B i) ^^ carryOf (fun (i : ℕ) => s (L.A i)) (fun (i : ℕ) => s (L.B i)) i)) ∧ (∀ (i : ℕ), k ≤ i → i < n → denote (gidneyForwardPrefix L k) s (L.A i) = s (L.A i)) ∧ ∀ (i : ℕ), k ≤ i → i < n → denote (gidneyForwardPrefix L k) s (L.B i) = s (L.B i)

The forward carry invariant. After the first k forward slices: every computed carry G i (i ≤ k) holds the true carry carryOf i; the not-yet-computed ancillas (k < i ≤ n) are still false; the processed addend bits (i < k) are XOR-shifted A i = a_i ⊕ carryOf i, B i = b_i ⊕ carryOf i; and the unprocessed addend bits (k ≤ i < n) are still their inputs. By induction on k, each step one Gidney cell on the fresh G (k+1).

Per-bit value of the full adder

theorem Reversible.gidneyAdd_sum_bit {m n : ℕ} (L : GidneyLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (hS0 : ∀ (i : ℕ), s (L.S i) = false) (k : ℕ) (hk : k < n) : denote (gidneyAdd L) s (L.S k) = (s (L.A k) ^^ s (L.B k) ^^ carryOf (fun (i : ℕ) => s (L.A i)) (fun (i : ℕ) => s (L.B i)) k)

Per-bit sum value. Bit k of the sum register holds A k ⊕ B k ⊕ carry k. The forward pass XOR-shifts the addends (A k ⊕ c, B k ⊕ c), the sum pass XORs them with G k = c (the two c shifts cancel one), and the reverse pass only touches A, B, G, so S k survives.

Headline theorems

theorem Reversible.gidneyAdd_correct {m n : ℕ} (L : GidneyLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (hS0 : ∀ (i : ℕ), s (L.S i) = false) : regValRange L.S (denote (gidneyAdd L) s) n = (regValRange L.A s n + regValRange L.B s n) % 2 ^ n

Gidney adder correctness. For a disjoint-wire layout with the carry chain and the sum register initialised false, the sum register ends holding (A + B) mod 2 ^ n. General n. The proof is the #30 arithmetic (adder_sum_identity) over the Gidney per-bit value gidneyAdd_sum_bit.

theorem Reversible.gidneyAdd_preserves_nonS {m n : ℕ} (L : GidneyLayout m n) (s : State m) (w : Fin m) (hw : ∀ i < n, w ≠ L.S i) : denote (gidneyAdd L) s w = s w

Non-S wires are restored. Any wire that is not a (used) sum-register wire is returned to its input: the sum pass leaves it untouched (andSumPrefix_preserves_of_ne_S), so the reverse pass inverse (gidneyForward L) undoes the forward pass on it (reversible_inverse_correct). The frame behind addend / carry restoration.

theorem Reversible.gidneyAdd_ancilla_clean {m n : ℕ} (L : GidneyLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (j : ℕ) : denote (gidneyAdd L) s (L.G j) = false

Ancilla-clean: every carry ancilla returns to false.

theorem Reversible.gidneyAdd_preserves_A {m n : ℕ} (L : GidneyLayout m n) (s : State m) (k : ℕ) : denote (gidneyAdd L) s (L.A k) = s (L.A k)

Addend A is restored. The forward XOR-shift A i ← A i ⊕ carry i is undone by the reverse pass.

theorem Reversible.gidneyAdd_preserves_B {m n : ℕ} (L : GidneyLayout m n) (s : State m) (k : ℕ) : denote (gidneyAdd L) s (L.B k) = s (L.B k)

Addend B is restored.

Derived cost: 2n Toffolis (n forward + n reverse)

theorem Reversible.gidneyForwardPrefix_toffoli {m n : ℕ} (L : GidneyLayout m n) (k : ℕ) : (circuitCost (gidneyForwardPrefix L k)).toffoli = k

theorem Reversible.gidneyForward_toffoli {m n : ℕ} (L : GidneyLayout m n) : (circuitCost (gidneyForward L)).toffoli = n

theorem Reversible.gidneyAdd_uncompute_toffoli {m n : ℕ} (L : GidneyLayout m n) : (circuitCost (inverse (gidneyForward L))).toffoli = n

The reverse pass is n Toffolis — the andUncompute-shaped blocks a measurement-based gadget eliminates (the win over Cuccaro). It equals the forward pass (gidneyForward, n) by cost_inverse_toffoli.

theorem Reversible.gidneyAdd_toffoli {m n : ℕ} (L : GidneyLayout m n) : (circuitCost (gidneyAdd L)).toffoli = 2 * n

Derived Toffoli cost: 2 * n. n forward Gidney cells (one Toffoli each) + n reverse uncompute Toffolis; the sum pass is CNOT-only. One third of #30's 6n; equal to Cuccaro's 2n at the unitary level (the win over Cuccaro is the measurement re-cost of the reverse n).

Non-vacuity witness + #eval cross-check

A concrete 2-bit Gidney layout on Fin 9: A → {0,1}, B → {2,3}, S → {4,5}, carry chain G → {6,7,8}. The headline applies, and the strict Array evaluator runArr (bridge regValRangeArr_eq) witnesses 2 + 3 = 5 (= 1 mod 4), every carry ancilla / addend restored.

def Reversible.gidneyLayout2 : GidneyLayout 9 2

A concrete 2-bit Gidney layout on Fin 9.

Equations

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

def Reversible.gidneyWitness2 : State 9

Witness: A = 2 (wires 0,1 = 0,1), B = 3 (wires 2,3 = 1,1), S/G init false.

Equations

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