From 32c471287954cdfd8c4c68a5bb6466e6a3a070af Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Tue, 20 Feb 2024 10:47:09 +0100
Subject: [PATCH] chore(kyber/F*): patches

---
 proofs/fstar/extraction-edited.patch          | 140 ++++++++--------
 .../fstar/extraction-secret-independent.patch | 154 +++++++++---------
 2 files changed, 155 insertions(+), 139 deletions(-)

diff --git a/proofs/fstar/extraction-edited.patch b/proofs/fstar/extraction-edited.patch
index e94f3b64..b828a0d7 100644
--- a/proofs/fstar/extraction-edited.patch
+++ b/proofs/fstar/extraction-edited.patch
@@ -1,6 +1,6 @@
 diff -ruN extraction/BitVecEq.fst extraction-edited/BitVecEq.fst
 --- extraction/BitVecEq.fst	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-edited/BitVecEq.fst	2024-02-20 09:10:16.218249868 +0100
++++ extraction-edited/BitVecEq.fst	2024-02-20 10:46:13.853093120 +0100
 @@ -0,0 +1,12 @@
 +module BitVecEq
 +
@@ -16,7 +16,7 @@ diff -ruN extraction/BitVecEq.fst extraction-edited/BitVecEq.fst
 +
 diff -ruN extraction/BitVecEq.fsti extraction-edited/BitVecEq.fsti
 --- extraction/BitVecEq.fsti	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-edited/BitVecEq.fsti	2024-02-20 09:10:16.254245649 +0100
++++ extraction-edited/BitVecEq.fsti	2024-02-20 10:46:13.894092295 +0100
 @@ -0,0 +1,294 @@
 +module BitVecEq
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -313,7 +313,7 @@ diff -ruN extraction/BitVecEq.fsti extraction-edited/BitVecEq.fsti
 + = admit ()
 +*)
 diff -ruN extraction/Libcrux.Digest.fst extraction-edited/Libcrux.Digest.fst
---- extraction/Libcrux.Digest.fst	2024-02-20 09:10:16.186253617 +0100
+--- extraction/Libcrux.Digest.fst	2024-02-20 10:46:13.825093683 +0100
 +++ extraction-edited/Libcrux.Digest.fst	1970-01-01 01:00:00.000000000 +0100
 @@ -1,48 +0,0 @@
 -module Libcrux.Digest
@@ -365,8 +365,8 @@ diff -ruN extraction/Libcrux.Digest.fst extraction-edited/Libcrux.Digest.fst
 -  then shake128x4_256_ v_LEN data0 data1 data2 data3
 -  else shake128x4_portable v_LEN data0 data1 data2 data3
 diff -ruN extraction/Libcrux.Digest.fsti extraction-edited/Libcrux.Digest.fsti
---- extraction/Libcrux.Digest.fsti	2024-02-20 09:10:16.175254907 +0100
-+++ extraction-edited/Libcrux.Digest.fsti	2024-02-20 09:10:16.249246235 +0100
+--- extraction/Libcrux.Digest.fsti	2024-02-20 10:46:13.815093884 +0100
++++ extraction-edited/Libcrux.Digest.fsti	2024-02-20 10:46:13.890092375 +0100
 @@ -3,6 +3,11 @@
  open Core
  open FStar.Mul
@@ -393,7 +393,7 @@ diff -ruN extraction/Libcrux.Digest.fsti extraction-edited/Libcrux.Digest.fsti
      : Prims.Pure (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)
 diff -ruN extraction/Libcrux.Kem.fst extraction-edited/Libcrux.Kem.fst
 --- extraction/Libcrux.Kem.fst	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-edited/Libcrux.Kem.fst	2024-02-20 09:10:16.237247641 +0100
++++ extraction-edited/Libcrux.Kem.fst	2024-02-20 10:46:13.879092596 +0100
 @@ -0,0 +1,6 @@
 +module Libcrux.Kem
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -402,9 +402,9 @@ diff -ruN extraction/Libcrux.Kem.fst extraction-edited/Libcrux.Kem.fst
 +
 +
 diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst
---- extraction/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 09:10:16.190253149 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 09:10:16.232248227 +0100
-@@ -1,81 +1,356 @@
+--- extraction/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 10:46:13.828093623 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 10:46:13.874092697 +0100
+@@ -1,81 +1,364 @@
  module Libcrux.Kem.Kyber.Arithmetic
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -447,7 +447,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.
 +let cast_i32_b #b1 #b2 x =
 +  x <: i32_b b2 
 +
-+#push-options "--ifuel 0 --z3rlimit 150"
++#push-options "--ifuel 0 --z3rlimit 250"
 +let shr_i32_b #b #t x y =
 +  let r = (x <: i32) >>! y in
 +  assert (v r == v x / pow2 (v y));
@@ -487,8 +487,16 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.
 +        r <: i32_b (nat_div_ceil b (pow2 (v y))))
 +#pop-options
 +
