Merge pull request #622 from cryspen/franziskus/update-c-extraction

Update C extraction to toolchanges
cryspen · Oct 9, 2024 · 5b51960 · 5b51960
2 parents 897008e + 43aaf16
commit 5b51960
Show file tree

Hide file tree

Showing 48 changed files with 9,095 additions and 7,257 deletions.
diff --git a/.docker/c/ext-tools.sh b/.docker/c/ext-tools.sh
@@ -4,23 +4,23 @@ set -v -e -x
 
 source $HOME/.profile
 
-curl -L https://github.com/AeneasVerif/charon/archive/28d543bfacc902ba9cc2a734b76baae9583892a4.zip \
+curl -L https://github.com/AeneasVerif/charon/archive/45f5a34f336e35c6cc2253bc90cbdb8d812cefa9.zip \
     --output charon.zip
 unzip charon.zip
 rm -rf charon.zip
-mv charon-28d543bfacc902ba9cc2a734b76baae9583892a4/ charon
+mv charon-45f5a34f336e35c6cc2253bc90cbdb8d812cefa9/ charon
 
-curl -L https://github.com/FStarLang/karamel/archive/15d4bce74a2d43e34a64f48f8311b7d9bcb0e152.zip \
+curl -L https://github.com/FStarLang/karamel/archive/8c3612018c25889288da6857771be3ad03b75bcd.zip \
     --output karamel.zip
 unzip karamel.zip
 rm -rf karamel.zip
-mv karamel-15d4bce74a2d43e34a64f48f8311b7d9bcb0e152/ karamel
+mv karamel-8c3612018c25889288da6857771be3ad03b75bcd/ karamel
 
-curl -L https://github.com/AeneasVerif/eurydice/archive/1a65dbf3758fe310833718c645a64266294a29ac.zip \
+curl -L https://github.com/AeneasVerif/eurydice/archive/1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c.zip \
     --output eurydice.zip
 unzip eurydice.zip
 rm -rf eurydice.zip
-mv eurydice-1a65dbf3758fe310833718c645a64266294a29ac/ eurydice
+mv eurydice-1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c/ eurydice
 
 echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
 echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile

diff --git a/libcrux-ml-kem/c.yaml b/libcrux-ml-kem/c.yaml
@@ -37,14 +37,6 @@ files:
       - '"intrinsics/libcrux_intrinsics_arm64.h"'
 
   - name: libcrux_sha3_avx2
-    # This is needed solely for the benchmarking test -- otherwise these would
-    # all be private. Note that the order matters! So we put these first so that
-    # they match immediately (and get promoted to internal), then the rest of
-    # the behavior applies.
-    internal:
-      monomorphizations_exact:
-        - [libcrux_sha3, generic_keccak, absorb_final_7f ]
-        - [libcrux_sha3, generic_keccak, squeeze_first_three_blocks_ed ]
     api:
       - [libcrux_sha3, avx2, "*"]
     private:
@@ -59,7 +51,7 @@ files:
         - [libcrux_sha3, avx2, "*"]
         - [libcrux_sha3, simd, avx2, "*"]
       monomorphizations_exact:
-        - [libcrux_sha3, generic_keccak, KeccakState_29]
+        - [libcrux_sha3, generic_keccak, KeccakState_55]
     include_in_h:
       - '"intrinsics/libcrux_intrinsics_avx2.h"'
 

diff --git a/libcrux-ml-kem/c/benches/sha3.cc b/libcrux-ml-kem/c/benches/sha3.cc
@@ -58,29 +58,29 @@ sha3_512_64(benchmark::State &state)
 }
 
 #ifdef LIBCRUX_X64
-__attribute__((target("avx2"))) static void
-shake128_34_504(benchmark::State &state)
-{
-    uint8_t digest0[504];
-    uint8_t digest1[504];
-    uint8_t digest2[504];
-    uint8_t digest3[504];
-    uint8_t input[34];
-    generate_random(input, 34);
-
-    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)};
-    auto st = libcrux_sha3_avx2_x4_incremental_init();
-    libcrux_sha3_generic_keccak_absorb_final_7f(&st, last);
-    libcrux_sha3_generic_keccak_squeeze_first_three_blocks_ed(&st, out);
-
-    for (auto _ : state)
-    {
-        auto st = libcrux_sha3_avx2_x4_incremental_init();
-        libcrux_sha3_generic_keccak_absorb_final_7f(&st, last);
-        libcrux_sha3_generic_keccak_squeeze_first_three_blocks_ed(&st, out);
-    }
-}
+// __attribute__((target("avx2"))) static void
+// shake128_34_504(benchmark::State &state)
+// {
+//     uint8_t digest0[504];
+//     uint8_t digest1[504];
+//     uint8_t digest2[504];
+//     uint8_t digest3[504];
+//     uint8_t input[34];
+//     generate_random(input, 34);
+
+//     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)};
+//     auto st = libcrux_sha3_avx2_x4_incremental_init();
+//     libcrux_sha3_generic_keccak_absorb_final_7f(&st, last);
+//     libcrux_sha3_generic_keccak_squeeze_first_three_blocks_ed(&st, out);
+
+//     for (auto _ : state)
+//     {
+//         auto st = libcrux_sha3_avx2_x4_incremental_init();
+//         libcrux_sha3_generic_keccak_absorb_final_7f(&st, last);
+//         libcrux_sha3_generic_keccak_squeeze_first_three_blocks_ed(&st, out);
+//     }
+// }
 
 __attribute__((target("avx2"))) static void
 shake256_1120_32(benchmark::State &state)
@@ -130,7 +130,7 @@ shake256_33_128(benchmark::State &state)
 
 BENCHMARK(sha3_256_1184);
 BENCHMARK(sha3_512_64);
-BENCHMARK(shake128_34_504);
+// BENCHMARK(shake128_34_504);
 BENCHMARK(shake256_1120_32);
 BENCHMARK(shake256_33_128);
 #endif

diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -1,6 +1,6 @@
 This code was generated with the following revisions:
-Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4
-Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac
-Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152
+Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
+Eurydice: 1fff1c51ae6e6c87eafd28ec9d5594f54bc91c0c
+Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
 F*: 5643e656b989aca7629723653a2570c7df6252b9-dirty
-Libcrux: 97f7cefe14dabf275e4671ffea87e032d7779b71
+Libcrux: 2e8f138dbcbfbfabf4bbd994c8587ec00d197102