Skip to content

Commit

Permalink
Merge pull request #707 from cryspen/franziskus/mldsa-c1
Browse files Browse the repository at this point in the history
First changes for ML-DSA C extraction
  • Loading branch information
franziskuskiefer authored Dec 10, 2024
2 parents 116d987 + 1214cd7 commit 767c2a7
Show file tree
Hide file tree
Showing 60 changed files with 2,311 additions and 2,352 deletions.
15 changes: 11 additions & 4 deletions libcrux-ml-dsa/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -32,9 +32,18 @@ criterion = "0.5"
pqcrypto-dilithium = { version = "0.5.0" } #, default-features = false

[features]
default = ["std", "mldsa44", "mldsa65", "mldsa87"]
simd128 = ["libcrux-sha3/simd128", "libcrux-intrinsics/simd128"]
simd256 = ["libcrux-sha3/simd256", "libcrux-intrinsics/simd256"]
acvp = [] # expose internal API for ACVP testing
acvp = [] # expose internal API for ACVP testing

# Features for the different key sizes of ML-DSA
mldsa44 = []
mldsa65 = []
mldsa87 = []

# std support
std = []

[[bench]]
name = "manual44"
Expand All @@ -53,6 +62,4 @@ name = "ml-dsa"
harness = false

[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = [
'cfg(hax)',
] }
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)'] }
41 changes: 41 additions & 0 deletions libcrux-ml-dsa/boring.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
#!/bin/bash

set -e

SED=$(which gsed &>/dev/null && echo gsed || echo sed)

no_clean=0

# Parse command line arguments.
all_args=("$@")
while [ $# -gt 0 ]; do
case "$1" in
--no-clean) no_clean=1 ;;
esac
shift
done

# Extract the C code
if [[ "$no_clean" = 0 ]]; then
cargo clean
fi
# TODO: add feature flags for mldsa65
./c.sh --config cg.yaml --out cg --mldsa65\
--no-glue --no-unrolling --no-karamel_include --no-karamel_include

