diff --git a/.docker/c/ext-tools.sh b/.docker/c/ext-tools.sh
index 0a7283577..4bec0ebcf 100644
--- a/.docker/c/ext-tools.sh
+++ b/.docker/c/ext-tools.sh
@@ -4,23 +4,23 @@ set -v -e -x
 
 source $HOME/.profile
 
-curl -L https://github.com/AeneasVerif/charon/archive/45f5a34f336e35c6cc2253bc90cbdb8d812cefa9.zip \
+curl -L https://github.com/AeneasVerif/charon/archive/db4e045d4597d06d854ce7a2c10e8dcfda6ecd25.zip \
     --output charon.zip
 unzip charon.zip
 rm -rf charon.zip
-mv charon-45f5a34f336e35c6cc2253bc90cbdb8d812cefa9/ charon
+mv charon-db4e045d4597d06d854ce7a2c10e8dcfda6ecd25/ charon
 
-curl -L https://github.com/FStarLang/karamel/archive/8c3612018c25889288da6857771be3ad03b75bcd.zip \
+curl -L https://github.com/FStarLang/karamel/archive/3823e3d82fa0b271d799b61c59ffb4742ddc1e65.zip \
     --output karamel.zip
 unzip karamel.zip
 rm -rf karamel.zip
-mv karamel-8c3612018c25889288da6857771be3ad03b75bcd/ karamel
+mv karamel-3823e3d82fa0b271d799b61c59ffb4742ddc1e65/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/83ab5654d49df0603797bf510475d52d67ca24d8.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20/ eurydice
+mv eurydice-83ab5654d49df0603797bf510475d52d67ca24d8/ eurydice
 
 echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
@@ -39,7 +39,7 @@ cd -
 
 cd eurydice/lib
 rm -f charon
-ln -s $CHARON_HOME/charon-ml charon
+ln -s $CHARON_HOME charon
 rm -f krml
 ln -s $KRML_HOME/lib krml
 cd ../
diff --git a/.docker/c/install.sh b/.docker/c/install.sh
index a29a0ba77..30d7b24a4 100644
--- a/.docker/c/install.sh
+++ b/.docker/c/install.sh
@@ -9,7 +9,7 @@ opam init --bare --disable-sandboxing --shell-setup --yes
 opam switch create 4.14.1
 
 # Get F*, HACL*, Charon, Karamel, Eurydice for running proofs and extraction
-curl -L https://github.com/FStarLang/FStar/releases/download/v2024.09.05/fstar_2024.09.05_Linux_x86_64.tar.gz \
+curl -L https://github.com/FStarLang/FStar/releases/download/v2024.12.03/fstar_2024.12.03_Linux_x86_64.tar.gz \
     --output Fstar.tar.gz
 tar --extract --file Fstar.tar.gz
 rm -f Fstar.tar.gz
@@ -32,5 +32,5 @@ echo "export PATH=\"${PATH}:$HOME/fstar/bin:$HOME/z3/bin\"" >>$HOME/.profile
 echo "[[ ! -r /home/$USER/.opam/opam-init/init.sh ]] || source /home/$USER/.opam/opam-init/init.sh  > /dev/null 2> /dev/null" >>$HOME/.profile
 
 source $HOME/.profile
-opam install --yes ocamlfind visitors menhir ppx_deriving_yojson core_unix sedlex wasm fix process pprint zarith yaml easy_logging terminal
+opam install --yes ocamlfind visitors menhir ppx_deriving_yojson core_unix sedlex wasm fix process pprint zarith yaml easy_logging terminal unionFind
 eval $(opam env)
diff --git a/.github/workflows/c.yml b/.github/workflows/c.yml
index 5345cad14..1202192db 100644
--- a/.github/workflows/c.yml
+++ b/.github/workflows/c.yml
@@ -35,7 +35,7 @@ jobs:
           include-hidden-files: true
           if-no-files-found: error
 
-  extract-header-only:
+  extract-header-only-ml-kem:
     runs-on: ubuntu-latest
     container: franziskus/libcrux-c:latest
     defaults:
@@ -52,11 +52,34 @@ jobs:
       - name: Upload header only C extraction
         uses: actions/upload-artifact@v4
         with:
-          name: header-only-c-extraction
+          name: header-only-c-extraction-ml-kem
           path: libcrux-ml-kem/cg/
           include-hidden-files: true
           if-no-files-found: error
 
+
+  extract-header-only-ml-dsa:
+    runs-on: ubuntu-latest
+    container: franziskus/libcrux-c:latest
+    defaults:
+      run:
+        working-directory: libcrux-ml-dsa
+        shell: bash
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Extract C (header only)
+        run: |
+          ./boring.sh --no-clean
+
+      - name: Upload header only C extraction
+        uses: actions/upload-artifact@v4
+        with:
+          name: header-only-c-extraction-ml-dsa
+          path: libcrux-ml-dsa/cg/
+          include-hidden-files: true
+          if-no-files-found: error
+
   diff:
     needs: [extract]
     runs-on: ubuntu-latest
@@ -77,8 +100,8 @@ jobs:
           libcrux-ml-kem/headers_kill_revs.sh ~/c-extraction
           diff -r libcrux-ml-kem/c ~/c-extraction
 
-  diff-header-only:
-    needs: [extract-header-only]
+  diff-header-only-ml-kem:
+    needs: [extract-header-only-ml-kem]
     runs-on: ubuntu-latest
     defaults:
       run:
@@ -86,16 +109,37 @@ jobs:
     steps:
       - uses: actions/download-artifact@v4
         with:
-          name: header-only-c-extraction
-          path: ~/c-extraction
+          name: header-only-c-extraction-ml-kem
+          path: ~/mlkem-c-extraction
 
       - uses: actions/checkout@v4
 
       - name: Diff Extraction
         run: |
           libcrux-ml-kem/headers_kill_revs.sh libcrux-ml-kem/cg
-          libcrux-ml-kem/headers_kill_revs.sh ~/c-extraction
-          diff -r libcrux-ml-kem/cg ~/c-extraction
+          libcrux-ml-kem/headers_kill_revs.sh ~/mlkem-c-extraction
+          diff -r libcrux-ml-kem/cg ~/mlkem-c-extraction
+
+  diff-header-only-ml-dsa:
+    needs: [extract-header-only-ml-dsa]
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: header-only-c-extraction-ml-dsa
+          path: ~/mldsa-c-extraction
+
+      - uses: actions/checkout@v4
+
+      - name: Diff Extraction
+        run: |
+          libcrux-ml-kem/headers_kill_revs.sh libcrux-ml-dsa/cg
+          libcrux-ml-kem/headers_kill_revs.sh ~/mldsa-c-extraction
+          diff -r libcrux-ml-dsa/cg ~/mldsa-c-extraction
+
 
   build:
     needs: [extract]
@@ -136,8 +180,8 @@ jobs:
           cmake --build build --config Release
         if: ${{ matrix.os != 'windows-latest' }}
 
-  build-header-only:
-    needs: [extract-header-only]
+  build-header-only-ml-kem:
+    needs: [extract-header-only-ml-kem]
     strategy:
       fail-fast: false
       matrix:
@@ -152,7 +196,7 @@ jobs:
     steps:
       - uses: actions/download-artifact@v4
         with:
-          name: header-only-c-extraction
+          name: header-only-c-extraction-ml-kem
 
       - name: 🔨 Build
         run: |
@@ -163,3 +207,38 @@ jobs:
       - name: 🏃🏻‍♀️ Test
         run: ./build/ml_kem_test
         if: ${{ matrix.os != 'windows-latest' }}
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/Debug/ml_kem_test
+        if: ${{ matrix.os == 'windows-latest' }}
+
+  build-header-only-ml-dsa:
+    needs: [extract-header-only-ml-dsa]
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+          - windows-latest
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/download-artifact@v4
+        with:
+          name: header-only-c-extraction-ml-dsa
+
+      - name: 🔨 Build
+        run: |
+          cmake -B build
+          cmake --build build
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/ml_dsa_test
+        if: ${{ matrix.os != 'windows-latest' }}
+
+      - name: 🏃🏻‍♀️ Test
+        run: ./build/Debug/ml_dsa_test
+        if: ${{ matrix.os == 'windows-latest' }}
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
index 0846a37b9..17e057f4b 100644
--- a/.github/workflows/hax.yml
+++ b/.github/workflows/hax.yml
@@ -34,7 +34,7 @@ jobs:
       - uses: DeterminateSystems/magic-nix-cache-action@main
 
       - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/v2024.09.05
+        run: nix profile install github:FStarLang/FStar/v2024.12.03
 
       - name: ⤵ Clone HACL-star repository
         uses: actions/checkout@v4
diff --git a/libcrux-intrinsics/src/avx2_extract.rs b/libcrux-intrinsics/src/avx2_extract.rs
index 7954efeb1..db36e70c1 100644
--- a/libcrux-intrinsics/src/avx2_extract.rs
+++ b/libcrux-intrinsics/src/avx2_extract.rs
@@ -1,7 +1,7 @@
 //! This file does not contain correct function signatures!
 //! Replace with a hand-written file after extraction.
 
-#![allow(unused_variables, non_camel_case_types)]
+#![allow(unused_variables, non_camel_case_types, dead_code)]
 
 #[cfg(hax)]
 #[derive(Clone, Copy)]
diff --git a/libcrux-ml-dsa/cg/CMakeLists.txt b/libcrux-ml-dsa/cg/CMakeLists.txt
index ad60c81f9..8460674da 100644
--- a/libcrux-ml-dsa/cg/CMakeLists.txt
+++ b/libcrux-ml-dsa/cg/CMakeLists.txt
@@ -18,6 +18,7 @@ if(NOT MSVC)
         -Wall
         -fstack-usage
         -Wunused-function
+        # -Wno-unused-function
         $<$<CONFIG:DEBUG>:-g>
         $<$<CONFIG:DEBUG>:-Og>
         $<$<CONFIG:RELEASE>:-g>
diff --git a/libcrux-ml-dsa/cg/code_gen.txt b/libcrux-ml-dsa/cg/code_gen.txt
index cd71b6131..80f8dd1aa 100644
--- a/libcrux-ml-dsa/cg/code_gen.txt
+++ b/libcrux-ml-dsa/cg/code_gen.txt
@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
-Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
-Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
 F*: b0961063393215ca65927f017720cb365a193833-dirty
-Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
diff --git a/libcrux-ml-dsa/cg/eurydice_glue.h b/libcrux-ml-dsa/cg/eurydice_glue.h
index 9bfd9f546..10fbb17ba 100644
--- a/libcrux-ml-dsa/cg/eurydice_glue.h
+++ b/libcrux-ml-dsa/cg/eurydice_glue.h
@@ -149,6 +149,14 @@ static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) {
 #endif
 }
 
+static inline uint32_t core_num__i32_2__count_ones(int32_t x0) {
+#ifdef _MSC_VER
+  return __popcnt(x0);
+#else
+  return __builtin_popcount(x0);
+#endif
+}
+
 // unsigned overflow wraparound semantics in C
 static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x, uint16_t y) {
   return x + y;
diff --git a/libcrux-ml-dsa/cg/header.txt b/libcrux-ml-dsa/cg/header.txt
index c0b53bd40..c8d136fbe 100644
--- a/libcrux-ml-dsa/cg/header.txt
+++ b/libcrux-ml-dsa/cg/header.txt
@@ -4,9 +4,9 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
diff --git a/libcrux-ml-dsa/cg/intrinsics/libcrux_intrinsics_avx2.h b/libcrux-ml-dsa/cg/intrinsics/libcrux_intrinsics_avx2.h
index b51a17c1d..934676bb6 100644
--- a/libcrux-ml-dsa/cg/intrinsics/libcrux_intrinsics_avx2.h
+++ b/libcrux-ml-dsa/cg/intrinsics/libcrux_intrinsics_avx2.h
@@ -22,6 +22,8 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm256_castsi256_si128(a) \
   (_mm256_castsi256_si128(a))
 
+#define libcrux_intrinsics_avx2_mm256_castsi256_ps(a) (_mm256_castsi256_ps(a))
+
 #define libcrux_intrinsics_avx2_mm256_cvtepi16_epi32(a) \
   (_mm256_cvtepi16_epi32(a))
 
@@ -62,12 +64,23 @@ typedef __m256i core_core_arch_x86___m256i;
                                                 x7)                         \
   (_mm256_set_epi32(x0, x1, x2, x3, x4, x5, x6, x7))
 
+#define libcrux_intrinsics_avx2_mm256_set_epi64x(x0, x1, x2, x3) \
+  (_mm256_set_epi64x(x0, x1, x2, x3))
+
+#define libcrux_intrinsics_avx2_mm256_set_m128i(h, l) (_mm256_set_m128i(h, l))
+
+#define libcrux_intrinsics_avx2_mm_set_epi32(x0, x1, x2, x3) \
+  (_mm_set_epi32(x0, x1, x2, x3))
+
 #define libcrux_intrinsics_avx2_mm256_loadu_si256_i16(a) \
   (_mm256_loadu_si256((const __m256i *)a.ptr))
 
 #define libcrux_intrinsics_avx2_mm256_loadu_si256_u8(a) \
   (_mm256_loadu_si256((const __m256i *)a.ptr))
 
+#define libcrux_intrinsics_avx2_mm256_loadu_si256_i32(a) \
+  (_mm256_loadu_si256((const __m256i *)a.ptr))
+
 #define libcrux_intrinsics_avx2_mm_loadu_si128(a) \
   (_mm_loadu_si128((const __m128i *)a.ptr))
 
@@ -83,18 +96,30 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm_storeu_si128(a, b) \
   (_mm_storeu_si128((__m128i *)a.ptr, b))
 
+#define libcrux_intrinsics_avx2_mm256_storeu_si256_i32(a, b) \
+  (_mm256_storeu_si256((__m256i *)a.ptr, b))
+
+#define libcrux_intrinsics_avx2_mm_storeu_si128_i32(a, b) \
+  (_mm_storeu_si128((__m128i *)a.ptr, b))
+
 // Arithmetic: Add, Sub
 
 #define libcrux_intrinsics_avx2_mm256_add_epi16(a, b) (_mm256_add_epi16(a, b))
 
 #define libcrux_intrinsics_avx2_mm256_add_epi32(a, b) (_mm256_add_epi32(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_add_epi64(a, b) (_mm256_add_epi64(a, b))
+
 #define libcrux_intrinsics_avx2_mm_add_epi16(a, b) (_mm_add_epi16(a, b))
 
 #define libcrux_intrinsics_avx2_mm256_sub_epi16(a, b) (_mm256_sub_epi16(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_sub_epi32(a, b) (_mm256_sub_epi32(a, b))
+
 #define libcrux_intrinsics_avx2_mm_sub_epi16(a, b) (_mm_sub_epi16(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_abs_epi32(a) (_mm256_abs_epi32(a))
+
 // Arithmetic: Mul low and high, Mul-Add combinations
 
 #define libcrux_intrinsics_avx2_mm256_mullo_epi16(a, b) \
@@ -105,6 +130,8 @@ typedef __m256i core_core_arch_x86___m256i;
 
 #define libcrux_intrinsics_avx2_mm256_mul_epu32(a, b) (_mm256_mul_epu32(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_mul_epi32(a, b) (_mm256_mul_epi32(a, b))
+
 #define libcrux_intrinsics_avx2_mm256_mullo_epi32(a, b) \
   (_mm256_mullo_epi32(a, b))
 
@@ -114,11 +141,22 @@ typedef __m256i core_core_arch_x86___m256i;
 
 #define libcrux_intrinsics_avx2_mm256_madd_epi16(a, b) (_mm256_madd_epi16(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_sign_epi32(a, b) (_mm256_sign_epi32(a, b))
