Merge pull request #472 from cryspen/protz_cosmetic

Leverage latest code quality improvements in Eurydice etc.

.docker/c/install.sh

@@ -25,24 +25,24 @@ unzip hacl-star.zip
 rm -rf hacl-star.zip
 mv hacl-star-2a8b61343a1a7232611cb763b0dc3e4dff84d656/ hacl-star
 
-curl -L https://github.com/AeneasVerif/charon/archive/3f6d1c304e0e5bef1e9e2ea65aec703661b05f39.zip \
+curl -L https://github.com/AeneasVerif/charon/archive/962f26311ccdf09a6a3cfeacbccafba22bf3d405.zip \
     --output charon.zip
 unzip charon.zip
 rm -rf charon.zip
-mv charon-3f6d1c304e0e5bef1e9e2ea65aec703661b05f39/ charon
+mv charon-962f26311ccdf09a6a3cfeacbccafba22bf3d405/ charon
 
 
-curl -L https://github.com/FStarLang/karamel/archive/fc56fce6a58754766809845f88fc62063b2c6b92.zip \
+curl -L https://github.com/FStarLang/karamel/archive/7862fdc3899b718d39ec98568f78ec40592a622a.zip \
     --output karamel.zip
 unzip karamel.zip
 rm -rf karamel.zip
-mv karamel-fc56fce6a58754766809845f88fc62063b2c6b92/ karamel
+mv karamel-7862fdc3899b718d39ec98568f78ec40592a622a/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/392674166bac86e60f5fffa861181a398fdc3896.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/e66abbc2119485abfafa17c1911bdbdada5b04f3.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-392674166bac86e60f5fffa861181a398fdc3896/ eurydice
+mv eurydice-e66abbc2119485abfafa17c1911bdbdada5b04f3/ eurydice
 
 echo "export FSTAR_HOME=$HOME/fstar" >>$HOME/.profile
 echo "export HACL_HOME=$HOME/hacl-star" >>$HOME/.profile

libcrux-ml-kem/c.yaml

@@ -230,3 +230,10 @@ files:
     private:
       - [libcrux_ml_kem, "*"]
     inline_static: true
+
+naming:
+  skip_prefix:
+    - [ core, core_arch, arm_shared, neon ]
+    - [ core, core_arch, x86 ]
+    - [libcrux_intrinsics, arm64]
+    - [libcrux_intrinsics, avx2]

libcrux-ml-kem/c/code_gen.txt

@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: 53530427db2941ce784201e64086766504bc5642
-Eurydice: 67f4341506300372fba9cb8de070234935839cb7
-Karamel: f9cdef256a2b88282398a609847b34dd8c9cf3e3
-F*: 58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7
-Libcrux: 06b02e72e21705b53062d5988d3233715af43ad2
+Charon: 962f26311ccdf09a6a3cfeacbccafba22bf3d405
+Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3
+Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a
+F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty
+Libcrux: 322297aa4545eea6f5ba5d5fdd1565a790e5f726

libcrux-ml-kem/c/eurydice_glue.h

