diff --git a/kyber-crate.sh b/kyber-crate.sh
index a5a37263b..289058737 100755
--- a/kyber-crate.sh
+++ b/kyber-crate.sh
@@ -64,7 +64,7 @@ rm src/kyber512.rs
 rm src/kyber1024.rs
 
 # Build & test
-# cargo test
+cargo test
 
 # Extract
 if [[ -z "$CHARON_HOME" ]]; then
diff --git a/proofs/fstar/extraction-edited.patch b/proofs/fstar/extraction-edited.patch
index bd9337bf1..d976d06c8 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
-+++ extraction-edited/BitVecEq.fst	2024-03-18 20:11:28
++++ extraction-edited/BitVecEq.fst	2024-03-18 20:52:52
 @@ -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
-+++ extraction-edited/BitVecEq.fsti	2024-03-18 20:11:28
++++ extraction-edited/BitVecEq.fsti	2024-03-18 20:52:52
 @@ -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.Incremental_x4.fsti extraction-edited/Libcrux.Digest.Incremental_x4.fsti
---- extraction/Libcrux.Digest.Incremental_x4.fsti	2024-03-18 20:11:27
+--- extraction/Libcrux.Digest.Incremental_x4.fsti	2024-03-18 20:52:52
 +++ extraction-edited/Libcrux.Digest.Incremental_x4.fsti	1970-01-01 01:00:00
 @@ -1,23 +0,0 @@
 -module Libcrux.Digest.Incremental_x4
@@ -340,8 +340,8 @@ diff -ruN extraction/Libcrux.Digest.Incremental_x4.fsti extraction-edited/Libcru
 -      Prims.l_True
 -      (fun _ -> Prims.l_True)
 diff -ruN extraction/Libcrux.Digest.fsti extraction-edited/Libcrux.Digest.fsti
---- extraction/Libcrux.Digest.fsti	2024-03-18 20:11:27
-+++ extraction-edited/Libcrux.Digest.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Digest.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Digest.fsti	2024-03-18 20:52:52
 @@ -3,11 +3,29 @@
  open Core
  open FStar.Mul
@@ -373,8 +373,8 @@ diff -ruN extraction/Libcrux.Digest.fsti extraction-edited/Libcrux.Digest.fsti
 +      Prims.l_True
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fst extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst
---- extraction/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:52:52
 @@ -1,81 +1,364 @@
  module Libcrux.Kem.Kyber.Arithmetic
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -780,8 +780,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-03-18 20:52:52
 @@ -3,10 +3,32 @@
  open Core
  open FStar.Mul
@@ -1129,8 +1129,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Arithmetic.fsti extraction-edited/Libcrux
 +
 +
 diff -ruN extraction/Libcrux.Kem.Kyber.Compress.fst extraction-edited/Libcrux.Kem.Kyber.Compress.fst
---- extraction/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:52:52
 @@ -1,39 +1,79 @@
  module Libcrux.Kem.Kyber.Compress
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -1234,8 +1234,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Compress.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-03-18 20:52:52
 @@ -3,8 +3,19 @@
  open Core
  open FStar.Mul
@@ -1301,8 +1301,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-03-18 20:52:52
 @@ -4,56 +4,163 @@
  open FStar.Mul
  
@@ -1488,8 +1488,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-03-18 20:11:28
-+++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-03-18 20:52:52
 @@ -20,7 +20,8 @@
  
  val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8)
@@ -1521,8 +1521,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.Constants.fsti extraction-edited/Libcrux.Kem.Kyber.Constants.fsti
---- extraction/Libcrux.Kem.Kyber.Constants.fsti	2024-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Constants.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Constants.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Constants.fsti	2024-03-18 20:52:52
 @@ -17,4 +17,6 @@
  
  let v_H_DIGEST_SIZE: usize = sz 32
@@ -1531,8 +1531,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Constants.fsti extraction-edited/Libcrux.
 +
  let v_SHARED_SECRET_SIZE: usize = sz 32
 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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Hash_functions.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-03-18 20:52:52
 @@ -3,129 +3,114 @@
  open Core
  open FStar.Mul
@@ -1766,8 +1766,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-03-18 20:52:52
 @@ -3,33 +3,17 @@
  open Core
  open FStar.Mul
@@ -1814,8 +1814,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-03-18 20:52:52
 @@ -1,5 +1,5 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -2519,8 +2519,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-03-18 20:52:52
 @@ -1,80 +1,151 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -2721,8 +2721,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Kyber1024.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-03-18 20:52:52
 @@ -7,19 +7,19 @@
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 3168))
        (ciphertext: Libcrux.Kem.Kyber.Types.t_MlKemCiphertext (sz 1568))
@@ -2756,8 +2756,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Kyber512.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-03-18 20:52:52
 @@ -7,19 +7,19 @@
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 1632))
        (ciphertext: Libcrux.Kem.Kyber.Types.t_MlKemCiphertext (sz 768))
@@ -2791,8 +2791,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Kyber768.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-03-18 20:52:52
 @@ -7,19 +7,19 @@
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 2400))
        (ciphertext: Libcrux.Kem.Kyber.Types.t_MlKemCiphertext (sz 1088))
@@ -2826,8 +2826,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Kyber768.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-03-18 20:52:52
 @@ -74,14 +74,15 @@
  val decapsulate
        (secret_key: Libcrux.Kem.Kyber.Types.t_MlKemPrivateKey (sz 2400))
@@ -2853,8 +2853,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Matrix.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-03-18 20:52:52
 @@ -3,192 +3,188 @@
  open Core
  open FStar.Mul
@@ -3652,8 +3652,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Matrix.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-03-18 20:52:52
 @@ -3,39 +3,71 @@
  open Core
  open FStar.Mul
