Merge pull request #623 from cryspen/franziskus/mlkem-serialize-sk

[ML-KEM] serialize sk

.docker/c/ext-tools.sh

@@ -16,11 +16,11 @@ unzip karamel.zip
 rm -rf karamel.zip
 mv karamel-8c3612018c25889288da6857771be3ad03b75bcd/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c/ eurydice
+mv eurydice-e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20/ eurydice
 
 echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile

libcrux-ml-kem/c/benches/mlkem768.cc

@@ -14,7 +14,7 @@
 
 void generate_random(uint8_t *output, uint32_t output_len)
 {
-  for (int i = 0; i < output_len; i++)
+  for (uint32_t i = 0; i < output_len; i++)
     output[i] = 13;
 }
 

libcrux-ml-kem/c/benches/mlkem768_encaps.cc

@@ -14,7 +14,7 @@
 
 void generate_random(uint8_t *output, uint32_t output_len)
 {
-    for (int i = 0; i < output_len; i++)
+    for (uint32_t i = 0; i < output_len; i++)
         output[i] = 13;
 }
 

libcrux-ml-kem/c/benches/mlkem768_keygen.cc

@@ -14,7 +14,7 @@
 
 void generate_random(uint8_t *output, uint32_t output_len)
 {
-    for (int i = 0; i < output_len; i++)
+    for (uint32_t i = 0; i < output_len; i++)
         output[i] = 13;
 }
 

libcrux-ml-kem/c/code_gen.txt

@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
 Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
-Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
+Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
 Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
 F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
-Libcrux: a31e411ce57494f7a7e8c5962c9951a52a62c770
+Libcrux: 122ee3d193e33f55c2324ee84f974e647255f545

libcrux-ml-kem/c/internal/libcrux_core.h

@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: a31e411ce57494f7a7e8c5962c9951a52a62c770
+ * Libcrux: 122ee3d193e33f55c2324ee84f974e647255f545
  */
 
 #ifndef __internal_libcrux_core_H
@@ -60,18 +60,6 @@ typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair768_s {
   uint8_t snd[1184U];
 } libcrux_ml_kem_utils_extraction_helper_Keypair768;
 
-/**
-This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
-libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
-*/
-/**
-A monomorphic instance of libcrux_ml_kem.types.from_40
-with const generics
-- SIZE= 1568
-*/
-libcrux_ml_kem_types_MlKemPublicKey_64 libcrux_ml_kem_types_from_40_af(
-    uint8_t value[1568U]);
-
 /**
  Create a new [`MlKemKeyPair`] from the secret and public key.
 */
@@ -101,18 +89,6 @@ with const generics
 libcrux_ml_kem_types_MlKemPrivateKey_83 libcrux_ml_kem_types_from_88_39(
     uint8_t value[3168U]);
 
-/**
-This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
-libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
-*/
-/**
-A monomorphic instance of libcrux_ml_kem.types.from_40
-with const generics
-- SIZE= 1184
-*/
-libcrux_ml_kem_types_MlKemPublicKey_30 libcrux_ml_kem_types_from_40_d0(
-    uint8_t value[1184U]);
-
 /**
  Create a new [`MlKemKeyPair`] from the secret and public key.
 */
@@ -142,18 +118,6 @@ with const generics
 libcrux_ml_kem_types_MlKemPrivateKey_d9 libcrux_ml_kem_types_from_88_28(
     uint8_t value[2400U]);
 
-/**
-This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
-libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
-*/
-/**
-A monomorphic instance of libcrux_ml_kem.types.from_40
-with const generics
-- SIZE= 800
-*/
-libcrux_ml_kem_types_MlKemPublicKey_52 libcrux_ml_kem_types_from_40_4d(
-    uint8_t value[800U]);
-
 /**
  Create a new [`MlKemKeyPair`] from the secret and public key.
 */
@@ -197,6 +161,39 @@ with const generics
 uint8_t *libcrux_ml_kem_types_as_slice_ba_d0(
     libcrux_ml_kem_types_MlKemPublicKey_30 *self);
 
