── Bit-reversal

theorem addmod32_lt (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (addMod32 a b).toNat < mod32.toNat

theorem submod32_lt (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : (subMod32 a b).toNat < mod32.toNat

theorem to_mont_lt (a : UInt32) (ha : a.toNat < mod32.toNat) : (toMont a).toNat < mod32.toNat

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

theorem mont_u_toNat_left (a b : UInt32) (ha : a.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

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

theorem mont_mul_lt_of_left (a b : UInt32) (ha : a.toNat < mod32.toNat) : (montMul a b).toNat < mod32.toNat

theorem mont_mul_comm (a b : UInt32) : montMul a b = montMul b a

theorem mont_mul_lt_of_right (a b : UInt32) (hb : b.toNat < mod32.toNat) : (montMul a b).toNat < mod32.toNat

theorem bitRevLoop_bound {n : ℕ} (k i : ℕ) (v : Vector UInt32 n) (j : ℕ) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((bitRevLoop k i v j).all fun (x : UInt32) => decide (x < mod32)) = true

theorem vector_all_lt_set {n : ℕ} (v : Vector UInt32 n) (i : ℕ) (h : i < n) (x : UInt32) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (hx : x.toNat < mod32.toNat) : ((v.set i x h).all fun (x : UInt32) => decide (x < mod32)) = true

theorem vector_all_lt_getElem {n : ℕ} (v : Vector UInt32 n) (j : Fin n) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : (v.get j).toNat < mod32.toNat

theorem radix2Pass_bound {n : ℕ} (k i : ℕ) (v : Vector UInt32 n) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((radix2Pass k i v).all fun (x : UInt32) => decide (x < mod32)) = true

theorem vector_all_lt_dite_set {n : ℕ} (v : Vector UInt32 n) (idx : ℕ) (x : UInt32) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) (hx : x.toNat < mod32.toNat) : ((if h : idx < n then v.set idx x h else v).all fun (x : UInt32) => decide (x < mod32)) = true

theorem vector_get_lt_of_all {n : ℕ} (v : Vector UInt32 n) (idx : ℕ) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : (if h' : idx < n then v.get ⟨idx, h'⟩ else 0).toNat < mod32.toNat

theorem butterfly4_bound {n : ℕ} (a : Vector UInt32 n) (inverse : Bool) (roots : Vector UInt32 n) (s len i2 j2 : ℕ) (hv : (a.all fun (x : UInt32) => decide (x < mod32)) = true) : ((butterfly4 a inverse roots s len i2 j2).all fun (x : UInt32) => decide (x < mod32)) = true

theorem radix4Inner_bound {n : ℕ} (inverse : Bool) (roots : Vector UInt32 n) (s len i2 k j2 : ℕ) (v : Vector UInt32 n) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((radix4Inner inverse roots s len i2 k j2 v).all fun (x : UInt32) => decide (x < mod32)) = true

theorem radix4Middle_bound {n : ℕ} (inverse : Bool) (roots : Vector UInt32 n) (s len k b : ℕ) (v : Vector UInt32 n) (hv : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((radix4Middle inverse roots s len k b v).all fun (x : UInt32) => decide (x < mod32)) = true

theorem ntt_inplace_output_bound {m : ℕ} (v : Vector UInt32 m) (inverse : Bool) (roots : Vector UInt32 m) (hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true) : ((nttInplace v inverse roots).all fun (x : UInt32) => decide (x < mod32)) = true

All outputs of nttInplace are < mod32.

── NTT forward correctness ───────────────────────────────────────────────────

Helper lemmas decompose the proof by function: Level 1 – arithmetic primitives in ZMod Level 2 – root-table correctness (ensureRoots) Level 3 – algorithm permutation (bitRevLoop) Level 4 – full forward-NTT correctness given a correct root table The main theorem follows from levels 2 + 4.

theorem two_pow32_ne_zero_ZMod : 2 ^ 32 ≠ 0

theorem prim_root_ne_zero_ZMod : ↑primRoot.toNat ≠ 0

theorem mont_r1_ne_zero_ZMod : ↑montR1.toNat ≠ 0

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

addMod32 a b computes addition in ZMod mod32.toNat.

theorem submod32_ZMod (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : ↑(subMod32 a b).toNat = ↑a.toNat - ↑b.toNat

subMod32 a b computes subtraction in ZMod mod32.toNat.

theorem mont_mul_ZMod (a b : UInt32) (ha : a.toNat < mod32.toNat) (hb : b.toNat < mod32.toNat) : ↑(montMul a b).toNat = ↑a.toNat * ↑b.toNat * (2 ^ 32)⁻¹

montMul a b computes a · b · R⁻¹ mod p in ZMod mod32.toNat, where R = 2^32.

theorem to_mont_ZMod (a : UInt32) (ha : a.toNat < mod32.toNat) : ↑(toMont a).toNat = ↑a.toNat * ↑montR1.toNat

toMont a maps a into the Montgomery domain: it computes a · R mod p in ZMod mod32.toNat, where R = 2^32 ≡ montR1 (mod p).