-+let v_BARRETT_R: i64 = 1L <<! v_BARRETT_SHIFT
-+let v_MONTGOMERY_R: i32 = 1l <<! v_MONTGOMERY_SHIFT
++let v_BARRETT_R: i64 =
++  let result = 1L <<! v_BARRETT_SHIFT in
++  assert_norm (result == mk_int (67108864 @%. Lib.IntTypes.S64));
++  result
++
++let v_MONTGOMERY_R =
++  let result: i32 = 1l <<! v_MONTGOMERY_SHIFT in
++  assert_norm (result == mk_int (65536 @%. Lib.IntTypes.S32));
++  result
++
 +let v_MONTGOMERY_R_INV = 
 +  assert_norm((v 169l * pow2 16) % 3329 == 1);
 +  169l
@@ -684,7 +692,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.
 +let derefine_matrix_b #v_K #b x =
 +  let r = createi v_K (fun i -> derefine_vector_b #v_K #b x.[i]) in
 +  r
-+
+ 
+-let add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement) =
 +let cast_poly_b #b1 #b2 x =
 +  let r = createi (sz 256) (fun i -> (x.f_coefficients.[i] <: i32_b b2)) in
 +  let res = {f_coefficients = r} in
@@ -697,8 +706,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.
 +  eq_intro dx dr;
 +  assert(Seq.equal dx dr);
 +  res
- 
--let add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement) =
++
 +let cast_vector_b #v_K #b1 #b2 x =
 +  let r = createi v_K (fun i -> cast_poly_b #b1 #b2 x.[i]) in
 +  let dx = derefine_vector_b x in
@@ -801,8 +809,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.
 +  
 + 
 diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti
---- extraction/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 09:10:16.165256079 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 09:10:16.222249399 +0100
+--- extraction/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 10:46:13.805094086 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 10:46:13.856093059 +0100
 @@ -3,10 +3,32 @@
  open Core
  open FStar.Mul
@@ -1153,8 +1161,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux
 -                <:
 -                bool))
 diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fst extraction-edited/Libcrux.Kem.Kyber.Compress.fst
---- extraction/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 09:10:16.170255493 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 09:10:16.212250571 +0100
+--- extraction/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 10:46:13.810093985 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 10:46:13.847093240 +0100
 @@ -1,39 +1,79 @@
  module Libcrux.Kem.Kyber.Compress
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -1258,8 +1266,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fst extraction-edited/Libcrux.Ke
 +  res <: Libcrux.Kem.Kyber.Arithmetic.i32_b 3328
 +#pop-options
 diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fsti extraction-edited/Libcrux.Kem.Kyber.Compress.fsti
---- extraction/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 09:10:16.144258540 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 09:10:16.244246821 +0100
+--- extraction/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 10:46:13.794094307 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 10:46:13.886092456 +0100
 @@ -3,8 +3,19 @@
  open Core
  open FStar.Mul
@@ -1325,8 +1333,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fsti extraction-edited/Libcrux.K
 +      (requires fe =. 0l || fe =. 1l) 
 +      (fun result -> v result >= 0 /\ v result < 3329)
 diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst
---- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 09:10:16.191253032 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 09:10:16.225249047 +0100
+--- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 10:46:13.829093603 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 10:46:13.860092979 +0100
 @@ -4,56 +4,163 @@
  open FStar.Mul
  
@@ -1512,8 +1520,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-edited/L
 +  )
 +#pop-options
 diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti
---- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 09:10:16.187253501 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 09:10:16.233248110 +0100
+--- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 10:46:13.827093643 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 10:46:13.876092657 +0100
 @@ -20,7 +20,8 @@
  
  val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8)
@@ -1545,8 +1553,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-edited/
 +          Hax_lib.implies (selector =. 0uy <: bool) (fun _ -> result =. lhs <: bool) &&
 +          Hax_lib.implies (selector <>. 0uy <: bool) (fun _ -> result =. rhs <: bool))
 diff -ruN extraction/Libcrux.Kem.Kyber.fst extraction-edited/Libcrux.Kem.Kyber.fst
