ML-DSA: verify portable `ntt`

[W95Psp]

[W95Psp]

@karthikbhargavan and I inverstigated a bit this.

Notes:

• the indirection via the values field of Coefficients will probably makes us hit https://github.com/FStarLang/FStar/issues/3800 to a certain degree. Would be much nicer to have IndexMut on coefficients. (see https://github.com/cryspen/hax/issues/644#issuecomment-2090950211)
• we should add an interpretations for Rust arrays (or F* sequences) as lists, defining lifts and simplification lemmas just as we did for bitvec<->int_vec
• then we can see e.g. ntt_at_layer_0 as a circuit
• it is less clear for outer_3_plus: there is a loop, and we need montgomery_multiply_by_constant, subtract and add to be circuits already

[karthikbhargavan]

Can likely be improved, but addressed for now in #989