ML-DSA: F*: add specs and proofs to the trait layer

[W95Psp]

Libcrux's ML-DSA delegates lower-level operations to simd::trait::Operations, a trait that defines parallel operations that can be performed by various "backends": avx2 on Intel CPUs, or portable otherwise.

In this repo, the proofs are mostly about functions below that abstraction.
The Operations trait lacks specifications, and its portable and avx2 implementations lacks glue proofs.
Some of the higher-level operations lack proofs: they rely on this Operations trait, that are often lacking specifications.

This PR aims at propagating specifications and proofs from the lower-level concrete (e.g. avx2 or portable) operations to the Operations trait, and then to the higher-level operations.

This PR (mostly by @clementblaudeau) is a start. This PR:

• adds some specifications to the trait
• adds some glue proofs between the implementations of the traits and the concrete (already proven) operations
• add a few proofs on higher-level operations, demonstrating that the proofs propagate correctly through the trait abstraction

This work is very partial, more specifications and proofs need to be added.