Merge pull request #652 from cryspen/dev-ind-cca-unpacked

Proofs for Ind-cca unpacked functions

libcrux-ml-kem/cg/code_gen.txt

@@ -3,4 +3,4 @@ Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f
 Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
 Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
 F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
-Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
+Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d

libcrux-ml-kem/cg/libcrux_core.h

@@ -8,7 +8,7 @@
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
  * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
  * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
- * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
+ * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
  */
 
 #ifndef __libcrux_core_H

libcrux-ml-kem/cg/libcrux_ct_ops.h

@@ -8,7 +8,7 @@
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
  * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
  * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
- * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
+ * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
  */
 
 #ifndef __libcrux_ct_ops_H

libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h

@@ -8,7 +8,7 @@
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
  * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
  * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
- * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
+ * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
  */
 
 #ifndef __libcrux_mlkem768_avx2_H
@@ -7030,40 +7030,24 @@ static inline tuple_c2 libcrux_ml_kem_mlkem768_avx2_unpacked_encapsulate(
 
 /**
 A monomorphic instance of
-libcrux_ml_kem.ind_cca.unpacked.generate_keypair.closure.closure with types
-libcrux_ml_kem_vector_avx2_SIMD256Vector,
-libcrux_ml_kem_hash_functions_avx2_Simd256Hash, libcrux_ml_kem_variant_MlKem
-with const generics
+libcrux_ml_kem.ind_cca.unpacked.transpose_a.closure.closure with types
+libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
 - K= 3
-- CPA_PRIVATE_KEY_SIZE= 1152
-- PRIVATE_KEY_SIZE= 2400
-- PUBLIC_KEY_SIZE= 1184
-- BYTES_PER_RING_ELEMENT= 1152
-- ETA1= 2
-- ETA1_RANDOMNESS_SIZE= 128
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static inline libcrux_ml_kem_polynomial_PolynomialRingElement_f6
-libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_closure_d6(size_t _j) {
+libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_closure_ab(size_t _j) {
   return libcrux_ml_kem_polynomial_ZERO_ef_61();
 }
 
 /**
-A monomorphic instance of
-libcrux_ml_kem.ind_cca.unpacked.generate_keypair.closure with types
-libcrux_ml_kem_vector_avx2_SIMD256Vector,
-libcrux_ml_kem_hash_functions_avx2_Simd256Hash, libcrux_ml_kem_variant_MlKem
+A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.closure
+with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 - K= 3
-- CPA_PRIVATE_KEY_SIZE= 1152
-- PRIVATE_KEY_SIZE= 2400
-- PUBLIC_KEY_SIZE= 1184
-- BYTES_PER_RING_ELEMENT= 1152
-- ETA1= 2
-- ETA1_RANDOMNESS_SIZE= 128
 */
 KRML_ATTRIBUTE_TARGET("avx2")
-static inline void libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_d6(
+static inline void libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_ab(
     size_t _i, libcrux_ml_kem_polynomial_PolynomialRingElement_f6 ret[3U]) {
   for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
     ret[i] = libcrux_ml_kem_polynomial_ZERO_ef_61();
@@ -7094,8 +7078,37 @@ libcrux_ml_kem_polynomial_clone_8d_61(
 }
 
 /**
- Generate Unpacked Keys
+A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a
+with types libcrux_ml_kem_vector_avx2_SIMD256Vector
+with const generics
+- K= 3
 */
+KRML_ATTRIBUTE_TARGET("avx2")
+static inline void libcrux_ml_kem_ind_cca_unpacked_transpose_a_ab(
+    libcrux_ml_kem_polynomial_PolynomialRingElement_f6 ind_cpa_a[3U][3U],
+    libcrux_ml_kem_polynomial_PolynomialRingElement_f6 ret[3U][3U]) {
+  libcrux_ml_kem_polynomial_PolynomialRingElement_f6 A[3U][3U];
+  for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
+    libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_ab(i, A[i]);
+  }
+  for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
+    size_t i0 = i;
+    libcrux_ml_kem_polynomial_PolynomialRingElement_f6 _a_i[3U][3U];
+    memcpy(_a_i, A,
+           (size_t)3U *
+               sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f6[3U]));
+    for (size_t i1 = (size_t)0U; i1 < (size_t)3U; i1++) {
+      size_t j = i1;
+      libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____0 =
+          libcrux_ml_kem_polynomial_clone_8d_61(&ind_cpa_a[j][i0]);
+      A[i0][j] = uu____0;
+    }
+  }
+  memcpy(ret, A,
+         (size_t)3U *
+             sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f6[3U]));
+}
+
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.generate_keypair
 with types libcrux_ml_kem_vector_avx2_SIMD256Vector,