@@ -3755,8 +3755,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Ntt.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-03-18 20:52:52
 @@ -1,56 +1,130 @@
  module Libcrux.Kem.Kyber.Ntt
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -4666,8 +4666,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Ntt.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-03-18 20:52:52
 @@ -2,223 +2,80 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -4956,8 +4956,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Sampling.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-03-18 20:52:52
 @@ -3,22 +3,34 @@
  open Core
  open FStar.Mul
@@ -5560,8 +5560,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Sampling.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-03-18 20:52:52
 @@ -3,84 +3,37 @@
  open Core
  open FStar.Mul
@@ -5671,8 +5671,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Serialize.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-03-18 20:52:52
 @@ -1,8 +1,15 @@
  module Libcrux.Kem.Kyber.Serialize
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -6234,87 +6234,11 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
    match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with
    | 4ul -> compress_then_serialize_4_ v_OUT_LEN re
    | 5ul -> compress_then_serialize_5_ v_OUT_LEN re
-@@ -665,109 +751,49 @@
+@@ -665,32 +751,49 @@
  
          <:
          Rust_primitives.Hax.t_Never)
--
--let deserialize_ring_elementes_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8) =
--  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
--    Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
-   in
--  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
--    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
--              (Core.Slice.impl__chunks_exact public_key
--                  Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT
--                <:
--                Core.Slice.Iter.t_ChunksExact u8)
--            <:
--            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
--        <:
--        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
--      deserialized_pk
--      (fun deserialized_pk temp_1_ ->
--          let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
--            deserialized_pk
--          in
--          let i, ring_element:(usize & t_Slice u8) = temp_1_ in
--          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
--            Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO
--          in
--          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
--            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
--                      (Core.Slice.impl__chunks_exact ring_element (sz 3)
--                        <:
--                        Core.Slice.Iter.t_ChunksExact u8)
--                    <:
--                    Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
--                <:
--                Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
--              re
--              (fun re temp_1_ ->
--                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement = re in
--                  let i, bytes:(usize & t_Slice u8) = temp_1_ in
--                  let byte1:i32 = cast (bytes.[ sz 0 ] <: u8) <: i32 in
--                  let byte2:i32 = cast (bytes.[ sz 1 ] <: u8) <: i32 in
--                  let byte3:i32 = cast (bytes.[ sz 2 ] <: u8) <: i32 in
--                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
--                    {
--                      re with
--                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
--                      =
--                      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
--                          .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
--                        (sz 2 *! i <: usize)
--                        ((((byte2 &. 15l <: i32) <<! 8l <: i32) |. (byte1 &. 255l <: i32) <: i32) %!
--                          Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
--                          <:
--                          i32)
--                    }
--                    <:
--                    Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
--                  in
--                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
--                    {
--                      re with
--                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
--                      =
--                      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
--                          .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
--                        ((sz 2 *! i <: usize) +! sz 1 <: usize)
--                        (((byte3 <<! 4l <: i32) |. ((byte2 >>! 4l <: i32) &. 15l <: i32) <: i32) %!
--                          Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
--                          <:
--                          i32)
--                    }
--                    <:
--                    Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
--                  in
--                  re)
--          in
--          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize deserialized_pk i re)
--  in
--  deserialized_pk
++  in
 +  admit (); // P-F
 +  res
  
@@ -6379,7 +6303,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -775,14 +801,12 @@
+@@ -698,14 +801,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  (sz 4 *! i <: usize)
@@ -6397,7 +6321,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -790,14 +814,12 @@
+@@ -713,14 +814,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 4 *! i <: usize) +! sz 1 <: usize)
@@ -6415,7 +6339,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -805,14 +827,12 @@
+@@ -728,14 +827,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 4 *! i <: usize) +! sz 2 <: usize)
@@ -6433,7 +6357,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -820,44 +840,43 @@
+@@ -743,44 +840,43 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 4 *! i <: usize) +! sz 3 <: usize)
@@ -6504,7 +6428,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
            let
            coefficient1,
            coefficient2,
-@@ -866,11 +885,21 @@
+@@ -789,11 +885,21 @@
            coefficient5,
            coefficient6,
            coefficient7,
@@ -6528,7 +6452,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -878,14 +907,12 @@
+@@ -801,14 +907,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  (sz 8 *! i <: usize)
@@ -6546,7 +6470,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -893,14 +920,12 @@
+@@ -816,14 +920,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 1 <: usize)
@@ -6564,7 +6488,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -908,14 +933,12 @@
+@@ -831,14 +933,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 2 <: usize)
@@ -6582,7 +6506,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -923,14 +946,12 @@
+@@ -846,14 +946,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 3 <: usize)
@@ -6600,7 +6524,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -938,14 +959,12 @@
+@@ -861,14 +959,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 4 <: usize)
@@ -6618,7 +6542,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -953,14 +972,12 @@
+@@ -876,14 +972,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 5 <: usize)
@@ -6636,7 +6560,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -968,14 +985,12 @@
+@@ -891,14 +985,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 6 <: usize)
@@ -6654,7 +6578,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -983,35 +998,33 @@
+@@ -906,35 +998,33 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 7 <: usize)
@@ -6705,7 +6629,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1024,9 +1037,9 @@
+@@ -947,9 +1037,9 @@
                    i32)
              }
              <:
@@ -6717,7 +6641,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1039,33 +1052,32 @@
+@@ -962,33 +1052,32 @@
                    i32)
              }
              <:
@@ -6768,7 +6692,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
            let
            coefficient1,
            coefficient2,
-@@ -1074,10 +1086,25 @@
+@@ -997,10 +1086,25 @@
            coefficient5,
            coefficient6,
            coefficient7,
