diff --git a/.gitignore b/.gitignore
index 5c3e1d548..f2eb8a8ef 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,3 +11,4 @@ fuzz/artifacts
 proofs/fstar/extraction/.cache
 __pycache__
 kyber-crate/
+*.llbc
diff --git a/libcrux-ml-kem/.gitignore b/libcrux-ml-kem/.gitignore
index af27795c5..fed5ebf9b 100644
--- a/libcrux-ml-kem/.gitignore
+++ b/libcrux-ml-kem/.gitignore
@@ -1,3 +1,4 @@
 Cargo.lock
 proofs/fstar/extraction/.cache/
 proofs/fstar/extraction/.depend
+c
diff --git a/libcrux-ml-kem/c.sh b/libcrux-ml-kem/c.sh
index 7a74b06ee..3b1f8b3e8 100755
--- a/libcrux-ml-kem/c.sh
+++ b/libcrux-ml-kem/c.sh
@@ -15,7 +15,7 @@ mkdir -p c
 cd c
 
 echo "Running eurydice ..."
-$EURYDICE_HOME/eurydice --config ../c.yaml ../libcrux_kyber.llbc
+$EURYDICE_HOME/eurydice --config ../c.yaml ../../libcrux_ml_kem.llbc
 cp $EURYDICE_HOME/include/eurydice_glue.h .
 
 if [[ -n "$HACL_PACKAGES_HOME" ]]; then
