Verify ML-DSA: Add length pre- and post-conditions to functions

[karthikbhargavan]

This is more of a meta-issue, but we will start with specific modules.
We need to add length pre- and post-conditions on all functions that have slice inputs.

As an illustrative example, see

libcrux/libcrux-ml-dsa/src/simd/traits.rs

Line 125 in 5689861

#[hax_lib::requires(serialized.len() == 4 || serialized.len() == 6)]

The general pattern is:

#[hax_lib::requires(input.len() == 10 && output.len == 12)]
#[hax_lib::ensures(|_| future(output).len ==  output.len)]
fn f(input: &[i32], output: &mut [u8]) {...}

The ensures clause above is a bit stupid and we will try to get rid of it, but is needed for now.