@@ -6796,7 +6720,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1085,14 +1112,12 @@
+@@ -1008,14 +1112,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  (sz 8 *! i <: usize)
@@ -6814,7 +6738,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1100,14 +1125,12 @@
+@@ -1023,14 +1125,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 1 <: usize)
@@ -6832,7 +6756,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1115,14 +1138,12 @@
+@@ -1038,14 +1138,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 2 <: usize)
@@ -6850,7 +6774,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1130,14 +1151,12 @@
+@@ -1053,14 +1151,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 3 <: usize)
@@ -6868,7 +6792,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1145,14 +1164,12 @@
+@@ -1068,14 +1164,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 4 <: usize)
@@ -6886,7 +6810,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1160,14 +1177,12 @@
+@@ -1083,14 +1177,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 5 <: usize)
@@ -6904,7 +6828,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1175,14 +1190,12 @@
+@@ -1098,14 +1190,12 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 6 <: usize)
@@ -6922,7 +6846,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1190,33 +1203,27 @@
+@@ -1113,33 +1203,27 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 8 *! i <: usize) +! sz 7 <: usize)
@@ -6966,7 +6890,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
            let i, byte:(usize & u8) = temp_1_ in
            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                      Core.Ops.Range.f_start = sz 0;
-@@ -1228,10 +1235,11 @@
+@@ -1151,10 +1235,11 @@
                Core.Ops.Range.t_Range usize)
              re
              (fun re j ->
@@ -6980,7 +6904,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
                    {
                      re with
                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1245,19 +1253,20 @@
+@@ -1168,19 +1253,20 @@
                          i32)
                    }
                    <:
@@ -7007,7 +6931,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
    match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with
    | 10ul -> deserialize_then_decompress_10_ serialized
    | 11ul -> deserialize_then_decompress_11_ serialized
-@@ -1267,11 +1276,11 @@
+@@ -1190,11 +1276,11 @@
          <:
          Rust_primitives.Hax.t_Never)
  
@@ -7023,7 +6947,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
    match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with
    | 4ul -> deserialize_then_decompress_4_ serialized
    | 5ul -> deserialize_then_decompress_5_ serialized
-@@ -1280,27 +1289,32 @@
+@@ -1203,28 +1289,32 @@
  
          <:
          Rust_primitives.Hax.t_Never)
@@ -7031,7 +6955,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
 +  admit(); //P-F
 +  res
  
--let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) =
+-let deserialize_to_reduced_ring_element (ring_element: t_Slice u8) =
 +#push-options "--z3rlimit 220"
 +let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) = 
    let _:Prims.unit = () <: Prims.unit in
@@ -7042,7 +6966,8 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
    in
 -  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
 -    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
--              (Core.Slice.impl__chunks_exact serialized (sz 3) <: Core.Slice.Iter.t_ChunksExact u8)
+-              (Core.Slice.impl__chunks_exact ring_element (sz 3) <: Core.Slice.Iter.t_ChunksExact u8
+-              )
 -            <:
 -            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
 -        <:
@@ -7072,7 +6997,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1308,12 +1322,12 @@
+@@ -1232,186 +1322,102 @@
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  (sz 2 *! i <: usize)
@@ -7083,14 +7008,30 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
 -            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 +            Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement
            in
+-          let tmp:i32 =
+-            (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ sz 2 *! i <: usize ] <: i32) %! 3329l
+-          in
 -          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
 +          let re:Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement =
              {
                re with
                Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-@@ -1321,58 +1335,89 @@
+               =
                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
                    .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-                (sz 2 *! i <: usize)
+-                tmp
+-            }
+-            <:
+-            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+-          in
+-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+-            {
+-              re with
+-              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-              =
+-              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+-                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
                  ((sz 2 *! i <: usize) +! sz 1 <: usize)
 -                ((byte3 <<! 4l <: i32) |. ((byte2 >>! 4l <: i32) &. 15l <: i32) <: i32)
 +                coef2
@@ -7099,28 +7040,110 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
 -            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 +            Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement
            in
+-          let tmp:i32 =
+-            (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ (sz 2 *! i <: usize) +! sz 1 <: usize
+-              ]
+-              <:
+-              i32) %!
+-            3329l
+-          in
+-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+-            {
+-              re with
+-              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-              =
+-              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+-                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-                ((sz 2 *! i <: usize) +! sz 1 <: usize)
+-                tmp
+-            }
+-            <:
+-            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+-          in
            re)
    in
    re
 +#pop-options
  
--let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement) =
--  let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.repeat 0uy (sz 384) in
--  let serialized:t_Array u8 (sz 384) =
+-let deserialize_ring_elements_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8) =
+-  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+-    Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
+-  in
+-  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
 -    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
--              (Core.Slice.impl__chunks_exact (Rust_primitives.unsize re
--                        .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
--                    <:
--                    t_Slice i32)
--                  (sz 2)
+-              (Core.Slice.impl__chunks_exact public_key
+-                  Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT
 -                <:
--                Core.Slice.Iter.t_ChunksExact i32)
+-                Core.Slice.Iter.t_ChunksExact u8)
 -            <:
--            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact i32))
+-            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
 -        <:
