Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update C extraction to toolchanges #622

Merged
merged 3 commits into from
Oct 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .docker/c/ext-tools.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 1 addition & 9 deletions libcrux-ml-kem/c.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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"'

Expand Down
48 changes: 24 additions & 24 deletions libcrux-ml-kem/c/benches/sha3.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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
franziskuskiefer marked this conversation as resolved.
Show resolved Hide resolved
// 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)
Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions libcrux-ml-kem/c/code_gen.txt
Original file line number Diff line number Diff line change
@@ -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
Loading
Loading