clang-format-18 --style=Google -i cg/*.h

if [[ -n "$BORINGSSL_HOME" ]]; then
echo "Copying the files into $BORINGSSL_HOME/third_party/libcrux/"

cp cg/libcrux_*.h $BORINGSSL_HOME/third_party/libcrux/
cp cg/code_gen.txt $BORINGSSL_HOME/third_party/libcrux/
cp -r cg/intrinsics $BORINGSSL_HOME/third_party/libcrux/

# We use special files here.
cp cg/boring/eurydice_glue.h $BORINGSSL_HOME/third_party/libcrux/
cp -r cg/boring/karamel $BORINGSSL_HOME/third_party/libcrux/

libcrux_rev=$(git rev-parse HEAD)
echo "libcrux: $libcrux_rev" >> $BORINGSSL_HOME/third_party/libcrux/code_gen.txt
fi
133 changes: 133 additions & 0 deletions libcrux-ml-dsa/c.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,133 @@
#!/usr/bin/env bash

set -e
set -o pipefail

if [[ -z "$CHARON_HOME" ]]; then
echo "Please set CHARON_HOME to the Charon directory" 1>&2
exit 1
fi
if [[ -z "$EURYDICE_HOME" ]]; then
echo "Please set EURYDICE_HOME to the Eurydice directory" 1>&2
exit 1
fi
if [[ -z "$KRML_HOME" ]]; then
echo "Please set KRML_HOME to the KaRaMeL directory" 1>&2
exit 1
fi

portable_only=0
no_hacl=0
no_charon=0
clean=0
config=c.yaml
out=c
glue=$EURYDICE_HOME/include/eurydice_glue.h
features=""
eurydice_glue=1
karamel_include=1
unrolling=16

# Parse command line arguments.
all_args=("$@")
while [ $# -gt 0 ]; do
case "$1" in
-p | --portable) portable_only=1 ;;
--no-hacl) no_hacl=1 ;;
--no-charon) no_charon=1 ;;
-c | --clean) clean=1 ;;
--config) config="$2"; shift ;;
--out) out="$2"; shift ;;
--glue) glue="$2"; shift ;;
--mldsa65) features="${features} --cargo-arg=--no-default-features --cargo-arg=--features=mldsa65" ;;
--no-glue) eurydice_glue=0 ;;
--no-karamel_include) karamel_include=0 ;;
--no-unrolling) unrolling=0 ;;
esac
shift
done

if [[ "$portable_only" = 1 ]]; then
export LIBCRUX_DISABLE_SIMD256=1
export LIBCRUX_DISABLE_SIMD128=1
fi

# TODO: add LIBCRUX_ENABLE_SIMD128=1 LIBCRUX_ENABLE_SIMD256=1 charon invocations
if [[ "$no_charon" = 0 ]]; then
rm -rf ../libcrux_ml_dsa.llbc ../libcrux_sha3.llbc
echo "Running charon (sha3) ..."
(cd ../libcrux-sha3 && RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon)
if ! [[ -f ../libcrux_sha3.llbc ]]; then
echo "😱😱😱 You are the victim of a bug."
echo "Suggestion: rm -rf ../target or cargo clean"
exit 1
fi
echo "Running charon (ml-dsa) with $features ..."
RUSTFLAGS="--cfg eurydice" $CHARON_HOME/bin/charon $features
else
echo "Skipping charon"
fi

mkdir -p $out
cd $out

# Clean only when requesting it.
# Note that we can not extract for all platforms on any platform right now.
# Make sure to keep files from other platforms.
if [[ "$clean" = 1 ]]; then
rm -rf *.c *.h
rm -rf internal/*.h
fi

# Write out infos about the used tools
[[ -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 "$LIBCRUX_REV" ]] && export LIBCRUX_REV=$(git 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 revisions:" >> code_gen.txt
echo -n "Charon: " >> code_gen.txt
echo "$CHARON_REV" >> code_gen.txt
echo -n "Eurydice: " >> code_gen.txt
echo "$EURYDICE_REV" >> code_gen.txt
echo -n "Karamel: " >> code_gen.txt
echo "$KRML_REV" >> code_gen.txt
echo -n "F*: " >> code_gen.txt
echo "$FSTAR_REV" >> code_gen.txt
echo -n "Libcrux: " >> code_gen.txt
echo "$LIBCRUX_REV" >> code_gen.txt

# Generate header
cat spdx-header.txt > header.txt
sed -e 's/^/ * /' code_gen.txt >> header.txt
echo " */" >> header.txt

# Run eurydice to extract the C code
echo "Running eurydice ..."
echo $EURYDICE_HOME/eurydice --config ../$config -funroll-loops $unrolling \
--header header.txt \
../../libcrux_ml_dsa.llbc ../../libcrux_sha3.llbc
$EURYDICE_HOME/eurydice --debug "-dast" --config ../$config -funroll-loops $unrolling \
--header header.txt \
../../libcrux_ml_dsa.llbc ../../libcrux_sha3.llbc
if [[ "$eurydice_glue" = 1 ]]; then
cp $EURYDICE_HOME/include/eurydice_glue.h .
fi

if [[ "$karamel_include" = 1 ]]; then
echo "Copying karamel/include ..."
mkdir -p karamel
cp -R $KRML_HOME/include karamel/
fi

find . -type f -name '*.c' -and -not -path '*_deps*' -exec clang-format --style=Google -i "{}" \;
find . -type f -name '*.h' -and -not -path '*_deps*' -exec clang-format --style=Google -i "{}" \;
if [ -d "internal" ]; then
clang-format --style=Google -i internal/*.h
fi
clang-format --style=Google -i intrinsics/*.h
Loading

0 comments on commit 767c2a7

Please sign in to comment.