ML-DSA: AVX2 target feature

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti

@@ -4,7 +4,7 @@ open Core
 open FStar.Mul
 
 /// Portable SHAKE 128 state
-type t_Shake128 = | Shake128 : t_Shake128
+val t_Shake128:Type0
 
 /// Portable SHAKE 128 x4 state.
 /// We\'re using a portable implementation so this is actually sequential.
@@ -21,9 +21,6 @@ val t_Shake256Absorb:Type0
 
 val t_Shake256Squeeze:Type0
 
-val init_absorb__init_absorb (input: t_Slice u8)
-    : Prims.Pure Libcrux_sha3.Portable.t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
-
 val init_absorb (input0 input1 input2 input3: t_Slice u8)
     : Prims.Pure t_Shake128X4 Prims.l_True (fun _ -> Prims.l_True)
 

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti

@@ -11,13 +11,22 @@ val t_Shake128x4:Type0
 /// AVX2 SHAKE 256 x4 state.
 val t_Shake256x4:Type0
 
+/// AVX2 SHAKE 256 state
+val t_Shake256:Type0
+
 /// Init the state and absorb 4 blocks in parallel.
 val init_absorb (input0 input1 input2 input3: t_Slice u8)
     : Prims.Pure t_Shake128x4 Prims.l_True (fun _ -> Prims.l_True)
 
+val init_absorb_shake256 (input: t_Slice u8)
+    : Prims.Pure t_Shake256 Prims.l_True (fun _ -> Prims.l_True)
+
 val init_absorb_x4 (input0 input1 input2 input3: t_Slice u8)
     : Prims.Pure t_Shake256x4 Prims.l_True (fun _ -> Prims.l_True)
 
+val shake256 (v_OUTPUT_LENGTH: usize) (input: t_Slice u8) (out: t_Array u8 v_OUTPUT_LENGTH)
+    : Prims.Pure (t_Array u8 v_OUTPUT_LENGTH) Prims.l_True (fun _ -> Prims.l_True)
+
 val shake256_x4
       (v_OUT_LEN: usize)
       (input0 input1 input2 input3: t_Slice u8)
@@ -27,6 +36,9 @@ val shake256_x4
       Prims.l_True
       (fun _ -> Prims.l_True)
 
+val squeeze_first_block_shake256 (state: t_Shake256)
+    : Prims.Pure (t_Shake256 & t_Array u8 (sz 136)) Prims.l_True (fun _ -> Prims.l_True)
+
 val squeeze_first_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
@@ -143,6 +155,58 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
+val squeeze_next_block_shake256 (state: t_Shake256)
+    : Prims.Pure (t_Shake256 & t_Array u8 (sz 136)) Prims.l_True (fun _ -> Prims.l_True)
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof t_Shake256 =
+  {
+    f_shake256_pre
+    =
+    (fun (v_OUTPUT_LENGTH: usize) (input: t_Slice u8) (out: t_Array u8 v_OUTPUT_LENGTH) -> true);
+    f_shake256_post
+    =
+    (fun
+        (v_OUTPUT_LENGTH: usize)
+        (input: t_Slice u8)
+        (out: t_Array u8 v_OUTPUT_LENGTH)
+        (out1: t_Array u8 v_OUTPUT_LENGTH)
+        ->
+        true);
+    f_shake256
+    =
+    (fun (v_OUTPUT_LENGTH: usize) (input: t_Slice u8) (out: t_Array u8 v_OUTPUT_LENGTH) ->
+        let hax_temp_output, out:(Prims.unit & t_Array u8 v_OUTPUT_LENGTH) =
+          (), shake256 v_OUTPUT_LENGTH input out <: (Prims.unit & t_Array u8 v_OUTPUT_LENGTH)
+        in
+        out);
+    f_init_absorb_pre = (fun (input: t_Slice u8) -> true);
+    f_init_absorb_post = (fun (input: t_Slice u8) (out: t_Shake256) -> true);
+    f_init_absorb = (fun (input: t_Slice u8) -> init_absorb_shake256 input);
+    f_squeeze_first_block_pre = (fun (self: t_Shake256) -> true);
+    f_squeeze_first_block_post
+    =
+    (fun (self: t_Shake256) (out2: (t_Shake256 & t_Array u8 (sz 136))) -> true);
+    f_squeeze_first_block
+    =
+    (fun (self: t_Shake256) ->
+        let tmp0, out1:(t_Shake256 & t_Array u8 (sz 136)) = squeeze_first_block_shake256 self in
+        let self:t_Shake256 = tmp0 in
+        let hax_temp_output:t_Array u8 (sz 136) = out1 in
+        self, hax_temp_output <: (t_Shake256 & t_Array u8 (sz 136)));
+    f_squeeze_next_block_pre = (fun (self: t_Shake256) -> true);
+    f_squeeze_next_block_post
+    =
+    (fun (self: t_Shake256) (out2: (t_Shake256 & t_Array u8 (sz 136))) -> true);
+    f_squeeze_next_block
+    =
+    fun (self: t_Shake256) ->
+      let tmp0, out1:(t_Shake256 & t_Array u8 (sz 136)) = squeeze_next_block_shake256 self in
+      let self:t_Shake256 = tmp0 in
+      let hax_temp_output:t_Array u8 (sz 136) = out1 in
+      self, hax_temp_output <: (t_Shake256 & t_Array u8 (sz 136))
+  }
+
 val squeeze_next_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
