diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt index 69ab3fe65..13b6368d7 100644 --- a/libcrux-ml-kem/cg/code_gen.txt +++ b/libcrux-ml-kem/cg/code_gen.txt @@ -3,4 +3,4 @@ Charon: 3a133fe0eee9bd3928d5bb16c24ddd2dd0f3ee7f Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198 F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc -Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9 +Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h index c948f2203..30f40f051 100644 --- a/libcrux-ml-kem/cg/libcrux_core.h +++ b/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 diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h index f5f5ce2f6..244aa8e45 100644 --- a/libcrux-ml-kem/cg/libcrux_ct_ops.h +++ b/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 diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h index 791e21461..7a5dafa68 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h +++ b/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[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,10 +7287,10 @@ 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[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 @@ -7293,7 +7298,7 @@ with const generics 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,20 +7354,17 @@ 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[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 @@ -7370,7 +7372,7 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ 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,17 +7382,14 @@ 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[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 @@ -7398,10 +7397,10 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ 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[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[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, diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h index f7e64752f..fe16c7d0b 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h +++ b/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 diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h index fe8e065e0..a5cfe8f8d 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198 * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc - * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9 + * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d */ #ifndef __libcrux_mlkem768_portable_H @@ -6965,38 +6965,22 @@ static inline tuple_c2 libcrux_ml_kem_mlkem768_portable_unpacked_encapsulate( /** A monomorphic instance of -libcrux_ml_kem.ind_cca.unpacked.generate_keypair.closure.closure with types -libcrux_ml_kem_vector_portable_vector_type_PortableVector, -libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]], -libcrux_ml_kem_variant_MlKem with const generics +libcrux_ml_kem.ind_cca.unpacked.transpose_a.closure.closure with types +libcrux_ml_kem_vector_portable_vector_type_PortableVector 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 */ static inline libcrux_ml_kem_polynomial_PolynomialRingElement_1d -libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_closure_f8(size_t _j) { +libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_closure_1b(size_t _j) { return libcrux_ml_kem_polynomial_ZERO_ef_8c(); } /** -A monomorphic instance of -libcrux_ml_kem.ind_cca.unpacked.generate_keypair.closure with types -libcrux_ml_kem_vector_portable_vector_type_PortableVector, -libcrux_ml_kem_hash_functions_portable_PortableHash[[$3size_t]], -libcrux_ml_kem_variant_MlKem with const generics +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a.closure +with types libcrux_ml_kem_vector_portable_vector_type_PortableVector +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 */ -static inline void libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_f8( +static inline void libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_1b( size_t _i, libcrux_ml_kem_polynomial_PolynomialRingElement_1d ret[3U]) { for (size_t i = (size_t)0U; i < (size_t)3U; i++) { ret[i] = libcrux_ml_kem_polynomial_ZERO_ef_8c(); @@ -7029,8 +7013,36 @@ libcrux_ml_kem_polynomial_clone_8d_8c( } /** - Generate Unpacked Keys +A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.transpose_a +with types libcrux_ml_kem_vector_portable_vector_type_PortableVector +with const generics +- K= 3 */ +static inline void libcrux_ml_kem_ind_cca_unpacked_transpose_a_1b( + libcrux_ml_kem_polynomial_PolynomialRingElement_1d ind_cpa_a[3U][3U], + libcrux_ml_kem_polynomial_PolynomialRingElement_1d ret[3U][3U]) { + libcrux_ml_kem_polynomial_PolynomialRingElement_1d A[3U][3U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) { + libcrux_ml_kem_ind_cca_unpacked_transpose_a_closure_1b(i, A[i]); + } + for (size_t i = (size_t)0U; i < (size_t)3U; i++) { + size_t i0 = i; + libcrux_ml_kem_polynomial_PolynomialRingElement_1d _a_i[3U][3U]; + memcpy(_a_i, A, + (size_t)3U * + sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_1d[3U])); + for (size_t i1 = (size_t)0U; i1 < (size_t)3U; i1++) { + size_t j = i1; + libcrux_ml_kem_polynomial_PolynomialRingElement_1d uu____0 = + libcrux_ml_kem_polynomial_clone_8d_8c(&ind_cpa_a[j][i0]); + A[i0][j] = uu____0; + } + } + memcpy(ret, A, + (size_t)3U * + sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_1d[3U])); +} + /** A monomorphic instance of libcrux_ml_kem.ind_cca.unpacked.generate_keypair with types libcrux_ml_kem_vector_portable_vector_type_PortableVector, @@ -7057,20 +7069,12 @@ static KRML_MUSTINLINE void libcrux_ml_kem_ind_cca_unpacked_generate_keypair_f8( libcrux_ml_kem_ind_cpa_generate_keypair_unpacked_1c( ind_cpa_keypair_randomness, &out->private_key.ind_cpa_private_key, &out->public_key.ind_cpa_public_key); + libcrux_ml_kem_polynomial_PolynomialRingElement_1d uu____0[3U][3U]; + memcpy(uu____0, out->public_key.ind_cpa_public_key.A, + (size_t)3U * + sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_1d[3U])); libcrux_ml_kem_polynomial_PolynomialRingElement_1d A[3U][3U]; - for (size_t i = (size_t)0U; i < (size_t)3U; i++) { - libcrux_ml_kem_ind_cca_unpacked_generate_keypair_closure_f8(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_1d uu____0 = - libcrux_ml_kem_polynomial_clone_8d_8c( - &out->public_key.ind_cpa_public_key.A[j][i1]); - A[i1][j] = uu____0; - } - } + libcrux_ml_kem_ind_cca_unpacked_transpose_a_1b(uu____0, A); libcrux_ml_kem_polynomial_PolynomialRingElement_1d uu____1[3U][3U]; memcpy(uu____1, A, (size_t)3U * @@ -7140,16 +7144,16 @@ static inline void libcrux_ml_kem_mlkem768_portable_unpacked_generate_key_pair( /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked[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_portable_vector_type_PortableVector with const generics - K= 3 */ static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 -libcrux_ml_kem_ind_cca_unpacked_default_1c_1b(void) { +libcrux_ml_kem_ind_cca_unpacked_default_09_1b(void) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 lit; lit.ind_cpa_public_key = libcrux_ml_kem_ind_cpa_unpacked_default_8d_1b(); lit.public_key_hash[0U] = 0U; @@ -7190,17 +7194,17 @@ libcrux_ml_kem_ind_cca_unpacked_default_1c_1b(void) { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked[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_portable_vector_type_PortableVector with const generics - K= 3 */ static KRML_MUSTINLINE libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked - libcrux_ml_kem_ind_cca_unpacked_default_07_1b(void) { + libcrux_ml_kem_ind_cca_unpacked_default_53_1b(void) { libcrux_ml_kem_ind_cca_unpacked_MlKemPrivateKeyUnpacked_a0 uu____0; uu____0.ind_cpa_private_key = libcrux_ml_kem_ind_cpa_unpacked_default_1a_1b(); uu____0.implicit_rejection_value[0U] = 0U; @@ -7238,7 +7242,7 @@ static KRML_MUSTINLINE return (CLITERAL( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked){ .private_key = uu____0, - .public_key = libcrux_ml_kem_ind_cca_unpacked_default_1c_1b()}); + .public_key = libcrux_ml_kem_ind_cca_unpacked_default_09_1b()}); } /** @@ -7246,7 +7250,7 @@ static KRML_MUSTINLINE */ static inline libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked libcrux_ml_kem_mlkem768_portable_unpacked_init_key_pair(void) { - return libcrux_ml_kem_ind_cca_unpacked_default_07_1b(); + return libcrux_ml_kem_ind_cca_unpacked_default_53_1b(); } /** @@ -7254,27 +7258,24 @@ libcrux_ml_kem_mlkem768_portable_unpacked_init_key_pair(void) { */ static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 libcrux_ml_kem_mlkem768_portable_unpacked_init_public_key(void) { - return libcrux_ml_kem_ind_cca_unpacked_default_1c_1b(); + return libcrux_ml_kem_ind_cca_unpacked_default_09_1b(); } -/** - Get the serialized public key. -*/ /** This function found in impl {libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked[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_portable_vector_type_PortableVector with const generics - K= 3 - RANKED_BYTES_PER_RING_ELEMENT= 1152 - PUBLIC_KEY_SIZE= 1184 */ static KRML_MUSTINLINE void -libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_6c( +libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_6c( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *self, libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) { libcrux_ml_kem_ind_cpa_serialize_public_key_mut_6c( @@ -7284,27 +7285,24 @@ libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_6c( serialized->value); } -/** - Get the serialized public key. -*/ /** This function found in impl {libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked[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_portable_vector_type_PortableVector with const generics - K= 3 - RANKED_BYTES_PER_RING_ELEMENT= 1152 - PUBLIC_KEY_SIZE= 1184 */ static KRML_MUSTINLINE void -libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_6c( +libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_fc_6c( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked *self, libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_6c( + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_6c( &self->public_key, serialized); } @@ -7315,7 +7313,7 @@ static inline void libcrux_ml_kem_mlkem768_portable_unpacked_key_pair_serialized_public_key( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked *key_pair, libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_6c(key_pair, + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_fc_6c(key_pair, serialized); } @@ -7358,16 +7356,16 @@ libcrux_ml_kem_ind_cpa_unpacked_clone_ef_1b( /** This function found in impl {(core::clone::Clone for libcrux_ml_kem::ind_cca::unpacked::MlKemPublicKeyUnpacked[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_portable_vector_type_PortableVector with const generics - K= 3 */ static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 -libcrux_ml_kem_ind_cca_unpacked_clone_28_1b( +libcrux_ml_kem_ind_cca_unpacked_clone_dd_1b( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *self) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 lit; lit.ind_cpa_public_key = @@ -7379,22 +7377,19 @@ libcrux_ml_kem_ind_cca_unpacked_clone_28_1b( return lit; } -/** - Get the serialized public key. -*/ /** This function found in impl {libcrux_ml_kem::ind_cca::unpacked::MlKemKeyPairUnpacked[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_portable_vector_type_PortableVector with const generics - K= 3 */ static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 * -libcrux_ml_kem_ind_cca_unpacked_public_key_de_1b( +libcrux_ml_kem_ind_cca_unpacked_public_key_fc_1b( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked *self) { return &self->public_key; } @@ -7406,8 +7401,8 @@ static inline void libcrux_ml_kem_mlkem768_portable_unpacked_public_key( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked *key_pair, libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *pk) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 uu____0 = - libcrux_ml_kem_ind_cca_unpacked_clone_28_1b( - libcrux_ml_kem_ind_cca_unpacked_public_key_de_1b(key_pair)); + libcrux_ml_kem_ind_cca_unpacked_clone_dd_1b( + libcrux_ml_kem_ind_cca_unpacked_public_key_fc_1b(key_pair)); pk[0U] = uu____0; } @@ -7418,13 +7413,10 @@ static inline void libcrux_ml_kem_mlkem768_portable_unpacked_serialized_public_key( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *public_key, libcrux_ml_kem_types_MlKemPublicKey_30 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_6c(public_key, + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_30_6c(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_portable_PortableHash[[$3size_t]], diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h index 2657c84ae..3133e6233 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h @@ -8,7 +8,7 @@ * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198 * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc - * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9 + * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d */ #ifndef __libcrux_mlkem768_portable_types_H diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h index 5c7645481..cf22f9844 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h @@ -8,7 +8,7 @@ * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198 * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc - * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9 + * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/cg/libcrux_sha3_portable.h b/libcrux-ml-kem/cg/libcrux_sha3_portable.h index 7a3a3cfc9..0b6f7b530 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h @@ -8,7 +8,7 @@ * Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c * Karamel: c31a22c1e07d2118c07ee5cebb640d863e31a198 * F*: 2c32d6e230851bbceadac7a21fc418fa2bb7e4bc - * Libcrux: 18a089ceff3ef1a9f6876cd99a9f4f42c0fe05d9 + * Libcrux: 7ed909f8033142d720fcbfe309243b9fa52d181d */ #ifndef __libcrux_sha3_portable_H diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst index feecb5229..90b5d0f43 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst @@ -14,7 +14,7 @@ let _ = let open Libcrux_ml_kem.Vector.Traits in () -let impl_2__private_key +let impl_4__private_key (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -23,7 +23,7 @@ let impl_2__private_key (self: t_MlKemKeyPairUnpacked v_K v_Vector) = self.f_private_key -let impl_2__public_key +let impl_4__public_key (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -32,7 +32,7 @@ let impl_2__public_key (self: t_MlKemKeyPairUnpacked v_K v_Vector) = self.f_public_key -let impl_2__serialized_private_key +let impl_4__serialized_private_key (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -40,11 +40,105 @@ let impl_2__serialized_private_key Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) = + let _:Prims.unit = admit () in Rust_primitives.Hax.never_to_any (Core.Panicking.panic "not yet implemented" <: Rust_primitives.Hax.t_Never) -let impl_2__new +let transpose_a + (v_K: usize) + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i1: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + (ind_cpa_a: + t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K) + = + let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + Core.Array.from_fn #(t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) + v_K + (fun v__i -> + let v__i:usize = v__i in + Core.Array.from_fn #(Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) + v_K + (fun v__j -> + let v__j:usize = v__j in + Libcrux_ml_kem.Polynomial.impl_2__ZERO #v_Vector () + <: + Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) + <: + t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) + in + let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + Rust_primitives.Hax.Folds.fold_range (sz 0) + v_K + (fun v_A i -> + let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) + v_K = + v_A + in + let i:usize = i in + forall (j: nat). + j < v i ==> + (forall (k: nat). + k < v v_K ==> Seq.index (Seq.index v_A j) k == Seq.index (Seq.index ind_cpa_a k) j)) + v_A + (fun v_A i -> + let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) + v_K = + v_A + in + let i:usize = i in + let v__a_i:t_Array + (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + v_A + in + Rust_primitives.Hax.Folds.fold_range (sz 0) + v_K + (fun v_A j -> + let v_A:t_Array + (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + v_A + in + let j:usize = j in + (forall (k: nat). k < v i ==> Seq.index v_A k == Seq.index v__a_i k) /\ + (forall (k: nat). + k < v j ==> + Seq.index (Seq.index v_A (v i)) k == Seq.index (Seq.index ind_cpa_a k) (v i))) + v_A + (fun v_A j -> + let v_A:t_Array + (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + v_A + in + let j:usize = j in + let v_A:t_Array + (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v_A + i + (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (v_A.[ i ] + <: + t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) + j + (Core.Clone.f_clone #(Libcrux_ml_kem.Polynomial.t_PolynomialRingElement + v_Vector) + #FStar.Tactics.Typeclasses.solve + ((ind_cpa_a.[ j ] + <: + t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) + v_K).[ i ] + <: + Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) + <: + Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) + <: + t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) + in + v_A)) + in + v_A + +let impl_4__new (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -92,6 +186,14 @@ let unpack_public_key <: t_MlKemPublicKeyUnpacked v_K v_Vector in + let _:Prims.unit = + let _, seed = split public_key.f_value (Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE v_K) in + Lib.Sequence.eq_intro #u8 #32 (Libcrux_ml_kem.Utils.into_padded_array (sz 32) seed) seed; + Lib.Sequence.eq_intro #u8 + #32 + (Seq.slice (Libcrux_ml_kem.Utils.into_padded_array (sz 34) seed) 0 32) + seed + in let unpacked_public_key:t_MlKemPublicKeyUnpacked v_K v_Vector = { unpacked_public_key with @@ -175,6 +277,12 @@ let encapsulate (public_key: t_MlKemPublicKeyUnpacked v_K v_Vector) (randomness: t_Array u8 (sz 32)) = + let _:Prims.unit = + Lib.Sequence.eq_intro #u8 + #32 + (Seq.slice (Libcrux_ml_kem.Utils.into_padded_array (sz 64) randomness) 0 32) + randomness + in let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) = Libcrux_ml_kem.Utils.into_padded_array (sz 64) (randomness <: t_Slice u8) in @@ -193,6 +301,9 @@ let encapsulate <: t_Slice u8) in + let _:Prims.unit = + Lib.Sequence.eq_intro #u8 #64 to_hash (concat randomness public_key.f_public_key_hash) + in let hashed:t_Array u8 (sz 64) = Libcrux_ml_kem.Hash_functions.f_G #v_Hasher #v_K @@ -222,7 +333,7 @@ let encapsulate <: (Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32)) -let impl__serialized_public_key_mut +let impl_3__serialized_public_key_mut (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) @@ -250,7 +361,7 @@ let impl__serialized_public_key_mut in serialized -let impl_2__serialized_public_key_mut +let impl_4__serialized_public_key_mut (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) @@ -263,7 +374,7 @@ let impl_2__serialized_public_key_mut let hax_temp_output, serialized:(Prims.unit & Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) = (), - impl__serialized_public_key_mut v_K + impl_3__serialized_public_key_mut v_K #v_Vector v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE @@ -274,7 +385,7 @@ let impl_2__serialized_public_key_mut in serialized -let impl__serialized_public_key +let impl_3__serialized_public_key (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) @@ -295,7 +406,7 @@ let impl__serialized_public_key <: t_Array u8 v_PUBLIC_KEY_SIZE) -let impl_2__serialized_public_key +let impl_4__serialized_public_key (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) @@ -304,12 +415,14 @@ let impl_2__serialized_public_key Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (self: t_MlKemKeyPairUnpacked v_K v_Vector) = - impl__serialized_public_key v_K + impl_3__serialized_public_key v_K #v_Vector v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE self.f_public_key +#push-options "--z3rlimit 200 --ext context_pruning" + let generate_keypair (v_K v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_BYTES_PER_RING_ELEMENT v_ETA1 v_ETA1_RANDOMNESS_SIZE: usize) @@ -375,78 +488,39 @@ let generate_keypair in let _:Prims.unit = () in let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = - Core.Array.from_fn #(t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - v_K - (fun v__i -> - let v__i:usize = v__i in - Core.Array.from_fn #(Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) - v_K - (fun v__j -> - let v__j:usize = v__j in - Libcrux_ml_kem.Polynomial.impl_2__ZERO #v_Vector () - <: - Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) - <: - t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - in - let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = - Rust_primitives.Hax.Folds.fold_range (sz 0) - v_K - (fun v_A temp_1_ -> - let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - v_K = - v_A - in - let _:usize = temp_1_ in - true) - v_A - (fun v_A i -> - let v_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - v_K = - v_A - in - let i:usize = i in - Rust_primitives.Hax.Folds.fold_range (sz 0) - v_K - (fun v_A temp_1_ -> - let v_A:t_Array - (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = - v_A - in - let _:usize = temp_1_ in - true) - v_A - (fun v_A j -> - let v_A:t_Array - (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = - v_A - in - let j:usize = j in - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v_A - i - (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (v_A.[ i ] - <: - t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - j - (Core.Clone.f_clone #(Libcrux_ml_kem.Polynomial.t_PolynomialRingElement - v_Vector) - #FStar.Tactics.Typeclasses.solve - ((out.f_public_key.f_ind_cpa_public_key - .Libcrux_ml_kem.Ind_cpa.Unpacked.f_A.[ j ] - <: - t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) - v_K).[ i ] - <: - Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) - <: - Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) - <: - t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - <: - t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) - v_K) - <: - t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K) + transpose_a v_K + #v_Vector + out.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A + in + let _:Prims.unit = + let ind_cpa_keypair_randomness, _ = + split randomness Spec.MLKEM.v_CPA_KEY_GENERATION_SEED_SIZE + in + let (((_, _), matrix_A_as_ntt), _), sufficient_randomness = + Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K ind_cpa_keypair_randomness + in + let m_v_A = Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector v_A in + let m_f_A = + Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K + #v_Vector + out.f_public_key.f_ind_cpa_public_key.f_A + in + let m_A:Spec.MLKEM.matrix v_K = createi v_K (Spec.MLKEM.matrix_A_as_ntt_i matrix_A_as_ntt) in + assert (forall (i: nat). + i < v v_K ==> + (forall (j: nat). + j < v v_K ==> Seq.index (Seq.index m_v_A i) j == Seq.index (Seq.index m_f_A j) i)); + let lemma_aux (i: nat{i < v v_K}) + : Lemma (sufficient_randomness ==> Seq.index m_v_A i == Seq.index m_A i) = + if sufficient_randomness + then + Lib.Sequence.eq_intro #(Spec.MLKEM.polynomial) + #(v v_K) + (Seq.index m_v_A i) + (Seq.index m_A i) + in + Classical.forall_intro lemma_aux; + if sufficient_randomness then Lib.Sequence.eq_intro #(Spec.MLKEM.vector v_K) #(v v_K) m_A m_v_A in let out:t_MlKemKeyPairUnpacked v_K v_Vector = { @@ -523,6 +597,10 @@ let generate_keypair in out +#pop-options + +#push-options "--z3rlimit 200 --ext context_pruning --z3refresh" + let decapsulate (v_K v_SECRET_KEY_SIZE v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_SIZE v_C2_SIZE v_VECTOR_U_COMPRESSION_FACTOR v_VECTOR_V_COMPRESSION_FACTOR v_C1_BLOCK_SIZE v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE v_IMPLICIT_REJECTION_HASH_INPUT_SIZE: usize) @@ -536,6 +614,15 @@ let decapsulate (key_pair: t_MlKemKeyPairUnpacked v_K v_Vector) (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE) = + let _:Prims.unit = + assert (v v_IMPLICIT_REJECTION_HASH_INPUT_SIZE == 32 + v (Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K)); + assert (v (Spec.MLKEM.v_C1_SIZE v_K +! Spec.MLKEM.v_C2_SIZE v_K) == + v (Spec.MLKEM.v_C1_SIZE v_K) + v (Spec.MLKEM.v_C2_SIZE v_K)); + assert (v (Spec.MLKEM.v_C1_SIZE v_K) == v (Spec.MLKEM.v_C1_BLOCK_SIZE v_K) * v v_K); + assert (v (Spec.MLKEM.v_C1_BLOCK_SIZE v_K) == + 32 * v (Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K)); + assert (v (Spec.MLKEM.v_C2_SIZE v_K) == 32 * v (Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K)) + in let decrypted:t_Array u8 (sz 32) = Libcrux_ml_kem.Ind_cpa.decrypt_unpacked v_K v_CIPHERTEXT_SIZE @@ -549,6 +636,7 @@ let decapsulate let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) = Libcrux_ml_kem.Utils.into_padded_array (sz 64) (decrypted <: t_Slice u8) in + let _:Prims.unit = Lib.Sequence.eq_intro #u8 #32 (Seq.slice to_hash 0 32) decrypted in let to_hash:t_Array u8 (sz 64) = Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE } @@ -564,6 +652,9 @@ let decapsulate <: t_Slice u8) in + let _:Prims.unit = + Lib.Sequence.lemma_concat2 32 decrypted 32 key_pair.f_public_key.f_public_key_hash to_hash + in let hashed:t_Array u8 (sz 64) = Libcrux_ml_kem.Hash_functions.f_G #v_Hasher #v_K @@ -580,6 +671,12 @@ let decapsulate Libcrux_ml_kem.Utils.into_padded_array v_IMPLICIT_REJECTION_HASH_INPUT_SIZE (key_pair.f_private_key.f_implicit_rejection_value <: t_Slice u8) in + let _:Prims.unit = + Lib.Sequence.eq_intro #u8 + #32 + (Seq.slice to_hash 0 32) + key_pair.f_private_key.f_implicit_rejection_value + in let to_hash:t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE = Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE } @@ -600,6 +697,13 @@ let decapsulate <: t_Slice u8) in + let _:Prims.unit = + Lib.Sequence.lemma_concat2 32 + key_pair.f_private_key.f_implicit_rejection_value + (v (Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K)) + ciphertext.f_value + to_hash + in let (implicit_rejection_shared_secret: t_Array u8 (sz 32)):t_Array u8 (sz 32) = Libcrux_ml_kem.Hash_functions.f_PRF #v_Hasher #v_K @@ -626,3 +730,5 @@ let decapsulate Libcrux_ml_kem.Constant_time_ops.select_shared_secret_in_constant_time shared_secret (implicit_rejection_shared_secret <: t_Slice u8) selector + +#pop-options diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti index 8a8daa153..6bccf5010 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti @@ -39,7 +39,7 @@ type t_MlKemKeyPairUnpacked } /// Get the serialized public key. -val impl_2__private_key +val impl_4__private_key (v_K: usize) (#v_Vector: Type0) {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} @@ -47,7 +47,7 @@ val impl_2__private_key : Prims.Pure (t_MlKemPrivateKeyUnpacked v_K v_Vector) Prims.l_True (fun _ -> Prims.l_True) /// Get the serialized public key. -val impl_2__public_key +val impl_4__public_key (v_K: usize) (#v_Vector: Type0) {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} @@ -55,15 +55,36 @@ val impl_2__public_key : Prims.Pure (t_MlKemPublicKeyUnpacked v_K v_Vector) Prims.l_True (fun _ -> Prims.l_True) /// Get the serialized private key. -val impl_2__serialized_private_key +val impl_4__serialized_private_key (v_K: usize) (#v_Vector: Type0) {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPrivateKey v_K) Prims.l_True (fun _ -> Prims.l_True) +val transpose_a + (v_K: usize) + (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (ind_cpa_a: + t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K) + : Prims.Pure + (t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K) + Prims.l_True + (ensures + fun result -> + let result:t_Array + (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K = + result + in + forall (i: nat). + i < v v_K ==> + (forall (j: nat). + j < v v_K ==> + Seq.index (Seq.index result i) j == Seq.index (Seq.index ind_cpa_a j) i)) + [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1 +let impl (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -90,7 +111,7 @@ let impl_1 } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_3 +let impl_1 (v_K: usize) (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -128,7 +149,7 @@ let impl_3 } /// Create a new empty unpacked key pair. -val impl_2__new: +val impl_4__new: v_K: usize -> #v_Vector: Type0 -> {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} -> @@ -143,7 +164,28 @@ val unpack_public_key {| i3: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) (unpacked_public_key: t_MlKemPublicKeyUnpacked v_K v_Vector) - : Prims.Pure (t_MlKemPublicKeyUnpacked v_K v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_MlKemPublicKeyUnpacked v_K v_Vector) + (requires + Spec.MLKEM.is_rank v_K /\ v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + v_T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE v_K) + (ensures + fun unpacked_public_key_future -> + let unpacked_public_key_future:t_MlKemPublicKeyUnpacked v_K v_Vector = + unpacked_public_key_future + in + let public_key_hash, (seed, (deserialized_pk, (matrix_A, valid))) = + Spec.MLKEM.ind_cca_unpack_public_key v_K public_key.f_value + in + (valid ==> + Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K + #v_Vector + unpacked_public_key_future.f_ind_cpa_public_key.f_A == + matrix_A) /\ + Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + unpacked_public_key_future.f_ind_cpa_public_key.f_t_as_ntt == + deserialized_pk /\ unpacked_public_key_future.f_ind_cpa_public_key.f_seed_for_A == seed /\ + unpacked_public_key_future.f_public_key_hash == public_key_hash) val encapsulate (v_K v_CIPHERTEXT_SIZE v_PUBLIC_KEY_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_SIZE v_C2_SIZE v_VECTOR_U_COMPRESSION_FACTOR v_VECTOR_V_COMPRESSION_FACTOR v_VECTOR_U_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE: @@ -154,11 +196,38 @@ val encapsulate (public_key: t_MlKemPublicKeyUnpacked v_K v_Vector) (randomness: t_Array u8 (sz 32)) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32)) - Prims.l_True - (fun _ -> Prims.l_True) + (requires + Spec.MLKEM.is_rank v_K /\ v_ETA1 == Spec.MLKEM.v_ETA1 v_K /\ + v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\ + v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\ + v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\ + v_C1_SIZE == Spec.MLKEM.v_C1_SIZE v_K /\ v_C2_SIZE == Spec.MLKEM.v_C2_SIZE v_K /\ + v_VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\ + v_VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\ + v_VECTOR_U_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\ + v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K) + (ensures + fun temp_0_ -> + let ciphertext_result, shared_secret_array:(Libcrux_ml_kem.Types.t_MlKemCiphertext + v_CIPHERTEXT_SIZE & + t_Array u8 (sz 32)) = + temp_0_ + in + let ciphertext, shared_secret = + Spec.MLKEM.ind_cca_unpack_encapsulate v_K + public_key.f_public_key_hash + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + public_key.f_ind_cpa_public_key.f_t_as_ntt) + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K + #v_Vector + public_key.f_ind_cpa_public_key.f_A) + randomness + in + ciphertext_result.f_value == ciphertext /\ shared_secret_array == shared_secret) /// Get the serialized public key. -val impl__serialized_public_key_mut +val impl_3__serialized_public_key_mut (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) @@ -166,11 +235,30 @@ val impl__serialized_public_key_mut (self: t_MlKemPublicKeyUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) - Prims.l_True - (fun _ -> Prims.l_True) + (requires + Spec.MLKEM.is_rank v_K /\ + v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + (forall (i: nat). + i < v v_K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self + .f_ind_cpa_public_key + .f_t_as_ntt + i))) + (ensures + fun serialized_future -> + let serialized_future:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = + serialized_future + in + serialized_future.f_value == + Seq.append (Spec.MLKEM.vector_encode_12 #v_K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + self.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_ind_cpa_public_key.f_seed_for_A) /// Get the serialized public key. -val impl_2__serialized_public_key_mut +val impl_4__serialized_public_key_mut (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) @@ -178,30 +266,83 @@ val impl_2__serialized_public_key_mut (self: t_MlKemKeyPairUnpacked v_K v_Vector) (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) - Prims.l_True - (fun _ -> Prims.l_True) + (requires + Spec.MLKEM.is_rank v_K /\ + v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + (forall (i: nat). + i < v v_K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key + .f_ind_cpa_public_key + .f_t_as_ntt + i))) + (ensures + fun serialized_future -> + let serialized_future:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = + serialized_future + in + serialized_future.f_value == + Seq.append (Spec.MLKEM.vector_encode_12 #v_K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_public_key.f_ind_cpa_public_key.f_seed_for_A) /// Get the serialized public key. -val impl__serialized_public_key +val impl_3__serialized_public_key (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemPublicKeyUnpacked v_K v_Vector) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) - Prims.l_True - (fun _ -> Prims.l_True) + (requires + Spec.MLKEM.is_rank v_K /\ + v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + (forall (i: nat). + i < v v_K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self + .f_ind_cpa_public_key + .f_t_as_ntt + i))) + (ensures + fun res -> + let res:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = res in + res.f_value == + Seq.append (Spec.MLKEM.vector_encode_12 #v_K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + self.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_ind_cpa_public_key.f_seed_for_A) /// Get the serialized public key. -val impl_2__serialized_public_key +val impl_4__serialized_public_key (v_K: usize) (#v_Vector: Type0) (v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) {| i2: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_MlKemKeyPairUnpacked v_K v_Vector) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE) - Prims.l_True - (fun _ -> Prims.l_True) + (requires + Spec.MLKEM.is_rank v_K /\ + v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\ + (forall (i: nat). + i < v v_K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key + .f_ind_cpa_public_key + .f_t_as_ntt + i))) + (ensures + fun res -> + let res:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = res in + res.f_value == + Seq.append (Spec.MLKEM.vector_encode_12 #v_K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_public_key.f_ind_cpa_public_key.f_seed_for_A) /// Generate Unpacked Keys val generate_keypair @@ -213,7 +354,24 @@ val generate_keypair {| i5: Libcrux_ml_kem.Variant.t_Variant v_Scheme |} (randomness: t_Array u8 (sz 64)) (out: t_MlKemKeyPairUnpacked v_K v_Vector) - : Prims.Pure (t_MlKemKeyPairUnpacked v_K v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_MlKemKeyPairUnpacked v_K v_Vector) + (requires + Spec.MLKEM.is_rank v_K /\ v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\ + v_ETA1 == Spec.MLKEM.v_ETA1 v_K /\ + v_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\ + v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K) + (ensures + fun out_future -> + let out_future:t_MlKemKeyPairUnpacked v_K v_Vector = out_future in + let ((m_A, public_key_hash), implicit_rejection_value), valid = + Spec.MLKEM.ind_cca_unpack_generate_keypair v_K randomness + in + valid ==> + Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K + #v_Vector + out_future.f_public_key.f_ind_cpa_public_key.f_A == + m_A /\ out_future.f_public_key.f_public_key_hash == public_key_hash /\ + out_future.f_private_key.f_implicit_rejection_value == implicit_rejection_value) val decapsulate (v_K v_SECRET_KEY_SIZE v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_SIZE v_C2_SIZE v_VECTOR_U_COMPRESSION_FACTOR v_VECTOR_V_COMPRESSION_FACTOR v_C1_BLOCK_SIZE v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE v_IMPLICIT_REJECTION_HASH_INPUT_SIZE: @@ -223,4 +381,32 @@ val decapsulate {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} (key_pair: t_MlKemKeyPairUnpacked v_K v_Vector) (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE) - : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_Array u8 (sz 32)) + (requires + Spec.MLKEM.is_rank v_K /\ v_ETA1 == Spec.MLKEM.v_ETA1 v_K /\ + v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\ + v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\ + v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\ + v_C1_SIZE == Spec.MLKEM.v_C1_SIZE v_K /\ v_C2_SIZE == Spec.MLKEM.v_C2_SIZE v_K /\ + v_VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\ + v_VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\ + v_C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\ + v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\ + v_IMPLICIT_REJECTION_HASH_INPUT_SIZE == Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE v_K) + (ensures + fun result -> + let result:t_Array u8 (sz 32) = result in + result == + Spec.MLKEM.ind_cca_unpack_decapsulate v_K + key_pair.f_public_key.f_public_key_hash + key_pair.f_private_key.f_implicit_rejection_value + ciphertext.f_value + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + key_pair.f_private_key.f_ind_cpa_private_key.f_secret_as_ntt) + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + key_pair.f_public_key.f_ind_cpa_public_key.f_t_as_ntt) + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K + #v_Vector + key_pair.f_public_key.f_ind_cpa_public_key.f_A)) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst index aa3f657ef..29146d11c 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst @@ -382,6 +382,8 @@ let sample_vector_cbd_then_ntt_out <: (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8) +#push-options "--z3rlimit 500 --ext context_pruning --z3refresh" + let generate_keypair_unpacked (v_K v_ETA1 v_ETA1_RANDOMNESS_SIZE: usize) (#v_Vector #v_Hasher #v_Scheme: Type0) @@ -496,12 +498,14 @@ let generate_keypair_unpacked Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector in let _:Prims.unit = - let ((t_as_ntt, seed_for_A), secret_as_ntt), valid = + let (((t_as_ntt, seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid = Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed in assert (valid ==> ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key.f_t_as_ntt) == t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\ + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key.f_A == matrix_A_as_ntt + ) /\ ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector private_key.f_secret_as_ntt) == secret_as_ntt)); assert ((forall (i: nat). @@ -520,6 +524,8 @@ let generate_keypair_unpacked (Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPrivateKeyUnpacked v_K v_Vector & Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector) +#pop-options + #push-options "--z3rlimit 200 --ext context_pruning --z3refresh" let compress_then_serialize_u diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti index 51c306877..32c317b57 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti @@ -165,16 +165,17 @@ val generate_keypair_unpacked Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector) = temp_0_ in - let ((t_as_ntt, seed_for_A), secret_as_ntt), valid = + let (((t_as_ntt, seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid = Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed in (valid ==> - ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key_future.f_t_as_ntt - ) == + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key_future.f_t_as_ntt == t_as_ntt) /\ (public_key_future.f_seed_for_A == seed_for_A) /\ - ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K - #v_Vector - private_key_future.f_secret_as_ntt) == + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key_future.f_A == + matrix_A_as_ntt) /\ + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K + #v_Vector + private_key_future.f_secret_as_ntt == secret_as_ntt)) /\ (forall (i: nat). i < v v_K ==> diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile index b7a4485d1..b054ead79 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Makefile +++ b/libcrux-ml-kem/proofs/fstar/extraction/Makefile @@ -1,7 +1,6 @@ SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst -ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \ - Libcrux_ml_kem.Vector.Avx2.fsti \ +ADMIT_MODULES = Libcrux_ml_kem.Vector.Avx2.fsti \ Libcrux_ml_kem.Vector.Avx2.fst \ Libcrux_ml_kem.Vector.Avx2.Ntt.fst \ Libcrux_ml_kem.Vector.Avx2.Sampling.fst \ diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst index 7defc385c..a6114ea93 100644 --- a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst +++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst @@ -189,6 +189,7 @@ let sample_vector_cbd2 (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v d let sample_vector_cbd_then_ntt (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v domain_sep < 2 * v r}) : vector r = vector_ntt (sample_vector_cbd1 #r seed domain_sep) +[@ "opaque_to_smt"] let vector_encode_12 (#r:rank) (v: vector r) : t_Array u8 (v_T_AS_NTT_ENCODED_SIZE r) = let s: t_Array (t_Array _ (sz 384)) r = map_array (byte_encode 12) (coerce_vector_12 v) in flatten s @@ -229,7 +230,7 @@ let decode_then_decompress_v (u:usize{u == sz 4 \/ u == sz 5}): t_Array u8 (sz 3 (** IND-CPA Functions *) val ind_cpa_generate_keypair_unpacked (r:rank) (randomness:t_Array u8 v_CPA_KEY_GENERATION_SEED_SIZE) : - ((((vector r) & (t_Array u8 (sz 32))) & (vector r)) & bool) + (((((vector r) & (t_Array u8 (sz 32))) & (matrix r)) & (vector r)) & bool) let ind_cpa_generate_keypair_unpacked r randomness = let hashed = v_G (Seq.append randomness (Seq.create 1 (cast r <: u8))) in let (seed_for_A, seed_for_secret_and_error) = split hashed (sz 32) in @@ -237,7 +238,7 @@ let ind_cpa_generate_keypair_unpacked r randomness = let secret_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error (sz 0) in let error_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error r in let t_as_ntt = compute_As_plus_e_ntt #r matrix_A_as_ntt secret_as_ntt error_as_ntt in - (((t_as_ntt,seed_for_A), secret_as_ntt), sufficient_randomness) + (((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), sufficient_randomness /// This function implements most of Algorithm 12 of the /// NIST FIPS 203 specification; this is the MLKEM CPA-PKE key generation algorithm. @@ -249,7 +250,7 @@ let ind_cpa_generate_keypair_unpacked r randomness = val ind_cpa_generate_keypair (r:rank) (randomness:t_Array u8 v_CPA_KEY_GENERATION_SEED_SIZE) : (t_MLKEMCPAKeyPair r & bool) let ind_cpa_generate_keypair r randomness = - let (((t_as_ntt,seed_for_A), secret_as_ntt), sufficient_randomness) = + let ((((t_as_ntt,seed_for_A), _), secret_as_ntt), sufficient_randomness) = ind_cpa_generate_keypair_unpacked r randomness in let public_key_serialized = Seq.append (vector_encode_12 #r t_as_ntt) seed_for_A in let secret_key_serialized = vector_encode_12 #r secret_as_ntt in @@ -380,3 +381,67 @@ let ind_cca_decapsulate p secret_key ciphertext = if reencrypted = ciphertext then success_shared_secret, sufficient_randomness else rejection_shared_secret, sufficient_randomness + +val ind_cca_unpack_public_key (r:rank) (public_key: t_MLKEMPublicKey r) : + t_Array u8 (sz 32) & (t_Array u8 (sz 32) & (vector r & (matrix r & bool))) +let ind_cca_unpack_public_key p public_key = + let (ring_elements, seed) = split public_key (v_T_AS_NTT_ENCODED_SIZE p) in + let deserialized_pk = vector_decode_12 #p ring_elements in + let (matrix_A, sufficient_randomness) = sample_matrix_A_ntt seed in + let matrix_A = matrix_transpose #p matrix_A in + let public_key_hash = v_H public_key in + public_key_hash, (seed, (deserialized_pk, (matrix_A, sufficient_randomness))) + +let matrix_A_as_ntt_j (#r:rank) (matrix_A_as_ntt:matrix r) (i:usize{i <. r}) (j:usize{j <. r}) : polynomial = + Seq.index (Seq.index matrix_A_as_ntt (v j)) (v i) + +let matrix_A_as_ntt_i (#r:rank) (matrix_A_as_ntt:matrix r) (i:usize{i <. r}) : vector r = + createi r (matrix_A_as_ntt_j matrix_A_as_ntt i) + +val ind_cca_unpack_generate_keypair (r:rank) (randomness:t_Array u8 v_KEY_GENERATION_SEED_SIZE) : + ((matrix r & t_Array u8 (sz 32)) & t_Array u8 (sz 32)) & bool +let ind_cca_unpack_generate_keypair p randomness = + let (ind_cpa_keypair_randomness, implicit_rejection_value) = split randomness v_CPA_KEY_GENERATION_SEED_SIZE in + let ((((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), sufficient_randomness) = + ind_cpa_generate_keypair_unpacked p ind_cpa_keypair_randomness in + // let m_A = + // createi p (fun i -> + // createi p (fun j -> + // Seq.index (Seq.index matrix_A_as_ntt j) i + // )) + // in + let m_A = createi p (matrix_A_as_ntt_i matrix_A_as_ntt) in + let pk_serialized = Seq.append (vector_encode_12 t_as_ntt) seed_for_A in + let public_key_hash = v_H pk_serialized in + ((m_A, public_key_hash), implicit_rejection_value), sufficient_randomness + +val ind_cca_unpack_encapsulate (r:rank) (public_key_hash:t_Array u8 (sz 32)) + (t_as_ntt:vector r) + (matrix_A_as_ntt:matrix r) + (randomness:t_Array u8 v_SHARED_SECRET_SIZE) : + (t_MLKEMCiphertext r & t_Array u8 v_SHARED_SECRET_SIZE) +let ind_cca_unpack_encapsulate r public_key_hash t_as_ntt matrix_A_as_ntt randomness = + let to_hash = concat randomness public_key_hash in + let hashed = v_G to_hash in + let (shared_secret, pseudorandomness) = split hashed v_SHARED_SECRET_SIZE in + let ciphertext = ind_cpa_encrypt_unpacked r randomness pseudorandomness t_as_ntt matrix_A_as_ntt in + ciphertext, shared_secret + +val ind_cca_unpack_decapsulate (r:rank) (public_key_hash:t_Array u8 (sz 32)) + (implicit_rejection_value:t_Array u8 (sz 32)) + (ciphertext: t_MLKEMCiphertext r) + (secret_as_ntt:vector r) + (t_as_ntt:vector r) + (matrix_A_as_ntt:matrix r) : + t_Array u8 v_SHARED_SECRET_SIZE +let ind_cca_unpack_decapsulate r public_key_hash implicit_rejection_value ciphertext secret_as_ntt t_as_ntt matrix_A_as_ntt = + let decrypted = ind_cpa_decrypt_unpacked r ciphertext secret_as_ntt in + let to_hash = concat decrypted public_key_hash in + let hashed = v_G to_hash in + let (shared_secret, pseudorandomness) = split hashed v_SHARED_SECRET_SIZE in + let to_hash:t_Array u8 (v_IMPLICIT_REJECTION_HASH_INPUT_SIZE r) = concat implicit_rejection_value ciphertext in + let implicit_rejection_shared_secret = v_PRF v_SHARED_SECRET_SIZE to_hash in + let expected_ciphertext = ind_cpa_encrypt_unpacked r decrypted pseudorandomness t_as_ntt matrix_A_as_ntt in + if ciphertext = expected_ciphertext + then shared_secret + else implicit_rejection_shared_secret diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs index 825da534d..3d05ce368 100644 --- a/libcrux-ml-kem/src/ind_cca.rs +++ b/libcrux-ml-kem/src/ind_cca.rs @@ -420,6 +420,19 @@ pub(crate) mod unpacked { } /// Generate an unpacked key from a serialized key. + #[hax_lib::requires( + fstar!("Spec.MLKEM.is_rank $K /\\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K") + )] + #[hax_lib::ensures(|result| + fstar!("let (public_key_hash, (seed, (deserialized_pk, (matrix_A, valid)))) = + Spec.MLKEM.ind_cca_unpack_public_key $K ${public_key}.f_value in (valid ==> + Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_A == matrix_A) /\\ + Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_t_as_ntt == deserialized_pk /\\ + ${unpacked_public_key}_future.f_ind_cpa_public_key.f_seed_for_A == seed /\\ + ${unpacked_public_key}_future.f_public_key_hash == public_key_hash")) + ] #[inline(always)] pub(crate) fn unpack_public_key< const K: usize, @@ -436,6 +449,10 @@ pub(crate) mod unpacked { &public_key.value[..T_AS_NTT_ENCODED_SIZE], &mut unpacked_public_key.ind_cpa_public_key.t_as_ntt, ); + hax_lib::fstar!("let (_, seed) = split ${public_key}.f_value (Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K) in + Lib.Sequence.eq_intro #u8 #32 (Libcrux_ml_kem.Utils.into_padded_array (sz 32) seed) seed; + Lib.Sequence.eq_intro #u8 #32 + (Seq.slice (Libcrux_ml_kem.Utils.into_padded_array (sz 34) seed) 0 32) seed"); unpacked_public_key.ind_cpa_public_key.seed_for_A = into_padded_array(&public_key.value[T_AS_NTT_ENCODED_SIZE..]); sample_matrix_A::( @@ -446,9 +463,23 @@ pub(crate) mod unpacked { unpacked_public_key.public_key_hash = Hasher::H(public_key.as_slice()); } + #[hax_lib::attributes] impl MlKemPublicKeyUnpacked { /// Get the serialized public key. #[inline(always)] + #[requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + (forall (i:nat). i < v $K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index + self.f_ind_cpa_public_key.f_t_as_ntt i))"))] + #[ensures(|_| + fstar!("${serialized}_future.f_value == + Seq.append (Spec.MLKEM.vector_encode_12 #$K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector + self.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_ind_cpa_public_key.f_seed_for_A)") + )] pub fn serialized_public_key_mut< const RANKED_BYTES_PER_RING_ELEMENT: usize, const PUBLIC_KEY_SIZE: usize, @@ -465,6 +496,18 @@ pub(crate) mod unpacked { /// Get the serialized public key. #[inline(always)] + #[requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + (forall (i:nat). i < v $K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index + self.f_ind_cpa_public_key.f_t_as_ntt i))"))] + #[ensures(|res| + fstar!("${res}.f_value == Seq.append (Spec.MLKEM.vector_encode_12 #$K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector + self.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_ind_cpa_public_key.f_seed_for_A)") + )] pub fn serialized_public_key< const RANKED_BYTES_PER_RING_ELEMENT: usize, const PUBLIC_KEY_SIZE: usize, @@ -489,6 +532,7 @@ pub(crate) mod unpacked { } } + #[hax_lib::attributes] impl MlKemKeyPairUnpacked { /// Create a new empty unpacked key pair. #[inline(always)] @@ -498,6 +542,19 @@ pub(crate) mod unpacked { /// Get the serialized public key. #[inline(always)] + #[requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + (forall (i:nat). i < v $K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index + self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"))] + #[ensures(|_| + fstar!("${serialized}_future.f_value == + Seq.append (Spec.MLKEM.vector_encode_12 #$K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector + self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)") + )] pub fn serialized_public_key_mut< const RANKED_BYTES_PER_RING_ELEMENT: usize, const PUBLIC_KEY_SIZE: usize, @@ -513,6 +570,18 @@ pub(crate) mod unpacked { /// Get the serialized public key. #[inline(always)] + #[requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\ + (forall (i:nat). i < v $K ==> + Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index + self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"))] + #[ensures(|res| + fstar!("${res}.f_value == Seq.append (Spec.MLKEM.vector_encode_12 #$K + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector + self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)) + self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)") + )] pub fn serialized_public_key< const RANKED_BYTES_PER_RING_ELEMENT: usize, const PUBLIC_KEY_SIZE: usize, @@ -537,6 +606,7 @@ pub(crate) mod unpacked { /// Get the serialized private key. pub fn serialized_private_key(&self) -> MlKemPrivateKey { + hax_lib::fstar!("admit()"); todo!() } } @@ -554,8 +624,62 @@ pub(crate) mod unpacked { } } + #[hax_lib::ensures(|result| + fstar!("forall (i: nat). i < v $K ==> + (forall (j: nat). j < v $K ==> + Seq.index (Seq.index $result i) j == + Seq.index (Seq.index $ind_cpa_a j) i)")) + ] + pub(crate) fn transpose_a< + const K: usize, + Vector: Operations, + >( + ind_cpa_a: [[PolynomialRingElement; K]; K], + ) -> [[PolynomialRingElement; K]; K] { + // We need to un-transpose the A_transpose matrix provided by IND-CPA + // We would like to write the following but it is not supported by Eurydice yet. + // https://github.com/AeneasVerif/eurydice/issues/39 + // + // let A = from_fn(|i| { + // from_fn(|j| A_transpose[j][i]) + // }); + + #[allow(non_snake_case)] + let mut A = from_fn(|_i| from_fn(|_j| PolynomialRingElement::::ZERO())); + for i in 0..K { + hax_lib::loop_invariant!(|i: usize| { fstar!("forall (j: nat). j < v $i ==> + (forall (k: nat). k < v $K ==> + Seq.index (Seq.index $A j) k == + Seq.index (Seq.index $ind_cpa_a k) j)") }); + let _a_i = A; + for j in 0..K { + hax_lib::loop_invariant!(|j: usize| { fstar!("(forall (k: nat). k < v $i ==> + Seq.index $A k == Seq.index $_a_i k) /\\ + (forall (k: nat). k < v $j ==> + Seq.index (Seq.index $A (v $i)) k == + Seq.index (Seq.index $ind_cpa_a k) (v $i))") }); + A[i][j] = ind_cpa_a[j][i].clone(); + } + }; + A + } + /// Generate Unpacked Keys #[inline(always)] + #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] + #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ + $BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\\ + $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K"))] + #[hax_lib::ensures(|result| + fstar!("let ((m_A, public_key_hash), implicit_rejection_value), valid = + Spec.MLKEM.ind_cca_unpack_generate_keypair $K $randomness in + valid ==> Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector + ${out}_future.f_public_key.f_ind_cpa_public_key.f_A == m_A /\\ + ${out}_future.f_public_key.f_public_key_hash == public_key_hash /\\ + ${out}_future.f_private_key.f_implicit_rejection_value == implicit_rejection_value")) + ] pub(crate) fn generate_keypair< const K: usize, const CPA_PRIVATE_KEY_SIZE: usize, @@ -580,21 +704,27 @@ pub(crate) mod unpacked { &mut out.public_key.ind_cpa_public_key, ); - // We need to un-transpose the A_transpose matrix provided by IND-CPA - // We would like to write the following but it is not supported by Eurydice yet. - // https://github.com/AeneasVerif/eurydice/issues/39 - // - // let A = from_fn(|i| { - // from_fn(|j| A_transpose[j][i]) - // }); - #[allow(non_snake_case)] - let mut A = from_fn(|_i| from_fn(|_j| PolynomialRingElement::::ZERO())); - for i in 0..K { - for j in 0..K { - A[i][j] = out.public_key.ind_cpa_public_key.A[j][i].clone(); - } - } + let A = transpose_a::(out.public_key.ind_cpa_public_key.A); + hax_lib::fstar!("let (ind_cpa_keypair_randomness, _) = split $randomness Spec.MLKEM.v_CPA_KEY_GENERATION_SEED_SIZE in + let ((((_, _), matrix_A_as_ntt), _), sufficient_randomness) = + Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K ind_cpa_keypair_randomness in + let m_v_A = Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector $A in + let m_f_A = Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector out.f_public_key.f_ind_cpa_public_key.f_A in + let m_A:Spec.MLKEM.matrix $K = createi $K (Spec.MLKEM.matrix_A_as_ntt_i matrix_A_as_ntt) in + assert (forall (i: nat). i < v $K ==> + (forall (j: nat). j < v $K ==> + Seq.index (Seq.index m_v_A i) j == + Seq.index (Seq.index m_f_A j) i)); + let lemma_aux (i: nat{ i < v $K }) : Lemma + (sufficient_randomness ==> Seq.index m_v_A i == Seq.index m_A i) = + if sufficient_randomness then + Lib.Sequence.eq_intro #(Spec.MLKEM.polynomial) #(v $K) + (Seq.index m_v_A i) (Seq.index m_A i) + in + Classical.forall_intro lemma_aux; + if sufficient_randomness then + Lib.Sequence.eq_intro #(Spec.MLKEM.vector $K) #(v $K) m_A m_v_A"); out.public_key.ind_cpa_public_key.A = A; let pk_serialized = @@ -608,6 +738,26 @@ pub(crate) mod unpacked { // Encapsulate with Unpacked Public Key #[inline(always)] + #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ + $ETA2 == Spec.MLKEM.v_ETA2 $K /\\ + $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\ + $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\\ + $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\\ + $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\ + $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\ + $VECTOR_U_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\ + $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K"))] + #[hax_lib::ensures(|(ciphertext_result, shared_secret_array)| + fstar!("let (ciphertext, shared_secret) = + Spec.MLKEM.ind_cca_unpack_encapsulate $K ${public_key}.f_public_key_hash + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}.f_ind_cpa_public_key.f_t_as_ntt) + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}.f_ind_cpa_public_key.f_A) + $randomness in + ${ciphertext_result}.f_value == ciphertext /\\ + $shared_secret_array == shared_secret")) + ] pub(crate) fn encapsulate< const K: usize, const CIPHERTEXT_SIZE: usize, @@ -628,8 +778,12 @@ pub(crate) mod unpacked { public_key: &MlKemPublicKeyUnpacked, randomness: [u8; SHARED_SECRET_SIZE], ) -> (MlKemCiphertext, MlKemSharedSecret) { + hax_lib::fstar!("Lib.Sequence.eq_intro #u8 #32 (Seq.slice ( + Libcrux_ml_kem.Utils.into_padded_array (sz 64) $randomness) 0 32) $randomness"); let mut to_hash: [u8; 2 * H_DIGEST_SIZE] = into_padded_array(&randomness); to_hash[H_DIGEST_SIZE..].copy_from_slice(&public_key.public_key_hash); + hax_lib::fstar!("Lib.Sequence.eq_intro #u8 #64 $to_hash ( + concat $randomness ${public_key}.f_public_key_hash)"); let hashed = Hasher::G(&to_hash); let (shared_secret, pseudorandomness) = hashed.split_at(SHARED_SECRET_SIZE); @@ -657,6 +811,28 @@ pub(crate) mod unpacked { // Decapsulate with Unpacked Private Key #[inline(always)] + #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning --z3refresh")] + #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\ + $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ + $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ + $ETA2 == Spec.MLKEM.v_ETA2 $K /\\ + $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\ + $C1_SIZE == Spec.MLKEM.v_C1_SIZE $K /\\ + $C2_SIZE == Spec.MLKEM.v_C2_SIZE $K /\\ + $VECTOR_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\ + $VECTOR_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\ + $C1_BLOCK_SIZE == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\ + $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\ + $IMPLICIT_REJECTION_HASH_INPUT_SIZE == Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE $K"))] + #[hax_lib::ensures(|result| + fstar!("$result == + Spec.MLKEM.ind_cca_unpack_decapsulate $K ${key_pair}.f_public_key.f_public_key_hash + ${key_pair}.f_private_key.f_implicit_rejection_value + ${ciphertext}.f_value + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${key_pair}.f_private_key.f_ind_cpa_private_key.f_secret_as_ntt) + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt) + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${key_pair}.f_public_key.f_ind_cpa_public_key.f_A)")) + ] pub(crate) fn decapsulate< const K: usize, const SECRET_KEY_SIZE: usize, @@ -680,6 +856,11 @@ pub(crate) mod unpacked { key_pair: &MlKemKeyPairUnpacked, ciphertext: &MlKemCiphertext, ) -> MlKemSharedSecret { + hax_lib::fstar!("assert (v $IMPLICIT_REJECTION_HASH_INPUT_SIZE == 32 + v (Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K)); + assert (v (Spec.MLKEM.v_C1_SIZE $K +! Spec.MLKEM.v_C2_SIZE $K) == v (Spec.MLKEM.v_C1_SIZE $K) + v (Spec.MLKEM.v_C2_SIZE $K)); + assert (v (Spec.MLKEM.v_C1_SIZE $K) == v (Spec.MLKEM.v_C1_BLOCK_SIZE $K) * v $K); + assert (v (Spec.MLKEM.v_C1_BLOCK_SIZE $K) == 32 * v (Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K)); + assert (v (Spec.MLKEM.v_C2_SIZE $K) == 32 * v (Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K))"); let decrypted = crate::ind_cpa::decrypt_unpacked::< K, CIPHERTEXT_SIZE, @@ -690,14 +871,20 @@ pub(crate) mod unpacked { >(&key_pair.private_key.ind_cpa_private_key, &ciphertext.value); let mut to_hash: [u8; SHARED_SECRET_SIZE + H_DIGEST_SIZE] = into_padded_array(&decrypted); + hax_lib::fstar!("Lib.Sequence.eq_intro #u8 #32 (Seq.slice $to_hash 0 32) $decrypted"); to_hash[SHARED_SECRET_SIZE..].copy_from_slice(&key_pair.public_key.public_key_hash); + hax_lib::fstar!("Lib.Sequence.lemma_concat2 32 $decrypted 32 ${key_pair}.f_public_key.f_public_key_hash $to_hash"); let hashed = Hasher::G(&to_hash); let (shared_secret, pseudorandomness) = hashed.split_at(SHARED_SECRET_SIZE); let mut to_hash: [u8; IMPLICIT_REJECTION_HASH_INPUT_SIZE] = into_padded_array(&key_pair.private_key.implicit_rejection_value); + hax_lib::fstar!("Lib.Sequence.eq_intro #u8 #32 + (Seq.slice $to_hash 0 32) ${key_pair}.f_private_key.f_implicit_rejection_value"); to_hash[SHARED_SECRET_SIZE..].copy_from_slice(ciphertext.as_ref()); + hax_lib::fstar!("Lib.Sequence.lemma_concat2 32 ${key_pair}.f_private_key.f_implicit_rejection_value + (v (Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K)) ${ciphertext}.f_value $to_hash"); let implicit_rejection_shared_secret: [u8; SHARED_SECRET_SIZE] = Hasher::PRF(&to_hash); let expected_ciphertext = crate::ind_cpa::encrypt_unpacked::< diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index 7f6bb9c1d..4891caff8 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -357,14 +357,16 @@ fn sample_vector_cbd_then_ntt_out< /// The NIST FIPS 203 standard can be found at /// . #[allow(non_snake_case)] +#[hax_lib::fstar::options("--z3rlimit 500 --ext context_pruning --z3refresh")] #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\ $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\ $ETA1 == Spec.MLKEM.v_ETA1 $K /\\ length $key_generation_seed == Spec.MLKEM.v_CPA_KEY_GENERATION_SEED_SIZE"))] -#[hax_lib::ensures(|_| fstar!("let (((t_as_ntt,seed_for_A), secret_as_ntt), valid) = Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in - (valid ==> ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}_future.f_t_as_ntt) == t_as_ntt) /\\ +#[hax_lib::ensures(|_| fstar!("let ((((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid) = Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in + (valid ==> (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}_future.f_t_as_ntt == t_as_ntt) /\\ (${public_key}_future.f_seed_for_A == seed_for_A) /\\ - ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${private_key}_future.f_secret_as_ntt) == secret_as_ntt)) /\\ + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}_future.f_A == matrix_A_as_ntt) /\\ + (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${private_key}_future.f_secret_as_ntt == secret_as_ntt)) /\\ (forall (i:nat). i < v $K ==> Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${private_key}_future.f_secret_as_ntt i)) /\\ (forall (i:nat). i < v $K ==> @@ -417,11 +419,12 @@ pub(crate) fn generate_keypair_unpacked< public_key.seed_for_A = seed_for_A.try_into().unwrap(); - hax_lib::fstar!("let ((t_as_ntt, seed_for_A), secret_as_ntt), valid = + hax_lib::fstar!("let (((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid = Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in assert (valid ==> ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector public_key.f_t_as_ntt) == t_as_ntt) /\\ (public_key.f_seed_for_A == seed_for_A) /\\ + (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector public_key.f_A == matrix_A_as_ntt) /\\ ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector private_key.f_secret_as_ntt) == secret_as_ntt)); assert ((forall (i: nat). i < v $K ==>