diff --git a/libcrux-ml-kem/src/sampling.rs b/libcrux-ml-kem/src/sampling.rs
index 002b85488..74edc5c2b 100644
--- a/libcrux-ml-kem/src/sampling.rs
+++ b/libcrux-ml-kem/src/sampling.rs
@@ -158,23 +158,25 @@ pub(super) fn sample_from_xof<const K: usize>(seeds: [[u8; 34]; K]) -> [Polynomi
 fn sample_from_binomial_distribution_2(randomness: &[u8]) -> PolynomialRingElement {
     let mut sampled_i32s = [0i32; 256];
 
-    for (chunk_number, byte_chunk) in randomness.chunks_exact(4).enumerate() {
-        let random_bits_as_u32: u32 = (byte_chunk[0] as u32)
-            | (byte_chunk[1] as u32) << 8
-            | (byte_chunk[2] as u32) << 16
-            | (byte_chunk[3] as u32) << 24;
-
-        let even_bits = random_bits_as_u32 & 0x55555555;
-        let odd_bits = (random_bits_as_u32 >> 1) & 0x55555555;
-        let coin_toss_outcomes = even_bits + odd_bits;
-
-        cloop! {
-            for outcome_set in (0..u32::BITS).step_by(4) {
-                let outcome_1 = ((coin_toss_outcomes >> outcome_set) & 0x3) as i32;
-                let outcome_2 = ((coin_toss_outcomes >> (outcome_set + 2)) & 0x3) as i32;
-
-                let offset = (outcome_set >> 2) as usize;
-                sampled_i32s[8 * chunk_number + offset] = outcome_1 - outcome_2;
+    cloop! {
+        for (chunk_number, byte_chunk) in randomness.chunks_exact(4).enumerate() {
+            let random_bits_as_u32: u32 = (byte_chunk[0] as u32)
+                | (byte_chunk[1] as u32) << 8
+                | (byte_chunk[2] as u32) << 16
+                | (byte_chunk[3] as u32) << 24;
+
+            let even_bits = random_bits_as_u32 & 0x55555555;
+            let odd_bits = (random_bits_as_u32 >> 1) & 0x55555555;
+            let coin_toss_outcomes = even_bits + odd_bits;
+
+            cloop! {
+                for outcome_set in (0..u32::BITS).step_by(4) {
+                    let outcome_1 = ((coin_toss_outcomes >> outcome_set) & 0x3) as i32;
+                    let outcome_2 = ((coin_toss_outcomes >> (outcome_set + 2)) & 0x3) as i32;
+
+                    let offset = (outcome_set >> 2) as usize;
+                    sampled_i32s[8 * chunk_number + offset] = outcome_1 - outcome_2;
+                }
             }
         }
     }
diff --git a/libcrux-ml-kem/src/simd/portable.rs b/libcrux-ml-kem/src/simd/portable.rs
index 7fd8d9820..f0cbff6fc 100644
--- a/libcrux-ml-kem/src/simd/portable.rs
+++ b/libcrux-ml-kem/src/simd/portable.rs
@@ -228,7 +228,7 @@ fn ntt_multiply(
     zeta0: i32,
     zeta1: i32,
 ) -> PortableVector {
-    let mut out = PortableVector::ZERO();
+    let mut out = ZERO();
     let product = ntt_multiply_binomials(
         (lhs.elements[0], lhs.elements[1]),
         (rhs.elements[0], rhs.elements[1]),
@@ -275,7 +275,7 @@ fn serialize_1(v: PortableVector) -> u8 {
 
 #[inline(always)]
 fn deserialize_1(v: u8) -> PortableVector {
-    let mut result = PortableVector::ZERO();
+    let mut result = ZERO();
     for i in 0..FIELD_ELEMENTS_IN_VECTOR {
         result.elements[i] = ((v >> i) & 0x1) as i32;
     }
@@ -297,7 +297,7 @@ fn serialize_4(v: PortableVector) -> [u8; 4] {
 
 #[inline(always)]
 fn deserialize_4(bytes: &[u8]) -> PortableVector {
-    let mut v = PortableVector::ZERO();
+    let mut v = ZERO();
 
     v.elements[0] = (bytes[0] & 0x0F) as i32;
     v.elements[1] = ((bytes[0] >> 4) & 0x0F) as i32;
@@ -329,7 +329,7 @@ fn serialize_5(v: PortableVector) -> [u8; 5] {
 
 #[inline(always)]
 fn deserialize_5(bytes: &[u8]) -> PortableVector {
-    let mut v = PortableVector::ZERO();
+    let mut v = ZERO();
 
     v.elements[0] = (bytes[0] & 0x1F) as i32;
     v.elements[1] = ((bytes[1] & 0x3) << 3 | (bytes[0] >> 5)) as i32;
@@ -364,7 +364,7 @@ fn serialize_10(v: PortableVector) -> [u8; 10] {
 
 #[inline(always)]
 fn deserialize_10(bytes: &[u8]) -> PortableVector {
-    let mut result = PortableVector::ZERO();
+    let mut result = ZERO();
 
     result.elements[0] = ((bytes[1] as i32 & 0x03) << 8 | (bytes[0] as i32 & 0xFF)) as i32;
     result.elements[1] = ((bytes[2] as i32 & 0x0F) << 6 | (bytes[1] as i32 >> 2)) as i32;
@@ -398,7 +398,7 @@ fn serialize_11(v: PortableVector) -> [u8; 11] {
 
 #[inline(always)]
 fn deserialize_11(bytes: &[u8]) -> PortableVector {
-    let mut result = PortableVector::ZERO();
+    let mut result = ZERO();
     result.elements[0] = ((bytes[1] as i32 & 0x7) << 8 | bytes[0] as i32) as i32;
     result.elements[1] = ((bytes[2] as i32 & 0x3F) << 5 | (bytes[1] as i32 >> 3)) as i32;
     result.elements[2] = ((bytes[4] as i32 & 0x1) << 10
@@ -438,7 +438,7 @@ fn serialize_12(v: PortableVector) -> [u8; 12] {
 
 #[inline(always)]
 fn deserialize_12(bytes: &[u8]) -> PortableVector {
-    let mut re = PortableVector::ZERO();
+    let mut re = ZERO();
 
     let byte0 = bytes[0] as i32;
     let byte1 = bytes[1] as i32;