Inverse NTT preprocessing invariant #
preprocessing_establishes_inv_inverse: after bitRevLoop (and optional radix2Pass),
the outerLoop_inv_inverse holds at the starting level start_q.
This mirrors preprocessing_establishes_inv but for the inverse path:
no toMont is applied, and the invariant uses ntt_sub_input_inv.
theorem
preprocessing_establishes_inv_inverse
{m : ℕ}
(n : ℕ)
(hm_eq : m = 2 ^ n)
(h_dvd : m ∣ mod64.toNat - 1)
(v : Vector UInt32 m)
(hv_bound : (v.all fun (x : UInt32) => decide (x < mod32)) = true)
:
have a1 := bitRevLoop (m - 1) 0 v 0;
have parity := nttInplace.go 64 m 0 &&& 1 != 0;
have a_in := if parity = true then radix2Pass (m / 2) 0 a1 else a1;
have start_q := if parity = true then 1 else 0;
∃ (hle : start_q ≤ n), outerLoop_inv_inverse n start_q hle hm_eq v a_in