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

libcrux-kem/Cargo.toml

@@ -21,6 +21,9 @@ rand = { version = "0.8" }
 [features]
 tests = [] # Expose functions for testing.
 kyber = ["libcrux-ml-kem/kyber"]
+pre-verification = ["libcrux-ml-kem/pre-verification"]
+
+
 
 [dev-dependencies]
 libcrux-kem = { version = "0.0.2-pre.2", path = "./", features = ["tests"] }

libcrux-kem/src/kem.rs

@@ -484,7 +484,7 @@ impl PrivateKey {
  .map_err(|_| Error::InvalidPrivateKey)
  .map(Self::MlKem768),
  Algorithm::X25519MlKem768Draft00 => {
- let key: [u8; MlKem768PrivateKey::len() + 32] =
+ let key: [u8; MlKem768PrivateKey::size() + 32] =
  bytes.try_into().map_err(|_| Error::InvalidPrivateKey)?;
  let (xsk, ksk) = key.split_at(32);
  Ok(Self::X25519MlKem768Draft00(
@@ -790,7 +790,7 @@ impl Ct {
  .map_err(|_| Error::InvalidCiphertext)
  .map(Self::MlKem768),
  Algorithm::X25519MlKem768Draft00 => {
- let key: [u8; MlKem768Ciphertext::len() + 32] =
+ let key: [u8; MlKem768Ciphertext::size() + 32] =
  bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;
  let (xct, kct) = key.split_at(32);
  Ok(Self::X25519MlKem768Draft00(
@@ -799,9 +799,9 @@ impl Ct {
  ))
  }
  Algorithm::XWingKemDraft02 => {
- let key: [u8; MlKem768Ciphertext::len() + 32] =
+ let key: [u8; MlKem768Ciphertext::size() + 32] =
  bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;
- let (ct_m, ct_x) = key.split_at(MlKem768Ciphertext::len());
+ let (ct_m, ct_x) = key.split_at(MlKem768Ciphertext::size());
  Ok(Self::XWingKemDraft02(
  ct_m.try_into().map_err(|_| Error::InvalidCiphertext)?,
  ct_x.try_into().map_err(|_| Error::InvalidCiphertext)?,
@@ -818,6 +818,26 @@ impl Ct {
  ))
  }
  #[cfg(feature = "kyber")]
+ Algorithm::XWingKyberDraft02 => {
+ let key: [u8; MlKem768Ciphertext::len() + 32] =
+ bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;
+ let (ct_m, ct_x) = key.split_at(MlKem768Ciphertext::size());
+ Ok(Self::XWingKyberDraft02(
+ ct_m.try_into().map_err(|_| Error::InvalidCiphertext)?,
+ ct_x.try_into().map_err(|_| Error::InvalidCiphertext)?,
+ ))
+ }
+ #[cfg(feature = "kyber")]
+ Algorithm::X25519Kyber768Draft00 => {
+ let key: [u8; MlKem768Ciphertext::len() + 32] =
+ bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;
+ let (xct, kct) = key.split_at(32);
+ Ok(Self::X25519Kyber768Draft00(
+ kct.try_into().map_err(|_| Error::InvalidCiphertext)?,
+ xct.try_into().map_err(|_| Error::InvalidCiphertext)?,
+ ))
+ }
+ #[cfg(feature = "kyber")]
  Algorithm::XWingKyberDraft02 => {
  let key: [u8; MlKem768Ciphertext::len() + 32] =
  bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;

libcrux-ml-kem/Cargo.toml

@@ -27,6 +27,7 @@ libcrux-intrinsics = { version = "0.0.2-pre.2", path = "../libcrux-intrinsics" }
 # The hax config is set by the hax toolchain.
 [target.'cfg(hax)'.dependencies]
 hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax/" }
+hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax/" }
 
 [features]
 default = ["std", "mlkem512", "mlkem768", "mlkem1024"]
@@ -37,6 +38,7 @@ mlkem768 = []
 mlkem1024 = []
 std = []
 kyber = []
+pre-verification = []
 
 [dev-dependencies]
 rand = { version = "0.8" }

libcrux-ml-kem/src/cfg.rs

@@ -0,0 +1,30 @@
+/// Macro to simplify feature gating of verified code
+macro_rules! cfg_verified {
+ ($($item:item)*) => {
+ $(
+ #[cfg(not(feature = "pre-verification"))]
+ $item
+ )*
+ }
+}
+
+/// Macro to simplify `pre-verification` feature gating
+macro_rules! cfg_pre_verification {
+ ($($item:item)*) => {
+ $(
+ #[cfg(feature = "pre-verification")]
+ $item
+ )*
+ }
+}
+
+/// Macro to simplify `kyber` feature gating
+#[cfg(feature = "pre-verification")]
+macro_rules! cfg_kyber {
+ ($($item:item)*) => {
+ $(
+ #[cfg(feature = "kyber")]
+ $item
+ )*
+ }
+}

libcrux-ml-kem/src/kem.rs

@@ -0,0 +1,37 @@
+// hacspec code: don't let clippy touch it.
+#[allow(clippy::all)]
+pub mod kyber;
+
+// TODO: These functions are currently exposed simply in order to make NIST KAT
+// testing possible without an implementation of the NIST AES-CTR DRBG. Remove them
+// (and change the visibility of the exported functions to pub(crate)) the
+// moment we have an implementation of one. This is tracked by:
+// https://github.com/cryspen/libcrux/issues/36
+#[cfg(feature = "tests")]
+pub mod deterministic {
+ pub use super::kyber::kyber1024::decapsulate as kyber1024_decapsulate_derand;
+ pub use super::kyber::kyber1024::encapsulate as kyber1024_encapsulate_derand;
+ pub use super::kyber::kyber1024::generate_key_pair as kyber1024_generate_keypair_derand;
+ pub use super::kyber::kyber512::decapsulate as kyber512_decapsulate_derand;
+ pub use super::kyber::kyber512::encapsulate as kyber512_encapsulate_derand;
+ pub use super::kyber::kyber512::generate_key_pair as kyber512_generate_keypair_derand;
+ pub use super::kyber::kyber768::decapsulate as kyber768_decapsulate_derand;
+ pub use super::kyber::kyber768::encapsulate as kyber768_encapsulate_derand;
+ pub use super::kyber::kyber768::generate_key_pair as kyber768_generate_keypair_derand;
+}
+
+// use self::kyber::MlKemSharedSecret;
+// use self::kyber::{kyber1024, kyber512, kyber768};
+// pub use kyber::{
+// kyber1024::{MlKem1024Ciphertext, MlKem1024PrivateKey, MlKem1024PublicKey},
+// kyber512::{MlKem512Ciphertext, MlKem512PrivateKey, MlKem512PublicKey},
+// kyber768::{MlKem768Ciphertext, MlKem768PrivateKey, MlKem768PublicKey},
+// MlKemCiphertext, MlKemKeyPair,
+// };
+
+#[cfg(feature = "tests")]
+pub use kyber::{
+ kyber1024::validate_public_key as ml_kem1024_validate_public_key,
+ kyber512::validate_public_key as ml_kem512_validate_public_key,
+ kyber768::validate_public_key as ml_kem768_validate_public_key,
+};