Carry-safe addition and subtraction of reduced residues

Widen both operands before adding, then reduce and truncate. The extra bit prevents wraparound before modular reduction; comparisons and selections are charged. For modular subtraction of two already reduced residues, no widening or general division is needed: three subtractions, one comparison, and one word selection suffice.

Main definitions

• addResidue a b r: modulus a, initial residue b, and increment r; return b unchanged when b ≥ a.
• subtractResidues a b d: modular difference (a - b) mod d of reduced residues a, b < d.

Main results

• toNat_addResidue: exact modular addition of two reduced residues.
• synthesis_addResidue: at most 100 * (k + 1) gates.
• toNat_subtractResidues: exact modular subtraction of two reduced residues.
• synthesis_subtractResidues: at most 140 * (k + 1) gates.

References

• Adapted from lean/Proofs/{CounterRemainders,ReducedResidue}.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

def Cslib.Circuits.Boolean.Iteration.addResidue {k : ℕ} (a b r : BitVec k) : BitVec k

Add reduced residues b and r modulo a (requiring b < a and r < a for modular-addition correctness), retaining b when b ≥ a. Retaining the carry bit is essential: two valid residues can overflow k bits.

theorem Cslib.Circuits.Boolean.Iteration.toNat_addResidue {k : ℕ} (d a b : BitVec k) (ha : a.toNat < d.toNat) (hb : b.toNat < d.toNat) : (addResidue d a b).toNat = (a.toNat + b.toNat) % d.toNat

Addition of reduced residues is exact even when their narrow-word sum overflows.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_addResidue {k n : ℕ} (s : Set (BitString n → Bool)) (a b r : BitString n → BitVec k) (ha : wordWires a ⊆ s) (hb : wordWires b ⊆ s) (hr : wordWires r ⊆ s) : Synthesis interpretation s (wordWires fun (x : BitString n) => addResidue (a x) (b x) (r x)) (100 * (k + 1))

Linear arithmetic and two selections, with a shared zero for widening.

def Cslib.Circuits.Boolean.Iteration.subtractResidues {k : ℕ} (a b d : BitVec k) : BitVec k

Subtract reduced residues a and b modulo d without general division when a < d and b < d.

theorem Cslib.Circuits.Boolean.Iteration.toNat_subtractResidues {k : ℕ} (a b d : BitVec k) (ha : a.toNat < d.toNat) (hb : b.toNat < d.toNat) : (subtractResidues a b d).toNat = (a.toNat + d.toNat - b.toNat % d.toNat) % d.toNat

Modular subtraction of reduced residues is exact without widening.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_subtractResidues {k n : ℕ} (s : Set (BitString n → Bool)) (a b d : BitString n → BitVec k) (ha : wordWires a ⊆ s) (hb : wordWires b ⊆ s) (hd : wordWires d ⊆ s) : Synthesis interpretation s (wordWires fun (x : BitString n) => subtractResidues (a x) (b x) (d x)) (140 * (k + 1))

Three shared-carry subtractions, a comparison, and one word selection.