From 19040cda2f92b690c7e9d5c1fcde4e65a8af12ab Mon Sep 17 00:00:00 2001
From: Jonas Schneider-Bensch <jonas@cryspen.com>
Date: Thu, 27 Jun 2024 11:02:58 +0200
Subject: [PATCH] Fix hax extraction

---
 Cargo.lock                          | 1 +
 libcrux-ml-kem/Cargo.toml           | 1 +
 libcrux-ml-kem/src/kem/kyber/ntt.rs | 2 ++
 3 files changed, 4 insertions(+)

diff --git a/Cargo.lock b/Cargo.lock
index 87093de82..e7500ff9f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1030,6 +1030,7 @@ version = "0.0.2-pre.2"
 dependencies = [
  "criterion",
  "hax-lib 0.1.0-pre.1 (git+https://github.com/hacspec/hax/)",
+ "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax/)",
  "hex",
  "libcrux-intrinsics",
  "libcrux-platform",
diff --git a/libcrux-ml-kem/Cargo.toml b/libcrux-ml-kem/Cargo.toml
index 2f66da634..c72c48e45 100644
--- 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
index 6e933b02a..78448ee1b 100644
--- 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,