fstar

cryspen · Dec 3, 2024 · 83a72e7 · 83a72e7
1 parent 294c580
commit 83a72e7
Show file tree

Hide file tree

Showing 4 changed files with 127 additions and 172 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fst
@@ -9,103 +9,10 @@ let impl_13__len (v_SIZE: usize) (_: Prims.unit) = v_SIZE
 
 let impl_20__len (v_SIZE: usize) (_: Prims.unit) = v_SIZE
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true);
-    f_from
-    =
-    fun (value: t_Array u8 v_SIZE) ->
-      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
-      <:
-      t_MlKemCiphertext v_SIZE
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_MlKemCiphertext v_SIZE) -> true);
-    f_from_post = (fun (value: t_MlKemCiphertext v_SIZE) (out: t_Array u8 v_SIZE) -> true);
-    f_from = fun (value: t_MlKemCiphertext v_SIZE) -> value.f_value
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post
-    =
-    (fun (value: t_Array u8 v_SIZE) (result: t_MlKemCiphertext v_SIZE) -> result.f_value = value);
-    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemCiphertext v_SIZE
-  }
-
 let impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE) = self.f_value
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPrivateKey v_SIZE) -> true);
-    f_from
-    =
-    fun (value: t_Array u8 v_SIZE) ->
-      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
-      <:
-      t_MlKemPrivateKey v_SIZE
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_MlKemPrivateKey v_SIZE) -> true);
-    f_from_post = (fun (value: t_MlKemPrivateKey v_SIZE) (out: t_Array u8 v_SIZE) -> true);
-    f_from = fun (value: t_MlKemPrivateKey v_SIZE) -> value.f_value
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post
-    =
-    (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPrivateKey v_SIZE) -> result.f_value = value);
-    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPrivateKey v_SIZE
-  }
-
 let impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE) = self.f_value
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPublicKey v_SIZE) -> true);
-    f_from
-    =
-    fun (value: t_Array u8 v_SIZE) ->
-      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
-      <:
-      t_MlKemPublicKey v_SIZE
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_MlKemPublicKey v_SIZE) -> true);
-    f_from_post = (fun (value: t_MlKemPublicKey v_SIZE) (out: t_Array u8 v_SIZE) -> true);
-    f_from = fun (value: t_MlKemPublicKey v_SIZE) -> value.f_value
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
-  {
-    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
-    f_from_post
-    =
-    (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPublicKey v_SIZE) -> result.f_value = value);
-    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPublicKey v_SIZE
-  }
-
 let impl_20__as_slice (v_SIZE: usize) (self: t_MlKemPublicKey v_SIZE) = self.f_value
 
 let impl_21__from
