Verify ML-DSA: set up SIMD scaffolding

[karthikbhargavan]

• Verify constants.rs
• Verify portable/vector_type.rs
• Verify avx2/vector_type.rs
• Verify simd/traits.rs

[karthikbhargavan]

Initial Analysis

I did a review of these files, and I believe this should take half a day.
The main work will be on defining the pre and post conditions for traits.rs.
The rest of these should be trivial.

[karthikbhargavan]

This is currently blocked by cryspen/hax#1266
Working around to make progress.

[karthikbhargavan]

This PR is currently blocked by some issues with the translations of attributes.
In particular, in the treatment of bool vs Prop.
https://github.com/cryspen/hax-evit/issues/11

[franziskuskiefer]

@karthikbhargavan what's the state here? https://github.com/cryspen/hax-evit/issues/12 got merged.

[karthikbhargavan]

Addressed in #788