Reversible modular addition — register encoding, verified full adder, ripple cost

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

The addition layer of the reversible-circuit substrate (Circuit.lean / Cost.lean; the application that motivated this substrate lives in the Ecdsafail repository, specs/ecdsa/ecdlp-resource-plan.md there). Pass 1 delivers a sorry-free semantic + derived-cost scaffold: the register readout regVal, the fully verified four-gate full-adder gadget, its derived cost, and the linear Toffoli / CNOT count of a k-slice ripple adder (composed through the Tranche-1 cost_comp_* lemmas, not re-derived).

The locked design decision is respected throughout: every cost claim is about an exhibited Circuit and is discharged through circuitCost. The full-adder correctness is genuine all-inputs coverage (decide over Fintype (Fin 4 → Bool)), not a single example.

What is proved here

Pass 1 (cost + gadget):

• regVal little-endian readout, regVal_lt_two_pow, and the bit-update law regVal_update_eq.
• fullAdder (four gates) with full all-inputs correctness on the concrete State 4 layout: sum bit b ← a ⊕ b ⊕ cin, carry-out cout ← majority(a, b, cin) (with cout init false), a and cin preserved.
• fullAdder_cost: derived toffoli = 2, cnot = 2 (and the full Cost record).
• rippleAdder (a k-slice concatenation of fullAdder gadgets) with linear cost: (circuitCost (rippleAdder ...)).toffoli = 2 * k and .cnot = 2 * k, composed through the Tranche-1 composition lemmas.

Pass 2 Stage A (general gadget): fullAdder_correct_general lifts the full-adder correctness off the concrete State 4 to arbitrary distinct Fin n wires, via the Circuit-level frame lemma denote_apply_of_forall_not_mem / fullAdder_apply_of_ne.

Pass 2 Stage B (carry-chain arithmetic — the modular-addition correctness): rippleCirc, the in-place ripple adder over a disjoint-wire RippleLayout with all carry wires initially false, computes (A + B) mod 2 ^ n into register B: rippleCirc_correct. Proved by induction on the slices (rippleCirc_invariant, the 4-clause carry invariant) lifting fullAdder_correct_general through the frame lemma and the per-slice arithmetic fulladder_nat. Non-vacuity witnessed by rippleLayout2 (a concrete 2-bit layout on Fin 7). This is the genuine computational correctness, not just the cost.

The addition modulus is 2 ^ n. The carry wires are part of the supplied layout and are not uncomputed by this circuit. circuitCost fixes ancilla = 0 and counts Toffoli as a primitive with tCount = 0; these conventions do not assert zero carry workspace or a zero-T implementation over a decomposed gate set. Its toffoliDepth is the sequential gate count.

Register encoding (little-endian)

def Reversible.regVal {n : ℕ} (s : State n) : ℕ

Little-endian binary readout of a wire state: wire i carries place value 2 ^ i.

Equations

• Reversible.regVal s = ∑ i : Fin n, if s i = true then 2 ^ ↑i else 0

@[simp]

theorem Reversible.regVal_zero (s : State 0) : regVal s = 0

theorem Reversible.regVal_lt_two_pow {n : ℕ} (s : State n) : regVal s < 2 ^ n

The register value is bounded by 2 ^ n (an n-wire register holds an n-bit number).

theorem Reversible.regVal_update_eq {n : ℕ} (s : State n) (i : Fin n) (b : Bool) : regVal (Function.update s i b) = (regVal s - if s i = true then 2 ^ ↑i else 0) + if b = true then 2 ^ ↑i else 0

The general place-value update law for Function.update s i b: replacing wire i's bit by b (for ANY prior bit s i and ANY new bit b) removes i's old place-value contribution and adds the new one. The reusable round-trip helper consumed by ModMul / ScalarMul.

The full-adder gadget (the verified primitive)

def Reversible.majority (a b c : Bool) : Bool

Boolean majority of three bits: at least two are set.

Equations

• Reversible.majority a b c = (a && b || a && c || b && c)

def Reversible.fullAdder {n : ℕ} (a b cin cout : Fin n) : Circuit n

The four-gate full adder on pairwise-distinct wires a b cin cout (with cout initialised false): b ← a ⊕ b ⊕ cin (sum bit), cout ← majority(a, b, cin) (carry-out), a/cin unchanged.

The gate order realises the standard in-place adder: write the partial carry into cout from (a,b), fold a into b, fold (cin,b) into cout, fold cin into b. Correctness on the concrete layout is fullAdder_correct.

Equations

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

theorem Reversible.fullAdder_correct (s : State 4) : s 3 = false → denote (fullAdder 0 1 2 3) s 1 = (s 0 ^^ s 1 ^^ s 2) ∧ denote (fullAdder 0 1 2 3) s 3 = majority (s 0) (s 1) (s 2) ∧ denote (fullAdder 0 1 2 3) s 0 = s 0 ∧ denote (fullAdder 0 1 2 3) s 2 = s 2

