Reversible modular subtraction — the verified value primitive (a, b) ↦ (a − b mod N, b) (ECDLP Phase 2, Stage S6.3e-1)

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

This module verifies the modular-subtraction VALUE primitive a − b mod N over bit registers, the one genuinely-missing field-operation primitive the elliptic-curve point formulas need (both the a = 0 doubling 9X⁴ − 8XY² and the addition use field subtraction). It mirrors the verified ModAdd development (fullAdder → rippleCirc → rippleCirc_correct) step-for-step, with a borrow chain in place of the carry chain, and reuses the S6.3a conditional-add-back-on-a-flag structure (cRippleCirc controlled on the borrow flag) for the modular fix.

modSub L = rippleSub L.subStep ++ cRippleCirc L.fixStep

• Subtract step rippleSub L.subStep (minuend register B holds a, subtrahend Sub holds b read-only, fresh borrow chain Bor): rippleSub_correct writes B ← (a − b) mod 2ⁿ and the borrow-out wire Bor n becomes the comparison flag decide (a < b) (rippleSub_borrowout), preserving Sub = b.
• Modular fix cRippleCirc L.fixStep (Nreg preset to N, same B, fresh carry chain C, control = the borrow flag Bor n, fresh ancilla anc): conditional add-back of N, gated on the borrow a < b — exactly the S6.3a controlled-add structure. The borrow flag is already the a < b predicate (no X-flip needed, unlike modReduce where the carry-out is N ≤ x and must be flipped).

The two branches (verified in modSub_correct):

• a ≥ b (borrow clear): subtract step value (a − b) mod 2ⁿ = a − b, no add-back; a − b < N since a < N. So B = a − b = (a + N − b) mod N.
• a < b (borrow set): subtract step value (a − b) mod 2ⁿ = a + 2ⁿ − b (no underflow wrap into range, a − b is computed mod 2ⁿ); then + N mod 2ⁿ = (a + 2ⁿ − b + N) mod 2ⁿ. Since a − b + N < N ≤ 2ⁿ (as a < b ⇒ a + N − b < N), a + 2ⁿ − b + N = 2ⁿ + (a + N − b) wraps to a + N − b = (a + N − b) mod N.

The headline is stated as (a + N − b) % N to stay in ℕ-truncated-subtraction-safe form: for a, b < N this is exactly the integer (a − b) mod N (both branches above land on it).

The subtractor (route (i): fullSub borrow chain, mirroring fullAdder)

fullSub mw sw bin bout := [X mw] ++ fullAdder sw mw bin bout ++ [X mw]: borrow-subtract is "invert minuend, add, invert result". The full adder on (sw, mw, bin, bout) after flipping mw computes into mw the bit sw ⊕ ¬mw ⊕ bin = ¬(mw ⊕ sw ⊕ bin) and into bout the carry majority(sw, ¬mw, bin) = majority(¬mw, sw, bin) = bout (the borrow-out), so a final X mw yields diff = mw ⊕ sw ⊕ bin. Verified by decide over all inputs (fullSub_correct), exactly like fullAdder_correct.

Carve line (what this is, and is NOT)

This is the value-correct modular-subtraction atom in the fresh-ancilla model. ℕ / mod N bit arithmetic; NO field / group semantics are in play here. It is a field-operation PRIMITIVE: the full SLP → circuit assembly of the EC point operation (routing all field ops — add / sub / mul / double / const-mult — and deriving M as an exhibited-circuit count) is the later S6.3e stages; nsmul (const-mult) / neg compose from {modAdd, modDouble, modSub}. This module does NOT claim the point operation.

Named residue (same fresh-ancilla model as modAdd): the borrow chain Bor, the comparison flag Bor n, and the fix-step carry chain C are left dirty after modSub; correctness holds because the layout supplies fresh wires per use (modSub_correct requires Bor / C / anc initialised false). In-place reuse across many subtractions needs carry/borrow-clean adders — which rippleCirc / rippleSub / cRippleCirc do NOT provide. That is the genuine remaining cleanup work, NOT built here.

