hax.yml

name: hax

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

  pull_request:
    branches: ["dev", "main"]

  schedule:
    - cron: "0 0 * * *"

  workflow_dispatch:
  merge_group:

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.09.05

      - 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/hax
          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 ML-KEM crate
        working-directory: libcrux-ml-kem
        run: ./hax.py extract

      - name: 🏃 Lax ML-KEM crate
        working-directory: libcrux-ml-kem
        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.py prove --admit

      - name: 🏃 Extract ML-DSA crate
        working-directory: libcrux-ml-dsa
        run: ./hax.py extract

      - name: 🏃 Lax ML-DSA crate
        working-directory: libcrux-ml-dsa
        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.py prove --admit