From 0979e5c69127ebc8f24b32efb5eea0c32cf18328 Mon Sep 17 00:00:00 2001
From: Franziskus Kiefer <franziskuskiefer@gmail.com>
Date: Wed, 3 Jul 2024 21:26:17 +0200
Subject: [PATCH 1/2] add boring.sh

---
 libcrux-ml-kem/boring.sh                      | 20 ++++++++++++
 libcrux-ml-kem/c.sh                           |  7 +++--
 libcrux-ml-kem/cg/code_gen.txt                |  8 ++---
 .../cg/intrinsics/libcrux_intrinsics_avx2.h   | 15 ---------
 libcrux-ml-kem/cg/karamel/target.h            | 13 ++++----
 libcrux-ml-kem/cg/libcrux_core.h              | 13 +++++---
 libcrux-ml-kem/cg/libcrux_mlkem768_portable.h |  3 ++
 libcrux-ml-kem/cg/libcrux_sha3_portable.h     | 31 +++++++++++++++++++
 8 files changed, 77 insertions(+), 33 deletions(-)
 create mode 100755 libcrux-ml-kem/boring.sh

diff --git a/libcrux-ml-kem/boring.sh b/libcrux-ml-kem/boring.sh
new file mode 100755
index 000000000..b157d7b53
--- /dev/null
+++ b/libcrux-ml-kem/boring.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+set -e
+
+SED=$(which gsed &>/dev/null && echo gsed || echo sed)
+
+# Extract the C code
+# cargo clean
+./c.sh --config cg.yaml --out cg --mlkem768 --no-glue --no-unrolling --no-charon
+
+# Fixup code
+# TODO: This should go away as soon as the code generation is fixed.
+sed -i -E 's/static inline/__attribute__((target("avx2")))\nstatic inline/g' cg/libcrux_sha3_avx2.h
+sed -i -E 's/static inline/__attribute__((target("avx2")))\nstatic inline/g' cg/libcrux_mlkem768_avx2.h
+
+sed -i -E 's/.*libcrux_ml_kem_types_MlKemCiphertext_s.*//g' cg/libcrux_core.h
+sed -i -E 's/.*Eurydice_error_t_cg_array.*//g' cg/libcrux_core.h
+sed -i -E 's/.*libcrux_ml_kem_types_MlKemCiphertext;//g' cg/libcrux_core.h
+sed -i -E 's/.*libcrux_ml_kem_ind_cca_MlKem_s.*//g' cg/libcrux_core.h
+sed -i -E 's/.*libcrux_ml_kem_ind_cca_MlKem;;//g' cg/libcrux_core.h
diff --git a/libcrux-ml-kem/c.sh b/libcrux-ml-kem/c.sh
index 1299cf49b..50c9463b3 100755
--- a/libcrux-ml-kem/c.sh
+++ b/libcrux-ml-kem/c.sh
@@ -79,8 +79,11 @@ if [[ "$eurydice_glue" = 1 ]]; then
     cp $EURYDICE_HOME/include/eurydice_glue.h .
 fi
 
-clang-format --style=Google -i *.c *.h
-clang-format --style=Google -i internal/*.h
+find . -type f -name "*.c" -exec clang-format --style=Google -i "{}" \;
+find . -type f -name "*.h" -exec clang-format --style=Google -i "{}" \;
+if [ -d "internal" ]; then
+    clang-format --style=Google -i internal/*.h
+fi
 clang-format --style=Google -i intrinsics/*.h
 
 # Write out infos about the used tools
diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt
index fdcf0ec5e..0addeb43f 100644
--- a/libcrux-ml-kem/cg/code_gen.txt
+++ b/libcrux-ml-kem/cg/code_gen.txt
@@ -1,5 +1,5 @@
 This code was generated with the following tools:
-Charon: d799ceb29f648614b276f60d227794ee535473d2
-Eurydice: b38d5dd3b4099cce6bbb9d91c80fb2bf0aaff1f7
-Karamel: 409fe4552f8f46351241cba1decfaa4d9fa6ffea
-F*: 
+Charon: aeeae1d46704810bf498db552a75dff15aa3abcc
+Eurydice: ffeb01ce4cf0646e5cadec836bc042f98b8a16a8
+Karamel: 42a431696cd32d41155d7e484720eb71fd5dc7b1
+F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty
diff --git a/libcrux-ml-kem/cg/intrinsics/libcrux_intrinsics_avx2.h b/libcrux-ml-kem/cg/intrinsics/libcrux_intrinsics_avx2.h
index e504a6da3..dd7f4d9c3 100644
--- a/libcrux-ml-kem/cg/intrinsics/libcrux_intrinsics_avx2.h
+++ b/libcrux-ml-kem/cg/intrinsics/libcrux_intrinsics_avx2.h
@@ -128,13 +128,10 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm256_andnot_si256(a, b) \
   (_mm256_andnot_si256(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_xor_si256(a, b) (_mm256_xor_si256(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm_movemask_epi8(a) (_mm_movemask_epi8(a))
 
-
 // Shift operations
 #define libcrux_intrinsics_avx2_mm256_srai_epi16(a, b, _) \
   (_mm256_srai_epi16(b, a))
@@ -151,7 +148,6 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm256_slli_epi64_(a, b) \
   (_mm256_slli_epi64(b, a))
 
-
 #define libcrux_intrinsics_avx2_mm256_slli_epi64(a, b, c) \
   (libcrux_intrinsics_avx2_mm256_slli_epi64_(a, b))
 
@@ -163,11 +159,9 @@ 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_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))
 
@@ -176,26 +170,20 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm256_unpacklo_epi32(a, b) \
   (_mm256_unpacklo_epi32(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_unpacklo_epi64(a, b) \
   (_mm256_unpacklo_epi64(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_unpackhi_epi32(a, b) \
   (_mm256_unpackhi_epi32(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_unpackhi_epi64(a, b) \
   (_mm256_unpackhi_epi64(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_packs_epi32(a, b) \
   (_mm256_packs_epi32(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm_packs_epi16(a, b) (_mm_packs_epi16(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_shuffle_epi32(a, b, _) \
   (_mm256_shuffle_epi32(b, a))
 
@@ -217,14 +205,11 @@ typedef __m256i core_core_arch_x86___m256i;
 #define libcrux_intrinsics_avx2_mm256_shuffle_epi8(a, b) \
   (_mm256_shuffle_epi8(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm256_permutevar8x32_epi32(a, b) \
   (_mm256_permutevar8x32_epi32(a, b))
 
-
 #define libcrux_intrinsics_avx2_mm_shuffle_epi8(a, b) (_mm_shuffle_epi8(a, b))
 
-
 #if defined(__cplusplus)
 }
 #endif
diff --git a/libcrux-ml-kem/cg/karamel/target.h b/libcrux-ml-kem/cg/karamel/target.h
index 804507b80..402a54e03 100644
--- a/libcrux-ml-kem/cg/karamel/target.h
+++ b/libcrux-ml-kem/cg/karamel/target.h
@@ -5,20 +5,19 @@
 #define __KRML_TARGET_H
 
 #ifndef KRML_HOST_PRINTF
-#  define KRML_HOST_PRINTF printf
+#define KRML_HOST_PRINTF printf
 #endif
 
-#if                                                                          \
-    ((defined(__STDC_VERSION__) && __STDC_VERSION__ >= 199901L) ||           \
-     (defined(__cplusplus) && __cplusplus > 199711L)) &&                     \
+#if ((defined(__STDC_VERSION__) && __STDC_VERSION__ >= 199901L) || \
+     (defined(__cplusplus) && __cplusplus > 199711L)) &&           \
     (!defined(KRML_HOST_EPRINTF))
-#  define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
+#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
 #elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
-#  define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
+#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
 #endif
 
 #ifndef KRML_HOST_EXIT
-#  define KRML_HOST_EXIT exit
+#define KRML_HOST_EXIT exit
 #endif
 
 #endif
diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h
index a1ebccaf7..1e6d4b46c 100644
--- a/libcrux-ml-kem/cg/libcrux_core.h
+++ b/libcrux-ml-kem/cg/libcrux_core.h
@@ -84,10 +84,9 @@ libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(
 
 #define LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE ((size_t)32U)
 
-static inline void libcrux_ml_kem_constant_time_ops_select(Eurydice_slice lhs,
-                                                           Eurydice_slice rhs,
-                                                           uint8_t selector,
-                                                           uint8_t ret[32U]) {
+static inline void libcrux_ml_kem_constant_time_ops_select_ct(
+    Eurydice_slice lhs, Eurydice_slice rhs, uint8_t selector,
+    uint8_t ret[32U]) {
   uint8_t mask = core_num__u8_6__wrapping_sub(
       libcrux_ml_kem_constant_time_ops_is_non_zero(selector), 1U);
   uint8_t out[32U] = {0U};
@@ -109,7 +108,7 @@ libcrux_ml_kem_constant_time_ops_select_shared_secret_in_constant_time(
     Eurydice_slice lhs, Eurydice_slice rhs, uint8_t selector,
     uint8_t ret[32U]) {
   uint8_t ret0[32U];
-  libcrux_ml_kem_constant_time_ops_select(lhs, rhs, selector, ret0);
+  libcrux_ml_kem_constant_time_ops_select_ct(lhs, rhs, selector, ret0);
   memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
 }
 
@@ -380,6 +379,10 @@ core_result__core__result__Result_T__E___unwrap__int16_t_16size_t__core_array_Tr
   }
 }
 
+
+
+
+
 typedef struct
     core_result_Result__uint8_t_8size_t__core_array_TryFromSliceError_s {
   core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_tags tag;
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
index ceb834e84..141441cb7 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
@@ -32,6 +32,9 @@ typedef struct libcrux_ml_kem_hash_functions_neon_Simd128Hash_s {
   (LIBCRUX_ML_KEM_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE + \
    LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE)
 
+typedef struct libcrux_ml_kem_ind_cca_MlKem_s {
+} libcrux_ml_kem_ind_cca_MlKem;
+
 typedef uint8_t libcrux_ml_kem_ind_cca_MlKemSharedSecret[32U];
 
 static const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U] =
diff --git a/libcrux-ml-kem/cg/libcrux_sha3_portable.h b/libcrux-ml-kem/cg/libcrux_sha3_portable.h
index 53df0e9b0..cf5acbaab 100644
--- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h
@@ -2668,6 +2668,37 @@ libcrux_sha3_portable_incremental_shake128_squeeze_first_five_blocks(
       s, buf);
 }
 
+static inline void libcrux_sha3_portable_incremental_shake256_absorb_final(
+    libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
+    Eurydice_slice data0) {
+  Eurydice_slice buf[1U] = {data0};
+  libcrux_sha3_generic_keccak_absorb_final__uint64_t_1size_t_136size_t_31uint8_t(
+      s, buf);
+}
+
+static inline libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t
+libcrux_sha3_portable_incremental_shake256_init(void) {
+  return libcrux_sha3_generic_keccak__libcrux_sha3__generic_keccak__KeccakState_T__N__TraitClause_0__1__new__uint64_t_1size_t();
+}
+
+static inline void
+libcrux_sha3_portable_incremental_shake256_squeeze_first_block(
+    libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
+    Eurydice_slice out0) {
+  Eurydice_slice buf[1U] = {out0};
+  libcrux_sha3_generic_keccak_squeeze_first_block__uint64_t_1size_t_136size_t(
+      s, buf);
+}
+
+static inline void
+libcrux_sha3_portable_incremental_shake256_squeeze_next_block(
+    libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
+    Eurydice_slice out0) {
+  Eurydice_slice buf[1U] = {out0};
+  libcrux_sha3_generic_keccak_squeeze_next_block__uint64_t_1size_t_136size_t(
+      s, buf);
+}
+
 static inline libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t
 libcrux_sha3_portable___core__clone__Clone_for_libcrux_sha3__portable__KeccakState___clone(
     libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *self) {

From 64cb3da74e8fb38b9b60da7239831f4f26a0497b Mon Sep 17 00:00:00 2001
From: Franziskus Kiefer <franziskuskiefer@gmail.com>
Date: Thu, 4 Jul 2024 11:58:49 +0200
Subject: [PATCH 2/2] boring update script and code

---
 libcrux-ml-kem/boring.sh                      |  23 +-
 libcrux-ml-kem/cg.yaml                        |   7 +-
 libcrux-ml-kem/cg/eurydice_glue.h             |   7 +
 libcrux-ml-kem/cg/libcrux_core.h              |  69 --
 libcrux-ml-kem/cg/libcrux_ct_ops.h            |  91 +++
 libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h     | 636 +++++++-----------
 libcrux-ml-kem/cg/libcrux_mlkem768_portable.h |   4 +-
 libcrux-ml-kem/cg/libcrux_sha3_avx2.h         | 405 +++++------
 8 files changed, 527 insertions(+), 715 deletions(-)
 create mode 100644 libcrux-ml-kem/cg/libcrux_ct_ops.h

diff --git a/libcrux-ml-kem/boring.sh b/libcrux-ml-kem/boring.sh
index b157d7b53..87fa2bd0f 100755
--- a/libcrux-ml-kem/boring.sh
+++ b/libcrux-ml-kem/boring.sh
@@ -5,8 +5,8 @@ set -e
 SED=$(which gsed &>/dev/null && echo gsed || echo sed)
 
 # Extract the C code
-# cargo clean
-./c.sh --config cg.yaml --out cg --mlkem768 --no-glue --no-unrolling --no-charon
+cargo clean
+./c.sh --config cg.yaml --out cg --mlkem768 --no-glue --no-unrolling
 
 # Fixup code
 # TODO: This should go away as soon as the code generation is fixed.
@@ -16,5 +16,20 @@ sed -i -E 's/static inline/__attribute__((target("avx2")))\nstatic inline/g' cg/
 sed -i -E 's/.*libcrux_ml_kem_types_MlKemCiphertext_s.*//g' cg/libcrux_core.h
 sed -i -E 's/.*Eurydice_error_t_cg_array.*//g' cg/libcrux_core.h
 sed -i -E 's/.*libcrux_ml_kem_types_MlKemCiphertext;//g' cg/libcrux_core.h
