[ML-KEM] Link NTT Proofs to High-Level Spec

[karthikbhargavan]

trafficstars

The arithmetic and NTT functions need to be properly linked to MLKEM.Spec rather than to localised specifications.

• [x] vector/portable/arithmetic.rs
• [x] vector/portable/ntt.rs
• [x] vector/avx2/arithmetic.rs
• [ ] vector/avx2/ntt.rs
• [ ] ntt.rs
• [ ] invert_ntt.rs
• [ ] polynomial.rs