Reversible modular constant-multiply and negation — the last two field-op gadgets (ECDLP Phase 2, Stage S6.3e-2a)

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

This module verifies the last two modular field-operation gadgets the SLP → circuit router needs, completing the toolkit {modAdd, modSub, modDouble, mulLoop}:

• modConstMul (c · a mod N, with c a CLASSICAL constant): repeated modular addition. From acc = 0 and a fixed operand register Aop = a, run c successive modAdd (Aop = a) → (B = acc) on fresh per-step banks; each maps acc ← (a + acc) mod N (modAdd_correct), preserving a (modAdd_preserves_operand) and acc < N (modAdd_in_range). After c steps acc = (c·a) mod N.
• modNeg ((N − b) mod N, the additive inverse (−b) mod N): exactly modSub with the minuend register holding 0. modSub_correct at a := 0 gives (0 + N − b) % N = (N − b) % N.

modConstMul L c = ((List.range c).map (fun j => modAdd (L.bank j))).flatMap id
modNeg L        = modSub L                      -- with the minuend register init 0

Carve line (what this is, and is NOT)

These are the value-correct field-operation PRIMITIVES in the fresh-ancilla model, completing the gadget set. ℕ / mod N bit arithmetic; NO field / group / curve semantics here.

• modConstMul is repeated modAdd: an O(c)-add schedule. An optional cost optimisation is the double-and-add variant (O(log c) modular doublings + adds), which is the standard speedup; it is NOT built here, and is not needed for the SMALL EC coefficients (the nsmul coefficients the EC point op uses are constants ≤ 8, which do not even count toward the free parameter M).
• modNeg is modSub with a zero minuend. (N − b) % N is 0 when b = 0 and N − b when 0 < b < N — the genuine additive inverse (−b) mod N.

Named residue (same fresh-ancilla model as modAdd / modSub): the per-bank carry chains and the borrow chain / comparison flags are left dirty; correctness holds because each bank / use supplies fresh wires (the Cadd / C1 / C2 / anc of each modConstMul bank, the Bor / C / anc of modNeg, are required false). In-place reuse needs carry-clean / ancilla-restoring adders the corpus does NOT yet provide. The SLP → circuit assembly of the EC point operation (routing ALL opcodes — add, sub, mul / sq, nsmul, neg — and deriving M as an exhibited-circuit count) is S6.3e-2b / S6.3e-3, NOT claimed here. This module supplies the two missing opcode gadgets.

Honest cost

• modConstMul_toffoli derives c · 12 · n Toffolis: c modular adds, each 12n (modularAdd_toffoli), composed through cost_comp_toffoli_count over the fold.
• modNeg_toffoli is 10n, inherited verbatim from modSub_toffoli.

Part 1 — modConstMul (c · a mod N, repeated modular addition)

A ConstMulLayout bundles c per-step ModAddLayout banks (bank j, S6.3b), all sharing the operand register Aop (the fixed addend a) and the accumulator B, with bank j supplying its OWN fresh Cadd / A1 / C1 / A2 / C2 / anc. The inter-bank geometry — bank j must not touch bank k's clean / preset wires (k ≠ j) — is carried by the membership footprints CTouches / CClean and the single disjointness field hInter, mirroring mulLoop's Touches / Clean schema but SIMPLER: no control bit, no doubling, and the operand Aop is FIXED (shared) across every bank.

def Reversible.CTouches {m n : ℕ} (L : ℕ → ModAddLayout m n) (j : ℕ) (w : Fin m) : Prop

The wire families bank j's modAdd circuit touches (writes or reads): the shared operand Aop, the shared accumulator B, and bank j's private carry chains / presets / ancilla.

Equations

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

def Reversible.CClean {m n : ℕ} (L : ℕ → ModAddLayout m n) (k : ℕ) (w : Fin m) : Prop

The wire families bank k's modAdd_correct reads as a clean / preset precondition: the carry chains Cadd / C1 / C2 (false), the ancilla anc (false), and the constant presets A1 / A2. (The shared Aop and B are handled separately by the running invariant.)

Equations

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

structure Reversible.ConstMulLayout (m n c : ℕ) : Type

