Cleanup Rust annotations for Generic ML-KEM

cryspen / libcrux

The formally verified crypto library for Rust

https://cryspen.com/libcrux

Apache License 2.0

78 stars 13 forks source link

Cleanup Rust annotations for Generic ML-KEM #565

Open karthikbhargavan opened 1 week ago

karthikbhargavan commented 1 week ago

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.

[x] Ind_cca.rs (no lax functions, encapsulate/decapsulate get out of memory when verifying the post-conditions. I created #588)
[x] Ind_cpa.rs (#578)
[x] sampling.rs (1 lax function - it uses Rust_primitives.f_while_loop which doesn't support loop invariant. #570)
[x] serialize.rs (#587)
[x] matrix.rs (Mainstream)
[x] ntt.rs/invert_ntt.rss (#576)

mamonet commented 1 week ago

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 commented 1 week ago

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 commented 1 week ago

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