--        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact i32))
+-        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+-      deserialized_pk
+-      (fun deserialized_pk temp_1_ ->
+-          let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+-            deserialized_pk
+-          in
+-          let i, ring_element:(usize & t_Slice u8) = temp_1_ in
+-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize deserialized_pk
+-            i
+-            (deserialize_to_reduced_ring_element ring_element
+-              <:
+-              Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement)
+-          <:
+-          t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
+-  in
+-  deserialized_pk
 +module A = Libcrux.Kem.Kyber.Arithmetic
-+
+ 
+-let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) =
+-  let _:Prims.unit = () <: Prims.unit in
+-  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+-    Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO
+-  in
+-  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+-              (Core.Slice.impl__chunks_exact serialized (sz 3) <: Core.Slice.Iter.t_ChunksExact u8)
+-            <:
+-            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+-        <:
+-        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+-      re
+-      (fun re temp_1_ ->
+-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement = re in
+-          let i, bytes:(usize & t_Slice u8) = temp_1_ in
+-          let byte1:i32 = cast (bytes.[ sz 0 ] <: u8) <: i32 in
+-          let byte2:i32 = cast (bytes.[ sz 1 ] <: u8) <: i32 in
+-          let byte3:i32 = cast (bytes.[ sz 2 ] <: u8) <: i32 in
+-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+-            {
+-              re with
+-              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-              =
+-              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+-                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-                (sz 2 *! i <: usize)
+-                (((byte2 &. 15l <: i32) <<! 8l <: i32) |. (byte1 &. 255l <: i32) <: i32)
+-            }
+-            <:
+-            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+-          in
+-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+-            {
+-              re with
+-              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-              =
+-              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+-                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-                ((sz 2 *! i <: usize) +! sz 1 <: usize)
+-                ((byte3 <<! 4l <: i32) |. ((byte2 >>! 4l <: i32) &. 15l <: i32) <: i32)
+-            }
+-            <:
+-            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+-          in
+-          re)
+-  in
+-  re
 +[@@"opaque_to_smt"]
 +let update3 #n (s: t_Array 't n) (offset: usize {v offset + 3 <= v n}) (i0 i1 i2: 't)
 +  : s': t_Array 't n { Seq.index s' (v offset +  0) == i0
@@ -7131,7 +7154,22 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fst extraction-edited/Libcrux.K
 +    let s = update_at_usize s  offset           i0 in
 +    let s = update_at_usize s (offset +! sz  1) i1 in
 +    update_at_usize s (offset +! sz  2) i2
-+
+ 
+-let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement) =
+-  let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.repeat 0uy (sz 384) in
+-  let serialized:t_Array u8 (sz 384) =
+-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+-              (Core.Slice.impl__chunks_exact (Rust_primitives.unsize re
+-                        .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+-                    <:
+-                    t_Slice i32)
+-                  (sz 2)
+-                <:
+-                Core.Slice.Iter.t_ChunksExact i32)
+-            <:
+-            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact i32))
+-        <:
+-        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact i32))
 +let slice_map_lemma #t #u #n (f: t -> u) (arr: t_Array t n)
 +  (start: nat) (len: nat {start + len <= v n})
 +  : Lemma (  Seq.slice (Spec.Kyber.map' f arr) start (start + len)
@@ -7224,9 +7262,9 @@ 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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-03-18 20:11:28
-@@ -2,123 +2,188 @@
+--- extraction/Libcrux.Kem.Kyber.Serialize.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-03-18 20:52:52
+@@ -2,128 +2,188 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
  open FStar.Mul
@@ -7392,28 +7430,28 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux.
 -      (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement)
 -    : Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True)
 -
--val deserialize_ring_elementes_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8)
--    : Prims.Pure (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
+-val deserialize_then_decompress_10_ (serialized: t_Slice u8)
+-    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 +val deserialize_then_decompress_10_ (serialized: t_Slice u8 {Seq.length serialized == 320})
 +    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement
        Prims.l_True
        (fun _ -> Prims.l_True)
  
--val deserialize_then_decompress_10_ (serialized: t_Slice u8)
+-val deserialize_then_decompress_11_ (serialized: t_Slice u8)
 -    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 +val deserialize_then_decompress_11_ (serialized: t_Slice u8 {Seq.length serialized == 352})
 +    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement
        Prims.l_True
        (fun _ -> Prims.l_True)
  
--val deserialize_then_decompress_11_ (serialized: t_Slice u8)
+-val deserialize_then_decompress_4_ (serialized: t_Slice u8)
 -    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 +val deserialize_then_decompress_4_ (serialized: t_Slice u8 {Seq.length serialized == 128})
 +    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement
        Prims.l_True
        (fun _ -> Prims.l_True)
  
--val deserialize_then_decompress_4_ (serialized: t_Slice u8)
+-val deserialize_then_decompress_5_ (serialized: t_Slice u8)
 -    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 +val deserialize_then_decompress_5_ 
 +  (serialized: t_Slice u8 {Seq.length serialized == 160})
@@ -7421,11 +7459,6 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux.
        Prims.l_True
        (fun _ -> Prims.l_True)
  
--val deserialize_then_decompress_5_ (serialized: t_Slice u8)
--    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
--      Prims.l_True
--      (fun _ -> Prims.l_True)
--
  val deserialize_then_decompress_message (serialized: t_Array u8 (sz 32))
 -    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 -      Prims.l_True
@@ -7466,6 +7499,16 @@ diff -ruN extraction/Libcrux.Kem.Kyber.Serialize.fsti extraction-edited/Libcrux.
 +      (ensures fun res -> Libcrux.Kem.Kyber.Arithmetic.to_spec_poly_b res
 +                    == Spec.Kyber.decode_then_decompress_v p serialized)
  
+-val deserialize_to_reduced_ring_element (ring_element: t_Slice u8)
+-    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+-      Prims.l_True
+-      (fun _ -> Prims.l_True)
+-
+-val deserialize_ring_elements_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8)
+-    : Prims.Pure (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
+-      Prims.l_True
+-      (fun _ -> Prims.l_True)
+-
  val deserialize_to_uncompressed_ring_element (serialized: t_Slice u8)
 -    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
 -      Prims.l_True
@@ -7484,8 +7527,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.Types.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-03-18 20:52:52
 @@ -40,13 +40,41 @@
      f_from = fun (value: t_MlKemCiphertext v_SIZE) -> value.f_value
    }
