more updates

cryspen · Jun 28, 2024 · 43cab0a · 43cab0a
1 parent 58c79cd
commit 43cab0a
Show file tree

Hide file tree

Showing 11 changed files with 1,953 additions and 1,977 deletions.
diff --git a/.github/workflows/mlkem.yml b/.github/workflows/mlkem.yml
@@ -158,14 +158,16 @@ jobs:
           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 --no-dev-deps $RUST_TARGET_FLAG
+          cargo hack test --each-feature $EXCLUDE_FEATURES --verbose $RUST_TARGET_FLAG
 
   benchmarks:
     strategy:

diff --git a/libcrux-ml-kem/c.sh b/libcrux-ml-kem/c.sh
@@ -21,6 +21,7 @@ out=c
 glue=$EURYDICE_HOME/include/eurydice_glue.h
 features="--cargo-arg=--features=pre-verification"
 eurydice_glue=1
+unrolling=16
 
 # Parse command line arguments.
 all_args=("$@")
@@ -35,6 +36,7 @@ while [ $# -gt 0 ]; do
     --glue) glue="$2"; shift ;;
     --mlkem768) features="${features} --cargo-arg=--no-default-features --cargo-arg=--features=mlkem768" ;;
     --no-glue) eurydice_glue=0 ;;
+    --no-unrolling) unrolling=0 ;;
     esac
     shift
 done
@@ -72,7 +74,7 @@ if [[ "$clean" = 1 ]]; then
 fi
 
 echo "Running eurydice ..."
-$EURYDICE_HOME/eurydice --config ../$config ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc
+$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

diff --git a/libcrux-ml-kem/cg.yaml b/libcrux-ml-kem/cg.yaml
@@ -48,50 +48,6 @@ files:
       monomorphizations_using:
         - [libcrux_sha3, "*"]
 
-  # Common parts of SHA3 (this catches stuff that hasn't matched above). Must
-  # # come after the (more precise) patterns above concerning platform-specific hash_functions
-  # - name: libcrux_sha3_internal
-  #   api:
-  #     patterns:
-  #       - [libcrux_sha3, "*"]
-  #     monomorphizations_of:
-  #       - [libcrux_sha3, "*"]
-  #     monomorphizations_using:
-  #       - [libcrux_sha3, "*"]
-  #   inline_static: true
-
-  # MLKEM: HASH FUNCTIONS (as used by mlkem)
-
-  # - name: libcrux_mlkem_avx2
-  #   api:
-  #     - [libcrux_ml_kem, vector, avx2, "*"]
-  #     - [libcrux_ml_kem, hash_functions, avx2, "*"]
-  #   private:
-  #     monomorphizations_using:
-  #       - [libcrux_ml_kem, vector, avx2, "*"]
-  #       - [libcrux_ml_kem, hash_functions, avx2, "*"]
-  #     monomorphizations_of:
-  #       - [libcrux_ml_kem, vector, avx2, "*"]
-  #       - [libcrux_ml_kem, hash_functions, avx2, "*"]
-
-  # # This covers slightly more than the two bundles above, but this greatly
-  # # simplifies our lives.
-  # - name: libcrux_mlkem_portable
-  #   inline_static: true
-  #   api:
-  #     patterns:
-  #       - [libcrux_ml_kem, vector, "*"]
-  #       - [libcrux_ml_kem, hash_functions, portable, "*"]
-  #       - [ libcrux_ml_kem, polynomial, "*" ]
-  #     monomorphizations_using:
-  #       - [ libcrux_ml_kem, polynomial, "*" ]
-  #       - [libcrux_ml_kem, vector, "*"]
-  #       - [libcrux_ml_kem, hash_functions, portable, "*"]
-  #     monomorphizations_of:
-  #       - [ libcrux_ml_kem, polynomial, "*" ]
-  #       - [libcrux_ml_kem, vector, "*"]
-  #       - [libcrux_ml_kem, hash_functions, portable, "*"]
-
   # MLKEM: MISC NON-ARCHITECTURE SPECIFIC HEADERS
   - name: libcrux_core
     inline_static: true
@@ -139,7 +95,6 @@ files:
         - [libcrux_ml_kem, "*"]
         - [libcrux_ml_kem, vector, "*"]
         - [libcrux_ml_kem, hash_functions, portable, "*"]
-        # - [libcrux_ml_kem, polynomial, "*" ]
         - [libcrux_ml_kem, mlkem768, portable, "*"]
         - [libcrux_ml_kem, ind_cca, instantiations, portable, "*"]
       monomorphizations_of:

diff --git a/libcrux-ml-kem/cg/README.md b/libcrux-ml-kem/cg/README.md
@@ -11,7 +11,7 @@ While running the commands separately is possible, it is not recommended because
 the script sets all necessary configuration flags.
 
 ```bash
-./c.sh --config cg.yaml --out cg --mlkem768 --no-glue
+./c.sh --config cg.yaml --out cg --mlkem768 --no-glue --no-unrolling
 ```
 
 ## Build

