Make verified ML-KEM available in libcrux-ml-kem

[jschneider-bensch]

This PR integrates the version of ML-KEM into libcrux-ml-kem that was verified and previously lived in the kem module of libcrux. I've also introduced a pre-verification feature gate in libcrux-ml-kem and libcrux-kem for code that is not verified, yet.

Fixes #326

[franziskuskiefer]

waiting for the code updates, please re-request review.

[franziskuskiefer]

lgtm with a few nits and one bigger issue below.

Looks like I didn't feature guard tests, example etc. in #333. Now things fail when running without default features.

You can run cargo hack test --each-feature (excluding things like simd128 on x64 machines with --exclude-features) to see what happens. In particular cargo test --no-default-features seems to fail already. We should get that on CI.

So broken combinations are at least

• --no-default-features
• --no-default-features --features kyber

Especially the second one should work.

But we can do that in a follow up if you want.

[jschneider-bensch]

I added more feature gates, so cargo test --no-default-features at least should work now.

fixing gh

[franziskuskiefer]

I did a pass and fixed all the remaining issues (that I found, there may be more).
I also added more docs and regenerated F* and C code. I think this is good to go.