fixups

.github/workflows/c.yml

@@ -50,9 +50,10 @@ jobs:
           cmake -B build -DCMAKE_BUILD_TYPE=Release
           cmake --build build --config Release
 
-      - name: 🏃🏻‍♀️ Benchmark
-        run: ./build/Release/ml_kem_bench
-        if: ${{ matrix.os == 'windows-latest' }}
+      # FIXME: Benchmarks on Windows CI are not working right now.
+      # - name: 🏃🏻‍♀️ Benchmark
+      #   run: ./build/Release/ml_kem_bench
+      #   if: ${{ matrix.os == 'windows-latest' }}
 
       - name: 🏃🏻‍♀️ Benchmark
         run: ./build/ml_kem_bench

libcrux-ml-kem/c.sh

@@ -68,3 +68,15 @@ cp $EURYDICE_HOME/include/eurydice_glue.h .
 clang-format --style=Google -i *.c *.h
 clang-format --style=Google -i internal/*.h
 clang-format --style=Google -i intrinsics/*.h
+
+# Write out infos about the used tools
+rm -f code_gen.txt
+echo "This code was generated with the following tools:" >> code_gen.txt
+echo -n "Charon: " >> code_gen.txt
+git -C $CHARON_HOME rev-parse HEAD >> code_gen.txt
+echo -n "Eurydice: " >> code_gen.txt
+git -C $EURYDICE_HOME rev-parse HEAD >> code_gen.txt
+echo -n "Karamel: " >> code_gen.txt
+git -C $KRML_HOME rev-parse HEAD >> code_gen.txt
+echo -n "F*: " >> code_gen.txt
+git -C $FSTAR_HOME rev-parse HEAD >> code_gen.txt

libcrux-ml-kem/c.yaml

@@ -13,10 +13,6 @@ files:
     api:
       - [libcrux_intrinsics, avx2]
 
-  - name: libcrux_platform
-    private:
-      - [libcrux_platform, "*"]
-
   # SHA3 (no mention of libcrux_mlkem in this section, please)
 
   # Keep the per-target seperation idea: each SHA3 variant in its own file
@@ -158,7 +154,7 @@ files:
         - [ core, "*"]
         - [ libcrux_ml_kem, types, "*"]
         - [ libcrux_ml_kem, constant_time_ops, "*"]
-        - [ libcrux_ml_kem, utils ]
+        - [ libcrux_ml_kem, utils, "*" ]
       monomorphizations_using:
         - [ Eurydice, "*" ]
         - [ libcrux_ml_kem, types, "*"]
@@ -167,7 +163,7 @@ files:
         - [ libcrux_ml_kem, types ]
         - [ libcrux_ml_kem, constants ]
         - [ libcrux_ml_kem, constant_time_ops, "*"]
-        - [ libcrux_ml_kem, utils ]
+        - [ libcrux_ml_kem, utils, "*" ]
     api:
       - [Eurydice, "*"]
 

libcrux-ml-kem/c/CMakeLists.txt

@@ -88,7 +88,7 @@ if(CMAKE_SYSTEM_PROCESSOR MATCHES "x86_64|amd64|AMD64")
 endif()
 
 # This is only for local testing and we assume neon on arm64.
-if(CMAKE_SYSTEM_PROCESSOR MATCHES "aarch64|arm64|arm64v8" AND DEFINED $ENV{LIBCRUX_NEON})
+if(CMAKE_SYSTEM_PROCESSOR MATCHES "aarch64|arm64|arm64v8" AND DEFINED ENV{LIBCRUX_NEON})
     message(STATUS "Detected an arm64 architecture")
     add_compile_definitions(LIBCRUX_AARCH64)
 

libcrux-ml-kem/c/README.md

@@ -17,6 +17,8 @@ cmake -B build -G "Ninja Multi-Config"
 cmake --build build
 ```
 
+To enable neon builds, set `LIBCRUX_NEON=1`.
+
 ### Test
 
 ```bash

libcrux-ml-kem/src/ind_cca.rs

@@ -4,10 +4,10 @@ use crate::{
     },
     constants::{CPA_PKE_KEY_GENERATION_SEED_SIZE, H_DIGEST_SIZE, SHARED_SECRET_SIZE},
     hash_functions::Hash,
-    utils::into_padded_array,
     ind_cpa::serialize_public_key,
     serialize::deserialize_ring_elements_reduced,
     types::{MlKemCiphertext, MlKemKeyPair, MlKemPrivateKey, MlKemPublicKey},
+    utils::into_padded_array,
     vector::Operations,
 };
 

libcrux-ml-kem/src/ind_cpa.rs

@@ -13,8 +13,8 @@ use crate::{
         deserialize_then_decompress_ring_element_v, deserialize_to_uncompressed_ring_element,
         serialize_uncompressed_ring_element,
     },
-    vector::Operations,
     utils::into_padded_array,
+    vector::Operations,
 };
 
 /// Concatenate `t` and `ρ` into the public key.

libcrux-ml-kem/src/mlkem1024.rs

@@ -21,9 +21,9 @@ const VECTOR_V_COMPRESSION_FACTOR_1024: usize = 5;
 const C2_SIZE_1024: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_1024) / 8;
 const CPA_PKE_SECRET_KEY_SIZE_1024: usize =
     (RANK_1024 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8;
-const CPA_PKE_PUBLIC_KEY_SIZE_1024: usize = T_AS_NTT_ENCODED_SIZE_1024 + 32;
+pub(crate) const CPA_PKE_PUBLIC_KEY_SIZE_1024: usize = T_AS_NTT_ENCODED_SIZE_1024 + 32;
 const CPA_PKE_CIPHERTEXT_SIZE_1024: usize = C1_SIZE_1024 + C2_SIZE_1024;
-const SECRET_KEY_SIZE_1024: usize = CPA_PKE_SECRET_KEY_SIZE_1024
+pub(crate) const SECRET_KEY_SIZE_1024: usize = CPA_PKE_SECRET_KEY_SIZE_1024
     + CPA_PKE_PUBLIC_KEY_SIZE_1024
     + H_DIGEST_SIZE
     + SHARED_SECRET_SIZE;

libcrux-ml-kem/src/mlkem512.rs

@@ -21,9 +21,9 @@ const VECTOR_V_COMPRESSION_FACTOR_512: usize = 4;
 const C2_SIZE_512: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_512) / 8;
 const CPA_PKE_SECRET_KEY_SIZE_512: usize =
     (RANK_512 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8;
-const CPA_PKE_PUBLIC_KEY_SIZE_512: usize = T_AS_NTT_ENCODED_SIZE_512 + 32;
+pub(crate) const CPA_PKE_PUBLIC_KEY_SIZE_512: usize = T_AS_NTT_ENCODED_SIZE_512 + 32;
 const CPA_PKE_CIPHERTEXT_SIZE_512: usize = C1_SIZE_512 + C2_SIZE_512;
-const SECRET_KEY_SIZE_512: usize =
+pub(crate) const SECRET_KEY_SIZE_512: usize =
     CPA_PKE_SECRET_KEY_SIZE_512 + CPA_PKE_PUBLIC_KEY_SIZE_512 + H_DIGEST_SIZE + SHARED_SECRET_SIZE;
 
 const ETA1: usize = 3;

libcrux-ml-kem/src/mlkem768.rs

@@ -21,7 +21,7 @@ const VECTOR_V_COMPRESSION_FACTOR_768: usize = 4;
 const C2_SIZE_768: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_768) / 8;
 const CPA_PKE_SECRET_KEY_SIZE_768: usize =
     (RANK_768 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8;
-const CPA_PKE_PUBLIC_KEY_SIZE_768: usize = T_AS_NTT_ENCODED_SIZE_768 + 32;
+pub(crate) const CPA_PKE_PUBLIC_KEY_SIZE_768: usize = T_AS_NTT_ENCODED_SIZE_768 + 32;
 // These two are used in the hybrid kem. This could probably be improved.
 pub(crate) const CPA_PKE_CIPHERTEXT_SIZE_768: usize = C1_SIZE_768 + C2_SIZE_768;
 pub(crate) const SECRET_KEY_SIZE_768: usize =

libcrux-ml-kem/src/utils.rs

@@ -1,3 +1,4 @@
+// C extraction:
 // A couple helper functions and definitions -- this file ends up being bundled in
 // libcrux_core.{c,h}, so if you need something that has to be shared across multiple mlkem
 // instances / implementations, it can go in here.
@@ -11,6 +12,10 @@ pub(crate) fn into_padded_array<const LEN: usize>(slice: &[u8]) -> [u8; LEN] {
     out
 }
 
+// C extraction:
+//
+// This is only enabled when extracting.
+//
 // Without these type abbreviations, the monomorphized definitions end up being inserted at the
 // first location that they are used, which might be, e.g., the avx2 impl of mlkem512, resulting in
 // the portable impl of mlkem512 including the header for the avx2 impl of mlkem512 to have this
@@ -19,7 +24,10 @@ pub(crate) fn into_padded_array<const LEN: usize>(slice: &[u8]) -> [u8; LEN] {
 // To avoid that, we manually place those definitions in this file, which ends up in a shared
 // header.
 //
-// TODO: use proper constants
-type Keypair512 = ([u8; 768], [u8;800]);
-type Keypair768 = ([u8; 1152], [u8;1184]);
-type Keypair1024 = ([u8; 1536], [u8;1568]);
+// TODO: use proper constants. They don't work right now ...
+#[cfg(eurydice)]
+mod extraction_helper {
+    type Keypair512 = ([u8; 768], [u8; 800]);
+    type Keypair768 = ([u8; 1152], [u8; 1184]);
+    type Keypair1024 = ([u8; 1536], [u8; 1568]);
+}