@@ -54,33 +54,33 @@ typedef struct {
 // which is NOT correct C syntax, so we add a dedicated phase in Eurydice that
 // adds an extra argument to this macro at the last minute so that we have the
 // correct type of *pointers* to elements.
-#define Eurydice_slice_index(s, i, t, t_ptr_t, _ret_t) (((t_ptr_t)s.ptr)[i])
-#define Eurydice_slice_subslice(s, r, t, _, _ret_t) \
+#define Eurydice_slice_index(s, i, t, t_ptr_t) (((t_ptr_t)s.ptr)[i])
+#define Eurydice_slice_subslice(s, r, t, _) \
   EURYDICE_SLICE((t *)s.ptr, r.start, r.end)
 // Variant for when the start and end indices are statically known (i.e., the
 // range argument `r` is a literal).
-#define Eurydice_slice_subslice2(s, start, end, t, _) \
+#define Eurydice_slice_subslice2(s, start, end, t) \
   EURYDICE_SLICE((t *)s.ptr, start, end)
-#define Eurydice_slice_subslice_to(s, subslice_end_pos, t, _, _ret_t) \
+#define Eurydice_slice_subslice_to(s, subslice_end_pos, t, _) \
   EURYDICE_SLICE((t *)s.ptr, 0, subslice_end_pos)
-#define Eurydice_slice_subslice_from(s, subslice_start_pos, t, _, _ret_t) \
+#define Eurydice_slice_subslice_from(s, subslice_start_pos, t, _) \
   EURYDICE_SLICE((t *)s.ptr, subslice_start_pos, s.len)
-#define Eurydice_array_to_slice(end, x, t, _ret_t) \
-  EURYDICE_SLICE(x, 0,                             \
+#define Eurydice_array_to_slice(end, x, t) \
+  EURYDICE_SLICE(x, 0,                     \
                  end) /* x is already at an array type, no need for cast */
-#define Eurydice_array_to_subslice(_arraylen, x, r, t, _, _ret_t) \
+#define Eurydice_array_to_subslice(_arraylen, x, r, t, _) \
   EURYDICE_SLICE((t *)x, r.start, r.end)
 // Same as above, variant for when start and end are statically known
-#define Eurydice_array_to_subslice2(x, start, end, t, _ret_t) \
+#define Eurydice_array_to_subslice2(x, start, end, t) \
   EURYDICE_SLICE((t *)x, start, end)
-#define Eurydice_array_to_subslice_to(_size, x, r, t, _range_t, _ret_t) \
+#define Eurydice_array_to_subslice_to(_size, x, r, t, _range_t) \
   EURYDICE_SLICE((t *)x, 0, r)
-#define Eurydice_array_to_subslice_from(size, x, r, t, _range_t, _ret_t) \
+#define Eurydice_array_to_subslice_from(size, x, r, t, _range_t) \
   EURYDICE_SLICE((t *)x, r, size)
-#define Eurydice_array_repeat(dst, len, init, t, _ret_t) \
+#define Eurydice_array_repeat(dst, len, init, t) \
   ERROR "should've been desugared"
-#define core_slice___Slice_T___len(s, t, _ret_t) EURYDICE_SLICE_LEN(s, t)
-#define core_slice___Slice_T___copy_from_slice(dst, src, t, _ret_t) \
+#define Eurydice_slice_len(s, t) EURYDICE_SLICE_LEN(s, t)
+#define Eurydice_slice_copy(dst, src, t) \
   memcpy(dst.ptr, src.ptr, dst.len * sizeof(t))
 #define core_array___Array_T__N__23__as_slice(len_, ptr_, t, _ret_t) \
   ((Eurydice_slice){.ptr = ptr_, .len = len_})
@@ -90,25 +90,26 @@ typedef struct {
   (memcpy(dst, src, len * sizeof(elem_type)))
 #define core_array_TryFromSliceError uint8_t
 
-#define Eurydice_array_eq(sz, a1, a2, t, _, _ret_t) \
+#define Eurydice_array_eq(sz, a1, a2, t, _) \
   (memcmp(a1, a2, sz * sizeof(t)) == 0)
-#define core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq \
-  Eurydice_array_eq
+#define core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq( \
+    sz, a1, a2, t, _, _ret_t)                                                           \
+  Eurydice_array_eq(sz, a1, a2, t, _)
 
-#define core_slice___Slice_T___split_at(slice, mid, element_type, ret_t) \
-  (CLITERAL(ret_t){                                                      \
-      .fst = EURYDICE_SLICE((element_type *)slice.ptr, 0, mid),          \
+#define Eurydice_slice_split_at(slice, mid, element_type, ret_t) \
+  (CLITERAL(ret_t){                                              \
+      .fst = EURYDICE_SLICE((element_type *)slice.ptr, 0, mid),  \
       .snd = EURYDICE_SLICE((element_type *)slice.ptr, mid, slice.len)})
-#define core_slice___Slice_T___split_at_mut(slice, mid, element_type, ret_t) \
-  (CLITERAL(ret_t){                                                          \
-      .fst = {.ptr = slice.ptr, .len = mid},                                 \
-      .snd = {.ptr = (char *)slice.ptr + mid * sizeof(element_type),         \
+#define Eurydice_slice_split_at_mut(slice, mid, element_type, ret_t) \
+  (CLITERAL(ret_t){                                                  \
+      .fst = {.ptr = slice.ptr, .len = mid},                         \
+      .snd = {.ptr = (char *)slice.ptr + mid * sizeof(element_type), \
               .len = slice.len - mid}})
 
 // Conversion of slice to an array, rewritten (by Eurydice) to name the
 // destination array, since arrays are not values in C.
 // N.B.: see note in karamel/lib/Inlining.ml if you change this.
-#define Eurydice_slice_to_array2(dst, src, _, t_arr, _ret_t)              \
+#define Eurydice_slice_to_array2(dst, src, _, t_arr)                      \
   Eurydice_slice_to_array3(&(dst)->tag, (char *)&(dst)->val.case_Ok, src, \
                            sizeof(t_arr))