Skip to content

Commit

Permalink
Merge branch 'dev' into franziskus/symcrypt_bench
Browse files Browse the repository at this point in the history
  • Loading branch information
franziskuskiefer committed Jun 12, 2024
2 parents a2be70e + fbdd7ed commit 9dbe0c0
Show file tree
Hide file tree
Showing 202 changed files with 17,544 additions and 11,803 deletions.
7 changes: 4 additions & 3 deletions .github/workflows/c.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
62 changes: 2 additions & 60 deletions .github/workflows/hax.yml
Original file line number Diff line number Diff line change
Expand Up @@ -52,70 +52,12 @@ jobs:
run: |
nix profile install ./hax
- name: 🏃 Extract the Kyber reference code
run: |
eval $(opam env)
(cd proofs/fstar/extraction/ && ./clean.sh)
rm -f sys/platform/proofs/fstar/extraction/*.fst*
./hax-driver.py --kyber-reference
- name: 🏃 Regenerate `extraction-*` folders
run: ./proofs/fstar/patches.sh apply

- name: 🏃 Make sure snapshots are up-to-date
run: git diff --exit-code

- name: 🏃 Verify the Kyber reference code
run: |
env FSTAR_HOME=${{ github.workspace }}/fstar \
HACL_HOME=${{ github.workspace }}/hacl-star \
HAX_HOME=${{ github.workspace }}/hax \
PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
./hax-driver.py --verify-extraction
- name: 🏃 Verify Kyber `extraction-edited` F* code
run: |
env FSTAR_HOME=${{ github.workspace }}/fstar \
HACL_HOME=${{ github.workspace }}/hacl-star \
HAX_HOME=${{ github.workspace }}/hax \
PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
make -C proofs/fstar/extraction-edited
- name: 🏃 Verify Kyber `extraction-secret-independent` F* code
run: |
env FSTAR_HOME=${{ github.workspace }}/fstar \
HACL_HOME=${{ github.workspace }}/hacl-star \
HAX_HOME=${{ github.workspace }}/hax \
PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
make -C proofs/fstar/extraction-secret-independent
- name: 🏃 Extract & Verify ML-KEM crate (lax)
- name: 🏃 Extract ML-KEM crate
run: |
cd libcrux-ml-kem
# ./hax.py extract
./hax.py extract
# env FSTAR_HOME=${{ github.workspace }}/fstar \
# HACL_HOME=${{ github.workspace }}/hacl-star \
# HAX_HOME=${{ github.workspace }}/hax \
# PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
# ./hax.py prove --admit
- name: 🏃 Extract the Kyber specification
run: |
eval $(opam env)
# Extract the functions in the compress module individually to test
# the function-extraction code.
# Extract functions from the remaining modules to test the
# module-extraction code.
./hax-driver.py --crate-path specs/kyber \
--functions hacspec_kyber::compress::compress \
hacspec_kyber::compress::decompress \
hacspec_kyber::compress::compress_d \
hacspec::kyber::compress::decompress_d \
--modules ind_cpa \
hacspec_kyber \
matrix \
ntt \
parameters \
sampling \
serialize \
--exclude-modules libcrux::hacl::sha3 libcrux::digest
3 changes: 3 additions & 0 deletions .github/workflows/mldsa.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ jobs:
steps:
- uses: actions/checkout@v4

- name: Update dependencies
run: cargo update

- run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
if: ${{ matrix.bits == 64 }}

Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/mlkem.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ jobs:
steps:
- uses: actions/checkout@v4

- name: Update dependencies
run: cargo update

- run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
if: ${{ matrix.bits == 64 }}

Expand Down Expand Up @@ -168,6 +171,9 @@ jobs:
steps:
- uses: actions/checkout@v4

- name: Update dependencies
run: cargo update

- run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
if: ${{ matrix.bits == 64 }}

Expand Down
20 changes: 20 additions & 0 deletions .github/workflows/nix.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
name: Nix

on:
push:
branches: [main, dev]
pull_request:

jobs:
nix:
runs-on: ubuntu-latest
steps:
- uses: DeterminateSystems/nix-installer-action@v12
- uses: DeterminateSystems/magic-nix-cache-action@v7
- name: Install & configure Cachix
shell: bash
run: |
nix-env --quiet -j8 -iA cachix -f https://cachix.org/api/v1/install
cachix use hax
- uses: actions/checkout@v4
- run: nix build -L .#ml-kem
3 changes: 3 additions & 0 deletions .github/workflows/platform.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ jobs:
steps:
- uses: actions/checkout@v4

- name: Update dependencies
run: cargo update

- name: 🔨 Build
run: cargo build --verbose

Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@ jobs:
steps:
- uses: actions/checkout@v4

- name: Update dependencies
run: cargo update

- run: echo "RUST_TARGET_FLAG=" > $GITHUB_ENV
if: ${{ matrix.bits == 64 }}

Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/specs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ jobs:
- uses: actions/checkout@v3

- name: Update dependencies
run: cargo update

- name: Build
working-directory: specs
run: cargo build --verbose
Expand Down
1 change: 0 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
/target
/Cargo.lock
.vscode
.DS_Store
benches/boringssl/build
Expand Down
Loading

0 comments on commit 9dbe0c0

Please sign in to comment.