Add missing models and some hax annotations

crates/utils/intrinsics/src/arm64_extract.rs

@@ -160,10 +160,22 @@ pub fn _vbcaxq_u64(a: _uint64x2_t, b: _uint64x2_t, c: _uint64x2_t) -> _uint64x2_
 pub fn _vreinterpretq_s16_u16(m0: _uint16x8_t) -> _int16x8_t {
     unimplemented!()
 }
+
 #[inline(always)]
 pub fn _vreinterpretq_u16_s16(m0: _int16x8_t) -> _uint16x8_t {
     unimplemented!()
 }
+
+#[inline(always)]
+pub fn _vreinterpretq_u32_u8(a: _uint8x16_t) -> _uint32x4_t {
+    unimplemented!()
+}
+
+#[inline(always)]
+pub fn _vreinterpretq_u8_u32(a: _uint32x4_t) -> _uint8x16_t {
+    unimplemented!()
+}
+
 #[inline(always)]
 pub fn _vmulq_s16(v: _int16x8_t, c: _int16x8_t) -> _int16x8_t {
     unimplemented!()
@@ -395,3 +407,51 @@ pub fn _vcleq_s16(a: _int16x8_t, b: _int16x8_t) -> _uint16x8_t {
 pub fn _vaddvq_u16(a: _uint16x8_t) -> u16 {
     unimplemented!()
 }
+
+////
+///
+
+#[inline(always)]
+pub fn _vld1q_u32(ptr: &[u32]) -> _uint32x4_t {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _veorq_u32(a: _uint32x4_t, b: _uint32x4_t) -> _uint32x4_t {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _vextq_u32<const N: i32>(a: _uint32x4_t, b: _uint32x4_t) -> _uint32x4_t {
+    unimplemented!()
+}
+
+#[inline(always)]
+pub fn _vmull_p64(a: u64, b: u64) -> u128 {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _veorq_u8(a: _uint8x16_t, b: _uint8x16_t) -> _uint8x16_t {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _vaesmcq_u8(data: _uint8x16_t) -> _uint8x16_t {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _vaeseq_u8(data: _uint8x16_t, key: _uint8x16_t) -> _uint8x16_t {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _vdupq_n_u8(value: u8) -> _uint8x16_t {
+    unimplemented!()
+}
+
+#[inline]
+pub fn _vdupq_laneq_u32<const N: i32>(a: _uint32x4_t) -> _uint32x4_t {
+    unimplemented!()
+}

crates/utils/intrinsics/src/avx2_extract.rs

@@ -621,3 +621,23 @@ pub fn mm256_unpacklo_epi64(a: Vec256, b: Vec256) -> Vec256 {
 pub fn mm256_permute2x128_si256<const IMM8: i32>(a: Vec256, b: Vec256) -> Vec256 {
     unimplemented!()
 }
+
+#[inline(always)]
+pub fn mm_clmulepi64_si128<const IMM8: i32>(a: Vec128, b: Vec128) -> Vec128 {
+    unimplemented!()
+}
+
+#[inline(always)]
+pub fn mm_aesenc_si128(a: Vec128, b: Vec128) -> Vec128 {
+    unimplemented!()
+}
+
+#[inline(always)]
+pub fn mm_aesenclast_si128(a: Vec128, b: Vec128) -> Vec128 {
+    unimplemented!()
+}
+
+#[inline(always)]
+pub fn mm_aeskeygenassist_si128<const RCON: i32>(a: Vec128) -> Vec128 {
+    unimplemented!()
+}

crates/utils/secrets/src/int/classify_public.rs

@@ -2,12 +2,8 @@
 //! We give definitions for all conversions so that they can be tested.
 //! We define no-ops here and force inlining, to ensure that these are free.
 
-#[cfg(not(hax))]
 use crate::traits::*;
 
-#[cfg(hax)]
-use crate::traits::{ClassifyRef, DeclassifyRef, Scalar};
-
 // TODO: Remove hax exemptions once this is supported.
 //       See https://github.com/cryspen/hax/issues/1674.
 
@@ -30,7 +26,7 @@ impl<'a, T: Scalar> DeclassifyRef for &'a [T] {
 }
 
 // Classify any mutable reference (identity)
-#[cfg(not(hax))]
+#[hax_lib::exclude]
 impl<'a, T> ClassifyRefMut for &'a mut T {
     type ClassifiedRefMut = &'a mut T;
     #[inline(always)]
@@ -40,7 +36,7 @@ impl<'a, T> ClassifyRefMut for &'a mut T {
 }
 
 // Declassify any mutable reference (identity)
-#[cfg(not(hax))]
+#[hax_lib::exclude]
 impl<'a, T> DeclassifyRefMut for &'a mut T {
     type DeclassifiedRefMut = &'a mut T;
     #[inline(always)]

libcrux-ml-kem/src/mlkem768.rs

@@ -36,7 +36,7 @@ const IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize = SHARED_SECRET_SIZE + CPA_PKE_C
 /// The ML-KEM 768 algorithms
 pub struct MlKem768;
 
-#[cfg(not(any(hax, eurydice)))]
+#[cfg(not(eurydice))]
 crate::impl_kem_trait!(
     MlKem768,
     MlKem768PublicKey,