mldsa: cleanup simd trait

fstar-helpers/core-models/.gitignore

@@ -0,0 +1 @@
+proofs

libcrux-intrinsics/.gitignore

@@ -0,0 +1 @@
+proofs

libcrux-ml-dsa/proofs/fstar/extraction/.gitignore

@@ -0,0 +1 @@
+*.fst

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

@@ -1,6 +1,6 @@
 use crate::{
     constants::{Eta, Gamma2},
-    simd::traits::{Operations, COEFFICIENTS_IN_SIMD_UNIT, SIMD_UNITS_IN_RING_ELEMENT},
+    simd::traits::{Operations, SIMD_UNITS_IN_RING_ELEMENT},
 };
 
 #[cfg(not(eurydice))]
@@ -15,15 +15,18 @@ mod vector_type;
 
 pub(crate) use vector_type::{AVX2RingElement, Vec256 as AVX2SIMDUnit};
 
-#[cfg(not(eurydice))]
+#[cfg(hax)]
 impl Repr for AVX2SIMDUnit {
-    fn repr(&self) -> [i32; COEFFICIENTS_IN_SIMD_UNIT] {
-        let mut result = [0i32; COEFFICIENTS_IN_SIMD_UNIT];
+    fn repr(&self) -> [i32; super::traits::COEFFICIENTS_IN_SIMD_UNIT] {
+        let mut result = [0i32; super::traits::COEFFICIENTS_IN_SIMD_UNIT];
         vector_type::to_coefficient_array(self, &mut result);
         result
     }
 }
 
+#[cfg(any(eurydice, not(hax)))]
+impl Repr for AVX2SIMDUnit {}
+
 /// Implementing the [`Operations`] for AVX2.
 impl Operations for AVX2SIMDUnit {
     #[inline(always)]

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

@@ -1,10 +1,7 @@
 use libcrux_intrinsics::avx2::*;
 
 #[cfg(hax)]
-use core_models::abstractions::{
-    bit::Bit,
-    bitvec::{bitvec_postprocess_norm, BitVec},
-};
+use core_models::abstractions::bitvec::{bitvec_postprocess_norm, BitVec};
 
 #[hax_lib::ensures(|(lower, upper)| {
     use hax_lib::*;

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

@@ -19,15 +19,16 @@ mod sample;
 pub(crate) use vector_type::Coefficients as PortableSIMDUnit;
 use vector_type::Coefficients;
 
-use super::traits::COEFFICIENTS_IN_SIMD_UNIT;
-
-#[cfg(not(eurydice))]
+#[cfg(hax)]
 impl Repr for Coefficients {
-    fn repr(&self) -> [i32; COEFFICIENTS_IN_SIMD_UNIT] {
+    fn repr(&self) -> [i32; super::traits::COEFFICIENTS_IN_SIMD_UNIT] {
         self.values
     }
 }
 
+#[cfg(any(eurydice, not(hax)))]
+impl Repr for Coefficients {}
+
 impl Operations for Coefficients {
     fn zero() -> Coefficients {
         vector_type::zero()

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

@@ -1,7 +1,8 @@
 use crate::constants::{Eta, Gamma2};
 
+/// Specs for the proofs
 #[cfg(hax)]
-use hax_lib::*;
+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;
@@ -19,61 +20,15 @@ pub const INVERSE_OF_MODULUS_MOD_MONTGOMERY_R: u64 = 58_728_449;
 /// We use 'fer' as a shorthand for this type.
 pub(crate) type FieldElementTimesMontgomeryR = i32;
 
-#[cfg(not(eurydice))]
+#[cfg(hax)]
 #[hax_lib::attributes]
 pub(crate) trait Repr: Copy + Clone {
     #[requires(true)]
     fn repr(&self) -> [i32; COEFFICIENTS_IN_SIMD_UNIT];
 }
 
-#[cfg(hax)]
-pub(crate) mod specs {
-    use hax_lib::*;
-
-    type SIMDContent = [i32; COEFFICIENTS_IN_SIMD_UNIT];
-    // Avoiding a recursive bundle
-    const COEFFICIENTS_IN_SIMD_UNIT: usize = 8;
-
-    pub(crate) fn int_is_i32(i: Int) -> bool {
-        i <= i32::MAX.to_int() && i >= i32::MIN.to_int()
-    }
-
-    pub(crate) fn add_pre(lhs: &SIMDContent, rhs: &SIMDContent) -> Prop {
-        forall(|i: usize| {
-            implies(
-                i < COEFFICIENTS_IN_SIMD_UNIT,
-                int_is_i32(lhs[i].to_int() + rhs[i].to_int()),
-            )
-        })
-    }
-
-    pub(crate) fn add_post(lhs: &SIMDContent, rhs: &SIMDContent, future_lhs: &SIMDContent) -> Prop {
-        forall(|i: usize| {
-            implies(
-                i < COEFFICIENTS_IN_SIMD_UNIT,
-                future_lhs[i].to_int() == (lhs[i].to_int() + rhs[i].to_int()),
-            )
-        })
-    }
-
-    pub(crate) fn sub_pre(lhs: &SIMDContent, rhs: &SIMDContent) -> Prop {
-        forall(|i: usize| {
-            implies(
-                i < COEFFICIENTS_IN_SIMD_UNIT,
-                int_is_i32(lhs[i].to_int() - rhs[i].to_int()),
-            )
-        })
-    }
-
-    pub(crate) fn sub_post(lhs: &SIMDContent, rhs: &SIMDContent, future_lhs: &SIMDContent) -> Prop {
-        forall(|i: usize| {
-            implies(
-                i < COEFFICIENTS_IN_SIMD_UNIT,
-                future_lhs[i].to_int() == (lhs[i].to_int() - rhs[i].to_int()),
-            )
-        })
-    }
-}
+#[cfg(any(eurydice, not(hax)))]
+pub trait Repr {}
 
 #[cfg(not(eurydice))]
 #[hax_lib::attributes]
@@ -153,67 +108,3 @@ pub(crate) trait Operations: Copy + Clone + Repr {
     // invert NTT and convert to standard domain
     fn invert_ntt_montgomery(simd_units: &mut [Self; SIMD_UNITS_IN_RING_ELEMENT]);
 }
-
-#[cfg(eurydice)]
-pub(crate) trait Operations: Copy + Clone {
-    fn zero() -> Self;
-
-    fn from_coefficient_array(array: &[i32], out: &mut Self);
-    fn to_coefficient_array(value: &Self, out: &mut [i32]);
-
-    // Arithmetic
-    fn add(lhs: &mut Self, rhs: &Self);
-    fn subtract(lhs: &mut Self, rhs: &Self);
-    fn infinity_norm_exceeds(simd_unit: &Self, bound: i32) -> bool;
-    fn decompose(gamma2: Gamma2, simd_unit: &Self, low: &mut Self, high: &mut Self);
-    fn compute_hint(low: &Self, high: &Self, gamma2: i32, hint: &mut Self) -> usize;
-    fn use_hint(gamma2: Gamma2, simd_unit: &Self, hint: &mut Self);
-
-    // Modular operations
-    fn montgomery_multiply(lhs: &mut Self, rhs: &Self);
-    fn shift_left_then_reduce<const SHIFT_BY: i32>(simd_unit: &mut Self);
-
-    // Decomposition operations
-    fn power2round(t0: &mut Self, t1: &mut Self);
-
-    // Sampling
-    //
-    // In the sampling functions, since each SIMD unit can hold 8 coefficients,
-    // we expect that `out` has the capacity for up to 8 coefficients.
-
-    // Since each coefficient could potentially be sampled with 3 bytes, we expect
-    // `randomness` to hold 24 bytes.
-    fn rejection_sample_less_than_field_modulus(randomness: &[u8], out: &mut [i32]) -> usize;
-
-    // Since each coefficient could potentially be sampled with half a byte,
-    // we expect `randomness` to hold 4 bytes.
-    fn rejection_sample_less_than_eta_equals_2(randomness: &[u8], out: &mut [i32]) -> usize;
-    fn rejection_sample_less_than_eta_equals_4(randomness: &[u8], out: &mut [i32]) -> usize;
-
-    // Encoding operations
-
-    // Gamma1
-    fn gamma1_serialize(simd_unit: &Self, serialized: &mut [u8], gamma1_exponent: usize);
-    fn gamma1_deserialize(serialized: &[u8], out: &mut Self, gamma1_exponent: usize);
-
-    // Commitment
-    fn commitment_serialize(simd_unit: &Self, serialized: &mut [u8]);
-
-    // Error
-    fn error_serialize(eta: Eta, simd_unit: &Self, serialized: &mut [u8]);
-    fn error_deserialize(eta: Eta, serialized: &[u8], out: &mut Self);
-
-    // t0
-    fn t0_serialize(simd_unit: &Self, out: &mut [u8]); // out len 13
-    fn t0_deserialize(serialized: &[u8], out: &mut Self);
-
-    // t1
-    fn t1_serialize(simd_unit: &Self, out: &mut [u8]); // out len 10
-    fn t1_deserialize(serialized: &[u8], out: &mut Self);
-
-    // NTT
-    fn ntt(simd_units: &mut [Self; SIMD_UNITS_IN_RING_ELEMENT]);
-
-    // invert NTT and convert to standard domain
-    fn invert_ntt_montgomery(simd_units: &mut [Self; SIMD_UNITS_IN_RING_ELEMENT]);
-}

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

@@ -0,0 +1,45 @@
+use hax_lib::*;
+
+type SIMDContent = [i32; COEFFICIENTS_IN_SIMD_UNIT];
+// Avoiding a recursive bundle
+const COEFFICIENTS_IN_SIMD_UNIT: usize = 8;
+
+pub(crate) fn int_is_i32(i: Int) -> bool {
+    i <= i32::MAX.to_int() && i >= i32::MIN.to_int()
+}
+
+pub(crate) fn add_pre(lhs: &SIMDContent, rhs: &SIMDContent) -> Prop {
+    forall(|i: usize| {
+        implies(
+            i < COEFFICIENTS_IN_SIMD_UNIT,
+            int_is_i32(lhs[i].to_int() + rhs[i].to_int()),
+        )
+    })
+}
+
+pub(crate) fn add_post(lhs: &SIMDContent, rhs: &SIMDContent, future_lhs: &SIMDContent) -> Prop {
+    forall(|i: usize| {
+        implies(
+            i < COEFFICIENTS_IN_SIMD_UNIT,
+            future_lhs[i].to_int() == (lhs[i].to_int() + rhs[i].to_int()),
+        )
+    })
+}
+
+pub(crate) fn sub_pre(lhs: &SIMDContent, rhs: &SIMDContent) -> Prop {
+    forall(|i: usize| {
+        implies(
+            i < COEFFICIENTS_IN_SIMD_UNIT,
+            int_is_i32(lhs[i].to_int() - rhs[i].to_int()),
+        )
+    })
+}
+
+pub(crate) fn sub_post(lhs: &SIMDContent, rhs: &SIMDContent, future_lhs: &SIMDContent) -> Prop {
+    forall(|i: usize| {
+        implies(
+            i < COEFFICIENTS_IN_SIMD_UNIT,
+            future_lhs[i].to_int() == (lhs[i].to_int() - rhs[i].to_int()),
+        )
+    })
+}

libcrux-sha3/proofs/fstar/extraction/.gitignore

@@ -0,0 +1,2 @@
+*.fst
+*.fsti

secrets/.gitignore

@@ -0,0 +1 @@
+proofs

sys/platform/.gitignore

@@ -1,2 +1,3 @@
 target/
 Cargo.lock
+proofs