Merge branch main into dev-panic-free

.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

Cargo.toml

@@ -26,6 +26,7 @@ members = [
     "poly1305",
     "chacha20poly1305",
     "rsa",
+    "blake2",
 ]
 
 [workspace.package]
@@ -87,7 +88,7 @@ log = { version = "0.4", optional = true }
 # WASM API
 wasm-bindgen = { version = "0.2.87", optional = true }
 getrandom = { version = "0.2", features = ["js"], optional = true }
-hax-lib = { version = "0.1.0-alpha.1", git = "https://github.com/hacspec/hax/" }
+hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/" }
 
 [dev-dependencies]
 libcrux = { path = ".", features = ["rand", "tests"] }

blake2/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "libcrux-blake2"
+description = "Formally verified blake2 hash library"
+
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+
+[dependencies]
+libcrux-hacl-rs = { version = "=0.0.2-beta.2", path = "../hacl-rs/" }
+libcrux-macros = { version = "=0.0.2-beta.2", path = "../macros" }