@@ -151,7 +215,7 @@ val squeeze_next_block_x4 (state: t_Shake256x4)
       (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 t_Shake256x4 =
+let impl_2: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 t_Shake256x4 =
   {
     f_init_absorb_x4_pre
     =

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fst

@@ -0,0 +1,97 @@
+module Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
+open Core
+open FStar.Mul
+
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Libcrux_ml_dsa.Hash_functions.Shake128 in
+  let open Libcrux_ml_dsa.Hash_functions.Shake256 in
+  let open Libcrux_ml_dsa.Hash_functions.Simd256 in
+  let open Libcrux_ml_dsa.Pre_hash in
+  let open Libcrux_ml_dsa.Simd.Avx2 in
+  let open Libcrux_ml_dsa.Simd.Traits in
+  ()
+
+let generate_key_pair
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE:
+          usize)
+      (randomness: t_Array u8 (sz 32))
+     =
+  Libcrux_ml_dsa.Ml_dsa_generic.generate_key_pair #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA
+    v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE randomness
+
+let sign
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize)
+      (v_GAMMA2: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE:
+          usize)
+      (signing_key: t_Array u8 v_SIGNING_KEY_SIZE)
+      (message context: t_Slice u8)
+      (randomness: t_Array u8 (sz 32))
+     =
+  Libcrux_ml_dsa.Ml_dsa_generic.sign #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA
+    v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 v_COMMITMENT_RING_ELEMENT_SIZE
+    v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT
+    v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE signing_key message context
+    randomness
+
+let sign_pre_hashed_shake128
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize)
+      (v_GAMMA2: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE:
+          usize)
+      (signing_key: t_Array u8 v_SIGNING_KEY_SIZE)
+      (message context: t_Slice u8)
+      (randomness: t_Array u8 (sz 32))
+     =
+  Libcrux_ml_dsa.Ml_dsa_generic.sign_pre_hashed #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH
+    (sz 256) v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2
+    v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE
+    v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE
+    v_SIGNATURE_SIZE signing_key message context randomness
+
+let verify
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE:
+          usize)
+      (v_GAMMA2 v_BETA: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT:
+          usize)
+      (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE)
+      (message context: t_Slice u8)
+      (signature: t_Array u8 v_SIGNATURE_SIZE)
+     =
+  Libcrux_ml_dsa.Ml_dsa_generic.verify #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE
+    v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 v_BETA
+    v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE
+    v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT verification_key message context signature
+
+let verify_pre_hashed_shake128
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE:
+          usize)
+      (v_GAMMA2 v_BETA: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT:
+          usize)
+      (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE)
+      (message context: t_Slice u8)
+      (signature: t_Array u8 v_SIGNATURE_SIZE)
+     =
+  Libcrux_ml_dsa.Ml_dsa_generic.verify_pre_hashed #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
+    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH
+    (sz 256) v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT
+    v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 v_BETA v_COMMITMENT_RING_ELEMENT_SIZE
+    v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT
+    verification_key message context signature

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fsti