---- extraction/Libcrux.Kem.Kyber.fst	2024-02-20 09:10:16.146258305 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.fst	2024-02-20 09:10:16.216250102 +0100
+--- extraction/Libcrux.Kem.Kyber.fst	2024-02-20 10:46:13.795094287 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.fst	2024-02-20 10:46:13.851093160 +0100
 @@ -1,12 +1,29 @@
  module Libcrux.Kem.Kyber
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -1820,8 +1828,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.fst extraction-edited/Libcrux.Kem.Kyber.f
      (Core.Convert.f_into public_key <: Libcrux.Kem.Kyber.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
 +
 diff -ruN extraction/Libcrux.Kem.Kyber.fsti extraction-edited/Libcrux.Kem.Kyber.fsti
---- extraction/Libcrux.Kem.Kyber.fsti	2024-02-20 09:10:16.179254438 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.fsti	2024-02-20 09:10:16.247246469 +0100
+--- extraction/Libcrux.Kem.Kyber.fsti	2024-02-20 10:46:13.819093804 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.fsti	2024-02-20 10:46:13.888092415 +0100
 @@ -10,36 +10,84 @@
    Libcrux.Kem.Kyber.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE +!
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE
@@ -1922,8 +1930,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.fsti extraction-edited/Libcrux.Kem.Kyber.
 +      (ensures (fun kp -> 
 +                (kp.f_sk.f_value,kp.f_pk.f_value) == Spec.Kyber.ind_cca_generate_keypair p randomness))
 diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fst extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst
---- extraction/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 09:10:16.193252797 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 09:10:16.223249282 +0100
+--- extraction/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 10:46:13.831093562 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 10:46:13.858093019 +0100
 @@ -3,13 +3,23 @@
  open Core
  open FStar.Mul
@@ -1976,8 +1984,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fst extraction-edited/Libc
 +  admit(); // We assume that shake128x4 correctly implements XOFx4
 +  out 
 diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti
---- extraction/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 09:10:16.140259008 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 09:10:16.252245883 +0100
+--- extraction/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 10:46:13.791094367 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 10:46:13.893092315 +0100
 @@ -3,12 +3,17 @@
  open Core
  open FStar.Mul
@@ -2003,8 +2011,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-edited/Lib
 +          (ensures (fun res ->
 +            (forall i. i < v v_K ==> Seq.index res i == Spec.Kyber.v_XOF (sz 840) (Seq.index input i))))
 diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst
---- extraction/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 09:10:16.147258188 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 09:10:16.251246001 +0100
+--- extraction/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 10:46:13.797094247 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 10:46:13.891092355 +0100
 @@ -1,5 +1,5 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -2715,8 +2723,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-edited/Libcrux.Kem
 +  res
 + 
 diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti
---- extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 09:10:16.197252329 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 09:10:16.240247290 +0100
+--- extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 10:46:13.834093502 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 10:46:13.881092556 +0100
 @@ -1,80 +1,151 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -2918,8 +2926,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-edited/Libcrux.Ke
 + 
 +    
 diff -ruN extraction/Libcrux.Kem.Kyber.Kyber1024.fst extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst
---- extraction/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 09:10:16.181254204 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 09:10:16.206251274 +0100
+--- extraction/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 10:46:13.821093764 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 10:46:13.842093341 +0100
 @@ -7,19 +7,19 @@
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 3168))
        (ciphertext: Libcrux.Kem.Kyber.Types.t_MlKemCiphertext (sz 1568))
@@ -2953,8 +2961,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber1024.fst extraction-edited/Libcrux.K
      (sz 3168)
      (sz 1568)
 diff -ruN extraction/Libcrux.Kem.Kyber.Kyber512.fst extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst
---- extraction/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 09:10:16.139259125 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 09:10:16.228248696 +0100
+--- extraction/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 10:46:13.789094408 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 10:46:13.863092918 +0100
 @@ -7,19 +7,19 @@
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 1632))
        (ciphertext: Libcrux.Kem.Kyber.Types.t_MlKemCiphertext (sz 768))
@@ -2988,8 +2996,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber512.fst extraction-edited/Libcrux.Ke
      (sz 1632)
      (sz 800)
 diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fst extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst
---- extraction/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 09:10:16.142258774 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 09:10:16.227248813 +0100
+--- extraction/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 10:46:13.792094347 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 10:46:13.861092959 +0100
 @@ -7,19 +7,19 @@
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 2400))
        (ciphertext: Libcrux.Kem.Kyber.Types.t_MlKemCiphertext (sz 1088))
@@ -3023,8 +3031,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fst extraction-edited/Libcrux.Ke
      (sz 2400)
      (sz 1184)
 diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fsti extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti
---- extraction/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 09:10:16.173255141 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 09:10:16.214250337 +0100
+--- extraction/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 10:46:13.813093925 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 10:46:13.850093180 +0100
 @@ -74,14 +74,15 @@
  val decapsulate
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 2400))
@@ -3050,8 +3058,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Kyber768.fsti extraction-edited/Libcrux.K
 -      (fun _ -> Prims.l_True)
 +      (ensures (fun kp -> (kp.f_sk.f_value,kp.f_pk.f_value) == Spec.Kyber.kyber768_generate_keypair randomness))
 diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fst extraction-edited/Libcrux.Kem.Kyber.Matrix.fst
---- extraction/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 09:10:16.151257719 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 09:10:16.257245298 +0100
+--- extraction/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 10:46:13.800094186 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 10:46:13.897092234 +0100
 @@ -3,192 +3,188 @@
  open Core
  open FStar.Mul
@@ -3842,8 +3850,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fst extraction-edited/Libcrux.Kem.
 +  admit(); //P-F
    v_A_transpose
 diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fsti extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti
---- extraction/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 09:10:16.166255961 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 09:10:16.238247524 +0100
+--- extraction/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 10:46:13.807094045 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 10:46:13.880092576 +0100
 @@ -3,39 +3,71 @@
  open Core
  open FStar.Mul
@@ -3946,8 +3954,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Matrix.fsti extraction-edited/Libcrux.Kem
 +        if transpose then Libcrux.Kem.Kyber.Arithmetic.to_spec_matrix_b #p res == matrix_A
 +        else Libcrux.Kem.Kyber.Arithmetic.to_spec_matrix_b #p res == Spec.Kyber.matrix_transpose matrix_A)
 diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fst extraction-edited/Libcrux.Kem.Kyber.Ntt.fst
---- extraction/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 09:10:16.168255727 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 09:10:16.220249633 +0100
+--- extraction/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 10:46:13.809094005 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 10:46:13.855093079 +0100
 @@ -1,56 +1,130 @@
  module Libcrux.Kem.Kyber.Ntt
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -4878,8 +4886,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fst extraction-edited/Libcrux.Kem.Kyb
 +  down_cast_poly_b #(8*3328) #3328 re 
 +#pop-options
 diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fsti extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti
---- extraction/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 09:10:16.172255258 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 09:10:16.202251743 +0100
+--- extraction/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 10:46:13.812093945 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 10:46:13.838093421 +0100
 @@ -2,223 +2,80 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -5172,8 +5180,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Ntt.fsti extraction-edited/Libcrux.Kem.Ky
 +      (ensures fun _ -> True)
 +
 diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fst extraction-edited/Libcrux.Kem.Kyber.Sampling.fst
---- extraction/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 09:10:16.194252680 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 09:10:16.246246586 +0100
+--- extraction/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 10:46:13.832093542 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 10:46:13.887092436 +0100
 @@ -3,27 +3,34 @@
  open Core
  open FStar.Mul
@@ -5586,8 +5594,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fst extraction-edited/Libcrux.Ke
 +  out 
 +#pop-options
 diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fsti extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti
---- extraction/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 09:10:16.163256313 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 09:10:16.256245415 +0100
+--- extraction/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 10:46:13.803094126 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 10:46:13.895092274 +0100
 @@ -3,77 +3,37 @@
  open Core
  open FStar.Mul
@@ -5688,8 +5696,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Sampling.fsti extraction-edited/Libcrux.K
 +//      (ensures fun result -> (forall i. v (result.f_coefficients.[i]) >= 0))
 +      
 diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.Kem.Kyber.Serialize.fst
---- extraction/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 09:10:16.178254555 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 09:10:16.209250923 +0100
+--- extraction/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 10:46:13.818093824 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 10:46:13.845093281 +0100
 @@ -1,8 +1,15 @@
  module Libcrux.Kem.Kyber.Serialize
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -7166,8 +7174,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
 +#pop-options
 +
 diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti
---- extraction/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 09:10:16.149257954 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 09:10:16.241247172 +0100
+--- extraction/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 10:46:13.798094227 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 10:46:13.883092516 +0100
 @@ -2,118 +2,188 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -7425,8 +7433,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux.
 +        int_t_array_bitwise_eq res 8 coefficients 12
 +      ))
 diff -ruN extraction/Libcrux.Kem.Kyber.Types.fst extraction-edited/Libcrux.Kem.Kyber.Types.fst
---- extraction/Libcrux.Kem.Kyber.Types.fst	2024-02-20 09:10:16.161256547 +0100
-+++ extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-02-20 09:10:16.235247876 +0100
+--- extraction/Libcrux.Kem.Kyber.Types.fst	2024-02-20 10:46:13.801094166 +0100
++++ extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-02-20 10:46:13.877092637 +0100
 @@ -50,7 +50,9 @@
  let impl_6__len (v_SIZE: usize) (self: t_MlKemCiphertext v_SIZE) : usize = v_SIZE
  