@@ -7672,8 +7715,8 @@ 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) = {
    f_sk:t_MlKemPrivateKey v_PRIVATE_KEY_SIZE;
 diff -ruN extraction/Libcrux.Kem.Kyber.fst extraction-edited/Libcrux.Kem.Kyber.fst
---- extraction/Libcrux.Kem.Kyber.fst	2024-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.fst	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.fst	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.fst	2024-03-18 20:52:52
 @@ -1,12 +1,29 @@
  module Libcrux.Kem.Kyber
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -7887,7 +7930,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.fst extraction-edited/Libcrux.Kem.Kyber.f
        (public_key: t_Array u8 v_PUBLIC_KEY_SIZE)
       =
 -  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
--    Libcrux.Kem.Kyber.Serialize.deserialize_ring_elementes_reduced v_PUBLIC_KEY_SIZE
+-    Libcrux.Kem.Kyber.Serialize.deserialize_ring_elements_reduced v_PUBLIC_KEY_SIZE
 -      v_K
 +  let pk:t_Array Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement v_K =
 +    Libcrux.Kem.Kyber.Ind_cpa.deserialize_public_key #p v_K
@@ -7948,8 +7991,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-03-18 20:11:27
-+++ extraction-edited/Libcrux.Kem.Kyber.fsti	2024-03-18 20:11:28
+--- extraction/Libcrux.Kem.Kyber.fsti	2024-03-18 20:52:52
++++ extraction-edited/Libcrux.Kem.Kyber.fsti	2024-03-18 20:52:52
 @@ -10,36 +10,84 @@
    Libcrux.Kem.Kyber.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE +!
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE
@@ -8051,7 +8094,7 @@ diff -ruN extraction/Libcrux.Kem.Kyber.fsti extraction-edited/Libcrux.Kem.Kyber.
 +                (kp.f_sk.f_value,kp.f_pk.f_value) == Spec.Kyber.ind_cca_generate_keypair p randomness))
 diff -ruN extraction/Libcrux.Kem.fst extraction-edited/Libcrux.Kem.fst
 --- extraction/Libcrux.Kem.fst	1970-01-01 01:00:00
-+++ extraction-edited/Libcrux.Kem.fst	2024-03-18 20:11:28
++++ extraction-edited/Libcrux.Kem.fst	2024-03-18 20:52:52
 @@ -0,0 +1,6 @@
 +module Libcrux.Kem
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -8061,7 +8104,7 @@ diff -ruN extraction/Libcrux.Kem.fst extraction-edited/Libcrux.Kem.fst
 +
 diff -ruN extraction/Libcrux_platform.Platform.fsti extraction-edited/Libcrux_platform.Platform.fsti
 --- extraction/Libcrux_platform.Platform.fsti	1970-01-01 01:00:00
-+++ extraction-edited/Libcrux_platform.Platform.fsti	2024-03-18 20:11:28
++++ extraction-edited/Libcrux_platform.Platform.fsti	2024-03-18 20:52:52
 @@ -0,0 +1,20 @@
 +module Libcrux_platform.Platform
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -8085,7 +8128,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
-+++ extraction-edited/MkSeq.fst	2024-03-18 20:11:28
++++ extraction-edited/MkSeq.fst	2024-03-18 20:52:52
 @@ -0,0 +1,91 @@
 +module MkSeq
 +open Core
@@ -8180,7 +8223,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
-+++ extraction-edited/Spec.Kyber.fst	2024-03-18 20:11:28
++++ extraction-edited/Spec.Kyber.fst	2024-03-18 20:52:52
 @@ -0,0 +1,435 @@
 +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 c44e02ae0..7f9dce2fa 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-03-18 20:11:28
+--- extraction-edited/BitVecEq.fst	2024-03-18 20:52:52
 +++ extraction-secret-independent/BitVecEq.fst	1970-01-01 01:00:00
 @@ -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-03-18 20:11:28
+--- extraction-edited/BitVecEq.fsti	2024-03-18 20:52:52
 +++ extraction-secret-independent/BitVecEq.fsti	1970-01-01 01:00:00
 @@ -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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Digest.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Digest.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Digest.fsti	2024-03-18 20:52:52
 @@ -1,31 +1,41 @@
  module Libcrux.Digest
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -379,8 +379,8 @@ diff -ruN extraction-edited/Libcrux.Digest.fsti extraction-secret-independent/Li
 -      (fun _ -> Prims.l_True)
 +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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fst	2024-03-18 20:52:52
 @@ -1,364 +1,81 @@
  module Libcrux.Kem.Kyber.Arithmetic
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -785,8 +785,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Arithmetic.fsti	2024-03-18 20:52:52
 @@ -3,32 +3,10 @@
  open Core
  open FStar.Mul
@@ -1140,8 +1140,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fst	2024-03-18 20:52:52
 @@ -1,79 +1,39 @@
  module Libcrux.Kem.Kyber.Compress
 -#set-options "--fuel 0 --ifuel 0 --z3rlimit 200"
@@ -1246,8 +1246,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Compress.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Compress.fsti	2024-03-18 20:52:52
 @@ -3,42 +3,44 @@
  open Core
  open FStar.Mul
@@ -1319,8 +1319,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fst	2024-03-18 20:52:52
 @@ -4,163 +4,61 @@
  open FStar.Mul
  
@@ -1509,8 +1509,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Constant_time_ops.fsti	2024-03-18 20:52:52
 @@ -20,26 +20,30 @@
  
  val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8)
@@ -1554,7 +1554,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
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst	2024-03-18 20:11:28
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Conversions.fst	2024-03-18 20:52:52
 @@ -0,0 +1,87 @@
 +module Libcrux.Kem.Kyber.Conversions
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -1645,8 +1645,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
 \ No newline at end of file
 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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fst	2024-03-18 20:52:52
 @@ -3,28 +3,18 @@
  open Core
  open FStar.Mul
@@ -1714,8 +1714,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Hash_functions.fsti	2024-03-18 20:52:52
 @@ -3,17 +3,12 @@
  open Core
  open FStar.Mul
@@ -1742,7 +1742,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
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst	2024-03-18 20:11:28
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Helper.fst	2024-03-18 20:52:52
 @@ -0,0 +1,6 @@
 +module Libcrux.Kem.Kyber.Helper
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -1751,8 +1751,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fst	2024-03-18 20:52:52
 @@ -1,5 +1,5 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -2460,8 +2460,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ind_cpa.fsti	2024-03-18 20:52:52
 @@ -1,151 +1,80 @@
  module Libcrux.Kem.Kyber.Ind_cpa
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -2662,8 +2662,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fst	2024-03-18 20:52:52
 @@ -3,37 +3,22 @@
  open Core
  open FStar.Mul
