ml-dsa make

libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti

@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Arm64_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti

@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Avx2_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fsti

@@ -3,28 +3,43 @@ module Libcrux_ml_dsa.Simd.Avx2.Arithmetic
 open Core
 open FStar.Mul
 
-val add (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val add (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
-val compute_hint (v_GAMMA2: i32) (low high: u8)
-    : Prims.Pure (usize & u8) Prims.l_True (fun _ -> Prims.l_True)
+val compute_hint (v_GAMMA2: i32) (low high: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure (usize & Libcrux_intrinsics.Avx2_extract.t_Vec256)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
 
-val infinity_norm_exceeds (simd_unit: u8) (bound: i32)
+val infinity_norm_exceeds (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (bound: i32)
     : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
-val subtract (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val subtract (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
-val shift_left_then_reduce (v_SHIFT_BY: i32) (simd_unit: u8)
-    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val shift_left_then_reduce (v_SHIFT_BY: i32) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
-val to_unsigned_representatives (t: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val to_unsigned_representatives (t: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
-val power2round (r: u8) : Prims.Pure (u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+val power2round (r: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure
+      (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
 
-val montgomery_multiply (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val montgomery_multiply (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
-val montgomery_multiply_by_constant (lhs: u8) (constant: i32)
-    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val montgomery_multiply_by_constant (lhs: Libcrux_intrinsics.Avx2_extract.t_Vec256) (constant: i32)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
 
-val decompose (v_GAMMA2: i32) (r: u8) : Prims.Pure (u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
+val decompose (v_GAMMA2: i32) (r: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure
+      (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
 
-val use_hint (v_GAMMA2: i32) (r hint: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+val use_hint (v_GAMMA2: i32) (r hint: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst

@@ -3,30 +3,34 @@ module Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment
 open Core
 open FStar.Mul
 
-let serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
+let serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
   let serialized:t_Array u8 (sz 19) = Rust_primitives.Hax.repeat 0uy (sz 19) in
   match cast (v_OUTPUT_SIZE <: usize) <: u8 with
   | 4uy ->
-    let adjacent_2_combined:u8 =
+    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 28l 0l 28l 0l 28l 0l 28l <: u8)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 28l 0l 28l 0l 28l 0l 28l
+          <:
+          Libcrux_intrinsics.Avx2_extract.t_Vec256)
     in
-    let adjacent_2_combined:u8 =
+    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_srli_epi64 28l adjacent_2_combined
     in
-    let adjacent_4_combined:u8 =
+    let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_permutevar8x32_epi32 adjacent_2_combined
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 6l 2l 4l 0l <: u8)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 6l 2l 4l 0l
+          <:
+          Libcrux_intrinsics.Avx2_extract.t_Vec256)
     in
-    let adjacent_4_combined:u8 =
+    let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
       Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_4_combined
     in
-    let adjacent_4_combined:u8 =
+    let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
       Libcrux_intrinsics.Avx2_extract.mm_shuffle_epi8 adjacent_4_combined
         (Libcrux_intrinsics.Avx2_extract.mm_set_epi8 240uy 240uy 240uy 240uy 240uy 240uy 240uy 240uy
             240uy 240uy 240uy 240uy 12uy 4uy 8uy 0uy
           <:
-          u8)
+          Libcrux_intrinsics.Avx2_extract.t_Vec128)
     in
     let serialized:t_Array u8 (sz 19) =
       Rust_primitives.Hax.Monomorphized_update_at.update_at_range serialized
@@ -58,33 +62,39 @@ let serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
         <:
         Core.Result.t_Result (t_Array u8 v_OUTPUT_SIZE) Core.Array.t_TryFromSliceError)
   | 6uy ->
-    let adjacent_2_combined:u8 =
+    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 26l 0l 26l 0l 26l 0l 26l <: u8)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 26l 0l 26l 0l 26l 0l 26l
+          <:
+          Libcrux_intrinsics.Avx2_extract.t_Vec256)
     in
-    let adjacent_2_combined:u8 =
+    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_srli_epi64 26l adjacent_2_combined
     in
-    let adjacent_3_combined:u8 =
+    let adjacent_3_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_shuffle_epi8 adjacent_2_combined
         (Libcrux_intrinsics.Avx2_extract.mm256_set_epi8 (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) (-1y)
             (-1y) (-1y) (-1y) (-1y) (-1y) 9y 8y 1y 0y (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) (-1y)
             (-1y) (-1y) (-1y) (-1y) (-1y) 9y 8y 1y 0y
           <:
-          u8)
+          Libcrux_intrinsics.Avx2_extract.t_Vec256)
     in
-    let adjacent_3_combined:u8 =
+    let adjacent_3_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_mullo_epi16 adjacent_3_combined
         (Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 1s 1s 1s 1s 1s 1s 1s (1s <<! 4l <: i16) 1s
             1s 1s 1s 1s 1s 1s (1s <<! 4l <: i16)
           <:
-          u8)
+          Libcrux_intrinsics.Avx2_extract.t_Vec256)
     in
-    let adjacent_3_combined:u8 =
+    let adjacent_3_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
       Libcrux_intrinsics.Avx2_extract.mm256_srlv_epi32 adjacent_3_combined
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 4l 0l 0l 0l 4l <: u8)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 4l 0l 0l 0l 4l
+          <:
+          Libcrux_intrinsics.Avx2_extract.t_Vec256)
+    in
+    let lower_3_:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
+      Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_3_combined
     in
-    let lower_3_:u8 = Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_3_combined in
     let serialized:t_Array u8 (sz 19) =
       Rust_primitives.Hax.Monomorphized_update_at.update_at_range serialized
         ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 16 }
@@ -102,7 +112,7 @@ let serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
           <:
           t_Slice u8)
     in
-    let upper_3_:u8 =
+    let upper_3_:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
       Libcrux_intrinsics.Avx2_extract.mm256_extracti128_si256 1l adjacent_3_combined
     in
     let serialized:t_Array u8 (sz 19) =

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fsti

@@ -3,5 +3,5 @@ module Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment
 open Core
 open FStar.Mul
 
-val serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8)
+val serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256)
     : Prims.Pure (t_Array u8 v_OUTPUT_SIZE) Prims.l_True (fun _ -> Prims.l_True)

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Error.fst

@@ -12,7 +12,7 @@ let deserialize_to_unsigned_when_eta_is_2_ (bytes: t_Slice u8) =
       in
       ()
   in
-  let bytes_in_simd_unit:u8 =
+  let bytes_in_simd_unit:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 (cast (bytes.[ sz 2 ] <: u8) <: i32)
       (cast (bytes.[ sz 2 ] <: u8) <: i32)
       (((cast (bytes.[ sz 2 ] <: u8) <: i32) <<! 8l <: i32) |. (cast (bytes.[ sz 1 ] <: u8) <: i32)
@@ -26,15 +26,17 @@ let deserialize_to_unsigned_when_eta_is_2_ (bytes: t_Slice u8) =
       (cast (bytes.[ sz 0 ] <: u8) <: i32)
       (cast (bytes.[ sz 0 ] <: u8) <: i32)
   in
-  let coefficients:u8 =
+  let coefficients:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_srlv_epi32 bytes_in_simd_unit
-      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 5l 2l 7l 4l 1l 6l 3l 0l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 5l 2l 7l 4l 1l 6l 3l 0l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
   Libcrux_intrinsics.Avx2_extract.mm256_and_si256 coefficients
     (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32 deserialize_to_unsigned_when_eta_is_2___COEFFICIENT_MASK
 
       <:
-      u8)
+      Libcrux_intrinsics.Avx2_extract.t_Vec256)
 
 let deserialize_to_unsigned_when_eta_is_4_ (bytes: t_Slice u8) =
   let _:Prims.unit =
@@ -45,7 +47,7 @@ let deserialize_to_unsigned_when_eta_is_4_ (bytes: t_Slice u8) =
       in
       ()
   in
-  let bytes_in_simd_unit:u8 =
+  let bytes_in_simd_unit:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 (cast (bytes.[ sz 3 ] <: u8) <: i32)
       (cast (bytes.[ sz 3 ] <: u8) <: i32)
       (cast (bytes.[ sz 2 ] <: u8) <: i32)
@@ -55,15 +57,17 @@ let deserialize_to_unsigned_when_eta_is_4_ (bytes: t_Slice u8) =
       (cast (bytes.[ sz 0 ] <: u8) <: i32)
       (cast (bytes.[ sz 0 ] <: u8) <: i32)
   in
-  let coefficients:u8 =
+  let coefficients:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_srlv_epi32 bytes_in_simd_unit
-      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 4l 0l 4l 0l 4l 0l 4l 0l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 4l 0l 4l 0l 4l 0l 4l 0l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
   Libcrux_intrinsics.Avx2_extract.mm256_and_si256 coefficients
     (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32 deserialize_to_unsigned_when_eta_is_4___COEFFICIENT_MASK
 
       <:
-      u8)
+      Libcrux_intrinsics.Avx2_extract.t_Vec256)
 
 let deserialize_to_unsigned (v_ETA: usize) (serialized: t_Slice u8) =
   match cast (v_ETA <: usize) <: u8 with
@@ -76,56 +80,67 @@ let deserialize_to_unsigned (v_ETA: usize) (serialized: t_Slice u8) =
         Rust_primitives.Hax.t_Never)
 
 let deserialize (v_ETA: usize) (serialized: t_Slice u8) =