@@ -7462,7 +7470,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Types.fst extraction-edited/Libcrux.Kem.K
  type t_MlKemKeyPair (v_PRIVATE_KEY_SIZE: usize) (v_PUBLIC_KEY_SIZE: usize) = {
 diff -ruN extraction/Libcrux_platform.Platform.fsti extraction-edited/Libcrux_platform.Platform.fsti
 --- extraction/Libcrux_platform.Platform.fsti	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-edited/Libcrux_platform.Platform.fsti	2024-02-20 09:10:16.230248462 +0100
++++ extraction-edited/Libcrux_platform.Platform.fsti	2024-02-20 10:46:13.873092717 +0100
 @@ -0,0 +1,20 @@
 +module Libcrux_platform.Platform
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -7486,7 +7494,7 @@ diff -ruN extraction/Libcrux_platform.Platform.fsti extraction-edited/Libcrux_pl
 +val simd128_support: Prims.unit -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 diff -ruN extraction/MkSeq.fst extraction-edited/MkSeq.fst
 --- extraction/MkSeq.fst	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-edited/MkSeq.fst	2024-02-20 09:10:16.205251391 +0100
++++ extraction-edited/MkSeq.fst	2024-02-20 10:46:13.841093361 +0100
 @@ -0,0 +1,91 @@
 +module MkSeq
 +open Core
@@ -7581,7 +7589,7 @@ diff -ruN extraction/MkSeq.fst extraction-edited/MkSeq.fst
 +%splice[] (init 13 (fun i -> create_gen_tac (i + 1)))
 diff -ruN extraction/Spec.Kyber.fst extraction-edited/Spec.Kyber.fst
 --- extraction/Spec.Kyber.fst	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-edited/Spec.Kyber.fst	2024-02-20 09:10:16.243246938 +0100
++++ extraction-edited/Spec.Kyber.fst	2024-02-20 10:46:13.884092496 +0100
 @@ -0,0 +1,433 @@
 +module Spec.Kyber
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
diff --git a/proofs/fstar/extraction-secret-independent.patch b/proofs/fstar/extraction-secret-independent.patch
index dc18f7e3..11e71ed8 100644
--- a/proofs/fstar/extraction-secret-independent.patch
+++ b/proofs/fstar/extraction-secret-independent.patch
@@ -1,5 +1,5 @@
 diff -ruN extraction-edited/BitVecEq.fst extraction-secret-independent/BitVecEq.fst
---- extraction-edited/BitVecEq.fst	2024-02-20 09:10:16.218249868 +0100
+--- extraction-edited/BitVecEq.fst	2024-02-20 10:46:13.853093120 +0100
 +++ extraction-secret-independent/BitVecEq.fst	1970-01-01 01:00:00.000000000 +0100
 @@ -1,12 +0,0 @@
 -module BitVecEq
@@ -15,7 +15,7 @@ diff -ruN extraction-edited/BitVecEq.fst extraction-secret-independent/BitVecEq.
 -
 -
 diff -ruN extraction-edited/BitVecEq.fsti extraction-secret-independent/BitVecEq.fsti
---- extraction-edited/BitVecEq.fsti	2024-02-20 09:10:16.254245649 +0100
+--- extraction-edited/BitVecEq.fsti	2024-02-20 10:46:13.894092295 +0100
 +++ extraction-secret-independent/BitVecEq.fsti	1970-01-01 01:00:00.000000000 +0100
 @@ -1,294 +0,0 @@
 -module BitVecEq
@@ -313,8 +313,8 @@ diff -ruN extraction-edited/BitVecEq.fsti extraction-secret-independent/BitVecEq
 - = admit ()
 -*)
 diff -ruN extraction-edited/Libcrux.Digest.fsti extraction-secret-independent/Libcrux.Digest.fsti
---- extraction-edited/Libcrux.Digest.fsti	2024-02-20 09:10:16.249246235 +0100
-+++ extraction-secret-independent/Libcrux.Digest.fsti	2024-02-20 09:10:16.277242954 +0100
+--- extraction-edited/Libcrux.Digest.fsti	2024-02-20 10:46:13.890092375 +0100
++++ extraction-secret-independent/Libcrux.Digest.fsti	2024-02-20 10:46:13.916091852 +0100
 @@ -1,31 +1,41 @@
  module Libcrux.Digest
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -385,9 +385,9 @@ diff -ruN extraction-edited/Libcrux.Digest.fsti extraction-secret-independent/Li
 +
 +val shake256 (v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst
---- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 09:10:16.232248227 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 09:10:16.310239087 +0100
-@@ -1,356 +1,81 @@
+--- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 10:46:13.874092697 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst	2024-02-20 10:46:13.944091288 +0100
+@@ -1,364 +1,81 @@
  module Libcrux.Kem.Kyber.Arithmetic
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -429,7 +429,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-i
 -let cast_i32_b #b1 #b2 x =
 -  x <: i32_b b2 
 -
--#push-options "--ifuel 0 --z3rlimit 150"
+-#push-options "--ifuel 0 --z3rlimit 250"
 -let shr_i32_b #b #t x y =
 -  let r = (x <: i32) >>! y in
 -  assert (v r == v x / pow2 (v y));
@@ -469,8 +469,16 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-i
 -        r <: i32_b (nat_div_ceil b (pow2 (v y))))
 -#pop-options
 -
--let v_BARRETT_R: i64 = 1L <<! v_BARRETT_SHIFT
--let v_MONTGOMERY_R: i32 = 1l <<! v_MONTGOMERY_SHIFT
+-let v_BARRETT_R: i64 =
+-  let result = 1L <<! v_BARRETT_SHIFT in
+-  assert_norm (result == mk_int (67108864 @%. Lib.IntTypes.S64));
+-  result
+-
+-let v_MONTGOMERY_R =
+-  let result: i32 = 1l <<! v_MONTGOMERY_SHIFT in
+-  assert_norm (result == mk_int (65536 @%. Lib.IntTypes.S32));
+-  result
+-
 -let v_MONTGOMERY_R_INV = 
 -  assert_norm((v 169l * pow2 16) % 3329 == 1);
 -  169l
