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

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

Equations

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

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

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

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

theorem montgomeryReduceNat_quotient_lt_two_p {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) : (T + T % UInt64.word * p' % UInt64.word * p) / UInt64.word < 2 * p

The unreduced Montgomery quotient is always below 2p, so one subtraction is enough to normalize the result.