Merge pull request #453 from cryspen/franziskus/ml-kem-c-update

ml kem c update

include/Hacl_Hash_SHA3_Simd256.h

@@ -141,12 +141,12 @@ Hacl_Hash_SHA3_Simd256_sha3_512(
 /**
 Allocate quadruple state buffer (200-bytes for each)
 */
-uint64_t *Hacl_Hash_SHA3_Simd256_state_malloc(void);
+Lib_IntVector_Intrinsics_vec256 *Hacl_Hash_SHA3_Simd256_state_malloc(void);
 
 /**
 Free quadruple state buffer
 */
-void Hacl_Hash_SHA3_Simd256_state_free(uint64_t *s);
+void Hacl_Hash_SHA3_Simd256_state_free(Lib_IntVector_Intrinsics_vec256 *s);
 
 /**
 Absorb number of blocks of 4 input buffers and write the output states

libcrux/include/Eurydice.h

@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
+  F* version: a32b316e
+  KaRaMeL version: abb38e1d
  */
 
 #ifndef __Eurydice_H

libcrux/include/core.h

@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
+  F* version: a32b316e
+  KaRaMeL version: abb38e1d
  */
 
 #ifndef __core_H

libcrux/include/eurydice_glue.h

@@ -45,7 +45,8 @@ typedef struct {
 
 #define core_array_TryFromSliceError uint8_t
 
-#define core_array_equality___Array_A__N___eq(sz, a1, a2, t, _, _ret_t) (memcmp(a1, a2, sz * sizeof(t)) == 0)
+#define Eurydice_array_eq(sz, a1, a2, t, _, _ret_t) (memcmp(a1, a2, sz * sizeof(t)) == 0)
+#define core_array_equality___core__cmp__PartialEq__Array_B__N___for__Array_A__N____eq Eurydice_array_eq
 
 #define core_slice___Slice_T___split_at(slice, mid, element_type, ret_t) \
   ((ret_t){ \
@@ -74,8 +75,12 @@ static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) {
   memcpy(dst, &x, 4);
 }
 
-static inline int64_t core_convert_num__i64_59__from(int32_t x) { return x; }
-static inline int32_t core_convert_num__i32_56__from(int16_t x) { return x; }
+static inline int64_t
+core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x)
+{
+  return x;
+}
+
 // unsigned overflow wraparound semantics in C
 static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x, uint16_t y) { return x + y; }
 static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x, uint8_t y) { return x - y; }
@@ -90,13 +95,16 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { return (*p) >>
 // ITERATORS
 
 #define core_num_nonzero_NonZeroUsize size_t
-#define core_iter_range__core__ops__range__Range_A__3__next(iter_ptr, t, ret_t) ( \
+#define Eurydice_range_iter_next(iter_ptr, t, ret_t) ( \
   ((iter_ptr)->start == (iter_ptr)->end) ? \
     ((ret_t) { .tag = core_option_None }) : \
     ((ret_t) { .tag = core_option_Some, .f0 = (iter_ptr)->start++ }) \
   )
 
-#define core_iter_traits_collect__I__into_iter(x, t, _ret_t) (x)
+#define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next Eurydice_range_iter_next
+
+#define Eurydice_into_iter(x, t, _ret_t) (x)
+#define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter Eurydice_into_iter
 
 typedef struct {
   Eurydice_slice slice;
@@ -123,7 +131,7 @@ static inline Eurydice_slice chunk_next(Eurydice_chunks *chunks, size_t element_
     .chunk_size = sz_ })
 #define core_slice_iter_Chunks Eurydice_chunks
 #define core_slice_iter_ChunksExact Eurydice_chunks
