Make verified ML-KEM available in libcrux-ml-kem (#329)

* Revert changes to Kyber (Round 3) for ML-KEM

* Fix swapped private key decoding

* Pull out Kyber encaps

* Make Kyber API available behind `kyber` feature

* Format

* Introduce `kyber` feature in `libcrux-kem`

* Format

* Include verified ML-KEM in `libcrux-ml-kem`

* WIP separation of verified API

* Integrating pre-verification and verified testing

* Integrating verified ML-KEM in `libcrux-kem`

* Format

* Test portable pre-verification ML-KEM 768

* fix C extraction

* Fix typo

* Give more accurate test names (`kyber...` to `mlkem...`)

* Avoid unused warning when testing

* Use `Hasher` trait to select best KDF for Kyber

* Document differences between Kyber (Round 3) and ML-KEM

* Inline ML-KEM/Kyber variant differences

* `kyber{512,768,1024}` top level modules

* Fix `kyber` feature in `libcrux-kem`

* Rename NIST KAT files for ML-KEM

* Include NIST KATs for all Kyber parameter sets

* Document single Kyber 768 KAT from boringssl

* Format

* Test Kyber on CI

* Fix insufficient feature gating

* Get rid of various warnings

* Format

* Remove commented `use` declarations

* Fix `unused_mut` warning

* Feature gating helper macros

* Fix hax extraction

* Feature flag documentation

* Fix mistaken feature guards

* Remove commented code

* `size` -> `len`

* Drop explicit dependency on `hax-lib-macros`

* Hide helper macro docs

* Formatting

* Call out the `kyber` feature more prominently

* Feature gate tests etc so `--no-std-features` tests

* cleanup; make features work

* more cleanup and docs

* update hax extraction

* fixup x64 and hax extract

* update C extraction

* update header only C code

* update C code

* install cargo hack on ci

* ci

* more updates

---------

Co-authored-by: Franziskus Kiefer <franziskuskiefer@gmail.com>

.github/workflows/mlkem.yml

@@ -40,13 +40,20 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
+      - uses: taiki-e/install-action@cargo-hack
 
       - name: Update dependencies
         run: cargo update
 
       - run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
         if: ${{ matrix.bits == 64 }}
 
+      - run: echo 'EXCLUDE_FEATURES=--exclude-features simd256' > $GITHUB_ENV
+        if: ${{ matrix.os == 'macos-latest' }}
+
+      - run: echo 'EXCLUDE_FEATURES=--exclude-features simd128' > $GITHUB_ENV
+        if: ${{ matrix.os != 'macos-latest' }}
+
       - name: 🛠️ Setup Rust Nightly
         run: rustup toolchain install nightly
 
@@ -150,6 +157,17 @@ jobs:
           cargo clean
           cargo test --features kyber --verbose $RUST_TARGET_FLAG
 
+      - name: 🏃🏻‍♀️ Cargo Check Features
+        if: ${{ matrix.bits == 64 }}
+        run: |
+          cargo clean
+          cargo hack check --feature-powerset $EXCLUDE_FEATURES --verbose --no-dev-deps $RUST_TARGET_FLAG
+
+      - name: 🏃🏻‍♀️ Cargo Test Features
+        if: ${{ matrix.bits == 64 }}
+        run: |
+          cargo clean
+          cargo hack test --each-feature $EXCLUDE_FEATURES --verbose $RUST_TARGET_FLAG
 
   benchmarks:
     strategy:

Cargo.toml

@@ -14,7 +14,8 @@ members = [
     "libcrux-kem",
     "libcrux-hmac",
     "libcrux-hkdf",
-    "libcrux-ecdh", "libcrux-psq",
+    "libcrux-ecdh",
+    "libcrux-psq",
 ]
 
 [workspace.package]

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

@@ -3,12 +3,6 @@ module Libcrux_intrinsics.Avx2
 open Core
 open FStar.Mul
 
-unfold
-let t_Vec128 = Core.Core_arch.X86.t____m128i
-
-unfold
-let t_Vec256 = Core.Core_arch.X86.t____m256i
-
 val mm256_add_epi16 (lhs rhs: Core.Core_arch.X86.t____m256i)
     : Prims.Pure Core.Core_arch.X86.t____m256i Prims.l_True (fun _ -> Prims.l_True)
 

libcrux-kem/Cargo.toml

@@ -17,10 +17,10 @@ libcrux-sha3 = { version = "0.0.2-pre.2", path = "../libcrux-sha3" }
 libcrux-ecdh = { version = "0.0.2-pre.2", path = "../libcrux-ecdh" }
 rand = { version = "0.8" }
 
-
 [features]
-tests = [] # Expose functions for testing.
+tests = []                                             # Expose functions for testing.
 kyber = ["libcrux-ml-kem/kyber"]
+pre-verification = ["libcrux-ml-kem/pre-verification"]
 
 [dev-dependencies]
 libcrux-kem = { version = "0.0.2-pre.2", path = "./", features = ["tests"] }

libcrux-kem/src/kem.rs

@@ -827,6 +827,26 @@ impl Ct {
                     ct_x.try_into().map_err(|_| Error::InvalidCiphertext)?,
                 ))
             }
