Regenerate code with the C++ tweak

cryspen · Jun 10, 2024 · 9418eef · 9418eef
1 parent c851d5b
commit 9418eef
Show file tree

Hide file tree

Showing 43 changed files with 707 additions and 11,707 deletions.
diff --git a/libcrux-ml-kem/c.yaml b/libcrux-ml-kem/c.yaml
@@ -14,7 +14,7 @@ files:
  - [libcrux_intrinsics, avx2]
 
  - name: libcrux_platform
- api:
+ private:
  - [libcrux_platform, "*"]
 
  # SHA3 (no mention of libcrux_mlkem in this section, please)

diff --git a/libcrux-ml-kem/c/eurydice_glue.h b/libcrux-ml-kem/c/eurydice_glue.h
@@ -22,9 +22,9 @@ extern "C" {
 // SLICES, ARRAYS, ETC.
 
 #if defined(__cplusplus)
- #define CLITERAL(type)  type
+#define CLITERAL(type) type
 #else
- #define CLITERAL(type)  (type)
+#define CLITERAL(type) (type)
 #endif
 
 // We represent a slice as a pair of an (untyped) pointer, along with the length
@@ -89,12 +89,14 @@ typedef struct {
  Eurydice_array_eq
 
 #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), \
- .snd = EURYDICE_SLICE((element_type *)slice.ptr, mid, slice.len)})
+ (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), \
- .len = slice.len - mid}})
+ (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.
@@ -166,8 +168,9 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
 #define core_num_nonzero_NonZeroUsize size_t
 #define Eurydice_range_iter_next(iter_ptr, t, ret_t) \
  (((iter_ptr)->start == (iter_ptr)->end) \
- ? (CLITERAL(ret_t){.tag = core_option_None}) \
- : (CLITERAL(ret_t){.tag = core_option_Some, .f0 = (iter_ptr)->start++}))
+ ? (CLITERAL(ret_t){.tag = core_option_None}) \
+ : (CLITERAL(ret_t){.tag = core_option_Some, \
+ .f0 = (iter_ptr)->start++}))
 
 // Old name (TODO: remove once everyone has upgraded to the latest Charon)
 #define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next \
@@ -232,9 +235,10 @@ typedef struct {
  ret_t) \
  (((iter)->index == (iter)->s.len) \
  ? (CLITERAL(ret_t){.tag = core_option_None}) \
- : (CLITERAL(ret_t){.tag = core_option_Some, \
- .f0 = ((iter)->index++, \
- &((t *)((iter)->s.ptr))[(iter)->index - 1])}))
+ : (CLITERAL(ret_t){ \
+ .tag = core_option_Some, \
+ .f0 = ((iter)->index++, \
+ &((t *)((iter)->s.ptr))[(iter)->index - 1])}))
 
 // STRINGS
 

diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __internal_libcrux_core_H
@@ -15,6 +15,9 @@ extern "C" {
 #include "../libcrux_core.h"
 #include "eurydice_glue.h"
 
+extern void core_fmt_rt__core__fmt__rt__Argument__a__1__none(
+ core_fmt_rt_Argument x0[0U]);
+
 extern core_fmt_Arguments core_fmt__core__fmt__Arguments__a__2__new_v1(
  Eurydice_slice x0, Eurydice_slice x1);
 

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_neon.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_neon.h
diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __internal_libcrux_sha3_internal_H

diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #include "internal/libcrux_core.h"
@@ -50,7 +50,8 @@ libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
 libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___3168size_t_1568size_t(
  libcrux_ml_kem_types_MlKemPrivateKey____3168size_t sk,
  libcrux_ml_kem_types_MlKemPublicKey____1568size_t pk) {
- return ((libcrux_ml_kem_mlkem1024_MlKem1024KeyPair){.sk = sk, .pk = pk});
+ return (
+ CLITERAL(libcrux_ml_kem_mlkem1024_MlKem1024KeyPair){.sk = sk, .pk = pk});
 }
 
 libcrux_ml_kem_types_MlKemPrivateKey____3168size_t
@@ -108,7 +109,7 @@ void libcrux_ml_kem_ind_cpa_into_padded_array___1600size_t(Eurydice_slice slice,
  core_slice___Slice_T___copy_from_slice(
  Eurydice_array_to_subslice(
  (size_t)1600U, uu____0,
- ((core_ops_range_Range__size_t){
+ (CLITERAL(core_ops_range_Range__size_t){
  .start = (size_t)0U,
  .end = core_slice___Slice_T___len(slice, uint8_t, size_t)}),
  uint8_t, core_ops_range_Range__size_t, Eurydice_slice),
@@ -130,7 +131,8 @@ libcrux_ml_kem_mlkem768_MlKem768KeyPair
 libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t(
  libcrux_ml_kem_types_MlKemPrivateKey____2400size_t sk,
  libcrux_ml_kem_types_MlKemPublicKey____1184size_t pk) {
- return ((libcrux_ml_kem_mlkem768_MlKem768KeyPair){.sk = sk, .pk = pk});
+ return (
+ CLITERAL(libcrux_ml_kem_mlkem768_MlKem768KeyPair){.sk = sk, .pk = pk});
 }
 
 libcrux_ml_kem_types_MlKemPrivateKey____2400size_t
@@ -188,7 +190,7 @@ void libcrux_ml_kem_ind_cpa_into_padded_array___1120size_t(Eurydice_slice slice,
  core_slice___Slice_T___copy_from_slice(
  Eurydice_array_to_subslice(
  (size_t)1120U, uu____0,
- ((core_ops_range_Range__size_t){
+ (CLITERAL(core_ops_range_Range__size_t){
  .start = (size_t)0U,
  .end = core_slice___Slice_T___len(slice, uint8_t, size_t)}),
  uint8_t, core_ops_range_Range__size_t, Eurydice_slice),
@@ -210,7 +212,7 @@ libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t
 libcrux_ml_kem_types__libcrux_ml_kem__types__MlKemKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___1632size_t_800size_t(
  libcrux_ml_kem_types_MlKemPrivateKey____1632size_t sk,
  libcrux_ml_kem_types_MlKemPublicKey____800size_t pk) {
- return ((libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t){
+ return (CLITERAL(libcrux_ml_kem_types_MlKemKeyPair____1632size_t__800size_t){
  .sk = sk, .pk = pk});
 }
 
@@ -262,7 +264,7 @@ void libcrux_ml_kem_ind_cpa_into_padded_array___33size_t(Eurydice_slice slice,
  core_slice___Slice_T___copy_from_slice(
  Eurydice_array_to_subslice(
  (size_t)33U, uu____0,
- ((core_ops_range_Range__size_t){
+ (CLITERAL(core_ops_range_Range__size_t){
  .start = (size_t)0U,
  .end = core_slice___Slice_T___len(slice, uint8_t, size_t)}),
  uint8_t, core_ops_range_Range__size_t, Eurydice_slice),
@@ -277,7 +279,7 @@ void libcrux_ml_kem_ind_cpa_into_padded_array___34size_t(Eurydice_slice slice,
  core_slice___Slice_T___copy_from_slice(
  Eurydice_array_to_subslice(
  (size_t)34U, uu____0,
- ((core_ops_range_Range__size_t){
+ (CLITERAL(core_ops_range_Range__size_t){
  .start = (size_t)0U,
  .end = core_slice___Slice_T___len(slice, uint8_t, size_t)}),
  uint8_t, core_ops_range_Range__size_t, Eurydice_slice),
@@ -299,7 +301,7 @@ void libcrux_ml_kem_ind_cpa_into_padded_array___800size_t(Eurydice_slice slice,
  core_slice___Slice_T___copy_from_slice(
  Eurydice_array_to_subslice(
  (size_t)800U, uu____0,
- ((core_ops_range_Range__size_t){
+ (CLITERAL(core_ops_range_Range__size_t){
  .start = (size_t)0U,
  .end = core_slice___Slice_T___len(slice, uint8_t, size_t)}),
  uint8_t, core_ops_range_Range__size_t, Eurydice_slice),
@@ -314,7 +316,7 @@ void libcrux_ml_kem_ind_cpa_into_padded_array___64size_t(Eurydice_slice slice,
  core_slice___Slice_T___copy_from_slice(
  Eurydice_array_to_subslice(
  (size_t)64U, uu____0,
- ((core_ops_range_Range__size_t){
+ (CLITERAL(core_ops_range_Range__size_t){
  .start = (size_t)0U,
  .end = core_slice___Slice_T___len(slice, uint8_t, size_t)}),
  uint8_t, core_ops_range_Range__size_t, Eurydice_slice),

diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __libcrux_core_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __libcrux_mlkem1024_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #include "libcrux_mlkem1024_avx2.h"
@@ -43,11 +43,11 @@ libcrux_ml_kem_mlkem1024_avx2_validate_public_key(
  uu____0;
  if (libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key___4size_t_1536size_t_1568size_t(
  public_key.value)) {
- uu____0 = ((
+ uu____0 = (CLITERAL(
  core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1568size_t__){
  .tag = core_option_Some, .f0 = public_key});
  } else {
- uu____0 = ((
+ uu____0 = (CLITERAL(
  core_option_Option__libcrux_ml_kem_types_MlKemPublicKey___1568size_t__){
  .tag = core_option_None});
  }

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
@@ -1,8 +1,8 @@
 /*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
- KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
- ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
- KaRaMeL version: 40e3a603
+ KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../c.yaml
+ ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: 58c915a8 KaRaMeL
+ version: 40e3a603
  */
 
 #ifndef __libcrux_mlkem1024_avx2_H