Montgomery Reduction

Radix-generic specification and correctness lemmas for single-word Montgomery reduction. Word-specific implementations refine these results in sibling modules.

def Montgomery.reduceNat (R p negInv x : ℕ) : ℕ

Natural-number Montgomery reduction used to specify the native-word reducer.

def Montgomery.reduceNatQuotient (R p negInv x : ℕ) : ℕ

The quotient before the final conditional subtraction in Montgomery reduction.

theorem Montgomery.reduceNatQuotient_lt_two_mul (R p negInv x : ℕ) (hR : 0 < R) (hp : 0 < p) (hx : x < p * R) : reduceNatQuotient R p negInv x < 2 * p

The pre-subtraction quotient is below twice the modulus.

theorem Montgomery.reduceNat_lt (R p negInv x : ℕ) (hR : 0 < R) (hp : 0 < p) (hx : x < p * R) : reduceNat R p negInv x < p

Montgomery reduction returns a canonical representative.

theorem Montgomery.dvd_add (R p negInv : ℕ) (hR : 0 < R) (hnegInv : negInv * p % R = R - 1) (x : ℕ) : R ∣ x + x % R * negInv % R * p

The Montgomery divisibility identity: if (negInv * p) % R = R - 1 (i.e. negInv = -p⁻¹ mod R), then R ∣ x + ((x mod R)·negInv mod R)·p for every x.

theorem Montgomery.reduceNatQuotient_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R) (hnegInv : negInv * p % R = R - 1) (hRne : ↑R ≠ 0) (x : ℕ) : ↑(reduceNatQuotient R p negInv x) = ↑x * (↑R)⁻¹

The pre-subtraction quotient represents multiplication by R⁻¹ in ZMod p.

theorem Montgomery.reduceNat_cast (R p negInv : ℕ) [Fact (Nat.Prime p)] (hR : 0 < R) (hnegInv : negInv * p % R = R - 1) (hRne : ↑R ≠ 0) (x : ℕ) : ↑(reduceNat R p negInv x) = ↑x * (↑R)⁻¹

Montgomery reduction represents multiplication by R⁻¹ in ZMod p.

theorem Montgomery.natCast_inj_of_lt {p a b : ℕ} (h : ↑a = ↑b) (ha : a < p) (hb : b < p) : a = b

Two naturals below p are equal once their ZMod p casts agree.