+            #[cfg(feature = "kyber")]
+            Algorithm::X25519Kyber768Draft00 => {
+                let key: [u8; MlKem768Ciphertext::len() + 32] =
+                    bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;
+                let (xct, kct) = key.split_at(32);
+                Ok(Self::X25519Kyber768Draft00(
+                    kct.try_into().map_err(|_| Error::InvalidCiphertext)?,
+                    xct.try_into().map_err(|_| Error::InvalidCiphertext)?,
+                ))
+            }
+            #[cfg(feature = "kyber")]
+            Algorithm::XWingKyberDraft02 => {
+                let key: [u8; MlKem768Ciphertext::len() + 32] =
+                    bytes.try_into().map_err(|_| Error::InvalidCiphertext)?;
+                let (ct_m, ct_x) = key.split_at(MlKem768Ciphertext::len());
+                Ok(Self::XWingKyberDraft02(
+                    ct_m.try_into().map_err(|_| Error::InvalidCiphertext)?,
+                    ct_x.try_into().map_err(|_| Error::InvalidCiphertext)?,
+                ))
+            }
             Algorithm::MlKem1024 => bytes
                 .try_into()
                 .map_err(|_| Error::InvalidCiphertext)

libcrux-ml-dsa/src/hash_functions.rs

@@ -7,29 +7,29 @@ pub(crate) fn H<const OUTPUT_LENGTH: usize>(input: &[u8]) -> [u8; OUTPUT_LENGTH]
 }
 
 pub(crate) mod H_128 {
-    use libcrux_sha3::portable::{incremental, KeccakState1};
+    use libcrux_sha3::portable::{incremental, KeccakState};
 
     const BLOCK_SIZE: usize = 168;
     const FIVE_BLOCKS_SIZE: usize = BLOCK_SIZE * 5;
 
     #[inline(always)]
-    pub(crate) fn new(seed: [u8; 34]) -> KeccakState1 {
+    pub(crate) fn new(seed: [u8; 34]) -> KeccakState {
         let mut state = incremental::shake128_init();
         incremental::shake128_absorb_final(&mut state, &seed);
 
         state
     }
 
     #[inline(always)]
-    pub(crate) fn squeeze_first_five_blocks(state: &mut KeccakState1) -> [u8; FIVE_BLOCKS_SIZE] {
+    pub(crate) fn squeeze_first_five_blocks(state: &mut KeccakState) -> [u8; FIVE_BLOCKS_SIZE] {
         let mut out = [0u8; FIVE_BLOCKS_SIZE];
         incremental::shake128_squeeze_first_five_blocks(state, &mut out);
 
         out
     }
 
     #[inline(always)]
-    pub(crate) fn squeeze_next_block(state: &mut KeccakState1) -> [u8; BLOCK_SIZE] {
+    pub(crate) fn squeeze_next_block(state: &mut KeccakState) -> [u8; BLOCK_SIZE] {
         let mut out = [0u8; BLOCK_SIZE];
         incremental::shake128_squeeze_next_block(state, &mut out);
 

libcrux-ml-kem/Cargo.toml

@@ -29,15 +29,28 @@ libcrux-intrinsics = { version = "0.0.2-pre.2", path = "../libcrux-intrinsics" }
 hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax/" }
 
 [features]
+# By default all variants and std are enabled.
 default = ["std", "mlkem512", "mlkem768", "mlkem1024"]
+
+# Hardware features can be force enabled.
+# It is not recommended to use these. This crate performs CPU feature detection
+# and enables the features when they are available.
 simd128 = ["libcrux-sha3/simd128"]
 simd256 = ["libcrux-sha3/simd256"]
+
+# Features for the different key sizes of ML-KEM
 mlkem512 = []
 mlkem768 = []
 mlkem1024 = []
-std = []
+
+# Enable Round 3 Kyber in addition to ML-KEM
 kyber = []
 
+# Code that is not yet verified
+pre-verification = []
+
+std = []
+
 [dev-dependencies]
 rand = { version = "0.8" }
 serde_json = { version = "1.0" }
@@ -48,3 +61,26 @@ criterion = "0.5"
 [[bench]]
 name = "ml-kem"
 harness = false
+
+[[example]]
+name = "encapsulate"
+required-features = ["mlkem768"]
+
+[[example]]
+name = "decapsulate"
+required-features = ["mlkem768"]
+
+[[example]]
+name = "keygen"
+required-features = ["mlkem768"]
+
+[package.metadata."docs.rs"]
+features = ["pre-verification", "kyber"]
+rustdoc-args = ["--cfg", "doc_cfg"]
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = [
+    'cfg(hax)',
+    'cfg(eurydice)',
+    'cfg(doc_cfg)',
+] }

libcrux-ml-kem/c.sh

@@ -19,7 +19,9 @@ clean=0
 config=c.yaml
 out=c
 glue=$EURYDICE_HOME/include/eurydice_glue.h
-features=
+features="--cargo-arg=--features=pre-verification"
+eurydice_glue=1
+unrolling=16
 
 # Parse command line arguments.
 all_args=("$@")
@@ -32,7 +34,9 @@ while [ $# -gt 0 ]; do
     --config) config="$2"; shift ;;
     --out) out="$2"; shift ;;
     --glue) glue="$2"; shift ;;
-    --mlkem768) features="--cargo-arg=--no-default-features --cargo-arg=--features=mlkem768" ;;
+    --mlkem768) features="${features} --cargo-arg=--no-default-features --cargo-arg=--features=mlkem768" ;;
+    --no-glue) eurydice_glue=0 ;;
+    --no-unrolling) unrolling=0 ;;
     esac
     shift
 done