Honest cost

modSub_toffoli derives 10n Toffolis from the exhibited gate list: subtract step 2n (rippleSub, two Toffolis per fullSub slice — the two X mw framing gates are free) + fix step 8n (cRippleCirc_toffoli, the controlled add-back), composed through cost_comp_toffoli_count. Same 10n as the single-step modReduce (S6.3a): a verified compare-and-conditional-add.

The full-subtractor gadget (the verified primitive)

def Reversible.fullSub {n : ℕ} (mw sw bin bout : Fin n) : Circuit n

The six-gate full subtractor on wires mw sw bin bout (with bout initialised false): mw ← mw ⊕ sw ⊕ bin (difference bit, in place into the minuend wire mw), bout ← majority(¬mw, sw, bin) (borrow-out), sw/bin unchanged.

Borrow-subtract is "invert the minuend, add, invert the result": fullSub flips mw, runs fullAdder sw mw bin bout (which writes the sum sw ⊕ ¬mw ⊕ bin into mw and the carry majority(sw, ¬mw, bin) into bout), then flips mw back. Correctness on the concrete layout is fullSub_correct.

Equations

• Reversible.fullSub mw sw bin bout = [Reversible.Gate.X mw] ++ Reversible.fullAdder sw mw bin bout ++ [Reversible.Gate.X mw]

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

Full-subtractor correctness — genuine all-inputs coverage. On the concrete State 4 layout (wires 0,1,2,3 = mw, sw, bin, bout), with bout initialised false, the gadget computes the difference bit on mw (wire 0), the borrow-out on bout (wire 3), and preserves sw (wire 1) and bin (wire 2). Proved by decide over the finite State 4 (16 inputs, each with s 3 = false).

theorem Reversible.fullSub_apply_of_ne {n : ℕ} {mw sw bin bout w : Fin n} (hmw : w ≠ mw) (hsw : w ≠ sw) (hbin : w ≠ bin) (hbout : w ≠ bout) (s : State n) : denote (fullSub mw sw bin bout) s w = s w

