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

[karthikbhargavan]

trafficstars

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 https://github.com/cryspen/libcrux/blob/568986148e094fb3d0944c0768a4dba15b0f6a47/libcrux-ml-dsa/src/simd/traits.rs#L125

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.

• [ ] src/hash_functions.rs
• [ ] src/matrix.rs
• [ ] src/ml_dsa_44.rs
• [ ] src/ml_dsa_65.rs
• [ ] src/ml_dsa_87.rs
• [ ] src/ml_dsa_generic/instantiations/avx2.rs
• [ ] src/ml_dsa_generic/multiplexing.rs
• [ ] src/ml_dsa_generic/instantiations.rs
• [ ] src/ml_dsa_generic.rs
• [ ] src/polynomial.rs
• [ ] src/pre_hash.rs
• [ ] src/sample.rs
• [ ] src/samplex4.rs
• [ ] src/types.rs

[karthikbhargavan]

A grep for the patter "& [" yields: src/arithmetic.rs src/encoding/commitment.rs src/encoding/error.rs src/encoding/t1.rs src/encoding/verification_key.rs src/encoding/t0.rs src/encoding/gamma1.rs src/encoding/signing_key.rs src/encoding/signature.rs src/hash_functions.rs src/matrix.rs src/ml_dsa_44.rs src/ml_dsa_65.rs src/ml_dsa_87.rs src/ml_dsa_generic/instantiations/avx2.rs src/ml_dsa_generic/multiplexing.rs src/ml_dsa_generic/instantiations.rs src/ml_dsa_generic.rs src/polynomial.rs src/pre_hash.rs src/sample.rs src/samplex4.rs src/simd/avx2/rejection_sample/less_than_field_modulus.rs src/simd/avx2/rejection_sample/less_than_eta.rs src/simd/avx2/encoding/error.rs src/simd/avx2/encoding/t1.rs src/simd/avx2/encoding/t0.rs src/simd/avx2/encoding/gamma1.rs src/simd/avx2/vector_type.rs src/simd/portable/encoding/error.rs src/simd/portable/encoding/t1.rs src/simd/portable/encoding/t0.rs src/simd/portable/encoding/gamma1.rs src/simd/portable/vector_type.rs src/simd/portable/sample.rs src/simd/tests.rs src/simd/traits.rs src/simd/avx2.rs src/simd/portable.rs src/types.rs

A grep for the pattern "&mut [u8]" yields:

src/encoding/commitment.rs src/encoding/error.rs src/encoding/t1.rs src/encoding/verification_key.rs src/encoding/t0.rs src/encoding/gamma1.rs src/encoding/signing_key.rs src/encoding/signature.rs src/hash_functions.rs src/ml_dsa_generic/instantiations/avx2.rs src/ml_dsa_generic/multiplexing.rs src/ml_dsa_generic/instantiations.rs src/ml_dsa_generic.rs src/pre_hash.rs src/simd/avx2/encoding/commitment.rs src/simd/avx2/encoding/error.rs src/simd/avx2/encoding/t1.rs src/simd/avx2/encoding/t0.rs src/simd/avx2/encoding/gamma1.rs src/simd/portable/encoding/commitment.rs src/simd/portable/encoding/error.rs src/simd/portable/encoding/t1.rs src/simd/portable/encoding/t0.rs src/simd/portable/encoding/gamma1.rs src/simd/traits.rs src/simd/avx2.rs src/simd/portable.rs src/types.rs

These would be files to start with.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[karthikbhargavan]

We have done this for some modules, for others, will do this on a best-effort basis, and am closing this for now.