SIMD Traits Spec and Pre-Condition Style

[karthikbhargavan]

This PR addresses #746
It needs to be merged after #776 and #780
We should also discuss and agree on the style here

As a side-effect, this PR also improves the specs and proofs for ML-DSA in the following ways:

• the specs for simd/portable/arithmetic.rs now use the add_pre, add_post, sub_pre, sub_post functions from simd/traits.rs. This reduces clutter and will help verification performance
• the proofs for simd/portable/encoding/commitment.rs are now fully automated, relying on a hand-unrolling of the loops

[franziskuskiefer]

I think here too, a transparent attribute could make things nicer. Let's look at this together.

[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

[karthikbhargavan]

With the work in cryspen/hax#1301, I've now updated this PR so it passes F*.
Let's work towards merging that hax PR next and then get back to this one (should be quick)

[karthikbhargavan]

@W95Psp @mamonet you may want to look at the styles here:

• We should aim for full automation using SMT in the style of simd/portable/encoding/commitment.rs whenever possible
• We should aim to re-use predicates like add_pre (see simd/portable/arithmetic.rs) as much as possible. (We can them make these predicates opaque if necessary, without the need to make the functions add, sub opaque.)

@W95Psp: we still need a little more work on cryspen/hax#1301 for this.
In particular, the forall predicates within the add_pre etc get compiled into valid F* but do not easily lend themselves to use in proofs. It would be better to have a custom translation of everything in Hax_lib.Prop so that these specs can be super-compact in F*.

[karthikbhargavan]

Seeing this failure (outside CI): https://github.com/cryspen/libcrux/actions/runs/13447960542

[franziskuskiefer]

Let's get this in.