+/**
+This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
+libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.types.from_40
+with const generics
+- SIZE= 1184
+*/
+libcrux_ml_kem_types_MlKemPublicKey_30 libcrux_ml_kem_types_from_40_d0(
+    uint8_t value[1184U]);
+
+typedef struct Eurydice_slice_uint8_t_x4_s {
+  Eurydice_slice fst;
+  Eurydice_slice snd;
+  Eurydice_slice thd;
+  Eurydice_slice f3;
+} Eurydice_slice_uint8_t_x4;
+
+/**
+ Unpack an incoming private key into it's different parts.
+
+ We have this here in types to extract into a common core for C.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.types.unpack_private_key
+with const generics
+- CPA_SECRET_KEY_SIZE= 1152
+- PUBLIC_KEY_SIZE= 1184
+*/
+Eurydice_slice_uint8_t_x4 libcrux_ml_kem_types_unpack_private_key_b4(
+    Eurydice_slice private_key);
+
 /**
 This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
 libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#3}
@@ -246,6 +243,32 @@ with const generics
 uint8_t *libcrux_ml_kem_types_as_slice_ba_4d(
     libcrux_ml_kem_types_MlKemPublicKey_52 *self);
 
+/**
+This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
+libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.types.from_40
+with const generics
+- SIZE= 800
+*/
+libcrux_ml_kem_types_MlKemPublicKey_52 libcrux_ml_kem_types_from_40_4d(
+    uint8_t value[800U]);
+
+/**
+ Unpack an incoming private key into it's different parts.
+
+ We have this here in types to extract into a common core for C.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.types.unpack_private_key
+with const generics
+- CPA_SECRET_KEY_SIZE= 768
+- PUBLIC_KEY_SIZE= 800
+*/
+Eurydice_slice_uint8_t_x4 libcrux_ml_kem_types_unpack_private_key_0c(
+    Eurydice_slice private_key);
+
 /**
 This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
 libcrux_ml_kem::types::MlKemCiphertext<SIZE>)#3}
@@ -295,6 +318,32 @@ with const generics
 uint8_t *libcrux_ml_kem_types_as_slice_ba_af(
     libcrux_ml_kem_types_MlKemPublicKey_64 *self);
 
+/**
+This function found in impl {(core::convert::From<@Array<u8, SIZE>> for
+libcrux_ml_kem::types::MlKemPublicKey<SIZE>)#17}
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.types.from_40
+with const generics
+- SIZE= 1568
+*/
+libcrux_ml_kem_types_MlKemPublicKey_64 libcrux_ml_kem_types_from_40_af(
+    uint8_t value[1568U]);
+
+/**
+ Unpack an incoming private key into it's different parts.
+
+ We have this here in types to extract into a common core for C.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.types.unpack_private_key
+with const generics
+- CPA_SECRET_KEY_SIZE= 1536
+- PUBLIC_KEY_SIZE= 1568
+*/
+Eurydice_slice_uint8_t_x4 libcrux_ml_kem_types_unpack_private_key_1f(
+    Eurydice_slice private_key);
+
 /**
 A monomorphic instance of core.result.Result
 with types uint8_t[32size_t], core_array_TryFromSliceError

libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h

@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: a31e411ce57494f7a7e8c5962c9951a52a62c770
+ * Libcrux: 122ee3d193e33f55c2324ee84f974e647255f545
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H
@@ -50,6 +50,21 @@ with const generics
 */
 bool libcrux_ml_kem_ind_cca_validate_public_key_ed(uint8_t *public_key);
 
+/**
+ Validate an ML-KEM private key.
+
+ This implements the Hash check in 7.3 3.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.ind_cca.validate_private_key_only
+with types libcrux_ml_kem_hash_functions_avx2_Simd256Hash
+with const generics
+- K= 3
+- SECRET_KEY_SIZE= 2400
+*/
+bool libcrux_ml_kem_ind_cca_validate_private_key_only_ae(
+    libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key);
+
 /**
  Validate an ML-KEM private key.
 
@@ -159,6 +174,21 @@ with const generics
 */
 bool libcrux_ml_kem_ind_cca_validate_public_key_1e(uint8_t *public_key);
 