@@ -70,8 +74,10 @@ if [[ "$clean" = 1 ]]; then
 fi
 
 echo "Running eurydice ..."
-$EURYDICE_HOME/eurydice --config ../$config ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc
-cp $EURYDICE_HOME/include/eurydice_glue.h .
+$EURYDICE_HOME/eurydice --config ../$config -funroll-loops $unrolling ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc
+if [[ "$eurydice_glue" = 1 ]]; then
+    cp $EURYDICE_HOME/include/eurydice_glue.h .
+fi
 
 clang-format --style=Google -i *.c *.h
 clang-format --style=Google -i internal/*.h
@@ -81,7 +87,11 @@ clang-format --style=Google -i intrinsics/*.h
 [[ -z "$CHARON_REV" && -d $CHARON_HOME/.git ]] && export CHARON_REV=$(git -C $CHARON_HOME rev-parse HEAD)
 [[ -z "$EURYDICE_REV" && -d $EURYDICE_HOME/.git ]] && export EURYDICE_REV=$(git -C $EURYDICE_HOME rev-parse HEAD)
 [[ -z "$KRML_REV" && -d $KRML_HOME/.git ]] && export KRML_REV=$(git -C $KRML_HOME rev-parse HEAD)
-[[ -z "$FSTAR_REV" && -d $FSTAR_HOME/.git ]] && export FSTAR_REV=$(git -C $FSTAR_HOME rev-parse HEAD)
+if [[ -z "$FSTAR_REV" && -d $FSTAR_HOME/.git ]]; then
+    export FSTAR_REV=$(git -C $FSTAR_HOME rev-parse HEAD)
+else
+    export FSTAR_REV=$(fstar.exe --version | grep commit | sed 's/commit=\(.*\)/\1/')
+fi
 rm -f code_gen.txt
 echo "This code was generated with the following tools:" >> code_gen.txt
 echo -n "Charon: " >> code_gen.txt

libcrux-ml-kem/c/benches/sha3.cc

@@ -71,13 +71,13 @@ shake128_34_504(benchmark::State &state)
 
     Eurydice_slice last[4] = {EURYDICE_SLICE(input, 0, 34), EURYDICE_SLICE(input, 0, 34), EURYDICE_SLICE(input, 0, 34), EURYDICE_SLICE(input, 0, 34)};
     Eurydice_slice out[4] = {EURYDICE_SLICE(digest0, 0, 504), EURYDICE_SLICE(digest1, 0, 504), EURYDICE_SLICE(digest2, 0, 504), EURYDICE_SLICE(digest3, 0, 504)};
-    libcrux_sha3_avx2_x4_incremental_KeccakState4 st = libcrux_sha3_avx2_x4_incremental_shake128_init();
+    libcrux_sha3_avx2_x4_incremental_KeccakState st = libcrux_sha3_avx2_x4_incremental_shake128_init();
     libcrux_sha3_generic_keccak_absorb_final__core_core_arch_x86___m256i_4size_t_168size_t_31uint8_t(&st, last);
     libcrux_sha3_generic_keccak_squeeze_first_three_blocks__core_core_arch_x86___m256i_4size_t_168size_t(&st, out);
 
     for (auto _ : state)
     {
-        libcrux_sha3_avx2_x4_incremental_KeccakState4 st = libcrux_sha3_avx2_x4_incremental_shake128_init();
+        libcrux_sha3_avx2_x4_incremental_KeccakState st = libcrux_sha3_avx2_x4_incremental_shake128_init();
         libcrux_sha3_generic_keccak_absorb_final__core_core_arch_x86___m256i_4size_t_168size_t_31uint8_t(&st, last);
         libcrux_sha3_generic_keccak_squeeze_first_three_blocks__core_core_arch_x86___m256i_4size_t_168size_t(&st, out);
     }

libcrux-ml-kem/c/code_gen.txt

@@ -1,5 +1,5 @@
 This code was generated with the following tools:
-Charon: ae55966c01a1a4b185a1a34da7861ba5db74c8ad
-Eurydice: bbfd102bbfbc3e4c362953f093dbfd65e2fbc10c
+Charon: 23f20c184e51015582b7918ea4f1eb063b28daba
+Eurydice: 30fdb50add4dabaee90051878c166bac8c5ac26a
 Karamel: 42a431696cd32d41155d7e484720eb71fd5dc7b1
-F*: f09228ef9a64ac4ef383ee0e10656ccb612db2ee
+F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty

libcrux-ml-kem/c/eurydice_glue.h

@@ -85,7 +85,7 @@ typedef struct {
 
 #define Eurydice_array_eq(sz, a1, a2, t, _, _ret_t) \
   (memcmp(a1, a2, sz * sizeof(t)) == 0)
-#define core_array_equality___core__cmp__PartialEq__Array_B__N___for__Array_A__N____eq \
+#define core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq \
   Eurydice_array_eq
 
 #define core_slice___Slice_T___split_at(slice, mid, element_type, ret_t) \
@@ -135,6 +135,21 @@ core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x) {
   return x;
 }
 
+static inline uint64_t
+core_convert_num___core__convert__From_u8__for_u64__66__from(uint8_t x) {
+  return x;
+}
+
+static inline uint64_t
+core_convert_num___core__convert__From_u16__for_u64__70__from(uint16_t x) {
+  return x;
+}
+
+static inline size_t
+core_convert_num___core__convert__From_u16__for_usize__96__from(uint16_t x) {
+  return x;
+}
+
 static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) {
 #ifdef _MSC_VER
   return __popcnt(x0);
@@ -163,9 +178,14 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
   return (*p) >> v;
 }
 
-// ITERATORS
+#define core_num_nonzero_private_NonZeroUsizeInner size_t
+static inline core_num_nonzero_private_NonZeroUsizeInner
+core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner__26__clone(
+    core_num_nonzero_private_NonZeroUsizeInner *x0) {
+  return *x0;
+}
 
-#define core_num_nonzero_NonZeroUsize size_t
+// ITERATORS
 #define Eurydice_range_iter_next(iter_ptr, t, ret_t) \
   (((iter_ptr)->start == (iter_ptr)->end)            \
        ? (CLITERAL(ret_t){.tag = core_option_None})  \
@@ -183,6 +203,9 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
 #define Eurydice_into_iter(x, t, _ret_t) (x)
 #define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter \
   Eurydice_into_iter
+// This name changed on 20240627
+#define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I__1__into_iter \
+  Eurydice_into_iter
 
 typedef struct {
   Eurydice_slice slice;
@@ -214,11 +237,15 @@ static inline Eurydice_slice chunk_next(Eurydice_chunks *chunks,
       .chunk_size = sz_})
 #define core_slice_iter_Chunks Eurydice_chunks
 #define core_slice_iter_ChunksExact Eurydice_chunks
-#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___70__next( \
-    iter, t, ret_t)                                                                                              \
-  (((iter)->slice.len == 0) ? ((ret_t){.tag = core_option_None})                                                 \
-                            : ((ret_t){.tag = core_option_Some,                                                  \
+#define Eurydice_chunks_next(iter, t, ret_t)                     \
+  (((iter)->slice.len == 0) ? ((ret_t){.tag = core_option_None}) \
+                            : ((ret_t){.tag = core_option_Some,  \
                                        .f0 = chunk_next(iter, sizeof(t))}))
+#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___70__next \
+  Eurydice_chunks_next
+// This name changed on 20240627
+#define core_slice_iter___core__iter__traits__iterator__Iterator_for_core__slice__iter__Chunks__a__T___71__next \
+  Eurydice_chunks_next
 #define core_slice_iter__core__slice__iter__ChunksExact__a__T__89__next( \
     iter, t, _ret_t)                                                     \
   core_slice_iter__core__slice__iter__Chunks__a__T__70__next(iter, t)