Skip to content

more principled generic printer #83

more principled generic printer

more principled generic printer #83

Workflow file for this run

name: Extract and TC ML-Kem
on:
pull_request:
merge_group:
workflow_dispatch:
push:
branches: [main]
env:
CARGO_TERM_COLOR: always
jobs:
extract-mlkem:
if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'merge_group' }}
runs-on: "ubuntu-latest"
steps:
- name: ⤵ Clone Libcrux repository
uses: actions/checkout@v4
with:
repository: cryspen/libcrux
- uses: actions/checkout@v4
with:
path: hax
- uses: DeterminateSystems/nix-installer-action@main
- uses: DeterminateSystems/magic-nix-cache-action@main
- name: ⤵ Install hax
run: |
nix profile install ./hax
- name: ⤵ Install FStar
run: nix profile install github:FStarLang/FStar/v2024.01.13
- name: ⤵ Clone HACL-star repository
uses: actions/checkout@v4
with:
repository: hacl-star/hacl-star
path: hacl-star
- 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 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