+
 // Comparison
 
 #define libcrux_intrinsics_avx2_mm256_cmpgt_epi16(a, b) \
   (_mm256_cmpgt_epi16(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_cmpgt_epi32(a, b) \
+  (_mm256_cmpgt_epi32(a, b))
+
+#define libcrux_intrinsics_avx2_mm256_testz_si256(a, b) \
+  (_mm256_testz_si256(a, b))
+
+#define libcrux_intrinsics_avx2_mm256_cmpeq_epi32(a, b) \
+  (_mm256_cmpeq_epi32(a, b))
+
 // Bitwise operations
 
 #define libcrux_intrinsics_avx2_mm256_and_si256(a, b) (_mm256_and_si256(a, b))
@@ -130,6 +168,10 @@ typedef __m256i core_core_arch_x86___m256i;
 
 #define libcrux_intrinsics_avx2_mm_movemask_epi8(a) (_mm_movemask_epi8(a))
 
+#define libcrux_intrinsics_avx2_mm256_movemask_ps(a) (_mm256_movemask_ps(a))
+
+#define libcrux_intrinsics_avx2_mm256_or_si256(a, b) (_mm256_or_si256(a, b))
+
 // Shift operations
 #define libcrux_intrinsics_avx2_mm256_srai_epi16(a, b, _) \
   (_mm256_srai_epi16(b, a))
@@ -157,12 +199,23 @@ typedef __m256i core_core_arch_x86___m256i;
 
 #define libcrux_intrinsics_avx2_mm256_sllv_epi32(a, b) (_mm256_sllv_epi32(a, b))
 
+#define libcrux_intrinsics_avx2_mm_sllv_epi32(a, b) (_mm_sllv_epi32(a, b))
+
+#define libcrux_intrinsics_avx2_mm_srli_epi64(a, b, _t) (_mm_srli_epi64(b, a))
+
 #define libcrux_intrinsics_avx2_mm256_srli_epi64_(a, b) \
   (_mm256_srli_epi64(b, a))
 
 #define libcrux_intrinsics_avx2_mm256_srli_epi64(a, b, c) \
   (libcrux_intrinsics_avx2_mm256_srli_epi64_(a, b))
 
+#define libcrux_intrinsics_avx2_mm256_srlv_epi32(a, b) (_mm256_srlv_epi32(a, b))
+
+#define libcrux_intrinsics_avx2_mm256_bsrli_epi128(a, b, _t) \
+  (_mm256_bsrli_epi128(b, a))
+
+#define libcrux_intrinsics_avx2_mm256_srlv_epi64(a, b) (_mm256_srlv_epi64(a, b))
+
 // Shuffle and Vector Interleaving
 
 #define libcrux_intrinsics_avx2_mm256_unpacklo_epi32(a, b) \
@@ -200,6 +253,14 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm256_blend_epi16(a, b, c, _) \
   (_mm256_blend_epi16(b, c, a))
 
+#define libcrux_intrinsics_avx2_mm256_blend_epi32(a, b, c, _) \
+  (_mm256_blend_epi32(b, c, a))
+
+#define libcrux_intrinsics_avx2_vec256_blendv_epi32(a, b, mask) \
+  (_mm256_castps_si256(_mm256_blendv_ps(_mm256_castsi256_ps(a), \
+                                        _mm256_castsi256_ps(b), \
+                                        _mm256_castsi256_ps(mask))))
+
 #define libcrux_intrinsics_avx2_mm256_shuffle_epi8(a, b) \
   (_mm256_shuffle_epi8(a, b))
 
diff --git a/libcrux-ml-dsa/cg/libcrux_core.h b/libcrux-ml-dsa/cg/libcrux_core.h
index cb97a4566..ac346a7d3 100644
--- a/libcrux-ml-dsa/cg/libcrux_core.h
+++ b/libcrux-ml-dsa/cg/libcrux_core.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_core_H
@@ -148,10 +148,10 @@ static inline uint8_t *libcrux_ml_dsa_types_as_ref_8f_fa(
   return self->value;
 }
 
-#define libcrux_ml_dsa_types_MalformedHintError 0
-#define libcrux_ml_dsa_types_SignerResponseExceedsBoundError 1
-#define libcrux_ml_dsa_types_CommitmentHashesDontMatchError 2
-#define libcrux_ml_dsa_types_VerificationContextTooLongError 3
+#define libcrux_ml_dsa_types_VerificationError_MalformedHintError 0
+#define libcrux_ml_dsa_types_VerificationError_SignerResponseExceedsBoundError 1
+#define libcrux_ml_dsa_types_VerificationError_CommitmentHashesDontMatchError 2
+#define libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError 3
 
 typedef uint8_t libcrux_ml_dsa_types_VerificationError;
 
@@ -245,8 +245,8 @@ typedef struct Option_67_s {
   uint8_t f0[48U];
 } Option_67;
 
-#define libcrux_ml_dsa_types_RejectionSamplingError 0
-#define libcrux_ml_dsa_types_ContextTooLongError 1
+#define libcrux_ml_dsa_types_SigningError_RejectionSamplingError 0
+#define libcrux_ml_dsa_types_SigningError_ContextTooLongError 1
 
 typedef uint8_t libcrux_ml_dsa_types_SigningError;
 
diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h
index a79e5a218..660143729 100644
--- a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h
+++ b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mldsa65_avx2_H
@@ -2104,19 +2104,6 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_avx2_ntt_ntt(__m256i re[32U],
   memcpy(ret, re, (size_t)32U * sizeof(__m256i));
 }
 
-/**
-This function found in impl {(libcrux_ml_dsa::simd::traits::Operations for
-libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit)}
-*/
-KRML_ATTRIBUTE_TARGET("avx2")
-static inline __m256i libcrux_ml_dsa_simd_avx2_ntt_closure_a2(__m256i **state,
-                                                              size_t i) {
-  KRML_HOST_EPRINTF(
-      "KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
-      "Eurydice error: Failure(\"unexpected / ill-typed projection\")\n");
-  KRML_HOST_EXIT(255U);
-}
-
 /**
 This function found in impl {(libcrux_ml_dsa::simd::traits::Operations for
 libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit)}
@@ -2138,13 +2125,18 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_avx2_ntt_a2(
   memcpy(copy_of_re, re, (size_t)32U * sizeof(__m256i));
   __m256i result[32U];
   libcrux_ml_dsa_simd_avx2_ntt_ntt(copy_of_re, result);
-  __m256i ret0[32U];
+  __m256i out[32U];
   for (size_t i = (size_t)0U; i < (size_t)32U; i++) {
-    ret0[i] = KRML_EABORT(
-        __m256i,
-        "Eurydice error: Failure(\"unexpected / ill-typed projection\")\n");
+    out[i] = libcrux_ml_dsa_simd_avx2_vector_type_ZERO();
+  }
+  for (size_t i = (size_t)0U;
+       i < Eurydice_slice_len(
+               Eurydice_array_to_slice((size_t)32U, result, __m256i), __m256i);
+       i++) {
+    size_t i0 = i;
+    out[i0] = result[i0];
   }
-  memcpy(ret, ret0, (size_t)32U * sizeof(__m256i));
+  memcpy(ret, out, (size_t)32U * sizeof(__m256i));
 }
 
 KRML_ATTRIBUTE_TARGET("avx2")
@@ -3187,19 +3179,6 @@ libcrux_ml_dsa_simd_avx2_invntt_invert_ntt_montgomery(__m256i re[32U],
   memcpy(ret, re, (size_t)32U * sizeof(__m256i));
 }
 
-/**
-This function found in impl {(libcrux_ml_dsa::simd::traits::Operations for
-libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit)}
-*/
-KRML_ATTRIBUTE_TARGET("avx2")
-static inline __m256i libcrux_ml_dsa_simd_avx2_invert_ntt_montgomery_closure_a2(
-    __m256i **state, size_t i) {
-  KRML_HOST_EPRINTF(
-      "KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
-      "Eurydice error: Failure(\"unexpected / ill-typed projection\")\n");
-  KRML_HOST_EXIT(255U);
-}
-
 /**
 This function found in impl {(libcrux_ml_dsa::simd::traits::Operations for
 libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit)}
@@ -3221,18 +3200,20 @@ static KRML_MUSTINLINE void libcrux_ml_dsa_simd_avx2_invert_ntt_montgomery_a2(
   memcpy(copy_of_re, re, (size_t)32U * sizeof(__m256i));
   __m256i result[32U];
   libcrux_ml_dsa_simd_avx2_invntt_invert_ntt_montgomery(copy_of_re, result);
-  __m256i ret0[32U];
+  __m256i out[32U];
   for (size_t i = (size_t)0U; i < (size_t)32U; i++) {
-    ret0[i] = KRML_EABORT(
-        __m256i,
-        "Eurydice error: Failure(\"unexpected / ill-typed projection\")\n");
+    out[i] = libcrux_ml_dsa_simd_avx2_vector_type_ZERO();
   }
-  memcpy(ret, ret0, (size_t)32U * sizeof(__m256i));
+  for (size_t i = (size_t)0U;
+       i < Eurydice_slice_len(
+               Eurydice_array_to_slice((size_t)32U, result, __m256i), __m256i);
+       i++) {
+    size_t i0 = i;
+    out[i0] = result[i0];
+  }
+  memcpy(ret, out, (size_t)32U * sizeof(__m256i));
 }
 
-typedef struct libcrux_ml_dsa_samplex4_avx2_AVX2Sampler_s {
-} libcrux_ml_dsa_samplex4_avx2_AVX2Sampler;
-
 /**
 A monomorphic instance of libcrux_ml_dsa.polynomial.PolynomialRingElement
 with types libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit
@@ -4988,11 +4969,12 @@ KRML_ATTRIBUTE_TARGET("avx2")
 static KRML_MUSTINLINE __m256i
 libcrux_ml_dsa_simd_avx2_encoding_error_deserialize_ac(
     Eurydice_slice serialized) {
-  __m256i unsigned =
+  __m256i deserialized =
       libcrux_ml_dsa_simd_avx2_encoding_error_deserialize_to_unsigned_ac(
           serialized);
   return libcrux_intrinsics_avx2_mm256_sub_epi32(
-      libcrux_intrinsics_avx2_mm256_set1_epi32((int32_t)(size_t)4U), unsigned);
+      libcrux_intrinsics_avx2_mm256_set1_epi32((int32_t)(size_t)4U),
+      deserialized);
 }
 
 /**
@@ -6497,184 +6479,174 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
   Option_67 commitment_hash0 = {.tag = None};
   Option_a4 signer_response0 = {.tag = None};
   Option_f0 hint0 = {.tag = None};
-  while (true) {
-    if (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) {
-      attempt++;
-      uint8_t uu____2[66U];
-      libcrux_ml_dsa_utils_into_padded_array_20(
-          Eurydice_array_to_slice((size_t)64U, mask_seed, uint8_t), uu____2);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 mask[5U];
-      libcrux_ml_dsa_sample_sample_mask_vector_51(
-          uu____2, &domain_separator_for_mask, mask);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 A_times_mask[6U];
-      libcrux_ml_dsa_matrix_compute_A_times_mask_fe(A_as_ntt, mask,
-                                                    A_times_mask);
-      /* Passing arrays by value in Rust generates a copy in C */
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-          copy_of_A_times_mask[6U];
-      memcpy(copy_of_A_times_mask, A_times_mask,
-             (size_t)6U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit_6size_t__x2
-          uu____4 = libcrux_ml_dsa_arithmetic_decompose_vector_fe(
-              copy_of_A_times_mask);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 w0[6U];
-      memcpy(w0, uu____4.fst,
-             (size_t)6U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 commitment[6U];
-      memcpy(commitment, uu____4.snd,
-             (size_t)6U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-      uint8_t commitment_hash_candidate[48U] = {0U};
+  while (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) {
+    attempt++;
+    uint8_t uu____2[66U];
+    libcrux_ml_dsa_utils_into_padded_array_20(
+        Eurydice_array_to_slice((size_t)64U, mask_seed, uint8_t), uu____2);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 mask[5U];
+    libcrux_ml_dsa_sample_sample_mask_vector_51(
+        uu____2, &domain_separator_for_mask, mask);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 A_times_mask[6U];
+    libcrux_ml_dsa_matrix_compute_A_times_mask_fe(A_as_ntt, mask, A_times_mask);
+    /* Passing arrays by value in Rust generates a copy in C */
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 copy_of_A_times_mask[6U];
+    memcpy(copy_of_A_times_mask, A_times_mask,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_libcrux_ml_dsa_simd_avx2_vector_type_AVX2SIMDUnit_6size_t__x2
+        uu____4 =
+            libcrux_ml_dsa_arithmetic_decompose_vector_fe(copy_of_A_times_mask);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 w0[6U];
+    memcpy(w0, uu____4.fst,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 commitment[6U];
+    memcpy(commitment, uu____4.snd,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
+    uint8_t commitment_hash_candidate[48U] = {0U};
+    /* Passing arrays by value in Rust generates a copy in C */
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 copy_of_commitment0[6U];
+    memcpy(copy_of_commitment0, commitment,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
+    uint8_t commitment_serialized[768U];
+    libcrux_ml_dsa_encoding_commitment_serialize_vector_ef(
+        copy_of_commitment0, commitment_serialized);
+    libcrux_sha3_portable_incremental_Shake256Xof shake =
+        libcrux_ml_dsa_hash_functions_portable_init_83();
+    libcrux_ml_dsa_hash_functions_portable_absorb_83(
+        &shake,
+        Eurydice_array_to_slice((size_t)64U, message_representative, uint8_t));
+    libcrux_ml_dsa_hash_functions_portable_absorb_final_83(
+        &shake,
+        Eurydice_array_to_slice((size_t)768U, commitment_serialized, uint8_t));
+    libcrux_ml_dsa_hash_functions_portable_squeeze_83(
+        &shake, Eurydice_array_to_slice((size_t)48U, commitment_hash_candidate,
+                                        uint8_t));
+    /* Passing arrays by value in Rust generates a copy in C */
+    uint8_t copy_of_commitment_hash_candidate[48U];
+    memcpy(copy_of_commitment_hash_candidate, commitment_hash_candidate,
+           (size_t)48U * sizeof(uint8_t));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24
+        verifier_challenge_as_ntt = libcrux_ml_dsa_ntt_ntt_ea(
+            libcrux_ml_dsa_sample_sample_challenge_ring_element_8a(
+                copy_of_commitment_hash_candidate));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 challenge_times_s1[5U];
+    libcrux_ml_dsa_matrix_vector_times_ring_element_1f(
+        s1_as_ntt, &verifier_challenge_as_ntt, challenge_times_s1);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24 challenge_times_s2[6U];
+    libcrux_ml_dsa_matrix_vector_times_ring_element_a3(
+        s2_as_ntt, &verifier_challenge_as_ntt, challenge_times_s2);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24
+        signer_response_candidate[5U];
+    libcrux_ml_dsa_matrix_add_vectors_1f(mask, challenge_times_s1,
+                                         signer_response_candidate);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24
+        w0_minus_challenge_times_s2[6U];
+    libcrux_ml_dsa_matrix_subtract_vectors_a3(w0, challenge_times_s2,
+                                              w0_minus_challenge_times_s2);
+    /* Passing arrays by value in Rust generates a copy in C */
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_24
+        copy_of_signer_response_candidate[5U];
+    memcpy(copy_of_signer_response_candidate, signer_response_candidate,
+           (size_t)5U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
+    if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_1f(
+            copy_of_signer_response_candidate,
+            ((int32_t)1 << (uint32_t)(size_t)19U) - BETA)) {
       /* Passing arrays by value in Rust generates a copy in C */
       libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-          copy_of_commitment0[6U];
-      memcpy(copy_of_commitment0, commitment,
+          copy_of_w0_minus_challenge_times_s2[6U];
+      memcpy(copy_of_w0_minus_challenge_times_s2, w0_minus_challenge_times_s2,
              (size_t)6U *
                  sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-      uint8_t commitment_serialized[768U];
-      libcrux_ml_dsa_encoding_commitment_serialize_vector_ef(
-          copy_of_commitment0, commitment_serialized);
-      libcrux_sha3_portable_incremental_Shake256Xof shake =
-          libcrux_ml_dsa_hash_functions_portable_init_83();
-      libcrux_ml_dsa_hash_functions_portable_absorb_83(
-          &shake, Eurydice_array_to_slice((size_t)64U, message_representative,
-                                          uint8_t));
-      libcrux_ml_dsa_hash_functions_portable_absorb_final_83(
-          &shake, Eurydice_array_to_slice((size_t)768U, commitment_serialized,
-                                          uint8_t));
-      libcrux_ml_dsa_hash_functions_portable_squeeze_83(
-          &shake, Eurydice_array_to_slice((size_t)48U,
-                                          commitment_hash_candidate, uint8_t));
-      /* Passing arrays by value in Rust generates a copy in C */
-      uint8_t copy_of_commitment_hash_candidate[48U];
-      memcpy(copy_of_commitment_hash_candidate, commitment_hash_candidate,
-             (size_t)48U * sizeof(uint8_t));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-          verifier_challenge_as_ntt = libcrux_ml_dsa_ntt_ntt_ea(
-              libcrux_ml_dsa_sample_sample_challenge_ring_element_8a(
-                  copy_of_commitment_hash_candidate));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 challenge_times_s1[5U];
-      libcrux_ml_dsa_matrix_vector_times_ring_element_1f(
-          s1_as_ntt, &verifier_challenge_as_ntt, challenge_times_s1);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24 challenge_times_s2[6U];
-      libcrux_ml_dsa_matrix_vector_times_ring_element_a3(
-          s2_as_ntt, &verifier_challenge_as_ntt, challenge_times_s2);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-          signer_response_candidate[5U];
-      libcrux_ml_dsa_matrix_add_vectors_1f(mask, challenge_times_s1,
-                                           signer_response_candidate);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-          w0_minus_challenge_times_s2[6U];
-      libcrux_ml_dsa_matrix_subtract_vectors_a3(w0, challenge_times_s2,
-                                                w0_minus_challenge_times_s2);
-      /* Passing arrays by value in Rust generates a copy in C */
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-          copy_of_signer_response_candidate[5U];
-      memcpy(copy_of_signer_response_candidate, signer_response_candidate,
-             (size_t)5U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-      if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_1f(
-              copy_of_signer_response_candidate,
-              ((int32_t)1 << (uint32_t)(size_t)19U) - BETA)) {
+      if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_a3(
+              copy_of_w0_minus_challenge_times_s2, (int32_t)261888 - BETA)) {
+        libcrux_ml_dsa_polynomial_PolynomialRingElement_24
+            challenge_times_t0[6U];
+        libcrux_ml_dsa_matrix_vector_times_ring_element_a3(
+            t0_as_ntt, &verifier_challenge_as_ntt, challenge_times_t0);
         /* Passing arrays by value in Rust generates a copy in C */
         libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-            copy_of_w0_minus_challenge_times_s2[6U];
-        memcpy(copy_of_w0_minus_challenge_times_s2, w0_minus_challenge_times_s2,
+            copy_of_challenge_times_t0[6U];
+        memcpy(copy_of_challenge_times_t0, challenge_times_t0,
                (size_t)6U *
                    sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
         if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_a3(
-                copy_of_w0_minus_challenge_times_s2, (int32_t)261888 - BETA)) {
+                copy_of_challenge_times_t0, (int32_t)261888)) {
           libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-              challenge_times_t0[6U];
-          libcrux_ml_dsa_matrix_vector_times_ring_element_a3(
-              t0_as_ntt, &verifier_challenge_as_ntt, challenge_times_t0);
+              w0_minus_c_times_s2_plus_c_times_t0[6U];
+          libcrux_ml_dsa_matrix_add_vectors_a3(
+              w0_minus_challenge_times_s2, challenge_times_t0,
+              w0_minus_c_times_s2_plus_c_times_t0);
           /* Passing arrays by value in Rust generates a copy in C */
           libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-              copy_of_challenge_times_t0[6U];
+              copy_of_w0_minus_c_times_s2_plus_c_times_t0[6U];
           memcpy(
-              copy_of_challenge_times_t0, challenge_times_t0,
+              copy_of_w0_minus_c_times_s2_plus_c_times_t0,
+              w0_minus_c_times_s2_plus_c_times_t0,
               (size_t)6U *
                   sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-          if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_a3(
-                  copy_of_challenge_times_t0, (int32_t)261888)) {
-            libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-                w0_minus_c_times_s2_plus_c_times_t0[6U];
-            libcrux_ml_dsa_matrix_add_vectors_a3(
-                w0_minus_challenge_times_s2, challenge_times_t0,
-                w0_minus_c_times_s2_plus_c_times_t0);
+          /* Passing arrays by value in Rust generates a copy in C */
+          libcrux_ml_dsa_polynomial_PolynomialRingElement_24
+              copy_of_commitment[6U];
+          memcpy(
+              copy_of_commitment, commitment,
+              (size_t)6U *
+                  sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
+          tuple_e6 uu____12 = libcrux_ml_dsa_arithmetic_make_hint_fe(
+              copy_of_w0_minus_c_times_s2_plus_c_times_t0, copy_of_commitment);
+          int32_t hint_candidate[6U][256U];
+          memcpy(hint_candidate, uu____12.fst,
+                 (size_t)6U * sizeof(int32_t[256U]));
+          size_t ones_in_hint = uu____12.snd;
+          if (!(ones_in_hint > (size_t)55U)) {
+            attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN;
+            /* Passing arrays by value in Rust generates a copy in C */
+            uint8_t copy_of_commitment_hash_candidate0[48U];
+            memcpy(copy_of_commitment_hash_candidate0,
+                   commitment_hash_candidate, (size_t)48U * sizeof(uint8_t));
+            Option_67 lit0;
+            lit0.tag = Some;
+            memcpy(lit0.f0, copy_of_commitment_hash_candidate0,
+                   (size_t)48U * sizeof(uint8_t));
+            commitment_hash0 = lit0;
             /* Passing arrays by value in Rust generates a copy in C */
             libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-                copy_of_w0_minus_c_times_s2_plus_c_times_t0[6U];
+                copy_of_signer_response_candidate0[5U];
             memcpy(
-                copy_of_w0_minus_c_times_s2_plus_c_times_t0,
-                w0_minus_c_times_s2_plus_c_times_t0,
-                (size_t)6U *
+                copy_of_signer_response_candidate0, signer_response_candidate,
+                (size_t)5U *
                     sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-            /* Passing arrays by value in Rust generates a copy in C */
-            libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-                copy_of_commitment[6U];
+            Option_a4 lit1;
+            lit1.tag = Some;
             memcpy(
-                copy_of_commitment, commitment,
-                (size_t)6U *
+                lit1.f0, copy_of_signer_response_candidate0,
+                (size_t)5U *
                     sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-            tuple_e6 uu____12 = libcrux_ml_dsa_arithmetic_make_hint_fe(
-                copy_of_w0_minus_c_times_s2_plus_c_times_t0,
-                copy_of_commitment);
-            int32_t hint_candidate[6U][256U];
-            memcpy(hint_candidate, uu____12.fst,
+            signer_response0 = lit1;
+            /* Passing arrays by value in Rust generates a copy in C */
+            int32_t copy_of_hint_candidate[6U][256U];
+            memcpy(copy_of_hint_candidate, hint_candidate,
                    (size_t)6U * sizeof(int32_t[256U]));
-            size_t ones_in_hint = uu____12.snd;
-            if (!(ones_in_hint > (size_t)55U)) {
-              attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN;
-              /* Passing arrays by value in Rust generates a copy in C */
-              uint8_t copy_of_commitment_hash_candidate0[48U];
-              memcpy(copy_of_commitment_hash_candidate0,
-                     commitment_hash_candidate, (size_t)48U * sizeof(uint8_t));
-              Option_67 lit0;
-              lit0.tag = Some;
-              memcpy(lit0.f0, copy_of_commitment_hash_candidate0,
-                     (size_t)48U * sizeof(uint8_t));
-              commitment_hash0 = lit0;
-              /* Passing arrays by value in Rust generates a copy in C */
-              libcrux_ml_dsa_polynomial_PolynomialRingElement_24
-                  copy_of_signer_response_candidate0[5U];
-              memcpy(
-                  copy_of_signer_response_candidate0, signer_response_candidate,
-                  (size_t)5U *
-                      sizeof(
-                          libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-              Option_a4 lit1;
-              lit1.tag = Some;
-              memcpy(
-                  lit1.f0, copy_of_signer_response_candidate0,
-                  (size_t)5U *
-                      sizeof(
-                          libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
-              signer_response0 = lit1;
-              /* Passing arrays by value in Rust generates a copy in C */
-              int32_t copy_of_hint_candidate[6U][256U];
-              memcpy(copy_of_hint_candidate, hint_candidate,
-                     (size_t)6U * sizeof(int32_t[256U]));
-              Option_f0 lit;
-              lit.tag = Some;
-              memcpy(lit.f0, copy_of_hint_candidate,
-                     (size_t)6U * sizeof(int32_t[256U]));
-              hint0 = lit;
-            }
+            Option_f0 lit;
+            lit.tag = Some;
+            memcpy(lit.f0, copy_of_hint_candidate,
+                   (size_t)6U * sizeof(int32_t[256U]));
+            hint0 = lit;
           }
         }
       }
-    } else {
-      break;
     }
   }
   Result_2e uu____16;
   if (commitment_hash0.tag == None) {
     uu____16 = (CLITERAL(Result_2e){
         .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_RejectionSamplingError}});
+        .val = {.case_Err =
+                    libcrux_ml_dsa_types_SigningError_RejectionSamplingError}});
   } else {
     uint8_t commitment_hash1[48U];
     memcpy(commitment_hash1, commitment_hash0.f0,
@@ -6684,7 +6656,9 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
     if (signer_response0.tag == None) {
       uu____16 = (CLITERAL(Result_2e){
           .tag = Err,
-          .val = {.case_Err = libcrux_ml_dsa_types_RejectionSamplingError}});
+          .val = {
+              .case_Err =
+                  libcrux_ml_dsa_types_SigningError_RejectionSamplingError}});
     } else {
       libcrux_ml_dsa_polynomial_PolynomialRingElement_24 signer_response1[5U];
       memcpy(signer_response1, signer_response0.f0,
@@ -6697,7 +6671,9 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
       if (hint0.tag == None) {
         uu____16 = (CLITERAL(Result_2e){
             .tag = Err,
-            .val = {.case_Err = libcrux_ml_dsa_types_RejectionSamplingError}});
+            .val = {
+                .case_Err =
+                    libcrux_ml_dsa_types_SigningError_RejectionSamplingError}});
       } else {
         int32_t hint1[6U][256U];
         memcpy(hint1, hint0.f0, (size_t)6U * sizeof(int32_t[256U]));
@@ -6724,15 +6700,16 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
                (size_t)5U *
                    sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
         memcpy(lit0.hint, copy_of_hint, (size_t)6U * sizeof(int32_t[256U]));
-        libcrux_ml_dsa_encoding_signature_serialize_92_cc(&lit0, signature);
+        /* original Rust expression is not an lvalue in C */
+        libcrux_ml_dsa_encoding_signature_Signature_ca lvalue = lit0;
+        libcrux_ml_dsa_encoding_signature_serialize_92_cc(&lvalue, signature);
         /* Passing arrays by value in Rust generates a copy in C */
         uint8_t copy_of_signature[3309U];
         memcpy(copy_of_signature, signature, (size_t)3309U * sizeof(uint8_t));
         Result_2e lit;
         lit.tag = Ok;
         lit.val.case_Ok = libcrux_ml_dsa_types_new_8f_fa(copy_of_signature);
-        uu____16 = lit;
-        return uu____16;
+        return lit;
       }
     }
   }
@@ -6768,25 +6745,23 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_6b(
     uint8_t randomness[32U]) {
   Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_45(
       context, (CLITERAL(Option_30){.tag = None}));
-  Result_2e uu____1;
-  if (uu____0.tag == Ok) {
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
-        dsc;
-    uint8_t *uu____2 = signing_key;
-    Eurydice_slice uu____3 = message;
-    Option_84 uu____4 = {.tag = Some, .f0 = domain_separation_context};
-    /* Passing arrays by value in Rust generates a copy in C */
-    uint8_t copy_of_randomness[32U];
-    memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-    uu____1 = libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
-        uu____2, uu____3, uu____4, copy_of_randomness);
-  } else {
-    uu____1 = (CLITERAL(Result_2e){
+  if (!(uu____0.tag == Ok)) {
+    return (CLITERAL(Result_2e){
         .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_ContextTooLongError}});
-  }
-  return uu____1;
+        .val = {.case_Err =
+                    libcrux_ml_dsa_types_SigningError_ContextTooLongError}});
+  }
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+      dsc;
+  uint8_t *uu____1 = signing_key;
+  Eurydice_slice uu____2 = message;
+  Option_84 uu____3 = {.tag = Some, .f0 = domain_separation_context};
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[32U];
+  memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+  return libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
+      uu____1, uu____2, uu____3, copy_of_randomness);
 }
 
 /**
@@ -6915,42 +6890,40 @@ libcrux_ml_dsa_ml_dsa_generic_sign_pre_hashed_b7(uint8_t *signing_key,
                                                  Eurydice_slice message,
                                                  Eurydice_slice context,
                                                  uint8_t randomness[32U]) {
-  Result_2e uu____0;
-  if (Eurydice_slice_len(context, uint8_t) >
-      LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN) {
-    uu____0 = (CLITERAL(Result_2e){
-        .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_ContextTooLongError}});
-  } else {
+  if (!(Eurydice_slice_len(context, uint8_t) >
+        LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN)) {
     uint8_t pre_hashed_message[256U];
     libcrux_ml_dsa_pre_hash_hash_bd_54(message, pre_hashed_message);
-    Eurydice_slice uu____1 = context;
+    Eurydice_slice uu____0 = context;
     Option_30 lit;
     lit.tag = Some;
     uint8_t ret[11U];
     libcrux_ml_dsa_pre_hash_oid_bd(ret);
     memcpy(lit.f0, ret, (size_t)11U * sizeof(uint8_t));
-    Result_a8 uu____2 = libcrux_ml_dsa_pre_hash_new_45(uu____1, lit);
-    if (uu____2.tag == Ok) {
-      libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____2.val.case_Ok;
-      libcrux_ml_dsa_pre_hash_DomainSeparationContext
-          domain_separation_context = dsc;
-      uint8_t *uu____3 = signing_key;
-      Eurydice_slice uu____4 =
-          Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t);
-      Option_84 uu____5 = {.tag = Some, .f0 = domain_separation_context};
-      /* Passing arrays by value in Rust generates a copy in C */
-      uint8_t copy_of_randomness[32U];
-      memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-      uu____0 = libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
-          uu____3, uu____4, uu____5, copy_of_randomness);
-    } else {
-      uu____0 = (CLITERAL(Result_2e){
+    Result_a8 uu____1 = libcrux_ml_dsa_pre_hash_new_45(uu____0, lit);
+    if (!(uu____1.tag == Ok)) {
+      return (CLITERAL(Result_2e){
           .tag = Err,
-          .val = {.case_Err = libcrux_ml_dsa_types_ContextTooLongError}});
+          .val = {.case_Err =
+                      libcrux_ml_dsa_types_SigningError_ContextTooLongError}});
     }
+    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____1.val.case_Ok;
+    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+        dsc;
+    uint8_t *uu____2 = signing_key;
+    Eurydice_slice uu____3 =
+        Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t);
+    Option_84 uu____4 = {.tag = Some, .f0 = domain_separation_context};
+    /* Passing arrays by value in Rust generates a copy in C */
+    uint8_t copy_of_randomness[32U];
+    memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+    return libcrux_ml_dsa_ml_dsa_generic_sign_internal_6b(
+        uu____2, uu____3, uu____4, copy_of_randomness);
   }
-  return uu____0;
+  return (CLITERAL(Result_2e){
+      .tag = Err,
+      .val = {.case_Err =
+                  libcrux_ml_dsa_types_SigningError_ContextTooLongError}});
 }
 
 /**
@@ -7192,188 +7165,174 @@ libcrux_ml_dsa_encoding_signature_deserialize_92_cc(uint8_t *serialized) {
   size_t previous_true_hints_seen = (size_t)0U;
   size_t i = (size_t)0U;
   bool malformed_hint = false;
-  while (true) {
-    if (i < (size_t)6U) {
-      if (malformed_hint) {
-        break;
-      } else {
-        size_t current_true_hints_seen = (size_t)Eurydice_slice_index(
-            hint_serialized, (size_t)55U + i, uint8_t, uint8_t *);
-        size_t j;
-        bool uu____2;
-        bool uu____3;
-        size_t uu____4;
-        size_t uu____5;
-        bool uu____6;
-        size_t uu____7;
-        size_t uu____8;
-        bool uu____9;
-        uint8_t uu____10;
-        size_t uu____11;
-        uint8_t uu____12;
-        size_t uu____13;
-        size_t uu____14;
-        bool uu____15;
-        size_t uu____16;
-        size_t uu____17;
-        uint8_t uu____18;
-        size_t uu____19;
-        bool uu____20;
-        size_t uu____21;
-        if (!(current_true_hints_seen < previous_true_hints_seen)) {
-          if (!(previous_true_hints_seen > (size_t)55U)) {
-            j = previous_true_hints_seen;
-            while (true) {
-              uu____2 = malformed_hint;
-              if (uu____2) {
-                break;
-              } else {
-                uu____4 = j;
-                uu____5 = current_true_hints_seen;
-                uu____3 = uu____4 < uu____5;
-                if (uu____3) {
-                  uu____7 = j;
-                  uu____8 = previous_true_hints_seen;
-                  uu____6 = uu____7 > uu____8;
-                  if (uu____6) {
-                    uu____11 = j;
-                    uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
-                                                    uint8_t, uint8_t *);
-                    uu____14 = j;
-                    uu____13 = uu____14 - (size_t)1U;
-                    uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
-                                                    uint8_t, uint8_t *);
-                    uu____9 = uu____10 <= uu____12;
-                    if (uu____9) {
-                      malformed_hint = true;
-                      uu____15 = malformed_hint;
-                      if (!uu____15) {
-                        uu____16 = i;
-                        uu____19 = j;
-                        uu____18 = Eurydice_slice_index(
-                            hint_serialized, uu____19, uint8_t, uint8_t *);
-                        uu____17 = (size_t)uu____18;
-                        hint[uu____16][uu____17] = (int32_t)1;
-                        j++;
-                      }
-                      continue;
+  while (i < (size_t)6U) {
+    if (malformed_hint) {
+      break;
+    } else {
+      size_t current_true_hints_seen = (size_t)Eurydice_slice_index(
+          hint_serialized, (size_t)55U + i, uint8_t, uint8_t *);
+      size_t j;
+      bool uu____2;
+      bool uu____3;
+      size_t uu____4;
+      size_t uu____5;
+      bool uu____6;
+      size_t uu____7;
+      size_t uu____8;
+      bool uu____9;
+      uint8_t uu____10;
+      size_t uu____11;
+      uint8_t uu____12;
+      size_t uu____13;
+      size_t uu____14;
+      bool uu____15;
+      size_t uu____16;
+      size_t uu____17;
+      uint8_t uu____18;
+      size_t uu____19;
+      bool uu____20;
+      size_t uu____21;
+      if (!(current_true_hints_seen < previous_true_hints_seen)) {
+        if (!(previous_true_hints_seen > (size_t)55U)) {
+          j = previous_true_hints_seen;
+          while (true) {
+            uu____2 = malformed_hint;
+            if (uu____2) {
+              break;
+            } else {
+              uu____4 = j;
+              uu____5 = current_true_hints_seen;
+              uu____3 = uu____4 < uu____5;
+              if (uu____3) {
+                uu____7 = j;
+                uu____8 = previous_true_hints_seen;
+                uu____6 = uu____7 > uu____8;
+                if (uu____6) {
+                  uu____11 = j;
+                  uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
+                                                  uint8_t, uint8_t *);
+                  uu____14 = j;
+                  uu____13 = uu____14 - (size_t)1U;
+                  uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
+                                                  uint8_t, uint8_t *);
+                  uu____9 = uu____10 <= uu____12;
+                  if (uu____9) {
+                    malformed_hint = true;
+                    uu____15 = malformed_hint;
+                    if (!uu____15) {
+                      uu____16 = i;
+                      uu____19 = j;
+                      uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                                      uint8_t, uint8_t *);
+                      uu____17 = (size_t)uu____18;
+                      hint[uu____16][uu____17] = (int32_t)1;
+                      j++;
                     }
+                    continue;
                   }
-                  uu____15 = malformed_hint;
-                  if (!uu____15) {
-                    uu____16 = i;
-                    uu____19 = j;
-                    uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
-                                                    uint8_t, uint8_t *);
-                    uu____17 = (size_t)uu____18;
-                    hint[uu____16][uu____17] = (int32_t)1;
-                    j++;
-                  }
-                } else {
-                  break;
                 }
+                uu____15 = malformed_hint;
+                if (!uu____15) {
+                  uu____16 = i;
+                  uu____19 = j;
+                  uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                                  uint8_t, uint8_t *);
+                  uu____17 = (size_t)uu____18;
+                  hint[uu____16][uu____17] = (int32_t)1;
+                  j++;
+                }
+              } else {
+                break;
               }
             }
-            uu____20 = malformed_hint;
-            if (!uu____20) {
-              uu____21 = current_true_hints_seen;
-              previous_true_hints_seen = uu____21;
-              i++;
-            }
-            continue;
           }
+          uu____20 = malformed_hint;
+          if (!uu____20) {
+            uu____21 = current_true_hints_seen;
+            previous_true_hints_seen = uu____21;
+            i++;
+          }
+          continue;
         }
-        malformed_hint = true;
-        j = previous_true_hints_seen;
-        while (true) {
-          uu____2 = malformed_hint;
-          if (uu____2) {
-            break;
-          } else {
-            uu____4 = j;
-            uu____5 = current_true_hints_seen;
-            uu____3 = uu____4 < uu____5;
-            if (uu____3) {
-              uu____7 = j;
-              uu____8 = previous_true_hints_seen;
-              uu____6 = uu____7 > uu____8;
-              if (uu____6) {
-                uu____11 = j;
-                uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
-                                                uint8_t, uint8_t *);
-                uu____14 = j;
-                uu____13 = uu____14 - (size_t)1U;
-                uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
-                                                uint8_t, uint8_t *);
-                uu____9 = uu____10 <= uu____12;
-                if (uu____9) {
-                  malformed_hint = true;
-                  uu____15 = malformed_hint;
-                  if (!uu____15) {
-                    uu____16 = i;
-                    uu____19 = j;
-                    uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
-                                                    uint8_t, uint8_t *);
-                    uu____17 = (size_t)uu____18;
-                    hint[uu____16][uu____17] = (int32_t)1;
-                    j++;
-                  }
-                  continue;
+      }
+      malformed_hint = true;
+      j = previous_true_hints_seen;
+      while (true) {
+        uu____2 = malformed_hint;
+        if (uu____2) {
+          break;
+        } else {
+          uu____4 = j;
+          uu____5 = current_true_hints_seen;
+          uu____3 = uu____4 < uu____5;
+          if (uu____3) {
+            uu____7 = j;
+            uu____8 = previous_true_hints_seen;
+            uu____6 = uu____7 > uu____8;
+            if (uu____6) {
+              uu____11 = j;
+              uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
+                                              uint8_t, uint8_t *);
+              uu____14 = j;
+              uu____13 = uu____14 - (size_t)1U;
+              uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
+                                              uint8_t, uint8_t *);
+              uu____9 = uu____10 <= uu____12;
+              if (uu____9) {
+                malformed_hint = true;
+                uu____15 = malformed_hint;
+                if (!uu____15) {
+                  uu____16 = i;
+                  uu____19 = j;
+                  uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                                  uint8_t, uint8_t *);
+                  uu____17 = (size_t)uu____18;
+                  hint[uu____16][uu____17] = (int32_t)1;
+                  j++;
                 }
+                continue;
               }
-              uu____15 = malformed_hint;
-              if (!uu____15) {
-                uu____16 = i;
-                uu____19 = j;
-                uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
-                                                uint8_t, uint8_t *);
-                uu____17 = (size_t)uu____18;
-                hint[uu____16][uu____17] = (int32_t)1;
-                j++;
-              }
-            } else {
-              break;
             }
+            uu____15 = malformed_hint;
+            if (!uu____15) {
+              uu____16 = i;
+              uu____19 = j;
+              uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                              uint8_t, uint8_t *);
+              uu____17 = (size_t)uu____18;
+              hint[uu____16][uu____17] = (int32_t)1;
+              j++;
+            }
+          } else {
+            break;
           }
         }
-        uu____20 = malformed_hint;
-        if (!uu____20) {
-          uu____21 = current_true_hints_seen;
-          previous_true_hints_seen = uu____21;
-          i++;
-        }
       }
-    } else {
-      break;
+      uu____20 = malformed_hint;
+      if (!uu____20) {
+        uu____21 = current_true_hints_seen;
+        previous_true_hints_seen = uu____21;
+        i++;
+      }
     }
   }
   i = previous_true_hints_seen;
-  while (true) {
-    if (i < (size_t)55U) {
-      if (malformed_hint) {
-        break;
-      } else {
-        if (Eurydice_slice_index(hint_serialized, i, uint8_t, uint8_t *) !=
-            0U) {
-          malformed_hint = true;
-        }
-        i++;
-      }
-    } else {
+  while (i < (size_t)55U) {
+    if (malformed_hint) {
       break;
+    } else {
+      if (Eurydice_slice_index(hint_serialized, i, uint8_t, uint8_t *) != 0U) {
+        malformed_hint = true;
+      }
+      i++;
     }
   }
-  Result_ef0 uu____22;
-  if (malformed_hint) {
-    uu____22 = (CLITERAL(Result_ef0){
-        .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_MalformedHintError}});
-  } else {
-    uint8_t uu____23[48U];
+  if (!malformed_hint) {
+    uint8_t uu____22[48U];
     Result_ae dst;
     Eurydice_slice_to_array2(&dst, commitment_hash, Eurydice_slice,
                              uint8_t[48U]);
-    unwrap_26_28(dst, uu____23);
+    unwrap_26_28(dst, uu____22);
     /* Passing arrays by value in Rust generates a copy in C */
     libcrux_ml_dsa_polynomial_PolynomialRingElement_24
         copy_of_signer_response[5U];
@@ -7385,16 +7344,19 @@ libcrux_ml_dsa_encoding_signature_deserialize_92_cc(uint8_t *serialized) {
     memcpy(copy_of_hint, hint, (size_t)6U * sizeof(int32_t[256U]));
     Result_ef0 lit;
     lit.tag = Ok;
-    memcpy(lit.val.case_Ok.commitment_hash, uu____23,
+    memcpy(lit.val.case_Ok.commitment_hash, uu____22,
            (size_t)48U * sizeof(uint8_t));
     memcpy(lit.val.case_Ok.signer_response, copy_of_signer_response,
            (size_t)5U *
                sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_24));
     memcpy(lit.val.case_Ok.hint, copy_of_hint,
            (size_t)6U * sizeof(int32_t[256U]));
-    uu____22 = lit;
+    return lit;
   }
-  return uu____22;
+  return (CLITERAL(Result_ef0){
+      .tag = Err,
+      .val = {.case_Err =
+                  libcrux_ml_dsa_types_VerificationError_MalformedHintError}});
 }
 
 /**
@@ -7669,7 +7631,8 @@ libcrux_ml_dsa_ml_dsa_generic_verify_internal_44(
             uu____3, ((int32_t)2 << (uint32_t)(size_t)19U) - (int32_t)196)) {
       uu____2 = (CLITERAL(Result_41){
           .tag = Err,
-          .f0 = libcrux_ml_dsa_types_SignerResponseExceedsBoundError});
+          .f0 =
+              libcrux_ml_dsa_types_VerificationError_SignerResponseExceedsBoundError});
     } else {
       libcrux_ml_dsa_polynomial_PolynomialRingElement_24 A_as_ntt[6U][5U];
       uint8_t ret[34U];
@@ -7744,7 +7707,8 @@ libcrux_ml_dsa_ml_dsa_generic_verify_internal_44(
       } else {
         uu____2 = (CLITERAL(Result_41){
             .tag = Err,
-            .f0 = libcrux_ml_dsa_types_CommitmentHashesDontMatchError});
+            .f0 =
+                libcrux_ml_dsa_types_VerificationError_CommitmentHashesDontMatchError});
       }
     }
   } else {
@@ -7781,21 +7745,19 @@ static KRML_MUSTINLINE Result_41 libcrux_ml_dsa_ml_dsa_generic_verify_44(
     Eurydice_slice context, uint8_t *signature_serialized) {
   Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_45(
       context, (CLITERAL(Option_30){.tag = None}));
-  Result_41 uu____1;
-  if (uu____0.tag == Ok) {
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
-        dsc;
-    uu____1 = libcrux_ml_dsa_ml_dsa_generic_verify_internal_44(
-        verification_key_serialized, message,
-        (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
-        signature_serialized);
-  } else {
-    uu____1 = (CLITERAL(Result_41){
+  if (!(uu____0.tag == Ok)) {
+    return (CLITERAL(Result_41){
         .tag = Err,
-        .f0 = libcrux_ml_dsa_types_VerificationContextTooLongError});
+        .f0 =
+            libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError});
   }
-  return uu____1;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+      dsc;
+  return libcrux_ml_dsa_ml_dsa_generic_verify_internal_44(
+      verification_key_serialized, message,
+      (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
+      signature_serialized);
 }
 
 /**
@@ -7912,22 +7874,20 @@ libcrux_ml_dsa_ml_dsa_generic_verify_pre_hashed_f8(
   libcrux_ml_dsa_pre_hash_oid_bd(ret);
   memcpy(lit.f0, ret, (size_t)11U * sizeof(uint8_t));
   Result_a8 uu____1 = libcrux_ml_dsa_pre_hash_new_45(uu____0, lit);
-  Result_41 uu____2;
-  if (uu____1.tag == Ok) {
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____1.val.case_Ok;
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
-        dsc;
-    uu____2 = libcrux_ml_dsa_ml_dsa_generic_verify_internal_44(
-        verification_key_serialized,
-        Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t),
-        (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
-        signature_serialized);
-  } else {
-    uu____2 = (CLITERAL(Result_41){
+  if (!(uu____1.tag == Ok)) {
+    return (CLITERAL(Result_41){
         .tag = Err,
-        .f0 = libcrux_ml_dsa_types_VerificationContextTooLongError});
-  }
-  return uu____2;
+        .f0 =
+            libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError});
+  }
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____1.val.case_Ok;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+      dsc;
+  return libcrux_ml_dsa_ml_dsa_generic_verify_internal_44(
+      verification_key_serialized,
+      Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t),
+      (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
+      signature_serialized);
 }
 
 /**
diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h
index 13e99f9fc..d3684f384 100644
--- a/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h
+++ b/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mldsa65_portable_H
@@ -536,7 +536,7 @@ typedef struct libcrux_ml_dsa_pre_hash_DomainSeparationContext_s {
   Option_30 pre_hash_oid;
 } libcrux_ml_dsa_pre_hash_DomainSeparationContext;
 
-#define libcrux_ml_dsa_pre_hash_ContextTooLongError 0
+#define libcrux_ml_dsa_pre_hash_DomainSeparationError_ContextTooLongError 0
 
 typedef uint8_t libcrux_ml_dsa_pre_hash_DomainSeparationError;
 
@@ -563,19 +563,18 @@ This function found in impl
 */
 static inline Result_a8 libcrux_ml_dsa_pre_hash_new_45(Eurydice_slice context,
                                                        Option_30 pre_hash_oid) {
-  Result_a8 uu____0;
-  if (Eurydice_slice_len(context, uint8_t) >
-      LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN) {
-    uu____0 = (CLITERAL(Result_a8){
-        .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_pre_hash_ContextTooLongError}});
-  } else {
-    uu____0 = (CLITERAL(Result_a8){
+  if (!(Eurydice_slice_len(context, uint8_t) >
+        LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN)) {
+    return (CLITERAL(Result_a8){
         .tag = Ok,
         .val = {
             .case_Ok = {.context = context, .pre_hash_oid = pre_hash_oid}}});
   }
-  return uu____0;
+  return (CLITERAL(Result_a8){
+      .tag = Err,
+      .val = {
+          .case_Err =
+              libcrux_ml_dsa_pre_hash_DomainSeparationError_ContextTooLongError}});
 }
 
 /**
@@ -654,9 +653,6 @@ static inline void libcrux_ml_dsa_pre_hash_oid_bd(uint8_t ret[11U]) {
          (size_t)11U * sizeof(uint8_t));
 }
 
-typedef struct libcrux_ml_dsa_pre_hash_SHAKE128_PH_s {
-} libcrux_ml_dsa_pre_hash_SHAKE128_PH;
-
 typedef struct libcrux_ml_dsa_simd_portable_vector_type_PortableSIMDUnit_s {
   int32_t coefficients[8U];
 } libcrux_ml_dsa_simd_portable_vector_type_PortableSIMDUnit;
@@ -4163,9 +4159,6 @@ static inline void libcrux_ml_dsa_simd_portable_invert_ntt_montgomery_36(
              sizeof(libcrux_ml_dsa_simd_portable_vector_type_PortableSIMDUnit));
 }
 
-typedef struct libcrux_ml_dsa_samplex4_portable_PortableSampler_s {
-} libcrux_ml_dsa_samplex4_portable_PortableSampler;
-
 /**
 A monomorphic instance of K.
 with types uint8_t[4032size_t], uint8_t[1952size_t]
@@ -7125,22 +7118,18 @@ libcrux_ml_dsa.simd.portable.arithmetic.compute_one_hint with const generics
 static KRML_MUSTINLINE int32_t
 libcrux_ml_dsa_simd_portable_arithmetic_compute_one_hint_80(int32_t low,
                                                             int32_t high) {
-  int32_t uu____0;
   if (!(low > (int32_t)261888)) {
     if (!(low < -(int32_t)261888)) {
       if (low == -(int32_t)261888) {
         if (!(high != (int32_t)0)) {
-          uu____0 = (int32_t)0;
-          return uu____0;
+          return (int32_t)0;
         }
       } else {
-        uu____0 = (int32_t)0;
-        return uu____0;
+        return (int32_t)0;
       }
     }
   }
-  uu____0 = (int32_t)1;
-  return uu____0;
+  return (int32_t)1;
 }
 
 /**
@@ -7473,184 +7462,174 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
   Option_67 commitment_hash0 = {.tag = None};
   Option_f3 signer_response0 = {.tag = None};
   Option_f0 hint0 = {.tag = None};
-  while (true) {
-    if (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) {
-      attempt++;
-      uint8_t uu____2[66U];
-      libcrux_ml_dsa_utils_into_padded_array_20(
-          Eurydice_array_to_slice((size_t)64U, mask_seed, uint8_t), uu____2);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b mask[5U];
-      libcrux_ml_dsa_sample_sample_mask_vector_0e(
-          uu____2, &domain_separator_for_mask, mask);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b A_times_mask[6U];
-      libcrux_ml_dsa_matrix_compute_A_times_mask_2f(A_as_ntt, mask,
-                                                    A_times_mask);
-      /* Passing arrays by value in Rust generates a copy in C */
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-          copy_of_A_times_mask[6U];
-      memcpy(copy_of_A_times_mask, A_times_mask,
-             (size_t)6U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_libcrux_ml_dsa_simd_portable_vector_type_PortableSIMDUnit_6size_t__x2
-          uu____4 = libcrux_ml_dsa_arithmetic_decompose_vector_2f(
-              copy_of_A_times_mask);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b w0[6U];
-      memcpy(w0, uu____4.fst,
-             (size_t)6U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b commitment[6U];
-      memcpy(commitment, uu____4.snd,
-             (size_t)6U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-      uint8_t commitment_hash_candidate[48U] = {0U};
+  while (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) {
+    attempt++;
+    uint8_t uu____2[66U];
+    libcrux_ml_dsa_utils_into_padded_array_20(
+        Eurydice_array_to_slice((size_t)64U, mask_seed, uint8_t), uu____2);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b mask[5U];
+    libcrux_ml_dsa_sample_sample_mask_vector_0e(
+        uu____2, &domain_separator_for_mask, mask);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b A_times_mask[6U];
+    libcrux_ml_dsa_matrix_compute_A_times_mask_2f(A_as_ntt, mask, A_times_mask);
+    /* Passing arrays by value in Rust generates a copy in C */
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b copy_of_A_times_mask[6U];
+    memcpy(copy_of_A_times_mask, A_times_mask,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_libcrux_ml_dsa_simd_portable_vector_type_PortableSIMDUnit_6size_t__x2
+        uu____4 =
+            libcrux_ml_dsa_arithmetic_decompose_vector_2f(copy_of_A_times_mask);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b w0[6U];
+    memcpy(w0, uu____4.fst,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b commitment[6U];
+    memcpy(commitment, uu____4.snd,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
+    uint8_t commitment_hash_candidate[48U] = {0U};
+    /* Passing arrays by value in Rust generates a copy in C */
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b copy_of_commitment0[6U];
+    memcpy(copy_of_commitment0, commitment,
+           (size_t)6U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
+    uint8_t commitment_serialized[768U];
+    libcrux_ml_dsa_encoding_commitment_serialize_vector_5d(
+        copy_of_commitment0, commitment_serialized);
+    libcrux_sha3_portable_incremental_Shake256Xof shake =
+        libcrux_ml_dsa_hash_functions_portable_init_83();
+    libcrux_ml_dsa_hash_functions_portable_absorb_83(
+        &shake,
+        Eurydice_array_to_slice((size_t)64U, message_representative, uint8_t));
+    libcrux_ml_dsa_hash_functions_portable_absorb_final_83(
+        &shake,
+        Eurydice_array_to_slice((size_t)768U, commitment_serialized, uint8_t));
+    libcrux_ml_dsa_hash_functions_portable_squeeze_83(
+        &shake, Eurydice_array_to_slice((size_t)48U, commitment_hash_candidate,
+                                        uint8_t));
+    /* Passing arrays by value in Rust generates a copy in C */
+    uint8_t copy_of_commitment_hash_candidate[48U];
+    memcpy(copy_of_commitment_hash_candidate, commitment_hash_candidate,
+           (size_t)48U * sizeof(uint8_t));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
+        verifier_challenge_as_ntt = libcrux_ml_dsa_ntt_ntt_ba(
+            libcrux_ml_dsa_sample_sample_challenge_ring_element_83(
+                copy_of_commitment_hash_candidate));
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b challenge_times_s1[5U];
+    libcrux_ml_dsa_matrix_vector_times_ring_element_4f(
+        s1_as_ntt, &verifier_challenge_as_ntt, challenge_times_s1);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b challenge_times_s2[6U];
+    libcrux_ml_dsa_matrix_vector_times_ring_element_07(
+        s2_as_ntt, &verifier_challenge_as_ntt, challenge_times_s2);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
+        signer_response_candidate[5U];
+    libcrux_ml_dsa_matrix_add_vectors_4f(mask, challenge_times_s1,
+                                         signer_response_candidate);
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
+        w0_minus_challenge_times_s2[6U];
+    libcrux_ml_dsa_matrix_subtract_vectors_07(w0, challenge_times_s2,
+                                              w0_minus_challenge_times_s2);
+    /* Passing arrays by value in Rust generates a copy in C */
+    libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
+        copy_of_signer_response_candidate[5U];
+    memcpy(copy_of_signer_response_candidate, signer_response_candidate,
+           (size_t)5U *
+               sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
+    if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_4f(
+            copy_of_signer_response_candidate,
+            ((int32_t)1 << (uint32_t)(size_t)19U) - BETA)) {
       /* Passing arrays by value in Rust generates a copy in C */
       libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-          copy_of_commitment0[6U];
-      memcpy(copy_of_commitment0, commitment,
+          copy_of_w0_minus_challenge_times_s2[6U];
+      memcpy(copy_of_w0_minus_challenge_times_s2, w0_minus_challenge_times_s2,
              (size_t)6U *
                  sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-      uint8_t commitment_serialized[768U];
-      libcrux_ml_dsa_encoding_commitment_serialize_vector_5d(
-          copy_of_commitment0, commitment_serialized);
-      libcrux_sha3_portable_incremental_Shake256Xof shake =
-          libcrux_ml_dsa_hash_functions_portable_init_83();
-      libcrux_ml_dsa_hash_functions_portable_absorb_83(
-          &shake, Eurydice_array_to_slice((size_t)64U, message_representative,
-                                          uint8_t));
-      libcrux_ml_dsa_hash_functions_portable_absorb_final_83(
-          &shake, Eurydice_array_to_slice((size_t)768U, commitment_serialized,
-                                          uint8_t));
-      libcrux_ml_dsa_hash_functions_portable_squeeze_83(
-          &shake, Eurydice_array_to_slice((size_t)48U,
-                                          commitment_hash_candidate, uint8_t));
-      /* Passing arrays by value in Rust generates a copy in C */
-      uint8_t copy_of_commitment_hash_candidate[48U];
-      memcpy(copy_of_commitment_hash_candidate, commitment_hash_candidate,
-             (size_t)48U * sizeof(uint8_t));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-          verifier_challenge_as_ntt = libcrux_ml_dsa_ntt_ntt_ba(
-              libcrux_ml_dsa_sample_sample_challenge_ring_element_83(
-                  copy_of_commitment_hash_candidate));
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b challenge_times_s1[5U];
-      libcrux_ml_dsa_matrix_vector_times_ring_element_4f(
-          s1_as_ntt, &verifier_challenge_as_ntt, challenge_times_s1);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b challenge_times_s2[6U];
-      libcrux_ml_dsa_matrix_vector_times_ring_element_07(
-          s2_as_ntt, &verifier_challenge_as_ntt, challenge_times_s2);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-          signer_response_candidate[5U];
-      libcrux_ml_dsa_matrix_add_vectors_4f(mask, challenge_times_s1,
-                                           signer_response_candidate);
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-          w0_minus_challenge_times_s2[6U];
-      libcrux_ml_dsa_matrix_subtract_vectors_07(w0, challenge_times_s2,
-                                                w0_minus_challenge_times_s2);
-      /* Passing arrays by value in Rust generates a copy in C */
-      libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-          copy_of_signer_response_candidate[5U];
-      memcpy(copy_of_signer_response_candidate, signer_response_candidate,
-             (size_t)5U *
-                 sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-      if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_4f(
-              copy_of_signer_response_candidate,
-              ((int32_t)1 << (uint32_t)(size_t)19U) - BETA)) {
+      if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_07(
+              copy_of_w0_minus_challenge_times_s2, (int32_t)261888 - BETA)) {
+        libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
+            challenge_times_t0[6U];
+        libcrux_ml_dsa_matrix_vector_times_ring_element_07(
+            t0_as_ntt, &verifier_challenge_as_ntt, challenge_times_t0);
         /* Passing arrays by value in Rust generates a copy in C */
         libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-            copy_of_w0_minus_challenge_times_s2[6U];
-        memcpy(copy_of_w0_minus_challenge_times_s2, w0_minus_challenge_times_s2,
+            copy_of_challenge_times_t0[6U];
+        memcpy(copy_of_challenge_times_t0, challenge_times_t0,
                (size_t)6U *
                    sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
         if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_07(
-                copy_of_w0_minus_challenge_times_s2, (int32_t)261888 - BETA)) {
+                copy_of_challenge_times_t0, (int32_t)261888)) {
           libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-              challenge_times_t0[6U];
-          libcrux_ml_dsa_matrix_vector_times_ring_element_07(
-              t0_as_ntt, &verifier_challenge_as_ntt, challenge_times_t0);
+              w0_minus_c_times_s2_plus_c_times_t0[6U];
+          libcrux_ml_dsa_matrix_add_vectors_07(
+              w0_minus_challenge_times_s2, challenge_times_t0,
+              w0_minus_c_times_s2_plus_c_times_t0);
           /* Passing arrays by value in Rust generates a copy in C */
           libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-              copy_of_challenge_times_t0[6U];
+              copy_of_w0_minus_c_times_s2_plus_c_times_t0[6U];
           memcpy(
-              copy_of_challenge_times_t0, challenge_times_t0,
+              copy_of_w0_minus_c_times_s2_plus_c_times_t0,
+              w0_minus_c_times_s2_plus_c_times_t0,
               (size_t)6U *
                   sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-          if (!libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_07(
-                  copy_of_challenge_times_t0, (int32_t)261888)) {
-            libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-                w0_minus_c_times_s2_plus_c_times_t0[6U];
-            libcrux_ml_dsa_matrix_add_vectors_07(
-                w0_minus_challenge_times_s2, challenge_times_t0,
-                w0_minus_c_times_s2_plus_c_times_t0);
+          /* Passing arrays by value in Rust generates a copy in C */
+          libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
+              copy_of_commitment[6U];
+          memcpy(
+              copy_of_commitment, commitment,
+              (size_t)6U *
+                  sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
+          tuple_e6 uu____12 = libcrux_ml_dsa_arithmetic_make_hint_2f(
+              copy_of_w0_minus_c_times_s2_plus_c_times_t0, copy_of_commitment);
+          int32_t hint_candidate[6U][256U];
+          memcpy(hint_candidate, uu____12.fst,
+                 (size_t)6U * sizeof(int32_t[256U]));
+          size_t ones_in_hint = uu____12.snd;
+          if (!(ones_in_hint > (size_t)55U)) {
+            attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN;
+            /* Passing arrays by value in Rust generates a copy in C */
+            uint8_t copy_of_commitment_hash_candidate0[48U];
+            memcpy(copy_of_commitment_hash_candidate0,
+                   commitment_hash_candidate, (size_t)48U * sizeof(uint8_t));
+            Option_67 lit0;
+            lit0.tag = Some;
+            memcpy(lit0.f0, copy_of_commitment_hash_candidate0,
+                   (size_t)48U * sizeof(uint8_t));
+            commitment_hash0 = lit0;
             /* Passing arrays by value in Rust generates a copy in C */
             libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-                copy_of_w0_minus_c_times_s2_plus_c_times_t0[6U];
+                copy_of_signer_response_candidate0[5U];
             memcpy(
-                copy_of_w0_minus_c_times_s2_plus_c_times_t0,
-                w0_minus_c_times_s2_plus_c_times_t0,
-                (size_t)6U *
+                copy_of_signer_response_candidate0, signer_response_candidate,
+                (size_t)5U *
                     sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-            /* Passing arrays by value in Rust generates a copy in C */
-            libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-                copy_of_commitment[6U];
+            Option_f3 lit1;
+            lit1.tag = Some;
             memcpy(
-                copy_of_commitment, commitment,
-                (size_t)6U *
+                lit1.f0, copy_of_signer_response_candidate0,
+                (size_t)5U *
                     sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-            tuple_e6 uu____12 = libcrux_ml_dsa_arithmetic_make_hint_2f(
-                copy_of_w0_minus_c_times_s2_plus_c_times_t0,
-                copy_of_commitment);
-            int32_t hint_candidate[6U][256U];
-            memcpy(hint_candidate, uu____12.fst,
+            signer_response0 = lit1;
+            /* Passing arrays by value in Rust generates a copy in C */
+            int32_t copy_of_hint_candidate[6U][256U];
+            memcpy(copy_of_hint_candidate, hint_candidate,
                    (size_t)6U * sizeof(int32_t[256U]));
-            size_t ones_in_hint = uu____12.snd;
-            if (!(ones_in_hint > (size_t)55U)) {
-              attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN;
-              /* Passing arrays by value in Rust generates a copy in C */
-              uint8_t copy_of_commitment_hash_candidate0[48U];
-              memcpy(copy_of_commitment_hash_candidate0,
-                     commitment_hash_candidate, (size_t)48U * sizeof(uint8_t));
-              Option_67 lit0;
-              lit0.tag = Some;
-              memcpy(lit0.f0, copy_of_commitment_hash_candidate0,
-                     (size_t)48U * sizeof(uint8_t));
-              commitment_hash0 = lit0;
-              /* Passing arrays by value in Rust generates a copy in C */
-              libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
-                  copy_of_signer_response_candidate0[5U];
-              memcpy(
-                  copy_of_signer_response_candidate0, signer_response_candidate,
-                  (size_t)5U *
-                      sizeof(
-                          libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-              Option_f3 lit1;
-              lit1.tag = Some;
-              memcpy(
-                  lit1.f0, copy_of_signer_response_candidate0,
-                  (size_t)5U *
-                      sizeof(
-                          libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
-              signer_response0 = lit1;
-              /* Passing arrays by value in Rust generates a copy in C */
-              int32_t copy_of_hint_candidate[6U][256U];
-              memcpy(copy_of_hint_candidate, hint_candidate,
-                     (size_t)6U * sizeof(int32_t[256U]));
-              Option_f0 lit;
-              lit.tag = Some;
-              memcpy(lit.f0, copy_of_hint_candidate,
-                     (size_t)6U * sizeof(int32_t[256U]));
-              hint0 = lit;
-            }
+            Option_f0 lit;
+            lit.tag = Some;
+            memcpy(lit.f0, copy_of_hint_candidate,
+                   (size_t)6U * sizeof(int32_t[256U]));
+            hint0 = lit;
           }
         }
       }
-    } else {
-      break;
     }
   }
   Result_2e uu____16;
   if (commitment_hash0.tag == None) {
     uu____16 = (CLITERAL(Result_2e){
         .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_RejectionSamplingError}});
+        .val = {.case_Err =
+                    libcrux_ml_dsa_types_SigningError_RejectionSamplingError}});
   } else {
     uint8_t commitment_hash1[48U];
     memcpy(commitment_hash1, commitment_hash0.f0,
@@ -7660,7 +7639,9 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
     if (signer_response0.tag == None) {
       uu____16 = (CLITERAL(Result_2e){
           .tag = Err,
-          .val = {.case_Err = libcrux_ml_dsa_types_RejectionSamplingError}});
+          .val = {
+              .case_Err =
+                  libcrux_ml_dsa_types_SigningError_RejectionSamplingError}});
     } else {
       libcrux_ml_dsa_polynomial_PolynomialRingElement_9b signer_response1[5U];
       memcpy(signer_response1, signer_response0.f0,
@@ -7673,7 +7654,9 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
       if (hint0.tag == None) {
         uu____16 = (CLITERAL(Result_2e){
             .tag = Err,
-            .val = {.case_Err = libcrux_ml_dsa_types_RejectionSamplingError}});
+            .val = {
+                .case_Err =
+                    libcrux_ml_dsa_types_SigningError_RejectionSamplingError}});
       } else {
         int32_t hint1[6U][256U];
         memcpy(hint1, hint0.f0, (size_t)6U * sizeof(int32_t[256U]));
@@ -7700,15 +7683,16 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
                (size_t)5U *
                    sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
         memcpy(lit0.hint, copy_of_hint, (size_t)6U * sizeof(int32_t[256U]));
-        libcrux_ml_dsa_encoding_signature_serialize_92_76(&lit0, signature);
+        /* original Rust expression is not an lvalue in C */
+        libcrux_ml_dsa_encoding_signature_Signature_44 lvalue = lit0;
+        libcrux_ml_dsa_encoding_signature_serialize_92_76(&lvalue, signature);
         /* Passing arrays by value in Rust generates a copy in C */
         uint8_t copy_of_signature[3309U];
         memcpy(copy_of_signature, signature, (size_t)3309U * sizeof(uint8_t));
         Result_2e lit;
         lit.tag = Ok;
         lit.val.case_Ok = libcrux_ml_dsa_types_new_8f_fa(copy_of_signature);
-        uu____16 = lit;
-        return uu____16;
+        return lit;
       }
     }
   }
@@ -7743,25 +7727,23 @@ static KRML_MUSTINLINE Result_2e libcrux_ml_dsa_ml_dsa_generic_sign_3f(
     uint8_t randomness[32U]) {
   Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_45(
       context, (CLITERAL(Option_30){.tag = None}));
-  Result_2e uu____1;
-  if (uu____0.tag == Ok) {
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
-        dsc;
-    uint8_t *uu____2 = signing_key;
-    Eurydice_slice uu____3 = message;
-    Option_84 uu____4 = {.tag = Some, .f0 = domain_separation_context};
-    /* Passing arrays by value in Rust generates a copy in C */
-    uint8_t copy_of_randomness[32U];
-    memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-    uu____1 = libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
-        uu____2, uu____3, uu____4, copy_of_randomness);
-  } else {
-    uu____1 = (CLITERAL(Result_2e){
+  if (!(uu____0.tag == Ok)) {
+    return (CLITERAL(Result_2e){
         .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_ContextTooLongError}});
-  }
-  return uu____1;
+        .val = {.case_Err =
+                    libcrux_ml_dsa_types_SigningError_ContextTooLongError}});
+  }
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+      dsc;
+  uint8_t *uu____1 = signing_key;
+  Eurydice_slice uu____2 = message;
+  Option_84 uu____3 = {.tag = Some, .f0 = domain_separation_context};
+  /* Passing arrays by value in Rust generates a copy in C */
+  uint8_t copy_of_randomness[32U];
+  memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+  return libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
+      uu____1, uu____2, uu____3, copy_of_randomness);
 }
 
 /**
@@ -7893,42 +7875,40 @@ libcrux_ml_dsa_ml_dsa_generic_sign_pre_hashed_da(uint8_t *signing_key,
                                                  Eurydice_slice message,
                                                  Eurydice_slice context,
                                                  uint8_t randomness[32U]) {
-  Result_2e uu____0;
-  if (Eurydice_slice_len(context, uint8_t) >
-      LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN) {
-    uu____0 = (CLITERAL(Result_2e){
-        .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_ContextTooLongError}});
-  } else {
+  if (!(Eurydice_slice_len(context, uint8_t) >
+        LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN)) {
     uint8_t pre_hashed_message[256U];
     libcrux_ml_dsa_pre_hash_hash_bd_54(message, pre_hashed_message);
-    Eurydice_slice uu____1 = context;
+    Eurydice_slice uu____0 = context;
     Option_30 lit;
     lit.tag = Some;
     uint8_t ret[11U];
     libcrux_ml_dsa_pre_hash_oid_bd(ret);
     memcpy(lit.f0, ret, (size_t)11U * sizeof(uint8_t));
-    Result_a8 uu____2 = libcrux_ml_dsa_pre_hash_new_45(uu____1, lit);
-    if (uu____2.tag == Ok) {
-      libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____2.val.case_Ok;
-      libcrux_ml_dsa_pre_hash_DomainSeparationContext
-          domain_separation_context = dsc;
-      uint8_t *uu____3 = signing_key;
-      Eurydice_slice uu____4 =
-          Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t);
-      Option_84 uu____5 = {.tag = Some, .f0 = domain_separation_context};
-      /* Passing arrays by value in Rust generates a copy in C */
-      uint8_t copy_of_randomness[32U];
-      memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
-      uu____0 = libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
-          uu____3, uu____4, uu____5, copy_of_randomness);
-    } else {
-      uu____0 = (CLITERAL(Result_2e){
+    Result_a8 uu____1 = libcrux_ml_dsa_pre_hash_new_45(uu____0, lit);
+    if (!(uu____1.tag == Ok)) {
+      return (CLITERAL(Result_2e){
           .tag = Err,
-          .val = {.case_Err = libcrux_ml_dsa_types_ContextTooLongError}});
+          .val = {.case_Err =
+                      libcrux_ml_dsa_types_SigningError_ContextTooLongError}});
     }
+    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____1.val.case_Ok;
+    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+        dsc;
+    uint8_t *uu____2 = signing_key;
+    Eurydice_slice uu____3 =
+        Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t);
+    Option_84 uu____4 = {.tag = Some, .f0 = domain_separation_context};
+    /* Passing arrays by value in Rust generates a copy in C */
+    uint8_t copy_of_randomness[32U];
+    memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t));
+    return libcrux_ml_dsa_ml_dsa_generic_sign_internal_3f(
+        uu____2, uu____3, uu____4, copy_of_randomness);
   }
-  return uu____0;
+  return (CLITERAL(Result_2e){
+      .tag = Err,
+      .val = {.case_Err =
+                  libcrux_ml_dsa_types_SigningError_ContextTooLongError}});
 }
 
 /**
@@ -8131,188 +8111,174 @@ libcrux_ml_dsa_encoding_signature_deserialize_92_76(uint8_t *serialized) {
   size_t previous_true_hints_seen = (size_t)0U;
   size_t i = (size_t)0U;
   bool malformed_hint = false;
-  while (true) {
-    if (i < (size_t)6U) {
-      if (malformed_hint) {
-        break;
-      } else {
-        size_t current_true_hints_seen = (size_t)Eurydice_slice_index(
-            hint_serialized, (size_t)55U + i, uint8_t, uint8_t *);
-        size_t j;
-        bool uu____2;
-        bool uu____3;
-        size_t uu____4;
-        size_t uu____5;
-        bool uu____6;
-        size_t uu____7;
-        size_t uu____8;
-        bool uu____9;
-        uint8_t uu____10;
-        size_t uu____11;
-        uint8_t uu____12;
-        size_t uu____13;
-        size_t uu____14;
-        bool uu____15;
-        size_t uu____16;
-        size_t uu____17;
-        uint8_t uu____18;
-        size_t uu____19;
-        bool uu____20;
-        size_t uu____21;
-        if (!(current_true_hints_seen < previous_true_hints_seen)) {
-          if (!(previous_true_hints_seen > (size_t)55U)) {
-            j = previous_true_hints_seen;
-            while (true) {
-              uu____2 = malformed_hint;
-              if (uu____2) {
-                break;
-              } else {
-                uu____4 = j;
-                uu____5 = current_true_hints_seen;
-                uu____3 = uu____4 < uu____5;
-                if (uu____3) {
-                  uu____7 = j;
-                  uu____8 = previous_true_hints_seen;
-                  uu____6 = uu____7 > uu____8;
-                  if (uu____6) {
-                    uu____11 = j;
-                    uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
-                                                    uint8_t, uint8_t *);
-                    uu____14 = j;
-                    uu____13 = uu____14 - (size_t)1U;
-                    uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
-                                                    uint8_t, uint8_t *);
-                    uu____9 = uu____10 <= uu____12;
-                    if (uu____9) {
-                      malformed_hint = true;
-                      uu____15 = malformed_hint;
-                      if (!uu____15) {
-                        uu____16 = i;
-                        uu____19 = j;
-                        uu____18 = Eurydice_slice_index(
-                            hint_serialized, uu____19, uint8_t, uint8_t *);
-                        uu____17 = (size_t)uu____18;
-                        hint[uu____16][uu____17] = (int32_t)1;
-                        j++;
-                      }
-                      continue;
+  while (i < (size_t)6U) {
+    if (malformed_hint) {
+      break;
+    } else {
+      size_t current_true_hints_seen = (size_t)Eurydice_slice_index(
+          hint_serialized, (size_t)55U + i, uint8_t, uint8_t *);
+      size_t j;
+      bool uu____2;
+      bool uu____3;
+      size_t uu____4;
+      size_t uu____5;
+      bool uu____6;
+      size_t uu____7;
+      size_t uu____8;
+      bool uu____9;
+      uint8_t uu____10;
+      size_t uu____11;
+      uint8_t uu____12;
+      size_t uu____13;
+      size_t uu____14;
+      bool uu____15;
+      size_t uu____16;
+      size_t uu____17;
+      uint8_t uu____18;
+      size_t uu____19;
+      bool uu____20;
+      size_t uu____21;
+      if (!(current_true_hints_seen < previous_true_hints_seen)) {
+        if (!(previous_true_hints_seen > (size_t)55U)) {
+          j = previous_true_hints_seen;
+          while (true) {
+            uu____2 = malformed_hint;
+            if (uu____2) {
+              break;
+            } else {
+              uu____4 = j;
+              uu____5 = current_true_hints_seen;
+              uu____3 = uu____4 < uu____5;
+              if (uu____3) {
+                uu____7 = j;
+                uu____8 = previous_true_hints_seen;
+                uu____6 = uu____7 > uu____8;
+                if (uu____6) {
+                  uu____11 = j;
+                  uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
+                                                  uint8_t, uint8_t *);
+                  uu____14 = j;
+                  uu____13 = uu____14 - (size_t)1U;
+                  uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
+                                                  uint8_t, uint8_t *);
+                  uu____9 = uu____10 <= uu____12;
+                  if (uu____9) {
+                    malformed_hint = true;
+                    uu____15 = malformed_hint;
+                    if (!uu____15) {
+                      uu____16 = i;
+                      uu____19 = j;
+                      uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                                      uint8_t, uint8_t *);
+                      uu____17 = (size_t)uu____18;
+                      hint[uu____16][uu____17] = (int32_t)1;
+                      j++;
                     }
+                    continue;
                   }
-                  uu____15 = malformed_hint;
-                  if (!uu____15) {
-                    uu____16 = i;
-                    uu____19 = j;
-                    uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
-                                                    uint8_t, uint8_t *);
-                    uu____17 = (size_t)uu____18;
-                    hint[uu____16][uu____17] = (int32_t)1;
-                    j++;
-                  }
-                } else {
-                  break;
                 }
+                uu____15 = malformed_hint;
+                if (!uu____15) {
+                  uu____16 = i;
+                  uu____19 = j;
+                  uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                                  uint8_t, uint8_t *);
+                  uu____17 = (size_t)uu____18;
+                  hint[uu____16][uu____17] = (int32_t)1;
+                  j++;
+                }
+              } else {
+                break;
               }
             }
-            uu____20 = malformed_hint;
-            if (!uu____20) {
-              uu____21 = current_true_hints_seen;
-              previous_true_hints_seen = uu____21;
-              i++;
-            }
-            continue;
           }
+          uu____20 = malformed_hint;
+          if (!uu____20) {
+            uu____21 = current_true_hints_seen;
+            previous_true_hints_seen = uu____21;
+            i++;
+          }
+          continue;
         }
-        malformed_hint = true;
-        j = previous_true_hints_seen;
-        while (true) {
-          uu____2 = malformed_hint;
-          if (uu____2) {
-            break;
-          } else {
-            uu____4 = j;
-            uu____5 = current_true_hints_seen;
-            uu____3 = uu____4 < uu____5;
-            if (uu____3) {
-              uu____7 = j;
-              uu____8 = previous_true_hints_seen;
-              uu____6 = uu____7 > uu____8;
-              if (uu____6) {
-                uu____11 = j;
-                uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
-                                                uint8_t, uint8_t *);
-                uu____14 = j;
-                uu____13 = uu____14 - (size_t)1U;
-                uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
-                                                uint8_t, uint8_t *);
-                uu____9 = uu____10 <= uu____12;
-                if (uu____9) {
-                  malformed_hint = true;
-                  uu____15 = malformed_hint;
-                  if (!uu____15) {
-                    uu____16 = i;
-                    uu____19 = j;
-                    uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
-                                                    uint8_t, uint8_t *);
-                    uu____17 = (size_t)uu____18;
-                    hint[uu____16][uu____17] = (int32_t)1;
-                    j++;
-                  }
-                  continue;
+      }
+      malformed_hint = true;
+      j = previous_true_hints_seen;
+      while (true) {
+        uu____2 = malformed_hint;
+        if (uu____2) {
+          break;
+        } else {
+          uu____4 = j;
+          uu____5 = current_true_hints_seen;
+          uu____3 = uu____4 < uu____5;
+          if (uu____3) {
+            uu____7 = j;
+            uu____8 = previous_true_hints_seen;
+            uu____6 = uu____7 > uu____8;
+            if (uu____6) {
+              uu____11 = j;
+              uu____10 = Eurydice_slice_index(hint_serialized, uu____11,
+                                              uint8_t, uint8_t *);
+              uu____14 = j;
+              uu____13 = uu____14 - (size_t)1U;
+              uu____12 = Eurydice_slice_index(hint_serialized, uu____13,
+                                              uint8_t, uint8_t *);
+              uu____9 = uu____10 <= uu____12;
+              if (uu____9) {
+                malformed_hint = true;
+                uu____15 = malformed_hint;
+                if (!uu____15) {
+                  uu____16 = i;
+                  uu____19 = j;
+                  uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                                  uint8_t, uint8_t *);
+                  uu____17 = (size_t)uu____18;
+                  hint[uu____16][uu____17] = (int32_t)1;
+                  j++;
                 }
+                continue;
               }
-              uu____15 = malformed_hint;
-              if (!uu____15) {
-                uu____16 = i;
-                uu____19 = j;
-                uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
-                                                uint8_t, uint8_t *);
-                uu____17 = (size_t)uu____18;
-                hint[uu____16][uu____17] = (int32_t)1;
-                j++;
-              }
-            } else {
-              break;
             }
+            uu____15 = malformed_hint;
+            if (!uu____15) {
+              uu____16 = i;
+              uu____19 = j;
+              uu____18 = Eurydice_slice_index(hint_serialized, uu____19,
+                                              uint8_t, uint8_t *);
+              uu____17 = (size_t)uu____18;
+              hint[uu____16][uu____17] = (int32_t)1;
+              j++;
+            }
+          } else {
+            break;
           }
         }
-        uu____20 = malformed_hint;
-        if (!uu____20) {
-          uu____21 = current_true_hints_seen;
-          previous_true_hints_seen = uu____21;
-          i++;
-        }
       }
-    } else {
-      break;
+      uu____20 = malformed_hint;
+      if (!uu____20) {
+        uu____21 = current_true_hints_seen;
+        previous_true_hints_seen = uu____21;
+        i++;
+      }
     }
   }
   i = previous_true_hints_seen;
-  while (true) {
-    if (i < (size_t)55U) {
-      if (malformed_hint) {
-        break;
-      } else {
-        if (Eurydice_slice_index(hint_serialized, i, uint8_t, uint8_t *) !=
-            0U) {
-          malformed_hint = true;
-        }
-        i++;
-      }
-    } else {
+  while (i < (size_t)55U) {
+    if (malformed_hint) {
       break;
+    } else {
+      if (Eurydice_slice_index(hint_serialized, i, uint8_t, uint8_t *) != 0U) {
+        malformed_hint = true;
+      }
+      i++;
     }
   }
-  Result_ef uu____22;
-  if (malformed_hint) {
-    uu____22 = (CLITERAL(Result_ef){
-        .tag = Err,
-        .val = {.case_Err = libcrux_ml_dsa_types_MalformedHintError}});
-  } else {
-    uint8_t uu____23[48U];
+  if (!malformed_hint) {
+    uint8_t uu____22[48U];
     Result_ae dst;
     Eurydice_slice_to_array2(&dst, commitment_hash, Eurydice_slice,
                              uint8_t[48U]);
-    unwrap_26_28(dst, uu____23);
+    unwrap_26_28(dst, uu____22);
     /* Passing arrays by value in Rust generates a copy in C */
     libcrux_ml_dsa_polynomial_PolynomialRingElement_9b
         copy_of_signer_response[5U];
@@ -8324,16 +8290,19 @@ libcrux_ml_dsa_encoding_signature_deserialize_92_76(uint8_t *serialized) {
     memcpy(copy_of_hint, hint, (size_t)6U * sizeof(int32_t[256U]));
     Result_ef lit;
     lit.tag = Ok;
-    memcpy(lit.val.case_Ok.commitment_hash, uu____23,
+    memcpy(lit.val.case_Ok.commitment_hash, uu____22,
            (size_t)48U * sizeof(uint8_t));
     memcpy(lit.val.case_Ok.signer_response, copy_of_signer_response,
            (size_t)5U *
                sizeof(libcrux_ml_dsa_polynomial_PolynomialRingElement_9b));
     memcpy(lit.val.case_Ok.hint, copy_of_hint,
            (size_t)6U * sizeof(int32_t[256U]));
-    uu____22 = lit;
+    return lit;
   }
-  return uu____22;
+  return (CLITERAL(Result_ef){
+      .tag = Err,
+      .val = {.case_Err =
+                  libcrux_ml_dsa_types_VerificationError_MalformedHintError}});
 }
 
 /**
@@ -8496,14 +8465,15 @@ libcrux_ml_dsa_simd_portable_arithmetic_use_one_hint_80(int32_t r,
   int32_t r0 = uu____0.fst;
   int32_t r1 = uu____0.snd;
   int32_t uu____1;
-  if (hint == (int32_t)0) {
-    uu____1 = r1;
-  } else if (r0 > (int32_t)0) {
-    uu____1 = (r1 + hint) & (int32_t)15;
-  } else {
-    uu____1 = (r1 - hint) & (int32_t)15;
+  if (!(hint == (int32_t)0)) {
+    if (r0 > (int32_t)0) {
+      uu____1 = (r1 + hint) & (int32_t)15;
+    } else {
+      uu____1 = (r1 - hint) & (int32_t)15;
+    }
+    return uu____1;
   }
-  return uu____1;
+  return r1;
 }
 
 /**
@@ -8638,7 +8608,8 @@ libcrux_ml_dsa_ml_dsa_generic_verify_internal_51(
             uu____3, ((int32_t)2 << (uint32_t)(size_t)19U) - (int32_t)196)) {
       uu____2 = (CLITERAL(Result_41){
           .tag = Err,
-          .f0 = libcrux_ml_dsa_types_SignerResponseExceedsBoundError});
+          .f0 =
+              libcrux_ml_dsa_types_VerificationError_SignerResponseExceedsBoundError});
     } else {
       libcrux_ml_dsa_polynomial_PolynomialRingElement_9b A_as_ntt[6U][5U];
       uint8_t ret[34U];
@@ -8713,7 +8684,8 @@ libcrux_ml_dsa_ml_dsa_generic_verify_internal_51(
       } else {
         uu____2 = (CLITERAL(Result_41){
             .tag = Err,
-            .f0 = libcrux_ml_dsa_types_CommitmentHashesDontMatchError});
+            .f0 =
+                libcrux_ml_dsa_types_VerificationError_CommitmentHashesDontMatchError});
       }
     }
   } else {
@@ -8749,21 +8721,19 @@ static KRML_MUSTINLINE Result_41 libcrux_ml_dsa_ml_dsa_generic_verify_51(
     Eurydice_slice context, uint8_t *signature_serialized) {
   Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_45(
       context, (CLITERAL(Option_30){.tag = None}));
-  Result_41 uu____1;
-  if (uu____0.tag == Ok) {
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
-        dsc;
-    uu____1 = libcrux_ml_dsa_ml_dsa_generic_verify_internal_51(
-        verification_key_serialized, message,
-        (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
-        signature_serialized);
-  } else {
-    uu____1 = (CLITERAL(Result_41){
+  if (!(uu____0.tag == Ok)) {
+    return (CLITERAL(Result_41){
         .tag = Err,
-        .f0 = libcrux_ml_dsa_types_VerificationContextTooLongError});
+        .f0 =
+            libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError});
   }
-  return uu____1;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+      dsc;
+  return libcrux_ml_dsa_ml_dsa_generic_verify_internal_51(
+      verification_key_serialized, message,
+      (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
+      signature_serialized);
 }
 
 /**
@@ -8847,22 +8817,20 @@ libcrux_ml_dsa_ml_dsa_generic_verify_pre_hashed_3b(
   libcrux_ml_dsa_pre_hash_oid_bd(ret);
   memcpy(lit.f0, ret, (size_t)11U * sizeof(uint8_t));
   Result_a8 uu____1 = libcrux_ml_dsa_pre_hash_new_45(uu____0, lit);
-  Result_41 uu____2;
-  if (uu____1.tag == Ok) {
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____1.val.case_Ok;
-    libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
-        dsc;
-    uu____2 = libcrux_ml_dsa_ml_dsa_generic_verify_internal_51(
-        verification_key_serialized,
-        Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t),
-        (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
-        signature_serialized);
-  } else {
-    uu____2 = (CLITERAL(Result_41){
+  if (!(uu____1.tag == Ok)) {
+    return (CLITERAL(Result_41){
         .tag = Err,
-        .f0 = libcrux_ml_dsa_types_VerificationContextTooLongError});
+        .f0 =
+            libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError});
   }
-  return uu____2;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____1.val.case_Ok;
+  libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context =
+      dsc;
+  return libcrux_ml_dsa_ml_dsa_generic_verify_internal_51(
+      verification_key_serialized,
+      Eurydice_array_to_slice((size_t)256U, pre_hashed_message, uint8_t),
+      (CLITERAL(Option_84){.tag = Some, .f0 = domain_separation_context}),
+      signature_serialized);
 }
 
 /**
@@ -8922,7 +8890,7 @@ libcrux_ml_dsa::types::SigningError)#2}
 */
 static inline libcrux_ml_dsa_types_SigningError libcrux_ml_dsa_pre_hash_from_4b(
     libcrux_ml_dsa_pre_hash_DomainSeparationError e) {
-  return libcrux_ml_dsa_types_ContextTooLongError;
+  return libcrux_ml_dsa_types_SigningError_ContextTooLongError;
 }
 
 /**
@@ -8933,7 +8901,7 @@ libcrux_ml_dsa::types::VerificationError)#3}
 static inline libcrux_ml_dsa_types_VerificationError
 libcrux_ml_dsa_pre_hash_from_b6(
     libcrux_ml_dsa_pre_hash_DomainSeparationError e) {
-  return libcrux_ml_dsa_types_VerificationContextTooLongError;
+  return libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError;
 }
 
 /**
@@ -8952,9 +8920,6 @@ typedef int32_t libcrux_ml_dsa_simd_portable_vector_type_FieldElement;
 
 typedef Result_a8 libcrux_ml_dsa_pre_hash_PreHashResult;
 
-typedef struct libcrux_ml_dsa_hash_functions_portable_Shake128_s {
-} libcrux_ml_dsa_hash_functions_portable_Shake128;
-
 #if defined(__cplusplus)
 }
 #endif
diff --git a/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h b/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h
index 876ec6f9b..9da49c8f6 100644
--- a/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h
+++ b/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_avx2_H
diff --git a/libcrux-ml-dsa/cg/libcrux_sha3_portable.h b/libcrux-ml-dsa/cg/libcrux_sha3_portable.h
index ebba16495..892fe9cff 100644
--- a/libcrux-ml-dsa/cg/libcrux_sha3_portable.h
+++ b/libcrux-ml-dsa/cg/libcrux_sha3_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: a68994d00017b76a805d0115ca06c1f2c1805e79
- * Eurydice: b665364a6d86749566ce2d650d13fa12c8fab2c5
- * Karamel: 96572bc631fde691a2aea7bce5a5a3838b3a5968
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
  * F*: b0961063393215ca65927f017720cb365a193833-dirty
- * Libcrux: 00424f6ff03ac7c79f2922ed628bf6a5b8723be3
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_portable_H
@@ -2710,10 +2710,10 @@ static inline void libcrux_sha3_portable_incremental_squeeze_68(
   libcrux_sha3_generic_keccak_squeeze_8b_c6(self, buf);
 }
 
-#define libcrux_sha3_Sha224 0
-#define libcrux_sha3_Sha256 1
-#define libcrux_sha3_Sha384 2
-#define libcrux_sha3_Sha512 3
+#define libcrux_sha3_Algorithm_Sha224 1
+#define libcrux_sha3_Algorithm_Sha256 2
+#define libcrux_sha3_Algorithm_Sha384 3
+#define libcrux_sha3_Algorithm_Sha512 4
 
 typedef uint8_t libcrux_sha3_Algorithm;
 
@@ -2721,31 +2721,16 @@ typedef uint8_t libcrux_sha3_Algorithm;
  Returns the output size of a digest.
 */
 static inline size_t libcrux_sha3_digest_size(libcrux_sha3_Algorithm mode) {
-  size_t uu____0;
-  switch (mode) {
-    case libcrux_sha3_Sha224: {
-      uu____0 = (size_t)28U;
-      break;
-    }
-    case libcrux_sha3_Sha256: {
-      uu____0 = (size_t)32U;
-      break;
-    }
-    case libcrux_sha3_Sha384: {
-      uu____0 = (size_t)48U;
-      break;
-    }
-    case libcrux_sha3_Sha512: {
-      uu____0 = (size_t)64U;
-      break;
-    }
-    default: {
-      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
-                        __LINE__);
-      KRML_HOST_EXIT(253U);
+  if (!(mode == libcrux_sha3_Algorithm_Sha224)) {
+    if (mode == libcrux_sha3_Algorithm_Sha256) {
+      return (size_t)32U;
+    } else if (mode == libcrux_sha3_Algorithm_Sha384) {
+      return (size_t)48U;
+    } else {
+      return (size_t)64U;
     }
   }
-  return uu____0;
+  return (size_t)28U;
 }
 
 /**
@@ -4856,31 +4841,16 @@ This function found in impl {(core::convert::From<libcrux_sha3::Algorithm> for
 u32)#1}
 */
 static inline uint32_t libcrux_sha3_from_eb(libcrux_sha3_Algorithm v) {
-  uint32_t uu____0;
-  switch (v) {
-    case libcrux_sha3_Sha224: {
-      uu____0 = 1U;
-      break;
-    }
-    case libcrux_sha3_Sha256: {
-      uu____0 = 2U;
-      break;
-    }
-    case libcrux_sha3_Sha384: {
-      uu____0 = 3U;
-      break;
-    }
-    case libcrux_sha3_Sha512: {
-      uu____0 = 4U;
-      break;
-    }
-    default: {
-      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
-                        __LINE__);
-      KRML_HOST_EXIT(253U);
+  if (!(v == libcrux_sha3_Algorithm_Sha224)) {
+    if (v == libcrux_sha3_Algorithm_Sha256) {
+      return 2U;
+    } else if (v == libcrux_sha3_Algorithm_Sha384) {
+      return 3U;
+    } else {
+      return 4U;
     }
   }
-  return uu____0;
+  return 1U;
 }
 
 /**
@@ -4888,23 +4858,18 @@ This function found in impl {(core::convert::From<u32> for
 libcrux_sha3::Algorithm)}
 */
 static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
-  libcrux_sha3_Algorithm uu____0;
   switch (v) {
     case 1U: {
-      uu____0 = libcrux_sha3_Sha224;
       break;
     }
     case 2U: {
-      uu____0 = libcrux_sha3_Sha256;
-      break;
+      return libcrux_sha3_Algorithm_Sha256;
     }
     case 3U: {
-      uu____0 = libcrux_sha3_Sha384;
-      break;
+      return libcrux_sha3_Algorithm_Sha384;
     }
     case 4U: {
-      uu____0 = libcrux_sha3_Sha512;
-      break;
+      return libcrux_sha3_Algorithm_Sha512;
     }
     default: {
       KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
@@ -4912,7 +4877,7 @@ static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
       KRML_HOST_EXIT(255U);
     }
   }
-  return uu____0;
+  return libcrux_sha3_Algorithm_Sha224;
 }
 
 typedef uint8_t libcrux_sha3_Sha3_512Digest[64U];
diff --git a/libcrux-ml-dsa/cg/tests/mldsa65.cc b/libcrux-ml-dsa/cg/tests/mldsa65.cc
index ea77a81b2..baa8dd911 100644
--- a/libcrux-ml-dsa/cg/tests/mldsa65.cc
+++ b/libcrux-ml-dsa/cg/tests/mldsa65.cc
@@ -55,3 +55,44 @@ TEST(MlDsa65TestPortable, ConsistencyTest)
 
     EXPECT_EQ(result.tag, Ok);
 }
+
+#ifdef LIBCRUX_X64
+#include "libcrux_mldsa65_avx2.h"
+
+TEST(MlDsa65TestAvx2, ConsistencyTest)
+{
+    // Generate key pair
+    uint8_t randomness[32];
+    for (int i = 0; i < 32; i++)
+    {
+        randomness[i] = 13;
+    }
+    auto key_pair = libcrux_ml_dsa_ml_dsa_65_avx2_generate_key_pair(randomness);
+
+    // Sign
+    uint8_t msg[79] = {0};
+    for (int i = 0; i < 32; i++)
+    {
+        randomness[i] = 0x55;
+    }
+    uint8_t context[3];
+
+    auto msg_slice = mk_slice(&msg, 79);
+    auto context_slice = mk_slice(&context, 3);
+    auto signature_result = libcrux_ml_dsa_ml_dsa_65_avx2_sign(
+        &key_pair.signing_key, msg_slice,
+        context_slice,
+        randomness);
+    EXPECT_EQ(signature_result.tag, Ok);
+    auto signature = signature_result.val.case_Ok;
+
+    // Verify
+    auto result = libcrux_ml_dsa_ml_dsa_65_avx2_verify(
+        &key_pair.verification_key,
+        msg_slice,
+        context_slice,
+        &signature);
+
+    EXPECT_EQ(result.tag, Ok);
+}
+#endif // LIBCRUX_X64
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst
index b1b0922d2..4aa6023ae 100644
--- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst
+++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst
@@ -80,14 +80,14 @@ let deserialize_to_unsigned (v_ETA: usize) (serialized: t_Slice u8) =
         Rust_primitives.Hax.t_Never)
 
 let deserialize (v_ETA: usize) (serialized: t_Slice u8) =
-  let unsigned:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+  let deserialized:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     deserialize_to_unsigned v_ETA serialized
   in
   Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32 (
           cast (v_ETA <: usize) <: i32)
       <:
       Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    unsigned
+    deserialized
 
 let serialize_when_eta_is_2_ (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (out: t_Slice u8) =
   let serialized:t_Array u8 (sz 16) = Rust_primitives.Hax.repeat 0uy (sz 16) in
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst
index 92aee3dbe..4a4ea00ea 100644
--- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst
+++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst
@@ -541,7 +541,7 @@ Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit =
     =
     (fun
         (simd_units: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
-        (out: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
+        (out1: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
         ->
         true);
     f_ntt
@@ -574,17 +574,39 @@ Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit =
         let result:t_Array Libcrux_intrinsics.Avx2_extract.t_Vec256 (sz 32) =
           Libcrux_ml_dsa.Simd.Avx2.Ntt.ntt re
         in
-        Core.Array.from_fn #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-          (sz 32)
-          (fun i ->
-              let i:usize = i in
-              {
-                Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_coefficients
-                =
-                result.[ i ] <: Libcrux_intrinsics.Avx2_extract.t_Vec256
-              }
+        let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) =
+          Rust_primitives.Hax.repeat (Libcrux_ml_dsa.Simd.Avx2.Vector_type.v_ZERO ()
+              <:
+              Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit)
+            (sz 32)
+        in
+        let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) =
+          Rust_primitives.Hax.Folds.fold_range (sz 0)
+            (Core.Slice.impl__len #Libcrux_intrinsics.Avx2_extract.t_Vec256
+                (result <: t_Slice Libcrux_intrinsics.Avx2_extract.t_Vec256)
               <:
-              Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit));
+              usize)
+            (fun out temp_1_ ->
+                let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) = out in
+                let _:usize = temp_1_ in
+                true)
+            out
+            (fun out i ->
+                let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) = out in
+                let i:usize = i in
+                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
+                  i
+                  ({
+                      Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_coefficients
+                      =
+                      result.[ i ] <: Libcrux_intrinsics.Avx2_extract.t_Vec256
+                    }
+                    <:
+                    Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit)
+                <:
+                t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
+        in
+        out);
     f_invert_ntt_montgomery_pre
     =
     (fun (simd_units: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32)) -> true);
@@ -592,7 +614,7 @@ Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit =
     =
     (fun
         (simd_units: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
-        (out: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
+        (out1: t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
         ->
         true);
     f_invert_ntt_montgomery
@@ -625,15 +647,37 @@ Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit =
       let result:t_Array Libcrux_intrinsics.Avx2_extract.t_Vec256 (sz 32) =
         Libcrux_ml_dsa.Simd.Avx2.Invntt.invert_ntt_montgomery re
       in
-      Core.Array.from_fn #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-        (sz 32)
-        (fun i ->
-            let i:usize = i in
-            {
-              Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_coefficients
-              =
-              result.[ i ] <: Libcrux_intrinsics.Avx2_extract.t_Vec256
-            }
+      let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) =
+        Rust_primitives.Hax.repeat (Libcrux_ml_dsa.Simd.Avx2.Vector_type.v_ZERO ()
             <:
             Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit)
+          (sz 32)
+      in
+      let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) =
+        Rust_primitives.Hax.Folds.fold_range (sz 0)
+          (Core.Slice.impl__len #Libcrux_intrinsics.Avx2_extract.t_Vec256
+              (result <: t_Slice Libcrux_intrinsics.Avx2_extract.t_Vec256)
+            <:
+            usize)
+          (fun out temp_1_ ->
+              let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) = out in
+              let _:usize = temp_1_ in
+              true)
+          out
+          (fun out i ->
+              let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) = out in
+              let i:usize = i in
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
+                i
+                ({
+                    Libcrux_ml_dsa.Simd.Avx2.Vector_type.f_coefficients
+                    =
+                    result.[ i ] <: Libcrux_intrinsics.Avx2_extract.t_Vec256
+                  }
+                  <:
+                  Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit)
+              <:
+              t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32))
+      in
+      out
   }
diff --git a/libcrux-ml-dsa/src/simd/avx2.rs b/libcrux-ml-dsa/src/simd/avx2.rs
index 8fb2c09cd..2359a4671 100644
--- a/libcrux-ml-dsa/src/simd/avx2.rs
+++ b/libcrux-ml-dsa/src/simd/avx2.rs
@@ -137,9 +137,13 @@ impl Operations for AVX2SIMDUnit {
         }
         let result = ntt::ntt(re);
 
-        core::array::from_fn(|i| Self {
-            coefficients: result[i],
-        })
+        let mut out = [vector_type::ZERO(); SIMD_UNITS_IN_RING_ELEMENT];
+        for i in 0..result.len() {
+            out[i] = Self {
+                coefficients: result[i],
+            };
+        }
+        out
     }
 
     #[inline(always)]
@@ -154,8 +158,12 @@ impl Operations for AVX2SIMDUnit {
         }
         let result = invntt::invert_ntt_montgomery(re);
 
-        core::array::from_fn(|i| Self {
-            coefficients: result[i],
-        })
+        let mut out = [vector_type::ZERO(); SIMD_UNITS_IN_RING_ELEMENT];
+        for i in 0..result.len() {
+            out[i] = Self {
+                coefficients: result[i],
+            };
+        }
+        out
     }
 }
diff --git a/libcrux-ml-dsa/src/simd/avx2/encoding/error.rs b/libcrux-ml-dsa/src/simd/avx2/encoding/error.rs
index dcc82f753..1bbf3ab75 100644
--- a/libcrux-ml-dsa/src/simd/avx2/encoding/error.rs
+++ b/libcrux-ml-dsa/src/simd/avx2/encoding/error.rs
@@ -130,7 +130,7 @@ pub(crate) fn deserialize_to_unsigned<const ETA: usize>(serialized: &[u8]) -> Ve
 
 #[inline(always)]
 pub(crate) fn deserialize<const ETA: usize>(serialized: &[u8]) -> Vec256 {
-    let unsigned = deserialize_to_unsigned::<ETA>(serialized);
+    let deserialized = deserialize_to_unsigned::<ETA>(serialized);
 
-    mm256_sub_epi32(mm256_set1_epi32(ETA as i32), unsigned)
+    mm256_sub_epi32(mm256_set1_epi32(ETA as i32), deserialized)
 }
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
index f79583aac..80f8dd1aa 100644
--- a/libcrux-ml-kem/c/code_gen.txt
+++ b/libcrux-ml-kem/c/code_gen.txt
@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
-Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
-Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
-F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
-Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+F*: b0961063393215ca65927f017720cb365a193833-dirty
+Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
diff --git a/libcrux-ml-kem/c/eurydice_glue.h b/libcrux-ml-kem/c/eurydice_glue.h
index ad026b9e1..746ab0dbf 100644
--- a/libcrux-ml-kem/c/eurydice_glue.h
+++ b/libcrux-ml-kem/c/eurydice_glue.h
@@ -213,7 +213,7 @@ core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__N
 
 // ITERATORS
 #define Eurydice_range_iter_next(iter_ptr, t, ret_t) \
-  (((iter_ptr)->start == (iter_ptr)->end)            \
+  (((iter_ptr)->start >= (iter_ptr)->end)            \
        ? (CLITERAL(ret_t){.tag = core_option_None})  \
        : (CLITERAL(ret_t){.tag = core_option_Some,   \
                           .f0 = (iter_ptr)->start++}))
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
index 12e124ead..dcee90a02 100644
--- a/libcrux-ml-kem/c/internal/libcrux_core.h
+++ b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __internal_libcrux_core_H
diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
index db1273acd..14a1b31bd 100644
--- a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
+++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H
diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
index 4eb95b685..12a192db5 100644
--- a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
+++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H
diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
index a8e016886..563366afd 100644
--- a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H
diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
index 29d383df5..44cad1c42 100644
--- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
+++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __internal_libcrux_sha3_internal_H
@@ -89,10 +89,10 @@ libcrux_sha3_portable_incremental_shake128_squeeze_next_block(
   libcrux_sha3_generic_keccak_squeeze_next_block_c6(s, buf);
 }
 
-#define libcrux_sha3_Sha224 0
-#define libcrux_sha3_Sha256 1
-#define libcrux_sha3_Sha384 2
-#define libcrux_sha3_Sha512 3
+#define libcrux_sha3_Algorithm_Sha224 1
+#define libcrux_sha3_Algorithm_Sha256 2
+#define libcrux_sha3_Algorithm_Sha384 3
+#define libcrux_sha3_Algorithm_Sha512 4
 
 typedef uint8_t libcrux_sha3_Algorithm;
 
@@ -100,31 +100,16 @@ typedef uint8_t libcrux_sha3_Algorithm;
  Returns the output size of a digest.
 */
 static inline size_t libcrux_sha3_digest_size(libcrux_sha3_Algorithm mode) {
-  size_t uu____0;
-  switch (mode) {
-    case libcrux_sha3_Sha224: {
-      uu____0 = (size_t)28U;
-      break;
-    }
-    case libcrux_sha3_Sha256: {
-      uu____0 = (size_t)32U;
-      break;
-    }
-    case libcrux_sha3_Sha384: {
-      uu____0 = (size_t)48U;
-      break;
-    }
-    case libcrux_sha3_Sha512: {
-      uu____0 = (size_t)64U;
-      break;
-    }
-    default: {
-      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
-                        __LINE__);
-      KRML_HOST_EXIT(253U);
+  if (!(mode == libcrux_sha3_Algorithm_Sha224)) {
+    if (mode == libcrux_sha3_Algorithm_Sha256) {
+      return (size_t)32U;
+    } else if (mode == libcrux_sha3_Algorithm_Sha384) {
+      return (size_t)48U;
+    } else {
+      return (size_t)64U;
     }
   }
-  return uu____0;
+  return (size_t)28U;
 }
 
 static const size_t libcrux_sha3_generic_keccak__PI[24U] = {
@@ -1396,31 +1381,16 @@ This function found in impl {(core::convert::From<libcrux_sha3::Algorithm> for
 u32)#1}
 */
 static inline uint32_t libcrux_sha3_from_eb(libcrux_sha3_Algorithm v) {
-  uint32_t uu____0;
-  switch (v) {
-    case libcrux_sha3_Sha224: {
-      uu____0 = 1U;
-      break;
-    }
-    case libcrux_sha3_Sha256: {
-      uu____0 = 2U;
-      break;
-    }
-    case libcrux_sha3_Sha384: {
-      uu____0 = 3U;
-      break;
-    }
-    case libcrux_sha3_Sha512: {
-      uu____0 = 4U;
-      break;
-    }
-    default: {
-      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
-                        __LINE__);
-      KRML_HOST_EXIT(253U);
+  if (!(v == libcrux_sha3_Algorithm_Sha224)) {
+    if (v == libcrux_sha3_Algorithm_Sha256) {
+      return 2U;
+    } else if (v == libcrux_sha3_Algorithm_Sha384) {
+      return 3U;
+    } else {
+      return 4U;
     }
   }
-  return uu____0;
+  return 1U;
 }
 
 /**
@@ -1428,23 +1398,18 @@ This function found in impl {(core::convert::From<u32> for
 libcrux_sha3::Algorithm)}
 */
 static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
-  libcrux_sha3_Algorithm uu____0;
   switch (v) {
     case 1U: {
-      uu____0 = libcrux_sha3_Sha224;
       break;
     }
     case 2U: {
-      uu____0 = libcrux_sha3_Sha256;
-      break;
+      return libcrux_sha3_Algorithm_Sha256;
     }
     case 3U: {
-      uu____0 = libcrux_sha3_Sha384;
-      break;
+      return libcrux_sha3_Algorithm_Sha384;
     }
     case 4U: {
-      uu____0 = libcrux_sha3_Sha512;
-      break;
+      return libcrux_sha3_Algorithm_Sha512;
     }
     default: {
       KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
@@ -1452,7 +1417,7 @@ static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
       KRML_HOST_EXIT(255U);
     }
   }
-  return uu____0;
+  return libcrux_sha3_Algorithm_Sha224;
 }
 
 typedef uint8_t libcrux_sha3_Sha3_512Digest[64U];
diff --git a/libcrux-ml-kem/c/karamel/include/krml/internal/target.h b/libcrux-ml-kem/c/karamel/include/krml/internal/target.h
index 25313e254..2b98cb368 100644
--- a/libcrux-ml-kem/c/karamel/include/krml/internal/target.h
+++ b/libcrux-ml-kem/c/karamel/include/krml/internal/target.h
@@ -19,6 +19,20 @@
 #define inline __inline__
 #endif
 
+/* There is no support for aligned_alloc() in macOS before Catalina, so
+ * let's make a macro to use _mm_malloc() and _mm_free() functions
+ * from mm_malloc.h. */
+#if defined(__APPLE__) && defined(__MACH__)
+#include <AvailabilityMacros.h>
+#if defined(MAC_OS_X_VERSION_MIN_REQUIRED) && \
+    (MAC_OS_X_VERSION_MIN_REQUIRED < 101500)
+#include <mm_malloc.h>
+#define LEGACY_MACOS
+#else
+#undef LEGACY_MACOS
+#endif
+#endif
+
 /******************************************************************************/
 /* Macros that KaRaMeL will generate.                                         */
 /******************************************************************************/
@@ -134,6 +148,8 @@
 #if (defined(_MSC_VER) || \
      (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR)))
 #define KRML_ALIGNED_MALLOC(X, Y) _aligned_malloc(Y, X)
+#elif defined(LEGACY_MACOS)
+#define KRML_ALIGNED_MALLOC(X, Y) _mm_malloc(Y, X)
 #else
 #define KRML_ALIGNED_MALLOC(X, Y) aligned_alloc(X, Y)
 #endif
@@ -150,6 +166,8 @@
 #if (defined(_MSC_VER) || \
      (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR)))
 #define KRML_ALIGNED_FREE(X) _aligned_free(X)
+#elif defined(LEGACY_MACOS)
+#define KRML_ALIGNED_FREE(X) _mm_free(X)
 #else
 #define KRML_ALIGNED_FREE(X) free(X)
 #endif
diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c
index 8d36883e4..59763e569 100644
--- a/libcrux-ml-kem/c/libcrux_core.c
+++ b/libcrux-ml-kem/c/libcrux_core.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "internal/libcrux_core.h"
@@ -279,10 +279,10 @@ with const generics
 */
 uint8_t libcrux_ml_kem_utils_prf_input_inc_e0(uint8_t (*prf_inputs)[33U],
                                               uint8_t domain_separator) {
-  uint8_t ret[3U][33U];
+  uint8_t _prf_inputs_init[3U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)3U, prf_inputs, ret, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(ret, uint8_t[3U][33U], void *);
+      (size_t)3U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[3U][33U], void *);
   KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, size_t i0 = i;
                   prf_inputs[i0][32U] = domain_separator;
                   domain_separator = (uint32_t)domain_separator + 1U;);
@@ -412,10 +412,10 @@ with const generics
 */
 uint8_t libcrux_ml_kem_utils_prf_input_inc_fd(uint8_t (*prf_inputs)[33U],
                                               uint8_t domain_separator) {
-  uint8_t ret[2U][33U];
+  uint8_t _prf_inputs_init[2U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)2U, prf_inputs, ret, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(ret, uint8_t[2U][33U], void *);
+      (size_t)2U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[2U][33U], void *);
   KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, size_t i0 = i;
                   prf_inputs[i0][32U] = domain_separator;
                   domain_separator = (uint32_t)domain_separator + 1U;);
@@ -585,10 +585,10 @@ with const generics
 */
 uint8_t libcrux_ml_kem_utils_prf_input_inc_ac(uint8_t (*prf_inputs)[33U],
                                               uint8_t domain_separator) {
-  uint8_t ret[4U][33U];
+  uint8_t _prf_inputs_init[4U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)4U, prf_inputs, ret, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(ret, uint8_t[4U][33U], void *);
+      (size_t)4U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[4U][33U], void *);
   KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i;
                   prf_inputs[i0][32U] = domain_separator;
                   domain_separator = (uint32_t)domain_separator + 1U;);
diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h
index 3e81d2dc0..ebef18f73 100644
--- a/libcrux-ml-kem/c/libcrux_core.h
+++ b/libcrux-ml-kem/c/libcrux_core.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_core_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h
index fb6f70eaa..6d930d2b1 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem1024_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
index 65c3d7236..a668fbffc 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_mlkem1024_avx2.h"
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
index 17b0c0046..c8d073164 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem1024_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
index 35b28ea4a..99cb4511a 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_mlkem1024_portable.h"
diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
index 2d9862c52..7fa5a824e 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem1024_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h
index 26616454d..f1e97d316 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem512_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
index b3197512a..54048e3b7 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_mlkem512_avx2.h"
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
index 17beb7efe..43a838911 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem512_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
index 95355e049..1e39aba00 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_mlkem512_portable.h"
diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
index 062f3666e..cfe5fbd20 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem512_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h
index aae08ebb5..004b15d7c 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem768_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
index e16553589..fb95e356d 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_mlkem768_avx2.h"
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
index a2ac464f9..531bd8b55 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem768_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
index 60b294d9a..187866f64 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_mlkem768_portable.h"
diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
index d3ef0d130..132dafef7 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem768_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
index 20fa22c11..c29a94848 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "internal/libcrux_mlkem_avx2.h"
@@ -3486,8 +3486,7 @@ compute_ring_element_v_ab(
                       ntt_multiply_ef_79(&t_as_ntt[i0], &r_as_ntt[i0]);
                   add_to_ring_element_ef_ab(&result, &product););
   invert_ntt_montgomery_ab(&result);
-  result = add_message_error_reduce_ef_79(error_2, message, result);
-  return result;
+  return add_message_error_reduce_ef_79(error_2, message, result);
 }
 
 /**
@@ -4630,8 +4629,7 @@ compute_message_ab(
                       ntt_multiply_ef_79(&secret_as_ntt[i0], &u_as_ntt[i0]);
                   add_to_ring_element_ef_ab(&result, &product););
   invert_ntt_montgomery_ab(&result);
-  result = subtract_reduce_ef_79(v, result);
-  return result;
+  return subtract_reduce_ef_79(v, result);
 }
 
 /**
@@ -6275,8 +6273,7 @@ compute_ring_element_v_42(
                       ntt_multiply_ef_79(&t_as_ntt[i0], &r_as_ntt[i0]);
                   add_to_ring_element_ef_42(&result, &product););
   invert_ntt_montgomery_42(&result);
-  result = add_message_error_reduce_ef_79(error_2, message, result);
-  return result;
+  return add_message_error_reduce_ef_79(error_2, message, result);
 }
 
 /**
@@ -6742,8 +6739,7 @@ compute_message_42(
                       ntt_multiply_ef_79(&secret_as_ntt[i0], &u_as_ntt[i0]);
                   add_to_ring_element_ef_42(&result, &product););
   invert_ntt_montgomery_42(&result);
-  result = subtract_reduce_ef_79(v, result);
-  return result;
+  return subtract_reduce_ef_79(v, result);
 }
 
 /**
@@ -8376,8 +8372,7 @@ compute_ring_element_v_89(
                       ntt_multiply_ef_79(&t_as_ntt[i0], &r_as_ntt[i0]);
                   add_to_ring_element_ef_89(&result, &product););
   invert_ntt_montgomery_89(&result);
-  result = add_message_error_reduce_ef_79(error_2, message, result);
-  return result;
+  return add_message_error_reduce_ef_79(error_2, message, result);
 }
 
 /**
@@ -8775,8 +8770,7 @@ compute_message_89(
                       ntt_multiply_ef_79(&secret_as_ntt[i0], &u_as_ntt[i0]);
                   add_to_ring_element_ef_89(&result, &product););
   invert_ntt_montgomery_89(&result);
-  result = subtract_reduce_ef_79(v, result);
-  return result;
+  return subtract_reduce_ef_79(v, result);
 }
 
 /**
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
index 8f6b4009e..9fab949c7 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.c b/libcrux-ml-kem/c/libcrux_mlkem_portable.c
index f787aa9c9..18f187b79 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c
+++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "internal/libcrux_mlkem_portable.h"
@@ -4728,8 +4728,7 @@ compute_ring_element_v_d0(
                       ntt_multiply_ef_96(&t_as_ntt[i0], &r_as_ntt[i0]);
                   add_to_ring_element_ef_d0(&result, &product););
   invert_ntt_montgomery_d0(&result);
-  result = add_message_error_reduce_ef_96(error_2, message, result);
-  return result;
+  return add_message_error_reduce_ef_96(error_2, message, result);
 }
 
 /**
@@ -5674,8 +5673,7 @@ compute_message_d0(
                       ntt_multiply_ef_96(&secret_as_ntt[i0], &u_as_ntt[i0]);
                   add_to_ring_element_ef_d0(&result, &product););
   invert_ntt_montgomery_d0(&result);
-  result = subtract_reduce_ef_96(v, result);
-  return result;
+  return subtract_reduce_ef_96(v, result);
 }
 
 /**
@@ -7327,8 +7325,7 @@ compute_ring_element_v_a0(
                       ntt_multiply_ef_96(&t_as_ntt[i0], &r_as_ntt[i0]);
                   add_to_ring_element_ef_a0(&result, &product););
   invert_ntt_montgomery_a0(&result);
-  result = add_message_error_reduce_ef_96(error_2, message, result);
-  return result;
+  return add_message_error_reduce_ef_96(error_2, message, result);
 }
 
 /**
@@ -7797,8 +7794,7 @@ compute_message_a0(
                       ntt_multiply_ef_96(&secret_as_ntt[i0], &u_as_ntt[i0]);
                   add_to_ring_element_ef_a0(&result, &product););
   invert_ntt_montgomery_a0(&result);
-  result = subtract_reduce_ef_96(v, result);
-  return result;
+  return subtract_reduce_ef_96(v, result);
 }
 
 /**
@@ -9375,8 +9371,7 @@ compute_ring_element_v_1b(
                       ntt_multiply_ef_96(&t_as_ntt[i0], &r_as_ntt[i0]);
                   add_to_ring_element_ef_1b(&result, &product););
   invert_ntt_montgomery_1b(&result);
-  result = add_message_error_reduce_ef_96(error_2, message, result);
-  return result;
+  return add_message_error_reduce_ef_96(error_2, message, result);
 }
 
 /**
@@ -9777,8 +9772,7 @@ compute_message_1b(
                       ntt_multiply_ef_96(&secret_as_ntt[i0], &u_as_ntt[i0]);
                   add_to_ring_element_ef_1b(&result, &product););
   invert_ntt_montgomery_1b(&result);
-  result = subtract_reduce_ef_96(v, result);
-  return result;
+  return subtract_reduce_ef_96(v, result);
 }
 
 /**
diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h
index fe8972889..d85e02501 100644
--- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h
+++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem_portable_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h
index 5b00b2050..1354eda6b 100644
--- a/libcrux-ml-kem/c/libcrux_sha3.h
+++ b/libcrux-ml-kem/c/libcrux_sha3.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.c b/libcrux-ml-kem/c/libcrux_sha3_avx2.c
index 86cd49d43..4d272653d 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c
+++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "internal/libcrux_sha3_avx2.h"
diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/libcrux_sha3_avx2.h
index 8cf00fb6d..77ad8ec75 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_avx2_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3_internal.h b/libcrux-ml-kem/c/libcrux_sha3_internal.h
index 16c7766a0..181c778e3 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_internal.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_internal_H
diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.c b/libcrux-ml-kem/c/libcrux_sha3_neon.c
index fb6b2e649..1d40fa9dc 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_neon.c
+++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #include "libcrux_sha3_neon.h"
diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.h b/libcrux-ml-kem/c/libcrux_sha3_neon.h
index 62eca860c..1a28e0c91 100644
--- a/libcrux-ml-kem/c/libcrux_sha3_neon.h
+++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_neon_H
diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt
index f79583aac..80f8dd1aa 100644
--- a/libcrux-ml-kem/cg/code_gen.txt
+++ b/libcrux-ml-kem/cg/code_gen.txt
@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
-Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
-Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
-F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
-Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+F*: b0961063393215ca65927f017720cb365a193833-dirty
+Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h
index 1536ceb2d..47d61e63e 100644
--- a/libcrux-ml-kem/cg/libcrux_core.h
+++ b/libcrux-ml-kem/cg/libcrux_core.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_core_H
@@ -2803,10 +2803,10 @@ with const generics
 */
 static KRML_MUSTINLINE uint8_t libcrux_ml_kem_utils_prf_input_inc_e0(
     uint8_t (*prf_inputs)[33U], uint8_t domain_separator) {
-  uint8_t ret[3U][33U];
+  uint8_t _prf_inputs_init[3U][33U];
   core_array___core__clone__Clone_for__Array_T__N___20__clone(
-      (size_t)3U, prf_inputs, ret, uint8_t[33U], void *);
-  LowStar_Ignore_ignore(ret, uint8_t[3U][33U], void *);
+      (size_t)3U, prf_inputs, _prf_inputs_init, uint8_t[33U], void *);
+  LowStar_Ignore_ignore(_prf_inputs_init, uint8_t[3U][33U], void *);
   for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
     size_t i0 = i;
     prf_inputs[i0][32U] = domain_separator;
diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h
index 515fb6146..97679ef48 100644
--- a/libcrux-ml-kem/cg/libcrux_ct_ops.h
+++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_ct_ops_H
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
index 0ed56b579..ffb15d06c 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem768_avx2_H
@@ -2507,8 +2507,7 @@ libcrux_ml_kem_matrix_compute_message_ab(
     libcrux_ml_kem_polynomial_add_to_ring_element_ef_ab(&result, &product);
   }
   libcrux_ml_kem_invert_ntt_invert_ntt_montgomery_ab(&result);
-  result = libcrux_ml_kem_polynomial_subtract_reduce_ef_79(v, result);
-  return result;
+  return libcrux_ml_kem_polynomial_subtract_reduce_ef_79(v, result);
 }
 
 /**
@@ -4001,9 +4000,8 @@ libcrux_ml_kem_matrix_compute_ring_element_v_ab(
     libcrux_ml_kem_polynomial_add_to_ring_element_ef_ab(&result, &product);
   }
   libcrux_ml_kem_invert_ntt_invert_ntt_montgomery_ab(&result);
-  result = libcrux_ml_kem_polynomial_add_message_error_reduce_ef_79(
+  return libcrux_ml_kem_polynomial_add_message_error_reduce_ef_79(
       error_2, message, result);
-  return result;
 }
 
 /**
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
index 1b133f2eb..79aa01af9 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_mlkem768_portable_H
@@ -3555,8 +3555,7 @@ libcrux_ml_kem_matrix_compute_message_1b(
     libcrux_ml_kem_polynomial_add_to_ring_element_ef_1b(&result, &product);
   }
   libcrux_ml_kem_invert_ntt_invert_ntt_montgomery_1b(&result);
-  result = libcrux_ml_kem_polynomial_subtract_reduce_ef_96(v, result);
-  return result;
+  return libcrux_ml_kem_polynomial_subtract_reduce_ef_96(v, result);
 }
 
 /**
@@ -5023,9 +5022,8 @@ libcrux_ml_kem_matrix_compute_ring_element_v_1b(
     libcrux_ml_kem_polynomial_add_to_ring_element_ef_1b(&result, &product);
   }
   libcrux_ml_kem_invert_ntt_invert_ntt_montgomery_1b(&result);
-  result = libcrux_ml_kem_polynomial_add_message_error_reduce_ef_96(
+  return libcrux_ml_kem_polynomial_add_message_error_reduce_ef_96(
       error_2, message, result);
-  return result;
 }
 
 /**
diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
index 1ae0f9b0f..8c38bc139 100644
--- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_avx2_H
diff --git a/libcrux-ml-kem/cg/libcrux_sha3_portable.h b/libcrux-ml-kem/cg/libcrux_sha3_portable.h
index 242a6e8dc..77bf47168 100644
--- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h
@@ -4,11 +4,11 @@
  * SPDX-License-Identifier: MIT or Apache-2.0
  *
  * This code was generated with the following revisions:
- * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
- * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
- * F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
- * Libcrux: da72c141597b1db012f3bc23a96330f6de112770
+ * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25
+ * Eurydice: 75eae2e2534a16f5ba5430e6ee5c69d8a46f3bea
+ * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65
+ * F*: b0961063393215ca65927f017720cb365a193833-dirty
+ * Libcrux: 834b7f51701fa4e8695a784c138ed230f49f0c4e
  */
 
 #ifndef __libcrux_sha3_portable_H
@@ -2364,10 +2364,10 @@ libcrux_sha3_portable_incremental_shake128_squeeze_next_block(
   libcrux_sha3_generic_keccak_squeeze_next_block_c61(s, buf);
 }
 
-#define libcrux_sha3_Sha224 0
-#define libcrux_sha3_Sha256 1
-#define libcrux_sha3_Sha384 2
-#define libcrux_sha3_Sha512 3
+#define libcrux_sha3_Algorithm_Sha224 1
+#define libcrux_sha3_Algorithm_Sha256 2
+#define libcrux_sha3_Algorithm_Sha384 3
+#define libcrux_sha3_Algorithm_Sha512 4
 
 typedef uint8_t libcrux_sha3_Algorithm;
 
@@ -2375,31 +2375,16 @@ typedef uint8_t libcrux_sha3_Algorithm;
  Returns the output size of a digest.
 */
 static inline size_t libcrux_sha3_digest_size(libcrux_sha3_Algorithm mode) {
-  size_t uu____0;
-  switch (mode) {
-    case libcrux_sha3_Sha224: {
-      uu____0 = (size_t)28U;
-      break;
-    }
-    case libcrux_sha3_Sha256: {
-      uu____0 = (size_t)32U;
-      break;
-    }
-    case libcrux_sha3_Sha384: {
-      uu____0 = (size_t)48U;
-      break;
-    }
-    case libcrux_sha3_Sha512: {
-      uu____0 = (size_t)64U;
-      break;
-    }
-    default: {
-      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
-                        __LINE__);
-      KRML_HOST_EXIT(253U);
+  if (!(mode == libcrux_sha3_Algorithm_Sha224)) {
+    if (mode == libcrux_sha3_Algorithm_Sha256) {
+      return (size_t)32U;
+    } else if (mode == libcrux_sha3_Algorithm_Sha384) {
+      return (size_t)48U;
+    } else {
+      return (size_t)64U;
     }
   }
-  return uu____0;
+  return (size_t)28U;
 }
 
 /**
@@ -4856,31 +4841,16 @@ This function found in impl {(core::convert::From<libcrux_sha3::Algorithm> for
 u32)#1}
 */
 static inline uint32_t libcrux_sha3_from_eb(libcrux_sha3_Algorithm v) {
-  uint32_t uu____0;
-  switch (v) {
-    case libcrux_sha3_Sha224: {
-      uu____0 = 1U;
-      break;
-    }
-    case libcrux_sha3_Sha256: {
-      uu____0 = 2U;
-      break;
-    }
-    case libcrux_sha3_Sha384: {
-      uu____0 = 3U;
-      break;
-    }
-    case libcrux_sha3_Sha512: {
-      uu____0 = 4U;
-      break;
-    }
-    default: {
-      KRML_HOST_EPRINTF("KaRaMeL incomplete match at %s:%d\n", __FILE__,
-                        __LINE__);
-      KRML_HOST_EXIT(253U);
+  if (!(v == libcrux_sha3_Algorithm_Sha224)) {
+    if (v == libcrux_sha3_Algorithm_Sha256) {
+      return 2U;
+    } else if (v == libcrux_sha3_Algorithm_Sha384) {
+      return 3U;
+    } else {
+      return 4U;
     }
   }
-  return uu____0;
+  return 1U;
 }
 
 /**
@@ -4888,23 +4858,18 @@ This function found in impl {(core::convert::From<u32> for
 libcrux_sha3::Algorithm)}
 */
 static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
-  libcrux_sha3_Algorithm uu____0;
   switch (v) {
     case 1U: {
-      uu____0 = libcrux_sha3_Sha224;
       break;
     }
     case 2U: {
-      uu____0 = libcrux_sha3_Sha256;
-      break;
+      return libcrux_sha3_Algorithm_Sha256;
     }
     case 3U: {
-      uu____0 = libcrux_sha3_Sha384;
-      break;
+      return libcrux_sha3_Algorithm_Sha384;
     }
     case 4U: {
-      uu____0 = libcrux_sha3_Sha512;
-      break;
+      return libcrux_sha3_Algorithm_Sha512;
     }
     default: {
       KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__,
@@ -4912,7 +4877,7 @@ static inline libcrux_sha3_Algorithm libcrux_sha3_from_2d(uint32_t v) {
       KRML_HOST_EXIT(255U);
     }
   }
-  return uu____0;
+  return libcrux_sha3_Algorithm_Sha224;
 }
 
 typedef uint8_t libcrux_sha3_Sha3_512Digest[64U];