A c-bank constant-multiply layout on Fin m. The c banks share the operand Aop and the accumulator B; bank j does not touch bank k's clean wires for k ≠ j (hInter). All hypotheses are bounded, so the schema is inhabitable for every c (the witness assigns each bank a disjoint contiguous block; see constMulLayout2).

• bank : ℕ → ModAddLayout m n

  The c per-step modular-addition banks (bank j runs the j-th acc ← (a + acc) mod N).

• hAopShare (j j' : ℕ) : (self.bank j).Aop = (self.bank j').Aop

  Sharing: every bank reads the same operand Aop (the fixed addend a).

• hBShare (j j' : ℕ) : (self.bank j).B = (self.bank j').B

  Sharing: every bank acts on the same accumulator B.

• hInter (j k : ℕ) (w : Fin m) : j < c → k < c → j ≠ k → CClean self.bank k w → ¬CTouches self.bank j w

  Inter-bank disjointness: for j ≠ k, bank j's circuit does not touch bank k's clean wires.

def Reversible.ConstMulLayout.Aop {m n c : ℕ} (L : ConstMulLayout m n c) : ℕ → Fin m

The shared operand register (Aop of bank 0).

Equations

• L.Aop = (L.bank 0).Aop

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

The shared accumulator register (B of bank 0).

Equations

• L.B = (L.bank 0).B

theorem Reversible.notCTouches_preserved {m n c : ℕ} (L : ConstMulLayout m n c) (j : ℕ) (s : State m) (w : Fin m) (hw : ¬CTouches L.bank j w) : denote (modAdd (L.bank j)) s w = s w

A wire not touched by bank j survives bank j's modular add. (The CTouches predicate lists exactly the 8 families modAdd_preserves_external requires disjointness from.)

theorem Reversible.cbank_step_preserves_clean {m n c : ℕ} (L : ConstMulLayout m n c) (j k : ℕ) (hj : j < c) (hk : k < c) (hjk : j ≠ k) (s : State m) (w : Fin m) (hw : CClean L.bank k w) : denote (modAdd (L.bank j)) s w = s w

A clean wire of bank k survives bank j's modular add (j ≠ k, both < c): by hInter it is not touched, so notCTouches_preserved applies.

The constant-multiply circuit and its prefix

def Reversible.constMulCirc {m n c : ℕ} (L : ConstMulLayout m n c) : Circuit m

The modular constant-multiply circuit. Run c successive modular adds acc ← (a + acc) mod N, one per bank, on the shared operand Aop = a and accumulator B = acc; every other wire is fresh.

Equations

• Reversible.constMulCirc L = List.flatMap id (List.map (fun (j : ℕ) => Reversible.modAdd (L.bank j)) (List.range c))

def Reversible.constMulUpto {m n c : ℕ} (L : ConstMulLayout m n c) (k : ℕ) : Circuit m

The first k banks of the constant-multiply (prefix [0, …, k-1]), the induction handle.

Equations

• Reversible.constMulUpto L k = List.flatMap id (List.map (fun (j : ℕ) => Reversible.modAdd (L.bank j)) (List.range k))

@[simp]

theorem Reversible.constMulUpto_zero {m n c : ℕ} (L : ConstMulLayout m n c) : constMulUpto L 0 = []

theorem Reversible.constMul_eq_upto {m n c : ℕ} (L : ConstMulLayout m n c) : constMulCirc L = constMulUpto L c

theorem Reversible.constMulUpto_succ {m n c : ℕ} (L : ConstMulLayout m n c) (k : ℕ) : constMulUpto L (k + 1) = constMulUpto L k ++ modAdd (L.bank k)

Split the prefix at its last bank: constMulUpto L (k+1) = constMulUpto L k ++ modAdd (bank k) (bank k runs LAST). From List.range_succ.

theorem Reversible.constMulUpto_preserves {m n c : ℕ} (L : ConstMulLayout m n c) (k : ℕ) (s : State m) (w : Fin m) (hw : ∀ j < k, ¬CTouches L.bank j w) : denote (constMulUpto L k) s w = s w

Prefix frame. A wire not touched by any bank j < k survives the whole prefix constMulUpto L k (fold of notCTouches_preserved).

theorem Reversible.cclean_pres {m n c : ℕ} (L : ConstMulLayout m n c) {k p : ℕ} (hk : k < c) (hpk : p ≤ k) (s : State m) (w : Fin m) (hw : CClean L.bank k w) : denote (constMulUpto L p) s w = s w

