Inverse NTT outer-loop infrastructure

These lemmas mirror the forward outer-loop lemmas (radix4Inner_single_block_correct, radix4Middle_advances_inv, outerLoop_from_inv, preprocessing_establishes_inv) but for the inverse pass (inverse = true). The key differences:

• The butterfly uses butterfly4_inverse_ZMod_combined (negated twiddles ω^{(mod64-1)/len * (len - j2)} instead of ω^{(mod64-1)/len * j2}).
• The loop invariant uses the inverse root (ωq)⁻¹ at each level and the sub-input without the Montgomery preprocessing (v[...] instead of toMont (v[...])). The ref_ntt_radix4_q* decomposition lemmas are abstract over the root, so they apply unchanged with the inverse top-level root ω_top⁻¹.

theorem butterfly4_getElem_ne_gen {N : ℕ} (inverse : Bool) (roots a : Vector UInt32 N) (s len i2 j2 : ℕ) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) (i : ℕ) (hi : i < N) (hne0 : i2 + j2 ≠ i) (hne1 : i2 + j2 + s ≠ i) (hne2 : i2 + len + j2 ≠ i) (hne3 : i2 + len + j2 + s ≠ i) : (butterfly4 a inverse roots s len i2 j2)[i] = a[i]

Structural fact: butterfly4 (any inverse flag) leaves position i unchanged when i is none of the four modified butterfly positions. Generalises butterfly4_getElem_ne.

theorem radix4Inner_getElem_ne_gen {N : ℕ} (inverse : Bool) (roots a : Vector UInt32 N) (s len i2 k j2_start hi : ℕ) (hlt : hi < N) (hbnd : ∀ (j2 : ℕ), j2_start ≤ j2 → j2 < j2_start + k → i2 + j2 < N ∧ i2 + j2 + s < N ∧ i2 + len + j2 < N ∧ i2 + len + j2 + s < N) (hne : ∀ (j2 : ℕ), j2_start ≤ j2 → j2 < j2_start + k → i2 + j2 ≠ hi ∧ i2 + j2 + s ≠ hi ∧ i2 + len + j2 ≠ hi ∧ i2 + len + j2 + s ≠ hi) : (radix4Inner inverse roots s len i2 k j2_start a)[hi] = a[hi]

Generalisation of radix4Inner_getElem_ne to any inverse flag.

theorem radix4Middle_getElem_ne_gen {N : ℕ} (inverse : Bool) (roots a : Vector UInt32 N) (s len k b_start hi : ℕ) (hlt : hi < N) (hbnd : ∀ (b : ℕ), b_start ≤ b → b < b_start + k → ∀ j2 < s, have i2 := b * 2 * len; i2 + j2 < N ∧ i2 + j2 + s < N ∧ i2 + len + j2 < N ∧ i2 + len + j2 + s < N) (hne : ∀ (b : ℕ), b_start ≤ b → b < b_start + k → ∀ j2 < s, have i2 := b * 2 * len; i2 + j2 ≠ hi ∧ i2 + j2 + s ≠ hi ∧ i2 + len + j2 ≠ hi ∧ i2 + len + j2 + s ≠ hi) : (radix4Middle inverse roots s len k b_start a)[hi] = a[hi]

Generalisation of radix4Middle_getElem_ne to any inverse flag.

theorem radix4Middle_leading_getElem_eq {N : ℕ} (inverse : Bool) (roots a : Vector UInt32 N) (s len b : ℕ) (hlen_s : 2 * s ≤ len) (hbnd : ∀ b' < b, (b' + 1) * 2 * len ≤ N) (target : ℕ) (htarget : target < N) (htarget_ge : b * 2 * len ≤ target) : (radix4Middle inverse roots s len b 0 a)[target] = a[target]

Leading b blocks of radix4Middle do not modify positions at or after b * 2 * len.

theorem radix4Middle_getElem_at_block {N : ℕ} (inverse : Bool) (roots a : Vector UInt32 N) (s len nBlocks b : ℕ) (hb : b < nBlocks) (hlen_s : 2 * s ≤ len) (hbnd : ∀ b' < nBlocks, (b' + 1) * 2 * len ≤ N) (idx : ℕ) (hidx : idx < N) (hidx_hi : idx < (b + 1) * 2 * len) : (radix4Middle inverse roots s len nBlocks 0 a)[idx] = (radix4Inner inverse roots s len (b * 2 * len) s 0 (radix4Middle inverse roots s len b 0 a))[idx]

For idx in block b (i.e. b * 2 * len ≤ idx < (b+1) * 2 * len), the full radix4Middle ... nBlocks 0 a at idx equals radix4Inner applied to block b of the leading-processed array radix4Middle ... b 0 a.

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

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

theorem twiddle_inv_exp (L j : ℕ) (hL : L ∣ mod64.toNat - 1) (hj : j ≤ L) (hLpos : 0 < L) : ↑primRoot.toNat ^ ((mod64.toNat - 1) / L * (L - j)) = (↑primRoot.toNat ^ ((mod64.toNat - 1) / L))⁻¹ ^ j

Inverse twiddle exponent identity: for L ∣ mod64-1 and j ≤ L, ω^{(mod64-1)/L * (L - j)} = ((ω^{(mod64-1)/L})⁻¹)^j where ω = primRoot.

noncomputable def ntt_sub_input_inv {m : ℕ} (n q : ℕ) (hq : q ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) : Fin (2 ^ q) → ZMod mod32.toNat

Sub-input for the inverse NTT: like ntt_sub_input but without the Montgomery toMont.

Equations

• ntt_sub_input_inv n q hq hm_eq v b j = ↑v[Fin.cast ⋯ ⟨2 ^ (n - q) * ↑j + bitRev (n - q) b, ⋯⟩].toNat

def outerLoop_inv_inverse {m : ℕ} (n q : ℕ) (hq : q ≤ n) (hm_eq : m = 2 ^ n) (v a : Vector UInt32 m) : Prop

Inverse loop invariant: like outerLoop_inv but with the inverse root (ωq)⁻¹ and the inverse sub-input (no toMont).

Equations

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

theorem ntt_sub_input_inv_block_0 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (hb : b < 2 ^ (n - q - 2)) (j : Fin (2 ^ q)) : ntt_sub_input_inv n q ⋯ hm_eq v (4 * b) j = ntt_sub_input_inv n (q + 2) hq2 hm_eq v b ⟨4 * ↑j, ⋯⟩

theorem ntt_sub_input_inv_block_1 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (j : Fin (2 ^ q)) : ntt_sub_input_inv n q ⋯ hm_eq v (4 * b + 1) j = ntt_sub_input_inv n (q + 2) hq2 hm_eq v b ⟨4 * ↑j + 2, ⋯⟩

theorem ntt_sub_input_inv_block_2 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (j : Fin (2 ^ q)) : ntt_sub_input_inv n q ⋯ hm_eq v (4 * b + 2) j = ntt_sub_input_inv n (q + 2) hq2 hm_eq v b ⟨4 * ↑j + 1, ⋯⟩

theorem ntt_sub_input_inv_block_3 {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (v : Vector UInt32 m) (b : ℕ) (hb : b < 2 ^ (n - q - 2)) (j : Fin (2 ^ q)) : ntt_sub_input_inv n q ⋯ hm_eq v (4 * b + 3) j = ntt_sub_input_inv n (q + 2) hq2 hm_eq v b ⟨4 * ↑j + 3, ⋯⟩