ML-DSA extraction on CI

cryspen · Oct 29, 2024 · 44af027 · 44af027
1 parent a17120e
commit 44af027
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -68,7 +68,7 @@ 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

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
@@ -170,7 +170,7 @@ let impl_1: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 t_Shake256x4 =
     f_init_absorb_x4
     =
     (fun (input0: t_Slice u8) (input1: t_Slice u8) (input2: t_Slice u8) (input3: t_Slice u8) ->
-        init_absorb_x4 input0 input2 input2 input3);
+        init_absorb_x4 input0 input1 input2 input3);
     f_squeeze_first_block_x4_pre = (fun (self: t_Shake256x4) -> true);
     f_squeeze_first_block_x4_post
     =