diff --git a/libcrux-iot/ml-kem/Cargo.toml b/libcrux-iot/ml-kem/Cargo.toml index 940cda35..2b778d8a 100644 --- a/libcrux-iot/ml-kem/Cargo.toml +++ b/libcrux-iot/ml-kem/Cargo.toml @@ -26,9 +26,9 @@ bench = false # so libtest doesn't eat the arguments to criterion [dependencies] rand = { version = "0.9", optional = true } -libcrux-iot-sha3 = { path = "../sha3" , features = [ +libcrux-iot-sha3 = { path = "../sha3", features = [ "full-unroll", - "unbuffered-xof" + "unbuffered-xof", ] } hax-lib.workspace = true libcrux-secrets.workspace = true @@ -61,10 +61,10 @@ alloc = [] check-secret-independence = [ - "libcrux-secrets/check-secret-independence", - "libcrux-iot-sha3/check-secret-independence", - "libcrux-traits/check-secret-independence" - ] + "libcrux-secrets/check-secret-independence", + "libcrux-iot-sha3/check-secret-independence", + "libcrux-traits/check-secret-independence", +] # PQCP Common APIs pqcp = [] @@ -75,7 +75,19 @@ serde_json = { version = "1.0" } serde = { version = "1.0", features = ["derive"] } hex = { version = "0.4.3", features = ["serde"] } criterion = "0.5" -libcrux-kats = { workspace = true, features = [ "mlkem"] } +libcrux-kats = { workspace = true, features = ["mlkem"] } + +# Cross-spec equivalence tests against the hacspec ML-KEM +hacspec_ml_kem = { git = "https://github.com/cryspen/libcrux", rev = "a4cfb1ebf26431b2ee81f0dc19383158aaf397b7" } +proptest = "1" + +[[test]] +name = "cross_spec" +required-features = ["mlkem512", "mlkem768", "mlkem1024"] + +[[test]] +name = "cross_spec_proptests" +required-features = ["mlkem512", "mlkem768", "mlkem1024"] [[bench]] name = "ml-kem" diff --git a/libcrux-iot/ml-kem/tests/cross_spec.rs b/libcrux-iot/ml-kem/tests/cross_spec.rs new file mode 100644 index 00000000..c5b43558 --- /dev/null +++ b/libcrux-iot/ml-kem/tests/cross_spec.rs @@ -0,0 +1,304 @@ +//! Cross-spec equivalence tests between `libcrux-iot-ml-kem` and `hacspec_ml_kem`. +//! +//! These tests assert byte-identical agreement between the optimized impl and +//! the FIPS-203 hacspec reference on the IND-CCA surface (KeyGen / Encaps / +//! Decaps) at all three parameter sets. + +use hacspec_ml_kem::{ + self as spec, ML_KEM_1024, ML_KEM_1024_CT_SIZE, ML_KEM_1024_DK_PKE_SIZE, ML_KEM_1024_DK_SIZE, + ML_KEM_1024_EK_SIZE, ML_KEM_1024_J_INPUT_SIZE, ML_KEM_1024_U_SIZE, ML_KEM_1024_V_SIZE, + ML_KEM_512, ML_KEM_512_CT_SIZE, ML_KEM_512_DK_PKE_SIZE, ML_KEM_512_DK_SIZE, ML_KEM_512_EK_SIZE, + ML_KEM_512_J_INPUT_SIZE, ML_KEM_512_U_SIZE, ML_KEM_512_V_SIZE, ML_KEM_768, ML_KEM_768_CT_SIZE, + ML_KEM_768_DK_PKE_SIZE, ML_KEM_768_DK_SIZE, ML_KEM_768_EK_SIZE, ML_KEM_768_J_INPUT_SIZE, + ML_KEM_768_U_SIZE, ML_KEM_768_V_SIZE, +}; + +// --------------------------------------------------------------------------- +// Const-generic size assertions — fail fast on any drift between the impl's +// hard-coded sizes (per FIPS-203 §8 table) and the spec's exported constants. +// --------------------------------------------------------------------------- + +#[cfg(feature = "mlkem512")] +#[test] +fn size_constants_agree_512() { + use libcrux_iot_ml_kem::mlkem512::*; + assert_eq!(MlKem512PublicKey::len(), ML_KEM_512_EK_SIZE); + assert_eq!(MlKem512PrivateKey::len(), ML_KEM_512_DK_SIZE); + assert_eq!(MlKem512Ciphertext::len(), ML_KEM_512_CT_SIZE); +} + +#[cfg(feature = "mlkem768")] +#[test] +fn size_constants_agree_768() { + use libcrux_iot_ml_kem::mlkem768::*; + assert_eq!(MlKem768PublicKey::len(), ML_KEM_768_EK_SIZE); + assert_eq!(MlKem768PrivateKey::len(), ML_KEM_768_DK_SIZE); + assert_eq!(MlKem768Ciphertext::len(), ML_KEM_768_CT_SIZE); +} + +#[cfg(feature = "mlkem1024")] +#[test] +fn size_constants_agree_1024() { + use libcrux_iot_ml_kem::mlkem1024::*; + assert_eq!(MlKem1024PublicKey::len(), ML_KEM_1024_EK_SIZE); + assert_eq!(MlKem1024PrivateKey::len(), ML_KEM_1024_DK_SIZE); + assert_eq!(MlKem1024Ciphertext::len(), ML_KEM_1024_CT_SIZE); +} + +// --------------------------------------------------------------------------- +// Seed tables — deterministic vectors exercised by every variant. The last +// entry in each is the first NIST ML-KEM KAT seed (identical across the +// 512/768/1024 KAT files), so the cross-comparison also runs on a known NIST +// vector. (Agreement with the published KAT outputs themselves is checked in +// `nistkats.rs`.) +// --------------------------------------------------------------------------- + +const KEYGEN_SEEDS: &[[u8; 64]] = &[ + [0x00; 64], + [0xFF; 64], + [0xAA; 64], + { + let mut s = [0u8; 64]; + let mut i = 0usize; + while i < 64 { + s[i] = i as u8; + i += 1; + } + s + }, + // First NIST ML-KEM KAT keygen seed. + [ + 0x7c, 0x99, 0x35, 0xa0, 0xb0, 0x76, 0x94, 0xaa, 0x0c, 0x6d, 0x10, 0xe4, 0xdb, 0x6b, 0x1a, + 0xdd, 0x2f, 0xd8, 0x1a, 0x25, 0xcc, 0xb1, 0x48, 0x03, 0x2d, 0xcd, 0x73, 0x99, 0x36, 0x73, + 0x7f, 0x2d, 0x86, 0x26, 0xed, 0x79, 0xd4, 0x51, 0x14, 0x08, 0x00, 0xe0, 0x3b, 0x59, 0xb9, + 0x56, 0xf8, 0x21, 0x0e, 0x55, 0x60, 0x67, 0x40, 0x7d, 0x13, 0xdc, 0x90, 0xfa, 0x9e, 0x8b, + 0x87, 0x2b, 0xfb, 0x8f, + ], +]; +const ENCAPS_SEEDS: &[[u8; 32]] = &[ + [0x00; 32], + [0xFF; 32], + [0xCD; 32], + // First NIST ML-KEM KAT encaps seed. + [ + 0x14, 0x7c, 0x03, 0xf7, 0xa5, 0xbe, 0xbb, 0xa4, 0x06, 0xc8, 0xfa, 0xe1, 0x87, 0x4d, 0x7f, + 0x13, 0xc8, 0x0e, 0xfe, 0x79, 0xa3, 0xa9, 0xa8, 0x74, 0xcc, 0x09, 0xfe, 0x76, 0xf6, 0x99, + 0x76, 0x15, + ], +]; + +// --------------------------------------------------------------------------- +// IND-CCA byte-level cross-comparison (impl vs spec). +// +// Generated per parameter set. Each variant gets: +// 1. keygen_matches_spec — pk, sk byte-equal. +// 2. encapsulate_matches_spec — ct, ss byte-equal on a fresh keypair. +// 3. full_roundtrip_matches_spec — encaps then decaps; impl ss matches +// spec ss on both sides. +// 4. decaps_rejection_matches_spec — flipping a ct byte triggers implicit +// rejection; impl ss matches spec ss +// (i.e., both produce J(s, c')). +// --------------------------------------------------------------------------- + +macro_rules! cross_spec_tests { + ( + $mod_name:ident, + $feature:literal, + $impl_mod:path, + $k:literal, + $params:expr, + $ek:expr, $dk:expr, $dk_pke:expr, + $u:expr, $v:expr, $ct:expr, $j:expr + ) => { + #[cfg(feature = $feature)] + mod $mod_name { + use super::*; + use libcrux_secrets::{Classify, Declassify, DeclassifyRef}; + use $impl_mod as impl_mod; + + #[test] + fn keygen_matches_spec() { + for (i, randomness) in KEYGEN_SEEDS.iter().enumerate() { + let (spec_ek, spec_dk) = + spec::generate_keypair::<$k, $ek, $dk, $dk_pke>(&$params, randomness) + .unwrap_or_else(|_| { + panic!( + concat!( + stringify!($mod_name), + " spec keygen failed for seed index {}; ", + "consider replacing KEYGEN_SEEDS[{}]" + ), + i, i + ) + }); + + let kp = impl_mod::generate_key_pair((*randomness).classify()); + + assert_eq!( + &kp.public_key().as_slice()[..], + &spec_ek[..], + concat!(stringify!($mod_name), " ek mismatch (seed idx={})"), + i + ); + assert_eq!( + &kp.private_key().as_slice().declassify_ref()[..], + &spec_dk[..], + concat!(stringify!($mod_name), " dk mismatch (seed idx={})"), + i + ); + } + } + + #[test] + fn encapsulate_matches_spec() { + let keygen_rand = [1u8; 64]; + let (spec_ek, _) = + spec::generate_keypair::<$k, $ek, $dk, $dk_pke>(&$params, &keygen_rand) + .expect("spec keygen failed"); + let kp = impl_mod::generate_key_pair(keygen_rand.classify()); + + for (i, encaps_rand) in ENCAPS_SEEDS.iter().enumerate() { + let (spec_ss, spec_ct) = + spec::encapsulate::<$k, $ek, $u, $v, $ct>(&$params, &spec_ek, encaps_rand) + .expect("spec encaps failed"); + + let (impl_ct, impl_ss) = + impl_mod::encapsulate(kp.public_key(), (*encaps_rand).classify()); + + assert_eq!( + impl_ct.as_ref(), + &spec_ct[..], + concat!(stringify!($mod_name), " ct mismatch (encaps idx={})"), + i + ); + assert_eq!( + &impl_ss.declassify()[..], + &spec_ss[..], + concat!(stringify!($mod_name), " ss mismatch (encaps idx={})"), + i + ); + } + } + + #[test] + fn full_roundtrip_matches_spec() { + for (i, randomness) in KEYGEN_SEEDS.iter().enumerate() { + let encaps_rand = ENCAPS_SEEDS[i % ENCAPS_SEEDS.len()]; + + let (spec_ek, spec_dk) = + spec::generate_keypair::<$k, $ek, $dk, $dk_pke>(&$params, randomness) + .unwrap_or_else(|_| { + panic!( + concat!(stringify!($mod_name), " spec keygen failed for seed idx {}"), + i + ) + }); + let (spec_ss, spec_ct) = + spec::encapsulate::<$k, $ek, $u, $v, $ct>(&$params, &spec_ek, &encaps_rand) + .expect("spec encaps failed"); + let spec_ss_d = + spec::decapsulate::<$k, $ek, $dk, $dk_pke, $u, $v, $ct, $j>( + &$params, &spec_dk, &spec_ct, + ) + .expect("spec decaps failed"); + + let kp = impl_mod::generate_key_pair((*randomness).classify()); + let (impl_ct, impl_ss_e) = + impl_mod::encapsulate(kp.public_key(), encaps_rand.classify()); + let impl_ss_d = impl_mod::decapsulate(kp.private_key(), &impl_ct); + + assert_eq!(impl_ct.as_ref(), &spec_ct[..], "ct (seed idx={})", i); + assert_eq!(&impl_ss_e.declassify()[..], &spec_ss[..], "encaps ss"); + assert_eq!(&impl_ss_d.declassify()[..], &spec_ss_d[..], "decaps ss"); + assert_eq!( + &impl_ss_e.declassify()[..], + &impl_ss_d.declassify()[..], + "impl encaps/decaps ss differ" + ); + } + } + + #[test] + fn decaps_rejection_matches_spec() { + // Implicit rejection: tampered ct should produce J(s, c'). + // Both impl and spec implement the FIPS-203 implicit rejection; + // they should agree byte-for-byte. + let keygen_rand = KEYGEN_SEEDS[1]; // 0xFF seed + let encaps_rand = ENCAPS_SEEDS[0]; + + let (spec_ek, spec_dk) = + spec::generate_keypair::<$k, $ek, $dk, $dk_pke>(&$params, &keygen_rand) + .expect("spec keygen failed"); + let (_spec_ss, spec_ct) = + spec::encapsulate::<$k, $ek, $u, $v, $ct>(&$params, &spec_ek, &encaps_rand) + .expect("spec encaps failed"); + + let kp = impl_mod::generate_key_pair(keygen_rand.classify()); + + // Tamper one byte of the ciphertext. + let mut tampered_ct: [u8; $ct] = spec_ct; + tampered_ct[7] ^= 0xA5; + + let spec_ss_rej = + spec::decapsulate::<$k, $ek, $dk, $dk_pke, $u, $v, $ct, $j>( + &$params, &spec_dk, &tampered_ct, + ) + .expect("spec decaps (rejection branch) failed"); + + let impl_tampered_ct = tampered_ct.into(); + let impl_ss_rej = impl_mod::decapsulate(kp.private_key(), &impl_tampered_ct); + + assert_eq!( + &impl_ss_rej.declassify()[..], + &spec_ss_rej[..], + concat!(stringify!($mod_name), " implicit rejection ss mismatch") + ); + } + } + }; +} + +cross_spec_tests!( + mlkem512_cross, + "mlkem512", + libcrux_iot_ml_kem::mlkem512, + 2, + ML_KEM_512, + { ML_KEM_512_EK_SIZE }, + { ML_KEM_512_DK_SIZE }, + { ML_KEM_512_DK_PKE_SIZE }, + { ML_KEM_512_U_SIZE }, + { ML_KEM_512_V_SIZE }, + ML_KEM_512_CT_SIZE, + { ML_KEM_512_J_INPUT_SIZE } +); + +cross_spec_tests!( + mlkem768_cross, + "mlkem768", + libcrux_iot_ml_kem::mlkem768, + 3, + ML_KEM_768, + { ML_KEM_768_EK_SIZE }, + { ML_KEM_768_DK_SIZE }, + { ML_KEM_768_DK_PKE_SIZE }, + { ML_KEM_768_U_SIZE }, + { ML_KEM_768_V_SIZE }, + ML_KEM_768_CT_SIZE, + { ML_KEM_768_J_INPUT_SIZE } +); + +cross_spec_tests!( + mlkem1024_cross, + "mlkem1024", + libcrux_iot_ml_kem::mlkem1024, + 4, + ML_KEM_1024, + { ML_KEM_1024_EK_SIZE }, + { ML_KEM_1024_DK_SIZE }, + { ML_KEM_1024_DK_PKE_SIZE }, + { ML_KEM_1024_U_SIZE }, + { ML_KEM_1024_V_SIZE }, + ML_KEM_1024_CT_SIZE, + { ML_KEM_1024_J_INPUT_SIZE } +); diff --git a/libcrux-iot/ml-kem/tests/cross_spec_proptests.rs b/libcrux-iot/ml-kem/tests/cross_spec_proptests.rs new file mode 100644 index 00000000..5990a956 --- /dev/null +++ b/libcrux-iot/ml-kem/tests/cross_spec_proptests.rs @@ -0,0 +1,163 @@ +//! Property-based cross-spec tests: random seeds in × byte equality out. +//! +//! Complements the deterministic table in `cross_spec.rs`. 32 cases per +//! variant by default — keep the per-variant budget under a few seconds so +//! the suite stays usable on every `cargo test`. Tune via +//! `PROPTEST_CASES` env var for deeper smoke runs. +//! +//! Unlucky-seed handling: `hacspec_ml_kem::generate_keypair` can return +//! `Err(BadRejectionSamplingRandomnessError)`. We `prop_assume!` past such +//! seeds. + +use proptest::prelude::*; + +use hacspec_ml_kem::{ + self as spec, ML_KEM_1024, ML_KEM_1024_CT_SIZE, ML_KEM_1024_DK_PKE_SIZE, ML_KEM_1024_DK_SIZE, + ML_KEM_1024_EK_SIZE, ML_KEM_1024_J_INPUT_SIZE, ML_KEM_1024_U_SIZE, ML_KEM_1024_V_SIZE, + ML_KEM_512, ML_KEM_512_CT_SIZE, ML_KEM_512_DK_PKE_SIZE, ML_KEM_512_DK_SIZE, ML_KEM_512_EK_SIZE, + ML_KEM_512_J_INPUT_SIZE, ML_KEM_512_U_SIZE, ML_KEM_512_V_SIZE, ML_KEM_768, ML_KEM_768_CT_SIZE, + ML_KEM_768_DK_PKE_SIZE, ML_KEM_768_DK_SIZE, ML_KEM_768_EK_SIZE, ML_KEM_768_J_INPUT_SIZE, + ML_KEM_768_U_SIZE, ML_KEM_768_V_SIZE, +}; +use libcrux_secrets::{Classify, Declassify, DeclassifyRef}; + +/// Strategy: arbitrary 64-byte arrays for KeyGen randomness. +fn keygen_seed_strategy() -> impl Strategy { + proptest::collection::vec(any::(), 64..=64).prop_map(|v| { + let mut a = [0u8; 64]; + a.copy_from_slice(&v); + a + }) +} + +/// Strategy: arbitrary 32-byte arrays for Encaps randomness. +fn encaps_seed_strategy() -> impl Strategy { + proptest::collection::vec(any::(), 32..=32).prop_map(|v| { + let mut a = [0u8; 32]; + a.copy_from_slice(&v); + a + }) +} + +proptest! { + #![proptest_config(ProptestConfig { + cases: 32, + .. ProptestConfig::default() + })] + + /// ML-KEM-512: spec ↔ impl agreement across KeyGen → Encaps → Decaps. + #[cfg(feature = "mlkem512")] + #[test] + fn mlkem512_roundtrip_matches_spec( + keygen_seed in keygen_seed_strategy(), + encaps_seed in encaps_seed_strategy(), + ) { + let spec_kp = spec::generate_keypair::< + 2, ML_KEM_512_EK_SIZE, ML_KEM_512_DK_SIZE, ML_KEM_512_DK_PKE_SIZE, + >(&ML_KEM_512, &keygen_seed); + + // Skip seeds the spec rejects. + prop_assume!(spec_kp.is_ok()); + let (spec_ek, spec_dk) = spec_kp.unwrap(); + + let kp = libcrux_iot_ml_kem::mlkem512::generate_key_pair(keygen_seed.classify()); + + prop_assert_eq!(&kp.public_key().as_slice()[..], &spec_ek[..]); + prop_assert_eq!(&kp.private_key().as_slice().declassify_ref()[..], &spec_dk[..]); + + let (spec_ss, spec_ct) = spec::encapsulate::< + 2, ML_KEM_512_EK_SIZE, ML_KEM_512_U_SIZE, ML_KEM_512_V_SIZE, ML_KEM_512_CT_SIZE, + >(&ML_KEM_512, &spec_ek, &encaps_seed) + .expect("encaps on a successfully-generated key should not fail"); + + let (impl_ct, impl_ss_e) = + libcrux_iot_ml_kem::mlkem512::encapsulate(kp.public_key(), encaps_seed.classify()); + prop_assert_eq!(impl_ct.as_ref(), &spec_ct[..]); + prop_assert_eq!(&impl_ss_e.declassify()[..], &spec_ss[..]); + + let spec_ss_d = spec::decapsulate::< + 2, ML_KEM_512_EK_SIZE, ML_KEM_512_DK_SIZE, ML_KEM_512_DK_PKE_SIZE, + ML_KEM_512_U_SIZE, ML_KEM_512_V_SIZE, ML_KEM_512_CT_SIZE, ML_KEM_512_J_INPUT_SIZE, + >(&ML_KEM_512, &spec_dk, &spec_ct) + .expect("spec decaps on a valid (ek, ct) should not fail"); + + let impl_ss_d = libcrux_iot_ml_kem::mlkem512::decapsulate(kp.private_key(), &impl_ct); + prop_assert_eq!(&impl_ss_d.declassify()[..], &spec_ss_d[..]); + } + + /// ML-KEM-768: spec ↔ impl agreement across KeyGen → Encaps → Decaps. + #[cfg(feature = "mlkem768")] + #[test] + fn mlkem768_roundtrip_matches_spec( + keygen_seed in keygen_seed_strategy(), + encaps_seed in encaps_seed_strategy(), + ) { + let spec_kp = spec::generate_keypair::< + 3, ML_KEM_768_EK_SIZE, ML_KEM_768_DK_SIZE, ML_KEM_768_DK_PKE_SIZE, + >(&ML_KEM_768, &keygen_seed); + prop_assume!(spec_kp.is_ok()); + let (spec_ek, spec_dk) = spec_kp.unwrap(); + + let kp = libcrux_iot_ml_kem::mlkem768::generate_key_pair(keygen_seed.classify()); + + prop_assert_eq!(&kp.public_key().as_slice()[..], &spec_ek[..]); + prop_assert_eq!(&kp.private_key().as_slice().declassify_ref()[..], &spec_dk[..]); + + let (spec_ss, spec_ct) = spec::encapsulate::< + 3, ML_KEM_768_EK_SIZE, ML_KEM_768_U_SIZE, ML_KEM_768_V_SIZE, ML_KEM_768_CT_SIZE, + >(&ML_KEM_768, &spec_ek, &encaps_seed) + .expect("encaps on a successfully-generated key should not fail"); + + let (impl_ct, impl_ss_e) = + libcrux_iot_ml_kem::mlkem768::encapsulate(kp.public_key(), encaps_seed.classify()); + prop_assert_eq!(impl_ct.as_ref(), &spec_ct[..]); + prop_assert_eq!(&impl_ss_e.declassify()[..], &spec_ss[..]); + + let spec_ss_d = spec::decapsulate::< + 3, ML_KEM_768_EK_SIZE, ML_KEM_768_DK_SIZE, ML_KEM_768_DK_PKE_SIZE, + ML_KEM_768_U_SIZE, ML_KEM_768_V_SIZE, ML_KEM_768_CT_SIZE, ML_KEM_768_J_INPUT_SIZE, + >(&ML_KEM_768, &spec_dk, &spec_ct) + .expect("spec decaps on a valid (ek, ct) should not fail"); + + let impl_ss_d = libcrux_iot_ml_kem::mlkem768::decapsulate(kp.private_key(), &impl_ct); + prop_assert_eq!(&impl_ss_d.declassify()[..], &spec_ss_d[..]); + } + + /// ML-KEM-1024: spec ↔ impl agreement across KeyGen → Encaps → Decaps. + #[cfg(feature = "mlkem1024")] + #[test] + fn mlkem1024_roundtrip_matches_spec( + keygen_seed in keygen_seed_strategy(), + encaps_seed in encaps_seed_strategy(), + ) { + let spec_kp = spec::generate_keypair::< + 4, ML_KEM_1024_EK_SIZE, ML_KEM_1024_DK_SIZE, ML_KEM_1024_DK_PKE_SIZE, + >(&ML_KEM_1024, &keygen_seed); + prop_assume!(spec_kp.is_ok()); + let (spec_ek, spec_dk) = spec_kp.unwrap(); + + let kp = libcrux_iot_ml_kem::mlkem1024::generate_key_pair(keygen_seed.classify()); + + prop_assert_eq!(&kp.public_key().as_slice()[..], &spec_ek[..]); + prop_assert_eq!(&kp.private_key().as_slice().declassify_ref()[..], &spec_dk[..]); + + let (spec_ss, spec_ct) = spec::encapsulate::< + 4, ML_KEM_1024_EK_SIZE, ML_KEM_1024_U_SIZE, ML_KEM_1024_V_SIZE, ML_KEM_1024_CT_SIZE, + >(&ML_KEM_1024, &spec_ek, &encaps_seed) + .expect("encaps on a successfully-generated key should not fail"); + + let (impl_ct, impl_ss_e) = + libcrux_iot_ml_kem::mlkem1024::encapsulate(kp.public_key(), encaps_seed.classify()); + prop_assert_eq!(impl_ct.as_ref(), &spec_ct[..]); + prop_assert_eq!(&impl_ss_e.declassify()[..], &spec_ss[..]); + + let spec_ss_d = spec::decapsulate::< + 4, ML_KEM_1024_EK_SIZE, ML_KEM_1024_DK_SIZE, ML_KEM_1024_DK_PKE_SIZE, + ML_KEM_1024_U_SIZE, ML_KEM_1024_V_SIZE, ML_KEM_1024_CT_SIZE, ML_KEM_1024_J_INPUT_SIZE, + >(&ML_KEM_1024, &spec_dk, &spec_ct) + .expect("spec decaps on a valid (ek, ct) should not fail"); + + let impl_ss_d = libcrux_iot_ml_kem::mlkem1024::decapsulate(kp.private_key(), &impl_ct); + prop_assert_eq!(&impl_ss_d.declassify()[..], &spec_ss_d[..]); + } +} diff --git a/libcrux-iot/sha3/Cargo.toml b/libcrux-iot/sha3/Cargo.toml index 2101f939..d12921aa 100644 --- a/libcrux-iot/sha3/Cargo.toml +++ b/libcrux-iot/sha3/Cargo.toml @@ -47,7 +47,7 @@ hex = "0.4.3" rand = "0.8.5" cavp.workspace = true #{ version = "0.0.2-beta.2", path = "../cavp" } pretty_env_logger = "0.5.0" -hacspec_sha3 = { git = "https://github.com/cryspen/libcrux.git", rev = "b313344" } +hacspec_sha3 = { git = "https://github.com/cryspen/libcrux.git", rev = "a4cfb1ebf26431b2ee81f0dc19383158aaf397b7" } proptest = "1.2.0" libcrux-kats = { workspace = true, features = ["sha3"] } diff --git a/libcrux-iot/sha3/hax_aeneas.py b/libcrux-iot/sha3/hax_aeneas.py index 91fbf96d..4f71b074 100755 --- a/libcrux-iot/sha3/hax_aeneas.py +++ b/libcrux-iot/sha3/hax_aeneas.py @@ -6,7 +6,7 @@ import sys from pathlib import Path -HAX_VERSION = "1f85fc13b9967080cc657863e2000ba5d4aa8647" +HAX_VERSION = "ffdf432705d409b62ec025d253a340234b59766f" AENEAS_VERSION = "8d2077c" @@ -14,6 +14,9 @@ def check_version(cmd: list[str], name: str, expected: str) -> None: result = subprocess.run(cmd, capture_output=True, text=True) output = result.stdout + result.stderr if expected not in output: + if os.environ.get("SKIP_VERSION_CHECK") == "1": + print(f"warning: version mismatch for {name} (expected {expected!r}); continuing because SKIP_VERSION_CHECK=1", file=sys.stderr) + return print(f"Version mismatch for {name}: expected {expected!r} in output:\n{output}", file=sys.stderr) sys.exit(1) diff --git a/libcrux-iot/sha3/proofs/aeneas-lean/LibcruxIotSha3/README.md b/libcrux-iot/sha3/proofs/aeneas-lean/LibcruxIotSha3/README.md index 9a805306..05d71bec 100644 --- a/libcrux-iot/sha3/proofs/aeneas-lean/LibcruxIotSha3/README.md +++ b/libcrux-iot/sha3/proofs/aeneas-lean/LibcruxIotSha3/README.md @@ -188,13 +188,17 @@ The resulting Lean files are: - For running the proofs: - Lean 4 toolchain `leanprover/lean4:v4.30.0-rc2` (pinned in `lean-toolchain`). - - Hacspec-style implementation from https://github.com/cryspen/libcrux at commit `b313344` + - Hacspec-style implementation from https://github.com/cryspen/libcrux at commit `a4cfb1ebf26431b2ee81f0dc19383158aaf397b7` - For extraction: - - Hax at commit `1f85fc13b9967080cc657863e2000ba5d4aa8647` + - Hax at commit `ffdf432705d409b62ec025d253a340234b59766f` (not publicly available yet, https://github.com/cryspen/hax-evit) with the corresponding charon/aeneas versions: - Charon at https://github.com/AeneasVerif/charon/releases/tag/nightly-2026.06.02 - Aeneas at https://github.com/cryspen/aeneas/releases/tag/nightly-2026.06.04 + — note: the `aeneas-pin` file in hax-evit at this commit names tag + `nightly-2026.06.03`, but commit `8d2077c` (the SHA the binary + must report) actually ships in `nightly-2026.06.04`. Use the + `06.04` release. ### Building diff --git a/libcrux-iot/sha3/proofs/aeneas-lean/lake-manifest.json b/libcrux-iot/sha3/proofs/aeneas-lean/lake-manifest.json index 450b3130..0052e608 100644 --- a/libcrux-iot/sha3/proofs/aeneas-lean/lake-manifest.json +++ b/libcrux-iot/sha3/proofs/aeneas-lean/lake-manifest.json @@ -5,32 +5,22 @@ "type": "git", "subDir": "specs/sha3/proofs/aeneas-lean", "scope": "", - "rev": "b31334479b26d90eef412292f85610dca95acd13", + "rev": "a4cfb1ebf26431b2ee81f0dc19383158aaf397b7", "name": "HacspecSha3", "manifestFile": "lake-manifest.json", - "inputRev": "b313344", + "inputRev": "a4cfb1ebf26431b2ee81f0dc19383158aaf397b7", "inherited": false, "configFile": "lakefile.toml"}, {"url": "ssh://git@github.com/cryspen/hax-evit", "type": "git", "subDir": "hax-lib/proof-libs/aeneas-lean", "scope": "", - "rev": "1f85fc13b9967080cc657863e2000ba5d4aa8647", + "rev": "ffdf432705d409b62ec025d253a340234b59766f", "name": "Hax", "manifestFile": "lake-manifest.json", - "inputRev": "1f85fc13b9967080cc657863e2000ba5d4aa8647", + "inputRev": "ffdf432705d409b62ec025d253a340234b59766f", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/cryspen/rust-core-models", - "type": "git", - "subDir": "lean", - "scope": "", - "rev": "c22543b20ae4cca02ae9839f4142208db6a2bfee", - "name": "«rust-core-models»", - "manifestFile": "lake-manifest.json", - "inputRev": "c22543b20ae4cca02ae9839f4142208db6a2bfee", - "inherited": true, - "configFile": "lakefile.toml"}, {"url": "https://github.com/cryspen/aeneas", "type": "git", "subDir": "backends/lean", diff --git a/libcrux-iot/sha3/proofs/aeneas-lean/lakefile.toml b/libcrux-iot/sha3/proofs/aeneas-lean/lakefile.toml index be4ab9f0..365c3d08 100644 --- a/libcrux-iot/sha3/proofs/aeneas-lean/lakefile.toml +++ b/libcrux-iot/sha3/proofs/aeneas-lean/lakefile.toml @@ -9,9 +9,9 @@ globs = ["LibcruxIotSha3", "LibcruxIotSha3.+"] [[require]] name = "Hax" git = { url = "ssh://git@github.com/cryspen/hax-evit", subDir = "hax-lib/proof-libs/aeneas-lean" } -rev = "1f85fc13b9967080cc657863e2000ba5d4aa8647" +rev = "ffdf432705d409b62ec025d253a340234b59766f" [[require]] name = "HacspecSha3" git = { url = "https://github.com/cryspen/libcrux", subDir = "specs/sha3/proofs/aeneas-lean" } -rev = "b313344" +rev = "a4cfb1ebf26431b2ee81f0dc19383158aaf397b7" diff --git a/libcrux-iot/sha3/src/lib.rs b/libcrux-iot/sha3/src/lib.rs index 8643a476..18c4db52 100644 --- a/libcrux-iot/sha3/src/lib.rs +++ b/libcrux-iot/sha3/src/lib.rs @@ -361,7 +361,7 @@ pub mod incremental { /// An unbuffered XOF state. #[derive(Clone, Copy)] - #[cfg_attr(not(eurydice), derive(Debug))] + #[cfg_attr(not(any(eurydice, hax_backend_lean)), derive(Debug))] #[cfg(feature = "unbuffered-xof")] pub struct UnbufferedXofState { state: crate::state::KeccakState,