Frame lemma for the gadget. A wire distinct from all four of mw, sw, bin, bout is untouched by fullSub (every gate's wires lie in {mw, sw, bin, bout}). Lets the borrow chain lift the slice over a register.

theorem Reversible.fullSub_correct_general {n : ℕ} {mw sw bin bout : Fin n} (hmwsw : mw ≠ sw) (hmwbin : mw ≠ bin) (hboutmw : bout ≠ mw) (hboutsw : bout ≠ sw) (hboutbin : bout ≠ bin) (hswbin : sw ≠ bin) {s : State n} (hb0 : s bout = false) : denote (fullSub mw sw bin bout) s mw = (s mw ^^ s sw ^^ s bin) ∧ denote (fullSub mw sw bin bout) s bout = majority (!s mw) (s sw) (s bin) ∧ denote (fullSub mw sw bin bout) s sw = s sw ∧ denote (fullSub mw sw bin bout) s bin = s bin

Full-subtractor correctness, general Fin n wires. For pairwise-distinct wires mw, sw, bin, bout with bout initialised false, the gadget writes the difference bit to mw, the borrow-out to bout, and preserves sw and bin — over arbitrary Fin n (not just the concrete State 4 of fullSub_correct). This is the slice the borrow chain iterates.

Derived cost of the gadget

theorem Reversible.fullSub_toffoli {n : ℕ} (mw sw bin bout : Fin n) : (circuitCost (fullSub mw sw bin bout)).toffoli = 2

Derived cost of the full subtractor (from the gate list, via circuitCost): two Toffolis, two CNOTs — the same as fullAdder (the two X framing gates are free). Read off [X, CCX, CX, CCX, CX, X].

The full-subtractor arithmetic identity on ℕ

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

The full-subtractor arithmetic identity on ℕ. The minuend bit plus twice the borrow-out equals the difference bit plus the subtrahend bit plus the borrow-in — the per-slice borrow fact the chain accumulates (the subtraction analogue of fulladder_nat).

The borrow chain (general n): B ← (a − b) mod 2ⁿ, borrow flag = a < b

A SubLayout lays out the minuend register B (overwritten with (a − b) mod 2ⁿ), the subtrahend register Sub (read-only b), and a borrow chain Bor (Bor 0 the input borrow, Bor n the output borrow = the comparison flag). Pairwise disjoint, bounded-injective — exactly the RippleLayout discipline.

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

A borrow-chain subtractor layout on m wires for n-bit registers: minuend register B (overwritten with the difference), subtrahend Sub (read-only), and a borrow chain Bor. The three images are pairwise disjoint and each is injective on its used index range. The injectivity fields are bounded (< n for registers, < n + 1 for the borrow chain) — an unbounded ℕ → Fin m injectivity field is uninhabitable and would make the theorem vacuous.

• B : ℕ → Fin m

  Minuend register (holds a, overwritten with (a − b) mod 2ⁿ).

• Sub : ℕ → Fin m

  Subtrahend register (holds b, read-only).

• Bor : ℕ → Fin m

  Borrow chain (Bor i = borrow into bit i; Bor n = the a < b flag).

• hBSub (i j : ℕ) : self.B i ≠ self.Sub j
• hBBor (i j : ℕ) : self.B i ≠ self.Bor j
• hSubBor (i j : ℕ) : self.Sub i ≠ self.Bor j
• hBinj (i j : ℕ) : i < n → j < n → self.B i = self.B j → i = j
• hSubinj (i j : ℕ) : i < n → j < n → self.Sub i = self.Sub j → i = j
• hBorinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Bor i = self.Bor j → i = j

def Reversible.subSlice {n m : ℕ} (L : SubLayout m n) (i : ℕ) : Circuit m

One borrow slice: a full subtractor on (B i, Sub i, Bor i, Bor (i+1)).

Equations

• Reversible.subSlice L i = Reversible.fullSub (L.B i) (L.Sub i) (L.Bor i) (L.Bor (i + 1))

def Reversible.subPrefix {n m : ℕ} (L : SubLayout m n) (k : ℕ) : Circuit m

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

Equations

• Reversible.subPrefix L k = List.flatMap (Reversible.subSlice L) (List.range k)

def Reversible.rippleSub {n m : ℕ} (L : SubLayout m n) : Circuit m

The full borrow-chain subtractor: all n slices.

Equations

• Reversible.rippleSub L = Reversible.subPrefix L n

theorem Reversible.denote_subPrefix_succ {n m : ℕ} (L : SubLayout m n) (k : ℕ) (s : State m) : denote (subPrefix L (k + 1)) s = denote (subSlice L k) (denote (subPrefix L k) s)

theorem Reversible.rippleSub_invariant {n m : ℕ} (L : SubLayout m n) (s : State m) (hBor0 : ∀ (j : ℕ), s (L.Bor j) = false) (k : ℕ) : k ≤ n → regValRange L.B s k + (denote (subPrefix L k) s (L.Bor k)).toNat * 2 ^ k = regValRange L.B (denote (subPrefix L k) s) k + regValRange L.Sub s k ∧ (∀ j < n, denote (subPrefix L k) s (L.Sub j) = s (L.Sub j)) ∧ (∀ (j : ℕ), k ≤ j → j < n → denote (subPrefix L k) s (L.B j) = s (L.B j)) ∧ ∀ (j : ℕ), k < j → j < n + 1 → denote (subPrefix L k) s (L.Bor j) = s (L.Bor j)

The borrow-chain invariant. After the first k slices: register B's low k bits plus the borrow into bit k scaled by 2^k equal the low-k minuend value plus the low-k subtrahend value (P1, the borrow recurrence B + 2^k·borrow = a + Sub over the low k bits); the subtrahend Sub is untouched (P2); the unprocessed high bits of B (P4) and the unset high borrows (P5) are preserved. By induction on k, lifting fullSub_correct_general through the frame lemma fullSub_apply_of_ne.

theorem Reversible.rippleSub_correct {n m : ℕ} (L : SubLayout m n) (s : State m) (hBor0 : ∀ (j : ℕ), s (L.Bor j) = false) : regValRange L.B (denote (rippleSub L) s) n = (regValRange L.B s n + 2 ^ n - regValRange L.Sub s n) % 2 ^ n

Borrow-chain subtractor correctness. For a disjoint-wire layout with all borrows initialised false, the ripple subtractor leaves the minuend register B holding (a − b) mod 2ⁿ, where a = B, b = Sub. The borrow recurrence, derived from the exhibited circuit rippleSub.

theorem Reversible.rippleSub_borrowout {n m : ℕ} (L : SubLayout m n) (s : State m) (hBor0 : ∀ (j : ℕ), s (L.Bor j) = false) : denote (rippleSub L) s (L.Bor n) = decide (regValRange L.B s n < regValRange L.Sub s n)

The borrow-out is the comparison flag. For a disjoint-wire layout with all borrows initialised false, the ripple subtractor's output borrow wire Bor n holds decide (a < b) — it is set exactly when the subtraction underflows, i.e. when the minuend a is below the subtrahend b. Read off rippleSub_invariant (clause P1) together with regValRange_lt. This is the comparison primitive for the modular fix: add N back iff the borrow is set.

Modular subtraction: the borrow chain + conditional add-back of N

A ModSubLayout bundles the subtract step's SubLayout (minuend B, subtrahend Sub, borrow chain Bor) and the fix step's controlled-add sub-data (constant register Nreg preset to N, fix carry chain C, shared ancilla anc), with the control being the borrow flag Bor n (= a < b). The fix step is the S6.3a conditional-add-back structure (cRippleCirc), gated directly on the borrow (no X-flip, since the borrow is already the a < b predicate that triggers the add-back).

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

A single-step modular-subtraction layout on Fin m for n-bit registers. Bundles:

• B — the minuend (holds a, overwritten with a − b mod N);
• Sub — the subtrahend (holds b, read-only, preserved);
• Bor — the borrow chain; Bor n is the comparison flag (= a < b), the control of the fix;
• Nreg — the fix constant register (preset to N), with a fresh carry chain C;
• anc — the shared clean ancilla for the controlled add-back.

The fields are pure wire geometry (pairwise disjointness + per-range bounded injectivity), mirroring the SubLayout / ModReduceLayout discipline. The injectivity fields are bounded (< n for registers, < n + 1 for chains) — an unbounded ℕ → Fin m injectivity field is uninhabitable and would make the theorem vacuous.

• B : ℕ → Fin m

  Minuend register: holds a, overwritten with a − b mod N.

• Sub : ℕ → Fin m

  Subtrahend register: holds b, read-only (preserved).

• Bor : ℕ → Fin m

  Borrow chain; Bor n is the comparison flag (= a < b).

• Nreg : ℕ → Fin m

  Fix-step constant register (preset to N).

• C : ℕ → Fin m

  Fix-step carry chain (distinct from the borrow chain).

• anc : Fin m

  Shared clean ancilla for the controlled add-back.

• hBSub (i j : ℕ) : self.B i ≠ self.Sub j
• hBBor (i j : ℕ) : self.B i ≠ self.Bor j
• hSubBor (i j : ℕ) : self.Sub i ≠ self.Bor j
• hBinj (i j : ℕ) : i < n → j < n → self.B i = self.B j → i = j
• hSubinj (i j : ℕ) : i < n → j < n → self.Sub i = self.Sub j → i = j
• hBorinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.Bor i = self.Bor j → i = j
• hBNreg (i j : ℕ) : self.B i ≠ self.Nreg j
• hBC (i j : ℕ) : self.B i ≠ self.C j
• hNregC (i j : ℕ) : self.Nreg i ≠ self.C j
• hNreginj (i j : ℕ) : i < n → j < n → self.Nreg i = self.Nreg j → i = j
• hCinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.C i = self.C j → i = j
• hflagNreg (j : ℕ) : self.Bor n ≠ self.Nreg j
• hflagB (j : ℕ) : self.Bor n ≠ self.B j
• hflagC (j : ℕ) : self.Bor n ≠ self.C j
• hflaganc : self.Bor n ≠ self.anc
• hancNreg (j : ℕ) : self.anc ≠ self.Nreg j
• hancB (j : ℕ) : self.anc ≠ self.B j
• hancC (j : ℕ) : self.anc ≠ self.C j
• hNregSub (i j : ℕ) : self.Nreg i ≠ self.Sub j
• hNregBor (i j : ℕ) : self.Nreg i ≠ self.Bor j
• hCSub (i j : ℕ) : self.C i ≠ self.Sub j
• hCBor (i j : ℕ) : self.C i ≠ self.Bor j
• hancSub (j : ℕ) : self.anc ≠ self.Sub j
• hancBor (j : ℕ) : self.anc ≠ self.Bor j
• hSubNreg (i j : ℕ) : self.Sub i ≠ self.Nreg j
• hSubC (i j : ℕ) : self.Sub i ≠ self.C j
• hSubanc (j : ℕ) : self.Sub j ≠ self.anc

def Reversible.ModSubLayout.subStep {n m : ℕ} (L : ModSubLayout m n) : SubLayout m n

The subtract step as a SubLayout: minuend B + subtrahend Sub + borrow chain Bor.

Equations

• L.subStep = { B := L.B, Sub := L.Sub, Bor := L.Bor, hBSub := ⋯, hBBor := ⋯, hSubBor := ⋯, hBinj := ⋯, hSubinj := ⋯, hBorinj := ⋯ }

def Reversible.ModSubLayout.fixStep {n m : ℕ} (L : ModSubLayout m n) : CRippleLayout m n

The fix step as a CRippleLayout: constant Nreg + data B + carry chain C, controlled on the borrow flag Bor n, with the shared ancilla.

Equations

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

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

The modular-subtraction circuit. Borrow-chain subtractor (rippleSub, producing the a < b borrow flag) followed by the S6.3a controlled add-back of N gated on the flag (cRippleCirc).

Equations

• Reversible.modSub L = Reversible.rippleSub L.subStep ++ Reversible.cRippleCirc L.fixStep

Frame: fix-step inputs survive the subtract step

rippleSub L.subStep touches only the wires {B k, Sub k, Bor k} (the slices are fullSub (B k) (Sub k) (Bor k) (Bor (k+1))). The fix step's Nreg, C, and anc are disjoint from those, so their values pass through the subtract step unchanged.

theorem Reversible.rippleSub_subStep_preserves {n m : ℕ} {L : ModSubLayout m n} (s : State m) (w : Fin m) (hB : ∀ (k : ℕ), w ≠ L.B k) (hS : ∀ (k : ℕ), w ≠ L.Sub k) (hBor : ∀ (k : ℕ), w ≠ L.Bor k) : denote (rippleSub L.subStep) s w = s w

Generic subtract-step frame. A wire w with w ≠ B k, w ≠ Sub k, w ≠ Bor k for all k is left unchanged by rippleSub L.subStep.

theorem Reversible.modSub_subStep_preserves_Nreg {n m : ℕ} {L : ModSubLayout m n} (s : State m) (j : ℕ) : denote (rippleSub L.subStep) s (L.Nreg j) = s (L.Nreg j)

After the subtract step, Nreg is unchanged on every wire.

theorem Reversible.modSub_subStep_preserves_C {n m : ℕ} {L : ModSubLayout m n} (s : State m) (j : ℕ) : denote (rippleSub L.subStep) s (L.C j) = s (L.C j)

After the subtract step, the fix carry chain C is unchanged on every wire.

theorem Reversible.modSub_subStep_preserves_anc {n m : ℕ} {L : ModSubLayout m n} (s : State m) : denote (rippleSub L.subStep) s L.anc = s L.anc

After the subtract step, the shared ancilla anc is unchanged.

Frame: the subtrahend Sub survives the fix step

cRippleCirc L.fixStep touches only {Nreg, B, C, anc, Bor n}. Since Sub is disjoint from all of these, the subtrahend passes through the fix step unchanged.

theorem Reversible.cRippleCirc_fixStep_preserves_Sub {n m : ℕ} {L : ModSubLayout m n} (s : State m) (j : ℕ) : denote (cRippleCirc L.fixStep) s (L.Sub j) = s (L.Sub j)

Subtrahend frame through the fix step. Sub j is untouched by cRippleCirc L.fixStep.

Value correctness, both branches

theorem Reversible.modSub_correct {n m : ℕ} (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 a b : ℕ} (hN : N ≤ 2 ^ n) (hNreg : regValRange L.Nreg s n = N) (hB : regValRange L.B s n = a) (hSub : regValRange L.Sub s n = b) (haN : a < N) (hbN : b < N) : regValRange L.B (denote (modSub L) s) n = (a + N - b) % N

The complete single-step modular subtraction — both branches, verified from the exhibited circuit. For a disjoint-wire ModSubLayout with the borrow chain Bor, the fix carry chain C, and the ancilla anc all initialised false, the constant register Nreg preset to N, minuend B holding a, subtrahend Sub holding b, with a < N, b < N, N ≤ 2ⁿ: the circuit modSub L leaves B holding (a + N − b) mod N (= a − b mod N).

Proof. The subtract step (rippleSub_correct) writes (a + 2ⁿ − b) mod 2ⁿ to B and sets the borrow flag Bor n = decide (a < b) (rippleSub_borrowout), preserving Sub = b and — via the frame lemmas — Nreg = N, C = false, anc = false. The fix step (cRippleCirc_correct) adds N back iff the flag is set. The two branches:

• a ≥ b (flag clear): subtract value (a + 2ⁿ − b) mod 2ⁿ = a − b (b ≤ a < 2ⁿ); no add-back, and a − b < N (a < N), so B = a − b = (a + N − b) mod N.
• a < b (flag set): subtract value (a + 2ⁿ − b) mod 2ⁿ = a + 2ⁿ − b (no wrap, a + 2ⁿ − b < 2ⁿ), then + N mod 2ⁿ = (a + 2ⁿ + N − b) mod 2ⁿ = a + N − b (a + N − b < N ≤ 2ⁿ), which is (a + N − b) mod N.

theorem Reversible.modSub_preserves_subtrahend {n m : ℕ} (L : ModSubLayout m n) (s : State m) (hBor : ∀ (j : ℕ), s (L.Bor j) = false) {b : ℕ} (hSub : regValRange L.Sub s n = b) : regValRange L.Sub (denote (modSub L) s) n = b

The subtrahend register is intact. modSub L leaves Sub holding b (read-only). The subtract step preserves Sub (P2 of the borrow invariant) and the fix step is disjoint from Sub.

theorem Reversible.modSub_in_range {n m : ℕ} (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 a b : ℕ} (hN : N ≤ 2 ^ n) (hNreg : regValRange L.Nreg s n = N) (hB : regValRange L.B s n = a) (hSub : regValRange L.Sub s n = b) (haN : a < N) (hbN : b < N) : regValRange L.B (denote (modSub L) s) n < N

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

Derived cost

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

Derived Toffoli cost of the modular subtractor: 10n Toffolis, from the exhibited gate list. Subtract step 2n (rippleSub, two Toffolis per fullSub slice — the framing Xs are free) + fix step 8n (cRippleCirc_toffoli, the controlled add-back), composed through cost_comp_toffoli_count. Same 10n as the single-step modReduce (S6.3a): a verified compare-and-conditional-add.

Non-vacuity witness

A concrete 3-bit modular-subtraction layout on Fin 25:

• minuend B → {0,1,2}, subtrahend Sub → {3,4,5}, borrow chain Bor → {6,7,8,9},
• fix constant Nreg → {10,11,12}, fix carry chain C → {13,14,15,16}, ancilla 17.

(n = 3 is taken to share the modAdd witness scale; N = 5 needs N ≤ 2³ = 8.) This exhibits that ModSubLayout is inhabited (the bounded-injectivity bundle is satisfiable), so the headlines are not vacuously quantified. The concrete runs below subtract modulo N = 5 at fully-specified input states, covering both branches: a = 3, b = 1 ↦ (3 − 1) mod 5 = 2 (the a ≥ b no-wrap branch), a = 1, b = 3 ↦ (1 − 3) mod 5 = 3 (the a < b WRAP branch, the load-bearing case), and a = b = 2 ↦ 0.

def Reversible.modSubLayout2 : ModSubLayout 25 3

A concrete 3-bit modular-subtraction layout on Fin 25.

Equations

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

Interface lemmas (CONVENTIONS §9.1, F1): the wire assignments of the concrete layout, one lemma per field.

theorem Reversible.modSubLayout2_B (i : ℕ) : modSubLayout2.B i = if i = 0 then 0 else if i = 1 then 1 else 2

modSubLayout2's minuend wires.

theorem Reversible.modSubLayout2_Sub (i : ℕ) : modSubLayout2.Sub i = if i = 0 then 3 else if i = 1 then 4 else 5

modSubLayout2's subtrahend wires.

theorem Reversible.modSubLayout2_Bor (i : ℕ) : modSubLayout2.Bor i = if i = 0 then 6 else if i = 1 then 7 else if i = 2 then 8 else 9

modSubLayout2's borrow-chain wires.

theorem Reversible.modSubLayout2_Nreg (i : ℕ) : modSubLayout2.Nreg i = if i = 0 then 10 else if i = 1 then 11 else 12

modSubLayout2's fix-step constant-register wires.

theorem Reversible.modSubLayout2_C (i : ℕ) : modSubLayout2.C i = if i = 0 then 13 else if i = 1 then 14 else if i = 2 then 15 else 16

modSubLayout2's fix-step carry-chain wires.

theorem Reversible.modSubLayout2_anc : modSubLayout2.anc = 17

modSubLayout2's ancilla wire.

def Reversible.modSubState2 (a0 a1 a2 b0 b1 b2 : Bool) : State 25

Concrete input state for n = 3, N = 5: minuend B = a (wires 0,1,2), subtrahend Sub = b (wires 3,4,5), Nreg = 5 (wires 10,12, bits 0 and 2), all borrows / fix carries / ancilla false. Parameterised by the data bits of a and b.

Equations

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

theorem Reversible.modSubState2_apply (a0 a1 a2 b0 b1 b2 : Bool) (w : Fin 25) : modSubState2 a0 a1 a2 b0 b1 b2 w = if w = 0 then a0 else if w = 1 then a1 else if w = 2 then a2 else if w = 3 then b0 else if w = 4 then b1 else if w = 5 then b2 else if w = 10 then true else if w = 12 then true else false

The concrete input state at a wire, as its defining case chain (interface lemma, §9.1).

theorem Reversible.modSubState2_pre (a0 a1 a2 b0 b1 b2 : Bool) : (∀ (j : ℕ), modSubState2 a0 a1 a2 b0 b1 b2 (modSubLayout2.Bor j) = false) ∧ (∀ (j : ℕ), modSubState2 a0 a1 a2 b0 b1 b2 (modSubLayout2.C j) = false) ∧ modSubState2 a0 a1 a2 b0 b1 b2 modSubLayout2.anc = false ∧ regValRange modSubLayout2.Nreg (modSubState2 a0 a1 a2 b0 b1 b2) 3 = 5

The hypotheses of modSub_correct hold at modSubState2 (borrows / carries / ancilla clear, Nreg = 5), for any data bits. The regValRange register-value preconditions are concrete sums, discharged by decide.

Harness cross-check (runArr / regValRangeArr, audited SOUND)

Fast Array Bool-backed runs of the full modSub circuit (the Fin 25 denote blows up under #eval via lazy Function.update re-reads; runArr is O(gates)). Each printed number is certified equal to the regValRange (denote …) of modSub_correct by regValRangeArr_eq. Both branches are covered: a ≥ b (no wrap) and a < b (the load-bearing WRAP, where the borrow flag must fire the add-back).