-#define core_slice_iter__core__slice__iter__Chunks__a__T__70__next(iter, t, ret_t) \
+#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___70__next(iter, t, ret_t) \
   (((iter)->slice.len == 0) ? \
     ((ret_t) { .tag = core_option_None }) : \
     ((ret_t){ \

libcrux/include/internal/core.h

@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
+  F* version: a32b316e
+  KaRaMeL version: abb38e1d
  */
 
 #ifndef __internal_core_H
@@ -11,7 +11,8 @@
 #include "../core.h"
 #include "eurydice_glue.h"
 
-static inline int64_t core_convert_num__i64_59__from(int32_t x0);
+static inline int64_t
+core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x0);
 
 typedef struct core_option_Option__size_t_s
 {

libcrux/include/internal/libcrux_kyber.h

@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
+  F* version: a32b316e
+  KaRaMeL version: abb38e1d
  */
 
 #ifndef __internal_libcrux_kyber_H

libcrux/include/libcrux_digest.h

@@ -1,14 +1,15 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
+  F* version: a32b316e
+  KaRaMeL version: abb38e1d
  */
 
 #ifndef __libcrux_digest_H
 #define __libcrux_digest_H
 
 #include "eurydice_glue.h"
+#include "libcrux_hacl_glue.h"
 
 extern void libcrux_digest_sha3_512(Eurydice_slice x0, uint8_t x1[64U]);
 
@@ -18,10 +19,6 @@ extern void libcrux_digest_sha3_256(Eurydice_slice x0, uint8_t x1[32U]);
 
 extern void libcrux_digest_shake256_(size_t x0, Eurydice_slice x1, uint8_t *x2);
 
-#define libcrux_digest_shake128(x_0, x_1, x_2, _ret_t) libcrux_digest_shake128_(x_0, x_1, x_2)
-
-extern void libcrux_digest_shake128_(size_t x0, Eurydice_slice x1, uint8_t *x2);
-
 
 #define __libcrux_digest_H_DEFINED
 #endif

libcrux/include/libcrux_hacl_glue.h

@@ -1,14 +1,45 @@
+/* Hand-written file */
+
 #pragma once
 
-#include "eurydice_glue.h"
-#include "libcrux_kyber.h"
+#include "Eurydice.h"
+
+#include <stdint.h>
+#include <string.h>
+
+#ifdef HACL_CAN_COMPILE_VEC256
+#include "libintvector.h"
+typedef struct libcrux_digest_incremental_x4_Shake128StateX4
+{
+  Lib_IntVector_Intrinsics_vec256* x4;
+  uint64_t* st0;
+  uint64_t* st1;
+  uint64_t* st2;
+  uint64_t* st3;
+} libcrux_digest_incremental_x4_Shake128StateX4;
+#else
+typedef struct libcrux_digest_incremental_x4_Shake128StateX4
+{
+  uint64_t* st0;
+  uint64_t* st1;
+  uint64_t* st2;
+  uint64_t* st3;
+} libcrux_digest_incremental_x4_Shake128StateX4;
+#endif
+
+extern void
+libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__squeeze_blocks_f(
+  libcrux_digest_incremental_x4_Shake128StateX4* xof_state,
+  size_t block_len,
+  uint8_t* output);
 
-extern K___uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_
-libcrux_digest_shake128x4f(size_t len,
-                           Eurydice_slice input0,
-                           Eurydice_slice input1,
-                           Eurydice_slice input2,
-                           Eurydice_slice input3);
+#define libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__squeeze_blocks( \
+  num_blocks, num, xof_state, output, c)                                                                 \
+  libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__squeeze_blocks_f(     \
+    xof_state, num_blocks, (uint8_t*)output[0])
 
-#define libcrux_digest_shake128x4(len, input0, input1, input2, input3, _)      \
-  libcrux_digest_shake128x4f(len, input0, input1, input2, input3)
+void
+libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__absorb_final_(
+  size_t k,
+  libcrux_digest_incremental_x4_Shake128StateX4* x0,
+  Eurydice_slice x1[3U]);

libcrux/include/libcrux_kyber.h

@@ -1,102 +1,124 @@
-/* 
+/*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config
+  ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: a32b316e KaRaMeL version:
+  abb38e1d
  */
 
 #ifndef __libcrux_kyber_H
 #define __libcrux_kyber_H
 
-#include "libcrux_platform.h"
-#include "libcrux_digest.h"
-#include "core.h"
 #include "Eurydice.h"
+#include "core.h"
 #include "eurydice_glue.h"
+#include "libcrux_digest.h"
 
 #define LIBCRUX_KYBER_KYBER768_RANK_768 ((size_t)3U)
 
-#define LIBCRUX_KYBER_KYBER768_RANKED_BYTES_PER_RING_ELEMENT_768 (LIBCRUX_KYBER_KYBER768_RANK_768 * BITS_PER_RING_ELEMENT / (size_t)8U)
+#define LIBCRUX_KYBER_KYBER768_RANKED_BYTES_PER_RING_ELEMENT_768               \
+  (LIBCRUX_KYBER_KYBER768_RANK_768 * BITS_PER_RING_ELEMENT / (size_t)8U)
 
-#define LIBCRUX_KYBER_KYBER768_T_AS_NTT_ENCODED_SIZE_768 (LIBCRUX_KYBER_KYBER768_RANK_768 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT / (size_t)8U)
+#define LIBCRUX_KYBER_KYBER768_T_AS_NTT_ENCODED_SIZE_768                       \
+  (LIBCRUX_KYBER_KYBER768_RANK_768 * COEFFICIENTS_IN_RING_ELEMENT *            \
+   BITS_PER_COEFFICIENT / (size_t)8U)
 
 #define LIBCRUX_KYBER_KYBER768_VECTOR_U_COMPRESSION_FACTOR_768 ((size_t)10U)
 
-#define LIBCRUX_KYBER_KYBER768_C1_BLOCK_SIZE_768 (COEFFICIENTS_IN_RING_ELEMENT * LIBCRUX_KYBER_KYBER768_VECTOR_U_COMPRESSION_FACTOR_768 / (size_t)8U)
+#define LIBCRUX_KYBER_KYBER768_C1_BLOCK_SIZE_768                               \
+  (COEFFICIENTS_IN_RING_ELEMENT *                                              \
+   LIBCRUX_KYBER_KYBER768_VECTOR_U_COMPRESSION_FACTOR_768 / (size_t)8U)
 
-#define LIBCRUX_KYBER_KYBER768_C1_SIZE_768 (LIBCRUX_KYBER_KYBER768_C1_BLOCK_SIZE_768 * LIBCRUX_KYBER_KYBER768_RANK_768)
+#define LIBCRUX_KYBER_KYBER768_C1_SIZE_768                                     \
+  (LIBCRUX_KYBER_KYBER768_C1_BLOCK_SIZE_768 * LIBCRUX_KYBER_KYBER768_RANK_768)
 
 #define LIBCRUX_KYBER_KYBER768_VECTOR_V_COMPRESSION_FACTOR_768 ((size_t)4U)
 
-#define LIBCRUX_KYBER_KYBER768_C2_SIZE_768 (COEFFICIENTS_IN_RING_ELEMENT * LIBCRUX_KYBER_KYBER768_VECTOR_V_COMPRESSION_FACTOR_768 / (size_t)8U)
+#define LIBCRUX_KYBER_KYBER768_C2_SIZE_768                                     \
+  (COEFFICIENTS_IN_RING_ELEMENT *                                              \
+   LIBCRUX_KYBER_KYBER768_VECTOR_V_COMPRESSION_FACTOR_768 / (size_t)8U)
 
-#define LIBCRUX_KYBER_KYBER768_CPA_PKE_SECRET_KEY_SIZE_768 (LIBCRUX_KYBER_KYBER768_RANK_768 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT / (size_t)8U)
+#define LIBCRUX_KYBER_KYBER768_CPA_PKE_SECRET_KEY_SIZE_768                     \
+  (LIBCRUX_KYBER_KYBER768_RANK_768 * COEFFICIENTS_IN_RING_ELEMENT *            \
+   BITS_PER_COEFFICIENT / (size_t)8U)
 
-#define LIBCRUX_KYBER_KYBER768_CPA_PKE_PUBLIC_KEY_SIZE_768 (LIBCRUX_KYBER_KYBER768_T_AS_NTT_ENCODED_SIZE_768 + (size_t)32U)
+#define LIBCRUX_KYBER_KYBER768_CPA_PKE_PUBLIC_KEY_SIZE_768                     \
+  (LIBCRUX_KYBER_KYBER768_T_AS_NTT_ENCODED_SIZE_768 + (size_t)32U)
 
-#define LIBCRUX_KYBER_KYBER768_CPA_PKE_CIPHERTEXT_SIZE_768 (LIBCRUX_KYBER_KYBER768_C1_SIZE_768 + LIBCRUX_KYBER_KYBER768_C2_SIZE_768)
+#define LIBCRUX_KYBER_KYBER768_CPA_PKE_CIPHERTEXT_SIZE_768                     \
+  (LIBCRUX_KYBER_KYBER768_C1_SIZE_768 + LIBCRUX_KYBER_KYBER768_C2_SIZE_768)
 
-#define LIBCRUX_KYBER_KYBER768_SECRET_KEY_SIZE_768 (LIBCRUX_KYBER_KYBER768_CPA_PKE_SECRET_KEY_SIZE_768 + LIBCRUX_KYBER_KYBER768_CPA_PKE_PUBLIC_KEY_SIZE_768 + H_DIGEST_SIZE + SHARED_SECRET_SIZE)
+#define LIBCRUX_KYBER_KYBER768_SECRET_KEY_SIZE_768                             \
+  (LIBCRUX_KYBER_KYBER768_CPA_PKE_SECRET_KEY_SIZE_768 +                        \
+   LIBCRUX_KYBER_KYBER768_CPA_PKE_PUBLIC_KEY_SIZE_768 + H_DIGEST_SIZE +        \
+   SHARED_SECRET_SIZE)
 
 #define LIBCRUX_KYBER_KYBER768_ETA1 ((size_t)2U)
 
-#define LIBCRUX_KYBER_KYBER768_ETA1_RANDOMNESS_SIZE (LIBCRUX_KYBER_KYBER768_ETA1 * (size_t)64U)
+#define LIBCRUX_KYBER_KYBER768_ETA1_RANDOMNESS_SIZE                            \
+  (LIBCRUX_KYBER_KYBER768_ETA1 * (size_t)64U)
 
 #define LIBCRUX_KYBER_KYBER768_ETA2 ((size_t)2U)
 
-#define LIBCRUX_KYBER_KYBER768_ETA2_RANDOMNESS_SIZE (LIBCRUX_KYBER_KYBER768_ETA2 * (size_t)64U)
+#define LIBCRUX_KYBER_KYBER768_ETA2_RANDOMNESS_SIZE                            \
+  (LIBCRUX_KYBER_KYBER768_ETA2 * (size_t)64U)
 
-#define LIBCRUX_KYBER_KYBER768_IMPLICIT_REJECTION_HASH_INPUT_SIZE (SHARED_SECRET_SIZE + LIBCRUX_KYBER_KYBER768_CPA_PKE_CIPHERTEXT_SIZE_768)
+#define LIBCRUX_KYBER_KYBER768_IMPLICIT_REJECTION_HASH_INPUT_SIZE              \
+  (SHARED_SECRET_SIZE + LIBCRUX_KYBER_KYBER768_CPA_PKE_CIPHERTEXT_SIZE_768)
 
 typedef uint8_t libcrux_kyber_types_MlKemPublicKey___1184size_t[1184U];
 
-typedef struct core_option_Option__libcrux_kyber_types_MlKemPublicKey__1184size_t___s
+typedef struct
+  core_option_Option__libcrux_kyber_types_MlKemPublicKey__1184size_t___s
 {
   core_option_Option__size_t_tags tag;
   libcrux_kyber_types_MlKemPublicKey___1184size_t f0;
-}
-core_option_Option__libcrux_kyber_types_MlKemPublicKey__1184size_t__;
+} core_option_Option__libcrux_kyber_types_MlKemPublicKey__1184size_t__;
 
 core_option_Option__libcrux_kyber_types_MlKemPublicKey__1184size_t__
 libcrux_kyber_kyber768_validate_public_key(uint8_t public_key[1184U]);
 
-typedef struct
-K___uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__s
-{
-  uint8_t fst[840U];
-  uint8_t snd[840U];
-  uint8_t thd[840U];
-  uint8_t f3[840U];
-}
-K___uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_;
-
 typedef struct libcrux_kyber_types_MlKemKeyPair___2400size_t_1184size_t_s
 {
   uint8_t sk[2400U];
   uint8_t pk[1184U];
-}
-libcrux_kyber_types_MlKemKeyPair___2400size_t_1184size_t;
+} libcrux_kyber_types_MlKemKeyPair___2400size_t_1184size_t;
 
 libcrux_kyber_types_MlKemKeyPair___2400size_t_1184size_t
 libcrux_kyber_kyber768_generate_key_pair(uint8_t randomness[64U]);
 