diff --git a/libcrux-ml-kem/cg/eurydice_glue.h b/libcrux-ml-kem/cg/eurydice_glue.h
@@ -129,13 +129,6 @@ static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x, uint8_t y) {
   return x - y;
 }
 
-// static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) {
-//   return (*p) & v;
-// }
-// static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) {
-//   return (*p) >> v;
-// }
-
 // ITERATORS
 
 #define Eurydice_range_iter_next(iter_ptr, t, ret_t) \

diff --git a/libcrux-ml-kem/cg/karamel/target.h b/libcrux-ml-kem/cg/karamel/target.h
@@ -4,8 +4,6 @@
 #ifndef __KRML_TARGET_H
 #define __KRML_TARGET_H
 
-/* For "bare" targets that do not have a C stdlib, the user might want to use
- * [-add-early-include '"mydefinitions.h"'] and override these. */
 #ifndef KRML_HOST_PRINTF
 #  define KRML_HOST_PRINTF printf
 #endif
@@ -23,190 +21,4 @@
 #  define KRML_HOST_EXIT exit
 #endif
 
-/* Macros for prettier unrolling of loops */
-#define KRML_LOOP1(i, n, x) { \
-  x \
-  i += n; \
-  (void) i; \
-}
-
-#define KRML_LOOP2(i, n, x)                                                    \
-  KRML_LOOP1(i, n, x)                                                          \
-  KRML_LOOP1(i, n, x)
-
-#define KRML_LOOP3(i, n, x)                                                    \
-  KRML_LOOP2(i, n, x)                                                          \
-  KRML_LOOP1(i, n, x)
-
-#define KRML_LOOP4(i, n, x)                                                    \
-  KRML_LOOP2(i, n, x)                                                          \
-  KRML_LOOP2(i, n, x)
-
-#define KRML_LOOP5(i, n, x)                                                    \
-  KRML_LOOP4(i, n, x)                                                          \
-  KRML_LOOP1(i, n, x)
-
-#define KRML_LOOP6(i, n, x)                                                    \
-  KRML_LOOP4(i, n, x)                                                          \
-  KRML_LOOP2(i, n, x)
-
-#define KRML_LOOP7(i, n, x)                                                    \
-  KRML_LOOP4(i, n, x)                                                          \
-  KRML_LOOP3(i, n, x)
-
-#define KRML_LOOP8(i, n, x)                                                    \
-  KRML_LOOP4(i, n, x)                                                          \
-  KRML_LOOP4(i, n, x)
-
-#define KRML_LOOP9(i, n, x)                                                    \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP1(i, n, x)
-
-#define KRML_LOOP10(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP2(i, n, x)
-
-#define KRML_LOOP11(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP3(i, n, x)
-
-#define KRML_LOOP12(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP4(i, n, x)
-
-#define KRML_LOOP13(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP5(i, n, x)
-
-#define KRML_LOOP14(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP6(i, n, x)
-
-#define KRML_LOOP15(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP7(i, n, x)
-
-#define KRML_LOOP16(i, n, x)                                                   \
-  KRML_LOOP8(i, n, x)                                                          \
-  KRML_LOOP8(i, n, x)
-
-#define KRML_UNROLL_FOR(i, z, n, k, x)                                         \
-  do {                                                                         \
-    uint32_t i = z;                                                            \
-    KRML_LOOP##n(i, k, x)                                                      \
-  } while (0)
-
-#define KRML_ACTUAL_FOR(i, z, n, k, x)                                         \
-  do {                                                                         \
-    for (uint32_t i = z; i < n; i += k) {                                      \
-      x                                                                        \
-    }                                                                          \
-  } while (0)
-
-#ifndef KRML_UNROLL_MAX
-#  define KRML_UNROLL_MAX 0
-#endif
-
-/* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */
-#if 0 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR0(i, z, n, k, x)
-#else
-#  define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 1 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x)
-#else
-#  define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 2 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x)
-#else
-#  define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 3 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x)
-#else
-#  define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 4 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x)
-#else
-#  define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 5 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x)
-#else
-#  define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 6 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x)
-#else
-#  define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 7 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x)
-#else
-#  define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 8 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x)
-#else
-#  define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 9 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x)
-#else
-#  define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 10 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x)
-#else
-#  define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 11 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x)
-#else
-#  define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 12 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x)
-#else
-#  define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 13 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x)
-#else
-#  define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 14 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x)
-#else
-#  define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 15 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x)
-#else
-#  define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
-
-#if 16 <= KRML_UNROLL_MAX
-#  define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x)
-#else
-#  define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
-#endif
 #endif
diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../cg.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version:
+  <unknown> KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_core_H