Merge pull request #646 from cryspen/ml-dsa-lax

Lax Checking for ML-DSA

.github/workflows/hax.yml

@@ -68,4 +68,13 @@ jobs:
 
       - name: 🏃 Extract ML-DSA crate
         working-directory: libcrux-ml-dsa
-        run: cargo hax into fstar
+        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

.gitignore

@@ -2,16 +2,19 @@
 .vscode
 .DS_Store
 benches/boringssl/build
-proofs/fstar/extraction/.depend
-proofs/fstar/extraction/#*#
-proofs/fstar/extraction/.#*
 fuzz/corpus
 fuzz/artifacts
-proofs/fstar/extraction/.cache
 __pycache__
 kyber-crate/
 *.llbc
 .cargo/
 
 # When using sed
 *.bak
+
+# F*
+.fstar-cache
+.depend
+/proofs/fstar/*/#*#
+/proofs/fstar/*/.#*
+hax.fst.config.json