A clean / preset wire of bank k survives every earlier-bank prefix (p ≤ k < c): each lies in CClean L.bank k, so hInter keeps it untouched by every bank j < p ≤ k.

theorem Reversible.cclean_pres_reg {m n c : ℕ} (L : ConstMulLayout m n c) {k p : ℕ} (hk : k < c) (hpk : p ≤ k) (s : State m) (f : ℕ → Fin m) (hf : ∀ (i : ℕ), CClean L.bank k (f i)) (q : ℕ) : regValRange f (denote (constMulUpto L p) s) q = regValRange f s q

The constant-multiply invariant and correctness

theorem Reversible.constMul_invariant {m n c : ℕ} (L : ConstMulLayout m n c) (s : State m) {N aval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (haN : aval < N) (hB0 : regValRange L.B s n = 0) (hAv : regValRange L.Aop s n = aval) (hCadd : ∀ (j i : ℕ), j < c → s ((L.bank j).Cadd i) = false) (hC1 : ∀ (j i : ℕ), j < c → s ((L.bank j).C1 i) = false) (hC2 : ∀ (j i : ℕ), j < c → s ((L.bank j).C2 i) = false) (hanc : ∀ j < c, s (L.bank j).anc = false) (hA1 : ∀ j < c, regValRange (L.bank j).A1 s n = 2 ^ n - N) (hA2 : ∀ j < c, regValRange (L.bank j).A2 s n = N) (k : ℕ) : k ≤ c → regValRange L.B (denote (constMulUpto L k) s) n = k * aval % N ∧ regValRange L.Aop (denote (constMulUpto L k) s) n = aval

The constant-multiply invariant. After the first k banks (k ≤ c), from acc = 0 the accumulator holds (k · aval) mod N and the operand still holds aval. By induction on k, splitting the last bank (constMulUpto_succ): the prefix preserves bank k's clean / preset wires (cclean_pres) and the running Aop/B; modAdd_correct then maps acc = (k·aval) mod N to (aval + (k·aval) mod N) mod N = ((k+1)·aval) mod N (Nat.add_mod), and modAdd_preserves_operand keeps aval.

theorem Reversible.modConstMul_correct {m n c : ℕ} (L : ConstMulLayout m n c) (s : State m) {N aval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (haN : aval < N) (hB0 : regValRange L.B s n = 0) (hAv : regValRange L.Aop s n = aval) (hCadd : ∀ (j i : ℕ), j < c → s ((L.bank j).Cadd i) = false) (hC1 : ∀ (j i : ℕ), j < c → s ((L.bank j).C1 i) = false) (hC2 : ∀ (j i : ℕ), j < c → s ((L.bank j).C2 i) = false) (hanc : ∀ j < c, s (L.bank j).anc = false) (hA1 : ∀ j < c, regValRange (L.bank j).A1 s n = 2 ^ n - N) (hA2 : ∀ j < c, regValRange (L.bank j).A2 s n = N) : regValRange L.B (denote (constMulCirc L) s) n = c * aval % N

The verified modular constant-multiply (the S6.3e-2a Part-1 headline). Under the accumulator initialised 0, the operand Aop holding aval < N, 2N ≤ 2ⁿ, and every bank's clean / preset wires set (carries / ancilla false, presets A1 = 2ⁿ − N, A2 = N), the circuit leaves the accumulator holding (c · aval) mod N: regValRange B (denote (constMulCirc L) s) n = (c · aval) % N.

Proof: constMul_invariant at k = c. Both branches — the c = 0 base (acc = 0 = (0·aval)%N) and the c → c+1 step ((aval + (k·aval)%N)%N = ((k+1)·aval)%N) — are genuinely covered by the induction.

theorem Reversible.modConstMul_preserves_operand {m n c : ℕ} (L : ConstMulLayout m n c) (s : State m) {N aval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (haN : aval < N) (hB0 : regValRange L.B s n = 0) (hAv : regValRange L.Aop s n = aval) (hCadd : ∀ (j i : ℕ), j < c → s ((L.bank j).Cadd i) = false) (hC1 : ∀ (j i : ℕ), j < c → s ((L.bank j).C1 i) = false) (hC2 : ∀ (j i : ℕ), j < c → s ((L.bank j).C2 i) = false) (hanc : ∀ j < c, s (L.bank j).anc = false) (hA1 : ∀ j < c, regValRange (L.bank j).A1 s n = 2 ^ n - N) (hA2 : ∀ j < c, regValRange (L.bank j).A2 s n = N) : regValRange L.Aop (denote (constMulCirc L) s) n = aval

The operand register is intact. modConstMul leaves Aop holding aval (read-only addend, which the SLP may reuse). Read off the invariant's second clause at k = c.

theorem Reversible.modConstMul_in_range {m n c : ℕ} (L : ConstMulLayout m n c) (s : State m) {N aval : ℕ} (h2N : 2 * N ≤ 2 ^ n) (haN : aval < N) (hB0 : regValRange L.B s n = 0) (hAv : regValRange L.Aop s n = aval) (hCadd : ∀ (j i : ℕ), j < c → s ((L.bank j).Cadd i) = false) (hC1 : ∀ (j i : ℕ), j < c → s ((L.bank j).C1 i) = false) (hC2 : ∀ (j i : ℕ), j < c → s ((L.bank j).C2 i) = false) (hanc : ∀ j < c, s (L.bank j).anc = false) (hA1 : ∀ j < c, regValRange (L.bank j).A1 s n = 2 ^ n - N) (hA2 : ∀ j < c, regValRange (L.bank j).A2 s n = N) : regValRange L.B (denote (constMulCirc L) s) n < N

The constant-multiply output is a genuine residue in [0, N). Corollary of modConstMul_correct and Nat.mod_lt.

Derived cost

theorem Reversible.modConstMul_toffoli {m n c : ℕ} (L : ConstMulLayout m n c) : (circuitCost (constMulCirc L)).toffoli = c * (12 * n)

Derived Toffoli cost of the modular constant-multiply: c · 12 · n Toffolis, from the exhibited gate list. The circuit is c modular adds (modularAdd_toffoli, 12n each), composed through the fold; the concatenation cost is the sum of the per-bank counts, c · 12n.

Honest reading: O(c) adds (fresh-ancilla model). The O(log c) double-and-add variant is the standard speedup but is NOT built here (and is not needed for the small EC nsmul coefficients).

Non-vacuity witness: a 3-bank (c = 3) constant-multiply on Fin 200

A genuine ConstMulLayout 200 4 3, exhibiting that ConstMulLayout is inhabited and modConstMul_correct applies. Shared operand Aop → {0,1,2,3}, shared accumulator B → {4,5,6,7}; each bank j owns the disjoint fresh block [8 + 24·j, 8 + 24·(j+1)) of Fin 200 for its private Cadd / A1 / C1 / A2 / C2 / anc. All disjointness is linear arithmetic on the wire indices (omega), so the schema is manifestly inhabitable; the same stride formula inhabits every c.

n = 4 is needed (not n = 3): the modular adder requires 2N ≤ 2ⁿ so the add does not wrap; for N = 5 that forces 2ⁿ ≥ 10, i.e. n ≥ 4. The registers (Aop, B, A1, A2) are 4-bit (min i 3); the carry chains (Cadd, C1, C2) are 5-element (min i 4).

def Reversible.cBank (base : ℕ) (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) : ModAddLayout 200 4

Bank j's ModAddLayout 200 4 on the shared Aop → {0,1,2,3}, B → {4,5,6,7} and the private block [base, base+24) with base = 8 + 24·j: Cadd → [base,base+5), A1 → [base+5,base+9), C1 → [base+9,base+14), A2 → [base+14,base+18), C2 → [base+18,base+23), anc → base+23.

Equations

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

Interface lemmas (CONVENTIONS §9.1, F1): the bank's wire assignments at the value level, one lemma per field — what the range/interleaving proofs project out of the structure.

theorem Reversible.cBank_Aop_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).Aop i) = min i 3

The bank's operand wires, value level.

theorem Reversible.cBank_B_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).B i) = 4 + min i 3