+/**
+ Validate an ML-KEM private key.
+
+ This implements the Hash check in 7.3 3.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.ind_cca.validate_private_key_only
+with types libcrux_ml_kem_hash_functions_avx2_Simd256Hash
+with const generics
+- K= 4
+- SECRET_KEY_SIZE= 3168
+*/
+bool libcrux_ml_kem_ind_cca_validate_private_key_only_5e(
+    libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key);
+
 /**
  Validate an ML-KEM private key.
 
@@ -268,6 +298,21 @@ with const generics
 */
 bool libcrux_ml_kem_ind_cca_validate_public_key_ba(uint8_t *public_key);
 
+/**
+ Validate an ML-KEM private key.
+
+ This implements the Hash check in 7.3 3.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.ind_cca.validate_private_key_only
+with types libcrux_ml_kem_hash_functions_avx2_Simd256Hash
+with const generics
+- K= 2
+- SECRET_KEY_SIZE= 1632
+*/
+bool libcrux_ml_kem_ind_cca_validate_private_key_only_4d(
+    libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key);
+
 /**
  Validate an ML-KEM private key.
 

libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h

@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: a31e411ce57494f7a7e8c5962c9951a52a62c770
+ * Libcrux: 122ee3d193e33f55c2324ee84f974e647255f545
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H
@@ -55,6 +55,21 @@ with const generics
 */
 bool libcrux_ml_kem_ind_cca_validate_public_key_00(uint8_t *public_key);
 
+/**
+ Validate an ML-KEM private key.
+
+ This implements the Hash check in 7.3 3.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.ind_cca.validate_private_key_only
+with types libcrux_ml_kem_hash_functions_portable_PortableHash[[$4size_t]]
+with const generics
+- K= 4
+- SECRET_KEY_SIZE= 3168
+*/
+bool libcrux_ml_kem_ind_cca_validate_private_key_only_60(
+    libcrux_ml_kem_types_MlKemPrivateKey_83 *private_key);
+
 /**
  Validate an ML-KEM private key.
 
@@ -164,6 +179,21 @@ with const generics
 */
 bool libcrux_ml_kem_ind_cca_validate_public_key_86(uint8_t *public_key);
 
+/**
+ Validate an ML-KEM private key.
+
+ This implements the Hash check in 7.3 3.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.ind_cca.validate_private_key_only
+with types libcrux_ml_kem_hash_functions_portable_PortableHash[[$2size_t]]
+with const generics
+- K= 2
+- SECRET_KEY_SIZE= 1632
+*/
+bool libcrux_ml_kem_ind_cca_validate_private_key_only_30(
+    libcrux_ml_kem_types_MlKemPrivateKey_fa *private_key);
+
 /**
  Validate an ML-KEM private key.
 
@@ -273,6 +303,21 @@ with const generics
 */
 bool libcrux_ml_kem_ind_cca_validate_public_key_6c(uint8_t *public_key);
 
+/**
+ Validate an ML-KEM private key.
+
+ This implements the Hash check in 7.3 3.
+*/
+/**
+A monomorphic instance of libcrux_ml_kem.ind_cca.validate_private_key_only
+with types libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]]
+with const generics
+- K= 3
+- SECRET_KEY_SIZE= 2400
+*/
+bool libcrux_ml_kem_ind_cca_validate_private_key_only_d6(
+    libcrux_ml_kem_types_MlKemPrivateKey_d9 *private_key);
+
 /**
  Validate an ML-KEM private key.
 

libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h

@@ -5,10 +5,10 @@
  *
  * This code was generated with the following revisions:
  * Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
- * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
+ * Eurydice: 7d686376ec943225ff89942978c6c3028bac689c
  * Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: a31e411ce57494f7a7e8c5962c9951a52a62c770
+ * Libcrux: 122ee3d193e33f55c2324ee84f974e647255f545
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H