-sed -i -E 's/.*libcrux_ml_kem_ind_cca_MlKem_s.*//g' cg/libcrux_core.h
-sed -i -E 's/.*libcrux_ml_kem_ind_cca_MlKem;;//g' cg/libcrux_core.h
+sed -i -E 's/.*libcrux_ml_kem_ind_cca_MlKem_s.*//g' cg/libcrux_mlkem768_portable.h
+sed -i -E 's/.*libcrux_ml_kem_ind_cca_MlKem;//g' cg/libcrux_mlkem768_portable.h
+
+sed -i -E 's/static inline/__attribute__((noinline,unused)) static/g' cg/libcrux_ct_ops.h
+
+clang-format --style=Google -i cg/*.h
+
+if [[ -n "$BORINGSSL_HOME" ]]; then
+    echo "Copying the files into $BORINGSSL_HOME/third_party/libcrux/"
+
+    cp cg/*.h $BORINGSSL_HOME/third_party/libcrux/
+    cp cg/code_gen.txt $BORINGSSL_HOME/third_party/libcrux/
+    cp -r cg/karamel $BORINGSSL_HOME/third_party/libcrux/
+    cp -r cg/intrinsics $BORINGSSL_HOME/third_party/libcrux/
+    libcrux_rev=$(git rev-parse HEAD)
+    echo "libcrux: $libcrux_rev" >> $BORINGSSL_HOME/third_party/libcrux/code_gen.txt
+fi
diff --git a/libcrux-ml-kem/cg.yaml b/libcrux-ml-kem/cg.yaml
index f7833c76c..2dbffb8bc 100644
--- a/libcrux-ml-kem/cg.yaml
+++ b/libcrux-ml-kem/cg.yaml
@@ -1,12 +1,17 @@
 files:
   # INTRINSICS
-
   - name: libcrux_intrinsics_avx2
     library: true
     inline_static: true
     api:
       - [libcrux_intrinsics, avx2]
 
+  # Constant time ops
+  - name: libcrux_ct_ops
+    inline_static: true
+    api:
+      - [libcrux_ml_kem, constant_time_ops]
+
   # SHA3 (no mention of libcrux_mlkem in this section, please)
 
   - name: libcrux_sha3_avx2
diff --git a/libcrux-ml-kem/cg/eurydice_glue.h b/libcrux-ml-kem/cg/eurydice_glue.h
index ec6d47b7f..48455c2d7 100644
--- a/libcrux-ml-kem/cg/eurydice_glue.h
+++ b/libcrux-ml-kem/cg/eurydice_glue.h
@@ -14,6 +14,9 @@ extern "C" {
 
 // SLICES, ARRAYS, ETC.
 
+// The MSVC C++ compiler does not support compound literals.
+// This CLITERAL is used to turn `(type){...}` into `type{...}` when using a C++
+// compiler.
 #if defined(__cplusplus)
 #define CLITERAL(type) type
 #else
@@ -30,6 +33,10 @@ extern "C" {
 // - if you need to use `len` for a C style function (e.g. memcpy, memcmp), you
 // need to multiply it
 //   by sizeof t, where t is the type of the elements.
+//
+// Empty slices have `len == 0` and `ptr` always needs to be valid pointer that
+// is not NULL (otherwise the construction in EURYDICE_SLICE computes `NULL +
+// start`).
 typedef struct {
   void *ptr;
   size_t len;
diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h
index 1e6d4b46c..f4d819d9f 100644
--- a/libcrux-ml-kem/cg/libcrux_core.h
+++ b/libcrux-ml-kem/cg/libcrux_core.h
@@ -45,73 +45,8 @@ static inline uint32_t core_num__u8_6__count_ones(uint8_t x0);
 
 static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x0, uint8_t x1);
 
-static inline uint8_t libcrux_ml_kem_constant_time_ops_inz(uint8_t value) {
-  uint16_t value0 = (uint16_t)value;
-  uint16_t uu____0 = value0;
-  uint16_t result = (((uint32_t)uu____0 |
-                      (uint32_t)core_num__u16_7__wrapping_add(~value0, 1U)) &
-                     0xFFFFU) >>
-                        8U &
-                    1U;
-  return (uint8_t)result;
-}
-
-static inline uint8_t libcrux_ml_kem_constant_time_ops_is_non_zero(
-    uint8_t value) {
-  return libcrux_ml_kem_constant_time_ops_inz(value);
-}
-
-static inline uint8_t libcrux_ml_kem_constant_time_ops_compare(
-    Eurydice_slice lhs, Eurydice_slice rhs) {
-  uint8_t r = 0U;
-  for (size_t i = (size_t)0U;
-       i < core_slice___Slice_T___len(lhs, uint8_t, size_t); i++) {
-    size_t i0 = i;
-    uint8_t uu____0 =
-        Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *, uint8_t);
-    r = (uint32_t)r |
-        ((uint32_t)uu____0 ^
-         (uint32_t)Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *, uint8_t));
-  }
-  return libcrux_ml_kem_constant_time_ops_is_non_zero(r);
-}
-
-static inline uint8_t
-libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(
-    Eurydice_slice lhs, Eurydice_slice rhs) {
-  return libcrux_ml_kem_constant_time_ops_compare(lhs, rhs);
-}
-
 #define LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE ((size_t)32U)
 
-static inline void libcrux_ml_kem_constant_time_ops_select_ct(
-    Eurydice_slice lhs, Eurydice_slice rhs, uint8_t selector,
-    uint8_t ret[32U]) {
-  uint8_t mask = core_num__u8_6__wrapping_sub(
-      libcrux_ml_kem_constant_time_ops_is_non_zero(selector), 1U);
-  uint8_t out[32U] = {0U};
-  for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE;
-       i++) {
-    size_t i0 = i;
-    uint8_t uu____0 =
-        (uint32_t)Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *, uint8_t) &
-        (uint32_t)mask;
-    uint8_t *uu____1 =
-        &Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *, uint8_t);
-    out[i0] = (uint32_t)uu____0 | ((uint32_t)uu____1[0U] & (uint32_t)~mask);
-  }
-  memcpy(ret, out, (size_t)32U * sizeof(uint8_t));
-}
-
-static inline void
-libcrux_ml_kem_constant_time_ops_select_shared_secret_in_constant_time(
-    Eurydice_slice lhs, Eurydice_slice rhs, uint8_t selector,
-    uint8_t ret[32U]) {
-  uint8_t ret0[32U];
-  libcrux_ml_kem_constant_time_ops_select_ct(lhs, rhs, selector, ret0);
-  memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
-}
-
 #define LIBCRUX_ML_KEM_CONSTANTS_BITS_PER_COEFFICIENT ((size_t)12U)
 
 #define LIBCRUX_ML_KEM_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT ((size_t)256U)
@@ -379,10 +314,6 @@ core_result__core__result__Result_T__E___unwrap__int16_t_16size_t__core_array_Tr
   }
 }
 
-
-
-
-
 typedef struct
     core_result_Result__uint8_t_8size_t__core_array_TryFromSliceError_s {
   core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_tags tag;
diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h
new file mode 100644
index 000000000..47354b2c4
--- /dev/null
+++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h
@@ -0,0 +1,91 @@
+/*
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../cg.yaml
+  -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version:
+  <unknown> KaRaMeL version: 42a43169
+ */
+
+#ifndef __libcrux_ct_ops_H
+#define __libcrux_ct_ops_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include "eurydice_glue.h"
+#include "libcrux_core.h"
+
+__attribute__((noinline, unused)) static uint8_t
+libcrux_ml_kem_constant_time_ops_inz(uint8_t value) {
+  uint16_t value0 = (uint16_t)value;
+  uint16_t uu____0 = value0;
+  uint16_t result = (((uint32_t)uu____0 |
+                      (uint32_t)core_num__u16_7__wrapping_add(~value0, 1U)) &
+                     0xFFFFU) >>
+                        8U &
+                    1U;
+  return (uint8_t)result;
+}
+
+__attribute__((noinline, unused)) static uint8_t
+libcrux_ml_kem_constant_time_ops_is_non_zero(uint8_t value) {
+  return libcrux_ml_kem_constant_time_ops_inz(value);
+}
+
+__attribute__((noinline, unused)) static uint8_t
+libcrux_ml_kem_constant_time_ops_compare(Eurydice_slice lhs,
+                                         Eurydice_slice rhs) {
+  uint8_t r = 0U;
+  for (size_t i = (size_t)0U;
+       i < core_slice___Slice_T___len(lhs, uint8_t, size_t); i++) {
+    size_t i0 = i;
+    uint8_t uu____0 =
+        Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *, uint8_t);
+    r = (uint32_t)r |
+        ((uint32_t)uu____0 ^
+         (uint32_t)Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *, uint8_t));
+  }
+  return libcrux_ml_kem_constant_time_ops_is_non_zero(r);
+}
+
+__attribute__((noinline, unused)) static uint8_t
+libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time(
+    Eurydice_slice lhs, Eurydice_slice rhs) {
+  return libcrux_ml_kem_constant_time_ops_compare(lhs, rhs);
+}
+
+__attribute__((noinline, unused)) static void
+libcrux_ml_kem_constant_time_ops_select_ct(Eurydice_slice lhs,
+                                           Eurydice_slice rhs, uint8_t selector,
+                                           uint8_t ret[32U]) {
+  uint8_t mask = core_num__u8_6__wrapping_sub(
+      libcrux_ml_kem_constant_time_ops_is_non_zero(selector), 1U);
+  uint8_t out[32U] = {0U};
+  for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE;
+       i++) {
+    size_t i0 = i;
+    uint8_t uu____0 =
+        (uint32_t)Eurydice_slice_index(lhs, i0, uint8_t, uint8_t *, uint8_t) &
+        (uint32_t)mask;
+    uint8_t *uu____1 =
+        &Eurydice_slice_index(rhs, i0, uint8_t, uint8_t *, uint8_t);
+    out[i0] = (uint32_t)uu____0 | ((uint32_t)uu____1[0U] & (uint32_t)~mask);
+  }
+  memcpy(ret, out, (size_t)32U * sizeof(uint8_t));
+}
+
+__attribute__((noinline, unused)) static void
+libcrux_ml_kem_constant_time_ops_select_shared_secret_in_constant_time(
+    Eurydice_slice lhs, Eurydice_slice rhs, uint8_t selector,
+    uint8_t ret[32U]) {
+  uint8_t ret0[32U];
+  libcrux_ml_kem_constant_time_ops_select_ct(lhs, rhs, selector, ret0);
+  memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __libcrux_ct_ops_H_DEFINED
+#endif
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
index 5a2915a0a..f6ce3ec08 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h
@@ -14,67 +14,60 @@ extern "C" {
 
 #include "eurydice_glue.h"
 #include "libcrux_core.h"
+#include "libcrux_ct_ops.h"
 #include "libcrux_mlkem768_portable.h"
 #include "libcrux_sha3_avx2.h"
 #include "libcrux_sha3_portable.h"
 
 typedef core_core_arch_x86___m256i libcrux_ml_kem_vector_avx2_SIMD256Vector;
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i libcrux_ml_kem_vector_avx2_zero(void) {
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
+libcrux_ml_kem_vector_avx2_zero(void) {
   return libcrux_intrinsics_avx2_mm256_setzero_si256();
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___ZERO(
     void) {
   return libcrux_ml_kem_vector_avx2_zero();
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_from_i16_array(Eurydice_slice array) {
   return libcrux_intrinsics_avx2_mm256_loadu_si256_i16(array);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___from_i16_array(
     Eurydice_slice array) {
   return libcrux_ml_kem_vector_avx2_from_i16_array(array);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_add(core_core_arch_x86___m256i lhs,
                                           core_core_arch_x86___m256i rhs) {
   return libcrux_intrinsics_avx2_mm256_add_epi16(lhs, rhs);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___add(
     core_core_arch_x86___m256i lhs, core_core_arch_x86___m256i *rhs) {
   return libcrux_ml_kem_vector_avx2_arithmetic_add(lhs, rhs[0U]);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_sub(core_core_arch_x86___m256i lhs,
                                           core_core_arch_x86___m256i rhs) {
   return libcrux_intrinsics_avx2_mm256_sub_epi16(lhs, rhs);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___sub(
     core_core_arch_x86___m256i lhs, core_core_arch_x86___m256i *rhs) {
   return libcrux_ml_kem_vector_avx2_arithmetic_sub(lhs, rhs[0U]);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_multiply_by_constant(
     core_core_arch_x86___m256i vector, int16_t constant) {
   core_core_arch_x86___m256i uu____0 = vector;
@@ -82,15 +75,13 @@ libcrux_ml_kem_vector_avx2_arithmetic_multiply_by_constant(
       uu____0, libcrux_intrinsics_avx2_mm256_set1_epi16(constant));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___multiply_by_constant(
     core_core_arch_x86___m256i v, int16_t c) {
   return libcrux_ml_kem_vector_avx2_arithmetic_multiply_by_constant(v, c);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_bitwise_and_with_constant(
     core_core_arch_x86___m256i vector, int16_t constant) {
   core_core_arch_x86___m256i uu____0 = vector;
@@ -98,16 +89,14 @@ libcrux_ml_kem_vector_avx2_arithmetic_bitwise_and_with_constant(
       uu____0, libcrux_intrinsics_avx2_mm256_set1_epi16(constant));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___bitwise_and_with_constant(
     core_core_arch_x86___m256i vector, int16_t constant) {
   return libcrux_ml_kem_vector_avx2_arithmetic_bitwise_and_with_constant(
       vector, constant);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_cond_subtract_3329(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus =
@@ -124,8 +113,7 @@ libcrux_ml_kem_vector_avx2_arithmetic_cond_subtract_3329(
                                                  conditional_add_field_modulus);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___cond_subtract_3329(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_arithmetic_cond_subtract_3329(vector);
@@ -134,8 +122,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
 #define LIBCRUX_ML_KEM_VECTOR_AVX2_ARITHMETIC_BARRETT_MULTIPLIER \
   ((int16_t)20159)
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i uu____0 = vector;
@@ -157,15 +144,13 @@ libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(
                                                  quotient_times_field_modulus);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___barrett_reduce(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(vector);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constant(
     core_core_arch_x86___m256i vector, int16_t constant) {
   core_core_arch_x86___m256i constant0 =
@@ -188,16 +173,14 @@ libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constant(
   return libcrux_intrinsics_avx2_mm256_sub_epi16(value_high, k_times_modulus);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___montgomery_multiply_by_constant(
     core_core_arch_x86___m256i vector, int16_t constant) {
   return libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constant(
       vector, constant);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_compress_message_coefficient(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus_halved =
@@ -221,16 +204,14 @@ libcrux_ml_kem_vector_avx2_compress_compress_message_coefficient(
       (int32_t)15, shifted_to_positive_in_range, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___compress_1(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_compress_message_coefficient(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_mulhi_mm256_epi32(
     core_core_arch_x86___m256i lhs, core_core_arch_x86___m256i rhs) {
   core_core_arch_x86___m256i prod02 =
@@ -247,8 +228,7 @@ libcrux_ml_kem_vector_avx2_compress_mulhi_mm256_epi32(
       uu____1, libcrux_intrinsics_avx2_mm256_unpackhi_epi32(prod02, prod13));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constants(
     core_core_arch_x86___m256i v, core_core_arch_x86___m256i c) {
   core_core_arch_x86___m256i value_low =
@@ -269,8 +249,7 @@ libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_by_constants(
   return libcrux_intrinsics_avx2_mm256_sub_epi16(value_high, k_times_modulus);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_ntt_layer_1_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1,
     int16_t zeta2, int16_t zeta3) {
@@ -287,8 +266,7 @@ libcrux_ml_kem_vector_avx2_ntt_ntt_layer_1_step(
   return libcrux_intrinsics_avx2_mm256_add_epi16(lhs, rhs0);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___ntt_layer_1_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1,
     int16_t zeta2, int16_t zeta3) {
@@ -296,8 +274,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
                                                          zeta2, zeta3);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_ntt_layer_2_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1) {
   core_core_arch_x86___m256i zetas = libcrux_intrinsics_avx2_mm256_set_epi16(
@@ -313,15 +290,13 @@ libcrux_ml_kem_vector_avx2_ntt_ntt_layer_2_step(
   return libcrux_intrinsics_avx2_mm256_add_epi16(lhs, rhs0);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___ntt_layer_2_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1) {
   return libcrux_ml_kem_vector_avx2_ntt_ntt_layer_2_step(vector, zeta0, zeta1);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m128i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m128i
 libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_m128i_by_constants(
     core_core_arch_x86___m128i v, core_core_arch_x86___m128i c) {
   core_core_arch_x86___m128i value_low =
@@ -342,8 +317,7 @@ libcrux_ml_kem_vector_avx2_arithmetic_montgomery_multiply_m128i_by_constants(
   return libcrux_intrinsics_avx2_mm_sub_epi16(value_high, k_times_modulus);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_ntt_layer_3_step(
     core_core_arch_x86___m256i vector, int16_t zeta) {
   core_core_arch_x86___m128i rhs =
@@ -367,15 +341,13 @@ libcrux_ml_kem_vector_avx2_ntt_ntt_layer_3_step(
   return combined0;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___ntt_layer_3_step(
     core_core_arch_x86___m256i vector, int16_t zeta) {
   return libcrux_ml_kem_vector_avx2_ntt_ntt_layer_3_step(vector, zeta);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_1_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1,
     int16_t zeta2, int16_t zeta3) {
@@ -405,8 +377,7 @@ libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_1_step(
       (int32_t)204, sum, sum_times_zetas, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___inv_ntt_layer_1_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1,
     int16_t zeta2, int16_t zeta3) {
@@ -414,8 +385,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
       vector, zeta0, zeta1, zeta2, zeta3);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_2_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1) {
   core_core_arch_x86___m256i lhs =
@@ -444,16 +414,14 @@ libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_2_step(
       (int32_t)240, sum, sum_times_zetas, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___inv_ntt_layer_2_step(
     core_core_arch_x86___m256i vector, int16_t zeta0, int16_t zeta1) {
   return libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_2_step(vector, zeta0,
                                                              zeta1);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_3_step(
     core_core_arch_x86___m256i vector, int16_t zeta) {
   core_core_arch_x86___m128i lhs =
@@ -478,15 +446,13 @@ libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_3_step(
   return combined0;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___inv_ntt_layer_3_step(
     core_core_arch_x86___m256i vector, int16_t zeta) {
   return libcrux_ml_kem_vector_avx2_ntt_inv_ntt_layer_3_step(vector, zeta);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_montgomery_reduce_i32s(
     core_core_arch_x86___m256i v) {
   core_core_arch_x86___m256i uu____0 = v;
@@ -511,8 +477,7 @@ libcrux_ml_kem_vector_avx2_arithmetic_montgomery_reduce_i32s(
                                                   core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_ntt_ntt_multiply(core_core_arch_x86___m256i lhs,
                                             core_core_arch_x86___m256i rhs,
                                             int16_t zeta0, int16_t zeta1,
@@ -594,8 +559,7 @@ libcrux_ml_kem_vector_avx2_ntt_ntt_multiply(core_core_arch_x86___m256i lhs,
                                                    core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___ntt_multiply(
     core_core_arch_x86___m256i *lhs, core_core_arch_x86___m256i *rhs,
     int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3) {
@@ -603,8 +567,8 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
                                                      zeta1, zeta2, zeta3);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_1(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_serialize_serialize_1(
     core_core_arch_x86___m256i vector, uint8_t ret[2U]) {
   core_core_arch_x86___m256i lsb_to_msb =
       libcrux_intrinsics_avx2_mm256_slli_epi16((int32_t)15, vector,
@@ -623,8 +587,7 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_1(
   memcpy(ret, serialized, (size_t)2U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___serialize_1(
     core_core_arch_x86___m256i vector, uint8_t ret[2U]) {
   uint8_t ret0[2U];
@@ -632,8 +595,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
   memcpy(ret, ret0, (size_t)2U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) {
   int16_t uu____0 = (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t,
                                                   uint8_t *, uint8_t);
@@ -686,15 +648,14 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) {
       (int32_t)15, coefficients_in_msb, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___deserialize_1(
     Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_1(bytes);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_4(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_serialize_serialize_4(
     core_core_arch_x86___m256i vector, uint8_t ret[8U]) {
   uint8_t serialized[16U] = {0U};
   core_core_arch_x86___m256i uu____0 = vector;
@@ -744,8 +705,7 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_4(
   memcpy(ret, ret0, (size_t)8U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___serialize_4(
     core_core_arch_x86___m256i vector, uint8_t ret[8U]) {
   uint8_t ret0[8U];
@@ -753,8 +713,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
   memcpy(ret, ret0, (size_t)8U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) {
   int16_t uu____0 = (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t,
                                                   uint8_t *, uint8_t);
@@ -813,15 +772,14 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) {
                                                          (int16_t)1));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___deserialize_4(
     Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_4(bytes);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_5(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_serialize_serialize_5(
     core_core_arch_x86___m256i vector, uint8_t ret[10U]) {
   uint8_t serialized[32U] = {0U};
   core_core_arch_x86___m256i uu____0 = vector;
@@ -888,8 +846,7 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_5(
   memcpy(ret, ret0, (size_t)10U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___serialize_5(
     core_core_arch_x86___m256i vector, uint8_t ret[10U]) {
   uint8_t ret0[10U];
@@ -897,8 +854,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
   memcpy(ret, ret0, (size_t)10U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) {
   uint8_t uu____0 =
       Eurydice_slice_index(bytes, (size_t)9U, uint8_t, uint8_t *, uint8_t);
@@ -965,15 +921,14 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) {
                                                   core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___deserialize_5(
     Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_5(bytes);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_10(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_serialize_serialize_10(
     core_core_arch_x86___m256i vector, uint8_t ret[20U]) {
   uint8_t serialized[32U] = {0U};
   core_core_arch_x86___m256i uu____0 = vector;
@@ -1039,8 +994,7 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_10(
   memcpy(ret, ret0, (size_t)20U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___serialize_10(
     core_core_arch_x86___m256i vector, uint8_t ret[20U]) {
   uint8_t ret0[20U];
@@ -1048,8 +1002,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
   memcpy(ret, ret0, (size_t)20U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) {
   core_core_arch_x86___m256i shift_lsbs_to_msbs =
       libcrux_intrinsics_avx2_mm256_set_epi16(
@@ -1103,16 +1056,15 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) {
   return coefficients3;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___deserialize_10(
     Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_10(bytes);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_to_i16_array(
-    core_core_arch_x86___m256i v, int16_t ret[16U]) {
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_to_i16_array(core_core_arch_x86___m256i v,
+                                        int16_t ret[16U]) {
   int16_t output[16U] = {0U};
   libcrux_intrinsics_avx2_mm256_storeu_si256_i16(
       Eurydice_array_to_slice((size_t)16U, output, int16_t, Eurydice_slice), v);
@@ -1123,8 +1075,8 @@ typedef struct libcrux_ml_kem_vector_avx2_portable_PortableVector_s {
   int16_t elements[16U];
 } libcrux_ml_kem_vector_avx2_portable_PortableVector;
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
 libcrux_ml_kem_vector_avx2_portable_from_i16_array(int16_t array[16U]) {
   int16_t uu____0[16U];
   memcpy(uu____0, array, (size_t)16U * sizeof(int16_t));
@@ -1133,8 +1085,8 @@ libcrux_ml_kem_vector_avx2_portable_from_i16_array(int16_t array[16U]) {
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_portable_serialize_11(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_portable_serialize_11(
     libcrux_ml_kem_vector_avx2_portable_PortableVector v, uint8_t ret[22U]) {
   uint8_t result[22U] = {0U};
   result[0U] = (uint8_t)v.elements[0U];
@@ -1192,8 +1144,8 @@ static inline void libcrux_ml_kem_vector_avx2_portable_serialize_11(
   memcpy(ret, result, (size_t)22U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_11(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_serialize_serialize_11(
     core_core_arch_x86___m256i vector, uint8_t ret[22U]) {
   int16_t array[16U];
   libcrux_ml_kem_vector_avx2_to_i16_array(vector, array);
@@ -1206,8 +1158,7 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_11(
   memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___serialize_11(
     core_core_arch_x86___m256i vector, uint8_t ret[22U]) {
   uint8_t ret0[22U];
@@ -1215,8 +1166,8 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
   memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
 libcrux_ml_kem_vector_avx2_portable_zero(void) {
   libcrux_ml_kem_vector_avx2_portable_PortableVector lit;
   lit.elements[0U] = (int16_t)0;
@@ -1238,8 +1189,8 @@ libcrux_ml_kem_vector_avx2_portable_zero(void) {
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
 libcrux_ml_kem_vector_avx2_portable_deserialize_11(Eurydice_slice bytes) {
   libcrux_ml_kem_vector_avx2_portable_PortableVector result =
       libcrux_ml_kem_vector_avx2_portable_zero();
@@ -1380,14 +1331,13 @@ libcrux_ml_kem_vector_avx2_portable_deserialize_11(Eurydice_slice bytes) {
   return result;
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_portable_to_i16_array(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_portable_to_i16_array(
     libcrux_ml_kem_vector_avx2_portable_PortableVector v, int16_t ret[16U]) {
   memcpy(ret, v.elements, (size_t)16U * sizeof(int16_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_serialize_deserialize_11(Eurydice_slice bytes) {
   libcrux_ml_kem_vector_avx2_portable_PortableVector output =
       libcrux_ml_kem_vector_avx2_portable_deserialize_11(bytes);
@@ -1397,15 +1347,14 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_11(Eurydice_slice bytes) {
       Eurydice_array_to_slice((size_t)16U, ret, int16_t, Eurydice_slice));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___deserialize_11(
     Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_11(bytes);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_12(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_vector_avx2_serialize_serialize_12(
     core_core_arch_x86___m256i vector, uint8_t ret[24U]) {
   uint8_t serialized[32U] = {0U};
   core_core_arch_x86___m256i uu____0 = vector;
@@ -1471,8 +1420,7 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_serialize_12(
   memcpy(ret, ret0, (size_t)24U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___serialize_12(
     core_core_arch_x86___m256i vector, uint8_t ret[24U]) {
   uint8_t ret0[24U];
@@ -1480,8 +1428,7 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc
   memcpy(ret, ret0, (size_t)24U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_serialize_deserialize_12(Eurydice_slice bytes) {
   core_core_arch_x86___m256i shift_lsbs_to_msbs =
       libcrux_intrinsics_avx2_mm256_set_epi16(
@@ -1535,16 +1482,15 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_12(Eurydice_slice bytes) {
   return coefficients3;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___deserialize_12(
     Eurydice_slice bytes) {
   return libcrux_ml_kem_vector_avx2_serialize_deserialize_12(bytes);
 }
 
-__attribute__((target("avx2")))
-static inline size_t libcrux_ml_kem_vector_avx2_sampling_rejection_sample(
-    Eurydice_slice input, Eurydice_slice output) {
+__attribute__((target("avx2"))) static inline size_t
+libcrux_ml_kem_vector_avx2_sampling_rejection_sample(Eurydice_slice input,
+                                                     Eurydice_slice output) {
   core_core_arch_x86___m256i field_modulus =
       libcrux_intrinsics_avx2_mm256_set1_epi16(
           LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS);
@@ -1596,8 +1542,7 @@ static inline size_t libcrux_ml_kem_vector_avx2_sampling_rejection_sample(
   return uu____0 + (size_t)core_num__u8_6__count_ones(good[1U]);
 }
 
-__attribute__((target("avx2")))
-static inline size_t
+__attribute__((target("avx2"))) static inline size_t
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___rej_sample(
     Eurydice_slice input, Eurydice_slice output) {
   return libcrux_ml_kem_vector_avx2_sampling_rejection_sample(input, output);
@@ -1608,8 +1553,8 @@ typedef struct
   core_core_arch_x86___m256i coefficients[16U];
 } libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector;
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     void) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1649,15 +1594,14 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_ind_cpa_deserialize_then_decompress_u_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1088size_t_10size_t(
     size_t _) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___10int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus =
@@ -1712,16 +1656,15 @@ libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___10int32_
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___decompress_ciphertext_coefficient___10int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___10int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_10__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1748,8 +1691,7 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_10__libcrux_ml_kem_vector_a
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___11int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus =
@@ -1804,16 +1746,15 @@ libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___11int32_
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___decompress_ciphertext_coefficient___11int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___11int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_11__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1840,8 +1781,8 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_11__libcrux_ml_kem_vector_a
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_ring_element_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_10size_t(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1858,16 +1799,15 @@ typedef struct
   core_core_arch_x86___m256i snd;
 } K___libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_vector_avx2_SIMD256Vector;
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_traits_montgomery_multiply_fe__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     core_core_arch_x86___m256i v, int16_t fer) {
   return libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___montgomery_multiply_by_constant(
       v, fer);
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_ntt_ntt_layer_int_vec_step__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b,
     int16_t zeta_r) {
@@ -1883,8 +1823,7 @@ libcrux_ml_kem_ntt_ntt_layer_int_vec_step__libcrux_ml_kem_vector_avx2_SIMD256Vec
       .fst = a, .snd = b});
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_at_layer_4_plus__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1913,8 +1852,7 @@ libcrux_ml_kem_ntt_ntt_at_layer_4_plus__libcrux_ml_kem_vector_avx2_SIMD256Vector
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_at_layer_3__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1931,8 +1869,7 @@ libcrux_ml_kem_ntt_ntt_at_layer_3__libcrux_ml_kem_vector_avx2_SIMD256Vector(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_at_layer_2__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1952,8 +1889,7 @@ libcrux_ml_kem_ntt_ntt_at_layer_2__libcrux_ml_kem_vector_avx2_SIMD256Vector(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_at_layer_1__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -1977,8 +1913,7 @@ libcrux_ml_kem_ntt_ntt_at_layer_1__libcrux_ml_kem_vector_avx2_SIMD256Vector(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___poly_barrett_reduce__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self) {
@@ -1992,8 +1927,7 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_vector_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_10size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re) {
@@ -2016,8 +1950,7 @@ libcrux_ml_kem_ntt_ntt_vector_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_10size
       re);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_deserialize_then_decompress_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1088size_t_10size_t(
     uint8_t *ciphertext,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2063,8 +1996,7 @@ libcrux_ml_kem_ind_cpa_deserialize_then_decompress_u__libcrux_ml_kem_vector_avx2
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___4int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus =
@@ -2119,16 +2051,15 @@ libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___4int32_t
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___decompress_ciphertext_coefficient___4int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___4int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_4__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2154,8 +2085,7 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_4__libcrux_ml_kem_vector_av
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___5int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus =
@@ -2210,16 +2140,15 @@ libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___5int32_t
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___decompress_ciphertext_coefficient___5int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient___5int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_5__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2247,8 +2176,8 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_5__libcrux_ml_kem_vector_av
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_ring_element_v__libcrux_ml_kem_vector_avx2_SIMD256Vector_4size_t(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2259,15 +2188,15 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_ring_element_v__libcrux_ml_
   return uu____0;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_ind_cpa_deserialize_secret_key_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     size_t _) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_to_uncompressed_ring_element__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2291,8 +2220,7 @@ libcrux_ml_kem_serialize_deserialize_to_uncompressed_ring_element__libcrux_ml_ke
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_deserialize_secret_key__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     Eurydice_slice secret_key,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2328,8 +2256,8 @@ libcrux_ml_kem_ind_cpa_deserialize_secret_key__libcrux_ml_kem_vector_avx2_SIMD25
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ntt_multiply__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self,
@@ -2360,8 +2288,7 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   return out;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___add_to_ring_element__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self,
@@ -2382,8 +2309,7 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_1__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2407,8 +2333,7 @@ libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_1__libcrux_ml_kem_vector_avx2_SIMD
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_2__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2428,8 +2353,7 @@ libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_2__libcrux_ml_kem_vector_avx2_SIMD
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_3__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2446,8 +2370,8 @@ libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_3__libcrux_ml_kem_vector_avx2_SIMD
   }
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_invert_ntt_inv_ntt_layer_int_vec_step_reduce__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b,
     int16_t zeta_r) {
@@ -2464,8 +2388,7 @@ libcrux_ml_kem_invert_ntt_inv_ntt_layer_int_vec_step_reduce__libcrux_ml_kem_vect
       .fst = a, .snd = b});
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_4_plus__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     size_t *zeta_i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2496,8 +2419,7 @@ libcrux_ml_kem_invert_ntt_invert_ntt_at_layer_4_plus__libcrux_ml_kem_vector_avx2
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_invert_ntt_invert_ntt_montgomery__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re) {
@@ -2521,8 +2443,8 @@ libcrux_ml_kem_invert_ntt_invert_ntt_montgomery__libcrux_ml_kem_vector_avx2_SIMD
       re);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___subtract_reduce__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self,
@@ -2543,8 +2465,8 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   return b;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_matrix_compute_message__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *v,
@@ -2572,23 +2494,20 @@ libcrux_ml_kem_matrix_compute_message__libcrux_ml_kem_vector_avx2_SIMD256Vector_
   return result;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_arithmetic_shift_right___15int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_intrinsics_avx2_mm256_srai_epi16((int32_t)15, vector,
                                                   core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___shift_right___15int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_arithmetic_shift_right___15int32_t(vector);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_traits_to_unsigned_representative__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     core_core_arch_x86___m256i a) {
   core_core_arch_x86___m256i t =
@@ -2601,8 +2520,7 @@ libcrux_ml_kem_vector_traits_to_unsigned_representative__libcrux_ml_kem_vector_a
       a, &fm);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_message__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         re,
@@ -2632,8 +2550,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_message__libcrux_ml_kem_vector_
   memcpy(ret, serialized, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_decrypt__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1088size_t_960size_t_10size_t_4size_t(
     Eurydice_slice secret_key, uint8_t *ciphertext, uint8_t ret[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2659,8 +2576,7 @@ libcrux_ml_kem_ind_cpa_decrypt__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t
   memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___G___3size_t(
     Eurydice_slice input, uint8_t ret[64U]) {
   uint8_t digest[64U] = {0U};
@@ -2670,8 +2586,7 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, digest, (size_t)64U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRF___3size_t_32size_t(
     Eurydice_slice input, uint8_t ret[32U]) {
   uint8_t digest[32U] = {0U};
@@ -2681,15 +2596,15 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, digest, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_1152size_t_3size_t(
     size_t _i) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_to_reduced_ring_element__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice serialized) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2716,8 +2631,7 @@ libcrux_ml_kem_serialize_deserialize_to_reduced_ring_element__libcrux_ml_kem_vec
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_deserialize_ring_elements_reduced__libcrux_ml_kem_vector_avx2_SIMD256Vector_1152size_t_3size_t(
     Eurydice_slice public_key,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2753,15 +2667,14 @@ libcrux_ml_kem_serialize_deserialize_ring_elements_reduced__libcrux_ml_kem_vecto
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_matrix_sample_matrix_A_closure_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t(
     size_t _j) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_matrix_sample_matrix_A_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t(
     size_t _i,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2782,8 +2695,8 @@ libcrux_ml_kem_matrix_sample_matrix_A_closure__libcrux_ml_kem_vector_avx2_SIMD25
 typedef libcrux_sha3_avx2_x4_incremental_KeccakState
     libcrux_ml_kem_hash_functions_avx2_Simd256Hash;
 
-__attribute__((target("avx2")))
-static inline libcrux_sha3_avx2_x4_incremental_KeccakState
+__attribute__((
+    target("avx2"))) static inline libcrux_sha3_avx2_x4_incremental_KeccakState
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_init_absorb___3size_t(
     uint8_t input[3U][34U]) {
   libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
@@ -2797,8 +2710,7 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   return state;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_squeeze_three_blocks___3size_t(
     libcrux_sha3_avx2_x4_incremental_KeccakState *self, uint8_t ret[3U][504U]) {
   uint8_t out[3U][504U] = {{0U}};
@@ -2824,8 +2736,7 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, out, (size_t)3U * sizeof(uint8_t[504U]));
 }
 
-__attribute__((target("avx2")))
-static inline bool
+__attribute__((target("avx2"))) static inline bool
 libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_504size_t(
     uint8_t randomness[3U][504U], size_t *sampled_coefficients,
     int16_t (*out)[272U]) {
@@ -2869,8 +2780,7 @@ libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_ve
   return done;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_squeeze_block___3size_t(
     libcrux_sha3_avx2_x4_incremental_KeccakState *self, uint8_t ret[3U][168U]) {
   uint8_t out[3U][168U] = {{0U}};
@@ -2896,8 +2806,7 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, out, (size_t)3U * sizeof(uint8_t[168U]));
 }
 
-__attribute__((target("avx2")))
-static inline bool
+__attribute__((target("avx2"))) static inline bool
 libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_168size_t(
     uint8_t randomness[3U][168U], size_t *sampled_coefficients,
     int16_t (*out)[272U]) {
@@ -2941,8 +2850,8 @@ libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_ve
   return done;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___from_i16_array__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice a) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -2964,8 +2873,8 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   return result;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_sampling_sample_from_xof_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t(
     int16_t s[272U]) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___from_i16_array__libcrux_ml_kem_vector_avx2_SIMD256Vector(
@@ -2976,8 +2885,7 @@ libcrux_ml_kem_sampling_sample_from_xof_closure__libcrux_ml_kem_vector_avx2_SIMD
                                  Eurydice_slice));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_sampling_sample_from_xof__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t(
     uint8_t seeds[3U][34U],
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -3027,8 +2935,7 @@ libcrux_ml_kem_sampling_sample_from_xof__libcrux_ml_kem_vector_avx2_SIMD256Vecto
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_matrix_sample_matrix_A__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t(
     uint8_t seed[34U], bool transpose,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -3094,15 +3001,14 @@ typedef struct
   uint8_t snd;
 } K___libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t__uint8_t;
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_ind_cpa_sample_vector_cbd_then_ntt_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_2size_t_128size_t(
     size_t _i) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRFxN___3size_t_128size_t(
     uint8_t (*input)[33U], uint8_t ret[3U][128U]) {
   uint8_t out[3U][128U] = {{0U}};
@@ -3131,8 +3037,8 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, out, (size_t)3U * sizeof(uint8_t[128U]));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_sampling_sample_from_binomial_distribution_2__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice randomness) {
   int16_t sampled_i16s[256U] = {0U};
@@ -3180,8 +3086,8 @@ libcrux_ml_kem_sampling_sample_from_binomial_distribution_2__libcrux_ml_kem_vect
                               Eurydice_slice));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_sampling_sample_from_binomial_distribution_3__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     Eurydice_slice randomness) {
   int16_t sampled_i16s[256U] = {0U};
@@ -3227,8 +3133,8 @@ libcrux_ml_kem_sampling_sample_from_binomial_distribution_3__libcrux_ml_kem_vect
                               Eurydice_slice));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_sampling_sample_from_binomial_distribution__libcrux_ml_kem_vector_avx2_SIMD256Vector_2size_t(
     Eurydice_slice randomness) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -3239,8 +3145,7 @@ libcrux_ml_kem_sampling_sample_from_binomial_distribution__libcrux_ml_kem_vector
   return uu____0;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_at_layer_7__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re) {
@@ -3261,8 +3166,7 @@ libcrux_ml_kem_ntt_ntt_at_layer_7__libcrux_ml_kem_vector_avx2_SIMD256Vector(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ntt_ntt_binomially_sampled_ring_element__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re) {
@@ -3285,8 +3189,8 @@ libcrux_ml_kem_ntt_ntt_binomially_sampled_ring_element__libcrux_ml_kem_vector_av
       re);
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t__uint8_t
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t__uint8_t
 libcrux_ml_kem_ind_cpa_sample_vector_cbd_then_ntt__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_2size_t_128size_t(
     uint8_t prf_input[33U], uint8_t domain_separator) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -3338,15 +3242,15 @@ libcrux_ml_kem_ind_cpa_sample_vector_cbd_then_ntt__libcrux_ml_kem_vector_avx2_SI
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_ind_cpa_sample_ring_element_cbd_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_128size_t_2size_t(
     size_t _i) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t__uint8_t
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t__uint8_t
 libcrux_ml_kem_ind_cpa_sample_ring_element_cbd__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_128size_t_2size_t(
     uint8_t prf_input[33U], uint8_t domain_separator) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -3396,8 +3300,7 @@ libcrux_ml_kem_ind_cpa_sample_ring_element_cbd__libcrux_ml_kem_vector_avx2_SIMD2
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRF___3size_t_128size_t(
     Eurydice_slice input, uint8_t ret[128U]) {
   uint8_t digest[128U] = {0U};
@@ -3407,15 +3310,14 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, digest, (size_t)128U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_matrix_compute_vector_u_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     size_t _i) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___add_error_reduce__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self,
@@ -3435,8 +3337,7 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_matrix_compute_vector_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector (
         *a_as_ntt)[3U],
@@ -3501,8 +3402,7 @@ libcrux_ml_kem_matrix_compute_vector_u__libcrux_ml_kem_vector_avx2_SIMD256Vector
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_traits_decompress_1__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     core_core_arch_x86___m256i v) {
   core_core_arch_x86___m256i uu____0 =
@@ -3513,8 +3413,8 @@ libcrux_ml_kem_vector_traits_decompress_1__libcrux_ml_kem_vector_avx2_SIMD256Vec
       (int16_t)1665);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_then_decompress_message__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     uint8_t serialized[32U]) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -3538,8 +3438,8 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_message__libcrux_ml_kem_vec
   return re;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___add_message_error_reduce__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self,
@@ -3567,8 +3467,8 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   return result;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_matrix_compute_ring_element_v__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *t_as_ntt,
@@ -3598,8 +3498,7 @@ libcrux_ml_kem_matrix_compute_ring_element_v__libcrux_ml_kem_vector_avx2_SIMD256
   return result;
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___10int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus_halved =
@@ -3657,16 +3556,14 @@ libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___10int32_t(
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___compress___10int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___10int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_10__libcrux_ml_kem_vector_avx2_SIMD256Vector_320size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re,
@@ -3695,8 +3592,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_10__libcrux_ml_kem_vector_avx2_
   memcpy(ret, serialized, (size_t)320U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___11int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus_halved =
@@ -3754,16 +3650,14 @@ libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___11int32_t(
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___compress___11int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___11int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_11__libcrux_ml_kem_vector_avx2_SIMD256Vector_320size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re,
@@ -3792,8 +3686,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_11__libcrux_ml_kem_vector_avx2_
   memcpy(ret, serialized, (size_t)320U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_ring_element_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_10size_t_320size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re,
@@ -3804,8 +3697,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_ring_element_u__libcrux_ml_kem_
   memcpy(ret, uu____0, (size_t)320U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_compress_then_serialize_u__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_960size_t_10size_t_320size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         input[3U],
@@ -3840,8 +3732,7 @@ libcrux_ml_kem_ind_cpa_compress_then_serialize_u__libcrux_ml_kem_vector_avx2_SIM
   }
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___4int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus_halved =
@@ -3899,16 +3790,14 @@ libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___4int32_t(
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___compress___4int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___4int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_4__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         re,
@@ -3935,8 +3824,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_4__libcrux_ml_kem_vector_avx2_S
   }
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___5int32_t(
     core_core_arch_x86___m256i vector) {
   core_core_arch_x86___m256i field_modulus_halved =
@@ -3994,16 +3882,14 @@ libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___5int32_t(
       (int32_t)216, compressed, core_core_arch_x86___m256i);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___compress___5int32_t(
     core_core_arch_x86___m256i vector) {
   return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient___5int32_t(
       vector);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_5__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         re,
@@ -4030,8 +3916,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_5__libcrux_ml_kem_vector_avx2_S
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_compress_then_serialize_ring_element_v__libcrux_ml_kem_vector_avx2_SIMD256Vector_4size_t_128size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         re,
@@ -4040,8 +3925,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_ring_element_v__libcrux_ml_kem_
       re, out);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_encrypt__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t(
     Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness,
     uint8_t ret[1088U]) {
@@ -4135,8 +4019,7 @@ libcrux_ml_kem_ind_cpa_encrypt__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux
   memcpy(ret, ciphertext, (size_t)1088U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cca___libcrux_ml_kem__ind_cca__Variant_for_libcrux_ml_kem__ind_cca__MlKem___kdf__libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_1088size_t(
     Eurydice_slice shared_secret, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *_,
     uint8_t ret[32U]) {
@@ -4147,8 +4030,7 @@ libcrux_ml_kem_ind_cca___libcrux_ml_kem__ind_cca__Variant_for_libcrux_ml_kem__in
   memcpy(ret, out, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_libcrux_ml_kem_ind_cca_MlKem_3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t(
     libcrux_ml_kem_types_MlKemPrivateKey____2400size_t *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) {
@@ -4241,8 +4123,7 @@ libcrux_ml_kem_ind_cca_decapsulate__libcrux_ml_kem_vector_avx2_SIMD256Vector_lib
   memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate___3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t(
     libcrux_ml_kem_types_MlKemPrivateKey____2400size_t *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) {
@@ -4252,8 +4133,8 @@ libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate___3size_t_2400size_t_1152
   memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_ml_kem_mlkem768_avx2_decapsulate(
+__attribute__((target("avx2"))) static inline void
+libcrux_ml_kem_mlkem768_avx2_decapsulate(
     libcrux_ml_kem_types_MlKemPrivateKey____2400size_t *private_key,
     libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) {
   uint8_t ret0[32U];
@@ -4262,8 +4143,7 @@ static inline void libcrux_ml_kem_mlkem768_avx2_decapsulate(
   memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cca___libcrux_ml_kem__ind_cca__Variant_for_libcrux_ml_kem__ind_cca__MlKem___entropy_preprocess__libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t(
     Eurydice_slice randomness, uint8_t ret[32U]) {
   uint8_t out[32U] = {0U};
@@ -4273,8 +4153,7 @@ libcrux_ml_kem_ind_cca___libcrux_ml_kem__ind_cca__Variant_for_libcrux_ml_kem__in
   memcpy(ret, out, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___H___3size_t(
     Eurydice_slice input, uint8_t ret[32U]) {
   uint8_t digest[32U] = {0U};
@@ -4284,8 +4163,8 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for
   memcpy(ret, digest, (size_t)32U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
 libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_libcrux_ml_kem_ind_cca_MlKem_3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t(
     libcrux_ml_kem_types_MlKemPublicKey____1184size_t *public_key,
     uint8_t randomness[32U]) {
@@ -4351,8 +4230,8 @@ libcrux_ml_kem_ind_cca_encapsulate__libcrux_ml_kem_vector_avx2_SIMD256Vector_lib
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
 libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate___3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t(
     libcrux_ml_kem_types_MlKemPublicKey____1184size_t *public_key,
     uint8_t randomness[32U]) {
@@ -4363,8 +4242,8 @@ libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate___3size_t_1088size_t_1184
       uu____0, uu____1);
 }
 
-__attribute__((target("avx2")))
-static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
+__attribute__((target(
+    "avx2"))) static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_
 libcrux_ml_kem_mlkem768_avx2_encapsulate(
     libcrux_ml_kem_types_MlKemPublicKey____1184size_t *public_key,
     uint8_t randomness[32U]) {
@@ -4375,23 +4254,21 @@ libcrux_ml_kem_mlkem768_avx2_encapsulate(
       uu____0, uu____1);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_matrix_compute_As_plus_e_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     size_t _i) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_traits_to_standard_domain__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     core_core_arch_x86___m256i v) {
   return libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___montgomery_multiply_by_constant(
       v, LIBCRUX_ML_KEM_VECTOR_TRAITS_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___add_standard_error_reduce__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *self,
@@ -4411,8 +4288,7 @@ libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vec
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_matrix_compute_As_plus_e__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector (
         *matrix_A)[3U],
@@ -4475,8 +4351,7 @@ libcrux_ml_kem_matrix_compute_As_plus_e__libcrux_ml_kem_vector_avx2_SIMD256Vecto
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_serialize_uncompressed_ring_element__libcrux_ml_kem_vector_avx2_SIMD256Vector(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         *re,
@@ -4504,8 +4379,7 @@ libcrux_ml_kem_serialize_serialize_uncompressed_ring_element__libcrux_ml_kem_vec
   memcpy(ret, serialized, (size_t)384U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_serialize_secret_key__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1152size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         key[3U],
@@ -4543,8 +4417,7 @@ libcrux_ml_kem_ind_cpa_serialize_secret_key__libcrux_ml_kem_vector_avx2_SIMD256V
   memcpy(ret, out, (size_t)1152U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cpa_serialize_public_key__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1152size_t_1184size_t(
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
         t_as_ntt[3U],
@@ -4577,8 +4450,8 @@ libcrux_ml_kem_ind_cpa_serialize_public_key__libcrux_ml_kem_vector_avx2_SIMD256V
   memcpy(ret, public_key_serialized, (size_t)1184U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_utils_extraction_helper_Keypair768
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_utils_extraction_helper_Keypair768
 libcrux_ml_kem_ind_cpa_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t(
     Eurydice_slice key_generation_seed) {
   uint8_t hashed[64U];
@@ -4660,8 +4533,7 @@ libcrux_ml_kem_ind_cpa_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vecto
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_ind_cca_serialize_kem_secret_key__libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_2400size_t(
     Eurydice_slice private_key, Eurydice_slice public_key,
     Eurydice_slice implicit_rejection_value, uint8_t ret[2400U]) {
@@ -4722,8 +4594,8 @@ libcrux_ml_kem_ind_cca_serialize_kem_secret_key__libcrux_ml_kem_hash_functions_a
   memcpy(ret, out, (size_t)2400U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair
+__attribute__((
+    target("avx2"))) static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair
 libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vector_libcrux_ml_kem_hash_functions_avx2_Simd256Hash_3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t(
     uint8_t randomness[64U]) {
   Eurydice_slice ind_cpa_keypair_randomness = Eurydice_array_to_subslice(
@@ -4764,8 +4636,8 @@ libcrux_ml_kem_ind_cca_generate_keypair__libcrux_ml_kem_vector_avx2_SIMD256Vecto
           uu____3));
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair
+__attribute__((
+    target("avx2"))) static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair
 libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t(
     uint8_t randomness[64U]) {
   uint8_t uu____0[64U];
@@ -4774,8 +4646,8 @@ libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair___3size_t_1152size_t
       uu____0);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair
+__attribute__((
+    target("avx2"))) static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair
 libcrux_ml_kem_mlkem768_avx2_generate_key_pair(uint8_t randomness[64U]) {
   uint8_t uu____0[64U];
   memcpy(uu____0, randomness, (size_t)64U * sizeof(uint8_t));
@@ -4783,15 +4655,14 @@ libcrux_ml_kem_mlkem768_avx2_generate_key_pair(uint8_t randomness[64U]) {
       uu____0);
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
 libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_1184size_t_3size_t(
     size_t _i) {
   return libcrux_ml_kem_polynomial__libcrux_ml_kem__polynomial__PolynomialRingElement_Vector__TraitClause_0___ZERO__libcrux_ml_kem_vector_avx2_SIMD256Vector();
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_ml_kem_serialize_deserialize_ring_elements_reduced__libcrux_ml_kem_vector_avx2_SIMD256Vector_1184size_t_3size_t(
     Eurydice_slice public_key,
     libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -4827,8 +4698,7 @@ libcrux_ml_kem_serialize_deserialize_ring_elements_reduced__libcrux_ml_kem_vecto
               libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector));
 }
 
-__attribute__((target("avx2")))
-static inline bool
+__attribute__((target("avx2"))) static inline bool
 libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1152size_t_1184size_t(
     uint8_t *public_key) {
   libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector
@@ -4854,16 +4724,15 @@ libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_avx2_SIMD256Ve
       (size_t)1184U, public_key, public_key_serialized, uint8_t, uint8_t, bool);
 }
 
-__attribute__((target("avx2")))
-static inline bool
+__attribute__((target("avx2"))) static inline bool
 libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key___3size_t_1152size_t_1184size_t(
     uint8_t *public_key) {
   return libcrux_ml_kem_ind_cca_validate_public_key__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_1152size_t_1184size_t(
       public_key);
 }
 
-__attribute__((target("avx2")))
-static inline core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1184size_t__
+__attribute__((target(
+    "avx2"))) static inline core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1184size_t__
 libcrux_ml_kem_mlkem768_avx2_validate_public_key(
     libcrux_ml_kem_types_MlKemPublicKey____1184size_t public_key) {
   core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1184size_t__
@@ -4881,15 +4750,14 @@ libcrux_ml_kem_mlkem768_avx2_validate_public_key(
   return uu____0;
 }
 
-__attribute__((target("avx2")))
-static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
+__attribute__((target(
+    "avx2"))) static inline libcrux_ml_kem_vector_avx2_portable_PortableVector
 libcrux_ml_kem_vector_avx2_portable___core__clone__Clone_for_libcrux_ml_kem__vector__avx2__portable__PortableVector___clone(
     libcrux_ml_kem_vector_avx2_portable_PortableVector *self) {
   return self[0U];
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_ml_kem_vector_avx2___core__clone__Clone_for_libcrux_ml_kem__vector__avx2__SIMD256Vector__1__clone(
     core_core_arch_x86___m256i *self) {
   return self[0U];
diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
index 141441cb7..6c534b5cf 100644
--- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
+++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h
@@ -14,6 +14,7 @@ extern "C" {
 
 #include "eurydice_glue.h"
 #include "libcrux_core.h"
+#include "libcrux_ct_ops.h"
 #include "libcrux_sha3_portable.h"
 
 #define LIBCRUX_ML_KEM_HASH_FUNCTIONS_BLOCK_SIZE ((size_t)168U)
@@ -32,9 +33,6 @@ typedef struct libcrux_ml_kem_hash_functions_neon_Simd128Hash_s {
   (LIBCRUX_ML_KEM_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE + \
    LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE)
 
-typedef struct libcrux_ml_kem_ind_cca_MlKem_s {
-} libcrux_ml_kem_ind_cca_MlKem;
-
 typedef uint8_t libcrux_ml_kem_ind_cca_MlKemSharedSecret[32U];
 
 static const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U] =
diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
index 1e8f134ed..01bc3b938 100644
--- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
+++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h
@@ -17,18 +17,18 @@ extern "C" {
 #include "libcrux_core.h"
 #include "libcrux_sha3_portable.h"
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___zero(
     void) {
   return libcrux_intrinsics_avx2_mm256_set1_epi64x((int64_t)0);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i libcrux_sha3_simd_avx2__veor5q_u64(
-    core_core_arch_x86___m256i a, core_core_arch_x86___m256i b,
-    core_core_arch_x86___m256i c, core_core_arch_x86___m256i d,
-    core_core_arch_x86___m256i e) {
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
+libcrux_sha3_simd_avx2__veor5q_u64(core_core_arch_x86___m256i a,
+                                   core_core_arch_x86___m256i b,
+                                   core_core_arch_x86___m256i c,
+                                   core_core_arch_x86___m256i d,
+                                   core_core_arch_x86___m256i e) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   core_core_arch_x86___m256i cd = libcrux_intrinsics_avx2_mm256_xor_si256(c, d);
   core_core_arch_x86___m256i abcd =
@@ -36,8 +36,7 @@ static inline core_core_arch_x86___m256i libcrux_sha3_simd_avx2__veor5q_u64(
   return libcrux_intrinsics_avx2_mm256_xor_si256(abcd, e);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor5(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b,
     core_core_arch_x86___m256i c, core_core_arch_x86___m256i d,
@@ -45,8 +44,7 @@ libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__fo
   return libcrux_sha3_simd_avx2__veor5q_u64(a, b, c, d, e);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___1int32_t_63int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -56,64 +54,58 @@ libcrux_sha3_simd_avx2_rotate_left___1int32_t_63int32_t(
                    (int32_t)63, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i libcrux_sha3_simd_avx2__vrax1q_u64(
-    core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
+libcrux_sha3_simd_avx2__vrax1q_u64(core_core_arch_x86___m256i a,
+                                   core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i uu____0 = a;
   return libcrux_intrinsics_avx2_mm256_xor_si256(
       uu____0, libcrux_sha3_simd_avx2_rotate_left___1int32_t_63int32_t(b));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___rotate_left1_and_xor(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vrax1q_u64(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i libcrux_sha3_simd_avx2__vbcaxq_u64(
-    core_core_arch_x86___m256i a, core_core_arch_x86___m256i b,
-    core_core_arch_x86___m256i c) {
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
+libcrux_sha3_simd_avx2__vbcaxq_u64(core_core_arch_x86___m256i a,
+                                   core_core_arch_x86___m256i b,
+                                   core_core_arch_x86___m256i c) {
   core_core_arch_x86___m256i uu____0 = a;
   return libcrux_intrinsics_avx2_mm256_xor_si256(
       uu____0, libcrux_intrinsics_avx2_mm256_andnot_si256(c, b));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___and_not_xor(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b,
     core_core_arch_x86___m256i c) {
   return libcrux_sha3_simd_avx2__vbcaxq_u64(a, b, c);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i libcrux_sha3_simd_avx2__veorq_n_u64(
-    core_core_arch_x86___m256i a, uint64_t c) {
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
+libcrux_sha3_simd_avx2__veorq_n_u64(core_core_arch_x86___m256i a, uint64_t c) {
   core_core_arch_x86___m256i c0 =
       libcrux_intrinsics_avx2_mm256_set1_epi64x((int64_t)c);
   return libcrux_intrinsics_avx2_mm256_xor_si256(a, c0);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_constant(
     core_core_arch_x86___m256i a, uint64_t c) {
   return libcrux_sha3_simd_avx2__veorq_n_u64(a, c);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_slice_4(Eurydice_slice a[4U],
-                                                  size_t start, size_t len,
-                                                  Eurydice_slice ret[4U]) {
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_slice_4(Eurydice_slice a[4U], size_t start, size_t len,
+                               Eurydice_slice ret[4U]) {
   Eurydice_slice uu____0 = Eurydice_slice_subslice(
       a[0U],
       (CLITERAL(core_ops_range_Range__size_t){.start = start,
@@ -139,8 +131,7 @@ static inline void libcrux_sha3_simd_avx2_slice_4(Eurydice_slice a[4U],
                                     Eurydice_slice);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___slice_n(
     Eurydice_slice a[4U], size_t start, size_t len, Eurydice_slice ret[4U]) {
   Eurydice_slice uu____0[4U];
@@ -150,8 +141,8 @@ libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__fo
   memcpy(ret, ret0, (size_t)4U * sizeof(Eurydice_slice));
 }
 
-__attribute__((target("avx2")))
-static inline K___Eurydice_slice_uint8_t_4size_t__Eurydice_slice_uint8_t_4size_t_
+__attribute__((target(
+    "avx2"))) static inline K___Eurydice_slice_uint8_t_4size_t__Eurydice_slice_uint8_t_4size_t_
 libcrux_sha3_simd_avx2_split_at_mut_4(Eurydice_slice out[4U], size_t mid) {
   Eurydice_slice out0 = out[0U];
   Eurydice_slice out1 = out[1U];
@@ -193,8 +184,8 @@ libcrux_sha3_simd_avx2_split_at_mut_4(Eurydice_slice out[4U], size_t mid) {
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline K___Eurydice_slice_uint8_t_4size_t__Eurydice_slice_uint8_t_4size_t_
+__attribute__((target(
+    "avx2"))) static inline K___Eurydice_slice_uint8_t_4size_t__Eurydice_slice_uint8_t_4size_t_
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___split_at_mut_n(
     Eurydice_slice a[4U], size_t mid) {
   return libcrux_sha3_simd_avx2_split_at_mut_4(a, mid);
@@ -205,8 +196,8 @@ typedef struct
   core_core_arch_x86___m256i st[5U][5U];
 } libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t;
 
-__attribute__((target("avx2")))
-static inline libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
+__attribute__((target(
+    "avx2"))) static inline libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
 libcrux_sha3_generic_keccak__libcrux_sha3__generic_keccak__KeccakState_T__N__TraitClause_0__1__new__core_core_arch_x86___m256i_4size_t(
     void) {
   libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
@@ -264,8 +255,8 @@ libcrux_sha3_generic_keccak__libcrux_sha3__generic_keccak__KeccakState_T__N__Tra
   return lit;
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_load_block___136size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_load_block___136size_t(
     core_core_arch_x86___m256i (*s)[5U], Eurydice_slice blocks[4U]) {
   for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)32U; i++) {
     size_t i0 = i;
@@ -474,8 +465,7 @@ static inline void libcrux_sha3_simd_avx2_load_block___136size_t(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___load_block___136size_t(
     core_core_arch_x86___m256i (*a)[5U], Eurydice_slice b[4U]) {
   core_core_arch_x86___m256i(*uu____0)[5U] = a;
@@ -484,8 +474,7 @@ libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__fo
   libcrux_sha3_simd_avx2_load_block___136size_t(uu____0, uu____1);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___36int32_t_28int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -495,23 +484,20 @@ libcrux_sha3_simd_avx2_rotate_left___36int32_t_28int32_t(
                    (int32_t)28, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___36int32_t_28int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___36int32_t_28int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___36int32_t_28int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___36int32_t_28int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___3int32_t_61int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -521,23 +507,20 @@ libcrux_sha3_simd_avx2_rotate_left___3int32_t_61int32_t(
                    (int32_t)61, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___3int32_t_61int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___3int32_t_61int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___3int32_t_61int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___3int32_t_61int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___41int32_t_23int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -547,23 +530,20 @@ libcrux_sha3_simd_avx2_rotate_left___41int32_t_23int32_t(
                    (int32_t)23, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___41int32_t_23int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___41int32_t_23int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___41int32_t_23int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___41int32_t_23int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___18int32_t_46int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -573,38 +553,33 @@ libcrux_sha3_simd_avx2_rotate_left___18int32_t_46int32_t(
                    (int32_t)46, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___18int32_t_46int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___18int32_t_46int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___18int32_t_46int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___18int32_t_46int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___1int32_t_63int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___1int32_t_63int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___1int32_t_63int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___1int32_t_63int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___44int32_t_20int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -614,23 +589,20 @@ libcrux_sha3_simd_avx2_rotate_left___44int32_t_20int32_t(
                    (int32_t)20, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___44int32_t_20int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___44int32_t_20int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___44int32_t_20int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___44int32_t_20int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___10int32_t_54int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -640,23 +612,20 @@ libcrux_sha3_simd_avx2_rotate_left___10int32_t_54int32_t(
                    (int32_t)54, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___10int32_t_54int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___10int32_t_54int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___10int32_t_54int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___10int32_t_54int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___45int32_t_19int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -666,23 +635,20 @@ libcrux_sha3_simd_avx2_rotate_left___45int32_t_19int32_t(
                    (int32_t)19, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___45int32_t_19int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___45int32_t_19int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___45int32_t_19int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___45int32_t_19int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___2int32_t_62int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -692,23 +658,20 @@ libcrux_sha3_simd_avx2_rotate_left___2int32_t_62int32_t(
                    (int32_t)62, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___2int32_t_62int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___2int32_t_62int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___2int32_t_62int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___2int32_t_62int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___62int32_t_2int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -718,23 +681,20 @@ libcrux_sha3_simd_avx2_rotate_left___62int32_t_2int32_t(
                    (int32_t)2, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___62int32_t_2int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___62int32_t_2int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___62int32_t_2int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___62int32_t_2int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___6int32_t_58int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -744,23 +704,20 @@ libcrux_sha3_simd_avx2_rotate_left___6int32_t_58int32_t(
                    (int32_t)58, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___6int32_t_58int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___6int32_t_58int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___6int32_t_58int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___6int32_t_58int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___43int32_t_21int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -770,23 +727,20 @@ libcrux_sha3_simd_avx2_rotate_left___43int32_t_21int32_t(
                    (int32_t)21, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___43int32_t_21int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___43int32_t_21int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___43int32_t_21int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___43int32_t_21int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___15int32_t_49int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -796,23 +750,20 @@ libcrux_sha3_simd_avx2_rotate_left___15int32_t_49int32_t(
                    (int32_t)49, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___15int32_t_49int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___15int32_t_49int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___15int32_t_49int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___15int32_t_49int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___61int32_t_3int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -822,23 +773,20 @@ libcrux_sha3_simd_avx2_rotate_left___61int32_t_3int32_t(
                    (int32_t)3, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___61int32_t_3int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___61int32_t_3int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___61int32_t_3int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___61int32_t_3int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___28int32_t_36int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -848,23 +796,20 @@ libcrux_sha3_simd_avx2_rotate_left___28int32_t_36int32_t(
                    (int32_t)36, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___28int32_t_36int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___28int32_t_36int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___28int32_t_36int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___28int32_t_36int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___55int32_t_9int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -874,23 +819,20 @@ libcrux_sha3_simd_avx2_rotate_left___55int32_t_9int32_t(
                    (int32_t)9, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___55int32_t_9int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___55int32_t_9int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___55int32_t_9int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___55int32_t_9int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___25int32_t_39int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -900,23 +842,20 @@ libcrux_sha3_simd_avx2_rotate_left___25int32_t_39int32_t(
                    (int32_t)39, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___25int32_t_39int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___25int32_t_39int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___25int32_t_39int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___25int32_t_39int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___21int32_t_43int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -926,23 +865,20 @@ libcrux_sha3_simd_avx2_rotate_left___21int32_t_43int32_t(
                    (int32_t)43, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___21int32_t_43int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___21int32_t_43int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___21int32_t_43int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___21int32_t_43int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___56int32_t_8int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -952,23 +888,20 @@ libcrux_sha3_simd_avx2_rotate_left___56int32_t_8int32_t(
                    (int32_t)8, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___56int32_t_8int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___56int32_t_8int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___56int32_t_8int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___56int32_t_8int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___27int32_t_37int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -978,23 +911,20 @@ libcrux_sha3_simd_avx2_rotate_left___27int32_t_37int32_t(
                    (int32_t)37, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___27int32_t_37int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___27int32_t_37int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___27int32_t_37int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___27int32_t_37int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___20int32_t_44int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -1004,23 +934,20 @@ libcrux_sha3_simd_avx2_rotate_left___20int32_t_44int32_t(
                    (int32_t)44, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___20int32_t_44int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___20int32_t_44int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___20int32_t_44int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___20int32_t_44int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___39int32_t_25int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -1030,23 +957,20 @@ libcrux_sha3_simd_avx2_rotate_left___39int32_t_25int32_t(
                    (int32_t)25, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___39int32_t_25int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___39int32_t_25int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___39int32_t_25int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___39int32_t_25int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___8int32_t_56int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -1056,23 +980,20 @@ libcrux_sha3_simd_avx2_rotate_left___8int32_t_56int32_t(
                    (int32_t)56, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___8int32_t_56int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___8int32_t_56int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___8int32_t_56int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___8int32_t_56int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2_rotate_left___14int32_t_50int32_t(
     core_core_arch_x86___m256i x) {
   core_core_arch_x86___m256i uu____0 = libcrux_intrinsics_avx2_mm256_slli_epi64(
@@ -1082,23 +1003,20 @@ libcrux_sha3_simd_avx2_rotate_left___14int32_t_50int32_t(
                    (int32_t)50, x, core_core_arch_x86___m256i));
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2__vxarq_u64___14int32_t_50int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   core_core_arch_x86___m256i ab = libcrux_intrinsics_avx2_mm256_xor_si256(a, b);
   return libcrux_sha3_simd_avx2_rotate_left___14int32_t_50int32_t(ab);
 }
 
-__attribute__((target("avx2")))
-static inline core_core_arch_x86___m256i
+__attribute__((target("avx2"))) static inline core_core_arch_x86___m256i
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___xor_and_rotate___14int32_t_50int32_t(
     core_core_arch_x86___m256i a, core_core_arch_x86___m256i b) {
   return libcrux_sha3_simd_avx2__vxarq_u64___14int32_t_50int32_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_theta_rho__core_core_arch_x86___m256i_4size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s) {
@@ -1246,8 +1164,7 @@ libcrux_sha3_generic_keccak_theta_rho__core_core_arch_x86___m256i_4size_t(
   s->st[4U][4U] = uu____32;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_pi__core_core_arch_x86___m256i_4size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s) {
@@ -1279,8 +1196,7 @@ libcrux_sha3_generic_keccak_pi__core_core_arch_x86___m256i_4size_t(
   s->st[4U][4U] = old[4U][1U];
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_chi__core_core_arch_x86___m256i_4size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s) {
@@ -1299,8 +1215,7 @@ libcrux_sha3_generic_keccak_chi__core_core_arch_x86___m256i_4size_t(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_iota__core_core_arch_x86___m256i_4size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -1311,8 +1226,7 @@ libcrux_sha3_generic_keccak_iota__core_core_arch_x86___m256i_4size_t(
   s->st[0U][0U] = uu____0;
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_keccakf1600__core_core_arch_x86___m256i_4size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s) {
@@ -1326,8 +1240,7 @@ libcrux_sha3_generic_keccak_keccakf1600__core_core_arch_x86___m256i_4size_t(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_absorb_block__core_core_arch_x86___m256i_4size_t_136size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -1341,8 +1254,8 @@ libcrux_sha3_generic_keccak_absorb_block__core_core_arch_x86___m256i_4size_t_136
       s);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_load_block_full___136size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_load_block_full___136size_t(
     core_core_arch_x86___m256i (*s)[5U], uint8_t blocks[4U][200U]) {
   Eurydice_slice buf[4U] = {Eurydice_array_to_slice((size_t)200U, blocks[0U],
                                                     uint8_t, Eurydice_slice),
@@ -1355,8 +1268,7 @@ static inline void libcrux_sha3_simd_avx2_load_block_full___136size_t(
   libcrux_sha3_simd_avx2_load_block___136size_t(s, buf);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___load_block_full___136size_t(
     core_core_arch_x86___m256i (*a)[5U], uint8_t b[4U][200U]) {
   core_core_arch_x86___m256i(*uu____0)[5U] = a;
@@ -1365,8 +1277,7 @@ libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__fo
   libcrux_sha3_simd_avx2_load_block_full___136size_t(uu____0, uu____1);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_absorb_final__core_core_arch_x86___m256i_4size_t_136size_t_31uint8_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -1395,8 +1306,8 @@ libcrux_sha3_generic_keccak_absorb_final__core_core_arch_x86___m256i_4size_t_136
       s);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_store_block___136size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_store_block___136size_t(
     core_core_arch_x86___m256i (*s)[5U], Eurydice_slice out[4U]) {
   for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)32U; i++) {
     size_t i0 = i;
@@ -1595,8 +1506,8 @@ static inline void libcrux_sha3_simd_avx2_store_block___136size_t(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_store_block_full___136size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_store_block_full___136size_t(
     core_core_arch_x86___m256i (*s)[5U], uint8_t ret[4U][200U]) {
   uint8_t out0[200U] = {0U};
   uint8_t out1[200U] = {0U};
@@ -1622,8 +1533,7 @@ static inline void libcrux_sha3_simd_avx2_store_block_full___136size_t(
   memcpy(ret[3U], uu____3, (size_t)200U * sizeof(uint8_t));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___store_block_full___136size_t(
     core_core_arch_x86___m256i (*a)[5U], uint8_t ret[4U][200U]) {
   uint8_t ret0[4U][200U];
@@ -1631,8 +1541,7 @@ libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__fo
   memcpy(ret, ret0, (size_t)4U * sizeof(uint8_t[200U]));
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_first_and_last__core_core_arch_x86___m256i_4size_t_136size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -1656,15 +1565,13 @@ libcrux_sha3_generic_keccak_squeeze_first_and_last__core_core_arch_x86___m256i_4
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___store_block___136size_t(
     core_core_arch_x86___m256i (*a)[5U], Eurydice_slice b[4U]) {
   libcrux_sha3_simd_avx2_store_block___136size_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_first_block__core_core_arch_x86___m256i_4size_t_136size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -1673,8 +1580,7 @@ libcrux_sha3_generic_keccak_squeeze_first_block__core_core_arch_x86___m256i_4siz
       s->st, out);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_next_block__core_core_arch_x86___m256i_4size_t_136size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -1685,8 +1591,7 @@ libcrux_sha3_generic_keccak_squeeze_next_block__core_core_arch_x86___m256i_4size
       s->st, out);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_last__core_core_arch_x86___m256i_4size_t_136size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         s,
@@ -1712,8 +1617,7 @@ libcrux_sha3_generic_keccak_squeeze_last__core_core_arch_x86___m256i_4size_t_136
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_keccak__core_core_arch_x86___m256i_4size_t_136size_t_31uint8_t(
     Eurydice_slice data[4U], Eurydice_slice out[4U]) {
   libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t s =
@@ -1790,11 +1694,11 @@ libcrux_sha3_generic_keccak_keccak__core_core_arch_x86___m256i_4size_t_136size_t
   }
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_avx2_x4_shake256(
-    Eurydice_slice input0, Eurydice_slice input1, Eurydice_slice input2,
-    Eurydice_slice input3, Eurydice_slice out0, Eurydice_slice out1,
-    Eurydice_slice out2, Eurydice_slice out3) {
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_avx2_x4_shake256(Eurydice_slice input0, Eurydice_slice input1,
+                              Eurydice_slice input2, Eurydice_slice input3,
+                              Eurydice_slice out0, Eurydice_slice out1,
+                              Eurydice_slice out2, Eurydice_slice out3) {
   Eurydice_slice buf0[4U] = {input0, input1, input2, input3};
   Eurydice_slice buf[4U] = {out0, out1, out2, out3};
   libcrux_sha3_generic_keccak_keccak__core_core_arch_x86___m256i_4size_t_136size_t_31uint8_t(
@@ -1804,14 +1708,14 @@ static inline void libcrux_sha3_avx2_x4_shake256(
 typedef libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
     libcrux_sha3_avx2_x4_incremental_KeccakState;
 
-__attribute__((target("avx2")))
-static inline libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
+__attribute__((target(
+    "avx2"))) static inline libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
 libcrux_sha3_avx2_x4_incremental_shake128_init(void) {
   return libcrux_sha3_generic_keccak__libcrux_sha3__generic_keccak__KeccakState_T__N__TraitClause_0__1__new__core_core_arch_x86___m256i_4size_t();
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_load_block___168size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_load_block___168size_t(
     core_core_arch_x86___m256i (*s)[5U], Eurydice_slice blocks[4U]) {
   for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)32U; i++) {
     size_t i0 = i;
@@ -2020,8 +1924,8 @@ static inline void libcrux_sha3_simd_avx2_load_block___168size_t(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_load_block_full___168size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_load_block_full___168size_t(
     core_core_arch_x86___m256i (*s)[5U], uint8_t blocks[4U][200U]) {
   Eurydice_slice buf[4U] = {Eurydice_array_to_slice((size_t)200U, blocks[0U],
                                                     uint8_t, Eurydice_slice),
@@ -2034,8 +1938,7 @@ static inline void libcrux_sha3_simd_avx2_load_block_full___168size_t(
   libcrux_sha3_simd_avx2_load_block___168size_t(s, buf);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___load_block_full___168size_t(
     core_core_arch_x86___m256i (*a)[5U], uint8_t b[4U][200U]) {
   core_core_arch_x86___m256i(*uu____0)[5U] = a;
@@ -2044,8 +1947,7 @@ libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__fo
   libcrux_sha3_simd_avx2_load_block_full___168size_t(uu____0, uu____1);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_absorb_final__core_core_arch_x86___m256i_4size_t_168size_t_31uint8_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -2074,8 +1976,8 @@ libcrux_sha3_generic_keccak_absorb_final__core_core_arch_x86___m256i_4size_t_168
       s);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_avx2_x4_incremental_shake128_absorb_final(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_avx2_x4_incremental_shake128_absorb_final(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
     Eurydice_slice data0, Eurydice_slice data1, Eurydice_slice data2,
@@ -2085,8 +1987,8 @@ static inline void libcrux_sha3_avx2_x4_incremental_shake128_absorb_final(
       s, buf);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_simd_avx2_store_block___168size_t(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_simd_avx2_store_block___168size_t(
     core_core_arch_x86___m256i (*s)[5U], Eurydice_slice out[4U]) {
   for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)32U; i++) {
     size_t i0 = i;
@@ -2285,15 +2187,13 @@ static inline void libcrux_sha3_simd_avx2_store_block___168size_t(
   }
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_simd_avx2___libcrux_sha3__traits__internal__KeccakItem_4__usize__for_core__core_arch__x86____m256i___store_block___168size_t(
     core_core_arch_x86___m256i (*a)[5U], Eurydice_slice b[4U]) {
   libcrux_sha3_simd_avx2_store_block___168size_t(a, b);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_next_block__core_core_arch_x86___m256i_4size_t_168size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -2304,8 +2204,8 @@ libcrux_sha3_generic_keccak_squeeze_next_block__core_core_arch_x86___m256i_4size
       s->st, out);
 }
 
-__attribute__((target("avx2")))
-static inline void libcrux_sha3_avx2_x4_incremental_shake128_squeeze_next_block(
+__attribute__((target("avx2"))) static inline void
+libcrux_sha3_avx2_x4_incremental_shake128_squeeze_next_block(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
     Eurydice_slice out0, Eurydice_slice out1, Eurydice_slice out2,
@@ -2315,8 +2215,7 @@ static inline void libcrux_sha3_avx2_x4_incremental_shake128_squeeze_next_block(
       s, buf);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_first_block__core_core_arch_x86___m256i_4size_t_168size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -2325,8 +2224,7 @@ libcrux_sha3_generic_keccak_squeeze_first_block__core_core_arch_x86___m256i_4siz
       s->st, out);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_generic_keccak_squeeze_first_three_blocks__core_core_arch_x86___m256i_4size_t_168size_t(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,
@@ -2353,8 +2251,7 @@ libcrux_sha3_generic_keccak_squeeze_first_three_blocks__core_core_arch_x86___m25
       s, o2);
 }
 
-__attribute__((target("avx2")))
-static inline void
+__attribute__((target("avx2"))) static inline void
 libcrux_sha3_avx2_x4_incremental_shake128_squeeze_first_three_blocks(
     libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t
         *s,