-typedef struct K___libcrux_kyber_types_MlKemCiphertext__1088size_t___uint8_t_32size_t__s
+typedef struct
+  K___libcrux_kyber_types_MlKemCiphertext__1088size_t___uint8_t_32size_t__s
 {
   uint8_t fst[1088U];
   uint8_t snd[32U];
-}
-K___libcrux_kyber_types_MlKemCiphertext__1088size_t___uint8_t_32size_t_;
+} K___libcrux_kyber_types_MlKemCiphertext__1088size_t___uint8_t_32size_t_;
 
 K___libcrux_kyber_types_MlKemCiphertext__1088size_t___uint8_t_32size_t_
-libcrux_kyber_kyber768_encapsulate(uint8_t (*public_key)[1184U], uint8_t randomness[32U]);
-
-void
-libcrux_kyber_kyber768_decapsulate(
-  uint8_t (*secret_key)[2400U],
-  uint8_t (*ciphertext)[1088U],
-  uint8_t ret[32U]
-);
-
+  libcrux_kyber_kyber768_encapsulate(uint8_t (*public_key)[1184U],
+                                     uint8_t randomness[32U]);
+
+void libcrux_kyber_kyber768_decapsulate(uint8_t (*secret_key)[2400U],
+                                        uint8_t (*ciphertext)[1088U],
+                                        uint8_t ret[32U]);
+
+extern libcrux_digest_incremental_x4_Shake128StateX4
+libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__new(
+  void);
+
+#define libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__absorb_final( \
+  x_0, x_1, x_2, _ret_t)                                                                               \
+  libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__absorb_final_(      \
+    x_0, x_1, x_2)
+
+extern void
+libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__absorb_final_(
+  size_t x0,
+  libcrux_digest_incremental_x4_Shake128StateX4* x1,
+  Eurydice_slice x2[3U]);
+
+extern void
+libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__free_memory(
+  libcrux_digest_incremental_x4_Shake128StateX4 x0);
 
 #define __libcrux_kyber_H_DEFINED
 #endif

libcrux/include/libcrux_platform.h

@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: eurydice ../libcrux_kyber.llbc --config config.yaml
-  F* version: 58c915a8
-  KaRaMeL version: 56c5c145
+  KaRaMeL invocation: /Users/bhargava/Desktop/repositories/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
+  F* version: a32b316e
+  KaRaMeL version: 08bfa78a
  */
 
 #ifndef __libcrux_platform_H