Sha3 lax check

.github/workflows/sha3-hax.yml

@@ -2,8 +2,12 @@ name: SHA3 - hax
 
 on:
   merge_group:
+    paths:
+      - "libcrux-sha3/**"
   pull_request:
     branches: ["dev", "main"]
+    paths:
+      - "libcrux-sha3/**"
 
   schedule:
     - cron: "0 0 * * *"
@@ -44,22 +48,81 @@ jobs:
         working-directory: libcrux-sha3
         run: ./hax.py extract
 
-      - name: ↑ Upload F* extraction
+      - name: ↑ Upload F* extraction (standard)
         uses: actions/upload-artifact@v4
         with:
-          name: fstar-extractions
+          name: fstar-extractions-standard
           path: "**/proofs/fstar"
           include-hidden-files: true
           if-no-files-found: error
-
+
+  extract-portable:
+    if: ${{ github.event_name != 'merge_group' }}
+    runs-on: ubuntu-latest
+    needs:
+      - get-hax-ref
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_ref || needs.get-hax-ref.outputs.hax_ref }}
+          fstar: v2025.02.17
+
+      - name: 🏃 Extract SHA3 crate (portable)
+        working-directory: libcrux-sha3
+        run: ./hax.py extract --portable
+
+      - name: ↑ Upload F* extraction (portable)
+        uses: actions/upload-artifact@v4
+        with:
+          name: fstar-extractions-portable
+          path: "**/proofs/fstar"
+          include-hidden-files: true
+          if-no-files-found: error
+
+  lax-portable:
+    runs-on: ubuntu-latest
+    needs:
+      - get-hax-ref
+      - extract-portable
+    if: ${{ github.event_name != 'merge_group' }}
+    steps:
+      - uses: actions/checkout@v5
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_ref || needs.get-hax-ref.outputs.hax_ref }}
+          fstar: v2025.02.17
+
+      - uses: actions/download-artifact@v5
+        with:
+          name: fstar-extractions-portable
+          path: .
+
+      - name: 🏃 Lax SHA3 crate (portable)
+        working-directory: libcrux-sha3
+        run: ./hax.py prove --admit
+
   sha3-extract-hax-status:
     if: ${{ always() }}
     needs: [get-hax-ref, extract]
     runs-on: ubuntu-latest
     steps:
       - name: Successful
-        if: ${{ !(contains(needs.*.result, 'failure')) }} 
-        run: exit 0 
+        if: ${{ !(contains(needs.*.result, 'failure')) }}
+        run: exit 0
+      - name: Failing
+        if: ${{ (contains(needs.*.result, 'failure')) }}
+        run: exit 1
+
+  sha3-lax-portable-hax-status:
+    if: ${{ always() }}
+    needs: [get-hax-ref, lax-portable]
+    runs-on: ubuntu-latest
+    steps:
+      - name: Successful
+        if: ${{ !(contains(needs.*.result, 'failure')) }}
+        run: exit 0
       - name: Failing
-        if: ${{ (contains(needs.*.result, 'failure')) }} 
-        run: exit 1 
+        if: ${{ (contains(needs.*.result, 'failure')) }}
+        run: exit 1

flake.nix

@@ -47,6 +47,7 @@
             cp -r ${eurydice}/include $out
           '';
           FSTAR_HOME = fstar.packages.${system}.default;
+          HAX_HOME = hax;
           KRML_HOME = karamel;
 
           CHARON_REV = charon.rev or "dirty";
@@ -238,6 +239,7 @@
             pkgs.clang_18
             pkgs.openssl
             pkgs.pkg-config
+            pkgs.jq
             fstar.packages.${system}.default
           ];
           inputsFrom = [ packages.ml-kem ];

fstar-helpers/core-models/src/core_arch/x86/interpretations.rs

@@ -98,7 +98,7 @@ pub mod int_vec {
     }
 
     pub fn _mm_mullo_epi16(a: i16x8, b: i16x8) -> i16x8 {
-        i16x8::from_fn(|i| (a[i].overflowing_mul(b[i]).0))
+        i16x8::from_fn(|i| a[i].overflowing_mul(b[i]).0)
     }
 
     pub fn _mm256_cmpgt_epi16(a: i16x16, b: i16x16) -> i16x16 {
@@ -152,16 +152,16 @@ pub mod int_vec {
 
     #[hax_lib::fstar::options("--z3rlimit 200")]
     pub fn _mm_mulhi_epi16(a: i16x8, b: i16x8) -> i16x8 {
-        i16x8::from_fn(|i| (((a[i] as i32) * (b[i] as i32) >> 16) as i16))
+        i16x8::from_fn(|i| ((a[i] as i32) * (b[i] as i32) >> 16) as i16)
     }
 
     pub fn _mm256_mullo_epi32(a: i32x8, b: i32x8) -> i32x8 {
-        i32x8::from_fn(|i| (a[i].overflowing_mul(b[i]).0))
+        i32x8::from_fn(|i| a[i].overflowing_mul(b[i]).0)
     }
 
     #[hax_lib::fstar::verification_status(lax)]
     pub fn _mm256_mulhi_epi16(a: i16x16, b: i16x16) -> i16x16 {
-        i16x16::from_fn(|i| (((a[i] as i32) * (b[i] as i32) >> 16) as i16))
+        i16x16::from_fn(|i| ((a[i] as i32) * (b[i] as i32) >> 16) as i16)
     }
 
     pub fn _mm256_mul_epu32(a: u32x8, b: u32x8) -> u64x4 {

libcrux-ml-dsa/cg/code_gen.txt

@@ -3,4 +3,4 @@ Charon: 667d2fc98984ff7f3df989c2367e6c1fa4a000e7
 Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
 Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
 F*: 71d8221589d4d438af3706d89cb653cf53e18aab
-Libcrux: d31e614e52a5b0d4d86d85f259594a1c9f6d9897
+Libcrux: ae00be9b55b2f9a172105512ea707a265f5bdd6e

libcrux-ml-dsa/cg/header.txt

@@ -8,5 +8,5 @@
  * Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
  * Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
  * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: d31e614e52a5b0d4d86d85f259594a1c9f6d9897
+ * Libcrux: ae00be9b55b2f9a172105512ea707a265f5bdd6e
  */

libcrux-ml-dsa/cg/libcrux_core.h

@@ -8,7 +8,7 @@
  * Eurydice: 2381cbc416ef2ad0b561c362c500bc84f36b6785
  * Karamel: 80f5435f2fc505973c469a4afcc8d875cddd0d8b
  * F*: 71d8221589d4d438af3706d89cb653cf53e18aab
- * Libcrux: d31e614e52a5b0d4d86d85f259594a1c9f6d9897
+ * Libcrux: ae00be9b55b2f9a172105512ea707a265f5bdd6e
  */
 
 #ifndef libcrux_core_H