Merge pull request #771 from cryspen/franziskus/hax-ci-update

Update hax CI
cryspen · Jan 24, 2025 · 58539f9 · 58539f9
2 parents a09ba24 + 17001a7
commit 58539f9
Showing 1 changed file with 89 additions and 38 deletions.
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -13,8 +13,8 @@ on:
   workflow_dispatch:
     inputs:
       hax_rev:
-        description: 'The hax revision you want this job to use'
-        default: 'main'
+        description: "The hax revision you want this job to use"
+        default: "main"
   merge_group:
 
 env:
@@ -25,61 +25,112 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  hax:
-    runs-on: "ubuntu-latest"
+  mlkem-extract:
+    runs-on: ubuntu-latest
 
     steps:
       - uses: actions/checkout@v4
-      - uses: DeterminateSystems/nix-installer-action@main
-      - uses: DeterminateSystems/magic-nix-cache-action@main
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_rev || 'main' }}
+          fstar: v2024.12.03
 
-      - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/v2024.12.03
+      - name: 🏃 Extract ML-KEM crate
+        working-directory: libcrux-ml-kem
+        run: ./hax.py extract
 
-      - name: ⤵ Clone HACL-star repository
-        uses: actions/checkout@v4
+      - name: ↑ Upload F* extraction
+        uses: actions/upload-artifact@v4
         with:
-          repository: hacl-star/hacl-star
-          path: hacl-star
+          name: fstar-extraction-mlkem
+          path: libcrux-ml-kem/proofs/
+          include-hidden-files: true
+          if-no-files-found: error
+
+  mlkem-diff:
+    needs: mlkem-extract
+    runs-on: ubuntu-latest
 
-      - name: ⤵ Clone hax repository
-        uses: actions/checkout@v4
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/download-artifact@v4
         with:
-          repository: hacspec/hax
-          ref: ${{ github.event.inputs.hax_rev || 'main' }}
-          path: hax
+          name: fstar-extraction-mlkem
+          path: ~/fstar-extraction-mlkem
 
-      - name: ⤵ Install & confiure Cachix
+      - name: = Diff Extraction
         run: |
-          nix profile install nixpkgs#cachix
-          cachix use hax
+          diff -r libcrux-ml-kem/proofs/fstar/extraction/ \
+            ~/fstar-extraction-mlkem/fstar/extraction/
 
-      - name: ⤵ Install hax
-        run: |
-          nix profile install ./hax
+  mlkem-lax:
+    runs-on: ubuntu-latest
+    needs:
+      - mlkem-extract
+      - mlkem-diff
 
-      - name: 🏃 Extract ML-KEM crate
-        working-directory: libcrux-ml-kem
-        run: ./hax.py extract
+    steps:
+      - uses: actions/checkout@v4
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_rev || 'main' }}
+          fstar: v2024.12.03
 
       - 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
+        run: ./hax.py prove --admit
+
+  mldsa-extract:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_rev || 'main' }}
+          fstar: v2024.12.03
 
       - name: 🏃 Extract ML-DSA crate
         working-directory: libcrux-ml-dsa
         run: ./hax.py extract
 
+      - name: ↑ Upload F* extraction
+        uses: actions/upload-artifact@v4
+        with:
+          name: fstar-extraction-mldsa
+          path: libcrux-ml-dsa/proofs/
+          include-hidden-files: true
+          if-no-files-found: error
+
+  mldsa-diff:
+    needs: mldsa-extract
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/download-artifact@v4
+        with:
+          name: fstar-extraction-mldsa
+          path: ~/fstar-extraction-mldsa
+
+      - name: = Diff Extraction
+        run: |
+          diff -r libcrux-ml-dsa/proofs/fstar/extraction/ \
+            ~/fstar-extraction-mldsa/fstar/extraction/
+
+  mldsa-lax:
+    runs-on: ubuntu-latest
+    needs:
+      - mldsa-extract
+      - mldsa-diff
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_rev || 'main' }}
+          fstar: v2024.12.03
+
       - 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
+        run: ./hax.py prove --admit