diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti index 7af7f302a..c2fb9704f 100644 --- a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti +++ b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti @@ -7,6 +7,8 @@ val mm256_add_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l val mm256_add_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) +val mm256_add_epi64 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + val mm256_and_si256 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) val mm256_andnot_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) @@ -14,6 +16,9 @@ val mm256_andnot_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_ val mm256_blend_epi16 (v_CONTROL: i32) (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) +val mm256_bsrli_epi128 (v_SHIFT_BY: i32) (x: u8) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + val mm256_castsi128_si256 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) val mm256_castsi256_si128 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) @@ -67,6 +72,9 @@ val mm256_set_epi16 val mm256_set_epi32 (input7 input6 input5 input4 input3 input2 input1 input0: i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) +val mm256_set_epi64x (input3 input2 input1 input0: i64) + : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + val mm256_set_epi8 (byte31 byte30 byte29 byte28 byte27 byte26 byte25 byte24 byte23 byte22 byte21 byte20 byte19 byte18 byte17 byte16 byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0: i8) @@ -104,6 +112,8 @@ val mm256_srli_epi32 (v_SHIFT_BY: i32) (vector: u8) val mm256_srli_epi64 (v_SHIFT_BY: i32) (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) +val mm256_srlv_epi64 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) + val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: u8) : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-intrinsics/src/avx2_extract.rs b/libcrux-intrinsics/src/avx2_extract.rs index f1d42e188..2dd4adadd 100644 --- a/libcrux-intrinsics/src/avx2_extract.rs +++ b/libcrux-intrinsics/src/avx2_extract.rs @@ -159,6 +159,10 @@ pub fn mm256_add_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } +pub fn mm256_add_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 { + unimplemented!() +} + pub fn mm256_sub_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 { unimplemented!() } @@ -313,6 +317,10 @@ pub fn mm256_slli_epi64(x: Vec256) -> Vec256 { unimplemented!() } +pub fn mm256_bsrli_epi128(x: Vec256) -> Vec256 { + unimplemented!() +} + #[inline(always)] pub fn mm256_andnot_si256(a: Vec256, b: Vec256) -> Vec256 { unimplemented!() @@ -332,3 +340,11 @@ pub fn mm256_unpacklo_epi64(a: Vec256, b: Vec256) -> Vec256 { pub fn mm256_permute2x128_si256(a: Vec256, b: Vec256) -> Vec256 { unimplemented!() } + +pub fn mm256_srlv_epi64(vector: Vec256, counts: Vec256) -> Vec256 { + unimplemented!() +} + +pub fn mm256_set_epi64x(input3: i64, input2: i64, input1: i64, input0: i64) -> Vec256 { + unimplemented!() +} diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt index c92c5be17..3f16d2187 100644 --- a/libcrux-ml-kem/c/code_gen.txt +++ b/libcrux-ml-kem/c/code_gen.txt @@ -3,4 +3,4 @@ Charon: 962f26311ccdf09a6a3cfeacbccafba22bf3d405 Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty -Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe +Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h index 3f6e7498f..d56ce580f 100644 --- a/libcrux-ml-kem/c/internal/libcrux_core.h +++ b/libcrux-ml-kem/c/internal/libcrux_core.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __internal_libcrux_core_H @@ -409,6 +409,29 @@ with types uint8_t[24size_t], core_array_TryFromSliceError */ void core_result_unwrap_41_1c(core_result_Result_6f self, uint8_t ret[24U]); +/** +A monomorphic instance of core.result.Result +with types uint8_t[22size_t], core_array_TryFromSliceError + +*/ +typedef struct core_result_Result_27_s { + core_result_Result_86_tags tag; + union { + uint8_t case_Ok[22U]; + core_array_TryFromSliceError case_Err; + } val; +} core_result_Result_27; + +/** +This function found in impl {core::result::Result} +*/ +/** +A monomorphic instance of core.result.unwrap_41 +with types uint8_t[22size_t], core_array_TryFromSliceError + +*/ +void core_result_unwrap_41_08(core_result_Result_27 self, uint8_t ret[22U]); + /** A monomorphic instance of core.result.Result with types uint8_t[20size_t], core_array_TryFromSliceError diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h index 0507dbaaf..198238b2d 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 a9b732317..085b13727 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 e87fcff90..353812b3c 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 34d3839a2..4382416fa 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 cf2942eaf..852c7afcd 100644 --- a/libcrux-ml-kem/c/libcrux_core.c +++ b/libcrux-ml-kem/c/libcrux_core.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #include "internal/libcrux_core.h" @@ -556,6 +556,26 @@ void core_result_unwrap_41_1c(core_result_Result_6f self, uint8_t ret[24U]) { } } +/** +This function found in impl {core::result::Result} +*/ +/** +A monomorphic instance of core.result.unwrap_41 +with types uint8_t[22size_t], core_array_TryFromSliceError + +*/ +void core_result_unwrap_41_08(core_result_Result_27 self, uint8_t ret[22U]) { + if (self.tag == core_result_Ok) { + uint8_t f0[22U]; + memcpy(f0, self.val.case_Ok, (size_t)22U * sizeof(uint8_t)); + memcpy(ret, f0, (size_t)22U * sizeof(uint8_t)); + } else { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, + "unwrap not Ok"); + KRML_HOST_EXIT(255U); + } +} + /** This function found in impl {core::result::Result} */ diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h index d284f5255..8141ec684 100644 --- a/libcrux-ml-kem/c/libcrux_core.h +++ b/libcrux-ml-kem/c/libcrux_core.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_core_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h index 7a7138a01..66ad1cf6a 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 6bd395b40..005f0d427 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #include "libcrux_mlkem1024_avx2.h" @@ -38,7 +38,7 @@ with const generics - ETA2_RANDOMNESS_SIZE= 128 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1600 */ -static void decapsulate_c1( +static void decapsulate_1c( libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key, libcrux_ml_kem_mlkem1024_MlKem1024Ciphertext *ciphertext, uint8_t ret[32U]) { @@ -56,7 +56,7 @@ void libcrux_ml_kem_mlkem1024_avx2_decapsulate( libcrux_ml_kem_types_MlKemPrivateKey_95 *private_key, libcrux_ml_kem_mlkem1024_MlKem1024Ciphertext *ciphertext, uint8_t ret[32U]) { - decapsulate_c1(private_key, ciphertext, ret); + decapsulate_1c(private_key, ciphertext, ret); } /** @@ -76,7 +76,7 @@ with const generics - ETA2= 2 - ETA2_RANDOMNESS_SIZE= 128 */ -static tuple_21 encapsulate_67( +static tuple_21 encapsulate_5c( libcrux_ml_kem_types_MlKemPublicKey_1f *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_1f *uu____0 = public_key; @@ -100,7 +100,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_67(uu____0, copy_of_randomness); + return encapsulate_5c(uu____0, copy_of_randomness); } /** @@ -117,7 +117,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_7e( +static libcrux_ml_kem_mlkem1024_MlKem1024KeyPair generate_keypair_29( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -133,7 +133,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_7e(copy_of_randomness); + return generate_keypair_29(copy_of_randomness); } /** @@ -147,7 +147,7 @@ generics - RANKED_BYTES_PER_RING_ELEMENT= 1536 - PUBLIC_KEY_SIZE= 1568 */ -static bool validate_public_key_320(uint8_t *public_key) { +static bool validate_public_key_6d0(uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_0a0(public_key); } @@ -159,7 +159,7 @@ static bool validate_public_key_320(uint8_t *public_key) { core_option_Option_99 libcrux_ml_kem_mlkem1024_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_1f public_key) { core_option_Option_99 uu____0; - if (validate_public_key_320(public_key.value)) { + if (validate_public_key_6d0(public_key.value)) { uu____0 = (CLITERAL(core_option_Option_99){.tag = core_option_Some, .f0 = public_key}); } else { diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h index c428d45b7..69c69fd81 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 50124a101..99315e861 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 682534bbb..28174e249 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_mlkem1024_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h index 0bd6bf2eb..afcea85e5 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 9a861af2f..6e1db25aa 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #include "libcrux_mlkem512_avx2.h" @@ -38,7 +38,7 @@ with const generics - ETA2_RANDOMNESS_SIZE= 128 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 800 */ -static void decapsulate_f8(libcrux_ml_kem_types_MlKemPrivateKey_5e *private_key, +static void decapsulate_de(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_42(private_key, ciphertext, ret); @@ -54,7 +54,7 @@ static void decapsulate_f8(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_f8(private_key, ciphertext, ret); + decapsulate_de(private_key, ciphertext, ret); } /** @@ -74,7 +74,7 @@ with const generics - ETA2= 2 - ETA2_RANDOMNESS_SIZE= 128 */ -static tuple_ec encapsulate_72( +static tuple_ec encapsulate_c7( libcrux_ml_kem_types_MlKemPublicKey_be *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_be *uu____0 = public_key; @@ -98,7 +98,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_72(uu____0, copy_of_randomness); + return encapsulate_c7(uu____0, copy_of_randomness); } /** @@ -115,7 +115,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_9f( +static libcrux_ml_kem_types_MlKemKeyPair_cb generate_keypair_c0( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -131,7 +131,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_9f(copy_of_randomness); + return generate_keypair_c0(copy_of_randomness); } /** @@ -145,7 +145,7 @@ generics - RANKED_BYTES_PER_RING_ELEMENT= 768 - PUBLIC_KEY_SIZE= 800 */ -static bool validate_public_key_32(uint8_t *public_key) { +static bool validate_public_key_6d(uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_0a(public_key); } @@ -157,7 +157,7 @@ static bool validate_public_key_32(uint8_t *public_key) { core_option_Option_04 libcrux_ml_kem_mlkem512_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_be public_key) { core_option_Option_04 uu____0; - if (validate_public_key_32(public_key.value)) { + if (validate_public_key_6d(public_key.value)) { uu____0 = (CLITERAL(core_option_Option_04){.tag = core_option_Some, .f0 = public_key}); } else { diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h index 51620676c..9adbdd046 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 da66678c6..9dd1de4f7 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 697c65cd3..49111e557 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_mlkem512_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h index a4aba4d66..a4baede23 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 ef03c9787..260b52d96 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #include "libcrux_mlkem768_avx2.h" @@ -38,7 +38,7 @@ with const generics - ETA2_RANDOMNESS_SIZE= 128 - IMPLICIT_REJECTION_HASH_INPUT_SIZE= 1120 */ -static void decapsulate_ba( +static void decapsulate_da( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_421(private_key, ciphertext, ret); @@ -54,7 +54,7 @@ static void decapsulate_ba( 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_ba(private_key, ciphertext, ret); + decapsulate_da(private_key, ciphertext, ret); } /** @@ -74,7 +74,7 @@ with const generics - ETA2= 2 - ETA2_RANDOMNESS_SIZE= 128 */ -static tuple_3c encapsulate_8a( +static tuple_3c encapsulate_df( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key; @@ -98,7 +98,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_8a(uu____0, copy_of_randomness); + return encapsulate_df(uu____0, copy_of_randomness); } /** @@ -115,7 +115,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_68( +static libcrux_ml_kem_mlkem768_MlKem768KeyPair generate_keypair_6d( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -131,7 +131,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_68(copy_of_randomness); + return generate_keypair_6d(copy_of_randomness); } /** @@ -145,7 +145,7 @@ generics - RANKED_BYTES_PER_RING_ELEMENT= 1152 - PUBLIC_KEY_SIZE= 1184 */ -static bool validate_public_key_321(uint8_t *public_key) { +static bool validate_public_key_6d1(uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_0a1(public_key); } @@ -157,7 +157,7 @@ static bool validate_public_key_321(uint8_t *public_key) { core_option_Option_92 libcrux_ml_kem_mlkem768_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_15 public_key) { core_option_Option_92 uu____0; - if (validate_public_key_321(public_key.value)) { + if (validate_public_key_6d1(public_key.value)) { uu____0 = (CLITERAL(core_option_Option_92){.tag = core_option_Some, .f0 = public_key}); } else { diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h index 813dfefb0..9d52f1995 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 eeb4a3abb..f09d52be5 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 ee82d1370..a42591f75 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 03a7b6c5c..3473af51a 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #include "internal/libcrux_mlkem_avx2.h" @@ -842,14 +842,45 @@ __m256i libcrux_ml_kem_vector_avx2_deserialize_10_ea(Eurydice_slice bytes) { KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_11( __m256i vector, uint8_t ret[22U]) { - int16_t array[16U] = {0U}; - mm256_storeu_si256_i16(Eurydice_array_to_slice((size_t)16U, array, int16_t), - vector); - libcrux_ml_kem_vector_portable_vector_type_PortableVector input = - libcrux_ml_kem_vector_portable_from_i16_array_0d( - Eurydice_array_to_slice((size_t)16U, array, int16_t)); + uint8_t serialized[32U] = {0U}; + __m256i adjacent_2_combined = mm256_madd_epi16( + vector, mm256_set_epi16((int16_t)1 << 11U, (int16_t)1, (int16_t)1 << 11U, + (int16_t)1, (int16_t)1 << 11U, (int16_t)1, + (int16_t)1 << 11U, (int16_t)1, (int16_t)1 << 11U, + (int16_t)1, (int16_t)1 << 11U, (int16_t)1, + (int16_t)1 << 11U, (int16_t)1, (int16_t)1 << 11U, + (int16_t)1)); + __m256i adjacent_4_combined = mm256_sllv_epi32( + adjacent_2_combined, + mm256_set_epi32((int32_t)0, (int32_t)10, (int32_t)0, (int32_t)10, + (int32_t)0, (int32_t)10, (int32_t)0, (int32_t)10)); + __m256i adjacent_4_combined0 = + mm256_srli_epi64((int32_t)10, adjacent_4_combined, __m256i); + __m256i second_4_combined = + mm256_bsrli_epi128((int32_t)8, adjacent_4_combined0, __m256i); + __m256i least_20_bits_shifted_up = + mm256_slli_epi64((int32_t)44, second_4_combined, __m256i); + __m256i bits_sequential = + mm256_add_epi64(adjacent_4_combined0, least_20_bits_shifted_up); + __m256i bits_sequential0 = mm256_srlv_epi64( + bits_sequential, + mm256_set_epi64x((int64_t)20, (int64_t)0, (int64_t)20, (int64_t)0)); + __m128i first_11_bytes = mm256_castsi256_si128(bits_sequential0); + mm_storeu_bytes_si128( + Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)16U, uint8_t), + first_11_bytes); + __m128i next_11_bytes = + mm256_extracti128_si256((int32_t)1, bits_sequential0, __m128i); + mm_storeu_bytes_si128(Eurydice_array_to_subslice2(serialized, (size_t)11U, + (size_t)27U, uint8_t), + next_11_bytes); uint8_t ret0[22U]; - libcrux_ml_kem_vector_portable_serialize_11_0d(input, ret0); + core_result_Result_27 dst; + Eurydice_slice_to_array2( + &dst, + Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)22U, uint8_t), + Eurydice_slice, uint8_t[22U]); + core_result_unwrap_41_08(dst, ret0); memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t)); } diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h index de251e8eb..049d5075e 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_mlkem_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.c b/libcrux-ml-kem/c/libcrux_mlkem_portable.c index 4c13b8d96..4bf2421df 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #include "internal/libcrux_mlkem_portable.h" @@ -66,147 +66,6 @@ const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U] = { (int16_t)-108, (int16_t)-308, (int16_t)996, (int16_t)991, (int16_t)958, (int16_t)-1460, (int16_t)1522, (int16_t)1628}; -KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_vector_type_from_i16_array( - Eurydice_slice array) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; - int16_t ret[16U]; - core_result_Result_c0 dst; - Eurydice_slice_to_array2( - &dst, Eurydice_slice_subslice2(array, (size_t)0U, (size_t)16U, int16_t), - Eurydice_slice, int16_t[16U]); - core_result_unwrap_41_f9(dst, ret); - memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); - return lit; -} - -/** -This function found in impl {(libcrux_ml_kem::vector::traits::Operations for -libcrux_ml_kem::vector::portable::vector_type::PortableVector)} -*/ -libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_from_i16_array_0d(Eurydice_slice array) { - return libcrux_ml_kem_vector_portable_vector_type_from_i16_array(array); -} - -KRML_MUSTINLINE uint8_t_x11 -libcrux_ml_kem_vector_portable_serialize_serialize_11_int(Eurydice_slice v) { - uint8_t r0 = (uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *); - uint8_t r1 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, - int16_t *) & - (int16_t)31) - << 3U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, - int16_t *) >> - 8U); - uint8_t r2 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, - int16_t *) & - (int16_t)3) - << 6U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, - int16_t *) >> - 5U); - uint8_t r3 = - (uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) >> 2U & - (int16_t)255); - uint8_t r4 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, - int16_t *) & - (int16_t)127) - << 1U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, - int16_t *) >> - 10U); - uint8_t r5 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, - int16_t *) & - (int16_t)15) - << 4U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, - int16_t *) >> - 7U); - uint8_t r6 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, - int16_t *) & - (int16_t)1) - << 7U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, - int16_t *) >> - 4U); - uint8_t r7 = - (uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) >> 1U & - (int16_t)255); - uint8_t r8 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, - int16_t *) & - (int16_t)63) - << 2U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, - int16_t *) >> - 9U); - uint8_t r9 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, - int16_t *) & - (int16_t)7) - << 5U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, - int16_t *) >> - 6U); - uint8_t r10 = - (uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) >> 3U); - return (CLITERAL(uint8_t_x11){.fst = r0, - .snd = r1, - .thd = r2, - .f3 = r3, - .f4 = r4, - .f5 = r5, - .f6 = r6, - .f7 = r7, - .f8 = r8, - .f9 = r9, - .f10 = r10}); -} - -KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_serialize_serialize_11( - libcrux_ml_kem_vector_portable_vector_type_PortableVector v, - uint8_t ret[22U]) { - uint8_t_x11 r0_10 = libcrux_ml_kem_vector_portable_serialize_serialize_11_int( - Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, int16_t)); - uint8_t_x11 r11_21 = - libcrux_ml_kem_vector_portable_serialize_serialize_11_int( - Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, - int16_t)); - uint8_t result[22U] = {0U}; - result[0U] = r0_10.fst; - result[1U] = r0_10.snd; - result[2U] = r0_10.thd; - result[3U] = r0_10.f3; - result[4U] = r0_10.f4; - result[5U] = r0_10.f5; - result[6U] = r0_10.f6; - result[7U] = r0_10.f7; - result[8U] = r0_10.f8; - result[9U] = r0_10.f9; - result[10U] = r0_10.f10; - result[11U] = r11_21.fst; - result[12U] = r11_21.snd; - result[13U] = r11_21.thd; - result[14U] = r11_21.f3; - result[15U] = r11_21.f4; - result[16U] = r11_21.f5; - result[17U] = r11_21.f6; - result[18U] = r11_21.f7; - result[19U] = r11_21.f8; - result[20U] = r11_21.f9; - result[21U] = r11_21.f10; - memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); -} - -/** -This function found in impl {(libcrux_ml_kem::vector::traits::Operations for -libcrux_ml_kem::vector::portable::vector_type::PortableVector)} -*/ -void libcrux_ml_kem_vector_portable_serialize_11_0d( - libcrux_ml_kem_vector_portable_vector_type_PortableVector a, - uint8_t ret[22U]) { - libcrux_ml_kem_vector_portable_serialize_serialize_11(a, ret); -} - KRML_MUSTINLINE int16_t_x8 libcrux_ml_kem_vector_portable_serialize_deserialize_11_int( Eurydice_slice bytes) { @@ -869,6 +728,29 @@ libcrux_ml_kem_vector_portable_ZERO_0d(void) { return libcrux_ml_kem_vector_portable_vector_type_zero(); } +KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_vector_type_from_i16_array( + Eurydice_slice array) { + libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; + int16_t ret[16U]; + core_result_Result_c0 dst; + Eurydice_slice_to_array2( + &dst, Eurydice_slice_subslice2(array, (size_t)0U, (size_t)16U, int16_t), + Eurydice_slice, int16_t[16U]); + core_result_unwrap_41_f9(dst, ret); + memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); + return lit; +} + +/** +This function found in impl {(libcrux_ml_kem::vector::traits::Operations for +libcrux_ml_kem::vector::portable::vector_type::PortableVector)} +*/ +libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_from_i16_array_0d(Eurydice_slice array) { + return libcrux_ml_kem_vector_portable_vector_type_from_i16_array(array); +} + KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_arithmetic_add( libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs, @@ -2010,6 +1892,124 @@ libcrux_ml_kem_vector_portable_deserialize_10_0d(Eurydice_slice a) { return libcrux_ml_kem_vector_portable_serialize_deserialize_10(a); } +KRML_MUSTINLINE uint8_t_x11 +libcrux_ml_kem_vector_portable_serialize_serialize_11_int(Eurydice_slice v) { + uint8_t r0 = (uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *); + uint8_t r1 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *) & + (int16_t)31) + << 3U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, + int16_t *) >> + 8U); + uint8_t r2 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *) & + (int16_t)3) + << 6U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *) >> + 5U); + uint8_t r3 = + (uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) >> 2U & + (int16_t)255); + uint8_t r4 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *) & + (int16_t)127) + << 1U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *) >> + 10U); + uint8_t r5 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, + int16_t *) & + (int16_t)15) + << 4U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *) >> + 7U); + uint8_t r6 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, + int16_t *) & + (int16_t)1) + << 7U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, + int16_t *) >> + 4U); + uint8_t r7 = + (uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) >> 1U & + (int16_t)255); + uint8_t r8 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, + int16_t *) & + (int16_t)63) + << 2U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, + int16_t *) >> + 9U); + uint8_t r9 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, + int16_t *) & + (int16_t)7) + << 5U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, + int16_t *) >> + 6U); + uint8_t r10 = + (uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) >> 3U); + return (CLITERAL(uint8_t_x11){.fst = r0, + .snd = r1, + .thd = r2, + .f3 = r3, + .f4 = r4, + .f5 = r5, + .f6 = r6, + .f7 = r7, + .f8 = r8, + .f9 = r9, + .f10 = r10}); +} + +KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_serialize_serialize_11( + libcrux_ml_kem_vector_portable_vector_type_PortableVector v, + uint8_t ret[22U]) { + uint8_t_x11 r0_10 = libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, int16_t)); + uint8_t_x11 r11_21 = + libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, + int16_t)); + uint8_t result[22U] = {0U}; + result[0U] = r0_10.fst; + result[1U] = r0_10.snd; + result[2U] = r0_10.thd; + result[3U] = r0_10.f3; + result[4U] = r0_10.f4; + result[5U] = r0_10.f5; + result[6U] = r0_10.f6; + result[7U] = r0_10.f7; + result[8U] = r0_10.f8; + result[9U] = r0_10.f9; + result[10U] = r0_10.f10; + result[11U] = r11_21.fst; + result[12U] = r11_21.snd; + result[13U] = r11_21.thd; + result[14U] = r11_21.f3; + result[15U] = r11_21.f4; + result[16U] = r11_21.f5; + result[17U] = r11_21.f6; + result[18U] = r11_21.f7; + result[19U] = r11_21.f8; + result[20U] = r11_21.f9; + result[21U] = r11_21.f10; + memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); +} + +/** +This function found in impl {(libcrux_ml_kem::vector::traits::Operations for +libcrux_ml_kem::vector::portable::vector_type::PortableVector)} +*/ +void libcrux_ml_kem_vector_portable_serialize_11_0d( + libcrux_ml_kem_vector_portable_vector_type_PortableVector a, + uint8_t ret[22U]) { + libcrux_ml_kem_vector_portable_serialize_serialize_11(a, ret); +} + KRML_MUSTINLINE uint8_t_x3 libcrux_ml_kem_vector_portable_serialize_serialize_12_int(Eurydice_slice v) { uint8_t r0 = diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h index 842002efe..460496c25 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_mlkem_portable_H @@ -39,49 +39,6 @@ void libcrux_ml_kem_hash_functions_portable_H(Eurydice_slice input, #define LIBCRUX_ML_KEM_VECTOR_TRAITS_INVERSE_OF_MODULUS_MOD_MONTGOMERY_R \ (62209U) -typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s { - int16_t elements[16U]; -} libcrux_ml_kem_vector_portable_vector_type_PortableVector; - -libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_vector_type_from_i16_array(Eurydice_slice array); - -/** -This function found in impl {(libcrux_ml_kem::vector::traits::Operations for -libcrux_ml_kem::vector::portable::vector_type::PortableVector)} -*/ -libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_from_i16_array_0d(Eurydice_slice array); - -typedef struct uint8_t_x11_s { - uint8_t fst; - uint8_t snd; - uint8_t thd; - uint8_t f3; - uint8_t f4; - uint8_t f5; - uint8_t f6; - uint8_t f7; - uint8_t f8; - uint8_t f9; - uint8_t f10; -} uint8_t_x11; - -uint8_t_x11 libcrux_ml_kem_vector_portable_serialize_serialize_11_int( - Eurydice_slice v); - -void libcrux_ml_kem_vector_portable_serialize_serialize_11( - libcrux_ml_kem_vector_portable_vector_type_PortableVector v, - uint8_t ret[22U]); - -/** -This function found in impl {(libcrux_ml_kem::vector::traits::Operations for -libcrux_ml_kem::vector::portable::vector_type::PortableVector)} -*/ -void libcrux_ml_kem_vector_portable_serialize_11_0d( - libcrux_ml_kem_vector_portable_vector_type_PortableVector a, - uint8_t ret[22U]); - typedef struct int16_t_x8_s { int16_t fst; int16_t snd; @@ -96,6 +53,10 @@ typedef struct int16_t_x8_s { int16_t_x8 libcrux_ml_kem_vector_portable_serialize_deserialize_11_int( Eurydice_slice bytes); +typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s { + int16_t elements[16U]; +} libcrux_ml_kem_vector_portable_vector_type_PortableVector; + libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_vector_type_zero(void); @@ -132,6 +93,16 @@ libcrux_ml_kem::vector::portable::vector_type::PortableVector)} libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_ZERO_0d(void); +libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_vector_type_from_i16_array(Eurydice_slice array); + +/** +This function found in impl {(libcrux_ml_kem::vector::traits::Operations for +libcrux_ml_kem::vector::portable::vector_type::PortableVector)} +*/ +libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_from_i16_array_0d(Eurydice_slice array); + libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_arithmetic_add( libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs, @@ -578,6 +549,35 @@ libcrux_ml_kem::vector::portable::vector_type::PortableVector)} libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_deserialize_10_0d(Eurydice_slice a); +typedef struct uint8_t_x11_s { + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; + uint8_t f4; + uint8_t f5; + uint8_t f6; + uint8_t f7; + uint8_t f8; + uint8_t f9; + uint8_t f10; +} uint8_t_x11; + +uint8_t_x11 libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_slice v); + +void libcrux_ml_kem_vector_portable_serialize_serialize_11( + libcrux_ml_kem_vector_portable_vector_type_PortableVector v, + uint8_t ret[22U]); + +/** +This function found in impl {(libcrux_ml_kem::vector::traits::Operations for +libcrux_ml_kem::vector::portable::vector_type::PortableVector)} +*/ +void libcrux_ml_kem_vector_portable_serialize_11_0d( + libcrux_ml_kem_vector_portable_vector_type_PortableVector a, + uint8_t ret[22U]); + typedef struct uint8_t_x3_s { uint8_t fst; uint8_t snd; diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h index 413cb8cfa..1650e131d 100644 --- a/libcrux-ml-kem/c/libcrux_sha3.h +++ b/libcrux-ml-kem/c/libcrux_sha3.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 0faa15823..5598ce791 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 1b23ca31d..7ed0a083e 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 1630106cf..dffc2877b 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 aed8b3ad4..09a4acc55 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.c +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 f2144bb1f..4cbf25306 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.h +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_sha3_neon_H diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt index a38d0a5db..3f16d2187 100644 --- a/libcrux-ml-kem/cg/code_gen.txt +++ b/libcrux-ml-kem/cg/code_gen.txt @@ -3,4 +3,4 @@ Charon: 962f26311ccdf09a6a3cfeacbccafba22bf3d405 Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty -Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 +Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h index 73953b59a..7b06cb223 100644 --- a/libcrux-ml-kem/cg/libcrux_core.h +++ b/libcrux-ml-kem/cg/libcrux_core.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_core_H @@ -116,6 +116,39 @@ static inline void unwrap_41_1c(Result_6f self, uint8_t ret[24U]) { } } +/** +A monomorphic instance of core.result.Result +with types uint8_t[22size_t], core_array_TryFromSliceError + +*/ +typedef struct Result_27_s { + Result_86_tags tag; + union { + uint8_t case_Ok[22U]; + TryFromSliceError case_Err; + } val; +} Result_27; + +/** +This function found in impl {core::result::Result} +*/ +/** +A monomorphic instance of core.result.unwrap_41 +with types uint8_t[22size_t], core_array_TryFromSliceError + +*/ +static inline void unwrap_41_08(Result_27 self, uint8_t ret[22U]) { + if (self.tag == Ok) { + uint8_t f0[22U]; + memcpy(f0, self.val.case_Ok, (size_t)22U * sizeof(uint8_t)); + memcpy(ret, f0, (size_t)22U * sizeof(uint8_t)); + } else { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, + "unwrap not Ok"); + KRML_HOST_EXIT(255U); + } +} + /** A monomorphic instance of core.result.Result with types uint8_t[20size_t], core_array_TryFromSliceError diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h index dc53c7231..fc944734b 100644 --- a/libcrux-ml-kem/cg/libcrux_ct_ops.h +++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 bf0c5a47d..f478dab33 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_mlkem768_avx2_H @@ -992,14 +992,48 @@ static inline __m256i libcrux_ml_kem_vector_avx2_deserialize_10_ea( KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_11( __m256i vector, uint8_t ret[22U]) { - int16_t array[16U] = {0U}; - libcrux_intrinsics_avx2_mm256_storeu_si256_i16( - Eurydice_array_to_slice((size_t)16U, array, int16_t), vector); - libcrux_ml_kem_vector_portable_vector_type_PortableVector input = - libcrux_ml_kem_vector_portable_from_i16_array_0d( - Eurydice_array_to_slice((size_t)16U, array, int16_t)); + 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 << 11U, (int16_t)1, (int16_t)1 << 11U, (int16_t)1, + (int16_t)1 << 11U, (int16_t)1, (int16_t)1 << 11U, (int16_t)1, + (int16_t)1 << 11U, (int16_t)1, (int16_t)1 << 11U, (int16_t)1, + (int16_t)1 << 11U, (int16_t)1, (int16_t)1 << 11U, (int16_t)1)); + __m256i adjacent_4_combined = libcrux_intrinsics_avx2_mm256_sllv_epi32( + adjacent_2_combined, + libcrux_intrinsics_avx2_mm256_set_epi32( + (int32_t)0, (int32_t)10, (int32_t)0, (int32_t)10, (int32_t)0, + (int32_t)10, (int32_t)0, (int32_t)10)); + __m256i adjacent_4_combined0 = libcrux_intrinsics_avx2_mm256_srli_epi64( + (int32_t)10, adjacent_4_combined, __m256i); + __m256i second_4_combined = libcrux_intrinsics_avx2_mm256_bsrli_epi128( + (int32_t)8, adjacent_4_combined0, __m256i); + __m256i least_20_bits_shifted_up = libcrux_intrinsics_avx2_mm256_slli_epi64( + (int32_t)44, second_4_combined, __m256i); + __m256i bits_sequential = libcrux_intrinsics_avx2_mm256_add_epi64( + adjacent_4_combined0, least_20_bits_shifted_up); + __m256i bits_sequential0 = libcrux_intrinsics_avx2_mm256_srlv_epi64( + bits_sequential, libcrux_intrinsics_avx2_mm256_set_epi64x( + (int64_t)20, (int64_t)0, (int64_t)20, (int64_t)0)); + __m128i first_11_bytes = + libcrux_intrinsics_avx2_mm256_castsi256_si128(bits_sequential0); + libcrux_intrinsics_avx2_mm_storeu_bytes_si128( + Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)16U, uint8_t), + first_11_bytes); + __m128i next_11_bytes = libcrux_intrinsics_avx2_mm256_extracti128_si256( + (int32_t)1, bits_sequential0, __m128i); + libcrux_intrinsics_avx2_mm_storeu_bytes_si128( + Eurydice_array_to_subslice2(serialized, (size_t)11U, (size_t)27U, + uint8_t), + next_11_bytes); uint8_t ret0[22U]; - libcrux_ml_kem_vector_portable_serialize_11_0d(input, ret0); + Result_27 dst; + Eurydice_slice_to_array2( + &dst, + Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)22U, uint8_t), + Eurydice_slice, uint8_t[22U]); + unwrap_41_08(dst, ret0); memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t)); } @@ -4302,7 +4336,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_dc( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_e5(private_key, ciphertext, ret); @@ -4319,7 +4353,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_dc(private_key, ciphertext, ret); } @@ -4452,7 +4486,7 @@ with const generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline tuple_3c -libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_41( +libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_93( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key; @@ -4477,7 +4511,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_41( + return libcrux_ml_kem_ind_cca_instantiations_avx2_encapsulate_93( uu____0, copy_of_randomness); } @@ -4908,7 +4942,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_c6( +libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair_79( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -4925,7 +4959,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_c6( + return libcrux_ml_kem_ind_cca_instantiations_avx2_generate_keypair_79( copy_of_randomness); } @@ -5084,7 +5118,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_f4( +libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_decapsulate_f9( libcrux_ml_kem_types_MlKemPrivateKey_55 *private_key, libcrux_ml_kem_mlkem768_MlKem768Ciphertext *ciphertext, uint8_t ret[32U]) { libcrux_ml_kem_ind_cca_decapsulate_e50(private_key, ciphertext, ret); @@ -5101,7 +5135,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_f4( + libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_decapsulate_f9( private_key, ciphertext, ret); } @@ -5219,7 +5253,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_9d( +libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_encapsulate_88( libcrux_ml_kem_types_MlKemPublicKey_15 *public_key, uint8_t randomness[32U]) { libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key; @@ -5244,7 +5278,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_9d( + return libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_encapsulate_88( uu____0, copy_of_randomness); } @@ -5414,7 +5448,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_mlkem768_MlKem768KeyPair -libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_e9( +libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_79( uint8_t randomness[64U]) { /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_randomness[64U]; @@ -5431,7 +5465,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_e9( + return libcrux_ml_kem_ind_cca_instantiations_avx2_kyber_generate_keypair_79( copy_of_randomness); } @@ -5531,7 +5565,7 @@ generics */ KRML_ATTRIBUTE_TARGET("avx2") static inline bool -libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_4d( +libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_d8( uint8_t *public_key) { return libcrux_ml_kem_ind_cca_validate_public_key_52(public_key); } @@ -5545,7 +5579,7 @@ KRML_ATTRIBUTE_TARGET("avx2") static inline Option_92 libcrux_ml_kem_mlkem768_avx2_validate_public_key( libcrux_ml_kem_types_MlKemPublicKey_15 public_key) { Option_92 uu____0; - if (libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_4d( + if (libcrux_ml_kem_ind_cca_instantiations_avx2_validate_public_key_d8( public_key.value)) { uu____0 = (CLITERAL(Option_92){.tag = Some, .f0 = public_key}); } else { diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h index 4e5fff02c..3797675e2 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_mlkem768_portable_H @@ -101,166 +101,6 @@ static const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U] = #define LIBCRUX_ML_KEM_VECTOR_TRAITS_INVERSE_OF_MODULUS_MOD_MONTGOMERY_R \ (62209U) -typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s { - int16_t elements[16U]; -} libcrux_ml_kem_vector_portable_vector_type_PortableVector; - -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_vector_type_from_i16_array( - Eurydice_slice array) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; - int16_t ret[16U]; - Result_c0 dst; - Eurydice_slice_to_array2( - &dst, Eurydice_slice_subslice2(array, (size_t)0U, (size_t)16U, int16_t), - Eurydice_slice, int16_t[16U]); - unwrap_41_f9(dst, ret); - memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); - return lit; -} - -/** -This function found in impl {(libcrux_ml_kem::vector::traits::Operations for -libcrux_ml_kem::vector::portable::vector_type::PortableVector)} -*/ -static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_from_i16_array_0d(Eurydice_slice array) { - return libcrux_ml_kem_vector_portable_vector_type_from_i16_array(array); -} - -typedef struct uint8_t_x11_s { - uint8_t fst; - uint8_t snd; - uint8_t thd; - uint8_t f3; - uint8_t f4; - uint8_t f5; - uint8_t f6; - uint8_t f7; - uint8_t f8; - uint8_t f9; - uint8_t f10; -} uint8_t_x11; - -static KRML_MUSTINLINE uint8_t_x11 -libcrux_ml_kem_vector_portable_serialize_serialize_11_int(Eurydice_slice v) { - uint8_t r0 = (uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *); - uint8_t r1 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, - int16_t *) & - (int16_t)31) - << 3U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, - int16_t *) >> - 8U); - uint8_t r2 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, - int16_t *) & - (int16_t)3) - << 6U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, - int16_t *) >> - 5U); - uint8_t r3 = - (uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) >> 2U & - (int16_t)255); - uint8_t r4 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, - int16_t *) & - (int16_t)127) - << 1U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, - int16_t *) >> - 10U); - uint8_t r5 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, - int16_t *) & - (int16_t)15) - << 4U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, - int16_t *) >> - 7U); - uint8_t r6 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, - int16_t *) & - (int16_t)1) - << 7U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, - int16_t *) >> - 4U); - uint8_t r7 = - (uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) >> 1U & - (int16_t)255); - uint8_t r8 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, - int16_t *) & - (int16_t)63) - << 2U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, - int16_t *) >> - 9U); - uint8_t r9 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, - int16_t *) & - (int16_t)7) - << 5U | - (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, - int16_t *) >> - 6U); - uint8_t r10 = - (uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) >> 3U); - return (CLITERAL(uint8_t_x11){.fst = r0, - .snd = r1, - .thd = r2, - .f3 = r3, - .f4 = r4, - .f5 = r5, - .f6 = r6, - .f7 = r7, - .f8 = r8, - .f9 = r9, - .f10 = r10}); -} - -static KRML_MUSTINLINE void -libcrux_ml_kem_vector_portable_serialize_serialize_11( - libcrux_ml_kem_vector_portable_vector_type_PortableVector v, - uint8_t ret[22U]) { - uint8_t_x11 r0_10 = libcrux_ml_kem_vector_portable_serialize_serialize_11_int( - Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, int16_t)); - uint8_t_x11 r11_21 = - libcrux_ml_kem_vector_portable_serialize_serialize_11_int( - Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, - int16_t)); - uint8_t result[22U] = {0U}; - result[0U] = r0_10.fst; - result[1U] = r0_10.snd; - result[2U] = r0_10.thd; - result[3U] = r0_10.f3; - result[4U] = r0_10.f4; - result[5U] = r0_10.f5; - result[6U] = r0_10.f6; - result[7U] = r0_10.f7; - result[8U] = r0_10.f8; - result[9U] = r0_10.f9; - result[10U] = r0_10.f10; - result[11U] = r11_21.fst; - result[12U] = r11_21.snd; - result[13U] = r11_21.thd; - result[14U] = r11_21.f3; - result[15U] = r11_21.f4; - result[16U] = r11_21.f5; - result[17U] = r11_21.f6; - result[18U] = r11_21.f7; - result[19U] = r11_21.f8; - result[20U] = r11_21.f9; - result[21U] = r11_21.f10; - memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); -} - -/** -This function found in impl {(libcrux_ml_kem::vector::traits::Operations for -libcrux_ml_kem::vector::portable::vector_type::PortableVector)} -*/ -static inline void libcrux_ml_kem_vector_portable_serialize_11_0d( - libcrux_ml_kem_vector_portable_vector_type_PortableVector a, - uint8_t ret[22U]) { - libcrux_ml_kem_vector_portable_serialize_serialize_11(a, ret); -} - typedef struct int16_t_x8_s { int16_t fst; int16_t snd; @@ -335,6 +175,10 @@ libcrux_ml_kem_vector_portable_serialize_deserialize_11_int( .f7 = r7}); } +typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s { + int16_t elements[16U]; +} libcrux_ml_kem_vector_portable_vector_type_PortableVector; + static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_vector_type_zero(void) { libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; @@ -935,6 +779,29 @@ libcrux_ml_kem_vector_portable_ZERO_0d(void) { return libcrux_ml_kem_vector_portable_vector_type_zero(); } +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_vector_type_from_i16_array( + Eurydice_slice array) { + libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; + int16_t ret[16U]; + Result_c0 dst; + Eurydice_slice_to_array2( + &dst, Eurydice_slice_subslice2(array, (size_t)0U, (size_t)16U, int16_t), + Eurydice_slice, int16_t[16U]); + unwrap_41_f9(dst, ret); + memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); + return lit; +} + +/** +This function found in impl {(libcrux_ml_kem::vector::traits::Operations for +libcrux_ml_kem::vector::portable::vector_type::PortableVector)} +*/ +static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_from_i16_array_0d(Eurydice_slice array) { + return libcrux_ml_kem_vector_portable_vector_type_from_i16_array(array); +} + static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_arithmetic_add( libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs, @@ -2119,6 +1986,139 @@ libcrux_ml_kem_vector_portable_deserialize_10_0d(Eurydice_slice a) { return libcrux_ml_kem_vector_portable_serialize_deserialize_10(a); } +typedef struct uint8_t_x11_s { + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; + uint8_t f4; + uint8_t f5; + uint8_t f6; + uint8_t f7; + uint8_t f8; + uint8_t f9; + uint8_t f10; +} uint8_t_x11; + +static KRML_MUSTINLINE uint8_t_x11 +libcrux_ml_kem_vector_portable_serialize_serialize_11_int(Eurydice_slice v) { + uint8_t r0 = (uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *); + uint8_t r1 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *) & + (int16_t)31) + << 3U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, + int16_t *) >> + 8U); + uint8_t r2 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *) & + (int16_t)3) + << 6U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *) >> + 5U); + uint8_t r3 = + (uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *) >> 2U & + (int16_t)255); + uint8_t r4 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *) & + (int16_t)127) + << 1U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *) >> + 10U); + uint8_t r5 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, + int16_t *) & + (int16_t)15) + << 4U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *) >> + 7U); + uint8_t r6 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, + int16_t *) & + (int16_t)1) + << 7U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, + int16_t *) >> + 4U); + uint8_t r7 = + (uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *) >> 1U & + (int16_t)255); + uint8_t r8 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, + int16_t *) & + (int16_t)63) + << 2U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, + int16_t *) >> + 9U); + uint8_t r9 = (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, + int16_t *) & + (int16_t)7) + << 5U | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, + int16_t *) >> + 6U); + uint8_t r10 = + (uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *) >> 3U); + return (CLITERAL(uint8_t_x11){.fst = r0, + .snd = r1, + .thd = r2, + .f3 = r3, + .f4 = r4, + .f5 = r5, + .f6 = r6, + .f7 = r7, + .f8 = r8, + .f9 = r9, + .f10 = r10}); +} + +static KRML_MUSTINLINE void +libcrux_ml_kem_vector_portable_serialize_serialize_11( + libcrux_ml_kem_vector_portable_vector_type_PortableVector v, + uint8_t ret[22U]) { + uint8_t_x11 r0_10 = libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_array_to_subslice2(v.elements, (size_t)0U, (size_t)8U, int16_t)); + uint8_t_x11 r11_21 = + libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_array_to_subslice2(v.elements, (size_t)8U, (size_t)16U, + int16_t)); + uint8_t result[22U] = {0U}; + result[0U] = r0_10.fst; + result[1U] = r0_10.snd; + result[2U] = r0_10.thd; + result[3U] = r0_10.f3; + result[4U] = r0_10.f4; + result[5U] = r0_10.f5; + result[6U] = r0_10.f6; + result[7U] = r0_10.f7; + result[8U] = r0_10.f8; + result[9U] = r0_10.f9; + result[10U] = r0_10.f10; + result[11U] = r11_21.fst; + result[12U] = r11_21.snd; + result[13U] = r11_21.thd; + result[14U] = r11_21.f3; + result[15U] = r11_21.f4; + result[16U] = r11_21.f5; + result[17U] = r11_21.f6; + result[18U] = r11_21.f7; + result[19U] = r11_21.f8; + result[20U] = r11_21.f9; + result[21U] = r11_21.f10; + memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); +} + +/** +This function found in impl {(libcrux_ml_kem::vector::traits::Operations for +libcrux_ml_kem::vector::portable::vector_type::PortableVector)} +*/ +static inline void libcrux_ml_kem_vector_portable_serialize_11_0d( + libcrux_ml_kem_vector_portable_vector_type_PortableVector a, + uint8_t ret[22U]) { + libcrux_ml_kem_vector_portable_serialize_serialize_11(a, ret); +} + typedef struct uint8_t_x3_s { uint8_t fst; uint8_t snd; diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h index 1dc4635ed..08d94001a 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #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 3e8e953d8..d84e46db6 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h @@ -8,7 +8,7 @@ * Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3 * Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a * F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty - * Libcrux: 7d3aa4de53d928af9db06c189a774877d4472c45 + * Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41 */ #ifndef __libcrux_sha3_portable_H diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti new file mode 100644 index 000000000..4d6616fd4 --- /dev/null +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti @@ -0,0 +1,243 @@ +module Libcrux_ml_kem.Variant +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let _ = + (* This module has implicit dependencies, here we make them explicit. *) + (* The implicit dependencies arise from typeclasses instances. *) + let open Libcrux_ml_kem.Hash_functions in + () + +/// Implements [`Variant`], to perform the ML-KEM-specific actions +/// during encapsulation and decapsulation. +/// Specifically, +/// * during key generation, the seed hash is domain separated (this is a difference from the FIPS 203 IPD and Kyber) +/// * during encapsulation, the initial randomness is used without prior hashing, +/// * the derivation of the shared secret does not include a hash of the ML-KEM ciphertext. +type t_MlKem = | MlKem : t_MlKem + +/// This trait collects differences in specification between ML-KEM +/// (FIPS 203) and the Round 3 CRYSTALS-Kyber submission in the +/// NIST PQ competition. +/// cf. FIPS 203, Appendix C +class t_Variant (v_Self: Type0) = { + f_kdf_pre: + v_K: usize -> + v_CIPHERTEXT_SIZE: usize -> + #v_Hasher: Type0 -> + {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + t_Slice u8 -> + Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE + -> Type0; + f_kdf_post: + v_K: usize -> + v_CIPHERTEXT_SIZE: usize -> + #v_Hasher: Type0 -> + {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + t_Slice u8 -> + Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE -> + t_Array u8 (sz 32) + -> Type0; + f_kdf: + v_K: usize -> + v_CIPHERTEXT_SIZE: usize -> + #v_Hasher: Type0 -> + {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + x0: t_Slice u8 -> + x1: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE + -> Prims.Pure (t_Array u8 (sz 32)) + (f_kdf_pre v_K v_CIPHERTEXT_SIZE #v_Hasher #i1 x0 x1) + (fun result -> f_kdf_post v_K v_CIPHERTEXT_SIZE #v_Hasher #i1 x0 x1 result); + f_entropy_preprocess_pre: + v_K: usize -> + #v_Hasher: Type0 -> + {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + t_Slice u8 + -> Type0; + f_entropy_preprocess_post: + v_K: usize -> + #v_Hasher: Type0 -> + {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + t_Slice u8 -> + t_Array u8 (sz 32) + -> Type0; + f_entropy_preprocess: + v_K: usize -> + #v_Hasher: Type0 -> + {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + x0: t_Slice u8 + -> Prims.Pure (t_Array u8 (sz 32)) + (f_entropy_preprocess_pre v_K #v_Hasher #i3 x0) + (fun result -> f_entropy_preprocess_post v_K #v_Hasher #i3 x0 result); + f_cpa_keygen_seed_pre: + v_K: usize -> + #v_Hasher: Type0 -> + {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + t_Slice u8 + -> Type0; + f_cpa_keygen_seed_post: + v_K: usize -> + #v_Hasher: Type0 -> + {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + t_Slice u8 -> + t_Array u8 (sz 64) + -> Type0; + f_cpa_keygen_seed: + v_K: usize -> + #v_Hasher: Type0 -> + {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} -> + x0: t_Slice u8 + -> Prims.Pure (t_Array u8 (sz 64)) + (f_cpa_keygen_seed_pre v_K #v_Hasher #i4 x0) + (fun result -> f_cpa_keygen_seed_post v_K #v_Hasher #i4 x0 result) +} + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: t_Variant t_MlKem = + { + f_kdf_pre + = + (fun + (v_K: usize) + (v_CIPHERTEXT_SIZE: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i1: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (shared_secret: t_Slice u8) + (_: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE) + -> + true); + f_kdf_post + = + (fun + (v_K: usize) + (v_CIPHERTEXT_SIZE: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i1: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (shared_secret: t_Slice u8) + (_: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE) + (out1: t_Array u8 (sz 32)) + -> + true); + f_kdf + = + (fun + (v_K: usize) + (v_CIPHERTEXT_SIZE: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i1: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (shared_secret: t_Slice u8) + (_: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE) + -> + let out:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in + let out:t_Array u8 (sz 32) = Core.Slice.impl__copy_from_slice #u8 out shared_secret in + out); + f_entropy_preprocess_pre + = + (fun + (v_K: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i3: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (randomness: t_Slice u8) + -> + true); + f_entropy_preprocess_post + = + (fun + (v_K: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i3: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (randomness: t_Slice u8) + (out1: t_Array u8 (sz 32)) + -> + true); + f_entropy_preprocess + = + (fun + (v_K: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i3: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (randomness: t_Slice u8) + -> + let out:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in + let out:t_Array u8 (sz 32) = Core.Slice.impl__copy_from_slice #u8 out randomness in + out); + f_cpa_keygen_seed_pre + = + (fun + (v_K: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i4: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (key_generation_seed: t_Slice u8) + -> + true); + f_cpa_keygen_seed_post + = + (fun + (v_K: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i4: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (key_generation_seed: t_Slice u8) + (out: t_Array u8 (sz 64)) + -> + true); + f_cpa_keygen_seed + = + fun + (v_K: usize) + (#v_Hasher: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i4: + Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K) + (key_generation_seed: t_Slice u8) + -> + let seed:t_Array u8 (sz 33) = Rust_primitives.Hax.repeat 0uy (sz 33) in + let seed:t_Array u8 (sz 33) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_range seed + ({ + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end = Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE + } + <: + Core.Ops.Range.t_Range usize) + (Core.Slice.impl__copy_from_slice #u8 + (seed.[ { + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end + = + Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE + } + <: + Core.Ops.Range.t_Range usize ] + <: + t_Slice u8) + key_generation_seed + <: + t_Slice u8) + in + let seed:t_Array u8 (sz 33) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed + Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE + (cast (v_K <: usize) <: u8) + in + Libcrux_ml_kem.Hash_functions.f_G #v_Hasher + #v_K + #FStar.Tactics.Typeclasses.solve + (seed <: t_Slice u8) + } 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 a7fa366a9..45c512e11 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 @@ -289,6 +289,87 @@ let serialize_10_ (vector: u8) = <: Core.Result.t_Result (t_Array u8 (sz 20)) Core.Array.t_TryFromSliceError) +let serialize_11_ (vector: u8) = + let serialized:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in + let adjacent_2_combined:u8 = + Libcrux_intrinsics.Avx2_extract.mm256_madd_epi16 vector + (Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 (1s < Prims.l_True) +val serialize_11_ (vector: u8) + : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True) + val serialize_12_ (vector: u8) : Prims.Pure (t_Array u8 (sz 24)) Prims.l_True (fun _ -> Prims.l_True) @@ -32,6 +35,3 @@ val serialize_5_ (vector: u8) : Prims.Pure (t_Array u8 (sz 10)) Prims.l_True (fu val serialize_4_ (vector: u8) : Prims.Pure (t_Array u8 (sz 8)) Prims.l_True (fun _ -> Prims.l_True) val deserialize_11_ (bytes: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True) - -val serialize_11_ (vector: u8) - : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-kem/src/vector/avx2/serialize.rs b/libcrux-ml-kem/src/vector/avx2/serialize.rs index 5b2a4fae5..10a4e51c2 100644 --- a/libcrux-ml-kem/src/vector/avx2/serialize.rs +++ b/libcrux-ml-kem/src/vector/avx2/serialize.rs @@ -1,5 +1,4 @@ use super::*; -use crate::vector::portable::PortableVector; #[inline(always)] pub(crate) fn serialize_1(vector: Vec256) -> [u8; 2] { @@ -515,17 +514,95 @@ pub(crate) fn deserialize_10(bytes: &[u8]) -> Vec256 { #[inline(always)] pub(crate) fn serialize_11(vector: Vec256) -> [u8; 22] { - let mut array = [0i16; 16]; - mm256_storeu_si256_i16(&mut array, vector); - let input = PortableVector::from_i16_array(&array); - PortableVector::serialize_11(input) + let mut serialized = [0u8; 32]; + + let adjacent_2_combined = mm256_madd_epi16( + vector, + mm256_set_epi16( + 1 << 11, + 1, + 1 << 11, + 1, + 1 << 11, + 1, + 1 << 11, + 1, + 1 << 11, + 1, + 1 << 11, + 1, + 1 << 11, + 1, + 1 << 11, + 1, + ), + ); + + let adjacent_4_combined = mm256_sllv_epi32( + adjacent_2_combined, + mm256_set_epi32(0, 10, 0, 10, 0, 10, 0, 10), + ); + let adjacent_4_combined = mm256_srli_epi64::<10>(adjacent_4_combined); + + let second_4_combined = mm256_bsrli_epi128::<8>(adjacent_4_combined); + let least_20_bits_shifted_up = mm256_slli_epi64::<44>(second_4_combined); + + let bits_sequential = mm256_add_epi64(adjacent_4_combined, least_20_bits_shifted_up); + let bits_sequential = mm256_srlv_epi64(bits_sequential, mm256_set_epi64x(20, 0, 20, 0)); + + let first_11_bytes = mm256_castsi256_si128(bits_sequential); + mm_storeu_bytes_si128(&mut serialized[0..16], first_11_bytes); + + let next_11_bytes = mm256_extracti128_si256::<1>(bits_sequential); + mm_storeu_bytes_si128(&mut serialized[11..27], next_11_bytes); + + serialized[0..22].try_into().unwrap() } #[inline(always)] pub(crate) fn deserialize_11(bytes: &[u8]) -> Vec256 { - let output = PortableVector::deserialize_11(bytes); - let array = PortableVector::to_i16_array(output); - mm256_loadu_si256_i16(&array) + let mut bytes_extended = [0u8; 32]; + bytes_extended[0..22].copy_from_slice(bytes); + + let bytes_loaded = mm256_loadu_si256_u8(&bytes_extended); + + let coefficients = mm256_permute4x64_epi64::<0b10_01_01_00>(bytes_loaded); + let coefficients = mm256_shuffle_epi8( + coefficients, + mm256_set_epi8( + 13, 12, 12, 11, 10, 9, 9, 8, 8, 7, 6, 5, 5, 4, 4, 3, 10, 9, 9, 8, 7, 6, 6, 5, 5, 4, 3, + 2, 2, 1, 1, 0, + ), + ); + + let coefficients = mm256_srlv_epi32(coefficients, mm256_set_epi32(0, 0, 1, 0, 0, 0, 1, 0)); + let coefficients = mm256_srlv_epi64(coefficients, mm256_set_epi64x(2, 0, 2, 0)); + + let coefficients_shifted_up = mm256_mullo_epi16( + coefficients, + mm256_set_epi16( + 1 << 2, + 1 << 5, + 1 << 0, + 1 << 3, + 1 << 5, + 1 << 0, + 1 << 2, + 1 << 5, + 1 << 2, + 1 << 5, + 1 << 0, + 1 << 3, + 1 << 5, + 1 << 0, + 1 << 2, + 1 << 5, + ), + ); + + // The coefficients are now in bit positions 5 to 16, so we shift them + // down to occupy bit positions 0 to 11. + mm256_srli_epi16::<5>(coefficients_shifted_up) } #[inline(always)]