Constants

theorem prime_3221225473 : Nat.Prime 3221225473

theorem mod32_eq_mod : mod64.toNat = mod32.toNat

theorem prime_mod : Nat.Prime mod64.toNat

theorem MONT_R1_spec : montR1.toNat = 2 ^ 32 % mod64.toNat

theorem MONT_R2_spec : montR2.toNat = 2 ^ 64 % mod64.toNat

theorem MONT_PPRIME_spec : (mod64.toNat * montPprime.toNat + 1) % 2 ^ 32 = 0

theorem MONT_R1_ZMod : ↑montR1.toNat = 2 ^ 32

theorem PRIM_ROOT_pow_ZMod : ↑primRoot.toNat ^ (mod64.toNat - 1) = 1

theorem powmodAux_correct (mod_ : UInt64) (f : ℕ) (b e r : UInt64) (hmod : 1 < mod_.toNat) (hmod_small : mod_.toNat ≤ 2 ^ 32) (hb : b.toNat < mod_.toNat) (hr : r.toNat < mod_.toNat) (hf : e.toNat < 2 ^ f) : (powModAuxU64 mod_ f b e r).toNat = r.toNat * b.toNat ^ e.toNat % mod_.toNat

theorem powmod_correct (base exp mod_ : UInt64) (hmod : 1 < mod_.toNat) (hmod_small : mod_.toNat ≤ 2 ^ 32) : (powModU64 base exp mod_).toNat = base.toNat ^ exp.toNat % mod_.toNat

theorem prim_root_half_eq_neg_one : ↑primRoot.toNat ^ ((mod64.toNat - 1) / 2) = -1

primRoot^{(mod64-1)/2} = -1 in ZMod mod32.toNat.

theorem prim_root_PRIM_ROOT : IsPrimitiveRoot (↑primRoot.toNat) (mod64.toNat - 1)

instance instFactPrimeToNatMod32 : Fact (Nat.Prime mod32.toNat)

instance instFactPrimeToNatMod64 : Fact (Nat.Prime mod64.toNat)

Montgomery arithmetic (R = 2^32, modulus p = mod64)

theorem addmod32_correct (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (addMod32 a b).toNat = (a.toNat + b.toNat) % mod32.toNat

theorem submod32_correct (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (subMod32 a b).toNat = (a.toNat + mod32.toNat - b.toNat) % mod32.toNat

theorem mont_mul_nat_u_bound (a b : ℕ) (ha : a < mod32.toNat) (hb : b < mod32.toNat) : have T := a * b; have m := T % 2 ^ 32 * montPprime.toNat % 2 ^ 32; (T + m * mod64.toNat) / 2 ^ 32 < 2 * mod64.toNat

theorem mont_m_toNat (a b : UInt32) : ((a.toUInt64 * b.toUInt64).toUInt32 * montPprime).toNat = a.toNat * b.toNat % 2 ^ 32 * montPprime.toNat % 2 ^ 32

theorem mont_u_toNat (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : have T := a.toUInt64 * b.toUInt64; have m := T.toUInt32 * montPprime; have mp := m.toUInt64 * mod64; have lo := T.toUInt32.toUInt64 + mp.toUInt32.toUInt64; have u := T >>> 32 + mp >>> 32 + lo >>> 32; u.toNat = (a.toNat * b.toNat + m.toNat * mod64.toNat) / 2 ^ 32

def montMulNat (a b : ℕ) : ℕ

Equations

• montMulNat a b = (a * b + a * b % 2 ^ 32 * montPprime.toNat % 2 ^ 32 * mod64.toNat) / 2 ^ 32 % mod64.toNat

theorem mont_cond_sub_mod (x : UInt64) (hx : x.toNat < 2 * mod64.toNat) : (if x ≥ mod64 then (x - mod64).toUInt32 else x.toUInt32).toNat = x.toNat % mod64.toNat

theorem mont_mul_eq_nat (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (montMul a b).toNat = montMulNat a.toNat b.toNat

theorem mont_mul_nat_bound (a b : ℕ) : montMulNat a b < mod32.toNat

theorem mont_mul_nat_congr (a b : ℕ) : montMulNat a b * 2 ^ 32 % mod32.toNat = a * b % mod32.toNat

theorem mont_mul_correct (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (montMul a b).toNat < mod32.toNat ∧ (montMul a b).toNat * 2 ^ 32 % mod32.toNat = a.toNat * b.toNat % mod32.toNat

theorem to_mont_correct (a : UInt32) (ha : a.toNat < mod32.toNat) : (toMont a).toNat < mod32.toNat ∧ (toMont a).toNat * 2 ^ 32 % mod32.toNat = a.toNat * (2 ^ 64 % mod32.toNat) % mod32.toNat