The bank's accumulator wires, value level.

theorem Reversible.cBank_Cadd_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).Cadd i) = base + min i 4

The bank's add-step carry wires, value level.

theorem Reversible.cBank_A1_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).A1 i) = base + 5 + min i 3

The bank's step-1 constant-register wires, value level.

theorem Reversible.cBank_C1_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).C1 i) = base + 9 + min i 4

The bank's step-1 carry wires, value level.

theorem Reversible.cBank_A2_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).A2 i) = base + 14 + min i 3

The bank's step-3 constant-register wires, value level.

theorem Reversible.cBank_C2_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) (i : ℕ) : ↑((cBank base hlo hb).C2 i) = base + 18 + min i 4

The bank's step-3 carry wires, value level.

theorem Reversible.cBank_anc_val {base : ℕ} (hlo : 8 ≤ base) (hb : base + 24 ≤ 200) : ↑(cBank base hlo hb).anc = base + 23

The bank's ancilla wire, value level.

theorem Reversible.cBank_clean_range (k : ℕ) (hk : k < 3) (w : Fin 200) (hw : CClean (fun (j : ℕ) => cBank (8 + 24 * min j 2) ⋯ ⋯) k w) : 8 + 24 * k ≤ ↑w ∧ ↑w < 8 + 24 * k + 24

