Cleanup Rust annotations for Generic ML-KEM

[karthikbhargavan]

The proofs for generic ML-KEM need to be made consistent with the latest Vector Trait annotations
and should be optimized so they do not run for memory and can be verified on CI.

• Ind_cca.rs (no lax functions, encapsulate/decapsulate get out of memory when verifying the post-conditions. I created Split encapsulate/decapsulate functions in Ind_cca.rs  #588)
• Ind_cpa.rs (Make generic ind_cpa module panic-free #578)
• sampling.rs (1 lax function - it uses Rust_primitives.f_while_loop which doesn't support loop invariant. Make functions in sampling.rs panic-free #570)
• serialize.rs (Add conditions for generic compress and serialize functions #587)
• matrix.rs (Mainstream)
• ntt.rs/invert_ntt.rss (Make ntt panic free #576)

[mamonet]

I started a WIP branch for this issue https://github.com/cryspen/libcrux/tree/dev-generic-cleanup
Currently, it marks certain function in sampling.rs and serialize.rs as lax as they don't have proper pre-conditions yet (e.g. the functions in serialize need to adapt the new conditions on vector trait). The branch also aims to figure a solution for functions in
Ind_cca.rs and Ind_cpa.rs that get out of memory.

[mamonet]

I pushed changes to dev-generic-cleanup branch that make sample_from_uniform_distribution_next and sample_from_binomial_distribution_2 functions panic-free in generic sampling.rs module, based on hax fold-step-boundary branch. I will create a PR once all functions in sampling.rs are panic-free (except for sample_from_xof that utilizes Rust_primitives.f_while_loop).

[mamonet]

I fixed the bug in generic polynomail.rs that blocks verifying the extracted code of constant ZETAS_TIMES_MONTGOMERY_R and I removed Libcrux_ml_kem.Polynomial.fst from ADMIT_MODULES in Makefile

[franziskuskiefer]

@karthikbhargavan @mamonet Looks like everything is ticked off here. Is there still something open or can this be closed?

[mamonet]

I need to merge dev to these PRs and do some modifications to get them work.

[karthikbhargavan]

lets tick this off once the prs are merged today and then continue afterwards

[mamonet]

This issue is completed!