Skip to content

Commit

Permalink
drop unnecessary hax jobs
Browse files Browse the repository at this point in the history
  • Loading branch information
franziskuskiefer committed Jun 12, 2024
1 parent 20402d5 commit e9e6067
Showing 1 changed file with 1 addition and 59 deletions.
60 changes: 1 addition & 59 deletions .github/workflows/hax.yml
Original file line number Diff line number Diff line change
Expand Up @@ -52,44 +52,7 @@ 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
Expand All @@ -98,24 +61,3 @@ jobs:
# 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

0 comments on commit e9e6067

Please sign in to comment.