update C extraction

cryspen · Sep 27, 2024 · 3c8b7f8 · 3c8b7f8
1 parent 49c0771
commit 3c8b7f8
Show file tree

Hide file tree

Showing 42 changed files with 1,805 additions and 1,703 deletions.
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -3,4 +3,4 @@ Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
 Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
 Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
 F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
-Libcrux: 97f7cefe14dabf275e4671ffea87e032d7779b71
+Libcrux: 49c07712f755745796ce294c5267a1945b9e9b6b
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -8,7 +8,7 @@
  * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
  * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 97f7cefe14dabf275e4671ffea87e032d7779b71
+ * Libcrux: 49c07712f755745796ce294c5267a1945b9e9b6b
  */
 
 #ifndef __internal_libcrux_core_H
@@ -69,7 +69,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_40
 with const generics
 - SIZE= 1568
 */
-libcrux_ml_kem_types_MlKemPublicKey_1f libcrux_ml_kem_types_from_40_601(
+libcrux_ml_kem_types_MlKemPublicKey_1f libcrux_ml_kem_types_from_40_cb1(
  uint8_t value[1568U]);
 
 /**
@@ -85,7 +85,7 @@ with const generics
 - PRIVATE_KEY_SIZE= 3168
 - PUBLIC_KEY_SIZE= 1568
 */
-libcrux_ml_kem_mlkem1024_MlKem1024KeyPair libcrux_ml_kem_types_from_17_8b1(
+libcrux_ml_kem_mlkem1024_MlKem1024KeyPair libcrux_ml_kem_types_from_17_dc1(
  libcrux_ml_kem_types_MlKemPrivateKey_95 sk,
  libcrux_ml_kem_types_MlKemPublicKey_1f pk);
 
@@ -98,7 +98,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_88
 with const generics
 - SIZE= 3168
 */
-libcrux_ml_kem_types_MlKemPrivateKey_95 libcrux_ml_kem_types_from_88_2d1(
+libcrux_ml_kem_types_MlKemPrivateKey_95 libcrux_ml_kem_types_from_88_581(
  uint8_t value[3168U]);
 
 /**
@@ -110,7 +110,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_40
 with const generics
 - SIZE= 1184
 */
-libcrux_ml_kem_types_MlKemPublicKey_15 libcrux_ml_kem_types_from_40_600(
+libcrux_ml_kem_types_MlKemPublicKey_15 libcrux_ml_kem_types_from_40_cb0(
  uint8_t value[1184U]);
 
 /**
@@ -126,7 +126,7 @@ with const generics
 - PRIVATE_KEY_SIZE= 2400
 - PUBLIC_KEY_SIZE= 1184
 */
-libcrux_ml_kem_mlkem768_MlKem768KeyPair libcrux_ml_kem_types_from_17_8b0(
+libcrux_ml_kem_mlkem768_MlKem768KeyPair libcrux_ml_kem_types_from_17_dc0(
  libcrux_ml_kem_types_MlKemPrivateKey_55 sk,
  libcrux_ml_kem_types_MlKemPublicKey_15 pk);
 
@@ -139,7 +139,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_88
 with const generics
 - SIZE= 2400
 */
-libcrux_ml_kem_types_MlKemPrivateKey_55 libcrux_ml_kem_types_from_88_2d0(
+libcrux_ml_kem_types_MlKemPrivateKey_55 libcrux_ml_kem_types_from_88_580(
  uint8_t value[2400U]);
 
 /**
@@ -151,7 +151,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_40
 with const generics
 - SIZE= 800
 */
-libcrux_ml_kem_types_MlKemPublicKey_be libcrux_ml_kem_types_from_40_60(
+libcrux_ml_kem_types_MlKemPublicKey_be libcrux_ml_kem_types_from_40_cb(
  uint8_t value[800U]);
 
 /**
@@ -167,7 +167,7 @@ with const generics
 - PRIVATE_KEY_SIZE= 1632
 - PUBLIC_KEY_SIZE= 800
 */
-libcrux_ml_kem_types_MlKemKeyPair_cb libcrux_ml_kem_types_from_17_8b(
+libcrux_ml_kem_types_MlKemKeyPair_cb libcrux_ml_kem_types_from_17_dc(
  libcrux_ml_kem_types_MlKemPrivateKey_5e sk,
  libcrux_ml_kem_types_MlKemPublicKey_be pk);
 
@@ -180,7 +180,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_88
 with const generics
 - SIZE= 1632
 */
-libcrux_ml_kem_types_MlKemPrivateKey_5e libcrux_ml_kem_types_from_88_2d(
+libcrux_ml_kem_types_MlKemPrivateKey_5e libcrux_ml_kem_types_from_88_58(
  uint8_t value[1632U]);
 
 /**
@@ -194,7 +194,7 @@ A monomorphic instance of libcrux_ml_kem.types.as_slice_ba
 with const generics
 - SIZE= 1184
 */
-uint8_t *libcrux_ml_kem_types_as_slice_ba_121(
+uint8_t *libcrux_ml_kem_types_as_slice_ba_661(
  libcrux_ml_kem_types_MlKemPublicKey_15 *self);
 
 /**
@@ -206,7 +206,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_fc
 with const generics
 - SIZE= 1088
 */
-libcrux_ml_kem_mlkem768_MlKem768Ciphertext libcrux_ml_kem_types_from_fc_361(
+libcrux_ml_kem_mlkem768_MlKem768Ciphertext libcrux_ml_kem_types_from_fc_0e1(
  uint8_t value[1088U]);
 
 /**
@@ -218,7 +218,7 @@ A monomorphic instance of libcrux_ml_kem.types.as_ref_fd
 with const generics
 - SIZE= 1088
 */
-Eurydice_slice libcrux_ml_kem_types_as_ref_fd_ed1(
+Eurydice_slice libcrux_ml_kem_types_as_ref_fd_f71(
  libcrux_ml_kem_mlkem768_MlKem768Ciphertext *self);
 
 /**
@@ -243,7 +243,7 @@ A monomorphic instance of libcrux_ml_kem.types.as_slice_ba
 with const generics
 - SIZE= 800
 */
-uint8_t *libcrux_ml_kem_types_as_slice_ba_120(
+uint8_t *libcrux_ml_kem_types_as_slice_ba_660(
  libcrux_ml_kem_types_MlKemPublicKey_be *self);
 
 /**
@@ -255,7 +255,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_fc
 with const generics
 - SIZE= 768
 */
-libcrux_ml_kem_types_MlKemCiphertext_e8 libcrux_ml_kem_types_from_fc_360(
+libcrux_ml_kem_types_MlKemCiphertext_e8 libcrux_ml_kem_types_from_fc_0e0(
  uint8_t value[768U]);
 
 /**
@@ -267,7 +267,7 @@ A monomorphic instance of libcrux_ml_kem.types.as_ref_fd
 with const generics
 - SIZE= 768
 */
-Eurydice_slice libcrux_ml_kem_types_as_ref_fd_ed0(
+Eurydice_slice libcrux_ml_kem_types_as_ref_fd_f70(
  libcrux_ml_kem_types_MlKemCiphertext_e8 *self);
 
 /**
@@ -292,7 +292,7 @@ A monomorphic instance of libcrux_ml_kem.types.as_slice_ba
 with const generics
 - SIZE= 1568
 */
-uint8_t *libcrux_ml_kem_types_as_slice_ba_12(
+uint8_t *libcrux_ml_kem_types_as_slice_ba_66(
  libcrux_ml_kem_types_MlKemPublicKey_1f *self);
 
 /**
@@ -339,7 +339,7 @@ A monomorphic instance of libcrux_ml_kem.types.from_fc
 with const generics
 - SIZE= 1568
 */
-libcrux_ml_kem_types_MlKemCiphertext_1f libcrux_ml_kem_types_from_fc_36(
+libcrux_ml_kem_types_MlKemCiphertext_1f libcrux_ml_kem_types_from_fc_0e(
  uint8_t value[1568U]);
 
 /**
@@ -362,7 +362,7 @@ A monomorphic instance of libcrux_ml_kem.types.as_ref_fd
 with const generics
 - SIZE= 1568
 */
-Eurydice_slice libcrux_ml_kem_types_as_ref_fd_ed(
+Eurydice_slice libcrux_ml_kem_types_as_ref_fd_f7(
  libcrux_ml_kem_types_MlKemCiphertext_1f *self);
 
 /**

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
@@ -8,7 +8,7 @@
  * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
  * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
  * F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
- * Libcrux: 97f7cefe14dabf275e4671ffea87e032d7779b71
+ * Libcrux: 49c07712f755745796ce294c5267a1945b9e9b6b
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H
@@ -48,7 +48,7 @@ with const generics
 - RANKED_BYTES_PER_RING_ELEMENT= 1152
 - PUBLIC_KEY_SIZE= 1184
 */
-bool libcrux_ml_kem_ind_cca_validate_public_key_051(uint8_t *public_key);
+bool libcrux_ml_kem_ind_cca_validate_public_key_fc1(uint8_t *public_key);
 
 /**
  Validate an ML-KEM private key.
@@ -65,7 +65,7 @@ with const generics
 - SECRET_KEY_SIZE= 2400
 - CIPHERTEXT_SIZE= 1088
 */
-bool libcrux_ml_kem_ind_cca_validate_private_key_4d1(
+bool libcrux_ml_kem_ind_cca_validate_private_key_2e1(
  libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key,
  libcrux_ml_kem_mlkem768_MlKem768Ciphertext *_ciphertext);
 
@@ -91,7 +91,7 @@ with const generics
 - ETA1_RANDOMNESS_SIZE= 128
 */
 libcrux_ml_kem_mlkem768_MlKem768KeyPair
-libcrux_ml_kem_ind_cca_generate_keypair_511(uint8_t randomness[64U]);
+libcrux_ml_kem_ind_cca_generate_keypair_cb1(uint8_t randomness[64U]);
 
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.encapsulate
@@ -112,7 +112,7 @@ with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-tuple_3c libcrux_ml_kem_ind_cca_encapsulate_9c1(
+tuple_3c libcrux_ml_kem_ind_cca_encapsulate_271(
  libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,
  uint8_t randomness[32U]);
 
@@ -138,7 +138,7 @@ with const generics
 - ETA2_RANDOMNESS_SIZE= 128
 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1120
 */
-void libcrux_ml_kem_ind_cca_decapsulate_971(
+void libcrux_ml_kem_ind_cca_decapsulate_061(
  libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key,
  libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]);
 
@@ -157,7 +157,7 @@ with const generics
 - RANKED_BYTES_PER_RING_ELEMENT= 1536
 - PUBLIC_KEY_SIZE= 1568
 */
-bool libcrux_ml_kem_ind_cca_validate_public_key_050(uint8_t *public_key);
+bool libcrux_ml_kem_ind_cca_validate_public_key_fc0(uint8_t *public_key);
 
 /**
  Validate an ML-KEM private key.
@@ -174,7 +174,7 @@ with const generics
 - SECRET_KEY_SIZE= 3168
 - CIPHERTEXT_SIZE= 1568
 */
-bool libcrux_ml_kem_ind_cca_validate_private_key_4d0(
+bool libcrux_ml_kem_ind_cca_validate_private_key_2e0(
  libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key,
  libcrux_ml_kem_types_MlKemCiphertext_1f *_ciphertext);
 
@@ -200,7 +200,7 @@ with const generics
 - ETA1_RANDOMNESS_SIZE= 128
 */
 libcrux_ml_kem_mlkem1024_MlKem1024KeyPair
-libcrux_ml_kem_ind_cca_generate_keypair_510(uint8_t randomness[64U]);
+libcrux_ml_kem_ind_cca_generate_keypair_cb0(uint8_t randomness[64U]);
 
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.encapsulate
@@ -221,7 +221,7 @@ with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-tuple_21 libcrux_ml_kem_ind_cca_encapsulate_9c0(
+tuple_21 libcrux_ml_kem_ind_cca_encapsulate_270(
  libcrux_ml_kem_types_MlKemPublicKey_1f *public_key,
  uint8_t randomness[32U]);
 
@@ -247,7 +247,7 @@ with const generics
 - ETA2_RANDOMNESS_SIZE= 128
 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1600
 */
-void libcrux_ml_kem_ind_cca_decapsulate_970(
+void libcrux_ml_kem_ind_cca_decapsulate_060(
  libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key,
  libcrux_ml_kem_types_MlKemCiphertext_1f *ciphertext, uint8_t ret[32U]);
 
@@ -266,7 +266,7 @@ with const generics
 - RANKED_BYTES_PER_RING_ELEMENT= 768
 - PUBLIC_KEY_SIZE= 800
 */
-bool libcrux_ml_kem_ind_cca_validate_public_key_05(uint8_t *public_key);
+bool libcrux_ml_kem_ind_cca_validate_public_key_fc(uint8_t *public_key);
 
 /**
  Validate an ML-KEM private key.
@@ -283,7 +283,7 @@ with const generics
 - SECRET_KEY_SIZE= 1632
 - CIPHERTEXT_SIZE= 768
 */
-bool libcrux_ml_kem_ind_cca_validate_private_key_4d(
+bool libcrux_ml_kem_ind_cca_validate_private_key_2e(
  libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key,
  libcrux_ml_kem_types_MlKemCiphertext_e8 *_ciphertext);
 
@@ -308,7 +308,7 @@ with const generics
 - ETA1= 3
 - ETA1_RANDOMNESS_SIZE= 192
 */
-libcrux_ml_kem_types_MlKemKeyPair_cb libcrux_ml_kem_ind_cca_generate_keypair_51(
+libcrux_ml_kem_types_MlKemKeyPair_cb libcrux_ml_kem_ind_cca_generate_keypair_cb(
  uint8_t randomness[64U]);
 
 /**
@@ -330,7 +330,7 @@ with const generics
 - ETA2= 2
 - ETA2_RANDOMNESS_SIZE= 128
 */
-tuple_ec libcrux_ml_kem_ind_cca_encapsulate_9c(
+tuple_ec libcrux_ml_kem_ind_cca_encapsulate_27(
  libcrux_ml_kem_types_MlKemPublicKey_be *public_key,
  uint8_t randomness[32U]);
 
@@ -356,7 +356,7 @@ with const generics
 - ETA2_RANDOMNESS_SIZE= 128
 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 800
 */
-void libcrux_ml_kem_ind_cca_decapsulate_97(
+void libcrux_ml_kem_ind_cca_decapsulate_06(
  libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key,
  libcrux_ml_kem_types_MlKemCiphertext_e8 *ciphertext, uint8_t ret[32U]);