@@ -178,65 +85,3 @@ let unpack_private_key (v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE: usize) (private
   <:
   (t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8)
 
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) =
-  {
-    f_default_pre = (fun (_: Prims.unit) -> true);
-    f_default_post = (fun (_: Prims.unit) (out: t_MlKemCiphertext v_SIZE) -> true);
-    f_default
-    =
-    fun (_: Prims.unit) ->
-      { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemCiphertext v_SIZE
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) =
-  {
-    f_default_pre = (fun (_: Prims.unit) -> true);
-    f_default_post = (fun (_: Prims.unit) (out: t_MlKemPrivateKey v_SIZE) -> true);
-    f_default
-    =
-    fun (_: Prims.unit) ->
-      { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPrivateKey v_SIZE
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) =
-  {
-    f_default_pre = (fun (_: Prims.unit) -> true);
-    f_default_post = (fun (_: Prims.unit) (out: t_MlKemPublicKey v_SIZE) -> true);
-    f_default
-    =
-    fun (_: Prims.unit) ->
-      { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPublicKey v_SIZE
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) =
-  {
-    f_as_ref_pre = (fun (self: t_MlKemCiphertext v_SIZE) -> true);
-    f_as_ref_post
-    =
-    (fun (self___: t_MlKemCiphertext v_SIZE) (result: t_Slice u8) -> result = self___.f_value);
-    f_as_ref = fun (self: t_MlKemCiphertext v_SIZE) -> self.f_value <: t_Slice u8
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) =
-  {
-    f_as_ref_pre = (fun (self: t_MlKemPrivateKey v_SIZE) -> true);
-    f_as_ref_post
-    =
-    (fun (self___: t_MlKemPrivateKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value);
-    f_as_ref = fun (self: t_MlKemPrivateKey v_SIZE) -> self.f_value <: t_Slice u8
-  }
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) =
-  {
-    f_as_ref_pre = (fun (self: t_MlKemPublicKey v_SIZE) -> true);
-    f_as_ref_post
-    =
-    (fun (self___: t_MlKemPublicKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value);
-    f_as_ref = fun (self: t_MlKemPublicKey v_SIZE) -> self.f_value <: t_Slice u8
-  }
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti
@@ -19,13 +19,35 @@ val impl_20__len: v_SIZE: usize -> Prims.unit
 type t_MlKemCiphertext (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE)
+let impl_1 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
+    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemCiphertext v_SIZE) -> true);
+    f_from
+    =
+    fun (value: t_Array u8 v_SIZE) ->
+      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
+      <:
+      t_MlKemCiphertext v_SIZE
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE)
+let impl_2 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemCiphertext v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_MlKemCiphertext v_SIZE) -> true);
+    f_from_post = (fun (value: t_MlKemCiphertext v_SIZE) (out: t_Array u8 v_SIZE) -> true);
+    f_from = fun (value: t_MlKemCiphertext v_SIZE) -> value.f_value
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE)
+let impl_5 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemCiphertext v_SIZE) (t_Array u8 v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
+    f_from_post
+    =
+    (fun (value: t_Array u8 v_SIZE) (result: t_MlKemCiphertext v_SIZE) -> result.f_value = value);
+    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemCiphertext v_SIZE
+  }
 
 /// A reference to the raw byte slice.
 val impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE)
@@ -40,13 +62,35 @@ val impl_6__as_slice (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE)
 type t_MlKemPrivateKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE)
+let impl_8 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
+    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPrivateKey v_SIZE) -> true);
+    f_from
+    =
+    fun (value: t_Array u8 v_SIZE) ->
+      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
+      <:
+      t_MlKemPrivateKey v_SIZE
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE)
+let impl_9 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPrivateKey v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_MlKemPrivateKey v_SIZE) -> true);
+    f_from_post = (fun (value: t_MlKemPrivateKey v_SIZE) (out: t_Array u8 v_SIZE) -> true);
+    f_from = fun (value: t_MlKemPrivateKey v_SIZE) -> value.f_value
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE)
+let impl_12 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPrivateKey v_SIZE) (t_Array u8 v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
+    f_from_post
+    =
+    (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPrivateKey v_SIZE) -> result.f_value = value);
+    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPrivateKey v_SIZE
+  }
 
 /// A reference to the raw byte slice.
 val impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE)
@@ -61,13 +105,35 @@ val impl_13__as_slice (v_SIZE: usize) (self: t_MlKemPrivateKey v_SIZE)
 type t_MlKemPublicKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE)
+let impl_15 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
+    f_from_post = (fun (value: t_Array u8 v_SIZE) (out: t_MlKemPublicKey v_SIZE) -> true);
+    f_from
+    =
+    fun (value: t_Array u8 v_SIZE) ->
+      { f_value = Core.Clone.f_clone #(t_Array u8 v_SIZE) #FStar.Tactics.Typeclasses.solve value }
+      <:
+      t_MlKemPublicKey v_SIZE
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE)
+let impl_16 (v_SIZE: usize) : Core.Convert.t_From (t_Array u8 v_SIZE) (t_MlKemPublicKey v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_MlKemPublicKey v_SIZE) -> true);
+    f_from_post = (fun (value: t_MlKemPublicKey v_SIZE) (out: t_Array u8 v_SIZE) -> true);
+    f_from = fun (value: t_MlKemPublicKey v_SIZE) -> value.f_value
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE)
+let impl_19 (v_SIZE: usize) : Core.Convert.t_From (t_MlKemPublicKey v_SIZE) (t_Array u8 v_SIZE) =
+  {
+    f_from_pre = (fun (value: t_Array u8 v_SIZE) -> true);
+    f_from_post
+    =
+    (fun (value: t_Array u8 v_SIZE) (result: t_MlKemPublicKey v_SIZE) -> result.f_value = value);
+    f_from = fun (value: t_Array u8 v_SIZE) -> { f_value = value } <: t_MlKemPublicKey v_SIZE
+  }
 
 /// A reference to the raw byte slice.
 val impl_20__as_slice (v_SIZE: usize) (self: t_MlKemPublicKey v_SIZE)
