Making ML-KEM Extract Again

cryspen / libcrux

The formally verified crypto library for Rust

https://cryspen.com/libcrux

Apache License 2.0

81 stars 13 forks source link

Making ML-KEM Extract Again #308

Closed karthikbhargavan closed 3 months ago

karthikbhargavan commented 3 months ago

This PR does some changes to make the new ML-KEM code extract to F*. This does not lax typecheck yet.

franziskuskiefer commented 3 months ago

I checked performance and couldn't measure a difference in Rust or C. I updated the C extraction with AeneasVerif/eurydice#25 and added a small helper for build after getting tired of calling cmake directly all the time.

The hax CI needs to get fixed and we need to re-enable the extraction of this crate on CI.