── Root table

theorem rootsInner_montPow (wm : UInt32) (halfLen : ℕ) {n : ℕ} (k j : ℕ) (v : Vector UInt32 n) (hj : j ≤ k) (hn : halfLen + k < n) : (rootsInner wm halfLen k 0 v)[halfLen + j] = montPow v[halfLen] wm j

theorem rootsInner_preserves_below (wm : UInt32) (halfLen : ℕ) {n : ℕ} (k i pos : ℕ) (v : Vector UInt32 n) (hpos : pos < n) (h : pos ≤ halfLen + i) : (rootsInner wm halfLen k i v)[pos] = v[pos]

theorem montPow_spec (wm : UInt32) (w j : ℕ) (hwm : wm.toNat = w * montR1.toNat % mod32.toNat) : (montPow montR1 wm j).toNat = w ^ j * montR1.toNat % mod32.toNat

theorem nat_toUInt64_faithful (m : ℕ) (hm : m < 2 ^ 64) : m.toUInt64.toNat = m

theorem pow2_toUInt64_le_nat (s n : ℕ) (hs : s < 63) (h : 2 ^ (s + 1) ≤ n) : ¬(2 ^ (s + 1)).toUInt64.toNat > n

ℕ-variant: (2^(s+1)).toUInt64.toNat = 2^(s+1) when s < 63, so ≤ n in ℕ.

theorem pow2_toUInt64_halfLen (s : ℕ) (hs : s < 63) : ((2 ^ (s + 1)).toUInt64 / 2).toNat = 2 ^ s

theorem pow2_toUInt64_shift (s : ℕ) (_hs : s < 63) : (2 ^ (s + 1)).toUInt64 <<< 1 = (2 ^ (s + 2)).toUInt64

theorem outer_preserves_target (n : ℕ) (hN : 0 < n) (v : Vector UInt32 n) (s f K j : ℕ) (hs_gt_K : s > K) (hj : j < 2 ^ K) (hKn : 2 ^ K + j < n) (hs_lt : s < 64) : (ensureRoots.outer n v (2 ^ (s + 1)).toUInt64 hN f)[2 ^ K + j] = v[2 ^ K + j]

theorem to_mont_nat_helper (x a : ℕ) (hx_lt : x < mod32.toNat) (h_cong : x * 2 ^ 32 % mod32.toNat = a * (2 ^ 64 % mod32.toNat) % mod32.toNat) : x = a * montR1.toNat % mod32.toNat

toMont a computes a.toNat * montR1.toNat % mod32.toNat at the Nat level.

theorem to_mont_nat (a : UInt32) (ha : a.toNat < mod32.toNat) : (toMont a).toNat = a.toNat * montR1.toNat % mod32.toNat

theorem UInt64_toUInt32_toNat (x : UInt64) (hx : x.toNat < 2 ^ 32) : x.toUInt32.toNat = x.toNat

Casting a UInt64 value below 2^32 to UInt32 and back preserves the Nat value.

theorem ensure_roots_base_case (n : ℕ) (hN : 0 < n) (v : Vector UInt32 n) (K j f : ℕ) (hlen_K : 2 ^ (K + 1) ≤ n) (hj : j < 2 ^ K) (hK63 : K < 63) (h_half : ((2 ^ (K + 1)).toUInt64 / 2).toNat < n) (hlt : 2 ^ K + j < n) : have wm := toMont (powModU64 primRoot ((mod64 - 1) / (2 ^ (K + 1)).toUInt64) mod64).toUInt32; have vr := rootsInner wm ((2 ^ (K + 1)).toUInt64 / 2).toNat (((2 ^ (K + 1)).toUInt64 / 2).toNat - 1) 0 (v.set ((2 ^ (K + 1)).toUInt64 / 2).toNat montR1 h_half); have res := ensureRoots.outer n vr (2 ^ (K + 2)).toUInt64 hN f; res[2 ^ K + j].toNat = (primRoot.toNat ^ ((mod64.toNat - 1) / 2 ^ (K + 1)) % mod64.toNat) ^ j * montR1.toNat % mod64.toNat

The s = K base step of ensure_roots_outer_inv: after one outer-loop iteration at level K, followed by any number of further iterations, position 2^K+j holds (w^j · montR1) % mod64.

theorem to_mont_mont_r1 (a : UInt32) (ha : a.toNat < mod32.toNat) : (toMont a).toNat = a.toNat * montR1.toNat % mod32.toNat

theorem ensure_roots_outer_inv (n : ℕ) (hN : 0 < n) (v : Vector UInt32 n) (s f K j : ℕ) (hlen_K : 2 ^ (K + 1) ≤ n) (hj : j < 2 ^ K) (hsK : s ≤ K) (hf : K < s + f) (hK63 : K < 63) : have w := primRoot.toNat ^ ((mod64.toNat - 1) / 2 ^ (K + 1)) % mod64.toNat; have hlt := ⋯; (ensureRoots.outer n v (2 ^ (s + 1)).toUInt64 hN f)[2 ^ K + j].toNat = w ^ j * montR1.toNat % mod64.toNat

theorem ensure_roots_outer_geom (n : ℕ) (hN : 0 < n) (K j : ℕ) (hK63 : K < 63) (hlen : 2 ^ (K + 1) ≤ n) (hj : j < 2 ^ K) : have w := primRoot.toNat ^ ((mod64.toNat - 1) / 2 ^ (K + 1)) % mod64.toNat; have hlt := ⋯; (ensureRoots.outer n (Vector.replicate n 0) 2 hN 64)[2 ^ K + j].toNat = w ^ j * montR1.toNat % mod64.toNat

theorem ensure_roots_spec (n k j : ℕ) (hk63 : k < 63) (hlen_le : 2 ^ (k + 1) ≤ n) (hj : j < 2 ^ k) : have w := primRoot.toNat ^ ((mod64.toNat - 1) / 2 ^ (k + 1)) % mod64.toNat; (have this := ⋯; (ensureRoots n)[2 ^ k + j].toNat) = w ^ j * montR1.toNat % mod64.toNat