@@ -169,22 +235,67 @@ val unpack_private_key (v_CPA_SECRET_KEY_SIZE v_PUBLIC_KEY_SIZE: usize) (private
             v Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE))
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE)
+let impl (v_SIZE: usize) : Core.Default.t_Default (t_MlKemCiphertext v_SIZE) =
+  {
+    f_default_pre = (fun (_: Prims.unit) -> true);
+    f_default_post = (fun (_: Prims.unit) (out: t_MlKemCiphertext v_SIZE) -> true);
+    f_default
+    =
+    fun (_: Prims.unit) ->
+      { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemCiphertext v_SIZE
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE)
+let impl_7 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPrivateKey v_SIZE) =
+  {
+    f_default_pre = (fun (_: Prims.unit) -> true);
+    f_default_post = (fun (_: Prims.unit) (out: t_MlKemPrivateKey v_SIZE) -> true);
+    f_default
+    =
+    fun (_: Prims.unit) ->
+      { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPrivateKey v_SIZE
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE)
+let impl_14 (v_SIZE: usize) : Core.Default.t_Default (t_MlKemPublicKey v_SIZE) =
+  {
+    f_default_pre = (fun (_: Prims.unit) -> true);
+    f_default_post = (fun (_: Prims.unit) (out: t_MlKemPublicKey v_SIZE) -> true);
+    f_default
+    =
+    fun (_: Prims.unit) ->
+      { f_value = Rust_primitives.Hax.repeat 0uy v_SIZE } <: t_MlKemPublicKey v_SIZE
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8)
+let impl_4 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemCiphertext v_SIZE) (t_Slice u8) =
+  {
+    f_as_ref_pre = (fun (self: t_MlKemCiphertext v_SIZE) -> true);
+    f_as_ref_post
+    =
+    (fun (self___: t_MlKemCiphertext v_SIZE) (result: t_Slice u8) -> result = self___.f_value);
+    f_as_ref = fun (self: t_MlKemCiphertext v_SIZE) -> self.f_value <: t_Slice u8
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8)
+let impl_11 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPrivateKey v_SIZE) (t_Slice u8) =
+  {
+    f_as_ref_pre = (fun (self: t_MlKemPrivateKey v_SIZE) -> true);
+    f_as_ref_post
+    =
+    (fun (self___: t_MlKemPrivateKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value);
+    f_as_ref = fun (self: t_MlKemPrivateKey v_SIZE) -> self.f_value <: t_Slice u8
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8)
+let impl_18 (v_SIZE: usize) : Core.Convert.t_AsRef (t_MlKemPublicKey v_SIZE) (t_Slice u8) =
+  {
+    f_as_ref_pre = (fun (self: t_MlKemPublicKey v_SIZE) -> true);
+    f_as_ref_post
+    =
+    (fun (self___: t_MlKemPublicKey v_SIZE) (result: t_Slice u8) -> result = self___.f_value);
+    f_as_ref = fun (self: t_MlKemPublicKey v_SIZE) -> self.f_value <: t_Slice u8
+  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_3 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemCiphertext v_SIZE) (t_Slice u8) =

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst
@@ -184,7 +184,7 @@ let cond_subtract_3329_ (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
 
 #pop-options
 
-#push-options "--z3rlimit 200"
+#push-options "--z3rlimit 250"
 
 let montgomery_multiply_by_constant
       (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256)

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Serialize.fst
@@ -38,7 +38,6 @@ let deserialize_1_ (bytes: t_Slice u8) =
   deserialize_1___deserialize_1_u8s (bytes.[ sz 0 ] <: u8) (bytes.[ sz 1 ] <: u8)
 
 [@@"opaque_to_smt"]
-
 let deserialize_4___deserialize_4_i16s (b0 b1 b2 b3 b4 b5 b6 b7: i16) =
   let coefficients:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
     Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 b7 b7 b6 b6 b5 b5 b4 b4 b3 b3 b2 b2 b1 b1 b0 b0