Every CClean (cBank' ·) k w wire (k < 3) lies in bank k's private block [8 + 24·k, 8 + 24·k + 24). (All 6 clean / preset families are private; none is Aop or B.)

theorem Reversible.cBank_touch_range (j : ℕ) (hj : j < 3) (w : Fin 200) (hw : CTouches (fun (j_1 : ℕ) => cBank (8 + 24 * min j_1 2) ⋯ ⋯) j w) : ↑w < 8 ∨ 8 + 24 * j ≤ ↑w ∧ ↑w < 8 + 24 * j + 24

Every CTouches (cBank' ·) j w wire (j < 3) lies in {0,…,7} ∪ [8 + 24·j, 8 + 24·j + 24) — the shared Aop/B and bank j's private block.

def Reversible.constMulLayout2 : ConstMulLayout 200 4 3

The concrete 3-bank (c = 3) constant-multiply layout on Fin 200. Aop → {0,1,2,3}, B → {4,5,6,7}, bank j on the fresh block [8 + 24·j, 8 + 24·(j+1)). The geometry fields reduce to the block-range lemmas cBank_clean_range / cBank_touch_range and omega.

Equations

• Reversible.constMulLayout2 = { bank := fun (j : ℕ) => Reversible.cBank (8 + 24 * min j 2) ⋯ ⋯, hAopShare := ⋯, hBShare := ⋯, hInter := ⋯ }

theorem Reversible.constMulLayout2_bank (j : ℕ) : constMulLayout2.bank j = cBank (8 + 24 * min j 2) ⋯ ⋯

Every bank of constMulLayout2 is the standard cBank at its stride-24 base (interface lemma, §9.1).

Harness #eval cross-checks and proven instances (c = 3, 8, 0, 1)

constMulState sets the shared Aop → {0,1,2,3} to aval, the accumulator B → {4,5,6,7} to 0, and presets every bank's reduce constants A1 = 2ⁿ − N = 11 (bits 0,1,3) and A2 = N = 5 (bits 0,2); every scratch / carry / ancilla is false. Reading register B (low 4 bits) off the strict Array Bool evaluator (runArr, via the proven bridge regValRangeArr_eq) gives the value modConstMul_correct constrains, computed instantly. N = 5 (2N = 10 ≤ 2⁴) throughout.

def Reversible.constMulState (a0 a1 a2 : Bool) : State 200

Concrete input state on Fin 200 for c, n = 4, N = 5: Aop = (a0,a1,a2) on wires {0,1,2} (top bit Aop 3 = 0), B = 0 (wires {4,5,6,7}), every bank's presets A1 = 11 (block bits 0,1,3) and A2 = 5 (block bits 0,2), all scratch / carries / ancilla false. Bank j's A1 is at wires {base+5, base+6, base+8}, A2 at {base+14, base+16} with base = 8 + 24·j.

Equations

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

theorem Reversible.cmin4_cases (i : ℕ) : min i 4 = 0 ∨ min i 4 = 1 ∨ min i 4 = 2 ∨ min i 4 = 3 ∨ min i 4 = 4

min i 4 ranges over {0,1,2,3,4}; turns an ∀ i carry-wire goal whose wire depends on i only through min i 4 into five concrete decide-able cases.

theorem Reversible.constMulState_pre (a0 a1 a2 : Bool) : (∀ (j i : ℕ), j < 3 → constMulState a0 a1 a2 ((constMulLayout2.bank j).Cadd i) = false) ∧ (∀ (j i : ℕ), j < 3 → constMulState a0 a1 a2 ((constMulLayout2.bank j).C1 i) = false) ∧ (∀ (j i : ℕ), j < 3 → constMulState a0 a1 a2 ((constMulLayout2.bank j).C2 i) = false) ∧ (∀ j < 3, constMulState a0 a1 a2 (constMulLayout2.bank j).anc = false) ∧ (∀ j < 3, regValRange (constMulLayout2.bank j).A1 (constMulState a0 a1 a2) 4 = 2 ^ 4 - 5) ∧ ∀ j < 3, regValRange (constMulLayout2.bank j).A2 (constMulState a0 a1 a2) 4 = 5

The clean / preset preconditions of modConstMul_correct hold at constMulState, for any operand bits (n = 4, N = 5). The carry / ancilla families are false; the presets A1 = 11, A2 = 5. Discharged by interval_cases over the 3 banks + cmin4_cases over the wire index.

def Reversible.constMulLayout1 : ConstMulLayout 200 4 1

Proven instance, c = 1: c = 1, a = 3, N = 5 ↦ (1 · 3) mod 5 = 3 (a single add). Uses a ConstMulLayout 200 4 1 — the same banks, c = 1.

Equations

• Reversible.constMulLayout1 = { bank := fun (j : ℕ) => Reversible.cBank (8 + 24 * min j 2) ⋯ ⋯, hAopShare := ⋯, hBShare := ⋯, hInter := ⋯ }

theorem Reversible.constMulLayout1_bank (j : ℕ) : constMulLayout1.bank j = cBank (8 + 24 * min j 2) ⋯ ⋯

Every bank of constMulLayout1 is the standard cBank at its stride-24 base (interface lemma, §9.1).

theorem Reversible.constMulState1_pre (a0 a1 a2 : Bool) : (∀ (j i : ℕ), j < 1 → constMulState a0 a1 a2 ((constMulLayout1.bank j).Cadd i) = false) ∧ (∀ (j i : ℕ), j < 1 → constMulState a0 a1 a2 ((constMulLayout1.bank j).C1 i) = false) ∧ (∀ (j i : ℕ), j < 1 → constMulState a0 a1 a2 ((constMulLayout1.bank j).C2 i) = false) ∧ (∀ j < 1, constMulState a0 a1 a2 (constMulLayout1.bank j).anc = false) ∧ (∀ j < 1, regValRange (constMulLayout1.bank j).A1 (constMulState a0 a1 a2) 4 = 2 ^ 4 - 5) ∧ ∀ j < 1, regValRange (constMulLayout1.bank j).A2 (constMulState a0 a1 a2) 4 = 5

def Reversible.constMulLayout0 : ConstMulLayout 200 4 0

Proven instance, the c = 0 base case: c = 0 ↦ 0 (empty circuit, accumulator unchanged at 0). Uses a ConstMulLayout 200 4 0; the headline lands on (0 · aval) % N = 0 with NO add.

Equations

• Reversible.constMulLayout0 = { bank := fun (j : ℕ) => Reversible.cBank (8 + 24 * min j 2) ⋯ ⋯, hAopShare := ⋯, hBShare := ⋯, hInter := ⋯ }

theorem Reversible.constMulLayout0_bank (j : ℕ) : constMulLayout0.bank j = cBank (8 + 24 * min j 2) ⋯ ⋯

Every bank of constMulLayout0 is the standard cBank at its stride-24 base (interface lemma, §9.1).

def Reversible.constMulLayout8 : ConstMulLayout 200 4 8

The c = 8 wrap witness (harness cross-check): c = 8, a = 2, N = 5 ↦ 16 mod 5 = 1. Needs a ConstMulLayout 200 4 8; the strided block formula inhabits c = 8 (8 + 24·7 + 24 = 200). The #eval prints 1, the genuinely-wrapped residue (16 = 3·5 + 1), confirming the running acc < N maintenance across all 8 adds.

Equations

• Reversible.constMulLayout8 = { bank := fun (j : ℕ) => Reversible.cBank (8 + 24 * min j 7) ⋯ ⋯, hAopShare := ⋯, hBShare := ⋯, hInter := ⋯ }

theorem Reversible.constMulLayout8_bank (j : ℕ) : constMulLayout8.bank j = cBank (8 + 24 * min j 7) ⋯ ⋯

Every bank of constMulLayout8 is the standard cBank at its stride-24 base (interface lemma, §9.1).

def Reversible.constMulState8 (a0 a1 a2 : Bool) : State 200

constMulState8 presets all 8 banks' A1 = 11 and A2 = 5 (blocks base = 8 + 24·j, j < 8), Aop = a, B = 0. Bank j's A1 is {base+5, base+6, base+8}, A2 is {base+14, base+16}.

Equations

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

Part 2 — modNeg ((N − b) mod N, the additive inverse)

modNeg(b) = (N − b) mod N = (0 − b) mod N, which is exactly modSub with the minuend register B holding 0. So modNeg IS modSub; the corollary modNeg_correct instantiates modSub_correct at a := 0. (N − b) % N is 0 when b = 0 and N − b when 0 < b < N — the genuine additive inverse (−b) mod N.

def Reversible.modNeg {m n : ℕ} (L : ModSubLayout m n) : Circuit m

The modular-negation circuit. Definitionally modSub (run with the minuend register B initialised to 0, so the output is (N − b) mod N).

Equations

• Reversible.modNeg L = Reversible.modSub L

theorem Reversible.modNeg_correct {m n : ℕ} (L : ModSubLayout m n) (s : State m) (hBor : ∀ (j : ℕ), s (L.Bor j) = false) (hC : ∀ (j : ℕ), s (L.C j) = false) (hanc : s L.anc = false) {N b : ℕ} (hN : N ≤ 2 ^ n) (hNpos : 0 < N) (hNreg : regValRange L.Nreg s n = N) (hB0 : regValRange L.B s n = 0) (hSub : regValRange L.Sub s n = b) (hbN : b < N) : regValRange L.B (denote (modNeg L) s) n = (N - b) % N

The verified modular negation (the S6.3e-2a Part-2 headline). For a disjoint-wire ModSubLayout with the borrow chain Bor, the fix carry chain C, and the ancilla anc initialised false, the constant register Nreg preset to N, the minuend B holding 0, the subtrahend Sub holding b, with b < N, N ≤ 2ⁿ: the circuit modNeg L leaves B holding (N − b) mod N.

A thin corollary of modSub_correct at a := 0: (0 + N − b) % N = (N − b) % N. Both branches are covered — b = 0 gives (N − 0) % N = 0 (the borrow-clear branch, a ≥ b), and 0 < b < N gives (N − b) % N = N − b (the borrow-set WRAP branch).

theorem Reversible.modNeg_in_range {m n : ℕ} (L : ModSubLayout m n) (s : State m) (hBor : ∀ (j : ℕ), s (L.Bor j) = false) (hC : ∀ (j : ℕ), s (L.C j) = false) (hanc : s L.anc = false) {N b : ℕ} (hN : N ≤ 2 ^ n) (hNpos : 0 < N) (hNreg : regValRange L.Nreg s n = N) (hB0 : regValRange L.B s n = 0) (hSub : regValRange L.Sub s n = b) (hbN : b < N) : regValRange L.B (denote (modNeg L) s) n < N

The modular-negation output is a genuine residue in [0, N). Corollary of modNeg_correct and Nat.mod_lt.

theorem Reversible.modNeg_toffoli {m n : ℕ} (L : ModSubLayout m n) : (circuitCost (modNeg L)).toffoli = 10 * n

Derived Toffoli cost of the modular negation: 10n Toffolis, inherited verbatim from modSub_toffoli (modNeg IS modSub).

modNeg non-vacuity + harness cross-checks (b = 2, 0, 4)

Reuse the modSubLayout2 / modSubState2 witness (Fin 25, n = 3, N = 5) from ModularSub, with the minuend B set to 0. The three runs cover b = 2 ↦ 3, b = 0 ↦ 0 (the B = b zero / borrow- clear branch), and b = 4 ↦ 1 (the borrow-set WRAP branch).