@@ -663,7 +671,10 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-i
 -let derefine_matrix_b #v_K #b x =
 -  let r = createi v_K (fun i -> derefine_vector_b #v_K #b x.[i]) in
 -  r
--
++  cast (fe +! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS &. (fe >>! 31l <: i32) <: i32) <: i32)
++  <:
++  u16
+ 
 -let cast_poly_b #b1 #b2 x =
 -  let r = createi (sz 256) (fun i -> (x.f_coefficients.[i] <: i32_b b2)) in
 -  let res = {f_coefficients = r} in
@@ -676,10 +687,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-i
 -  eq_intro dx dr;
 -  assert(Seq.equal dx dr);
 -  res
-+  cast (fe +! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS &. (fe >>! 31l <: i32) <: i32) <: i32)
-+  <:
-+  u16
- 
+-
 -let cast_vector_b #v_K #b1 #b2 x =
 -  let r = createi v_K (fun i -> cast_poly_b #b1 #b2 x.[i]) in
 -  let dx = derefine_vector_b x in
@@ -783,8 +791,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst extraction-secret-i
 -  
 - 
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 09:10:16.222249399 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 09:10:16.300240259 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 10:46:13.856093059 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-02-20 10:46:13.936091449 +0100
 @@ -3,32 +3,10 @@
  open Core
  open FStar.Mul
@@ -1141,8 +1149,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-secret-
 +                <:
 +                bool))
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fst extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst
---- extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 09:10:16.212250571 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 09:10:16.287241782 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 10:46:13.847093240 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst	2024-02-20 10:46:13.925091671 +0100
 @@ -1,79 +1,39 @@
  module Libcrux.Kem.Kyber.Compress
 -#set-options "--fuel 0 --ifuel 0 --z3rlimit 200"
@@ -1247,8 +1255,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fst extraction-secret-ind
 +  (Core.Ops.Arith.Neg.neg fe <: i32) &.
 +  ((Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS +! 1l <: i32) /! 2l <: i32)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 09:10:16.244246821 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 09:10:16.312238852 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 10:46:13.886092456 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti	2024-02-20 10:46:13.946091248 +0100
 @@ -3,42 +3,44 @@
  open Core
  open FStar.Mul
@@ -1320,8 +1328,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Compress.fsti extraction-secret-in
 -      (fun result -> v result >= 0 /\ v result < 3329)
 +    : Prims.Pure i32 (requires fe =. 0l || fe =. 1l) (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst
---- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 09:10:16.225249047 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 09:10:16.268244008 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 10:46:13.860092979 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-02-20 10:46:13.908092013 +0100
 @@ -4,163 +4,61 @@
  open FStar.Mul
  
@@ -1510,8 +1518,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst extraction-s
 -#pop-options
 +  out
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 09:10:16.233248110 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 09:10:16.304239790 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 10:46:13.876092657 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-02-20 10:46:13.939091389 +0100
 @@ -20,26 +20,30 @@
  
  val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8)
@@ -1555,7 +1563,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti extraction-
 +                result = rhs <: bool))
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Conversions.fst extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst
 --- extraction-edited/Libcrux.Kem.Kyber.Conversions.fst	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst	2024-02-20 09:10:16.265244360 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst	2024-02-20 10:46:13.905092073 +0100
 @@ -0,0 +1,87 @@
 +module Libcrux.Kem.Kyber.Conversions
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -1646,8 +1654,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Conversions.fst extraction-secret-
 +  cast (fe +! ((fe >>! 15l <: i32) &. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32)) <: u16
 \ Pas de fin de ligne à la fin du fichier
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.fst extraction-secret-independent/Libcrux.Kem.Kyber.fst
---- extraction-edited/Libcrux.Kem.Kyber.fst	2024-02-20 09:10:16.216250102 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.fst	2024-02-20 09:10:16.284242134 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.fst	2024-02-20 10:46:13.851093160 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.fst	2024-02-20 10:46:13.922091731 +0100
 @@ -1,29 +1,12 @@
  module Libcrux.Kem.Kyber
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -1926,8 +1934,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.fst extraction-secret-independent/
 -
 +    (Core.Convert.f_into public_key <: Libcrux.Kem.Kyber.Types.t_KyberPublicKey v_PUBLIC_KEY_SIZE)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.fsti extraction-secret-independent/Libcrux.Kem.Kyber.fsti
---- extraction-edited/Libcrux.Kem.Kyber.fsti	2024-02-20 09:10:16.247246469 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.fsti	2024-02-20 09:10:16.294240962 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.fsti	2024-02-20 10:46:13.888092415 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.fsti	2024-02-20 10:46:13.930091570 +0100
 @@ -4,90 +4,37 @@
  open FStar.Mul
  
