diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt index dc4e2de87..7599cb2f1 100644 --- a/libcrux-ml-kem/c/code_gen.txt +++ b/libcrux-ml-kem/c/code_gen.txt @@ -2,5 +2,5 @@ This code was generated with the following revisions: Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 -F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd -Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 +F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 +Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h index 159a636f7..31a212a7c 100644 --- a/libcrux-ml-kem/c/internal/libcrux_core.h +++ b/libcrux-ml-kem/c/internal/libcrux_core.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __internal_libcrux_core_H diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h index 4e09fe0de..c4c213b73 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __internal_libcrux_mlkem_avx2_H diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h index e94b99f4e..def86cf8e 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __internal_libcrux_mlkem_portable_H diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h index 01f450745..95df92565 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __internal_libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h index bf6cd4dc8..a57bfa85c 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __internal_libcrux_sha3_internal_H diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c index d429ee70b..bad4aa323 100644 --- a/libcrux-ml-kem/c/libcrux_core.c +++ b/libcrux-ml-kem/c/libcrux_core.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "internal/libcrux_core.h" diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h index 53e88573a..bc1f587a2 100644 --- a/libcrux-ml-kem/c/libcrux_core.h +++ b/libcrux-ml-kem/c/libcrux_core.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_core_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h index 2dd639ec9..63a7ab056 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem1024_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c index 3fca09119..1028b5ac1 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_mlkem1024_avx2.h" @@ -35,7 +35,7 @@ with const generics - ETA2_RANDOMNESS_SIZE= 128 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1600 */ -static void decapsulate_510( +static void decapsulate_0c0( libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key, libcrux_ml_kem_types_MlKemCiphertext_1f *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_7f0(private_key, ciphertext, ret); @@ -51,7 +51,7 @@ static void decapsulate_510( void libcrux_ml_kem_mlkem1024_avx2_decapsulate( libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key, libcrux_ml_kem_types_MlKemCiphertext_1f *ciphertext, uint8_t ret[32U]) { - decapsulate_510(private_key, ciphertext, ret); + decapsulate_0c0(private_key, ciphertext, ret); } /** @@ -71,7 +71,7 @@ with const generics - ETA2= 2 - ETA2_RANDOMNESS_SIZE= 128 */ -static tuple_21 encapsulate_d10( +static tuple_21 encapsulate_ae0( libcrux_ml_kem_types_MlKemPublicKey_1f *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_1f *uu____0 = public_key; @@ -95,7 +95,7 @@ tuple_21 libcrux_ml_kem_mlkem1024_avx2_encapsulate( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[32U]; memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t)); - return encapsulate_d10(uu____0, copy_of_randomness); + return encapsulate_ae0(uu____0, copy_of_randomness); } /** @@ -109,7 +109,7 @@ libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics - ETA1= 2 - ETA1_RANDOMNESS_SIZE= 128 */ -static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair generate_keypair_b80( +static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair generate_keypair_5a0( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -125,7 +125,7 @@ libcrux_ml_kem_mlkem1024_avx2_generate_key_pair(uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t)); - return generate_keypair_b80(copy_of_randomness); + return generate_keypair_5a0(copy_of_randomness); } /** @@ -136,7 +136,7 @@ generics - SECRET_KEY_SIZE= 3168 - CIPHERTEXT_SIZE= 1568 */ -static KRML_MUSTINLINE bool validate_private_key_650( +static KRML_MUSTINLINE bool validate_private_key_080( libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key, libcrux_ml_kem_types_MlKemCiphertext_1f *ciphertext) { return libcrux_ml_kem_ind_cca_validate_private_key_700(private_key, @@ -151,7 +151,7 @@ static KRML_MUSTINLINE bool validate_private_key_650( bool libcrux_ml_kem_mlkem1024_avx2_validate_private_key( libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key, libcrux_ml_kem_types_MlKemCiphertext_1f *ciphertext) { - return validate_private_key_650(private_key, ciphertext); + return validate_private_key_080(private_key, ciphertext); } /** @@ -162,7 +162,7 @@ generics - RANKED_BYTES_PER_RING_ELEMENT= 1536 - PUBLIC_KEY_SIZE= 1568 */ -static KRML_MUSTINLINE bool validate_public_key_3e0(uint8_t *public_key) { +static KRML_MUSTINLINE bool validate_public_key_f60(uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_520(public_key); } @@ -173,5 +173,5 @@ static KRML_MUSTINLINE bool validate_public_key_3e0(uint8_t *public_key) { */ bool libcrux_ml_kem_mlkem1024_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_1f *public_key) { - return validate_public_key_3e0(public_key->value); + return validate_public_key_f60(public_key->value); } diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h index ae31b1f2d..dede724bf 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem1024_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c index f4fbc294f..bed205e56 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_mlkem1024_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h index 1ab4a88d8..87b018021 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem1024_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h index ca35791e9..157226146 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem512_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c index ca848abb4..8008c0304 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_mlkem512_avx2.h" @@ -35,7 +35,7 @@ with const generics - ETA2_RANDOMNESS_SIZE= 128 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 800 */ -static void decapsulate_51(libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, +static void decapsulate_0c(libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, libcrux_ml_kem_types_MlKemCiphertext_e8 *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_7f(private_key, ciphertext, ret); @@ -51,7 +51,7 @@ static void decapsulate_51(libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, void libcrux_ml_kem_mlkem512_avx2_decapsulate( libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, libcrux_ml_kem_types_MlKemCiphertext_e8 *ciphertext, uint8_t ret[32U]) { - decapsulate_51(private_key, ciphertext, ret); + decapsulate_0c(private_key, ciphertext, ret); } /** @@ -71,7 +71,7 @@ with const generics - ETA2= 2 - ETA2_RANDOMNESS_SIZE= 128 */ -static tuple_ec encapsulate_d1( +static tuple_ec encapsulate_ae( libcrux_ml_kem_types_MlKemPublicKey_be *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_be *uu____0 = public_key; @@ -95,7 +95,7 @@ tuple_ec libcrux_ml_kem_mlkem512_avx2_encapsulate( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[32U]; memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t)); - return encapsulate_d1(uu____0, copy_of_randomness); + return encapsulate_ae(uu____0, copy_of_randomness); } /** @@ -109,7 +109,7 @@ libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics - ETA1= 3 - ETA1_RANDOMNESS_SIZE= 192 */ -static libcrux_ml_kem_types_MlKemKeyPair_cb generate_keypair_b8( +static libcrux_ml_kem_types_MlKemKeyPair_cb generate_keypair_5a( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -125,7 +125,7 @@ libcrux_ml_kem_mlkem512_avx2_generate_key_pair(uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t)); - return generate_keypair_b8(copy_of_randomness); + return generate_keypair_5a(copy_of_randomness); } /** @@ -136,7 +136,7 @@ generics - SECRET_KEY_SIZE= 1632 - CIPHERTEXT_SIZE= 768 */ -static KRML_MUSTINLINE bool validate_private_key_65( +static KRML_MUSTINLINE bool validate_private_key_08( libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, libcrux_ml_kem_types_MlKemCiphertext_e8 *ciphertext) { return libcrux_ml_kem_ind_cca_validate_private_key_70(private_key, @@ -151,7 +151,7 @@ static KRML_MUSTINLINE bool validate_private_key_65( bool libcrux_ml_kem_mlkem512_avx2_validate_private_key( libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, libcrux_ml_kem_types_MlKemCiphertext_e8 *ciphertext) { - return validate_private_key_65(private_key, ciphertext); + return validate_private_key_08(private_key, ciphertext); } /** @@ -162,7 +162,7 @@ generics - RANKED_BYTES_PER_RING_ELEMENT= 768 - PUBLIC_KEY_SIZE= 800 */ -static KRML_MUSTINLINE bool validate_public_key_3e(uint8_t *public_key) { +static KRML_MUSTINLINE bool validate_public_key_f6(uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_52(public_key); } @@ -173,5 +173,5 @@ static KRML_MUSTINLINE bool validate_public_key_3e(uint8_t *public_key) { */ bool libcrux_ml_kem_mlkem512_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_be *public_key) { - return validate_public_key_3e(public_key->value); + return validate_public_key_f6(public_key->value); } diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h index d116b682f..8a66b75c4 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem512_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c index cd3750a98..2fc5a3251 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_mlkem512_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h index 594ed03d2..66032c07f 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem512_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h index 0556cf23a..85985206f 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem768_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c index 4975abb16..3fd65a30d 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_mlkem768_avx2.h" @@ -35,7 +35,7 @@ with const generics - ETA2_RANDOMNESS_SIZE= 128 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1120 */ -static void decapsulate_511( +static void decapsulate_0c1( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_7f1(private_key, ciphertext, ret); @@ -51,7 +51,7 @@ static void decapsulate_511( void libcrux_ml_kem_mlkem768_avx2_decapsulate( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { - decapsulate_511(private_key, ciphertext, ret); + decapsulate_0c1(private_key, ciphertext, ret); } /** @@ -71,7 +71,7 @@ with const generics - ETA2= 2 - ETA2_RANDOMNESS_SIZE= 128 */ -static tuple_3c encapsulate_d11( +static tuple_3c encapsulate_ae1( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key; @@ -95,7 +95,7 @@ tuple_3c libcrux_ml_kem_mlkem768_avx2_encapsulate( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[32U]; memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t)); - return encapsulate_d11(uu____0, copy_of_randomness); + return encapsulate_ae1(uu____0, copy_of_randomness); } /** @@ -109,7 +109,7 @@ libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics - ETA1= 2 - ETA1_RANDOMNESS_SIZE= 128 */ -static libcrux_ml_kem_mlkem768_MlKem768KeyPair generate_keypair_b81( +static libcrux_ml_kem_mlkem768_MlKem768KeyPair generate_keypair_5a1( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -125,7 +125,7 @@ libcrux_ml_kem_mlkem768_avx2_generate_key_pair(uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t)); - return generate_keypair_b81(copy_of_randomness); + return generate_keypair_5a1(copy_of_randomness); } /** @@ -136,7 +136,7 @@ generics - SECRET_KEY_SIZE= 2400 - CIPHERTEXT_SIZE= 1088 */ -static KRML_MUSTINLINE bool validate_private_key_651( +static KRML_MUSTINLINE bool validate_private_key_081( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext) { return libcrux_ml_kem_ind_cca_validate_private_key_701(private_key, @@ -151,7 +151,7 @@ static KRML_MUSTINLINE bool validate_private_key_651( bool libcrux_ml_kem_mlkem768_avx2_validate_private_key( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext) { - return validate_private_key_651(private_key, ciphertext); + return validate_private_key_081(private_key, ciphertext); } /** @@ -162,7 +162,7 @@ generics - RANKED_BYTES_PER_RING_ELEMENT= 1152 - PUBLIC_KEY_SIZE= 1184 */ -static KRML_MUSTINLINE bool validate_public_key_3e1(uint8_t *public_key) { +static KRML_MUSTINLINE bool validate_public_key_f61(uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_521(public_key); } @@ -173,5 +173,5 @@ static KRML_MUSTINLINE bool validate_public_key_3e1(uint8_t *public_key) { */ bool libcrux_ml_kem_mlkem768_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key) { - return validate_public_key_3e1(public_key->value); + return validate_public_key_f61(public_key->value); } diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h index 25e02719b..af5edca86 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem768_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c index ac4156303..1794e74b4 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_mlkem768_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h index 2ac8e4939..4e8116617 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem768_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c index b89434a12..05520bf99 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "internal/libcrux_mlkem_avx2.h" @@ -164,7 +164,8 @@ libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(__m256i vector) { __m256i t0 = mm256_mulhi_epi16( vector, mm256_set1_epi16( LIBCRUX_ML_KEM_VECTOR_AVX2_ARITHMETIC_BARRETT_MULTIPLIER)); - __m256i t1 = mm256_add_epi16(t0, mm256_set1_epi16((int16_t)512)); + __m256i t512 = mm256_set1_epi16((int16_t)512); + __m256i t1 = mm256_add_epi16(t0, t512); __m256i quotient = mm256_srai_epi16((int32_t)10, t1, __m256i); __m256i quotient_times_field_modulus = mm256_mullo_epi16( quotient, mm256_set1_epi16(LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS)); @@ -522,8 +523,8 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_1( __m128i high_msbs = mm256_extracti128_si256((int32_t)1, lsb_to_msb, __m128i); __m128i msbs = mm_packs_epi16(low_msbs, high_msbs); int32_t bits_packed = mm_movemask_epi8(msbs); - ret[0U] = (uint8_t)bits_packed; - ret[1U] = (uint8_t)(bits_packed >> 8U); + uint8_t result[2U] = {(uint8_t)bits_packed, (uint8_t)(bits_packed >> 8U)}; + memcpy(ret, result, (size_t)2U * sizeof(uint8_t)); } /** @@ -536,34 +537,35 @@ void libcrux_ml_kem_vector_avx2_serialize_1_09(__m256i vector, } KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) { - __m256i coefficients = mm256_set_epi16( - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)); - __m256i shift_lsb_to_msb = mm256_set_epi16( - (int16_t)1 << 8U, (int16_t)1 << 9U, (int16_t)1 << 10U, (int16_t)1 << 11U, - (int16_t)1 << 12U, (int16_t)1 << 13U, (int16_t)1 << 14U, (int16_t)-32768, - (int16_t)1 << 8U, (int16_t)1 << 9U, (int16_t)1 << 10U, (int16_t)1 << 11U, - (int16_t)1 << 12U, (int16_t)1 << 13U, (int16_t)1 << 14U, (int16_t)-32768); - __m256i coefficients_in_msb = - mm256_mullo_epi16(coefficients, shift_lsb_to_msb); +libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_i16s( + int16_t a, int16_t b) { + __m256i coefficients = + mm256_set_epi16(b, b, b, b, b, b, b, b, a, a, a, a, a, a, a, a); + __m256i coefficients_in_msb = mm256_mullo_epi16( + coefficients, + mm256_set_epi16((int16_t)1 << 8U, (int16_t)1 << 9U, (int16_t)1 << 10U, + (int16_t)1 << 11U, (int16_t)1 << 12U, (int16_t)1 << 13U, + (int16_t)1 << 14U, (int16_t)-32768, (int16_t)1 << 8U, + (int16_t)1 << 9U, (int16_t)1 << 10U, (int16_t)1 << 11U, + (int16_t)1 << 12U, (int16_t)1 << 13U, (int16_t)1 << 14U, + (int16_t)-32768)); return mm256_srli_epi16((int32_t)15, coefficients_in_msb, __m256i); } +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_u8s( + uint8_t a, uint8_t b) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_i16s( + (int16_t)a, (int16_t)b); +} + +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_u8s( + Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *)); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -572,15 +574,27 @@ __m256i libcrux_ml_kem_vector_avx2_deserialize_1_09(Eurydice_slice bytes) { return libcrux_ml_kem_vector_avx2_serialize_deserialize_1(bytes); } +/** + `mm256_concat_pairs_n(n, x)` is then a sequence of 32 bits packets + of the shape `0b0…0b₁…bₙa₁…aₙ`, if `x` is a sequence of pairs of + 16 bits, of the shape `(0b0…0a₁…aₙ, 0b0…0b₁…bₙ)` (where the last + `n` bits are non-zero). +*/ +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(uint8_t n, + __m256i x) { + int16_t n0 = (int16_t)1 << (uint32_t)n; + return mm256_madd_epi16( + x, mm256_set_epi16(n0, (int16_t)1, n0, (int16_t)1, n0, (int16_t)1, n0, + (int16_t)1, n0, (int16_t)1, n0, (int16_t)1, n0, + (int16_t)1, n0, (int16_t)1)); +} + KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_4( __m256i vector, uint8_t ret[8U]) { uint8_t serialized[16U] = {0U}; - __m256i adjacent_2_combined = mm256_madd_epi16( - vector, mm256_set_epi16( - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1, - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1, - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1, - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1)); + __m256i adjacent_2_combined = + libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(4U, vector); __m256i adjacent_8_combined = mm256_shuffle_epi8( adjacent_2_combined, mm256_set_epi8((int8_t)-1, (int8_t)-1, (int8_t)-1, (int8_t)-1, (int8_t)-1, @@ -617,37 +631,47 @@ void libcrux_ml_kem_vector_avx2_serialize_4_09(__m256i vector, } KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) { - __m256i coefficients = mm256_set_epi16( - (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)); - __m256i shift_lsbs_to_msbs = mm256_set_epi16( - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U); - __m256i coefficients_in_msb = - mm256_mullo_epi16(coefficients, shift_lsbs_to_msbs); +libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_i16s( + int16_t b0, int16_t b1, int16_t b2, int16_t b3, int16_t b4, int16_t b5, + int16_t b6, int16_t b7) { + __m256i coefficients = mm256_set_epi16(b7, b7, b6, b6, b5, b5, b4, b4, b3, b3, + b2, b2, b1, b1, b0, b0); + __m256i coefficients_in_msb = mm256_mullo_epi16( + coefficients, + mm256_set_epi16((int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U)); __m256i coefficients_in_lsb = mm256_srli_epi16((int32_t)4, coefficients_in_msb, __m256i); return mm256_and_si256(coefficients_in_lsb, mm256_set1_epi16(((int16_t)1 << 4U) - (int16_t)1)); } +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_u8s( + uint8_t b0, uint8_t b1, uint8_t b2, uint8_t b3, uint8_t b4, uint8_t b5, + uint8_t b6, uint8_t b7) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_i16s( + (int16_t)b0, (int16_t)b1, (int16_t)b2, (int16_t)b3, (int16_t)b4, + (int16_t)b5, (int16_t)b6, (int16_t)b7); +} + +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_u8s( + Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *)); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -707,6 +731,22 @@ void libcrux_ml_kem_vector_avx2_serialize_5_09(__m256i vector, libcrux_ml_kem_vector_avx2_serialize_serialize_5(vector, ret); } +/** + We cannot model `mm256_inserti128_si256` on its own: it produces a + Vec256 where the upper 128 bits are undefined. Thus + `mm256_inserti128_si256` is not pure. + + Luckily, we always call `mm256_castsi128_si256` right after + `mm256_inserti128_si256`: this composition sets the upper bits, + making the whole computation pure again. +*/ +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128(__m128i lower, + __m128i upper) { + return mm256_inserti128_si256((int32_t)1, mm256_castsi128_si256(lower), upper, + __m256i); +} + KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) { __m128i coefficients = @@ -726,11 +766,11 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) { Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)); - __m256i coefficients_loaded = mm256_castsi128_si256(coefficients); - __m256i coefficients_loaded0 = mm256_inserti128_si256( - (int32_t)1, coefficients_loaded, coefficients, __m256i); + __m256i coefficients_loaded = + libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + coefficients, coefficients); __m256i coefficients0 = mm256_shuffle_epi8( - coefficients_loaded0, + coefficients_loaded, mm256_set_epi8((int8_t)15, (int8_t)14, (int8_t)15, (int8_t)14, (int8_t)13, (int8_t)12, (int8_t)13, (int8_t)12, (int8_t)11, (int8_t)10, (int8_t)11, (int8_t)10, (int8_t)9, (int8_t)8, (int8_t)9, @@ -757,16 +797,11 @@ __m256i libcrux_ml_kem_vector_avx2_deserialize_5_09(Eurydice_slice bytes) { return libcrux_ml_kem_vector_avx2_serialize_deserialize_5(bytes); } -KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( - __m256i vector, uint8_t ret[20U]) { - uint8_t serialized[32U] = {0U}; - __m256i adjacent_2_combined = mm256_madd_epi16( - vector, mm256_set_epi16((int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, - (int16_t)1, (int16_t)1 << 10U, (int16_t)1, - (int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, - (int16_t)1, (int16_t)1 << 10U, (int16_t)1, - (int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, - (int16_t)1)); +core_core_arch_x86___m128i_x2 +libcrux_ml_kem_vector_avx2_serialize_serialize_10_serialize_10_vec( + __m256i vector) { + __m256i adjacent_2_combined = + libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(10U, vector); __m256i adjacent_4_combined = mm256_sllv_epi32( adjacent_2_combined, mm256_set_epi32((int32_t)0, (int32_t)12, (int32_t)0, (int32_t)12, @@ -783,11 +818,23 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( (int8_t)9, (int8_t)8, (int8_t)4, (int8_t)3, (int8_t)2, (int8_t)1, (int8_t)0)); __m128i lower_8 = mm256_castsi256_si128(adjacent_8_combined); + __m128i upper_8 = + mm256_extracti128_si256((int32_t)1, adjacent_8_combined, __m128i); + return ( + CLITERAL(core_core_arch_x86___m128i_x2){.fst = lower_8, .snd = upper_8}); +} + +KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( + __m256i vector, uint8_t ret[20U]) { + core_core_arch_x86___m128i_x2 uu____0 = + libcrux_ml_kem_vector_avx2_serialize_serialize_10_serialize_10_vec( + vector); + __m128i lower_8 = uu____0.fst; + __m128i upper_8 = uu____0.snd; + uint8_t serialized[32U] = {0U}; mm_storeu_bytes_si128( Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)16U, uint8_t), lower_8); - __m128i upper_8 = - mm256_extracti128_si256((int32_t)1, adjacent_8_combined, __m128i); mm_storeu_bytes_si128(Eurydice_array_to_subslice2(serialized, (size_t)10U, (size_t)26U, uint8_t), upper_8); @@ -811,31 +858,40 @@ void libcrux_ml_kem_vector_avx2_serialize_10_09(__m256i vector, } KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) { - __m256i shift_lsbs_to_msbs = mm256_set_epi16( - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U); - __m128i lower_coefficients = mm_loadu_si128( - Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t)); - __m128i lower_coefficients0 = mm_shuffle_epi8( - lower_coefficients, mm_set_epi8(9U, 8U, 8U, 7U, 7U, 6U, 6U, 5U, 4U, 3U, - 3U, 2U, 2U, 1U, 1U, 0U)); - __m128i upper_coefficients = mm_loadu_si128( - Eurydice_slice_subslice2(bytes, (size_t)4U, (size_t)20U, uint8_t)); - __m128i upper_coefficients0 = mm_shuffle_epi8( - upper_coefficients, mm_set_epi8(15U, 14U, 14U, 13U, 13U, 12U, 12U, 11U, - 10U, 9U, 9U, 8U, 8U, 7U, 7U, 6U)); - __m256i coefficients = mm256_castsi128_si256(lower_coefficients0); - __m256i coefficients0 = mm256_inserti128_si256((int32_t)1, coefficients, - upper_coefficients0, __m256i); - __m256i coefficients1 = mm256_mullo_epi16(coefficients0, shift_lsbs_to_msbs); - __m256i coefficients2 = mm256_srli_epi16((int32_t)6, coefficients1, __m256i); - return mm256_and_si256(coefficients2, +libcrux_ml_kem_vector_avx2_serialize_deserialize_10_deserialize_10_vec( + __m128i lower_coefficients0, __m128i upper_coefficients0) { + __m128i lower_coefficients = mm_shuffle_epi8( + lower_coefficients0, mm_set_epi8(9U, 8U, 8U, 7U, 7U, 6U, 6U, 5U, 4U, 3U, + 3U, 2U, 2U, 1U, 1U, 0U)); + __m128i upper_coefficients = mm_shuffle_epi8( + upper_coefficients0, mm_set_epi8(15U, 14U, 14U, 13U, 13U, 12U, 12U, 11U, + 10U, 9U, 9U, 8U, 8U, 7U, 7U, 6U)); + __m256i coefficients = + libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + lower_coefficients, upper_coefficients); + __m256i coefficients0 = mm256_mullo_epi16( + coefficients, + mm256_set_epi16((int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, + (int16_t)1 << 6U, (int16_t)1 << 0U, (int16_t)1 << 2U, + (int16_t)1 << 4U, (int16_t)1 << 6U, (int16_t)1 << 0U, + (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, + (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, + (int16_t)1 << 6U)); + __m256i coefficients1 = mm256_srli_epi16((int32_t)6, coefficients0, __m256i); + return mm256_and_si256(coefficients1, mm256_set1_epi16(((int16_t)1 << 10U) - (int16_t)1)); } +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) { + Eurydice_slice lower_coefficients = + Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t); + Eurydice_slice upper_coefficients = + Eurydice_slice_subslice2(bytes, (size_t)4U, (size_t)20U, uint8_t); + return libcrux_ml_kem_vector_avx2_serialize_deserialize_10_deserialize_10_vec( + mm_loadu_si128(lower_coefficients), mm_loadu_si128(upper_coefficients)); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -884,16 +940,11 @@ __m256i libcrux_ml_kem_vector_avx2_deserialize_11_09(Eurydice_slice bytes) { return libcrux_ml_kem_vector_avx2_serialize_deserialize_11(bytes); } -KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( - __m256i vector, uint8_t ret[24U]) { - uint8_t serialized[32U] = {0U}; - __m256i adjacent_2_combined = mm256_madd_epi16( - vector, mm256_set_epi16((int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, - (int16_t)1, (int16_t)1 << 12U, (int16_t)1, - (int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, - (int16_t)1, (int16_t)1 << 12U, (int16_t)1, - (int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, - (int16_t)1)); +KRML_MUSTINLINE core_core_arch_x86___m128i_x2 +libcrux_ml_kem_vector_avx2_serialize_serialize_12_serialize_12_vec( + __m256i vector) { + __m256i adjacent_2_combined = + libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(12U, vector); __m256i adjacent_4_combined = mm256_sllv_epi32( adjacent_2_combined, mm256_set_epi32((int32_t)0, (int32_t)8, (int32_t)0, (int32_t)8, @@ -912,6 +963,18 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( __m128i lower_8 = mm256_castsi256_si128(adjacent_8_combined); __m128i upper_8 = mm256_extracti128_si256((int32_t)1, adjacent_8_combined, __m128i); + return ( + CLITERAL(core_core_arch_x86___m128i_x2){.fst = lower_8, .snd = upper_8}); +} + +KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( + __m256i vector, uint8_t ret[24U]) { + uint8_t serialized[32U] = {0U}; + core_core_arch_x86___m128i_x2 uu____0 = + libcrux_ml_kem_vector_avx2_serialize_serialize_12_serialize_12_vec( + vector); + __m128i lower_8 = uu____0.fst; + __m128i upper_8 = uu____0.snd; mm_storeu_bytes_si128( Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)16U, uint8_t), lower_8); @@ -937,30 +1000,39 @@ void libcrux_ml_kem_vector_avx2_serialize_12_09(__m256i vector, libcrux_ml_kem_vector_avx2_serialize_serialize_12(vector, ret); } +KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_12_deserialize_12_vec( + __m128i lower_coefficients0, __m128i upper_coefficients0) { + __m128i lower_coefficients = mm_shuffle_epi8( + lower_coefficients0, mm_set_epi8(11U, 10U, 10U, 9U, 8U, 7U, 7U, 6U, 5U, + 4U, 4U, 3U, 2U, 1U, 1U, 0U)); + __m128i upper_coefficients = mm_shuffle_epi8( + upper_coefficients0, mm_set_epi8(15U, 14U, 14U, 13U, 12U, 11U, 11U, 10U, + 9U, 8U, 8U, 7U, 6U, 5U, 5U, 4U)); + __m256i coefficients = + libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + lower_coefficients, upper_coefficients); + __m256i coefficients0 = mm256_mullo_epi16( + coefficients, + mm256_set_epi16((int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U)); + __m256i coefficients1 = mm256_srli_epi16((int32_t)4, coefficients0, __m256i); + return mm256_and_si256(coefficients1, + mm256_set1_epi16(((int16_t)1 << 12U) - (int16_t)1)); +} + KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_12(Eurydice_slice bytes) { - __m256i shift_lsbs_to_msbs = mm256_set_epi16( - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U); __m128i lower_coefficients = mm_loadu_si128( Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t)); - __m128i lower_coefficients0 = mm_shuffle_epi8( - lower_coefficients, mm_set_epi8(11U, 10U, 10U, 9U, 8U, 7U, 7U, 6U, 5U, 4U, - 4U, 3U, 2U, 1U, 1U, 0U)); __m128i upper_coefficients = mm_loadu_si128( Eurydice_slice_subslice2(bytes, (size_t)8U, (size_t)24U, uint8_t)); - __m128i upper_coefficients0 = mm_shuffle_epi8( - upper_coefficients, mm_set_epi8(15U, 14U, 14U, 13U, 12U, 11U, 11U, 10U, - 9U, 8U, 8U, 7U, 6U, 5U, 5U, 4U)); - __m256i coefficients = mm256_castsi128_si256(lower_coefficients0); - __m256i coefficients0 = mm256_inserti128_si256((int32_t)1, coefficients, - upper_coefficients0, __m256i); - __m256i coefficients1 = mm256_mullo_epi16(coefficients0, shift_lsbs_to_msbs); - __m256i coefficients2 = mm256_srli_epi16((int32_t)4, coefficients1, __m256i); - return mm256_and_si256(coefficients2, - mm256_set1_epi16(((int16_t)1 << 12U) - (int16_t)1)); + return libcrux_ml_kem_vector_avx2_serialize_deserialize_12_deserialize_12_vec( + lower_coefficients, upper_coefficients); } /** @@ -2952,7 +3024,7 @@ generics - COEFFICIENT_BITS= 10 */ static KRML_MUSTINLINE __m256i -compress_ciphertext_coefficient_43(__m256i vector) { +compress_ciphertext_coefficient_1a(__m256i vector) { __m256i field_modulus_halved = mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / (int32_t)2); @@ -2999,8 +3071,8 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_09 with const generics - COEFFICIENT_BITS= 10 */ -static __m256i compress_09_76(__m256i vector) { - return compress_ciphertext_coefficient_43(vector); +static __m256i compress_09_74(__m256i vector) { + return compress_ciphertext_coefficient_1a(vector); } /** @@ -3016,7 +3088,7 @@ static KRML_MUSTINLINE void compress_then_serialize_10_2b0( i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; __m256i coefficient = - compress_09_76(to_unsigned_field_modulus_7b(re->coefficients[i0])); + compress_09_74(to_unsigned_field_modulus_7b(re->coefficients[i0])); uint8_t bytes[20U]; libcrux_ml_kem_vector_avx2_serialize_10_09(coefficient, bytes); Eurydice_slice uu____0 = Eurydice_array_to_subslice2( @@ -3036,7 +3108,7 @@ generics - COEFFICIENT_BITS= 11 */ static KRML_MUSTINLINE __m256i -compress_ciphertext_coefficient_430(__m256i vector) { +compress_ciphertext_coefficient_1a0(__m256i vector) { __m256i field_modulus_halved = mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / (int32_t)2); @@ -3083,8 +3155,8 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_09 with const generics - COEFFICIENT_BITS= 11 */ -static __m256i compress_09_760(__m256i vector) { - return compress_ciphertext_coefficient_430(vector); +static __m256i compress_09_740(__m256i vector) { + return compress_ciphertext_coefficient_1a0(vector); } /** @@ -3139,7 +3211,7 @@ generics - COEFFICIENT_BITS= 4 */ static KRML_MUSTINLINE __m256i -compress_ciphertext_coefficient_431(__m256i vector) { +compress_ciphertext_coefficient_1a1(__m256i vector) { __m256i field_modulus_halved = mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / (int32_t)2); @@ -3186,8 +3258,8 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_09 with const generics - COEFFICIENT_BITS= 4 */ -static __m256i compress_09_761(__m256i vector) { - return compress_ciphertext_coefficient_431(vector); +static __m256i compress_09_741(__m256i vector) { + return compress_ciphertext_coefficient_1a1(vector); } /** @@ -3203,7 +3275,7 @@ static KRML_MUSTINLINE void compress_then_serialize_4_a4( i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; __m256i coefficient = - compress_09_761(to_unsigned_field_modulus_7b(re.coefficients[i0])); + compress_09_741(to_unsigned_field_modulus_7b(re.coefficients[i0])); uint8_t bytes[8U]; libcrux_ml_kem_vector_avx2_serialize_4_09(coefficient, bytes); Eurydice_slice_copy( @@ -3220,7 +3292,7 @@ generics - COEFFICIENT_BITS= 5 */ static KRML_MUSTINLINE __m256i -compress_ciphertext_coefficient_432(__m256i vector) { +compress_ciphertext_coefficient_1a2(__m256i vector) { __m256i field_modulus_halved = mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / (int32_t)2); @@ -3267,8 +3339,8 @@ A monomorphic instance of libcrux_ml_kem.vector.avx2.compress_09 with const generics - COEFFICIENT_BITS= 5 */ -static __m256i compress_09_762(__m256i vector) { - return compress_ciphertext_coefficient_432(vector); +static __m256i compress_09_742(__m256i vector) { + return compress_ciphertext_coefficient_1a2(vector); } /** @@ -3284,7 +3356,7 @@ static KRML_MUSTINLINE void compress_then_serialize_5_03( i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; __m256i coefficients = - compress_09_762(to_unsigned_representative_3f(re.coefficients[i0])); + compress_09_742(to_unsigned_representative_3f(re.coefficients[i0])); uint8_t bytes[10U]; libcrux_ml_kem_vector_avx2_serialize_5_09(coefficients, bytes); Eurydice_slice_copy( @@ -3570,7 +3642,7 @@ generics - COEFFICIENT_BITS= 10 */ static KRML_MUSTINLINE __m256i -decompress_ciphertext_coefficient_79(__m256i vector) { +decompress_ciphertext_coefficient_8e(__m256i vector) { __m256i field_modulus = mm256_set1_epi32((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); __m256i two_pow_coefficient_bits = @@ -3614,8 +3686,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_09 with const generics - COEFFICIENT_BITS= 10 */ -static __m256i decompress_ciphertext_coefficient_09_c6(__m256i vector) { - return decompress_ciphertext_coefficient_79(vector); +static __m256i decompress_ciphertext_coefficient_09_70(__m256i vector) { + return decompress_ciphertext_coefficient_8e(vector); } /** @@ -3638,7 +3710,7 @@ deserialize_then_decompress_10_c7(Eurydice_slice serialized) { Eurydice_slice bytes = Eurydice_slice_subslice2( serialized, i0 * (size_t)20U, i0 * (size_t)20U + (size_t)20U, uint8_t); __m256i coefficient = libcrux_ml_kem_vector_avx2_deserialize_10_09(bytes); - re.coefficients[i0] = decompress_ciphertext_coefficient_09_c6(coefficient); + re.coefficients[i0] = decompress_ciphertext_coefficient_09_70(coefficient); } return re; } @@ -3650,7 +3722,7 @@ generics - COEFFICIENT_BITS= 11 */ static KRML_MUSTINLINE __m256i -decompress_ciphertext_coefficient_790(__m256i vector) { +decompress_ciphertext_coefficient_8e0(__m256i vector) { __m256i field_modulus = mm256_set1_epi32((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); __m256i two_pow_coefficient_bits = @@ -3694,8 +3766,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_09 with const generics - COEFFICIENT_BITS= 11 */ -static __m256i decompress_ciphertext_coefficient_09_c60(__m256i vector) { - return decompress_ciphertext_coefficient_790(vector); +static __m256i decompress_ciphertext_coefficient_09_700(__m256i vector) { + return decompress_ciphertext_coefficient_8e0(vector); } /** @@ -3713,7 +3785,7 @@ deserialize_then_decompress_11_d5(Eurydice_slice serialized) { Eurydice_slice bytes = Eurydice_slice_subslice2( serialized, i0 * (size_t)22U, i0 * (size_t)22U + (size_t)22U, uint8_t); __m256i coefficient = libcrux_ml_kem_vector_avx2_deserialize_11_09(bytes); - re.coefficients[i0] = decompress_ciphertext_coefficient_09_c60(coefficient); + re.coefficients[i0] = decompress_ciphertext_coefficient_09_700(coefficient); } return re; } @@ -3794,7 +3866,7 @@ generics - COEFFICIENT_BITS= 4 */ static KRML_MUSTINLINE __m256i -decompress_ciphertext_coefficient_791(__m256i vector) { +decompress_ciphertext_coefficient_8e1(__m256i vector) { __m256i field_modulus = mm256_set1_epi32((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); __m256i two_pow_coefficient_bits = @@ -3838,8 +3910,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_09 with const generics - COEFFICIENT_BITS= 4 */ -static __m256i decompress_ciphertext_coefficient_09_c61(__m256i vector) { - return decompress_ciphertext_coefficient_791(vector); +static __m256i decompress_ciphertext_coefficient_09_701(__m256i vector) { + return decompress_ciphertext_coefficient_8e1(vector); } /** @@ -3857,7 +3929,7 @@ deserialize_then_decompress_4_75(Eurydice_slice serialized) { Eurydice_slice bytes = Eurydice_slice_subslice2( serialized, i0 * (size_t)8U, i0 * (size_t)8U + (size_t)8U, uint8_t); __m256i coefficient = libcrux_ml_kem_vector_avx2_deserialize_4_09(bytes); - re.coefficients[i0] = decompress_ciphertext_coefficient_09_c61(coefficient); + re.coefficients[i0] = decompress_ciphertext_coefficient_09_701(coefficient); } return re; } @@ -3869,7 +3941,7 @@ generics - COEFFICIENT_BITS= 5 */ static KRML_MUSTINLINE __m256i -decompress_ciphertext_coefficient_792(__m256i vector) { +decompress_ciphertext_coefficient_8e2(__m256i vector) { __m256i field_modulus = mm256_set1_epi32((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); __m256i two_pow_coefficient_bits = @@ -3913,8 +3985,8 @@ libcrux_ml_kem.vector.avx2.decompress_ciphertext_coefficient_09 with const generics - COEFFICIENT_BITS= 5 */ -static __m256i decompress_ciphertext_coefficient_09_c62(__m256i vector) { - return decompress_ciphertext_coefficient_792(vector); +static __m256i decompress_ciphertext_coefficient_09_702(__m256i vector) { + return decompress_ciphertext_coefficient_8e2(vector); } /** @@ -3933,7 +4005,7 @@ deserialize_then_decompress_5_f8(Eurydice_slice serialized) { serialized, i0 * (size_t)10U, i0 * (size_t)10U + (size_t)10U, uint8_t); re.coefficients[i0] = libcrux_ml_kem_vector_avx2_deserialize_5_09(bytes); re.coefficients[i0] = - decompress_ciphertext_coefficient_09_c62(re.coefficients[i0]); + decompress_ciphertext_coefficient_09_702(re.coefficients[i0]); } return re; } @@ -5444,7 +5516,7 @@ static KRML_MUSTINLINE void compress_then_serialize_11_17( i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; __m256i coefficient = - compress_09_760(to_unsigned_representative_3f(re->coefficients[i0])); + compress_09_740(to_unsigned_representative_3f(re->coefficients[i0])); uint8_t bytes[22U]; libcrux_ml_kem_vector_avx2_serialize_11_09(coefficient, bytes); Eurydice_slice uu____0 = Eurydice_array_to_subslice2( diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h index 42cc1517c..02a4b1c04 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem_avx2_H @@ -234,6 +234,12 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} */ void libcrux_ml_kem_vector_avx2_serialize_1_09(__m256i vector, uint8_t ret[2U]); +__m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_i16s( + int16_t a, int16_t b); + +__m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_u8s( + uint8_t a, uint8_t b); + __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_1( Eurydice_slice bytes); @@ -243,6 +249,15 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} */ __m256i libcrux_ml_kem_vector_avx2_deserialize_1_09(Eurydice_slice bytes); +/** + `mm256_concat_pairs_n(n, x)` is then a sequence of 32 bits packets + of the shape `0b0…0b₁…bₙa₁…aₙ`, if `x` is a sequence of pairs of + 16 bits, of the shape `(0b0…0a₁…aₙ, 0b0…0b₁…bₙ)` (where the last + `n` bits are non-zero). +*/ +__m256i libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(uint8_t n, + __m256i x); + void libcrux_ml_kem_vector_avx2_serialize_serialize_4(__m256i vector, uint8_t ret[8U]); @@ -252,6 +267,14 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} */ void libcrux_ml_kem_vector_avx2_serialize_4_09(__m256i vector, uint8_t ret[8U]); +__m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_i16s( + int16_t b0, int16_t b1, int16_t b2, int16_t b3, int16_t b4, int16_t b5, + int16_t b6, int16_t b7); + +__m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_u8s( + uint8_t b0, uint8_t b1, uint8_t b2, uint8_t b3, uint8_t b4, uint8_t b5, + uint8_t b6, uint8_t b7); + __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_4( Eurydice_slice bytes); @@ -271,6 +294,18 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} void libcrux_ml_kem_vector_avx2_serialize_5_09(__m256i vector, uint8_t ret[10U]); +/** + We cannot model `mm256_inserti128_si256` on its own: it produces a + Vec256 where the upper 128 bits are undefined. Thus + `mm256_inserti128_si256` is not pure. + + Luckily, we always call `mm256_castsi128_si256` right after + `mm256_inserti128_si256`: this composition sets the upper bits, + making the whole computation pure again. +*/ +__m256i libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + __m128i lower, __m128i upper); + __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_5( Eurydice_slice bytes); @@ -280,6 +315,15 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} */ __m256i libcrux_ml_kem_vector_avx2_deserialize_5_09(Eurydice_slice bytes); +typedef struct core_core_arch_x86___m128i_x2_s { + __m128i fst; + __m128i snd; +} core_core_arch_x86___m128i_x2; + +core_core_arch_x86___m128i_x2 +libcrux_ml_kem_vector_avx2_serialize_serialize_10_serialize_10_vec( + __m256i vector); + void libcrux_ml_kem_vector_avx2_serialize_serialize_10(__m256i vector, uint8_t ret[20U]); @@ -290,6 +334,9 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} void libcrux_ml_kem_vector_avx2_serialize_10_09(__m256i vector, uint8_t ret[20U]); +__m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_10_deserialize_10_vec( + __m128i lower_coefficients0, __m128i upper_coefficients0); + __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_10( Eurydice_slice bytes); @@ -318,6 +365,10 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} */ __m256i libcrux_ml_kem_vector_avx2_deserialize_11_09(Eurydice_slice bytes); +core_core_arch_x86___m128i_x2 +libcrux_ml_kem_vector_avx2_serialize_serialize_12_serialize_12_vec( + __m256i vector); + void libcrux_ml_kem_vector_avx2_serialize_serialize_12(__m256i vector, uint8_t ret[24U]); @@ -328,6 +379,9 @@ libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} void libcrux_ml_kem_vector_avx2_serialize_12_09(__m256i vector, uint8_t ret[24U]); +__m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_12_deserialize_12_vec( + __m128i lower_coefficients0, __m128i upper_coefficients0); + __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_12( Eurydice_slice bytes); diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.c b/libcrux-ml-kem/c/libcrux_mlkem_portable.c index 9c539cfa1..25021f8c9 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "internal/libcrux_mlkem_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h index c9875da03..e36fc4ae2 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem_portable_H diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h index 6e2ab7015..09a7923b5 100644 --- a/libcrux-ml-kem/c/libcrux_sha3.h +++ b/libcrux-ml-kem/c/libcrux_sha3.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_sha3_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.c b/libcrux-ml-kem/c/libcrux_sha3_avx2.c index d854d460d..49d6623c3 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "internal/libcrux_sha3_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/libcrux_sha3_avx2.h index 7da61a71e..1e2e63c96 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_internal.h b/libcrux-ml-kem/c/libcrux_sha3_internal.h index 1e2de3251..5b4b70a94 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_sha3_internal_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.c b/libcrux-ml-kem/c/libcrux_sha3_neon.c index 5cf30d99e..d84fc7126 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.c +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #include "libcrux_sha3_neon.h" diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.h b/libcrux-ml-kem/c/libcrux_sha3_neon.h index 362ca6ad1..bdb6771ab 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.h +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_sha3_neon_H diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt index dc4e2de87..7599cb2f1 100644 --- a/libcrux-ml-kem/cg/code_gen.txt +++ b/libcrux-ml-kem/cg/code_gen.txt @@ -2,5 +2,5 @@ This code was generated with the following revisions: Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 -F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd -Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 +F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 +Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h index dcf4fd6fe..c6916acab 100644 --- a/libcrux-ml-kem/cg/libcrux_core.h +++ b/libcrux-ml-kem/cg/libcrux_core.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #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 898681bb4..2b5ee19c2 100644 --- a/libcrux-ml-kem/cg/libcrux_ct_ops.h +++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #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 053e1683b..553bb0252 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem768_avx2_H @@ -204,8 +204,8 @@ libcrux_ml_kem_vector_avx2_arithmetic_barrett_reduce(__m256i vector) { __m256i t0 = libcrux_intrinsics_avx2_mm256_mulhi_epi16( vector, libcrux_intrinsics_avx2_mm256_set1_epi16( LIBCRUX_ML_KEM_VECTOR_AVX2_ARITHMETIC_BARRETT_MULTIPLIER)); - __m256i t1 = libcrux_intrinsics_avx2_mm256_add_epi16( - t0, libcrux_intrinsics_avx2_mm256_set1_epi16((int16_t)512)); + __m256i t512 = libcrux_intrinsics_avx2_mm256_set1_epi16((int16_t)512); + __m256i t1 = libcrux_intrinsics_avx2_mm256_add_epi16(t0, t512); __m256i quotient = libcrux_intrinsics_avx2_mm256_srai_epi16((int32_t)10, t1, __m256i); __m256i quotient_times_field_modulus = @@ -636,8 +636,8 @@ static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_1( (int32_t)1, lsb_to_msb, __m128i); __m128i msbs = libcrux_intrinsics_avx2_mm_packs_epi16(low_msbs, high_msbs); int32_t bits_packed = libcrux_intrinsics_avx2_mm_movemask_epi8(msbs); - ret[0U] = (uint8_t)bits_packed; - ret[1U] = (uint8_t)(bits_packed >> 8U); + uint8_t result[2U] = {(uint8_t)bits_packed, (uint8_t)(bits_packed >> 8U)}; + memcpy(ret, result, (size_t)2U * sizeof(uint8_t)); } /** @@ -652,35 +652,38 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_1_09(__m256i vector, KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) { +libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_i16s( + int16_t a, int16_t b) { __m256i coefficients = libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)); - __m256i shift_lsb_to_msb = libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 8U, (int16_t)1 << 9U, (int16_t)1 << 10U, (int16_t)1 << 11U, - (int16_t)1 << 12U, (int16_t)1 << 13U, (int16_t)1 << 14U, (int16_t)-32768, - (int16_t)1 << 8U, (int16_t)1 << 9U, (int16_t)1 << 10U, (int16_t)1 << 11U, - (int16_t)1 << 12U, (int16_t)1 << 13U, (int16_t)1 << 14U, (int16_t)-32768); - __m256i coefficients_in_msb = - libcrux_intrinsics_avx2_mm256_mullo_epi16(coefficients, shift_lsb_to_msb); + b, b, b, b, b, b, b, b, a, a, a, a, a, a, a, a); + __m256i coefficients_in_msb = libcrux_intrinsics_avx2_mm256_mullo_epi16( + coefficients, libcrux_intrinsics_avx2_mm256_set_epi16( + (int16_t)1 << 8U, (int16_t)1 << 9U, (int16_t)1 << 10U, + (int16_t)1 << 11U, (int16_t)1 << 12U, (int16_t)1 << 13U, + (int16_t)1 << 14U, (int16_t)-32768, (int16_t)1 << 8U, + (int16_t)1 << 9U, (int16_t)1 << 10U, (int16_t)1 << 11U, + (int16_t)1 << 12U, (int16_t)1 << 13U, (int16_t)1 << 14U, + (int16_t)-32768)); return libcrux_intrinsics_avx2_mm256_srli_epi16((int32_t)15, coefficients_in_msb, __m256i); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_u8s( + uint8_t a, uint8_t b) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_i16s( + (int16_t)a, (int16_t)b); +} + +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_1(Eurydice_slice bytes) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_1_deserialize_1_u8s( + Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *)); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -691,16 +694,29 @@ static inline __m256i libcrux_ml_kem_vector_avx2_deserialize_1_09( return libcrux_ml_kem_vector_avx2_serialize_deserialize_1(bytes); } +/** + `mm256_concat_pairs_n(n, x)` is then a sequence of 32 bits packets + of the shape `0b0…0b₁…bₙa₁…aₙ`, if `x` is a sequence of pairs of + 16 bits, of the shape `(0b0…0a₁…aₙ, 0b0…0b₁…bₙ)` (where the last + `n` bits are non-zero). +*/ +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(uint8_t n, + __m256i x) { + int16_t n0 = (int16_t)1 << (uint32_t)n; + return libcrux_intrinsics_avx2_mm256_madd_epi16( + x, libcrux_intrinsics_avx2_mm256_set_epi16( + n0, (int16_t)1, n0, (int16_t)1, n0, (int16_t)1, n0, (int16_t)1, n0, + (int16_t)1, n0, (int16_t)1, n0, (int16_t)1, n0, (int16_t)1)); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_4( __m256i vector, uint8_t ret[8U]) { uint8_t serialized[16U] = {0U}; - __m256i adjacent_2_combined = libcrux_intrinsics_avx2_mm256_madd_epi16( - vector, libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1, - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1, - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1, - (int16_t)1 << 4U, (int16_t)1, (int16_t)1 << 4U, (int16_t)1)); + __m256i adjacent_2_combined = + libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(4U, vector); __m256i adjacent_8_combined = libcrux_intrinsics_avx2_mm256_shuffle_epi8( adjacent_2_combined, libcrux_intrinsics_avx2_mm256_set_epi8( @@ -739,31 +755,19 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_4_09(__m256i vector, KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) { +libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_i16s( + int16_t b0, int16_t b1, int16_t b2, int16_t b3, int16_t b4, int16_t b5, + int16_t b6, int16_t b7) { __m256i coefficients = libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), - (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)); - __m256i shift_lsbs_to_msbs = libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U); + b7, b7, b6, b6, b5, b5, b4, b4, b3, b3, b2, b2, b1, b1, b0, b0); __m256i coefficients_in_msb = libcrux_intrinsics_avx2_mm256_mullo_epi16( - coefficients, shift_lsbs_to_msbs); + coefficients, libcrux_intrinsics_avx2_mm256_set_epi16( + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U)); __m256i coefficients_in_lsb = libcrux_intrinsics_avx2_mm256_srli_epi16( (int32_t)4, coefficients_in_msb, __m256i); return libcrux_intrinsics_avx2_mm256_and_si256( @@ -771,6 +775,30 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) { ((int16_t)1 << 4U) - (int16_t)1)); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_u8s( + uint8_t b0, uint8_t b1, uint8_t b2, uint8_t b3, uint8_t b4, uint8_t b5, + uint8_t b6, uint8_t b7) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_i16s( + (int16_t)b0, (int16_t)b1, (int16_t)b2, (int16_t)b3, (int16_t)b4, + (int16_t)b5, (int16_t)b6, (int16_t)b7); +} + +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_4(Eurydice_slice bytes) { + return libcrux_ml_kem_vector_avx2_serialize_deserialize_4_deserialize_4_u8s( + Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *), + Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *)); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -837,6 +865,24 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_5_09(__m256i vector, libcrux_ml_kem_vector_avx2_serialize_serialize_5(vector, ret); } +/** + We cannot model `mm256_inserti128_si256` on its own: it produces a + Vec256 where the upper 128 bits are undefined. Thus + `mm256_inserti128_si256` is not pure. + + Luckily, we always call `mm256_castsi128_si256` right after + `mm256_inserti128_si256`: this composition sets the upper bits, + making the whole computation pure again. +*/ +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128(__m128i lower, + __m128i upper) { + return libcrux_intrinsics_avx2_mm256_inserti128_si256( + (int32_t)1, libcrux_intrinsics_avx2_mm256_castsi128_si256(lower), upper, + __m256i); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) { @@ -858,11 +904,10 @@ libcrux_ml_kem_vector_avx2_serialize_deserialize_5(Eurydice_slice bytes) { Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *), Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *)); __m256i coefficients_loaded = - libcrux_intrinsics_avx2_mm256_castsi128_si256(coefficients); - __m256i coefficients_loaded0 = libcrux_intrinsics_avx2_mm256_inserti128_si256( - (int32_t)1, coefficients_loaded, coefficients, __m256i); + libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + coefficients, coefficients); __m256i coefficients0 = libcrux_intrinsics_avx2_mm256_shuffle_epi8( - coefficients_loaded0, + coefficients_loaded, libcrux_intrinsics_avx2_mm256_set_epi8( (int8_t)15, (int8_t)14, (int8_t)15, (int8_t)14, (int8_t)13, (int8_t)12, (int8_t)13, (int8_t)12, (int8_t)11, (int8_t)10, @@ -892,17 +937,17 @@ static inline __m256i libcrux_ml_kem_vector_avx2_deserialize_5_09( return libcrux_ml_kem_vector_avx2_serialize_deserialize_5(bytes); } +typedef struct core_core_arch_x86___m128i_x2_s { + __m128i fst; + __m128i snd; +} core_core_arch_x86___m128i_x2; + KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( - __m256i vector, uint8_t ret[20U]) { - uint8_t serialized[32U] = {0U}; - __m256i adjacent_2_combined = libcrux_intrinsics_avx2_mm256_madd_epi16( - vector, - libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, (int16_t)1, - (int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, (int16_t)1, - (int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, (int16_t)1, - (int16_t)1 << 10U, (int16_t)1, (int16_t)1 << 10U, (int16_t)1)); +static inline core_core_arch_x86___m128i_x2 +libcrux_ml_kem_vector_avx2_serialize_serialize_10_serialize_10_vec( + __m256i vector) { + __m256i adjacent_2_combined = + libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(10U, vector); __m256i adjacent_4_combined = libcrux_intrinsics_avx2_mm256_sllv_epi32( adjacent_2_combined, libcrux_intrinsics_avx2_mm256_set_epi32( @@ -921,11 +966,24 @@ static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( (int8_t)3, (int8_t)2, (int8_t)1, (int8_t)0)); __m128i lower_8 = libcrux_intrinsics_avx2_mm256_castsi256_si128(adjacent_8_combined); + __m128i upper_8 = libcrux_intrinsics_avx2_mm256_extracti128_si256( + (int32_t)1, adjacent_8_combined, __m128i); + return ( + CLITERAL(core_core_arch_x86___m128i_x2){.fst = lower_8, .snd = upper_8}); +} + +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( + __m256i vector, uint8_t ret[20U]) { + core_core_arch_x86___m128i_x2 uu____0 = + libcrux_ml_kem_vector_avx2_serialize_serialize_10_serialize_10_vec( + vector); + __m128i lower_8 = uu____0.fst; + __m128i upper_8 = uu____0.snd; + uint8_t serialized[32U] = {0U}; libcrux_intrinsics_avx2_mm_storeu_bytes_si128( Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)16U, uint8_t), lower_8); - __m128i upper_8 = libcrux_intrinsics_avx2_mm256_extracti128_si256( - (int32_t)1, adjacent_8_combined, __m128i); libcrux_intrinsics_avx2_mm_storeu_bytes_si128( Eurydice_array_to_subslice2(serialized, (size_t)10U, (size_t)26U, uint8_t), @@ -952,37 +1010,46 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_10_09( KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) { - __m256i shift_lsbs_to_msbs = libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, - (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U); - __m128i lower_coefficients = libcrux_intrinsics_avx2_mm_loadu_si128( - Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t)); - __m128i lower_coefficients0 = libcrux_intrinsics_avx2_mm_shuffle_epi8( - lower_coefficients, +libcrux_ml_kem_vector_avx2_serialize_deserialize_10_deserialize_10_vec( + __m128i lower_coefficients0, __m128i upper_coefficients0) { + __m128i lower_coefficients = libcrux_intrinsics_avx2_mm_shuffle_epi8( + lower_coefficients0, libcrux_intrinsics_avx2_mm_set_epi8(9U, 8U, 8U, 7U, 7U, 6U, 6U, 5U, 4U, 3U, 3U, 2U, 2U, 1U, 1U, 0U)); - __m128i upper_coefficients = libcrux_intrinsics_avx2_mm_loadu_si128( - Eurydice_slice_subslice2(bytes, (size_t)4U, (size_t)20U, uint8_t)); - __m128i upper_coefficients0 = libcrux_intrinsics_avx2_mm_shuffle_epi8( - upper_coefficients, libcrux_intrinsics_avx2_mm_set_epi8( - 15U, 14U, 14U, 13U, 13U, 12U, 12U, 11U, 10U, 9U, - 9U, 8U, 8U, 7U, 7U, 6U)); + __m128i upper_coefficients = libcrux_intrinsics_avx2_mm_shuffle_epi8( + upper_coefficients0, libcrux_intrinsics_avx2_mm_set_epi8( + 15U, 14U, 14U, 13U, 13U, 12U, 12U, 11U, 10U, 9U, + 9U, 8U, 8U, 7U, 7U, 6U)); __m256i coefficients = - libcrux_intrinsics_avx2_mm256_castsi128_si256(lower_coefficients0); - __m256i coefficients0 = libcrux_intrinsics_avx2_mm256_inserti128_si256( - (int32_t)1, coefficients, upper_coefficients0, __m256i); - __m256i coefficients1 = libcrux_intrinsics_avx2_mm256_mullo_epi16( - coefficients0, shift_lsbs_to_msbs); - __m256i coefficients2 = libcrux_intrinsics_avx2_mm256_srli_epi16( - (int32_t)6, coefficients1, __m256i); + libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + lower_coefficients, upper_coefficients); + __m256i coefficients0 = libcrux_intrinsics_avx2_mm256_mullo_epi16( + coefficients, libcrux_intrinsics_avx2_mm256_set_epi16( + (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, + (int16_t)1 << 6U, (int16_t)1 << 0U, (int16_t)1 << 2U, + (int16_t)1 << 4U, (int16_t)1 << 6U, (int16_t)1 << 0U, + (int16_t)1 << 2U, (int16_t)1 << 4U, (int16_t)1 << 6U, + (int16_t)1 << 0U, (int16_t)1 << 2U, (int16_t)1 << 4U, + (int16_t)1 << 6U)); + __m256i coefficients1 = libcrux_intrinsics_avx2_mm256_srli_epi16( + (int32_t)6, coefficients0, __m256i); return libcrux_intrinsics_avx2_mm256_and_si256( - coefficients2, libcrux_intrinsics_avx2_mm256_set1_epi16( + coefficients1, libcrux_intrinsics_avx2_mm256_set1_epi16( ((int16_t)1 << 10U) - (int16_t)1)); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_10(Eurydice_slice bytes) { + Eurydice_slice lower_coefficients = + Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t); + Eurydice_slice upper_coefficients = + Eurydice_slice_subslice2(bytes, (size_t)4U, (size_t)20U, uint8_t); + return libcrux_ml_kem_vector_avx2_serialize_deserialize_10_deserialize_10_vec( + libcrux_intrinsics_avx2_mm_loadu_si128(lower_coefficients), + libcrux_intrinsics_avx2_mm_loadu_si128(upper_coefficients)); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -1039,16 +1106,11 @@ static inline __m256i libcrux_ml_kem_vector_avx2_deserialize_11_09( } KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( - __m256i vector, uint8_t ret[24U]) { - uint8_t serialized[32U] = {0U}; - __m256i adjacent_2_combined = libcrux_intrinsics_avx2_mm256_madd_epi16( - vector, - libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, (int16_t)1, - (int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, (int16_t)1, - (int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, (int16_t)1, - (int16_t)1 << 12U, (int16_t)1, (int16_t)1 << 12U, (int16_t)1)); +static KRML_MUSTINLINE core_core_arch_x86___m128i_x2 +libcrux_ml_kem_vector_avx2_serialize_serialize_12_serialize_12_vec( + __m256i vector) { + __m256i adjacent_2_combined = + libcrux_ml_kem_vector_avx2_serialize_mm256_concat_pairs_n(12U, vector); __m256i adjacent_4_combined = libcrux_intrinsics_avx2_mm256_sllv_epi32( adjacent_2_combined, libcrux_intrinsics_avx2_mm256_set_epi32( (int32_t)0, (int32_t)8, (int32_t)0, (int32_t)8, @@ -1068,6 +1130,19 @@ static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( libcrux_intrinsics_avx2_mm256_castsi256_si128(adjacent_8_combined); __m128i upper_8 = libcrux_intrinsics_avx2_mm256_extracti128_si256( (int32_t)1, adjacent_8_combined, __m128i); + return ( + CLITERAL(core_core_arch_x86___m128i_x2){.fst = lower_8, .snd = upper_8}); +} + +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( + __m256i vector, uint8_t ret[24U]) { + uint8_t serialized[32U] = {0U}; + core_core_arch_x86___m128i_x2 uu____0 = + libcrux_ml_kem_vector_avx2_serialize_serialize_12_serialize_12_vec( + vector); + __m128i lower_8 = uu____0.fst; + __m128i upper_8 = uu____0.snd; libcrux_intrinsics_avx2_mm_storeu_bytes_si128( Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)16U, uint8_t), lower_8); @@ -1097,37 +1172,45 @@ static inline void libcrux_ml_kem_vector_avx2_serialize_12_09( KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_serialize_deserialize_12(Eurydice_slice bytes) { - __m256i shift_lsbs_to_msbs = libcrux_intrinsics_avx2_mm256_set_epi16( - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, - (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U); - __m128i lower_coefficients = libcrux_intrinsics_avx2_mm_loadu_si128( - Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t)); - __m128i lower_coefficients0 = libcrux_intrinsics_avx2_mm_shuffle_epi8( - lower_coefficients, +libcrux_ml_kem_vector_avx2_serialize_deserialize_12_deserialize_12_vec( + __m128i lower_coefficients0, __m128i upper_coefficients0) { + __m128i lower_coefficients = libcrux_intrinsics_avx2_mm_shuffle_epi8( + lower_coefficients0, libcrux_intrinsics_avx2_mm_set_epi8(11U, 10U, 10U, 9U, 8U, 7U, 7U, 6U, 5U, 4U, 4U, 3U, 2U, 1U, 1U, 0U)); - __m128i upper_coefficients = libcrux_intrinsics_avx2_mm_loadu_si128( - Eurydice_slice_subslice2(bytes, (size_t)8U, (size_t)24U, uint8_t)); - __m128i upper_coefficients0 = libcrux_intrinsics_avx2_mm_shuffle_epi8( - upper_coefficients, + __m128i upper_coefficients = libcrux_intrinsics_avx2_mm_shuffle_epi8( + upper_coefficients0, libcrux_intrinsics_avx2_mm_set_epi8(15U, 14U, 14U, 13U, 12U, 11U, 11U, 10U, 9U, 8U, 8U, 7U, 6U, 5U, 5U, 4U)); __m256i coefficients = - libcrux_intrinsics_avx2_mm256_castsi128_si256(lower_coefficients0); - __m256i coefficients0 = libcrux_intrinsics_avx2_mm256_inserti128_si256( - (int32_t)1, coefficients, upper_coefficients0, __m256i); - __m256i coefficients1 = libcrux_intrinsics_avx2_mm256_mullo_epi16( - coefficients0, shift_lsbs_to_msbs); - __m256i coefficients2 = libcrux_intrinsics_avx2_mm256_srli_epi16( - (int32_t)4, coefficients1, __m256i); + libcrux_ml_kem_vector_avx2_serialize_mm256_si256_from_two_si128( + lower_coefficients, upper_coefficients); + __m256i coefficients0 = libcrux_intrinsics_avx2_mm256_mullo_epi16( + coefficients, libcrux_intrinsics_avx2_mm256_set_epi16( + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U, (int16_t)1 << 0U, (int16_t)1 << 4U, + (int16_t)1 << 0U, (int16_t)1 << 4U, (int16_t)1 << 0U, + (int16_t)1 << 4U)); + __m256i coefficients1 = libcrux_intrinsics_avx2_mm256_srli_epi16( + (int32_t)4, coefficients0, __m256i); return libcrux_intrinsics_avx2_mm256_and_si256( - coefficients2, libcrux_intrinsics_avx2_mm256_set1_epi16( + coefficients1, libcrux_intrinsics_avx2_mm256_set1_epi16( ((int16_t)1 << 12U) - (int16_t)1)); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE __m256i +libcrux_ml_kem_vector_avx2_serialize_deserialize_12(Eurydice_slice bytes) { + __m128i lower_coefficients = libcrux_intrinsics_avx2_mm_loadu_si128( + Eurydice_slice_subslice2(bytes, (size_t)0U, (size_t)16U, uint8_t)); + __m128i upper_coefficients = libcrux_intrinsics_avx2_mm_loadu_si128( + Eurydice_slice_subslice2(bytes, (size_t)8U, (size_t)24U, uint8_t)); + return libcrux_ml_kem_vector_avx2_serialize_deserialize_12_deserialize_12_vec( + lower_coefficients, upper_coefficients); +} + /** This function found in impl {(libcrux_ml_kem::vector::traits::Operations for libcrux_ml_kem::vector::avx2::SIMD256Vector)#2} @@ -1322,7 +1405,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e6( +libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_53( __m256i vector) { __m256i field_modulus = libcrux_intrinsics_avx2_mm256_set1_epi32( (int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); @@ -1374,9 +1457,9 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline __m256i -libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a6( +libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e6( + return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_53( vector); } @@ -1404,7 +1487,7 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_10_86( serialized, i0 * (size_t)20U, i0 * (size_t)20U + (size_t)20U, uint8_t); __m256i coefficient = libcrux_ml_kem_vector_avx2_deserialize_10_09(bytes); re.coefficients[i0] = - libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a6( + libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb( coefficient); } return re; @@ -1418,7 +1501,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e60( +libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_530( __m256i vector) { __m256i field_modulus = libcrux_intrinsics_avx2_mm256_set1_epi32( (int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); @@ -1470,9 +1553,9 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline __m256i -libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a60( +libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb0( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e60( + return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_530( vector); } @@ -1495,7 +1578,7 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_11_6d( serialized, i0 * (size_t)22U, i0 * (size_t)22U + (size_t)22U, uint8_t); __m256i coefficient = libcrux_ml_kem_vector_avx2_deserialize_11_09(bytes); re.coefficients[i0] = - libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a60( + libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb0( coefficient); } return re; @@ -1741,7 +1824,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e61( +libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_531( __m256i vector) { __m256i field_modulus = libcrux_intrinsics_avx2_mm256_set1_epi32( (int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); @@ -1793,9 +1876,9 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline __m256i -libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a61( +libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb1( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e61( + return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_531( vector); } @@ -1818,7 +1901,7 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_4_c2( serialized, i0 * (size_t)8U, i0 * (size_t)8U + (size_t)8U, uint8_t); __m256i coefficient = libcrux_ml_kem_vector_avx2_deserialize_4_09(bytes); re.coefficients[i0] = - libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a61( + libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb1( coefficient); } return re; @@ -1832,7 +1915,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e62( +libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_532( __m256i vector) { __m256i field_modulus = libcrux_intrinsics_avx2_mm256_set1_epi32( (int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS); @@ -1884,9 +1967,9 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline __m256i -libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a62( +libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb2( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_e62( + return libcrux_ml_kem_vector_avx2_compress_decompress_ciphertext_coefficient_532( vector); } @@ -1909,7 +1992,7 @@ libcrux_ml_kem_serialize_deserialize_then_decompress_5_1b( serialized, i0 * (size_t)10U, i0 * (size_t)10U + (size_t)10U, uint8_t); re.coefficients[i0] = libcrux_ml_kem_vector_avx2_deserialize_5_09(bytes); re.coefficients[i0] = - libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_a62( + libcrux_ml_kem_vector_avx2_decompress_ciphertext_coefficient_09_eb2( re.coefficients[i0]); } return re; @@ -3511,7 +3594,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_82( +libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f( __m256i vector) { __m256i field_modulus_halved = libcrux_intrinsics_avx2_mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / @@ -3566,9 +3649,9 @@ with const generics - COEFFICIENT_BITS= 10 */ KRML_ATTRIBUTE_TARGET("avx2") -static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_4e( +static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_3e( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_82( + return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f( vector); } @@ -3586,7 +3669,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_10_34( for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; - __m256i coefficient = libcrux_ml_kem_vector_avx2_compress_09_4e( + __m256i coefficient = libcrux_ml_kem_vector_avx2_compress_09_3e( libcrux_ml_kem_serialize_to_unsigned_field_modulus_7b( re->coefficients[i0])); uint8_t bytes[20U]; @@ -3609,7 +3692,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_820( +libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f0( __m256i vector) { __m256i field_modulus_halved = libcrux_intrinsics_avx2_mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / @@ -3664,9 +3747,9 @@ with const generics - COEFFICIENT_BITS= 11 */ KRML_ATTRIBUTE_TARGET("avx2") -static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_4e0( +static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_3e0( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_820( + return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f0( vector); } @@ -3684,7 +3767,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_11_47( for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; - __m256i coefficient = libcrux_ml_kem_vector_avx2_compress_09_4e0( + __m256i coefficient = libcrux_ml_kem_vector_avx2_compress_09_3e0( libcrux_ml_kem_vector_traits_to_unsigned_representative_3f( re->coefficients[i0])); uint8_t bytes[22U]; @@ -3754,7 +3837,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_821( +libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f1( __m256i vector) { __m256i field_modulus_halved = libcrux_intrinsics_avx2_mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / @@ -3809,9 +3892,9 @@ with const generics - COEFFICIENT_BITS= 4 */ KRML_ATTRIBUTE_TARGET("avx2") -static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_4e1( +static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_3e1( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_821( + return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f1( vector); } @@ -3829,7 +3912,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_4_c3( for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; - __m256i coefficient = libcrux_ml_kem_vector_avx2_compress_09_4e1( + __m256i coefficient = libcrux_ml_kem_vector_avx2_compress_09_3e1( libcrux_ml_kem_serialize_to_unsigned_field_modulus_7b( re.coefficients[i0])); uint8_t bytes[8U]; @@ -3849,7 +3932,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE __m256i -libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_822( +libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f2( __m256i vector) { __m256i field_modulus_halved = libcrux_intrinsics_avx2_mm256_set1_epi32( ((int32_t)LIBCRUX_ML_KEM_VECTOR_TRAITS_FIELD_MODULUS - (int32_t)1) / @@ -3904,9 +3987,9 @@ with const generics - COEFFICIENT_BITS= 5 */ KRML_ATTRIBUTE_TARGET("avx2") -static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_4e2( +static inline __m256i libcrux_ml_kem_vector_avx2_compress_09_3e2( __m256i vector) { - return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_822( + return libcrux_ml_kem_vector_avx2_compress_compress_ciphertext_coefficient_4f2( vector); } @@ -3924,7 +4007,7 @@ libcrux_ml_kem_serialize_compress_then_serialize_5_de( for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; - __m256i coefficients = libcrux_ml_kem_vector_avx2_compress_09_4e2( + __m256i coefficients = libcrux_ml_kem_vector_avx2_compress_09_3e2( libcrux_ml_kem_vector_traits_to_unsigned_representative_3f( re.coefficients[i0])); uint8_t bytes[10U]; @@ -4210,7 +4293,7 @@ with const generics - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1120 */ KRML_ATTRIBUTE_TARGET("avx2") -static inline void libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate_14( +static inline void libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate_0b( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_1f(private_key, ciphertext, ret); @@ -4227,7 +4310,7 @@ KRML_ATTRIBUTE_TARGET("avx2") static inline void libcrux_ml_kem_mlkem768_avx2_decapsulate( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { - libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate_14(private_key, + libcrux_ml_kem_ind_cca_instantiations_avx2_decapsulate_0b(private_key, ciphertext, ret); } @@ -4360,7 +4443,7 @@ with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline tuple_3c -libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_14( +libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_71( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key; @@ -4385,7 +4468,7 @@ static inline tuple_3c libcrux_ml_kem_mlkem768_avx2_encapsulate( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[32U]; memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t)); - return libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_14( + return libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_71( uu____0, copy_of_randomness); } @@ -4841,7 +4924,7 @@ libcrux_ml_kem.ind_cca.instantiations.avx2.generate_keypair with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair -libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair_8b( +libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair_20( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -4858,7 +4941,7 @@ libcrux_ml_kem_mlkem768_avx2_generate_key_pair(uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t)); - return libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair_8b( + return libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair_20( copy_of_randomness); } @@ -5017,7 +5100,7 @@ libcrux_ml_kem.ind_cca.instantiations.avx2.kyber_decapsulate with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline void -libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_decapsulate_7a( +libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_decapsulate_02( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_1f0(private_key, ciphertext, ret); @@ -5034,7 +5117,7 @@ KRML_ATTRIBUTE_TARGET("avx2") static inline void libcrux_ml_kem_mlkem768_avx2_kyber_decapsulate( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { - libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_decapsulate_7a( + libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_decapsulate_02( private_key, ciphertext, ret); } @@ -5152,7 +5235,7 @@ libcrux_ml_kem.ind_cca.instantiations.avx2.kyber_encapsulate with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline tuple_3c -libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_encapsulate_ff( +libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_encapsulate_7a( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key; @@ -5177,7 +5260,7 @@ static inline tuple_3c libcrux_ml_kem_mlkem768_avx2_kyber_encapsulate( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[32U]; memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t)); - return libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_encapsulate_ff( + return libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_encapsulate_7a( uu____0, copy_of_randomness); } @@ -5362,7 +5445,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair -libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_a1( +libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_74( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -5379,7 +5462,7 @@ libcrux_ml_kem_mlkem768_avx2_kyber_generate_key_pair(uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t)); - return libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_a1( + return libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_74( copy_of_randomness); } @@ -5418,7 +5501,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE bool -libcrux_ml_kem_ind_cca_instantiations_avx2_validate_private_key_01( +libcrux_ml_kem_ind_cca_instantiations_avx2_validate_private_key_4f( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext) { return libcrux_ml_kem_ind_cca_validate_private_key_3a(private_key, @@ -5434,7 +5517,7 @@ KRML_ATTRIBUTE_TARGET("avx2") static inline bool libcrux_ml_kem_mlkem768_avx2_validate_private_key( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext) { - return libcrux_ml_kem_ind_cca_instantiations_avx2_validate_private_key_01( + return libcrux_ml_kem_ind_cca_instantiations_avx2_validate_private_key_4f( private_key, ciphertext); } @@ -5510,7 +5593,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE bool -libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_59( +libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_a4( uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_c0(public_key); } @@ -5523,7 +5606,7 @@ libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_59( KRML_ATTRIBUTE_TARGET("avx2") static inline bool libcrux_ml_kem_mlkem768_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key) { - return libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_59( + return libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_a4( public_key->value); } @@ -5636,7 +5719,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline void -libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_decapsulate_44( +libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_decapsulate_e8( libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *key_pair, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_unpacked_decapsulate_6a(key_pair, ciphertext, ret); @@ -5653,7 +5736,7 @@ KRML_ATTRIBUTE_TARGET("avx2") static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_decapsulate( libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { - libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_decapsulate_44( + libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_decapsulate_e8( private_key, ciphertext, ret); } @@ -5748,7 +5831,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline tuple_3c -libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_encapsulate_71( +libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_encapsulate_89( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *uu____0 = @@ -5777,7 +5860,7 @@ static inline tuple_3c libcrux_ml_kem_mlkem768_avx2_unpacked_encapsulate( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[32U]; memcpy(copy_of_randomness, randomness, (size_t)32U * sizeof(uint8_t)); - return libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_encapsulate_71( + return libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_encapsulate_89( uu____0, copy_of_randomness); } @@ -5934,7 +6017,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline void -libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_generate_keypair_00( +libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_generate_keypair_b7( uint8_t randomness[64U], libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *out) { /* Passing arrays by value in Rust generates a copy in C */ @@ -5953,7 +6036,7 @@ static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_generate_key_pair( /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; memcpy(copy_of_randomness, randomness, (size_t)64U * sizeof(uint8_t)); - libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_generate_keypair_00( + libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_generate_keypair_b7( copy_of_randomness, key_pair); } @@ -5970,7 +6053,7 @@ with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 -libcrux_ml_kem_ind_cca_unpacked_default_1c_44(void) { +libcrux_ml_kem_ind_cca_unpacked_default_1c_9e(void) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 lit; lit.ind_cpa_public_key = libcrux_ml_kem_ind_cpa_unpacked_default_8d_89(); lit.public_key_hash[0U] = 0U; @@ -6022,7 +6105,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_2c(void) { + libcrux_ml_kem_ind_cca_unpacked_default_07_e2(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_3c(); uu____0.implicit_rejection_value[0U] = 0U; @@ -6060,7 +6143,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_44()}); + .public_key = libcrux_ml_kem_ind_cca_unpacked_default_1c_9e()}); } /** @@ -6069,7 +6152,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_2c(); + return libcrux_ml_kem_ind_cca_unpacked_default_07_e2(); } /** @@ -6078,7 +6161,7 @@ libcrux_ml_kem_mlkem768_avx2_unpacked_init_key_pair(void) { KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 libcrux_ml_kem_mlkem768_avx2_unpacked_init_public_key(void) { - return libcrux_ml_kem_ind_cca_unpacked_default_1c_44(); + return libcrux_ml_kem_ind_cca_unpacked_default_1c_9e(); } /** @@ -6099,7 +6182,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_99( +libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_92( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *self, libcrux_ml_kem_types_MlKemPublicKey_15 *serialized) { libcrux_ml_kem_ind_cpa_serialize_public_key_mut_6c( @@ -6127,10 +6210,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_39( +libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_a7( libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *self, libcrux_ml_kem_types_MlKemPublicKey_15 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_99( + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_92( &self->public_key, serialized); } @@ -6142,7 +6225,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_15 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_39(key_pair, + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_a7(key_pair, serialized); } @@ -6159,7 +6242,7 @@ with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0 -libcrux_ml_kem_ind_cpa_unpacked_clone_ef_18( +libcrux_ml_kem_ind_cpa_unpacked_clone_ef_42( libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_a0 *self) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0[3U]; core_array___core__clone__Clone_for__Array_T__N___20__clone( @@ -6196,11 +6279,11 @@ with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 -libcrux_ml_kem_ind_cca_unpacked_clone_28_69( +libcrux_ml_kem_ind_cca_unpacked_clone_28_24( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *self) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 lit; lit.ind_cpa_public_key = - libcrux_ml_kem_ind_cpa_unpacked_clone_ef_18(&self->ind_cpa_public_key); + libcrux_ml_kem_ind_cpa_unpacked_clone_ef_42(&self->ind_cpa_public_key); uint8_t ret[32U]; core_array___core__clone__Clone_for__Array_T__N___20__clone( (size_t)32U, self->public_key_hash, ret, uint8_t, void *); @@ -6224,7 +6307,7 @@ with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 * -libcrux_ml_kem_ind_cca_unpacked_public_key_de_b9( +libcrux_ml_kem_ind_cca_unpacked_public_key_de_77( libcrux_ml_kem_mlkem768_avx2_unpacked_MlKem768KeyPairUnpacked *self) { return &self->public_key; } @@ -6237,8 +6320,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_a0 *pk) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 uu____0 = - libcrux_ml_kem_ind_cca_unpacked_clone_28_69( - libcrux_ml_kem_ind_cca_unpacked_public_key_de_b9(key_pair)); + libcrux_ml_kem_ind_cca_unpacked_clone_28_24( + libcrux_ml_kem_ind_cca_unpacked_public_key_de_77(key_pair)); pk[0U] = uu____0; } @@ -6249,7 +6332,7 @@ KRML_ATTRIBUTE_TARGET("avx2") static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_serialized_public_key( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *public_key, libcrux_ml_kem_types_MlKemPublicKey_15 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_99(public_key, + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_92(public_key, serialized); } @@ -6314,7 +6397,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline void -libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_unpack_public_key_7f( +libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_unpack_public_key_d1( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *unpacked_public_key) { @@ -6330,7 +6413,7 @@ static inline void libcrux_ml_kem_mlkem768_avx2_unpacked_unpacked_public_key( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_a0 *unpacked_public_key) { - libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_unpack_public_key_7f( + libcrux_ml_kem_ind_cca_instantiations_avx2_unpacked_unpack_public_key_d1( public_key, unpacked_public_key); } diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h index 1e215bec0..a99ed2625 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #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 3d23894e4..2d7b89018 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_mlkem768_portable_H @@ -6916,7 +6916,7 @@ with const generics - K= 3 */ static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 -libcrux_ml_kem_ind_cca_unpacked_default_1c_6e(void) { +libcrux_ml_kem_ind_cca_unpacked_default_1c_bd(void) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 lit; lit.ind_cpa_public_key = libcrux_ml_kem_ind_cpa_unpacked_default_8d_d1(); lit.public_key_hash[0U] = 0U; @@ -6967,7 +6967,7 @@ with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked - libcrux_ml_kem_ind_cca_unpacked_default_07_35(void) { + libcrux_ml_kem_ind_cca_unpacked_default_07_db(void) { libcrux_ml_kem_ind_cca_unpacked_MlKemPrivateKeyUnpacked_f8 uu____0; uu____0.ind_cpa_private_key = libcrux_ml_kem_ind_cpa_unpacked_default_1a_e9(); uu____0.implicit_rejection_value[0U] = 0U; @@ -7005,7 +7005,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_6e()}); + .public_key = libcrux_ml_kem_ind_cca_unpacked_default_1c_bd()}); } /** @@ -7013,7 +7013,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_35(); + return libcrux_ml_kem_ind_cca_unpacked_default_07_db(); } /** @@ -7021,7 +7021,7 @@ libcrux_ml_kem_mlkem768_portable_unpacked_init_key_pair(void) { */ static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 libcrux_ml_kem_mlkem768_portable_unpacked_init_public_key(void) { - return libcrux_ml_kem_ind_cca_unpacked_default_1c_6e(); + return libcrux_ml_kem_ind_cca_unpacked_default_1c_bd(); } /** @@ -7041,7 +7041,7 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - PUBLIC_KEY_SIZE= 1184 */ static KRML_MUSTINLINE void -libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_52( +libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_a1( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 *self, libcrux_ml_kem_types_MlKemPublicKey_15 *serialized) { libcrux_ml_kem_ind_cpa_serialize_public_key_mut_3c( @@ -7068,10 +7068,10 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - PUBLIC_KEY_SIZE= 1184 */ static KRML_MUSTINLINE void -libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_e1( +libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_a4( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked *self, libcrux_ml_kem_types_MlKemPublicKey_15 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_52( + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_a1( &self->public_key, serialized); } @@ -7082,7 +7082,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_15 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_e1(key_pair, + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_de_a4(key_pair, serialized); } @@ -7098,7 +7098,7 @@ with const generics - K= 3 */ static inline libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_f8 -libcrux_ml_kem_ind_cpa_unpacked_clone_ef_b5( +libcrux_ml_kem_ind_cpa_unpacked_clone_ef_59( libcrux_ml_kem_ind_cpa_unpacked_IndCpaPublicKeyUnpacked_f8 *self) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0[3U]; core_array___core__clone__Clone_for__Array_T__N___20__clone( @@ -7134,11 +7134,11 @@ with const generics - K= 3 */ static inline libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 -libcrux_ml_kem_ind_cca_unpacked_clone_28_5f( +libcrux_ml_kem_ind_cca_unpacked_clone_28_d3( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 *self) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 lit; lit.ind_cpa_public_key = - libcrux_ml_kem_ind_cpa_unpacked_clone_ef_b5(&self->ind_cpa_public_key); + libcrux_ml_kem_ind_cpa_unpacked_clone_ef_59(&self->ind_cpa_public_key); uint8_t ret[32U]; core_array___core__clone__Clone_for__Array_T__N___20__clone( (size_t)32U, self->public_key_hash, ret, uint8_t, void *); @@ -7161,7 +7161,7 @@ with const generics - K= 3 */ static KRML_MUSTINLINE libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 * -libcrux_ml_kem_ind_cca_unpacked_public_key_de_e7( +libcrux_ml_kem_ind_cca_unpacked_public_key_de_3d( libcrux_ml_kem_mlkem768_portable_unpacked_MlKem768KeyPairUnpacked *self) { return &self->public_key; } @@ -7173,8 +7173,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_f8 *pk) { libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 uu____0 = - libcrux_ml_kem_ind_cca_unpacked_clone_28_5f( - libcrux_ml_kem_ind_cca_unpacked_public_key_de_e7(key_pair)); + libcrux_ml_kem_ind_cca_unpacked_clone_28_d3( + libcrux_ml_kem_ind_cca_unpacked_public_key_de_3d(key_pair)); pk[0U] = uu____0; } @@ -7185,7 +7185,7 @@ static inline void libcrux_ml_kem_mlkem768_portable_unpacked_serialized_public_key( libcrux_ml_kem_ind_cca_unpacked_MlKemPublicKeyUnpacked_f8 *public_key, libcrux_ml_kem_types_MlKemPublicKey_15 *serialized) { - libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_52(public_key, + libcrux_ml_kem_ind_cca_unpacked_serialized_public_key_mut_dd_a1(public_key, serialized); } diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h index c283eae80..e305985cd 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #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 2e9dfdbc9..6cdf64314 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #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 cd92309a3..cfdd6e5d5 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h @@ -7,8 +7,8 @@ * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 - * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 + * F*: 3063d19312f8ec3af5945f24ed3ebbb6b6cd9678 + * Libcrux: a089e8609d2bf2df5c165076a79e3fd30dbf87cf */ #ifndef __libcrux_sha3_portable_H diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst index ac2d0d4c1..c6edc5b32 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst @@ -101,11 +101,12 @@ let barrett_reduce (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) = <: i16)) in + let t512:Libcrux_intrinsics.Avx2_extract.t_Vec256 = + Libcrux_intrinsics.Avx2_extract.mm256_set1_epi16 512s + in + let _:Prims.unit = assert (forall i. get_lane t512 i == 512s) in let t1:Libcrux_intrinsics.Avx2_extract.t_Vec256 = - Libcrux_intrinsics.Avx2_extract.mm256_add_epi16 t0 - (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi16 512s - <: - Libcrux_intrinsics.Avx2_extract.t_Vec256) + Libcrux_intrinsics.Avx2_extract.mm256_add_epi16 t0 t512 in let _:Prims.unit = assert (forall i. get_lane t1 i == get_lane t0 i +. 512s) in let quotient:Libcrux_intrinsics.Avx2_extract.t_Vec256 = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst index 5ab43253f..d0c07fe84 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst @@ -11,6 +11,7 @@ let _ = () [@@"opaque_to_smt"] + let deserialize_1___deserialize_1_i16s (a b: i16) = let coefficients:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 b b b b b b b b a a a a a a a a @@ -27,6 +28,7 @@ let deserialize_1___deserialize_1_i16s (a b: i16) = Libcrux_intrinsics.Avx2_extract.mm256_srli_epi16 15l coefficients_in_msb [@@"opaque_to_smt"] + let deserialize_1___deserialize_1_u8s (a b: u8) = deserialize_1___deserialize_1_i16s (cast (a <: u8) <: i16) (cast (b <: u8) <: i16) @@ -36,6 +38,7 @@ let deserialize_1_ (bytes: t_Slice u8) = deserialize_1___deserialize_1_u8s (bytes.[ sz 0 ] <: u8) (bytes.[ sz 1 ] <: u8) [@@"opaque_to_smt"] + let deserialize_4___deserialize_4_i16s (b0 b1 b2 b3 b4 b5 b6 b7: i16) = let coefficients:Libcrux_intrinsics.Avx2_extract.t_Vec256 = Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 b7 b7 b6 b6 b5 b5 b4 b4 b3 b3 b2 b2 b1 b1 b0 b0 @@ -59,6 +62,7 @@ let deserialize_4___deserialize_4_i16s (b0 b1 b2 b3 b4 b5 b6 b7: i16) = Libcrux_intrinsics.Avx2_extract.t_Vec256) [@@"opaque_to_smt"] + let deserialize_4___deserialize_4_u8s (b0 b1 b2 b3 b4 b5 b6 b7: u8) = deserialize_4___deserialize_4_i16s (cast (b0 <: u8) <: i16) (cast (b1 <: u8) <: i16) @@ -453,6 +457,7 @@ let serialize_4_ (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) = #pop-options [@@"opaque_to_smt"] + let deserialize_10___deserialize_10_vec (lower_coefficients0 upper_coefficients0: Libcrux_intrinsics.Avx2_extract.t_Vec128) = @@ -523,6 +528,7 @@ let deserialize_10_ (bytes: t_Slice u8) = Libcrux_intrinsics.Avx2_extract.t_Vec128) [@@"opaque_to_smt"] + let deserialize_12___deserialize_12_vec (lower_coefficients0 upper_coefficients0: Libcrux_intrinsics.Avx2_extract.t_Vec128) = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst index 31c67d6b2..cbc90050c 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst @@ -3,7 +3,7 @@ module Libcrux_ml_kem.Vector.Traits open Core open FStar.Mul -#push-options "--z3rlimit 100" +#push-options "--z3rlimit 200 --split_queries always" let decompress_1_ (#v_T: Type0) diff --git a/libcrux-ml-kem/src/vector/avx2/arithmetic.rs b/libcrux-ml-kem/src/vector/avx2/arithmetic.rs index 11749144a..7f6d7e6b3 100644 --- a/libcrux-ml-kem/src/vector/avx2/arithmetic.rs +++ b/libcrux-ml-kem/src/vector/avx2/arithmetic.rs @@ -145,7 +145,9 @@ const BARRETT_MULTIPLIER: i16 = 20159; pub(crate) fn barrett_reduce(vector: Vec256) -> Vec256 { let t0 = mm256_mulhi_epi16(vector, mm256_set1_epi16(BARRETT_MULTIPLIER)); hax_lib::fstar!("assert (forall i. get_lane $t0 i == (cast (((cast (get_lane $vector i) <: i32) *. (cast v_BARRETT_MULTIPLIER <: i32)) >>! 16l) <: i16))"); - let t1 = mm256_add_epi16(t0, mm256_set1_epi16(512)); + let t512 = mm256_set1_epi16(512); + hax_lib::fstar!("assert (forall i. get_lane $t512 i == 512s)"); + let t1 = mm256_add_epi16(t0, t512); hax_lib::fstar!("assert (forall i. get_lane $t1 i == get_lane $t0 i +. 512s)"); let quotient = mm256_srai_epi16::<10>(t1); hax_lib::fstar!( diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index 3dd66ac97..438ab4dd4 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -235,7 +235,7 @@ pub fn to_unsigned_representative(a: T) -> T { T::add(a, &fm) } -#[hax_lib::fstar::options("--z3rlimit 100")] +#[hax_lib::fstar::options("--z3rlimit 200 --split_queries always")] #[hax_lib::requires(fstar!("forall i. let x = Seq.index (i1._super_8706949974463268012.f_repr ${vec}) i in (x == 0s \\/ x == 1s)"))] pub fn decompress_1(vec: T) -> T {