@@ -7123,20 +7136,12 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_unpacked_generate_keypair_d6(
   libcrux_ml_kem_ind_cpa_generate_keypair_unpacked_22(
       ind_cpa_keypair_randomness, &out->private_key.ind_cpa_private_key,
       &out->public_key.ind_cpa_public_key);
+  libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____0[3U][3U];
+  memcpy(uu____0, out->public_key.ind_cpa_public_key.A,
+         (size_t)3U *
+             sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f6[3U]));
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 A[3U][3U];
-  for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
-    libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_d6(i, A[i]);
-  }
-  for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++) {
-    size_t i1 = i0;
-    for (size_t i = (size_t)0U; i < (size_t)3U; i++) {
-      size_t j = i;
-      libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____0 =
-          libcrux_ml_kem_polynomial_clone_8d_61(
-              &out->public_key.ind_cpa_public_key.A[j][i1]);
-      A[i1][j] = uu____0;
-    }
-  }
+  libcrux_ml_kem_ind_cca_unpacked_transpose_a_ab(uu____0, A);
   libcrux_ml_kem_polynomial_PolynomialRingElement_f6 uu____1[3U][3U];
   memcpy(uu____1, A,
          (size_t)3U *
@@ -7231,17 +7236,17 @@ static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_generate_key_pair(
 /**
 This function found in impl {(core::default::Default for
 libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked<Vector,
-K>[TraitClause@0, TraitClause@1])#1}
+K>[TraitClause@0, TraitClause@1])}
 */
 /**
-A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_1c
+A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_09
 with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 - K= 3
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63
-libcrux_ml_kem_ind_cca_unpacked_default_1c_ab(void) {
+libcrux_ml_kem_ind_cca_unpacked_default_09_ab(void) {
   libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 lit;
   lit.ind_cpa_public_key = libcrux_ml_kem_ind_cpa_unpacked_default_8d_ab();
   lit.public_key_hash[0U] = 0U;
@@ -7282,18 +7287,18 @@ libcrux_ml_kem_ind_cca_unpacked_default_1c_ab(void) {
 /**
 This function found in impl {(core::default::Default for
 libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked<Vector,
-K>[TraitClause@0, TraitClause@1])#3}
+K>[TraitClause@0, TraitClause@1])#1}
 */
 /**
-A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_07
+A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.default_53
 with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 - K= 3
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static KRML_MUSTINLINE
     libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked
-    libcrux_ml_kem_ind_cca_unpacked_default_07_ab(void) {
+    libcrux_ml_kem_ind_cca_unpacked_default_53_ab(void) {
   libcrux_ml_kem_ind_cca_unpacked_MlKemPrivateKeyUnpacked_63 uu____0;
   uu____0.ind_cpa_private_key = libcrux_ml_kem_ind_cpa_unpacked_default_1a_ab();
   uu____0.implicit_rejection_value[0U] = 0U;
@@ -7331,7 +7336,7 @@ static KRML_MUSTINLINE
   return (
       CLITERAL(libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked){
           .private_key = uu____0,
-          .public_key = libcrux_ml_kem_ind_cca_unpacked_default_1c_ab()});
+          .public_key = libcrux_ml_kem_ind_cca_unpacked_default_09_ab()});
 }
 
 /**
@@ -7340,7 +7345,7 @@ static KRML_MUSTINLINE
 KRML_ATTRIBUTE_TARGET("avx2")
 static inline libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked
 libcrux_ml_kem_mlkem768_avx2_unpacked_init_key_pair(void) {
-  return libcrux_ml_kem_ind_cca_unpacked_default_07_ab();
+  return libcrux_ml_kem_ind_cca_unpacked_default_53_ab();
 }
 
 /**
@@ -7349,28 +7354,25 @@ libcrux_ml_kem_mlkem768_avx2_unpacked_init_key_pair(void) {
 KRML_ATTRIBUTE_TARGET("avx2")
 static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63
 libcrux_ml_kem_mlkem768_avx2_unpacked_init_public_key(void) {
-  return libcrux_ml_kem_ind_cca_unpacked_default_1c_ab();
+  return libcrux_ml_kem_ind_cca_unpacked_default_09_ab();
 }
 
-/**
- Get the serialized public key.
-*/
 /**
 This function found in impl
 {libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked<Vector,
-K>[TraitClause@0, TraitClause@1]}
+K>[TraitClause@0, TraitClause@1]#3}
 */
 /**
 A monomorphic instance of
-libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_dd with types
+libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_30 with types
 libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
 - K= 3
 - RANKED_BYTES_PER_RING_ELEMENT= 1152
 - PUBLIC_KEY_SIZE= 1184
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static KRML_MUSTINLINE void
-libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(
+libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_ed(
     libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *self,
     libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
   libcrux_ml_kem_ind_cpa_serialize_public_key_mut_ed(
@@ -7380,28 +7382,25 @@ libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(
       serialized->value);
 }
 
-/**
- Get the serialized public key.
-*/
 /**
 This function found in impl
 {libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked<Vector,
-K>[TraitClause@0, TraitClause@1]#2}
+K>[TraitClause@0, TraitClause@1]#4}
 */
 /**
 A monomorphic instance of
-libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_de with types
+libcrux_ml_kem.ind_cca.unpacked.serialized_public_key_mut_fc with types
 libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics
 - K= 3
 - RANKED_BYTES_PER_RING_ELEMENT= 1152
 - PUBLIC_KEY_SIZE= 1184
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static KRML_MUSTINLINE void
-libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_ed(
+libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_fc_ed(
     libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *self,
     libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
-  libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(
+  libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_ed(
       &self->public_key, serialized);
 }
 
@@ -7413,7 +7412,7 @@ static inline void
 libcrux_ml_kem_mlkem768_avx2_unpacked_key_pair_serialized_public_key(
     libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *key_pair,
     libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
-  libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_ed(key_pair,
+  libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_fc_ed(key_pair,
                                                                   serialized);
 }
 
@@ -7457,17 +7456,17 @@ libcrux_ml_kem_ind_cpa_unpacked_clone_ef_ab(
 /**
 This function found in impl {(core::clone::Clone for
 libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked<Vector,
-K>[TraitClause@0, TraitClause@2])#4}
+K>[TraitClause@0, TraitClause@2])#2}
 */
 /**
-A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.clone_28
+A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.clone_dd
 with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 - K= 3
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63
-libcrux_ml_kem_ind_cca_unpacked_clone_28_ab(
+libcrux_ml_kem_ind_cca_unpacked_clone_dd_ab(
     libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *self) {
   libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 lit;
   lit.ind_cpa_public_key =
@@ -7479,23 +7478,20 @@ libcrux_ml_kem_ind_cca_unpacked_clone_28_ab(
   return lit;
 }
 
-/**
- Get the serialized public key.
-*/
 /**
 This function found in impl
 {libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked<Vector,
-K>[TraitClause@0, TraitClause@1]#2}
+K>[TraitClause@0, TraitClause@1]#4}
 */
 /**
-A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.public_key_de
+A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.public_key_fc
 with types libcrux_ml_kem_vector_avx2_SIMD256Vector
 with const generics
 - K= 3
 */
 KRML_ATTRIBUTE_TARGET("avx2")
 static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *
-libcrux_ml_kem_ind_cca_unpacked_public_key_de_ab(
+libcrux_ml_kem_ind_cca_unpacked_public_key_fc_ab(
     libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *self) {
   return &self->public_key;
 }
@@ -7508,8 +7504,8 @@ static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_public_key(
     libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *key_pair,
     libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *pk) {
   libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 uu____0 =
-      libcrux_ml_kem_ind_cca_unpacked_clone_28_ab(
-          libcrux_ml_kem_ind_cca_unpacked_public_key_de_ab(key_pair));
+      libcrux_ml_kem_ind_cca_unpacked_clone_dd_ab(
+          libcrux_ml_kem_ind_cca_unpacked_public_key_fc_ab(key_pair));
   pk[0U] = uu____0;
 }
 
@@ -7520,13 +7516,10 @@ KRML_ATTRIBUTE_TARGET("avx2")
 static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_serialized_public_key(
     libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_63 *public_key,
     libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) {
-  libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_ed(public_key,
+  libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_ed(public_key,
                                                                   serialized);
 }
 
-/**
- Generate an unpacked key from a serialized key.
-*/
 /**
 A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.unpack_public_key
 with types libcrux_ml_kem_hash_functions_avx2_Simd256Hash,

libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h

@@ -8,7 +8,7 @@
  * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
  * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198
  * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc
- * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9
+ * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d
  */
 
 #ifndef __libcrux_mlkem768_avx2_types_H