@@ -2712,8 +2712,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber1024.fsti	2024-03-18 20:52:52
 @@ -63,32 +63,27 @@
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_1024_
  
@@ -2759,8 +2759,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fst	2024-03-18 20:52:52
 @@ -3,37 +3,22 @@
  open Core
  open FStar.Mul
@@ -2809,8 +2809,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber512.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber512.fsti	2024-03-18 20:52:52
 @@ -63,32 +63,27 @@
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_512_
  
@@ -2856,8 +2856,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fst	2024-03-18 20:52:52
 @@ -3,37 +3,22 @@
  open Core
  open FStar.Mul
@@ -2906,8 +2906,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Kyber768.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Kyber768.fsti	2024-03-18 20:52:52
 @@ -63,33 +63,27 @@
    Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE +! v_CPA_PKE_CIPHERTEXT_SIZE_768_
  
@@ -2956,8 +2956,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Matrix.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fst	2024-03-18 20:52:52
 @@ -3,418 +3,432 @@
  open Core
  open FStar.Mul
@@ -3761,8 +3761,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Matrix.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Matrix.fsti	2024-03-18 20:52:52
 @@ -3,71 +3,39 @@
  open Core
  open FStar.Mul
@@ -3864,8 +3864,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Ntt.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fst	2024-03-18 20:52:52
 @@ -1,130 +1,56 @@
  module Libcrux.Kem.Kyber.Ntt
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -4795,8 +4795,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Ntt.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Ntt.fsti	2024-03-18 20:52:52
 @@ -2,80 +2,224 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -5086,8 +5086,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Sampling.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fst	2024-03-18 20:52:52
 @@ -3,34 +3,27 @@
  open Core
  open FStar.Mul
@@ -5524,8 +5524,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Sampling.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Sampling.fsti	2024-03-18 20:52:52
 @@ -3,37 +3,77 @@
  open Core
  open FStar.Mul
@@ -5626,8 +5626,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Serialize.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fst	2024-03-18 20:52:52
 @@ -1,15 +1,8 @@
  module Libcrux.Kem.Kyber.Serialize
 -#set-options "--fuel 0 --ifuel 0 --z3rlimit 50 --retry 3"
@@ -7110,8 +7110,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Serialize.fsti	2024-03-18 20:52:52
 @@ -2,188 +2,118 @@
  #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
  open Core
@@ -7365,8 +7365,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.Types.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.Types.fst	2024-03-18 20:52:52
 @@ -3,275 +3,193 @@
  open Core
  open FStar.Mul
@@ -7710,8 +7710,8 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.Types.fst extraction-secret-indepe
 +      (self: t_KyberKeyPair v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE)
      : t_Array u8 v_PRIVATE_KEY_SIZE = impl_12__as_slice v_PRIVATE_KEY_SIZE self.f_sk
 diff -ruN extraction-edited/Libcrux.Kem.Kyber.fst extraction-secret-independent/Libcrux.Kem.Kyber.fst
---- extraction-edited/Libcrux.Kem.Kyber.fst	2024-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.fst	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.fst	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.fst	2024-03-18 20:52:52
 @@ -1,29 +1,12 @@
  module Libcrux.Kem.Kyber
 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
@@ -7990,8 +7990,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-03-18 20:11:28
-+++ extraction-secret-independent/Libcrux.Kem.Kyber.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux.Kem.Kyber.fsti	2024-03-18 20:52:52
++++ extraction-secret-independent/Libcrux.Kem.Kyber.fsti	2024-03-18 20:52:52
 @@ -4,90 +4,37 @@
  open FStar.Mul
  
@@ -8100,7 +8100,7 @@ diff -ruN extraction-edited/Libcrux.Kem.Kyber.fsti extraction-secret-independent
 +      Prims.l_True
 +      (fun _ -> Prims.l_True)
 diff -ruN extraction-edited/Libcrux_platform.Platform.fsti extraction-secret-independent/Libcrux_platform.Platform.fsti
---- extraction-edited/Libcrux_platform.Platform.fsti	2024-03-18 20:11:28
+--- extraction-edited/Libcrux_platform.Platform.fsti	2024-03-18 20:52:52
 +++ extraction-secret-independent/Libcrux_platform.Platform.fsti	1970-01-01 01:00:00
 @@ -1,20 +0,0 @@
 -module Libcrux_platform.Platform
@@ -8125,14 +8125,14 @@ 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/Libcrux_platform.fsti extraction-secret-independent/Libcrux_platform.fsti
 --- extraction-edited/Libcrux_platform.fsti	1970-01-01 01:00:00
-+++ extraction-secret-independent/Libcrux_platform.fsti	2024-03-18 20:11:28
++++ extraction-secret-independent/Libcrux_platform.fsti	2024-03-18 20:52:52
 @@ -0,0 +1,4 @@
 +module Libcrux_platform
 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 +
 +val simd256_support : unit -> bool
 diff -ruN extraction-edited/MkSeq.fst extraction-secret-independent/MkSeq.fst
---- extraction-edited/MkSeq.fst	2024-03-18 20:11:28
+--- extraction-edited/MkSeq.fst	2024-03-18 20:52:52
 +++ extraction-secret-independent/MkSeq.fst	1970-01-01 01:00:00
 @@ -1,91 +0,0 @@
 -module MkSeq
@@ -8227,7 +8227,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-03-18 20:11:28
+--- extraction-edited/Spec.Kyber.fst	2024-03-18 20:52:52
 +++ extraction-secret-independent/Spec.Kyber.fst	1970-01-01 01:00:00
 @@ -1,435 +0,0 @@
 -module Spec.Kyber
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst
index 8602ce977..351b4d86f 100644
--- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst
+++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst
@@ -666,83 +666,6 @@ let compress_then_serialize_ring_element_v
         <:
         Rust_primitives.Hax.t_Never)
 
