update C extration

cryspen · Jun 12, 2024 · 5b13693 · 5b13693
1 parent ccc7d28
commit 5b13693
Show file tree

Hide file tree

Showing 6 changed files with 478 additions and 542 deletions.
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -1,5 +1,5 @@
 This code was generated with the following tools:
 Charon: 0b8b7a82c2a18f65ab9df16f222d52594c17f59c
-Eurydice: f5a2305081d09f3b45ed272e5388e542f4c4a7c1
+Eurydice: ec9da30ba3723647ca6f03810cfcfd418bd48bf8
 Karamel: 22425a93c68d9e3794909f98854aaffdc0560510
 F*: 
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -148,36 +148,12 @@ uint8_t
 libcrux_ml_kem_constant_time_ops_compare_ciphertexts_in_constant_time___768size_t(
     Eurydice_slice lhs, Eurydice_slice rhs);
 
-typedef struct
-    K___Eurydice_slice_uint8_t_128size_t__Eurydice_slice_uint8_t_128size_t__s {
-  Eurydice_slice fst;
-  Eurydice_slice snd;
-} K___Eurydice_slice_uint8_t_128size_t__Eurydice_slice_uint8_t_128size_t_;
-
-typedef struct
-    K___Eurydice_slice_uint8_t_192size_t__Eurydice_slice_uint8_t_192size_t__s {
-  Eurydice_slice fst;
-  Eurydice_slice snd;
-} K___Eurydice_slice_uint8_t_192size_t__Eurydice_slice_uint8_t_192size_t_;
-
 void libcrux_ml_kem_utils_into_padded_array___33size_t(Eurydice_slice slice,
                                                        uint8_t ret[33U]);
 
 void libcrux_ml_kem_utils_into_padded_array___34size_t(Eurydice_slice slice,
                                                        uint8_t ret[34U]);
 
