Fix hax extraction

cryspen · Jun 27, 2024 · 19040cd · 19040cd
1 parent 7f349f1
commit 19040cd
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 0 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/libcrux-ml-kem/Cargo.toml b/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"]

diff --git a/libcrux-ml-kem/src/kem/kyber/ntt.rs b/libcrux-ml-kem/src/kem/kyber/ntt.rs
@@ -7,6 +7,8 @@ use super::{
     },
     constants::COEFFICIENTS_IN_RING_ELEMENT,
 };
+#[cfg(hax)]
+use crate::kem::kyber::constants::FIELD_MODULUS;
 
 const ZETAS_TIMES_MONTGOMERY_R: [FieldElementTimesMontgomeryR; 128] = [
     -1044, -758, -359, -1517, 1493, 1422, 287, 202, -171, 622, 1577, 182, 962, -1202, -1474, 1468,