Specs for ML-DSA

libcrux-ml-dsa/Cargo.toml

@@ -43,6 +43,8 @@ serde_json = { version = "1.0" }
 serde = { version = "1.0", features = ["derive"] }
 criterion = "0.8"
 libcrux-kats = { workspace = true, features = ["mldsa"] }
+hacspec_ml_dsa = { path = "../specs/ml-dsa" }
+rand_chacha = "0.10"
 
 
 # This doesn't build on intel macos.
@@ -51,13 +53,14 @@ pqcrypto-mldsa = { version = "0.1.0" } #, default-features = false
 
 [target.'cfg(hax)'.dependencies]
 core-models = { path = "../crates/utils/core-models", version = "0.0.6" }
+hacspec_ml_dsa = { path = "../specs/ml-dsa" }
 
 [features]
 default = ["std", "mldsa44", "mldsa65", "mldsa87"]
 simd128 = ["libcrux-sha3/simd128", "libcrux-intrinsics/simd128"]
 simd256 = ["libcrux-sha3/simd256", "libcrux-intrinsics/simd256"]
 acvp = []                                                        # expose internal API for ACVP testing
-test-utils = []                                                  # exposing internal functions for testing
+cross-spec-tests = []                                            # tests/cross_spec.rs against the hacspec; re-exports internals for testing
 
 # Features for the different key sizes of ML-DSA
 mldsa44 = []
@@ -87,4 +90,7 @@ name = "ml-dsa"
 harness = false
 
 [lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)', 'cfg(valgrind_ct_test)'] }
+unexpected_cfgs = { level = "warn", check-cfg = [
+    'cfg(hax)',
+    'cfg(valgrind_ct_test)',
+] }

libcrux-ml-dsa/src/constants.rs

@@ -39,13 +39,13 @@ pub(crate) const CONTEXT_MAX_LEN: usize = 255;
 
 /// Eta values
 #[derive(Clone, Copy)]
-pub(crate) enum Eta {
+pub enum Eta {
     Two = 2,
     Four = 4,
 }
 
 /// Gamma2 values
-pub(crate) type Gamma2 = i32;
+pub type Gamma2 = i32;
 pub(crate) const GAMMA2_V261_888: Gamma2 = 261_888;
 pub(crate) const GAMMA2_V95_232: Gamma2 = 95_232;
 

libcrux-ml-dsa/src/lib.rs

@@ -31,6 +31,24 @@ pub use types::*;
 pub use crate::constants::KEY_GENERATION_RANDOMNESS_SIZE;
 pub use crate::constants::SIGNING_RANDOMNESS_SIZE;
 
+/// Internal items re-exported for cross-spec testing only.
+/// Gated behind the `cross-spec-tests` feature.
+#[cfg(feature = "cross-spec-tests")]
+pub mod test_utils {
+    pub use crate::constants::Eta;
+
+    /// SIMD per-lane arithmetic trait and the concrete impl types.
+    pub mod simd {
+        pub use crate::simd::portable::PortableSIMDUnit;
+        pub use crate::simd::traits::{
+            Operations, COEFFICIENTS_IN_SIMD_UNIT, SIMD_UNITS_IN_RING_ELEMENT,
+        };
+
+        #[cfg(feature = "simd256")]
+        pub use crate::simd::avx2::AVX2SIMDUnit;
+    }
+}
+
 #[cfg(feature = "mldsa44")]
 pub mod ml_dsa_44;
 

libcrux-ml-dsa/src/simd/avx2.rs

@@ -11,7 +11,8 @@ mod rejection_sample;
 mod vector_type;
 
 use arithmetic::shift_left_then_reduce;
-pub(crate) use vector_type::{AVX2RingElement, Vec256 as AVX2SIMDUnit};
+pub(crate) use vector_type::AVX2RingElement;
+pub use vector_type::Vec256 as AVX2SIMDUnit;
 
 #[cfg(hax)]
 impl Repr for AVX2SIMDUnit {

libcrux-ml-dsa/src/simd/avx2/vector_type.rs

@@ -2,7 +2,7 @@
 #[hax_lib::fstar::before("noeq")]
 #[derive(Clone, Copy)]
 #[repr(transparent)]
-pub(crate) struct Vec256 {
+pub struct Vec256 {
     pub(super) value: libcrux_intrinsics::avx2::Vec256,
 }
 

libcrux-ml-dsa/src/simd/portable.rs

@@ -14,7 +14,7 @@ mod sample;
 
 use arithmetic::shift_left_then_reduce;
 /// Portable SIMD coefficients
-pub(crate) use vector_type::Coefficients as PortableSIMDUnit;
+pub use vector_type::Coefficients as PortableSIMDUnit;
 use vector_type::Coefficients;
 
 #[cfg(hax)]

libcrux-ml-dsa/src/simd/portable/vector_type.rs

@@ -5,7 +5,7 @@ pub(crate) type FieldElement = i32;
 
 #[derive(Clone, Copy)]
 #[repr(transparent)]
-pub(crate) struct Coefficients {
+pub struct Coefficients {
     pub(super) values: [FieldElement; COEFFICIENTS_IN_SIMD_UNIT],
 }
 

libcrux-ml-dsa/src/simd/traits.rs

@@ -5,11 +5,11 @@ use crate::constants::{Eta, Gamma2};
 pub(crate) mod specs;
 
 // Each field element occupies 32 bits and the size of a simd_unit is 256 bits.
-pub(crate) const COEFFICIENTS_IN_SIMD_UNIT: usize = 8;
+pub const COEFFICIENTS_IN_SIMD_UNIT: usize = 8;
 
 // Note: For proofs, it is better to use concrete constants instead of const expressions
 //COEFFICIENTS_IN_RING_ELEMENT / COEFFICIENTS_IN_SIMD_UNIT;
-pub(crate) const SIMD_UNITS_IN_RING_ELEMENT: usize = 32;
+pub const SIMD_UNITS_IN_RING_ELEMENT: usize = 32;
 
 pub const FIELD_MODULUS: i32 = 8_380_417;
 
@@ -23,7 +23,7 @@ pub(crate) type FieldElementTimesMontgomeryR = i32;
 
 #[cfg(hax)]
 #[hax_lib::attributes]
-pub(crate) trait Repr: Copy + Clone {
+pub trait Repr: Copy + Clone {
     #[cfg(hax)]
     #[requires(true)]
     fn repr(&self) -> [i32; COEFFICIENTS_IN_SIMD_UNIT];
@@ -33,7 +33,7 @@ pub(crate) trait Repr: Copy + Clone {
 pub trait Repr {}
 
 #[hax_lib::attributes]
-pub(crate) trait Operations: Copy + Clone + Repr {
+pub trait Operations: Copy + Clone + Repr {
     #[hax_lib::requires(true)]
     #[hax_lib::ensures(|result| result.repr() == [0i32; COEFFICIENTS_IN_SIMD_UNIT])]
     fn zero() -> Self;

libcrux-ml-dsa/tests/cross_spec.rs

@@ -0,0 +1,14 @@
+//! Cross-comparison tests between the libcrux ML-DSA implementation and the
+//! hacspec specification at `specs/ml-dsa/`. Each `Operations`-trait method
+//! is exercised against its `hacspec_ml_dsa::*` equivalent.
+
+#![cfg(feature = "cross-spec-tests")]
+
+// Internal helpers and per-area test modules.
+mod cross_spec {
+    pub mod arithmetic;
+    pub mod encoding;
+    pub mod helpers;
+    pub mod ntt;
+    pub mod sampling;
+}