@@ -0,0 +1,78 @@
+module Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
+open Core
+open FStar.Mul
+
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Libcrux_ml_dsa.Hash_functions.Shake128 in
+  let open Libcrux_ml_dsa.Hash_functions.Shake256 in
+  let open Libcrux_ml_dsa.Hash_functions.Simd256 in
+  let open Libcrux_ml_dsa.Pre_hash in
+  let open Libcrux_ml_dsa.Simd.Avx2 in
+  let open Libcrux_ml_dsa.Simd.Traits in
+  ()
+
+/// Generate key pair.
+val generate_key_pair
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE:
+          usize)
+      (randomness: t_Array u8 (sz 32))
+    : Prims.Pure (t_Array u8 v_SIGNING_KEY_SIZE & t_Array u8 v_VERIFICATION_KEY_SIZE)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
+/// Sign.
+val sign
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize)
+      (v_GAMMA2: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE:
+          usize)
+      (signing_key: t_Array u8 v_SIGNING_KEY_SIZE)
+      (message context: t_Slice u8)
+      (randomness: t_Array u8 (sz 32))
+    : Prims.Pure
+      (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE)
+          Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True)
+
+/// Sign (pre-hashed).
+val sign_pre_hashed_shake128
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize)
+      (v_GAMMA2: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE:
+          usize)
+      (signing_key: t_Array u8 v_SIGNING_KEY_SIZE)
+      (message context: t_Slice u8)
+      (randomness: t_Array u8 (sz 32))
+    : Prims.Pure
+      (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE)
+          Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True)
+
+/// Verify.
+val verify
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE:
+          usize)
+      (v_GAMMA2 v_BETA: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT:
+          usize)
+      (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE)
+      (message context: t_Slice u8)
+      (signature: t_Array u8 v_SIGNATURE_SIZE)
+    : Prims.Pure (Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
+/// Verify (pre-hashed with SHAKE-128).
+val verify_pre_hashed_shake128
+      (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE:
+          usize)
+      (v_GAMMA2 v_BETA: i32)
+      (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT:
+          usize)
+      (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE)
+      (message context: t_Slice u8)
+      (signature: t_Array u8 v_SIGNATURE_SIZE)
+    : Prims.Pure (Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError)
+      Prims.l_True
+      (fun _ -> Prims.l_True)

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.fst

@@ -3,28 +3,18 @@ module Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2
 open Core
 open FStar.Mul
 
-let _ =
-  (* This module has implicit dependencies, here we make them explicit. *)
-  (* The implicit dependencies arise from typeclasses instances. *)
-  let open Libcrux_ml_dsa.Hash_functions.Portable in
-  let open Libcrux_ml_dsa.Hash_functions.Shake128 in
-  let open Libcrux_ml_dsa.Hash_functions.Shake256 in
-  let open Libcrux_ml_dsa.Hash_functions.Simd256 in
-  let open Libcrux_ml_dsa.Pre_hash in
-  let open Libcrux_ml_dsa.Simd.Avx2 in
-  let open Libcrux_ml_dsa.Simd.Traits in
-  ()
-
 let generate_key_pair
       (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE:
           usize)
       (randomness: t_Array u8 (sz 32))
      =
-  Libcrux_ml_dsa.Ml_dsa_generic.generate_key_pair #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
-    #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA
-    v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE randomness
+  Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.generate_key_pair v_ROWS_IN_A
+    v_COLUMNS_IN_A
+    v_ETA
+    v_ERROR_RING_ELEMENT_SIZE
+    v_SIGNING_KEY_SIZE
+    v_VERIFICATION_KEY_SIZE
+    randomness
 
 let sign
       (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize)
@@ -35,11 +25,8 @@ let sign
       (message context: t_Slice u8)
       (randomness: t_Array u8 (sz 32))
      =
-  Libcrux_ml_dsa.Ml_dsa_generic.sign #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
-    #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA
-    v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 v_COMMITMENT_RING_ELEMENT_SIZE
+  Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.sign v_ROWS_IN_A v_COLUMNS_IN_A
+    v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 v_COMMITMENT_RING_ELEMENT_SIZE
     v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT
     v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE signing_key message context
     randomness
@@ -53,11 +40,8 @@ let sign_pre_hashed_shake128
       (message context: t_Slice u8)
       (randomness: t_Array u8 (sz 32))
      =
-  Libcrux_ml_dsa.Ml_dsa_generic.sign_pre_hashed #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
-    #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH
-    (sz 256) v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2
+  Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.sign_pre_hashed_shake128 v_ROWS_IN_A
+    v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2
     v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE
     v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE
     v_SIGNATURE_SIZE signing_key message context randomness
@@ -72,11 +56,9 @@ let verify
       (message context: t_Slice u8)
       (signature: t_Array u8 v_SIGNATURE_SIZE)
      =
-  Libcrux_ml_dsa.Ml_dsa_generic.verify #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
-    #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE
-    v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 v_BETA
-    v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE
+  Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.verify v_ROWS_IN_A v_COLUMNS_IN_A
+    v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2
+    v_BETA v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE
     v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT verification_key message context signature
 
 let verify_pre_hashed_shake128
@@ -89,10 +71,8 @@ let verify_pre_hashed_shake128
       (message context: t_Slice u8)
       (signature: t_Array u8 v_SIGNATURE_SIZE)
      =
-  Libcrux_ml_dsa.Ml_dsa_generic.verify_pre_hashed #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit
-    #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4
-    #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH
-    (sz 256) v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT
+  Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.verify_pre_hashed_shake128 v_ROWS_IN_A
+    v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT
     v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 v_BETA v_COMMITMENT_RING_ELEMENT_SIZE
     v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT
     verification_key message context signature