ML-KEM: AVX2 implementation of serialize_11 and deserialize_11.

libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti

@@ -7,13 +7,18 @@ 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)
 
 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)
 

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<const LEFT: i32>(x: Vec256) -> Vec256 {
     unimplemented!()
 }
 
+pub fn mm256_bsrli_epi128<const SHIFT_BY: i32>(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<const IMM8: i32>(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!()
+}

libcrux-ml-kem/c/code_gen.txt

@@ -3,4 +3,4 @@ Charon: 962f26311ccdf09a6a3cfeacbccafba22bf3d405
 Eurydice: e66abbc2119485abfafa17c1911bdbdada5b04f3
 Karamel: 7862fdc3899b718d39ec98568f78ec40592a622a
 F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty
-Libcrux: 9a130a852767d2f8881c458e022bf35fec1f6afe
+Libcrux: a1a608ad503a9e3f8f017e9c2082ccf929194c41

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<T, E>}
+*/
+/**
+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

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

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

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

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

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<T, E>}
+*/
+/**
+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<T, E>}
 */

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

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

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 {

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

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"

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

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