-  let unsigned:u8 = deserialize_to_unsigned v_ETA serialized in
+  let unsigned:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    deserialize_to_unsigned v_ETA serialized
+  in
   Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32 (
           cast (v_ETA <: usize) <: i32)
       <:
-      u8)
+      Libcrux_intrinsics.Avx2_extract.t_Vec256)
     unsigned
 
-let serialize_when_eta_is_2_ (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
+let serialize_when_eta_is_2_
+      (v_OUTPUT_SIZE: usize)
+      (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+     =
   let serialized:t_Array u8 (sz 16) = Rust_primitives.Hax.repeat 0uy (sz 16) in
-  let simd_unit_shifted:u8 =
+  let simd_unit_shifted:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32
           serialize_when_eta_is_2___ETA
         <:
-        u8)
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
       simd_unit
   in
-  let adjacent_2_combined:u8 =
+  let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit_shifted
-      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 29l 0l 29l 0l 29l 0l 29l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 29l 0l 29l 0l 29l 0l 29l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
-  let adjacent_2_combined:u8 =
+  let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_srli_epi64 29l adjacent_2_combined
   in
-  let adjacent_4_combined:u8 =
+  let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_shuffle_epi8 adjacent_2_combined
       (Libcrux_intrinsics.Avx2_extract.mm256_set_epi8 (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) (-1y)
           (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) 8y (-1y) 0y (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) (-1y)
           (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) 8y (-1y) 0y
         <:
-        u8)
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
-  let adjacent_4_combined:u8 =
+  let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_madd_epi16 adjacent_4_combined
       (Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 0s 0s 0s 0s 0s 0s (1s <<! 6l <: i16) 1s 0s 0s
           0s 0s 0s 0s (1s <<! 6l <: i16) 1s
         <:
-        u8)
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
-  let adjacent_6_combined:u8 =
+  let adjacent_6_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_permutevar8x32_epi32 adjacent_4_combined
-      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 0l 0l 4l 0l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 0l 0l 4l 0l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
-  let adjacent_6_combined:u8 =
+  let adjacent_6_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
     Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_6_combined
   in
-  let adjacent_6_combined:u8 =
+  let adjacent_6_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
     Libcrux_intrinsics.Avx2_extract.mm_sllv_epi32 adjacent_6_combined
-      (Libcrux_intrinsics.Avx2_extract.mm_set_epi32 0l 0l 0l 20l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm_set_epi32 0l 0l 0l 20l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec128)
   in
-  let adjacent_6_combined:u8 =
+  let adjacent_6_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
     Libcrux_intrinsics.Avx2_extract.mm_srli_epi64 20l adjacent_6_combined
   in
   let serialized:t_Array u8 (sz 16) =
@@ -158,35 +173,42 @@ let serialize_when_eta_is_2_ (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
       <:
       Core.Result.t_Result (t_Array u8 v_OUTPUT_SIZE) Core.Array.t_TryFromSliceError)
 
-let serialize_when_eta_is_4_ (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
+let serialize_when_eta_is_4_
+      (v_OUTPUT_SIZE: usize)
+      (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+     =
   let serialized:t_Array u8 (sz 16) = Rust_primitives.Hax.repeat 0uy (sz 16) in
-  let simd_unit_shifted:u8 =
+  let simd_unit_shifted:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_sub_epi32 (Libcrux_intrinsics.Avx2_extract.mm256_set1_epi32
           serialize_when_eta_is_4___ETA
         <:
-        u8)
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
       simd_unit
   in
-  let adjacent_2_combined:u8 =
+  let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit_shifted
-      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 28l 0l 28l 0l 28l 0l 28l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 28l 0l 28l 0l 28l 0l 28l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
-  let adjacent_2_combined:u8 =
+  let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_srli_epi64 28l adjacent_2_combined
   in
-  let adjacent_4_combined:u8 =
+  let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_permutevar8x32_epi32 adjacent_2_combined
-      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 6l 2l 4l 0l <: u8)
+      (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 6l 2l 4l 0l
+        <:
+        Libcrux_intrinsics.Avx2_extract.t_Vec256)
   in
-  let adjacent_4_combined:u8 =
+  let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
     Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_4_combined
   in
-  let adjacent_4_combined:u8 =
+  let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
     Libcrux_intrinsics.Avx2_extract.mm_shuffle_epi8 adjacent_4_combined
       (Libcrux_intrinsics.Avx2_extract.mm_set_epi8 240uy 240uy 240uy 240uy 240uy 240uy 240uy 240uy
           240uy 240uy 240uy 240uy 12uy 4uy 8uy 0uy
         <:
-        u8)
+        Libcrux_intrinsics.Avx2_extract.t_Vec128)
   in
   let serialized:t_Array u8 (sz 16) =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range serialized
@@ -218,7 +240,7 @@ let serialize_when_eta_is_4_ (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
       <:
       Core.Result.t_Result (t_Array u8 v_OUTPUT_SIZE) Core.Array.t_TryFromSliceError)
 
-let serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
+let serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
   match cast (v_OUTPUT_SIZE <: usize) <: u8 with
   | 3uy -> serialize_when_eta_is_2_ v_OUTPUT_SIZE simd_unit
   | 4uy -> serialize_when_eta_is_4_ v_OUTPUT_SIZE simd_unit