Full-adder correctness — genuine all-inputs coverage. On the concrete State 4 layout (wires 0,1,2,3 = a,b,cin,cout), with cout initialised false, the gadget computes the sum bit on wire 1, the carry-out on wire 3, and preserves a (wire 0) and cin (wire 2). Proved by decide over the finite State 4 = Fin 4 → Bool: 16 states, of which eight satisfy the initialisation hypothesis s 3 = false.

theorem Reversible.fullAdder_apply_of_ne {n : ℕ} {a b cin cout w : Fin n} (ha : w ≠ a) (hb : w ≠ b) (hcin : w ≠ cin) (hcout : w ≠ cout) (s : State n) : denote (fullAdder a b cin cout) s w = s w

Frame lemma for the gadget. A wire distinct from all four of a, b, cin, cout is untouched by fullAdder (every gate's wires lie in {a, b, cin, cout}). The payoff of the Circuit-level denote_apply_of_forall_not_mem; lets the carry-chain (Pass 2) lift this slice over a register.

theorem Reversible.fullAdder_correct_general {n : ℕ} {a b cin cout : Fin n} (hba : b ≠ a) (hbcin : b ≠ cin) (hcouta : cout ≠ a) (hcoutb : cout ≠ b) (hcoutcin : cout ≠ cin) (hacin : a ≠ cin) {s : State n} (hc0 : s cout = false) : denote (fullAdder a b cin cout) s b = (s a ^^ s b ^^ s cin) ∧ denote (fullAdder a b cin cout) s cout = majority (s a) (s b) (s cin) ∧ denote (fullAdder a b cin cout) s a = s a ∧ denote (fullAdder a b cin cout) s cin = s cin

Full-adder correctness, general Fin n wires. For pairwise-distinct wires a, b, cin, cout with cout initialised false, the gadget writes the sum bit to b, the carry-out to cout, and preserves a and cin — over arbitrary Fin n (not just the concrete State 4 of fullAdder_correct). This is the slice the ripple carry-chain (Pass 2) iterates.

Derived cost of the gadget

theorem Reversible.fullAdder_cost {n : ℕ} (a b cin cout : Fin n) : circuitCost (fullAdder a b cin cout) = { qubits := n, ancilla := 0, toffoli := 2, toffoliDepth := 2, cnot := 2, tCount := 0, meas := 0 }

Derived cost of the full adder (from the gate list, via circuitCost): qubits = n, two Toffolis, two CNOTs and sequential Toffoli depth two. The remaining fields are zero by the abstract cost model; in particular, it does not separately count the supplied carry wire as ancilla or decompose Toffoli gates into T gates.

@[simp]

theorem Reversible.fullAdder_toffoli {n : ℕ} (a b cin cout : Fin n) : (circuitCost (fullAdder a b cin cout)).toffoli = 2

@[simp]

theorem Reversible.fullAdder_cnot {n : ℕ} (a b cin cout : Fin n) : (circuitCost (fullAdder a b cin cout)).cnot = 2

Ripple adder (general n): linear cost

def Reversible.rippleAdder {n : ℕ} (slices : List (Fin n × Fin n × Fin n × Fin n)) : Circuit n

A k-slice concatenation of fullAdder gadgets, one per quadruple (a, b, cin, cout) in slices. This definition imposes no wire-layout or initialisation conditions; the cost lemmas hold for any slice list. Arithmetic correctness is proved below for rippleCirc with a RippleLayout and zero-initialised carries.

Equations

• Reversible.rippleAdder slices = List.flatMap (fun (q : Fin n × Fin n × Fin n × Fin n) => Reversible.fullAdder q.1 q.2.1 q.2.2.1 q.2.2.2) slices

@[simp]

theorem Reversible.rippleAdder_nil {n : ℕ} : rippleAdder [] = []

theorem Reversible.rippleAdder_toffoli {n : ℕ} (slices : List (Fin n × Fin n × Fin n × Fin n)) : (circuitCost (rippleAdder slices)).toffoli = 2 * slices.length

Ripple-adder Toffoli count is linear in the number of slices. Each slice contributes exactly two Toffolis (fullAdder_toffoli); the count adds over the concatenation (cost_comp_toffoli_count). Proved by induction over the slice list, composing the Tranche-1 lemma — not by re-deriving the sum.

theorem Reversible.rippleAdder_cnot {n : ℕ} (slices : List (Fin n × Fin n × Fin n × Fin n)) : (circuitCost (rippleAdder slices)).cnot = 2 * slices.length

Ripple-adder CNOT count is linear in the number of slices. Same route via cost_comp_cnot_count + fullAdder_cnot.

Pass 2: ripple carry-chain arithmetic correctness

The Pass-1 ripple cost says nothing about what rippleAdder computes. Here we exhibit a concrete in-place ripple layout (input registers A, B and a carry chain C, as injective pairwise-disjoint wire families) and prove the register B ends up holding (A + B) mod 2 ^ n, by induction on the slices, lifting fullAdder_correct_general through the frame lemma fullAdder_apply_of_ne.

def Reversible.regValRange {m : ℕ} (f : ℕ → Fin m) (s : State m) (k : ℕ) : ℕ

Place-value readout of the low k bits of a register laid out on wires f i (place value 2 ^ i at index i). Indices are ℕ to keep the layout arithmetic coercion-free.

Equations

• Reversible.regValRange f s k = ∑ i ∈ Finset.range k, (s (f i)).toNat * 2 ^ i

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

theorem Reversible.regValRange_lt {m : ℕ} (f : ℕ → Fin m) (s : State m) (k : ℕ) : regValRange f s k < 2 ^ k

theorem Reversible.fulladder_nat (a b c : Bool) : (a ^^ b ^^ c).toNat + 2 * (majority a b c).toNat = a.toNat + b.toNat + c.toNat

The full-adder arithmetic identity on ℕ. The sum bit plus twice the carry equals the arithmetic sum of the three input bits — the per-slice fact the carry chain accumulates.

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

A ripple-carry adder layout on m wires for n-bit registers: input registers A, B and a carry chain C (with C 0 the input carry and C n the output carry), as ℕ-indexed wire families. The three families have disjoint images over all natural indices, including unused indices. Injectivity is required only on the used ranges: 0 .. n-1 for A, B and 0 .. n for C. These are wire-layout hypotheses; carry initialisation is assumed separately by correctness.

• A : ℕ → Fin m

  Wires of register A (the first addend).

• B : ℕ → Fin m

  Wires of register B (the second addend; overwritten with the sum).

• C : ℕ → Fin m

  Wires of the carry chain (C i = carry into bit i).

• hAB (i j : ℕ) : self.A i ≠ self.B j
• hAC (i j : ℕ) : self.A i ≠ self.C j
• hBC (i j : ℕ) : self.B i ≠ self.C 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
• hCinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.C i = self.C j → i = j

def Reversible.rippleSlice {n m : ℕ} (L : RippleLayout m n) (i : ℕ) : Circuit m

One ripple slice: a full adder on (A i, B i, C i, C (i+1)).

Equations

• Reversible.rippleSlice L i = Reversible.fullAdder (L.A i) (L.B i) (L.C i) (L.C (i + 1))

def Reversible.ripplePrefix {n m : ℕ} (L : RippleLayout m n) (k : ℕ) : Circuit m

The circuit of the first k slices (bits 0 .. k-1).

Equations

• Reversible.ripplePrefix L k = List.flatMap (Reversible.rippleSlice L) (List.range k)

def Reversible.rippleCirc {n m : ℕ} (L : RippleLayout m n) : Circuit m

The full ripple adder: all n slices.

Equations

• Reversible.rippleCirc L = Reversible.ripplePrefix L n

theorem Reversible.denote_ripplePrefix_succ {n m : ℕ} (L : RippleLayout m n) (k : ℕ) (s : State m) : denote (ripplePrefix L (k + 1)) s = denote (rippleSlice L k) (denote (ripplePrefix L k) s)

theorem Reversible.rippleCirc_invariant {n m : ℕ} (L : RippleLayout m n) (s : State m) (hC0 : ∀ (j : ℕ), s (L.C j) = false) (k : ℕ) : k ≤ n → regValRange L.B (denote (ripplePrefix L k) s) k + (denote (ripplePrefix L k) s (L.C k)).toNat * 2 ^ k = regValRange L.A s k + regValRange L.B s k ∧ (∀ j < n, denote (ripplePrefix L k) s (L.A j) = s (L.A j)) ∧ (∀ (j : ℕ), k ≤ j → j < n → denote (ripplePrefix L k) s (L.B j) = s (L.B j)) ∧ ∀ (j : ℕ), k < j → j < n + 1 → denote (ripplePrefix L k) s (L.C j) = s (L.C j)

The carry-chain invariant. With all carry wires initially false, after the first k slices: the value of register B's low k bits plus 2 ^ k times the carry into bit k equals the sum of the original low-k values of A and B (P1); register A is untouched (P2); the unprocessed high bits of B (P4) and the unset high carries (P5) are preserved. By induction on k, each step lifting fullAdder_correct_general through the frame lemma fullAdder_apply_of_ne.

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

Ripple-carry adder correctness (Pass 2 headline). For a disjoint-wire layout with all carries initialised false, the ripple adder leaves register B holding (A + B) mod 2 ^ n. The carry-chain identity, derived from the exhibited circuit rippleCirc — not postulated.

Non-vacuity witness

A concrete 2-bit ripple layout on Fin 7 (register A on wires 0,1, B on 2,3, carry chain C on 4,5,6), exhibiting that RippleLayout is inhabited and rippleCirc_correct applies — the headline is not vacuously quantified over an unsatisfiable hypothesis bundle.

def Reversible.rippleLayout2 : RippleLayout 7 2

A concrete 2-bit adder layout: A → {0,1}, B → {2,3}, carry chain C → {4,5,6} on Fin 7.

Equations

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