-let deserialize_ring_elementes_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8) =
-  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
-    Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
-  in
-  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-              (Core.Slice.impl__chunks_exact public_key
-                  Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT
-                <:
-                Core.Slice.Iter.t_ChunksExact u8)
-            <:
-            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
-        <:
-        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
-      deserialized_pk
-      (fun deserialized_pk temp_1_ ->
-          let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
-            deserialized_pk
-          in
-          let i, ring_element:(usize & t_Slice u8) = temp_1_ in
-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
-            Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO
-          in
-          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
-            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-                      (Core.Slice.impl__chunks_exact ring_element (sz 3)
-                        <:
-                        Core.Slice.Iter.t_ChunksExact u8)
-                    <:
-                    Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
-                <:
-                Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
-              re
-              (fun re temp_1_ ->
-                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement = re in
-                  let i, bytes:(usize & t_Slice u8) = temp_1_ in
-                  let byte1:i32 = cast (bytes.[ sz 0 ] <: u8) <: i32 in
-                  let byte2:i32 = cast (bytes.[ sz 1 ] <: u8) <: i32 in
-                  let byte3:i32 = cast (bytes.[ sz 2 ] <: u8) <: i32 in
-                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
-                    {
-                      re with
-                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-                      =
-                      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-                          .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-                        (sz 2 *! i <: usize)
-                        ((((byte2 &. 15l <: i32) <<! 8l <: i32) |. (byte1 &. 255l <: i32) <: i32) %!
-                          Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
-                          <:
-                          i32)
-                    }
-                    <:
-                    Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
-                  in
-                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
-                    {
-                      re with
-                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-                      =
-                      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
-                          .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
-                        ((sz 2 *! i <: usize) +! sz 1 <: usize)
-                        (((byte3 <<! 4l <: i32) |. ((byte2 >>! 4l <: i32) &. 15l <: i32) <: i32) %!
-                          Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
-                          <:
-                          i32)
-                    }
-                    <:
-                    Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
-                  in
-                  re)
-          in
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize deserialized_pk i re)
-  in
-  deserialized_pk
-
 let deserialize_then_decompress_10_ (serialized: t_Slice u8) =
   let _:Prims.unit = () <: Prims.unit in
   let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
@@ -1281,6 +1204,122 @@ let deserialize_then_decompress_ring_element_v
         <:
         Rust_primitives.Hax.t_Never)
 
+let deserialize_to_reduced_ring_element (ring_element: t_Slice u8) =
+  let _:Prims.unit = () <: Prims.unit in
+  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+    Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO
+  in
+  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+              (Core.Slice.impl__chunks_exact ring_element (sz 3) <: Core.Slice.Iter.t_ChunksExact u8
+              )
+            <:
+            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+        <:
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+      re
+      (fun re temp_1_ ->
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement = re in
+          let i, bytes:(usize & t_Slice u8) = temp_1_ in
+          let byte1:i32 = cast (bytes.[ sz 0 ] <: u8) <: i32 in
+          let byte2:i32 = cast (bytes.[ sz 1 ] <: u8) <: i32 in
+          let byte3:i32 = cast (bytes.[ sz 2 ] <: u8) <: i32 in
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+            {
+              re with
+              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+              =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                (sz 2 *! i <: usize)
+                (((byte2 &. 15l <: i32) <<! 8l <: i32) |. (byte1 &. 255l <: i32) <: i32)
+            }
+            <:
+            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+          in
+          let tmp:i32 =
+            (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ sz 2 *! i <: usize ] <: i32) %! 3329l
+          in
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+            {
+              re with
+              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+              =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                (sz 2 *! i <: usize)
+                tmp
+            }
+            <:
+            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+          in
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+            {
+              re with
+              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+              =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                ((sz 2 *! i <: usize) +! sz 1 <: usize)
+                ((byte3 <<! 4l <: i32) |. ((byte2 >>! 4l <: i32) &. 15l <: i32) <: i32)
+            }
+            <:
+            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+          in
+          let tmp:i32 =
+            (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ (sz 2 *! i <: usize) +! sz 1 <: usize
+              ]
+              <:
+              i32) %!
+            3329l
+          in
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+            {
+              re with
+              Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+              =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+                  .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                ((sz 2 *! i <: usize) +! sz 1 <: usize)
+                tmp
+            }
+            <:
+            Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+          in
+          re)
+  in
+  re
+
+let deserialize_ring_elements_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8) =
+  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+    Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
+  in
+  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+              (Core.Slice.impl__chunks_exact public_key
+                  Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT
+                <:
+                Core.Slice.Iter.t_ChunksExact u8)
+            <:
+            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+        <:
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+      deserialized_pk
+      (fun deserialized_pk temp_1_ ->
+          let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+            deserialized_pk
+          in
+          let i, ring_element:(usize & t_Slice u8) = temp_1_ in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize deserialized_pk
+            i
+            (deserialize_to_reduced_ring_element ring_element
+              <:
+              Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement)
+          <:
+          t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
+  in
+  deserialized_pk
+
 let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) =
   let _:Prims.unit = () <: Prims.unit in
   let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fsti b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fsti
index 331f45875..9bcfb25a8 100644
--- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fsti
+++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fsti
@@ -71,11 +71,6 @@ val compress_then_serialize_ring_element_v
       (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement)
     : Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True)
 
