Mutable Style for ML-KEM

fstar-helpers/core-models/src/core_arch/x86.rs

@@ -469,6 +469,12 @@ pub mod avx {
     pub fn _mm256_set1_epi16(_: i16) -> __m256i {
         unimplemented!()
     }
+
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_set1_epi8)
+    #[hax_lib::opaque]
+    pub fn _mm256_set1_epi8(_: i8) -> __m256i {
+        unimplemented!()
+    }
 }
 pub use avx2::*;
 pub mod avx2 {
@@ -547,6 +553,12 @@ pub mod avx2 {
         unimplemented!()
     }
 
+    /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_sign_epi16)
+    #[hax_lib::opaque]
+    pub fn _mm256_sign_epi16(_: __m256i, _: __m256i) -> __m256i {
+        unimplemented!()
+    }
+
     /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_mullo_epi32)
     #[hax_lib::opaque]
     pub fn _mm256_mullo_epi32(_: __m256i, _: __m256i) -> __m256i {

libcrux-intrinsics/src/arm64.rs

@@ -66,6 +66,11 @@ pub fn _vsubq_s16(lhs: int16x8_t, rhs: int16x8_t) -> int16x8_t {
     unsafe { vsubq_s16(lhs, rhs) }
 }
 
+#[inline(always)]
+pub fn _vnegq_s16(vec: int16x8_t) -> int16x8_t {
+    unsafe { vnegq_s16(vec) }
+}
+
 #[inline(always)]
 pub fn _vmulq_n_s16(v: int16x8_t, c: i16) -> int16x8_t {
     unsafe { vmulq_n_s16(v, c) }

libcrux-intrinsics/src/arm64_extract.rs

@@ -82,6 +82,11 @@ pub fn _vsubq_s16(lhs: _int16x8_t, rhs: _int16x8_t) -> _int16x8_t {
     unimplemented!()
 }
 
+#[inline(always)]
+pub fn _vnegq_s16(vec: _int16x8_t) -> _int16x8_t {
+    unimplemented!()
+}
+
 #[inline(always)]
 pub fn _vmulq_n_s16(v: _int16x8_t, c: i16) -> _int16x8_t {
     unimplemented!()

libcrux-intrinsics/src/avx2.rs

@@ -214,6 +214,12 @@ pub fn mm256_set1_epi16(constant: i16) -> Vec256 {
     unsafe { _mm256_set1_epi16(constant) }
 }
 
+#[hax_lib::opaque]
+#[inline(always)]
+pub fn mm256_set1_epi8(constant: i8) -> Vec256 {
+    unsafe { _mm256_set1_epi8(constant) }
+}
+
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set_epi16(
@@ -369,6 +375,12 @@ pub fn mm256_sign_epi32(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_sign_epi32(a, b) }
 }
 
+#[inline(always)]
+#[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
+pub fn mm256_sign_epi16(a: Vec256, b: Vec256) -> Vec256 {
+    unsafe { _mm256_sign_epi16(a, b) }
+}
+
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_castsi256_ps(a: Vec256) -> Vec256Float {

libcrux-intrinsics/src/avx2_extract.rs

@@ -345,6 +345,11 @@ pub fn mm256_sign_epi32(a: Vec256, b: Vec256) -> Vec256 {
     unimplemented!()
 }
 
+#[inline(always)]
+pub fn mm256_sign_epi16(a: Vec256, b: Vec256) -> Vec256 {
+    unimplemented!()
+}
+
 #[inline(always)]
 pub fn mm256_castsi256_ps(a: Vec256) -> Vec256Float {
     unimplemented!()

libcrux-ml-kem/README.md

@@ -4,14 +4,17 @@ This crate implements all three ML-KEM ([FIPS 203](https://csrc.nist.gov/pubs/fi
 For each algorithm, it inlcudes a portable Rust implementation, as well as SIMD implementations for Intel AVX2 and AArch64 Neon platforms.
 
 ## Verification
-![verified]
+![pre-verification]
 
-The portable and AVX2 code for field arithmetic, NTT polynomial arithmetic, serialization, and the generic code for high-level algorithms
+For [release `0.0.4`](https://crates.io/crates/libcrux-ml-kem/0.0.4) of this crate, the portable and AVX2 code for field arithmetic, NTT polynomial arithmetic, serialization, and the generic code for high-level algorithms
 is formally verified using [hax](https://cryspen.com/hax) and  [F*](https://fstar-lang.org).
 
-Please refer to [this file](proofs/verification_status.md) for detail on the verification of this crate.
+⚠️ In comparison, this current, *unreleased*, version of the crate (`HEAD` of branch `main`) introduces a number of open proof obligations, which we aim to resolve before the next release.
+
+Please refer to [this file](proofs/verification_status.md) for details on the current verification of this crate and comparison to the `0.0.4` release.
 
 [verified]: https://img.shields.io/badge/verified-brightgreen.svg?style=for-the-badge&logo=data:image/svg+xml;base64,PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz48IS0tIFVwbG9hZGVkIHRvOiBTVkcgUmVwbywgd3d3LnN2Z3JlcG8uY29tLCBHZW5lcmF0b3I6IFNWRyBSZXBvIE1peGVyIFRvb2xzIC0tPg0KPHN2ZyB3aWR0aD0iODAwcHgiIGhlaWdodD0iODAwcHgiIHZpZXdCb3g9IjAgMCAyNCAyNCIgZmlsbD0ibm9uZSIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3JnLzIwMDAvc3ZnIj4NCjxwYXRoIGQ9Ik05IDEyTDExIDE0TDE1IDkuOTk5OTlNMjAgMTJDMjAgMTYuNDYxMSAxNC41NCAxOS42OTM3IDEyLjY0MTQgMjAuNjgzQzEyLjQzNjEgMjAuNzkgMTIuMzMzNCAyMC44NDM1IDEyLjE5MSAyMC44NzEyQzEyLjA4IDIwLjg5MjggMTEuOTIgMjAuODkyOCAxMS44MDkgMjAuODcxMkMxMS42NjY2IDIwLjg0MzUgMTEuNTYzOSAyMC43OSAxMS4zNTg2IDIwLjY4M0M5LjQ1OTk2IDE5LjY5MzcgNCAxNi40NjExIDQgMTJWOC4yMTc1OUM0IDcuNDE4MDggNCA3LjAxODMzIDQuMTMwNzYgNi42NzQ3QzQuMjQ2MjcgNi4zNzExMyA0LjQzMzk4IDYuMTAwMjcgNC42Nzc2NiA1Ljg4NTUyQzQuOTUzNSA1LjY0MjQzIDUuMzI3OCA1LjUwMjA3IDYuMDc2NCA1LjIyMTM0TDExLjQzODIgMy4yMTA2N0MxMS42NDYxIDMuMTMyNzEgMTEuNzUgMy4wOTM3MyAxMS44NTcgMy4wNzgyN0MxMS45NTE4IDMuMDY0NTcgMTIuMDQ4MiAzLjA2NDU3IDEyLjE0MyAzLjA3ODI3QzEyLjI1IDMuMDkzNzMgMTIuMzUzOSAzLjEzMjcxIDEyLjU2MTggMy4yMTA2N0wxNy45MjM2IDUuMjIxMzRDMTguNjcyMiA1LjUwMjA3IDE5LjA0NjUgNS42NDI0MyAxOS4zMjIzIDUuODg1NTJDMTkuNTY2IDYuMTAwMjcgMTkuNzUzNyA2LjM3MTEzIDE5Ljg2OTIgNi42NzQ3QzIwIDcuMDE4MzMgMjAgNy40MTgwOCAyMCA4LjIxNzU5VjEyWiIgc3Ryb2tlPSIjMDAwMDAwIiBzdHJva2Utd2lkdGg9IjIiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIvPg0KPC9zdmc+
+[pre-verification]: https://img.shields.io/badge/pre_verification-orange.svg?style=for-the-badge&logo=data:image/svg+xml;base64,PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz48IS0tIFVwbG9hZGVkIHRvOiBTVkcgUmVwbywgd3d3LnN2Z3JlcG8uY29tLCBHZW5lcmF0b3I6IFNWRyBSZXBvIE1peGVyIFRvb2xzIC0tPg0KPHN2ZyB3aWR0aD0iODAwcHgiIGhlaWdodD0iODAwcHgiIHZpZXdCb3g9IjAgMCAyNCAyNCIgZmlsbD0ibm9uZSIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3JnLzIwMDAvc3ZnIj4NCjxwYXRoIGQ9Ik05IDEySDE1TTIwIDEyQzIwIDE2LjQ2MTEgMTQuNTQgMTkuNjkzNyAxMi42NDE0IDIwLjY4M0MxMi40MzYxIDIwLjc5IDEyLjMzMzQgMjAuODQzNSAxMi4xOTEgMjAuODcxMkMxMi4wOCAyMC44OTI4IDExLjkyIDIwLjg5MjggMTEuODA5IDIwLjg3MTJDMTEuNjY2NiAyMC44NDM1IDExLjU2MzkgMjAuNzkgMTEuMzU4NiAyMC42ODNDOS40NTk5NiAxOS42OTM3IDQgMTYuNDYxMSA0IDEyVjguMjE3NTlDNCA3LjQxODA4IDQgNy4wMTgzMyA0LjEzMDc2IDYuNjc0N0M0LjI0NjI3IDYuMzcxMTMgNC40MzM5OCA2LjEwMDI3IDQuNjc3NjYgNS44ODU1MkM0Ljk1MzUgNS42NDI0MyA1LjMyNzggNS41MDIwNyA2LjA3NjQgNS4yMjEzNEwxMS40MzgyIDMuMjEwNjdDMTEuNjQ2MSAzLjEzMjcxIDExLjc1IDMuMDkzNzMgMTEuODU3IDMuMDc4MjdDMTEuOTUxOCAzLjA2NDU3IDEyLjA0ODIgMy4wNjQ1NyAxMi4xNDMgMy4wNzgyN0MxMi4yNSAzLjA5MzczIDEyLjM1MzkgMy4xMzI3MSAxMi41NjE4IDMuMjEwNjdMMTcuOTIzNiA1LjIyMTM0QzE4LjY3MjIgNS41MDIwNyAxOS4wNDY1IDUuNjQyNDMgMTkuMzIyMyA1Ljg4NTUyQzE5LjU2NiA2LjEwMDI3IDE5Ljc1MzcgNi4zNzExMyAxOS44NjkyIDYuNjc0N0MyMCA3LjAxODMzIDIwIDcuNDE4MDggMjAgOC4yMTc1OVYxMloiIHN0cm9rZT0iIzAwMDAwMCIgc3Ryb2tlLXdpZHRoPSIyIiBzdHJva2UtbGluZWNhcD0icm91bmQiIHN0cm9rZS1saW5lam9pbj0icm91bmQiLz4NCjwvc3ZnPg==
 
 ## Usage
 

libcrux-ml-kem/extracts/c/generated/code_gen.txt

@@ -2,5 +2,5 @@ This code was generated with the following revisions:
 Charon: 667d2fc98984ff7f3df989c2367e6c1fa4a000e7
 Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
 Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
-F*: 71d8221589d4d438af3706d89cb653cf53e18aab
-Libcrux: 68dfed5a4a9e40277f62828471c029afed1ecdcc
+F*: unset
+Libcrux: bf73a8a7a0f119e66b105a3462265b4a2a3af63b

libcrux-ml-kem/extracts/c/generated/header.txt

@@ -7,6 +7,6 @@
  * Charon: 667d2fc98984ff7f3df989c2367e6c1fa4a000e7
  * Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
  * Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: 68dfed5a4a9e40277f62828471c029afed1ecdcc
+ * F*: unset
+ * Libcrux: bf73a8a7a0f119e66b105a3462265b4a2a3af63b
  */

libcrux-ml-kem/extracts/c/generated/internal/libcrux_core.h

@@ -7,8 +7,8 @@
  * Charon: 667d2fc98984ff7f3df989c2367e6c1fa4a000e7
  * Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
  * Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
- * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: 68dfed5a4a9e40277f62828471c029afed1ecdcc
+ * F*: unset
+ * Libcrux: bf73a8a7a0f119e66b105a3462265b4a2a3af63b
  */
 
 #ifndef internal_libcrux_core_H
@@ -38,11 +38,9 @@ static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1);
 
 static inline void core_num__u64__to_le_bytes(uint64_t x0, uint8_t x1[8U]);
 
-#define LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE ((size_t)32U)
-
 void libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_in_constant_time(
     Eurydice_slice lhs_c, Eurydice_slice rhs_c, Eurydice_slice lhs_s,
-    Eurydice_slice rhs_s, uint8_t ret[32U]);
+    Eurydice_slice rhs_s, Eurydice_slice out);
 
 #define LIBCRUX_ML_KEM_CONSTANTS_BITS_PER_COEFFICIENT ((size_t)12U)
 
@@ -58,6 +56,8 @@ void libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_i
 
 #define LIBCRUX_ML_KEM_CONSTANTS_H_DIGEST_SIZE ((size_t)32U)
 
+#define LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE ((size_t)32U)
+
 /**
  K * BITS_PER_RING_ELEMENT / 8
 
@@ -66,8 +66,6 @@ void libcrux_ml_kem_constant_time_ops_compare_ciphertexts_select_shared_secret_i
 */
 size_t libcrux_ml_kem_constants_ranked_bytes_per_ring_element(size_t rank);
 
-int16_t libcrux_secrets_int_I16(int16_t v);
-
 /**
 This function found in impl {libcrux_secrets::traits::Classify<T> for T}
 */
@@ -78,6 +76,16 @@ with types int16_t
 */
 int16_t libcrux_secrets_int_public_integers_classify_27_39(int16_t self);
 
+/**
+This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
+*/
+/**
+A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
+with types uint8_t
+
+*/
+uint8_t libcrux_secrets_int_public_integers_declassify_d8_90(uint8_t self);
+
 /**
 This function found in impl {libcrux_secrets::int::CastOps for u8}
 */
@@ -153,16 +161,6 @@ This function found in impl {libcrux_secrets::int::CastOps for i16}
 */
 int16_t libcrux_secrets_int_as_i16_f5(int16_t self);
 
-typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair1024_s {
-  uint8_t fst[1536U];
-  uint8_t snd[1568U];
-} libcrux_ml_kem_utils_extraction_helper_Keypair1024;
-
-typedef struct libcrux_ml_kem_utils_extraction_helper_Keypair768_s {
-  uint8_t fst[1152U];
-  uint8_t snd[1184U];
-} libcrux_ml_kem_utils_extraction_helper_Keypair768;
-
 /**
 This function found in impl
 {libcrux_ml_kem::types::MlKemKeyPair<PRIVATE_KEY_SIZE, PUBLIC_KEY_SIZE>}
@@ -190,15 +188,16 @@ libcrux_ml_kem_types_MlKemPrivateKey_83 libcrux_ml_kem_types_from_77_39(
     uint8_t value[3168U]);
 
 /**
-This function found in impl {libcrux_ml_kem::types::MlKemCiphertext<SIZE>}
+This function found in impl {core::default::Default for
+libcrux_ml_kem::types::MlKemCiphertext<SIZE>}
 */
 /**
-A monomorphic instance of libcrux_ml_kem.types.as_slice_a9
+A monomorphic instance of libcrux_ml_kem.types.default_73
 with const generics
 - SIZE= 1568
 */
-uint8_t *libcrux_ml_kem_types_as_slice_a9_af(
-    libcrux_ml_kem_types_MlKemCiphertext_64 *self);
+libcrux_ml_kem_types_MlKemCiphertext_64 libcrux_ml_kem_types_default_73_af(
+    void);
 
 /**
 This function found in impl
@@ -227,15 +226,16 @@ libcrux_ml_kem_types_MlKemPrivateKey_d9 libcrux_ml_kem_types_from_77_28(
     uint8_t value[2400U]);
 
 /**
-This function found in impl {libcrux_ml_kem::types::MlKemCiphertext<SIZE>}
+This function found in impl {core::default::Default for
+libcrux_ml_kem::types::MlKemCiphertext<SIZE>}
 */
 /**
-A monomorphic instance of libcrux_ml_kem.types.as_slice_a9
+A monomorphic instance of libcrux_ml_kem.types.default_73
 with const generics
 - SIZE= 1088
 */
-uint8_t *libcrux_ml_kem_types_as_slice_a9_80(
-    libcrux_ml_kem_mlkem768_MlKem768Ciphertext *self);
+libcrux_ml_kem_mlkem768_MlKem768Ciphertext libcrux_ml_kem_types_default_73_80(
+    void);
 
 /**
 This function found in impl {libcrux_ml_kem::types::MlKemPublicKey<SIZE>}
@@ -286,18 +286,6 @@ with const generics
 Eurydice_slice_uint8_t_x4 libcrux_ml_kem_types_unpack_private_key_b4(
     Eurydice_slice private_key);
 
-/**
-This function found in impl {core::convert::From<@Array<u8, SIZE>> for
-libcrux_ml_kem::types::MlKemCiphertext<SIZE>}
-*/
-/**
-A monomorphic instance of libcrux_ml_kem.types.from_e0
-with const generics
-- SIZE= 1088
-*/
-libcrux_ml_kem_mlkem768_MlKem768Ciphertext libcrux_ml_kem_types_from_e0_80(
-    uint8_t value[1088U]);
-
 /**
 A monomorphic instance of libcrux_ml_kem.utils.prf_input_inc
 with const generics
@@ -406,18 +394,6 @@ with const generics
 void libcrux_ml_kem_utils_into_padded_array_b6(Eurydice_slice slice,
                                                uint8_t ret[34U]);
 
-/**
-This function found in impl {core::convert::From<@Array<u8, SIZE>> for
-libcrux_ml_kem::types::MlKemCiphertext<SIZE>}
-*/
-/**
-A monomorphic instance of libcrux_ml_kem.types.from_e0
-with const generics
-- SIZE= 1568
-*/
-libcrux_ml_kem_types_MlKemCiphertext_64 libcrux_ml_kem_types_from_e0_af(
-    uint8_t value[1568U]);
-
 /**
 A monomorphic instance of libcrux_ml_kem.utils.prf_input_inc
 with const generics
@@ -471,72 +447,6 @@ with const generics
 void libcrux_ml_kem_utils_into_padded_array_24(Eurydice_slice slice,
                                                uint8_t ret[64U]);
 
-/**
-This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
-*/
-/**
-A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
-with types uint8_t[24size_t]
-
-*/
-void libcrux_secrets_int_public_integers_declassify_d8_d2(uint8_t self[24U],
-                                                          uint8_t ret[24U]);
-
-/**
-This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
-*/
-/**
-A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
-with types uint8_t[22size_t]
-
-*/
-void libcrux_secrets_int_public_integers_declassify_d8_fa(uint8_t self[22U],
-                                                          uint8_t ret[22U]);
-
-/**
-This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
-*/
-/**
-A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
-with types uint8_t[20size_t]
-
-*/
-void libcrux_secrets_int_public_integers_declassify_d8_57(uint8_t self[20U],
-                                                          uint8_t ret[20U]);
-
-/**
-This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
-*/
-/**
-A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
-with types uint8_t[10size_t]
-
-*/
-void libcrux_secrets_int_public_integers_declassify_d8_cc(uint8_t self[10U],
-                                                          uint8_t ret[10U]);
-
-/**
-This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
-*/
-/**
-A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
-with types uint8_t[8size_t]
-
-*/
-void libcrux_secrets_int_public_integers_declassify_d8_76(uint8_t self[8U],
-                                                          uint8_t ret[8U]);
-
-/**
-This function found in impl {libcrux_secrets::traits::Declassify<T> for T}
-*/
-/**
-A monomorphic instance of libcrux_secrets.int.public_integers.declassify_d8
-with types uint8_t[2size_t]
-
-*/
-void libcrux_secrets_int_public_integers_declassify_d8_d4(uint8_t self[2U],
-                                                          uint8_t ret[2U]);
-
 /**
  Classify a mutable slice (identity)
  We define a separate function for this because hax has limited support for
@@ -585,30 +495,6 @@ with types int16_t
 Eurydice_slice libcrux_secrets_int_classify_public_classify_ref_9b_39(
     Eurydice_slice self);
 
-/**
-A monomorphic instance of core.result.Result
-with types int16_t[16size_t], core_array_TryFromSliceError
-
-*/
-typedef struct core_result_Result_0a_s {
-  core_result_Result_fb_tags tag;
-  union {
-    int16_t case_Ok[16U];
-    core_array_TryFromSliceError case_Err;
-  } val;
-} core_result_Result_0a;
-
-/**
-This function found in impl {core::result::Result<T, E>[TraitClause@0,
-TraitClause@1]}
-*/
-/**
-A monomorphic instance of core.result.unwrap_26
-with types int16_t[16size_t], core_array_TryFromSliceError
-
-*/
-void core_result_unwrap_26_00(core_result_Result_0a self, int16_t ret[16U]);
-
 /**
 This function found in impl {libcrux_secrets::traits::Classify<T> for T}
 */