mlkem.yml

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