fixup hax

cryspen · Dec 28, 2024 · 834b7f5 · 834b7f5
1 parent c18be26
commit 834b7f5
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 11 deletions.
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -34,7 +34,7 @@ jobs:
       - uses: DeterminateSystems/magic-nix-cache-action@main
 
       - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/v2024.09.05
+        run: nix profile install github:FStarLang/FStar/v2024.12.03
 
       - name: ⤵ Clone HACL-star repository
         uses: actions/checkout@v4

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst
@@ -7,7 +7,6 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Libcrux_ml_dsa.Simd.Avx2.Vector_type in
-  let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
@@ -576,9 +575,7 @@ Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit =
           Libcrux_ml_dsa.Simd.Avx2.Ntt.ntt re
         in
         let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) =
-          Rust_primitives.Hax.repeat (Libcrux_ml_dsa.Simd.Traits.f_ZERO #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-                #FStar.Tactics.Typeclasses.solve
-                ()
+          Rust_primitives.Hax.repeat (Libcrux_ml_dsa.Simd.Avx2.Vector_type.v_ZERO ()
               <:
               Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit)
             (sz 32)
@@ -651,9 +648,7 @@ Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit =
         Libcrux_ml_dsa.Simd.Avx2.Invntt.invert_ntt_montgomery re
       in
       let out:t_Array Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit (sz 32) =
-        Rust_primitives.Hax.repeat (Libcrux_ml_dsa.Simd.Traits.f_ZERO #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-              #FStar.Tactics.Typeclasses.solve
-              ()
+        Rust_primitives.Hax.repeat (Libcrux_ml_dsa.Simd.Avx2.Vector_type.v_ZERO ()
             <:
             Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit)
           (sz 32)

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fsti
@@ -7,7 +7,6 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Libcrux_ml_dsa.Simd.Avx2.Vector_type in
-  let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]

diff --git a/libcrux-ml-dsa/src/simd/avx2.rs b/libcrux-ml-dsa/src/simd/avx2.rs
@@ -137,7 +137,7 @@ impl Operations for AVX2SIMDUnit {
         }
         let result = ntt::ntt(re);
 
-        let mut out = [Self::ZERO(); SIMD_UNITS_IN_RING_ELEMENT];
+        let mut out = [vector_type::ZERO(); SIMD_UNITS_IN_RING_ELEMENT];
         for i in 0..result.len() {
             out[i] = Self {
                 coefficients: result[i],
@@ -158,7 +158,7 @@ impl Operations for AVX2SIMDUnit {
         }
         let result = invntt::invert_ntt_montgomery(re);
 
-        let mut out = [Self::ZERO(); SIMD_UNITS_IN_RING_ELEMENT];
+        let mut out = [vector_type::ZERO(); SIMD_UNITS_IN_RING_ELEMENT];
         for i in 0..result.len() {
             out[i] = Self {
                 coefficients: result[i],