-val deserialize_ring_elementes_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8)
-    : Prims.Pure (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
-
 val deserialize_then_decompress_10_ (serialized: t_Slice u8)
     : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
       Prims.l_True
@@ -115,6 +110,16 @@ val deserialize_then_decompress_ring_element_v
       Prims.l_True
       (fun _ -> Prims.l_True)
 
+val deserialize_to_reduced_ring_element (ring_element: t_Slice u8)
+    : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
+val deserialize_ring_elements_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8)
+    : Prims.Pure (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
 val deserialize_to_uncompressed_ring_element (serialized: t_Slice u8)
     : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
       Prims.l_True
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst
index ecc4dcbfa..4b64aafc3 100644
--- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst
+++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst
@@ -265,7 +265,7 @@ let validate_public_key
       (public_key: t_Array u8 v_PUBLIC_KEY_SIZE)
      =
   let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
-    Libcrux.Kem.Kyber.Serialize.deserialize_ring_elementes_reduced v_PUBLIC_KEY_SIZE
+    Libcrux.Kem.Kyber.Serialize.deserialize_ring_elements_reduced v_PUBLIC_KEY_SIZE
       v_K
       (public_key.[ { Core.Ops.Range.f_end = v_RANKED_BYTES_PER_RING_ELEMENT }
           <:
diff --git a/src/kem/kyber.rs b/src/kem/kyber.rs
index c8a8b67c7..7999e1593 100644
--- a/src/kem/kyber.rs
+++ b/src/kem/kyber.rs
@@ -40,7 +40,7 @@ use self::{
     constants::{CPA_PKE_KEY_GENERATION_SEED_SIZE, H_DIGEST_SIZE, SHARED_SECRET_SIZE},
     hash_functions::{G, H, PRF},
     ind_cpa::{into_padded_array, serialize_public_key},
-    serialize::deserialize_ring_elementes_reduced,
+    serialize::deserialize_ring_elements_reduced,
 };
 
 /// Seed size for key generation
@@ -74,7 +74,7 @@ pub(super) fn validate_public_key<
 >(
     public_key: &[u8; PUBLIC_KEY_SIZE],
 ) -> bool {
-    let deserialized_pk = deserialize_ring_elementes_reduced::<PUBLIC_KEY_SIZE, K>(
+    let deserialized_pk = deserialize_ring_elements_reduced::<PUBLIC_KEY_SIZE, K>(
         &public_key[..RANKED_BYTES_PER_RING_ELEMENT],
     );
 
diff --git a/src/kem/kyber/serialize.rs b/src/kem/kyber/serialize.rs
index 802b76fd0..50106c2fe 100644
--- a/src/kem/kyber/serialize.rs
+++ b/src/kem/kyber/serialize.rs
@@ -6,8 +6,8 @@ use super::{
     },
     constants::{BYTES_PER_RING_ELEMENT, SHARED_SECRET_SIZE},
 };
+use crate::cloop;
 use crate::hax_utils::hax_debug_assert;
-use crate::{cloop, kem::kyber::constants::FIELD_MODULUS};
 
 #[cfg(not(hax))]
 use super::constants::COEFFICIENTS_IN_RING_ELEMENT;
@@ -101,12 +101,39 @@ pub(super) fn deserialize_to_uncompressed_ring_element(serialized: &[u8]) -> Pol
     re
 }
 
+#[inline(always)]
+fn deserialize_to_reduced_ring_element(ring_element: &[u8]) -> PolynomialRingElement {
+    hax_debug_assert!(ring_element.len() == BYTES_PER_RING_ELEMENT);
+
+    let mut re = PolynomialRingElement::ZERO;
+
+    cloop! {
+        for (i, bytes) in ring_element.chunks_exact(3).enumerate() {
+            let byte1 = bytes[0] as FieldElement;
+            let byte2 = bytes[1] as FieldElement;
+            let byte3 = bytes[2] as FieldElement;
+
+            // The modulus here is ok because the input must be public.
+            // XXX: The awkward code here is necessary to work around Charon shortcomings.
+            re.coefficients[2 * i] = (byte2 & 0x0F) << 8 | (byte1 & 0xFF);
+            let tmp = re.coefficients[2 * i] % 3329; // FIELD_MODULUS
+            re.coefficients[2 * i] = tmp;
+
+            re.coefficients[2 * i + 1] = (byte3 << 4) | ((byte2 >> 4) & 0x0F);
+            let tmp = re.coefficients[2 * i + 1] % 3329; // FIELD_MODULUS
+            re.coefficients[2 * i + 1] = tmp;
+        }
+    }
+
+    re
+}
+
 /// This function deserializes ring elements and reduces the result by the field
 /// modulus.
 ///
 /// This function MUST NOT be used on secret inputs.
 #[inline(always)]
-pub(super) fn deserialize_ring_elementes_reduced<const PUBLIC_KEY_SIZE: usize, const K: usize>(
+pub(super) fn deserialize_ring_elements_reduced<const PUBLIC_KEY_SIZE: usize, const K: usize>(
     public_key: &[u8],
 ) -> [PolynomialRingElement; K] {
     let mut deserialized_pk = [PolynomialRingElement::ZERO; K];
@@ -115,22 +142,7 @@ pub(super) fn deserialize_ring_elementes_reduced<const PUBLIC_KEY_SIZE: usize, c
             .chunks_exact(BYTES_PER_RING_ELEMENT)
             .enumerate()
         {
-            deserialized_pk[i] = {
-                let mut re = PolynomialRingElement::ZERO;
-                cloop! {
-                    for (i, bytes) in ring_element.chunks_exact(3).enumerate() {
-                        let byte1 = bytes[0] as FieldElement;
-                        let byte2 = bytes[1] as FieldElement;
-                        let byte3 = bytes[2] as FieldElement;
-
-                        // The modulus here is ok because the input must be public.
-                        re.coefficients[2 * i] = ((byte2 & 0x0F) << 8 | (byte1 & 0xFF)) % FIELD_MODULUS;
-                        re.coefficients[2 * i + 1] = ((byte3 << 4) | ((byte2 >> 4) & 0x0F)) % FIELD_MODULUS;
-                    }
-                }
-
-                re
-            }
+            deserialized_pk[i] =deserialize_to_reduced_ring_element(ring_element);
         }
     }
     deserialized_pk