Skip to content

mlkem c all versions #702

mlkem c all versions

mlkem c all versions #702

Workflow file for this run

name: hax
on:
push:
branches: ["dev", "main"]
pull_request:
branches: ["dev", "main"]
schedule:
- cron: "0 0 * * *"
workflow_dispatch:
env:
CARGO_TERM_COLOR: always
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
hax:
runs-on: "ubuntu-latest"
steps:
- uses: actions/checkout@v4
- uses: DeterminateSystems/nix-installer-action@main
- uses: DeterminateSystems/magic-nix-cache-action@main
- 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: ⤵ Clone hax repository
uses: actions/checkout@v4
with:
repository: hacspec/hacspec-v2
path: hax
- name: ⤵ Install & confiure Cachix
run: |
nix profile install nixpkgs#cachix
cachix use hax
- name: ⤵ Install hax
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)
run: |
cd libcrux-ml-kem
# ./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