@@ -2036,8 +2044,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.fsti extraction-secret-independent
 +      Prims.l_True
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst
---- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 09:10:16.223249282 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 09:10:16.293241079 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 10:46:13.858093019 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst	2024-02-20 10:46:13.929091590 +0100
 @@ -3,28 +3,18 @@
  open Core
  open FStar.Mul
@@ -2105,8 +2113,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst extraction-secr
 -  out 
 +  out
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 09:10:16.252245883 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 09:10:16.267244126 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 10:46:13.893092315 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-02-20 10:46:13.906092053 +0100
 @@ -3,17 +3,12 @@
  open Core
  open FStar.Mul
@@ -2133,7 +2141,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti extraction-sec
 +    : Prims.Pure (t_Array (t_Array u8 (sz 840)) v_K) Prims.l_True (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Helper.fst extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst
 --- extraction-edited/Libcrux.Kem.Kyber.Helper.fst	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst	2024-02-20 09:10:16.302240024 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst	2024-02-20 10:46:13.937091429 +0100
 @@ -0,0 +1,6 @@
 +module Libcrux.Kem.Kyber.Helper
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -2142,8 +2150,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Helper.fst extraction-secret-indep
 +
 +
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst
---- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 09:10:16.251246001 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 09:10:16.297240610 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 10:46:13.891092355 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-02-20 10:46:13.933091510 +0100
 @@ -1,5 +1,5 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -2858,8 +2866,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst extraction-secret-inde
 -  res
 - 
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 09:10:16.240247290 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 09:10:16.264244477 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 10:46:13.881092556 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-02-20 10:46:13.903092113 +0100
 @@ -1,151 +1,80 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -3061,8 +3069,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti extraction-secret-ind
 +      Prims.l_True
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst
---- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 09:10:16.206251274 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 09:10:16.274243305 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 10:46:13.842093341 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst	2024-02-20 10:46:13.914091892 +0100
 @@ -3,37 +3,22 @@
  open Core
  open FStar.Mul
@@ -3111,8 +3119,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst extraction-secret-in
      (sz 3168)
      (sz 1568)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-02-20 09:10:16.209250923 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-02-20 09:10:16.289241548 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-02-20 10:46:13.844093301 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-02-20 10:46:13.926091651 +0100
 @@ -63,32 +63,27 @@
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_1024_
  
@@ -3158,8 +3166,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti extraction-secret-i
        Prims.l_True
        (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst
---- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 09:10:16.228248696 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 09:10:16.316238384 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 10:46:13.863092918 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst	2024-02-20 10:46:13.949091188 +0100
 @@ -3,37 +3,22 @@
  open Core
  open FStar.Mul
@@ -3208,8 +3216,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst extraction-secret-ind
      (sz 1632)
      (sz 800)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti	2024-02-20 09:10:16.203251625 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fsti	2024-02-20 09:10:16.272243540 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti	2024-02-20 10:46:13.839093401 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fsti	2024-02-20 10:46:13.912091932 +0100
 @@ -63,32 +63,27 @@
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_512_
  
@@ -3255,8 +3263,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti extraction-secret-in
        Prims.l_True
        (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst
---- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 09:10:16.227248813 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 09:10:16.309239204 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 10:46:13.861092959 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst	2024-02-20 10:46:13.943091308 +0100
 @@ -3,37 +3,22 @@
  open Core
  open FStar.Mul
@@ -3305,8 +3313,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst extraction-secret-ind
      (sz 2400)
      (sz 1184)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 09:10:16.214250337 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 09:10:16.279242719 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 10:46:13.850093180 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti	2024-02-20 10:46:13.918091812 +0100
 @@ -63,33 +63,27 @@
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_768_
  
@@ -3355,8 +3363,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti extraction-secret-in
 -      (ensures (fun kp -> (kp.f_sk.f_value,kp.f_pk.f_value) == Spec.Kyber.kyber768_generate_keypair randomness))
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fst extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst
---- extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 09:10:16.257245298 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 09:10:16.282242368 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 10:46:13.897092234 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst	2024-02-20 10:46:13.921091751 +0100
 @@ -3,418 +3,432 @@
  open Core
  open FStar.Mul
@@ -4165,8 +4173,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fst extraction-secret-indep
 -  admit(); //P-F
    v_A_transpose
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 09:10:16.238247524 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 09:10:16.305239673 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 10:46:13.880092576 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti	2024-02-20 10:46:13.940091369 +0100
 @@ -3,71 +3,39 @@
  open Core
  open FStar.Mul
@@ -4269,8 +4277,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti extraction-secret-inde
 +      Prims.l_True
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fst extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst
---- extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 09:10:16.220249633 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 09:10:16.291241313 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 10:46:13.855093079 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst	2024-02-20 10:46:13.928091610 +0100
 @@ -1,130 +1,56 @@
  module Libcrux.Kem.Kyber.Ntt
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -5201,8 +5209,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fst extraction-secret-independ
 -#pop-options
 +  re
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 09:10:16.202251743 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 09:10:16.314238618 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 10:46:13.838093421 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti	2024-02-20 10:46:13.947091228 +0100
 @@ -2,80 +2,224 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -5496,8 +5504,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti extraction-secret-indepen
 +                <:
 +                bool))
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fst extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst
---- extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 09:10:16.246246586 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 09:10:16.262244712 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 10:46:13.887092436 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst	2024-02-20 10:46:13.902092134 +0100
 @@ -3,34 +3,27 @@
  open Core
  open FStar.Mul
@@ -5934,8 +5942,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fst extraction-secret-ind
 -#pop-options
 +  out
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 09:10:16.256245415 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 09:10:16.299240376 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 10:46:13.895092274 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti	2024-02-20 10:46:13.935091469 +0100
 @@ -3,37 +3,77 @@
  open Core
  open FStar.Mul
@@ -6036,8 +6044,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti extraction-secret-in
 +      Prims.l_True
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst
---- extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 09:10:16.209250923 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 09:10:16.281242485 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 10:46:13.845093281 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst	2024-02-20 10:46:13.919091791 +0100
 @@ -1,15 +1,8 @@
  module Libcrux.Kem.Kyber.Serialize
 -#set-options "--fuel 0 --ifuel 0 --z3rlimit 50 --retry 3"
@@ -7521,8 +7529,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fst extraction-secret-in
 -#pop-options
 -
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti
---- extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 09:10:16.241247172 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 09:10:16.270243774 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 10:46:13.883092516 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti	2024-02-20 10:46:13.910091973 +0100
 @@ -2,188 +2,118 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -7780,8 +7788,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti extraction-secret-i
 +val serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement)
 +    : Prims.Pure (t_Array u8 (sz 384)) Prims.l_True (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.Types.fst extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst
---- extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-02-20 09:10:16.235247876 +0100
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst	2024-02-20 09:10:16.275243188 +0100
+--- extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-02-20 10:46:13.877092637 +0100
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst	2024-02-20 10:46:13.915091872 +0100
 @@ -3,31 +3,31 @@
  open Core
  open FStar.Mul
@@ -8050,14 +8058,14 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Types.fst extraction-secret-indepe
      : t_Array u8 v_PRIVATE_KEY_SIZE = impl_12__as_slice v_PRIVATE_KEY_SIZE self.f_sk
 diff -ruN extraction-edited/Libcrux_platform.fsti extraction-secret-independent/Libcrux_platform.fsti
 --- extraction-edited/Libcrux_platform.fsti	1970-01-01 01:00:00.000000000 +0100
-+++ extraction-secret-independent/Libcrux_platform.fsti	2024-02-20 09:10:16.286241899 +0100
++++ extraction-secret-independent/Libcrux_platform.fsti	2024-02-20 10:46:13.923091711 +0100
 @@ -0,0 +1,4 @@
 +module Libcrux_platform
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 +
 +val simd256_support : unit -> bool
 diff -ruN extraction-edited/Libcrux_platform.Platform.fsti extraction-secret-independent/Libcrux_platform.Platform.fsti
---- extraction-edited/Libcrux_platform.Platform.fsti	2024-02-20 09:10:16.230248462 +0100
+--- extraction-edited/Libcrux_platform.Platform.fsti	2024-02-20 10:46:13.873092717 +0100
 +++ extraction-secret-independent/Libcrux_platform.Platform.fsti	1970-01-01 01:00:00.000000000 +0100
 @@ -1,20 +0,0 @@
 -module Libcrux_platform.Platform
@@ -8081,7 +8089,7 @@ diff -ruN extraction-edited/Libcrux_platform.Platform.fsti extraction-secret-ind
 -
 -val simd128_support: Prims.unit -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/MkSeq.fst extraction-secret-independent/MkSeq.fst
---- extraction-edited/MkSeq.fst	2024-02-20 09:10:16.205251391 +0100
+--- extraction-edited/MkSeq.fst	2024-02-20 10:46:13.841093361 +0100
 +++ extraction-secret-independent/MkSeq.fst	1970-01-01 01:00:00.000000000 +0100
 @@ -1,91 +0,0 @@
 -module MkSeq
@@ -8176,7 +8184,7 @@ diff -ruN extraction-edited/MkSeq.fst extraction-secret-independent/MkSeq.fst
 -
 -%splice[] (init 13 (fun i -> create_gen_tac (i + 1)))
 diff -ruN extraction-edited/Spec.Kyber.fst extraction-secret-independent/Spec.Kyber.fst
---- extraction-edited/Spec.Kyber.fst	2024-02-20 09:10:16.243246938 +0100
+--- extraction-edited/Spec.Kyber.fst	2024-02-20 10:46:13.884092496 +0100
 +++ extraction-secret-independent/Spec.Kyber.fst	1970-01-01 01:00:00.000000000 +0100
 @@ -1,433 +0,0 @@
 -module Spec.Kyber