7.5. Montgomery reduction🔗

Montgomery reduction is the alternative single-word reducer used when many modular multiplications share one odd modulus. It works in the Montgomery domain (residues scaled by R), where reduction becomes a multiply-add-shift with no trial division at all. As with Barrett, a Nat-level model states the computation before the machine-word encoding.

def

montgomeryReduceNat (p p' T : Nat) : Nat
montgomeryReduceNat (p p' T : Nat) : Nat

Nat-level Montgomery reduction with radix R = 2^64.

The model is proved to compute the reduced residue exactly and to land below the modulus, given the precomputed inverse word p' and an odd modulus below the radix.

theorem

montgomeryReduceNat_eq_mod {p p' T : Nat} (hp_pos : 0 < p)
  (hp_lt : p < UInt64.word)
  (hpp' : p * p' % UInt64.word = UInt64.word - 1)
  (hT : T < p * UInt64.word) :
  montgomeryReduceNat p p' T * UInt64.word % p = T % p
montgomeryReduceNat_eq_mod {p p' T : Nat}
  (hp_pos : 0 < p)
  (hp_lt : p < UInt64.word)
  (hpp' :
    p * p' % UInt64.word =
      UInt64.word - 1)
  (hT : T < p * UInt64.word) :
  montgomeryReduceNat p p' T *
        UInt64.word %
      p =
    T % p

Montgomery reduction computes a residue congruent to T * R⁻¹ modulo p.

theorem

montgomeryReduceNat_lt {p p' T : Nat} (hp_pos : 0 < p)
  (hp_lt : p < UInt64.word)
  (hpp' : p * p' % UInt64.word = UInt64.word - 1)
  (hT : T < p * UInt64.word) : montgomeryReduceNat p p' T < p
montgomeryReduceNat_lt {p p' T : Nat}
  (hp_pos : 0 < p)
  (hp_lt : p < UInt64.word)
  (hpp' :
    p * p' % UInt64.word =
      UInt64.word - 1)
  (hT : T < p * UInt64.word) :
  montgomeryReduceNat p p' T < p

Montgomery reduction lands in the canonical residue interval [0, p).

The executable side carries the machine-word Montgomery parameters in a MontCtx. montgomeryReduce consumes a two-word product (Thi, Tlo) and returns one reduced residue, proved to match the Nat model and to stay canonical.

structure

MontCtx (p : UInt64) : Type
MontCtx (p : UInt64) : Type

Runtime Montgomery context for an odd UInt64 modulus.

Constructor

MontCtx.mkCtx

Fields

p_odd : p % 2 = 1

The modulus is odd.

p' : UInt64

The Montgomery inverse word, satisfying p' · p ≡ -1 (mod R).

p'_eq : self.p'.toNat * p.toNat % UInt64.word = UInt64.word - 1

The inverse field satisfies p' · p ≡ R - 1 (mod R).

r2 : UInt64

The constant R² mod p, used to convert a residue into Montgomery form.

r2_eq : self.r2.toNat = UInt64.word * UInt64.word % p.toNat

The r2 field is exactly R² mod p.

def

montgomeryReduce {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64) :
  UInt64
montgomeryReduce {p : UInt64}
  (ctx : MontCtx p) (Thi Tlo : UInt64) :
  UInt64

Executable Montgomery reduction (classically REDC) from a two-word product (Thi, Tlo) encoded in base 2^64.

theorem

toNat_montgomeryReduce {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64)
  (hT : Tlo.toNat + Thi.toNat * UInt64.word < p.toNat * UInt64.word) :
  (montgomeryReduce ctx Thi Tlo).toNat =
    montgomeryReduceNat p.toNat ctx.p'.toNat
      (Tlo.toNat + Thi.toNat * UInt64.word)
toNat_montgomeryReduce {p : UInt64}
  (ctx : MontCtx p) (Thi Tlo : UInt64)
  (hT :
    Tlo.toNat + Thi.toNat * UInt64.word <
      p.toNat * UInt64.word) :
  (montgomeryReduce ctx Thi Tlo).toNat =
    montgomeryReduceNat p.toNat
      ctx.p'.toNat
      (Tlo.toNat +
        Thi.toNat * UInt64.word)

The executable REDC routine agrees with the Nat-level specification.

theorem

montgomeryReduce_lt {p : UInt64} (ctx : MontCtx p) (Thi Tlo : UInt64)
  (hT : Tlo.toNat + Thi.toNat * UInt64.word < p.toNat * UInt64.word) :
  montgomeryReduce ctx Thi Tlo < p
montgomeryReduce_lt {p : UInt64}
  (ctx : MontCtx p) (Thi Tlo : UInt64)
  (hT :
    Tlo.toNat + Thi.toNat * UInt64.word <
      p.toNat * UInt64.word) :
  montgomeryReduce ctx Thi Tlo < p

Executable REDC returns a canonical residue below the modulus.