search

cryspen / libcrux

The formally verified crypto library for Rust
https://cryspen.com/libcrux
Apache License 2.0
81 stars 13 forks source link

Make verified ML-KEM available in `libcrux-ml-kem` #329

Closed jschneider-bensch closed 3 months ago

jschneider-bensch commented 3 months ago

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

jschneider-bensch commented 3 months ago

I really didn't want to mess with the verified code beyond the minimum to make it work, hence it generates a lot of warnings about unused things, some of which are actually not used (unpacked...), and others only used in tests. This could be nicer for sure, I'd just like to know if the general approach to the feature makes sense before spending more time on making it nice.

franziskuskiefer commented 3 months ago

a lot of warnings about unused things

You can do re-export everything (pub use crate::kem::kyber::kyber768::*; etc) to get rid of most of these. The rest we should probably just drop.

You have a bunch of #[cfg(feature = "pre-verification")] in there. Can you instead move everything into a module and and re-export everything on the top level again to make the code look nicer? It would be nice to keep the changes to a minimum and easily observable on the rest of the code.

And really, this is temporary for a month or two. So I'm not too concerned about it. But there shouldn't be unexpected things like warnings.

jschneider-bensch commented 3 months ago

Introducing feature gating helper macros makes the presentation much cleaner! The only small wrinkle is the kem module which can't be feature gated by macro, otherwise this happens 

error: macro-expanded `macro_export` macros from the current crate cannot be referred to by absolute paths
  --> libcrux-ml-kem/src/kem/kyber/serialize.rs:9:5
   |
9  | use crate::cloop;
   |     ^^^^^^^^^^^^
   |
   = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
   = note: for more information, see issue #52234 <https://github.com/rust-lang/rust/issues/52234>
jschneider-bensch commented 3 months ago

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