def montPosInvStep (p x : UInt64) : UInt64

One Newton/Hensel refinement step for the positive Montgomery inverse.

Equations

• montPosInvStep p x = x * (2 - p * x)

def montPosInv (p : UInt64) : UInt64

Starting from the odd-modulus seed x = p, five refinement steps lift the inverse from mod 2^3 to mod 2^96 ≥ 2^64.

Equations

• montPosInv p = montPosInvStep p (montPosInvStep p (montPosInvStep p (montPosInvStep p (montPosInvStep p p))))

def montInv (p : UInt64) : UInt64

The user-facing Montgomery inverse is the negated positive inverse.

Equations

• montInv p = 0 - montPosInv p

theorem montPosInv_spec (p : UInt64) (hp_odd : p.toNat % 2 = 1) : p.toNat * (montPosInv p).toNat % UInt64.word = 1

The positive Montgomery inverse satisfies p * x ≡ 1 (mod 2^64).

theorem montInv_spec (p : UInt64) (hp_odd : p.toNat % 2 = 1) : p.toNat * (montInv p).toNat % UInt64.word = UInt64.word - 1

The negated Montgomery inverse satisfies p * p' ≡ -1 (mod 2^64).