-typedef struct
-    K___Eurydice_slice_uint8_t_168size_t__Eurydice_slice_uint8_t_168size_t__s {
-  Eurydice_slice fst;
-  Eurydice_slice snd;
-} K___Eurydice_slice_uint8_t_168size_t__Eurydice_slice_uint8_t_168size_t_;
-
-typedef struct
-    K___Eurydice_slice_uint8_t_504size_t__Eurydice_slice_uint8_t_504size_t__s {
-  Eurydice_slice fst;
-  Eurydice_slice snd;
-} K___Eurydice_slice_uint8_t_504size_t__Eurydice_slice_uint8_t_504size_t_;
-
 Eurydice_slice
 libcrux_ml_kem_types___core__convert__AsRef__Slice_u8___for_libcrux_ml_kem__types__MlKemCiphertext_SIZE___1__as_ref___768size_t(
     libcrux_ml_kem_types_MlKemCiphertext____768size_t *self);

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -45,7 +45,7 @@ libcrux_sha3_generic_keccak_squeeze_first_three_blocks__uint64_t_1size_t_168size
     libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
     Eurydice_slice out[1U]) {
   K___Eurydice_slice_uint8_t_1size_t__Eurydice_slice_uint8_t_1size_t_ uu____0 =
-      libcrux_sha3_portable_keccak___libcrux_sha3__traits__KeccakItem_1__usize__for_u64___split_at_mut_n(
+      libcrux_sha3_portable_keccak___libcrux_sha3__traits__internal__KeccakItem_1__usize__for_u64___split_at_mut_n(
           out, (size_t)168U);
   Eurydice_slice o0[1U];
   memcpy(o0, uu____0.fst, (size_t)1U * sizeof(Eurydice_slice));
@@ -54,7 +54,7 @@ libcrux_sha3_generic_keccak_squeeze_first_three_blocks__uint64_t_1size_t_168size
   libcrux_sha3_generic_keccak_squeeze_first_block__uint64_t_1size_t_168size_t(
       s, o0);
   K___Eurydice_slice_uint8_t_1size_t__Eurydice_slice_uint8_t_1size_t_ uu____1 =
-      libcrux_sha3_portable_keccak___libcrux_sha3__traits__KeccakItem_1__usize__for_u64___split_at_mut_n(
+      libcrux_sha3_portable_keccak___libcrux_sha3__traits__internal__KeccakItem_1__usize__for_u64___split_at_mut_n(
           o10, (size_t)168U);
   Eurydice_slice o1[1U];
   memcpy(o1, uu____1.fst, (size_t)1U * sizeof(Eurydice_slice));
@@ -129,7 +129,7 @@ libcrux_sha3_generic_keccak_squeeze_first_five_blocks__uint64_t_1size_t_168size_
     libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t *s,
     Eurydice_slice out[1U]) {
   K___Eurydice_slice_uint8_t_1size_t__Eurydice_slice_uint8_t_1size_t_ uu____0 =
-      libcrux_sha3_portable_keccak___libcrux_sha3__traits__KeccakItem_1__usize__for_u64___split_at_mut_n(
+      libcrux_sha3_portable_keccak___libcrux_sha3__traits__internal__KeccakItem_1__usize__for_u64___split_at_mut_n(
           out, (size_t)168U);
   Eurydice_slice o0[1U];
   memcpy(o0, uu____0.fst, (size_t)1U * sizeof(Eurydice_slice));
@@ -138,7 +138,7 @@ libcrux_sha3_generic_keccak_squeeze_first_five_blocks__uint64_t_1size_t_168size_
   libcrux_sha3_generic_keccak_squeeze_first_block__uint64_t_1size_t_168size_t(
       s, o0);
   K___Eurydice_slice_uint8_t_1size_t__Eurydice_slice_uint8_t_1size_t_ uu____1 =
-      libcrux_sha3_portable_keccak___libcrux_sha3__traits__KeccakItem_1__usize__for_u64___split_at_mut_n(
+      libcrux_sha3_portable_keccak___libcrux_sha3__traits__internal__KeccakItem_1__usize__for_u64___split_at_mut_n(
           o10, (size_t)168U);
   Eurydice_slice o1[1U];
   memcpy(o1, uu____1.fst, (size_t)1U * sizeof(Eurydice_slice));
@@ -147,7 +147,7 @@ libcrux_sha3_generic_keccak_squeeze_first_five_blocks__uint64_t_1size_t_168size_
   libcrux_sha3_generic_keccak_squeeze_next_block__uint64_t_1size_t_168size_t(
       s, o1);
   K___Eurydice_slice_uint8_t_1size_t__Eurydice_slice_uint8_t_1size_t_ uu____2 =
-      libcrux_sha3_portable_keccak___libcrux_sha3__traits__KeccakItem_1__usize__for_u64___split_at_mut_n(
+      libcrux_sha3_portable_keccak___libcrux_sha3__traits__internal__KeccakItem_1__usize__for_u64___split_at_mut_n(
           o20, (size_t)168U);
   Eurydice_slice o2[1U];
   memcpy(o2, uu____2.fst, (size_t)1U * sizeof(Eurydice_slice));
@@ -156,7 +156,7 @@ libcrux_sha3_generic_keccak_squeeze_first_five_blocks__uint64_t_1size_t_168size_
   libcrux_sha3_generic_keccak_squeeze_next_block__uint64_t_1size_t_168size_t(
       s, o2);
   K___Eurydice_slice_uint8_t_1size_t__Eurydice_slice_uint8_t_1size_t_ uu____3 =
-      libcrux_sha3_portable_keccak___libcrux_sha3__traits__KeccakItem_1__usize__for_u64___split_at_mut_n(
+      libcrux_sha3_portable_keccak___libcrux_sha3__traits__internal__KeccakItem_1__usize__for_u64___split_at_mut_n(
           o30, (size_t)168U);
   Eurydice_slice o3[1U];
   memcpy(o3, uu____3.fst, (size_t)1U * sizeof(Eurydice_slice));