diff --git a/git-hooks/pre-commit.py b/git-hooks/pre-commit.py
index d064a0bbf..141ba3719 100755
--- a/git-hooks/pre-commit.py
+++ b/git-hooks/pre-commit.py
@@ -26,10 +26,10 @@ def shell(command, expect=0, cwd=None):
     elif path.suffix == ".rs":
         format_rust_files = True
         if "kyber" in path.parts:
-            if "src" in path.parts:
-                update_libcrux_kyber_fstar_extraction = True
-            if "specs" in path.parts and "src" in path.parts:
+            if "specs" in path.parts and "kyber" in path.parts:
                 update_spec_kyber_fstar_extraction = True
+            if "src" in path.parts and "kem" in path.parts:
+                update_libcrux_kyber_fstar_extraction = True
 
 if format_python_files == True:
     shell(["black", "."])
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Compress.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Compress.fst
index 9ebd0344e..bd0da33fb 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Compress.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Compress.fst
@@ -11,13 +11,13 @@ let compress
       (sz 256) =
   Hacspec_lib.Ring.impl_2__new (Core.Array.impl_23__map (Hacspec_lib.Ring.impl_2__coefficients re
           <:
-          array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+          t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
         (fun coefficient ->
             compress_d coefficient bits_per_compressed_coefficient
             <:
             Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       <:
-      array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+      t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
 
 let decompress
       (re:
@@ -28,13 +28,13 @@ let decompress
       (sz 256) =
   Hacspec_lib.Ring.impl_2__new (Core.Array.impl_23__map (Hacspec_lib.Ring.impl_2__coefficients re
           <:
-          array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+          t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
         (fun coefficient ->
             decompress_d coefficient bits_per_compressed_coefficient
             <:
             Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       <:
-      array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+      t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
 
 let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size: usize)
     : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
@@ -47,10 +47,10 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
           Rust_primitives.Hax.t_Never)
   in
   let two_pow_bit_size:u32 =
-    Core.Num.impl_8__pow 2ul
+    Core.Num.impl__u32__pow 2ul
       (Core.Result.impl__unwrap_or_else (Core.Convert.f_try_into to_bit_size
             <:
-            Core.Result.t_Result u32 (Core.Convert.impl_6 usize u32).f_Error)
+            Core.Result.t_Result u32 Core.Num.Error.t_TryFromIntError)
           (fun _ ->
               Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize
                             (let list =
@@ -62,7 +62,7 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
                               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
                               Rust_primitives.Hax.array_of_list list)
                           <:
-                          slice string)
+                          t_Slice string)
                         (Rust_primitives.unsize (let list =
                                 [
                                   Core.Fmt.Rt.impl_1__new_display Hacspec_kyber.Parameters.v_BITS_PER_COEFFICIENT
@@ -74,7 +74,7 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
                               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
                               Rust_primitives.Hax.array_of_list list)
                           <:
-                          slice Core.Fmt.Rt.t_Argument)
+                          t_Slice Core.Fmt.Rt.t_Argument)
                       <:
                       Core.Fmt.t_Arguments)
                   <:
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ind_cpa.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ind_cpa.fst
index f21d0788c..ac6ccdb7f 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ind_cpa.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ind_cpa.fst
@@ -3,90 +3,94 @@ module Hacspec_kyber.Ind_cpa
 open Core
 
 type t_KeyPair = {
-  f_sk:array u8 (sz 1152);
-  f_pk:array u8 (sz 1184)
+  f_sk:t_Array u8 (sz 1152);
+  f_pk:t_Array u8 (sz 1184)
 }
 
-let impl__new (sk: array u8 (sz 1152)) (pk: array u8 (sz 1184)) : t_KeyPair =
+let impl__KeyPair__new (sk: t_Array u8 (sz 1152)) (pk: t_Array u8 (sz 1184)) : t_KeyPair =
   { f_sk = sk; f_pk = pk }
 
-let impl__serialize_secret_key (self: t_KeyPair) (implicit_rejection_value: array u8 (sz 32))
-    : array u8 (sz 2400) =
+let impl__KeyPair__serialize_secret_key
+      (self: t_KeyPair)
+      (implicit_rejection_value: t_Array u8 (sz 32))
+    : t_Array u8 (sz 2400) =
   Core.Convert.f_into (Hacspec_lib.f_push (Hacspec_lib.f_push (Hacspec_lib.f_push (Hacspec_lib.f_push
                     (Hacspec_lib.impl_6__new (Rust_primitives.Hax.repeat 0uy (sz 2400)
                           <:
-                          array u8 (sz 2400))
+                          t_Array u8 (sz 2400))
                       <:
                       Hacspec_lib.t_UpdatableArray (sz 2400))
-                    (Rust_primitives.unsize self.f_sk <: slice u8)
+                    (Rust_primitives.unsize self.f_sk <: t_Slice u8)
                   <:
                   Hacspec_lib.t_UpdatableArray (sz 2400))
-                (Rust_primitives.unsize self.f_pk <: slice u8)
+                (Rust_primitives.unsize self.f_pk <: t_Slice u8)
               <:
               Hacspec_lib.t_UpdatableArray (sz 2400))
             (Rust_primitives.unsize (Hacspec_kyber.Parameters.Hash_functions.v_H (Rust_primitives.unsize
                         self.f_pk
                       <:
-                      slice u8)
+                      t_Slice u8)
                   <:
-                  array u8 (sz 32))
+                  t_Array u8 (sz 32))
               <:
-              slice u8)
+              t_Slice u8)
           <:
           Hacspec_lib.t_UpdatableArray (sz 2400))
-        (Rust_primitives.unsize implicit_rejection_value <: slice u8)
+        (Rust_primitives.unsize implicit_rejection_value <: t_Slice u8)
       <:
       Hacspec_lib.t_UpdatableArray (sz 2400))
 
-let impl__pk (self: t_KeyPair) : array u8 (sz 1184) = self.f_pk
+let impl__KeyPair__pk (self: t_KeyPair) : t_Array u8 (sz 1184) = self.f_pk
 
-let generate_keypair (key_generation_seed: array u8 (sz 32))
+let generate_keypair (key_generation_seed: t_Array u8 (sz 32))
     : Core.Result.t_Result t_KeyPair Hacspec_kyber.t_BadRejectionSamplingRandomnessError =
-  let hashed:array u8 (sz 64) =
+  let hashed:t_Array u8 (sz 64) =
     Hacspec_kyber.Parameters.Hash_functions.v_G (Rust_primitives.unsize key_generation_seed
         <:
-        slice u8)
+        t_Slice u8)
   in
-  let seed_for_A, seed_for_secret_and_error:(slice u8 & slice u8) =
-    Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: slice u8) (sz 32)
+  let seed_for_A, seed_for_secret_and_error:(t_Slice u8 & t_Slice u8) =
+    Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: t_Slice u8) (sz 32)
   in
   let (domain_separator: u8):u8 = 0uy in
-  let v_A_as_ntt:array
+  let v_A_as_ntt:t_Array
     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
     (sz 3) =
     Rust_primitives.Hax.repeat Hacspec_lib.Vector.impl__ZERO (sz 3)
   in
-  let (xof_input: array u8 (sz 34)):array u8 (sz 34) = Hacspec_lib.f_into_padded_array seed_for_A in
-  let v_A_as_ntt, xof_input:(array
+  let (xof_input: t_Array u8 (sz 34)):t_Array u8 (sz 34) =
+    Hacspec_lib.f_into_padded_array seed_for_A
+  in
+  let v_A_as_ntt, xof_input:(t_Array
       (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
       (sz 3) &
-    array u8 (sz 34)) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    t_Array u8 (sz 34)) =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_RANK
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (v_A_as_ntt, xof_input)
       (fun (v_A_as_ntt, xof_input) i ->
-          Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                     Core.Ops.Range.f_start = sz 0;
                     Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_RANK
                   })
               <:
-              (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+              Core.Ops.Range.t_Range usize)
             (v_A_as_ntt, xof_input)
             (fun (v_A_as_ntt, xof_input) j ->
-                let xof_input:array u8 (sz 34) =
+                let xof_input:t_Array u8 (sz 34) =
                   Rust_primitives.Hax.update_at xof_input (sz 32) (Hacspec_lib.f_as_u8 i <: u8)
                 in
-                let xof_input:array u8 (sz 34) =
+                let xof_input:t_Array u8 (sz 34) =
                   Rust_primitives.Hax.update_at xof_input (sz 33) (Hacspec_lib.f_as_u8 j <: u8)
                 in
-                let (xof_bytes: array u8 (sz 840)):array u8 (sz 840) =
+                let (xof_bytes: t_Array u8 (sz 840)):t_Array u8 (sz 840) =
                   Hacspec_kyber.Parameters.Hash_functions.v_XOF (Rust_primitives.unsize xof_input
                       <:
-                      slice u8)
+                      t_Slice u8)
                 in
                 let* hoist2:Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
@@ -122,13 +126,13 @@ let generate_keypair (key_generation_seed: array u8 (sz 32))
                       j
                       hoist2
                   in
-                  let hoist4:array
+                  let hoist4:t_Array
                     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         (sz 256)
                         (sz 3)) (sz 3) =
                     Rust_primitives.Hax.update_at v_A_as_ntt i hoist3
                   in
-                  let v_A_as_ntt:array
+                  let v_A_as_ntt:t_Array
                     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         (sz 256)
                         (sz 3)) (sz 3) =
@@ -136,38 +140,38 @@ let generate_keypair (key_generation_seed: array u8 (sz 32))
                   in
                   v_A_as_ntt, xof_input))
           <:
-          (array
+          (t_Array
               (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                   (sz 256)
                   (sz 3)) (sz 3) &
-            array u8 (sz 34)))
+            t_Array u8 (sz 34)))
   in
   let secret:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
     Hacspec_lib.Vector.impl__ZERO
   in
-  let (prf_input: array u8 (sz 33)):array u8 (sz 33) =
+  let (prf_input: t_Array u8 (sz 33)):t_Array u8 (sz 33) =
     Hacspec_lib.f_into_padded_array seed_for_secret_and_error
   in
-  let domain_separator, prf_input, secret:(u8 & array u8 (sz 33) &
+  let domain_separator, prf_input, secret:(u8 & t_Array u8 (sz 33) &
     Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_lib.Vector.impl__len secret <: usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (domain_separator, prf_input, secret)
       (fun (domain_separator, prf_input, secret) i ->
-          let prf_input:array u8 (sz 33) =
+          let prf_input:t_Array u8 (sz 33) =
             Rust_primitives.Hax.update_at prf_input (sz 32) domain_separator
           in
           let domain_separator:u8 = domain_separator +! 1uy in
-          let (prf_output: array u8 (sz 128)):array u8 (sz 128) =
+          let (prf_output: t_Array u8 (sz 128)):t_Array u8 (sz 128) =
             Hacspec_kyber.Parameters.Hash_functions.v_PRF (Rust_primitives.unsize prf_input
                 <:
-                slice u8)
+                t_Slice u8)
           in
           let secret:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
             (sz 256)
@@ -175,7 +179,7 @@ let generate_keypair (key_generation_seed: array u8 (sz 32))
             Rust_primitives.Hax.update_at secret
               i
               (Hacspec_kyber.Sampling.sample_poly_cbd (sz 2)
-                  (prf_output.[ Core.Ops.Range.RangeFull ] <: slice u8)
+                  (prf_output.[ Core.Ops.Range.RangeFull ] <: t_Slice u8)
                 <:
                 Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
@@ -189,23 +193,23 @@ let generate_keypair (key_generation_seed: array u8 (sz 32))
   in
   let domain_separator, error, prf_input:(u8 &
     Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) &
-    array u8 (sz 33)) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    t_Array u8 (sz 33)) =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_lib.Vector.impl__len error <: usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (domain_separator, error, prf_input)
       (fun (domain_separator, error, prf_input) i ->
-          let prf_input:array u8 (sz 33) =
+          let prf_input:t_Array u8 (sz 33) =
             Rust_primitives.Hax.update_at prf_input (sz 32) domain_separator
           in
           let domain_separator:u8 = domain_separator +! 1uy in
-          let (prf_output: array u8 (sz 128)):array u8 (sz 128) =
+          let (prf_output: t_Array u8 (sz 128)):t_Array u8 (sz 128) =
             Hacspec_kyber.Parameters.Hash_functions.v_PRF (Rust_primitives.unsize prf_input
                 <:
-                slice u8)
+                t_Slice u8)
           in
           let error:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
             (sz 256)
@@ -213,7 +217,7 @@ let generate_keypair (key_generation_seed: array u8 (sz 32))
             Rust_primitives.Hax.update_at error
               i
               (Hacspec_kyber.Sampling.sample_poly_cbd (sz 2)
-                  (prf_output.[ Core.Ops.Range.RangeFull ] <: slice u8)
+                  (prf_output.[ Core.Ops.Range.RangeFull ] <: t_Slice u8)
                 <:
                 Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
@@ -230,41 +234,45 @@ let generate_keypair (key_generation_seed: array u8 (sz 32))
     (sz 3) =
     Hacspec_kyber.Ntt.vector_ntt error
   in
-  let tt_as_ntt =
+  let tt_as_ntt:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+    (sz 256)
+    (sz 3) =
     (Hacspec_kyber.Matrix.multiply_matrix_by_column v_A_as_ntt secret_as_ntt
       <:
       Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)) +!
     error_as_ntt
   in
-  let public_key_serialized:array u8 (sz 1184) =
+  let public_key_serialized:t_Array u8 (sz 1184) =
     Hacspec_lib.impl_6__array (Hacspec_lib.f_push (Hacspec_lib.f_push (Hacspec_lib.impl_6__new (Rust_primitives.Hax.repeat
                       0uy
                       (sz 1184)
                     <:
-                    array u8 (sz 1184))
+                    t_Array u8 (sz 1184))
                 <:
                 Hacspec_lib.t_UpdatableArray (sz 1184))
               (Rust_primitives.unsize (Hacspec_kyber.Serialize.vector_encode_12_ tt_as_ntt
                     <:
-                    array u8 (sz 1152))
+                    t_Array u8 (sz 1152))
                 <:
-                slice u8)
+                t_Slice u8)
             <:
             Hacspec_lib.t_UpdatableArray (sz 1184))
           seed_for_A
         <:
         Hacspec_lib.t_UpdatableArray (sz 1184))
   in
-  let secret_key_serialized:array u8 (sz 1152) =
+  let secret_key_serialized:t_Array u8 (sz 1152) =
     Hacspec_kyber.Serialize.vector_encode_12_ secret_as_ntt
   in
   Core.Result.Result_Ok
-  (impl__new (Hacspec_lib.f_into_array (Rust_primitives.unsize secret_key_serialized <: slice u8)
+  (impl__KeyPair__new (Hacspec_lib.f_into_array (Rust_primitives.unsize secret_key_serialized
+            <:
+            t_Slice u8)
         <:
-        array u8 (sz 1152))
-      (Hacspec_lib.f_into_array (Rust_primitives.unsize public_key_serialized <: slice u8)
+        t_Array u8 (sz 1152))
+      (Hacspec_lib.f_into_array (Rust_primitives.unsize public_key_serialized <: t_Slice u8)
         <:
-        array u8 (sz 1184)))
+        t_Array u8 (sz 1184)))
 
 let encode_and_compress_u
       (input:
@@ -273,18 +281,16 @@ let encode_and_compress_u
     : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
   let out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Hacspec_lib.Vector.impl__into_iter
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Hacspec_lib.Vector.impl__into_iter
               input
             <:
             Core.Array.Iter.t_IntoIter
               (Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Array.Iter.t_IntoIter
-              (Hacspec_lib.Ring.t_PolynomialRingElement
-                  (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3)))
-          .f_IntoIter)
+        Core.Array.Iter.t_IntoIter
+          (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+              (sz 256)) (sz 3))
       out
       (fun out re ->
           Alloc.Vec.impl_2__extend_from_slice out
@@ -297,14 +303,15 @@ let encode_and_compress_u
                   <:
                   Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
               <:
-              slice u8)
+              t_Slice u8)
           <:
           Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   out
 
-let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 32))
-    : Core.Result.t_Result (array u8 (sz 1088)) Hacspec_kyber.t_BadRejectionSamplingRandomnessError =
+let encrypt (public_key: t_Array u8 (sz 1184)) (message randomness: t_Array u8 (sz 32))
+    : Core.Result.t_Result (t_Array u8 (sz 1088))
+      Hacspec_kyber.t_BadRejectionSamplingRandomnessError =
   let (domain_separator: u8):u8 = 0uy in
   let tt_as_ntt:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
@@ -314,21 +321,19 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
   let tt_as_ntt:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Core.Slice.impl__chunks (public_key.[ {
                         Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_T_AS_NTT_ENCODED_SIZE
                       } ]
                     <:
-                    slice u8)
+                    t_Slice u8)
                   Hacspec_kyber.Parameters.v_BYTES_PER_RING_ELEMENT
                 <:
                 Core.Slice.Iter.t_Chunks u8)
             <:
             Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8)))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8))
       tt_as_ntt
       (fun tt_as_ntt (i, tt_as_ntt_bytes) ->
           Rust_primitives.Hax.update_at tt_as_ntt
@@ -341,45 +346,47 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
           Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)
       )
   in
-  let seed_for_A:slice u8 =
+  let seed_for_A:t_Slice u8 =
     public_key.[ { Core.Ops.Range.f_start = Hacspec_kyber.Parameters.v_T_AS_NTT_ENCODED_SIZE } ]
   in
-  let v_A_as_ntt:array
+  let v_A_as_ntt:t_Array
     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
     (sz 3) =
     Rust_primitives.Hax.repeat Hacspec_lib.Vector.impl__ZERO (sz 3)
   in
-  let (xof_input: array u8 (sz 34)):array u8 (sz 34) = Hacspec_lib.f_into_padded_array seed_for_A in
-  let v_A_as_ntt, xof_input:(array
+  let (xof_input: t_Array u8 (sz 34)):t_Array u8 (sz 34) =
+    Hacspec_lib.f_into_padded_array seed_for_A
+  in
+  let v_A_as_ntt, xof_input:(t_Array
       (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
       (sz 3) &
-    array u8 (sz 34)) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    t_Array u8 (sz 34)) =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_RANK
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (v_A_as_ntt, xof_input)
       (fun (v_A_as_ntt, xof_input) i ->
-          Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                     Core.Ops.Range.f_start = sz 0;
                     Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_RANK
                   })
               <:
-              (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+              Core.Ops.Range.t_Range usize)
             (v_A_as_ntt, xof_input)
             (fun (v_A_as_ntt, xof_input) j ->
-                let xof_input:array u8 (sz 34) =
+                let xof_input:t_Array u8 (sz 34) =
                   Rust_primitives.Hax.update_at xof_input (sz 32) (Hacspec_lib.f_as_u8 i <: u8)
                 in
-                let xof_input:array u8 (sz 34) =
+                let xof_input:t_Array u8 (sz 34) =
                   Rust_primitives.Hax.update_at xof_input (sz 33) (Hacspec_lib.f_as_u8 j <: u8)
                 in
-                let (xof_bytes: array u8 (sz 840)):array u8 (sz 840) =
+                let (xof_bytes: t_Array u8 (sz 840)):t_Array u8 (sz 840) =
                   Hacspec_kyber.Parameters.Hash_functions.v_XOF (Rust_primitives.unsize xof_input
                       <:
-                      slice u8)
+                      t_Slice u8)
                 in
                 let* hoist6:Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
@@ -396,7 +403,7 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
                       Core.Ops.Control_flow.ControlFlow.v_Break (Core.Ops.Try_trait.f_from_residual residual
 
                           <:
-                          Core.Result.t_Result (array u8 (sz 1088))
+                          Core.Result.t_Result (t_Array u8 (sz 1088))
                             Hacspec_kyber.t_BadRejectionSamplingRandomnessError)
                     in
                     Core.Ops.Control_flow.ControlFlow_Continue
@@ -415,13 +422,13 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
                       j
                       hoist6
                   in
-                  let hoist8:array
+                  let hoist8:t_Array
                     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         (sz 256)
                         (sz 3)) (sz 3) =
                     Rust_primitives.Hax.update_at v_A_as_ntt i hoist7
                   in
-                  let v_A_as_ntt:array
+                  let v_A_as_ntt:t_Array
                     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         (sz 256)
                         (sz 3)) (sz 3) =
@@ -429,34 +436,36 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
                   in
                   v_A_as_ntt, xof_input))
           <:
-          (array
+          (t_Array
               (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                   (sz 256)
                   (sz 3)) (sz 3) &
-            array u8 (sz 34)))
+            t_Array u8 (sz 34)))
   in
   let r:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) =
     Hacspec_lib.Vector.impl__ZERO
   in
-  let (prf_input: array u8 (sz 33)):array u8 (sz 33) = Hacspec_lib.f_into_padded_array randomness in
-  let domain_separator, prf_input, r:(u8 & array u8 (sz 33) &
+  let (prf_input: t_Array u8 (sz 33)):t_Array u8 (sz 33) =
+    Hacspec_lib.f_into_padded_array randomness
+  in
+  let domain_separator, prf_input, r:(u8 & t_Array u8 (sz 33) &
     Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_lib.Vector.impl__len r <: usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (domain_separator, prf_input, r)
       (fun (domain_separator, prf_input, r) i ->
-          let prf_input:array u8 (sz 33) =
+          let prf_input:t_Array u8 (sz 33) =
             Rust_primitives.Hax.update_at prf_input (sz 32) domain_separator
           in
           let domain_separator:u8 = domain_separator +! 1uy in
-          let (prf_output: array u8 (sz 128)):array u8 (sz 128) =
+          let (prf_output: t_Array u8 (sz 128)):t_Array u8 (sz 128) =
             Hacspec_kyber.Parameters.Hash_functions.v_PRF (Rust_primitives.unsize prf_input
                 <:
-                slice u8)
+                t_Slice u8)
           in
           let r:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
             (sz 256)
@@ -464,7 +473,7 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
             Rust_primitives.Hax.update_at r
               i
               (Hacspec_kyber.Sampling.sample_poly_cbd (sz 2)
-                  (Rust_primitives.unsize prf_output <: slice u8)
+                  (Rust_primitives.unsize prf_output <: t_Slice u8)
                 <:
                 Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
@@ -478,23 +487,23 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
   in
   let domain_separator, error_1_, prf_input:(u8 &
     Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) &
-    array u8 (sz 33)) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    t_Array u8 (sz 33)) =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_lib.Vector.impl__len error_1_ <: usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (domain_separator, error_1_, prf_input)
       (fun (domain_separator, error_1_, prf_input) i ->
-          let prf_input:array u8 (sz 33) =
+          let prf_input:t_Array u8 (sz 33) =
             Rust_primitives.Hax.update_at prf_input (sz 32) domain_separator
           in
           let domain_separator:u8 = domain_separator +! 1uy in
-          let (prf_output: array u8 (sz 128)):array u8 (sz 128) =
+          let (prf_output: t_Array u8 (sz 128)):t_Array u8 (sz 128) =
             Hacspec_kyber.Parameters.Hash_functions.v_PRF (Rust_primitives.unsize prf_input
                 <:
-                slice u8)
+                t_Slice u8)
           in
           let error_1_:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
             (sz 256)
@@ -502,34 +511,34 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
             Rust_primitives.Hax.update_at error_1_
               i
               (Hacspec_kyber.Sampling.sample_poly_cbd (sz 2)
-                  (Rust_primitives.unsize prf_output <: slice u8)
+                  (Rust_primitives.unsize prf_output <: t_Slice u8)
                 <:
                 Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
           in
           domain_separator, error_1_, prf_input)
   in
-  let prf_input:array u8 (sz 33) =
+  let prf_input:t_Array u8 (sz 33) =
     Rust_primitives.Hax.update_at prf_input (sz 32) domain_separator
   in
-  let (prf_output: array u8 (sz 128)):array u8 (sz 128) =
-    Hacspec_kyber.Parameters.Hash_functions.v_PRF (Rust_primitives.unsize prf_input <: slice u8)
+  let (prf_output: t_Array u8 (sz 128)):t_Array u8 (sz 128) =
+    Hacspec_kyber.Parameters.Hash_functions.v_PRF (Rust_primitives.unsize prf_input <: t_Slice u8)
   in
   let error_2_:Hacspec_lib.Ring.t_PolynomialRingElement
     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
-    Hacspec_kyber.Sampling.sample_poly_cbd (sz 2) (Rust_primitives.unsize prf_output <: slice u8)
+    Hacspec_kyber.Sampling.sample_poly_cbd (sz 2) (Rust_primitives.unsize prf_output <: t_Slice u8)
   in
   let r_as_ntt:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
     Hacspec_kyber.Ntt.vector_ntt r
   in
-  let v_A_as_ntt_transpose:array
+  let v_A_as_ntt_transpose:t_Array
     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
     (sz 3) =
     Hacspec_kyber.Matrix.transpose v_A_as_ntt
   in
-  let u =
+  let u:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) =
     (Hacspec_kyber.Ntt.vector_inverse_ntt (Hacspec_kyber.Matrix.multiply_matrix_by_column v_A_as_ntt_transpose
             r_as_ntt
           <:
@@ -542,13 +551,14 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
   let message_as_ring_element:Hacspec_lib.Ring.t_PolynomialRingElement
     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
     Hacspec_kyber.Compress.decompress (Hacspec_kyber.Serialize.byte_decode (sz 1)
-          (Rust_primitives.unsize message <: slice u8)
+          (Rust_primitives.unsize message <: t_Slice u8)
         <:
         Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
           (sz 256))
       (sz 1)
   in
-  let v =
+  let v:Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+    (sz 256) =
     ((Hacspec_kyber.Ntt.ntt_inverse (Hacspec_kyber.Matrix.multiply_column_by_row tt_as_ntt r_as_ntt
             <:
             Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
@@ -558,7 +568,8 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
           (sz 256)) +!
       error_2_
       <:
-      (Hacspec_lib.Ring.impl_6 (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)).f_Output) +!
+      Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+        (sz 256)) +!
     message_as_ring_element
   in
   let c1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = encode_and_compress_u u in
@@ -569,31 +580,34 @@ let encrypt (public_key: array u8 (sz 1184)) (message randomness: array u8 (sz 3
         Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
           (sz 256))
   in
-  let (ciphertext: array u8 (sz 1088)):array u8 (sz 1088) = Hacspec_lib.f_into_padded_array c1 in
-  let ciphertext:array u8 (sz 1088) =
+  let (ciphertext: t_Array u8 (sz 1088)):t_Array u8 (sz 1088) =
+    Hacspec_lib.f_into_padded_array c1
+  in
+  let ciphertext:t_Array u8 (sz 1088) =
     Rust_primitives.Hax.update_at ciphertext
       ({ Core.Ops.Range.f_start = Hacspec_kyber.Parameters.v_VECTOR_U_ENCODED_SIZE })
       (Core.Slice.impl__copy_from_slice (Core.Ops.Index.IndexMut.index_mut ciphertext
               ({ Core.Ops.Range.f_start = Hacspec_kyber.Parameters.v_VECTOR_U_ENCODED_SIZE })
             <:
-            slice u8)
-          (Alloc.Vec.impl_1__as_slice c2 <: slice u8)
+            t_Slice u8)
+          (Alloc.Vec.impl_1__as_slice c2 <: t_Slice u8)
         <:
-        slice u8)
+        t_Slice u8)
   in
   Core.Result.Result_Ok ciphertext
 
-let decrypt (secret_key: array u8 (sz 1152)) (ciphertext: array u8 (sz 1088)) : array u8 (sz 32) =
+let decrypt (secret_key: t_Array u8 (sz 1152)) (ciphertext: t_Array u8 (sz 1088))
+    : t_Array u8 (sz 32) =
   let u:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) =
     Hacspec_lib.Vector.impl__ZERO
   in
   let u:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Core.Slice.impl__chunks (ciphertext.[ {
                         Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_VECTOR_U_ENCODED_SIZE
                       } ]
                     <:
-                    slice u8)
+                    t_Slice u8)
                   ((Hacspec_kyber.Parameters.v_COEFFICIENTS_IN_RING_ELEMENT *!
                       Hacspec_kyber.Parameters.v_VECTOR_U_COMPRESSION_FACTOR
                       <:
@@ -606,9 +620,7 @@ let decrypt (secret_key: array u8 (sz 1152)) (ciphertext: array u8 (sz 1088)) :
             <:
             Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8)))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8))
       u
       (fun u (i, u_bytes) ->
           Rust_primitives.Hax.update_at u
@@ -633,7 +645,7 @@ let decrypt (secret_key: array u8 (sz 1152)) (ciphertext: array u8 (sz 1088)) :
                 Core.Ops.Range.f_start = Hacspec_kyber.Parameters.v_VECTOR_U_ENCODED_SIZE
               } ]
             <:
-            slice u8)
+            t_Slice u8)
         <:
         Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
           (sz 256))
@@ -647,17 +659,15 @@ let decrypt (secret_key: array u8 (sz 1152)) (ciphertext: array u8 (sz 1088)) :
   let secret_as_ntt:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-              (Core.Slice.impl__chunks_exact (Rust_primitives.unsize secret_key <: slice u8)
+    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 secret_key <: t_Slice u8)
                   Hacspec_kyber.Parameters.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.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8)))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
       secret_as_ntt
       (fun secret_as_ntt (i, secret_bytes) ->
           Rust_primitives.Hax.update_at secret_as_ntt
@@ -675,7 +685,8 @@ let decrypt (secret_key: array u8 (sz 1152)) (ciphertext: array u8 (sz 1088)) :
     (sz 3) =
     Hacspec_kyber.Ntt.vector_ntt u
   in
-  let message =
+  let message:Hacspec_lib.Ring.t_PolynomialRingElement
+    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
     v -!
     (Hacspec_kyber.Ntt.ntt_inverse (Hacspec_kyber.Matrix.multiply_column_by_row secret_as_ntt
             u_as_ntt
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Matrix.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Matrix.fst
index 70fde061a..78784558f 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Matrix.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Matrix.fst
@@ -4,25 +4,25 @@ open Core
 
 let transpose
       (matrix:
-          array
+          t_Array
             (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                 (sz 256)
                 (sz 3)) (sz 3))
-    : array
+    : t_Array
       (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
       (sz 3) =
-  let transpose:array
+  let transpose:t_Array
     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
     (sz 3) =
     Rust_primitives.Hax.repeat Hacspec_lib.Vector.impl__ZERO (sz 3)
   in
-  let transpose:array
+  let transpose:t_Array
     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
     (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Core.Slice.impl__iter (Rust_primitives.unsize matrix
                     <:
-                    slice
+                    t_Slice
                     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         (sz 256)
                         (sz 3)))
@@ -38,16 +38,14 @@ let transpose
                   (sz 256)
                   (sz 3))))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Slice.Iter.t_Iter
-              (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
-                  (sz 256)
-                  (sz 3)))))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate
+        (Core.Slice.Iter.t_Iter
+          (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+              (sz 256)
+              (sz 3))))
       transpose
       (fun transpose (i, row) ->
-          Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
                     (Hacspec_lib.Vector.impl__iter row
                       <:
                       Core.Slice.Iter.t_Iter
@@ -59,12 +57,10 @@ let transpose
                     (Hacspec_lib.Ring.t_PolynomialRingElement
                         (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))))
               <:
-              (Core.Iter.Traits.Collect.impl
-                (Core.Iter.Adapters.Enumerate.t_Enumerate
-                  (Core.Slice.Iter.t_Iter
-                    (Hacspec_lib.Ring.t_PolynomialRingElement
-                        (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)))))
-                .f_IntoIter)
+              Core.Iter.Adapters.Enumerate.t_Enumerate
+              (Core.Slice.Iter.t_Iter
+                (Hacspec_lib.Ring.t_PolynomialRingElement
+                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))))
             transpose
             (fun transpose (j, matrix_element) ->
                 Rust_primitives.Hax.update_at transpose
@@ -81,12 +77,12 @@ let transpose
                       (sz 256)
                       (sz 3))
                 <:
-                array
+                t_Array
                   (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                       (sz 256)
                       (sz 3)) (sz 3))
           <:
-          array
+          t_Array
             (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                 (sz 256)
                 (sz 3)) (sz 3))
@@ -95,7 +91,7 @@ let transpose
 
 let multiply_matrix_by_column
       (matrix:
-          array
+          t_Array
             (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                 (sz 256)
                 (sz 3)) (sz 3))
@@ -108,7 +104,7 @@ let multiply_matrix_by_column
     (sz 3) =
     Hacspec_lib.Vector.impl__ZERO
   in
-  let transposed:array
+  let transposed:t_Array
     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3))
     (sz 3) =
     transpose matrix
@@ -116,10 +112,10 @@ let multiply_matrix_by_column
   let result:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Core.Slice.impl__iter (Rust_primitives.unsize transposed
                     <:
-                    slice
+                    t_Slice
                     (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         (sz 256)
                         (sz 3)))
@@ -135,16 +131,14 @@ let multiply_matrix_by_column
                   (sz 256)
                   (sz 3))))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Slice.Iter.t_Iter
-              (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
-                  (sz 256)
-                  (sz 3)))))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate
+        (Core.Slice.Iter.t_Iter
+          (Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+              (sz 256)
+              (sz 3))))
       result
       (fun result (i, row) ->
-          Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
                     (Hacspec_lib.Vector.impl__iter row
                       <:
                       Core.Slice.Iter.t_Iter
@@ -156,12 +150,10 @@ let multiply_matrix_by_column
                     (Hacspec_lib.Ring.t_PolynomialRingElement
                         (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))))
               <:
-              (Core.Iter.Traits.Collect.impl
-                (Core.Iter.Adapters.Enumerate.t_Enumerate
-                  (Core.Slice.Iter.t_Iter
-                    (Hacspec_lib.Ring.t_PolynomialRingElement
-                        (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)))))
-                .f_IntoIter)
+              Core.Iter.Adapters.Enumerate.t_Enumerate
+              (Core.Slice.Iter.t_Iter
+                (Hacspec_lib.Ring.t_PolynomialRingElement
+                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))))
             result
             (fun result (j, matrix_element) ->
                 let product:Hacspec_lib.Ring.t_PolynomialRingElement
@@ -182,9 +174,8 @@ let multiply_matrix_by_column
                           (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) +!
                       product
                       <:
-                      (Hacspec_lib.Ring.impl_6 (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
-                          (sz 256))
-                        .f_Output)
+                      Hacspec_lib.Ring.t_PolynomialRingElement
+                        (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
                 in
                 result)
           <:
@@ -203,8 +194,9 @@ let multiply_column_by_row
     (sz 256) =
     Hacspec_lib.Ring.impl_2__ZERO
   in
-  let result =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_zip
+  let result:Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+    (sz 256) =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_zip
               (Hacspec_lib.Vector.impl__iter column_vector
                 <:
                 Core.Slice.Iter.t_Iter
@@ -217,24 +209,20 @@ let multiply_column_by_row
                     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)))
             <:
             Core.Iter.Adapters.Zip.t_Zip
-              (Core.Slice.Iter.t_Iter
-                (Hacspec_lib.Ring.t_PolynomialRingElement
-                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)))
-              (Core.Iter.Traits.Collect.impl
-                (Core.Slice.Iter.t_Iter
-                  (Hacspec_lib.Ring.t_PolynomialRingElement
-                      (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))))
-                .f_IntoIter)
-        <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Zip.t_Zip
               (Core.Slice.Iter.t_Iter
                 (Hacspec_lib.Ring.t_PolynomialRingElement
                     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)))
               (Core.Slice.Iter.t_Iter
                 (Hacspec_lib.Ring.t_PolynomialRingElement
-                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)))))
-          .f_IntoIter)
+                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))))
+        <:
+        Core.Iter.Adapters.Zip.t_Zip
+          (Core.Slice.Iter.t_Iter
+            (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+                (sz 256)))
+          (Core.Slice.Iter.t_Iter
+            (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+                (sz 256))))
       result
       (fun result (column_element, row_element) ->
           result +!
@@ -243,7 +231,7 @@ let multiply_column_by_row
             Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
               (sz 256))
           <:
-          (Hacspec_lib.Ring.impl_6 (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)).f_Output
-      )
+          Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+            (sz 256))
   in
   result
\ No newline at end of file
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ntt.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ntt.fst
index db09d2b74..8339230c8 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ntt.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Ntt.fst
@@ -7,7 +7,7 @@ let v_ZETA: Hacspec_lib.Field.t_PrimeFieldElement 3329us = { Hacspec_lib.Field.f
 let v_INVERSE_OF_128_: Hacspec_lib.Field.t_PrimeFieldElement 3329us =
   { Hacspec_lib.Field.f_value = 3303us }
 
-let v_NTT_LAYERS: array usize (sz 7) =
+let v_NTT_LAYERS: t_Array usize (sz 7) =
   let list = [sz 2; sz 4; sz 8; sz 16; sz 32; sz 64; sz 128] in
   FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 7);
   Rust_primitives.Hax.array_of_list list
@@ -15,12 +15,12 @@ let v_NTT_LAYERS: array usize (sz 7) =
 let bit_rev_7_ (value: u8) : u8 =
   let (reversed: u8):u8 = 0uy in
   let reversed:u8 =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = 0ul;
-              Core.Ops.Range.f_end = Core.Num.impl_6__BITS -! 1ul <: u32
+              Core.Ops.Range.f_end = Core.Num.impl__u8__BITS -! 1ul <: u32
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range u32)).f_IntoIter)
+        Core.Ops.Range.t_Range u32)
       reversed
       (fun reversed bit ->
           let reversed:u8 = reversed <<! 1l in
@@ -43,34 +43,28 @@ let ntt
   let ff_hat, k:(Hacspec_lib.Ring.t_PolynomialRingElement
       (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) &
     u8) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_rev
-              (Core.Slice.impl__iter (Rust_primitives.unsize v_NTT_LAYERS <: slice usize)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_rev
+              (Core.Slice.impl__iter (Rust_primitives.unsize v_NTT_LAYERS <: t_Slice usize)
                 <:
                 Core.Slice.Iter.t_Iter usize)
             <:
             Core.Iter.Adapters.Rev.t_Rev (Core.Slice.Iter.t_Iter usize))
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Iter.Adapters.Rev.t_Rev (Core.Slice.Iter.t_Iter usize))
-        )
-          .f_IntoIter)
+        Core.Iter.Adapters.Rev.t_Rev (Core.Slice.Iter.t_Iter usize))
       (ff_hat, k)
       (fun (ff_hat, k) len ->
-          Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_step_by
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_step_by
                     ({
                         Core.Ops.Range.f_start = sz 0;
                         Core.Ops.Range.f_end
                         =
-                        Hacspec_kyber.Parameters.v_COEFFICIENTS_IN_RING_ELEMENT -! len
-                        <:
-                        (Core.Ops.Arith.impl_71).f_Output
+                        Hacspec_kyber.Parameters.v_COEFFICIENTS_IN_RING_ELEMENT -! len <: usize
                       })
-                    (sz 2 *! len <: (Core.Ops.Arith.impl_127).f_Output)
+                    (sz 2 *! len <: usize)
                   <:
                   Core.Iter.Adapters.Step_by.t_StepBy (Core.Ops.Range.t_Range usize))
               <:
-              (Core.Iter.Traits.Collect.impl
-                (Core.Iter.Adapters.Step_by.t_StepBy (Core.Ops.Range.t_Range usize)))
-                .f_IntoIter)
+              Core.Iter.Adapters.Step_by.t_StepBy (Core.Ops.Range.t_Range usize))
             (ff_hat, k)
             (fun (ff_hat, k) start ->
                 let zeta:Hacspec_lib.Field.t_PrimeFieldElement 3329us =
@@ -79,27 +73,27 @@ let ntt
                 let k:u8 = k +! 1uy in
                 let ff_hat:Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
-                  Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+                  Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                             Core.Ops.Range.f_start = start;
-                            Core.Ops.Range.f_end = start +! len <: (Core.Ops.Arith.impl_15).f_Output
+                            Core.Ops.Range.f_end = start +! len <: usize
                           })
                       <:
-                      (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+                      Core.Ops.Range.t_Range usize)
                     ff_hat
                     (fun ff_hat j ->
-                        let t =
+                        let t:Hacspec_lib.Field.t_PrimeFieldElement 3329us =
                           zeta *!
-                          (ff_hat.[ j +! len <: (Core.Ops.Arith.impl_15).f_Output ]
+                          (ff_hat.[ j +! len <: usize ]
                             <:
                             Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         in
                         let ff_hat:Hacspec_lib.Ring.t_PolynomialRingElement
                           (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
                           Rust_primitives.Hax.update_at ff_hat
-                            (j +! len <: (Core.Ops.Arith.impl_15).f_Output)
+                            (j +! len <: usize)
                             ((ff_hat.[ j ] <: Hacspec_lib.Field.t_PrimeFieldElement 3329us) -! t
                               <:
-                              (Hacspec_lib.Field.impl_8 3329us).f_Output)
+                              Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         in
                         let ff_hat:Hacspec_lib.Ring.t_PolynomialRingElement
                           (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
@@ -107,7 +101,7 @@ let ntt
                             j
                             ((ff_hat.[ j ] <: Hacspec_lib.Field.t_PrimeFieldElement 3329us) +! t
                               <:
-                              (Hacspec_lib.Field.impl_7 3329us).f_Output)
+                              Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         in
                         ff_hat)
                 in
@@ -133,12 +127,12 @@ let ntt_inverse
   let f, k:(Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       (sz 256) &
     u8) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter v_NTT_LAYERS
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter v_NTT_LAYERS
         <:
-        (Core.Array.Iter.impl usize (sz 7)).f_IntoIter)
+        Core.Array.Iter.t_IntoIter usize (sz 7))
       (f, k)
       (fun (f, k) len ->
-          Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_step_by
+          Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_step_by
                     ({
                         Core.Ops.Range.f_start = sz 0;
                         Core.Ops.Range.f_end
@@ -149,9 +143,7 @@ let ntt_inverse
                   <:
                   Core.Iter.Adapters.Step_by.t_StepBy (Core.Ops.Range.t_Range usize))
               <:
-              (Core.Iter.Traits.Collect.impl
-                (Core.Iter.Adapters.Step_by.t_StepBy (Core.Ops.Range.t_Range usize)))
-                .f_IntoIter)
+              Core.Iter.Adapters.Step_by.t_StepBy (Core.Ops.Range.t_Range usize))
             (f, k)
             (fun (f, k) start ->
                 let zeta:Hacspec_lib.Field.t_PrimeFieldElement 3329us =
@@ -160,12 +152,12 @@ let ntt_inverse
                 let k:u8 = k -! 1uy in
                 let f:Hacspec_lib.Ring.t_PolynomialRingElement
                   (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
-                  Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+                  Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                             Core.Ops.Range.f_start = start;
                             Core.Ops.Range.f_end = start +! len <: usize
                           })
                       <:
-                      (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+                      Core.Ops.Range.t_Range usize)
                     f
                     (fun f j ->
                         let t:Hacspec_lib.Field.t_PrimeFieldElement 3329us = f.[ j ] in
@@ -178,7 +170,7 @@ let ntt_inverse
                                 <:
                                 Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                               <:
-                              (Hacspec_lib.Field.impl_7 3329us).f_Output)
+                              Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         in
                         let f:Hacspec_lib.Ring.t_PolynomialRingElement
                           (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
@@ -190,9 +182,9 @@ let ntt_inverse
                                   Hacspec_lib.Field.t_PrimeFieldElement 3329us) -!
                                 t
                                 <:
-                                (Hacspec_lib.Field.impl_8 3329us).f_Output)
+                                Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                               <:
-                              (Hacspec_lib.Field.impl_9 3329us).f_Output)
+                              Hacspec_lib.Field.t_PrimeFieldElement 3329us)
                         in
                         f)
                 in
@@ -204,27 +196,27 @@ let ntt_inverse
   in
   let f:Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end
               =
               Core.Slice.impl__len (Rust_primitives.unsize (Hacspec_lib.Ring.impl_2__coefficients f
                       <:
-                      array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+                      t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
                   <:
-                  slice (Hacspec_lib.Field.t_PrimeFieldElement 3329us))
+                  t_Slice (Hacspec_lib.Field.t_PrimeFieldElement 3329us))
               <:
               usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       f
       (fun f i ->
           Rust_primitives.Hax.update_at f
             i
             ((f.[ i ] <: Hacspec_lib.Field.t_PrimeFieldElement 3329us) *! v_INVERSE_OF_128_
               <:
-              (Hacspec_lib.Field.impl_9 3329us).f_Output)
+              Hacspec_lib.Field.t_PrimeFieldElement 3329us)
           <:
           Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
             (sz 256))
@@ -243,12 +235,12 @@ let multiply_ntts
   in
   let h_hat:Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = sz 128
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       h_hat
       (fun h_hat i ->
           let binomial_product:(Hacspec_lib.Field.t_PrimeFieldElement 3329us &
@@ -298,10 +290,10 @@ let base_case_multiply
       c with
       _1
       =
-      (a._1 *! b._1 <: (Hacspec_lib.Field.impl_9 3329us).f_Output) +!
-      ((a._2 *! b._2 <: (Hacspec_lib.Field.impl_9 3329us).f_Output) *! zeta
+      (a._1 *! b._1 <: Hacspec_lib.Field.t_PrimeFieldElement 3329us) +!
+      ((a._2 *! b._2 <: Hacspec_lib.Field.t_PrimeFieldElement 3329us) *! zeta
         <:
-        (Hacspec_lib.Field.impl_9 3329us).f_Output)
+        Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     }
   in
   let c:(Hacspec_lib.Field.t_PrimeFieldElement 3329us & Hacspec_lib.Field.t_PrimeFieldElement 3329us
@@ -310,8 +302,8 @@ let base_case_multiply
       c with
       _2
       =
-      (a._1 *! b._2 <: (Hacspec_lib.Field.impl_9 3329us).f_Output) +!
-      (a._2 *! b._1 <: (Hacspec_lib.Field.impl_9 3329us).f_Output)
+      (a._1 *! b._2 <: Hacspec_lib.Field.t_PrimeFieldElement 3329us) +!
+      (a._2 *! b._1 <: Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     }
   in
   c
@@ -329,7 +321,7 @@ let vector_ntt
   let vector_as_ntt:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Hacspec_lib.Vector.impl__into_iter vector
                 <:
                 Core.Array.Iter.t_IntoIter
@@ -341,12 +333,10 @@ let vector_ntt
                 (Hacspec_lib.Ring.t_PolynomialRingElement
                     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3)))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Array.Iter.t_IntoIter
-                (Hacspec_lib.Ring.t_PolynomialRingElement
-                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3))))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate
+        (Core.Array.Iter.t_IntoIter
+            (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+                (sz 256)) (sz 3)))
       vector_as_ntt
       (fun vector_as_ntt (i, re) ->
           Rust_primitives.Hax.update_at vector_as_ntt
@@ -374,7 +364,7 @@ let vector_inverse_ntt
   let vector:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256)
     (sz 3) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Hacspec_lib.Vector.impl__into_iter vector_as_ntt
                 <:
                 Core.Array.Iter.t_IntoIter
@@ -386,12 +376,10 @@ let vector_inverse_ntt
                 (Hacspec_lib.Ring.t_PolynomialRingElement
                     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3)))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Array.Iter.t_IntoIter
-                (Hacspec_lib.Ring.t_PolynomialRingElement
-                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3))))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate
+        (Core.Array.Iter.t_IntoIter
+            (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+                (sz 256)) (sz 3)))
       vector
       (fun vector (i, re_ntt) ->
           Rust_primitives.Hax.update_at vector
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Parameters.Hash_functions.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Parameters.Hash_functions.fst
index 7d1ee4bfb..9797f8bf0 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Parameters.Hash_functions.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Parameters.Hash_functions.fst
@@ -2,14 +2,14 @@ module Hacspec_kyber.Parameters.Hash_functions
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 
-let v_G (input: slice u8) : array u8 (sz 64) = Libcrux.Digest.sha3_512_ input
+let v_G (input: t_Slice u8) : t_Array u8 (sz 64) = Libcrux.Digest.sha3_512_ input
 
 let v_H_DIGEST_SIZE: usize = Libcrux.Digest.digest_size Libcrux.Digest.Algorithm_Sha3_256_
 
-let v_H (input: slice u8) : array u8 (sz 32) = Libcrux.Digest.sha3_256_ input
+let v_H (input: t_Slice u8) : t_Array u8 (sz 32) = Libcrux.Digest.sha3_256_ input
 
-let v_PRF (#v_LEN: usize) (input: slice u8) : array u8 v_LEN = Libcrux.Digest.shake256 input
+let v_PRF (#v_LEN: usize) (input: t_Slice u8) : t_Array u8 v_LEN = Libcrux.Digest.shake256 input
 
-let v_XOF (#v_LEN: usize) (input: slice u8) : array u8 v_LEN = Libcrux.Digest.shake128 input
+let v_XOF (#v_LEN: usize) (input: t_Slice u8) : t_Array u8 v_LEN = Libcrux.Digest.shake128 input
 
-let v_J (#v_LEN: usize) (input: slice u8) : array u8 v_LEN = Libcrux.Digest.shake256 input
\ No newline at end of file
+let v_J (#v_LEN: usize) (input: t_Slice u8) : t_Array u8 v_LEN = Libcrux.Digest.shake256 input
\ No newline at end of file
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Sampling.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Sampling.fst
index 89323b405..b0f362dd9 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Sampling.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Sampling.fst
@@ -2,7 +2,7 @@ module Hacspec_kyber.Sampling
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 
-let sample_ntt (bytes: array u8 (sz 840))
+let sample_ntt (bytes: t_Array u8 (sz 840))
     : Core.Result.t_Result
       (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
           (sz 256)) Hacspec_kyber.t_BadRejectionSamplingRandomnessError =
@@ -17,13 +17,13 @@ let sample_ntt (bytes: array u8 (sz 840))
   let a_hat, sampled_coefficients:(Hacspec_lib.Ring.t_PolynomialRingElement
       (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) &
     usize) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__chunks
-              (Rust_primitives.unsize bytes <: slice u8)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__chunks (
+                Rust_primitives.unsize bytes <: t_Slice u8)
               (sz 3)
             <:
             Core.Slice.Iter.t_Chunks u8)
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Slice.Iter.t_Chunks u8)).f_IntoIter)
+        Core.Slice.Iter.t_Chunks u8)
       (a_hat, sampled_coefficients)
       (fun (a_hat, sampled_coefficients) byte_chunk ->
           let b:u16 = Core.Convert.f_from (byte_chunk.[ sz 0 ] <: u8) in
@@ -65,21 +65,21 @@ let sample_ntt (bytes: array u8 (sz 840))
   then Core.Result.Result_Ok a_hat
   else Core.Result.Result_Err Hacspec_kyber.BadRejectionSamplingRandomnessError
 
-let sum_coins (coins: slice u8) : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
+let sum_coins (coins: t_Slice u8) : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
   let (sum: u8):u8 = 0uy in
   let sum:u8 =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter
-              coins
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter coins
+
             <:
             Core.Slice.Iter.t_Iter u8)
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Slice.Iter.t_Iter u8)).f_IntoIter)
+        Core.Slice.Iter.t_Iter u8)
       sum
       (fun sum coin -> Core.Ops.Arith.f_add_assign sum coin <: u8)
   in
   Core.Convert.f_into sum
 
-let sample_poly_cbd (eta: usize) (bytes: slice u8)
+let sample_poly_cbd (eta: usize) (bytes: t_Slice u8)
     : Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       (sz 256) =
   let _:Prims.unit =
@@ -97,7 +97,7 @@ let sample_poly_cbd (eta: usize) (bytes: slice u8)
   in
   let bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Hacspec_kyber.Serialize.bytes_to_bits bytes in
   let bits:Core.Slice.Iter.t_Chunks u8 =
-    Core.Slice.impl__chunks (Core.Ops.Deref.f_deref bits <: slice u8) eta
+    Core.Slice.impl__chunks (Core.Ops.Deref.f_deref bits <: t_Slice u8) eta
   in
   let
   (f:
@@ -109,39 +109,39 @@ let sample_poly_cbd (eta: usize) (bytes: slice u8)
   let bits, f:(Core.Slice.Iter.t_Chunks u8 &
     Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)
   ) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_lib.Ring.impl_2__len f <: usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (bits, f)
       (fun (bits, f) i ->
-          let tmp0, out:(Core.Slice.Iter.t_Chunks u8 &
-            Core.Option.t_Option (Core.Slice.Iter.impl_70 u8).f_Item) =
+          let tmp0, out:(Core.Slice.Iter.t_Chunks u8 & Core.Option.t_Option (t_Slice u8)) =
             Core.Iter.Traits.Iterator.f_next bits
           in
           let bits:Core.Slice.Iter.t_Chunks u8 = tmp0 in
-          let hoist9:Core.Option.t_Option (Core.Slice.Iter.impl_70 u8).f_Item = out in
-          let hoist10:slice u8 = Core.Option.impl__unwrap hoist9 in
+          let hoist9:Core.Option.t_Option (t_Slice u8) = out in
+          let hoist10:t_Slice u8 = Core.Option.impl__unwrap hoist9 in
           let (x: Hacspec_lib.Field.t_PrimeFieldElement 3329us):Hacspec_lib.Field.t_PrimeFieldElement
           3329us =
             sum_coins hoist10
           in
-          let tmp0, out:(Core.Slice.Iter.t_Chunks u8 &
-            Core.Option.t_Option (Core.Slice.Iter.impl_70 u8).f_Item) =
+          let tmp0, out:(Core.Slice.Iter.t_Chunks u8 & Core.Option.t_Option (t_Slice u8)) =
             Core.Iter.Traits.Iterator.f_next bits
           in
           let bits:Core.Slice.Iter.t_Chunks u8 = tmp0 in
-          let hoist11:Core.Option.t_Option (Core.Slice.Iter.impl_70 u8).f_Item = out in
-          let hoist12:slice u8 = Core.Option.impl__unwrap hoist11 in
+          let hoist11:Core.Option.t_Option (t_Slice u8) = out in
+          let hoist12:t_Slice u8 = Core.Option.impl__unwrap hoist11 in
           let (y: Hacspec_lib.Field.t_PrimeFieldElement 3329us):Hacspec_lib.Field.t_PrimeFieldElement
           3329us =
             sum_coins hoist12
           in
           let f:Hacspec_lib.Ring.t_PolynomialRingElement
             (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) =
-            Rust_primitives.Hax.update_at f i (x -! y <: (Hacspec_lib.Field.impl_8 3329us).f_Output)
+            Rust_primitives.Hax.update_at f
+              i
+              (x -! y <: Hacspec_lib.Field.t_PrimeFieldElement 3329us)
           in
           bits, f)
   in
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Serialize.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Serialize.fst
index cb6b38dcb..a3dd381f4 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Serialize.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Serialize.fst
@@ -13,33 +13,26 @@ let bits_to_bytes (bits: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   let bytes:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
   let bytes:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__chunks
-              (Core.Ops.Deref.f_deref bits <: slice u8)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__chunks (
+                Core.Ops.Deref.f_deref bits <: t_Slice u8)
               (sz 8)
             <:
             Core.Slice.Iter.t_Chunks u8)
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Slice.Iter.t_Chunks u8)).f_IntoIter)
+        Core.Slice.Iter.t_Chunks u8)
       bytes
       (fun bytes bit_chunk ->
           let byte_value:u8 = 0uy in
           let byte_value:u8 =
-            Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-                      (Core.Iter.Traits.Collect.f_into_iter bit_chunk
-                        <:
-                        (Core.Slice.Iter.impl u8).f_IntoIter)
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+                      (Core.Iter.Traits.Collect.f_into_iter bit_chunk <: Core.Slice.Iter.t_Iter u8)
                     <:
                     Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter u8))
                 <:
-                (Core.Iter.Traits.Collect.impl
-                  (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter u8)))
-                  .f_IntoIter)
+                Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter u8))
               byte_value
               (fun byte_value (i, bit) ->
-                  byte_value +!
-                  (bit *! (Core.Num.impl_6__pow 2uy (cast i <: u32) <: u8)
-                    <:
-                    (Core.Ops.Arith.impl_129).f_Output)
+                  byte_value +! (bit *! (Core.Num.impl__u8__pow 2uy (cast i <: u32) <: u8) <: u8)
                   <:
                   u8)
           in
@@ -50,25 +43,25 @@ let bits_to_bytes (bits: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   bytes
 
-let bytes_to_bits (bytes: slice u8) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+let bytes_to_bits (bytes: t_Slice u8) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
   let bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter
-              bytes
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.impl__iter bytes
+
             <:
             Core.Slice.Iter.t_Iter u8)
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Slice.Iter.t_Iter u8)).f_IntoIter)
+        Core.Slice.Iter.t_Iter u8)
       bits
       (fun bits byte ->
           let byte_value:u8 = byte in
           let bits, byte_value:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u8) =
-            Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                       Core.Ops.Range.f_start = 0ul;
-                      Core.Ops.Range.f_end = Core.Num.impl_6__BITS
+                      Core.Ops.Range.f_end = Core.Num.impl__u8__BITS
                     })
                 <:
-                (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range u32)).f_IntoIter)
+                Core.Ops.Range.t_Range u32)
               (bits, byte_value)
               (fun (bits, byte_value) _ ->
                   let bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
@@ -97,22 +90,22 @@ let byte_encode
   in
   let re_bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new in
   let re_bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Hacspec_lib.Ring.impl_2__coefficients
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Hacspec_lib.Ring.impl_2__coefficients
               re
             <:
-            array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
+            t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
         <:
-        (Core.Array.impl_13 (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)).f_IntoIter)
+        Core.Slice.Iter.t_Iter (Hacspec_lib.Field.t_PrimeFieldElement 3329us))
       re_bits
       (fun re_bits coefficient ->
           let coefficient_value:u16 = coefficient.Hacspec_lib.Field.f_value in
           let coefficient_value, re_bits:(u16 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-            Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
                       Core.Ops.Range.f_start = sz 0;
                       Core.Ops.Range.f_end = bits_per_coefficient
                     })
                 <:
-                (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+                Core.Ops.Range.t_Range usize)
               (coefficient_value, re_bits)
               (fun (coefficient_value, re_bits) _ ->
                   let bit:u16 = coefficient_value %! 2us in
@@ -126,7 +119,7 @@ let byte_encode
   in
   bits_to_bytes re_bits
 
-let field_element_from_bits (bits: slice u8) : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
+let field_element_from_bits (bits: t_Slice u8) : Hacspec_lib.Field.t_PrimeFieldElement 3329us =
   let _:Prims.unit =
     if
       ~.((Core.Slice.impl__len bits <: usize) <=. Hacspec_kyber.Parameters.v_BITS_PER_COEFFICIENT
@@ -139,25 +132,23 @@ let field_element_from_bits (bits: slice u8) : Hacspec_lib.Field.t_PrimeFieldEle
           Rust_primitives.Hax.t_Never)
   in
   let modulus:u16 =
-    Core.Num.impl_7__pow 2us (Hacspec_lib.f_as_u32 (Core.Slice.impl__len bits <: usize) <: u32)
+    Core.Num.impl__u16__pow 2us (Hacspec_lib.f_as_u32 (Core.Slice.impl__len bits <: usize) <: u32)
   in
   let (value: u16):u16 = 0us in
   let value:u16 =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-              (Core.Iter.Traits.Collect.f_into_iter bits <: (Core.Slice.Iter.impl u8).f_IntoIter)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+              (Core.Iter.Traits.Collect.f_into_iter bits <: Core.Slice.Iter.t_Iter u8)
             <:
             Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter u8))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter u8)))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter u8))
       value
       (fun value (i, bit) ->
           value +! (((cast bit <: u16) *! (1us <<! i <: u16) <: u16) %! modulus <: u16) <: u16)
   in
   Core.Convert.f_into value
 
-let byte_decode (bits_per_coefficient: usize) (re_bytes: slice u8)
+let byte_decode (bits_per_coefficient: usize) (re_bytes: t_Slice u8)
     : Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
       (sz 256) =
   let _:Prims.unit =
@@ -183,7 +174,7 @@ let byte_decode (bits_per_coefficient: usize) (re_bytes: slice u8)
   in
   let re_bits:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = bytes_to_bits re_bytes in
   let re_bit_chunks:Core.Slice.Iter.t_Chunks u8 =
-    Core.Slice.impl__chunks (Core.Ops.Deref.f_deref re_bits <: slice u8) bits_per_coefficient
+    Core.Slice.impl__chunks (Core.Ops.Deref.f_deref re_bits <: t_Slice u8) bits_per_coefficient
   in
   let re:Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
     (sz 256) =
@@ -192,21 +183,20 @@ let byte_decode (bits_per_coefficient: usize) (re_bytes: slice u8)
   let re, re_bit_chunks:(Hacspec_lib.Ring.t_PolynomialRingElement
       (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) &
     Core.Slice.Iter.t_Chunks u8) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end = Hacspec_lib.Ring.impl_2__len re <: usize
             })
         <:
-        (Core.Iter.Traits.Collect.impl (Core.Ops.Range.t_Range usize)).f_IntoIter)
+        Core.Ops.Range.t_Range usize)
       (re, re_bit_chunks)
       (fun (re, re_bit_chunks) i ->
-          let tmp0, out:(Core.Slice.Iter.t_Chunks u8 &
-            Core.Option.t_Option (Core.Slice.Iter.impl_70 u8).f_Item) =
+          let tmp0, out:(Core.Slice.Iter.t_Chunks u8 & Core.Option.t_Option (t_Slice u8)) =
             Core.Iter.Traits.Iterator.f_next re_bit_chunks
           in
           let re_bit_chunks:Core.Slice.Iter.t_Chunks u8 = tmp0 in
-          let hoist13:Core.Option.t_Option (Core.Slice.Iter.impl_70 u8).f_Item = out in
-          let hoist14:slice u8 = Core.Option.impl__unwrap hoist13 in
+          let hoist13:Core.Option.t_Option (t_Slice u8) = out in
+          let hoist14:t_Slice u8 = Core.Option.impl__unwrap hoist13 in
           let hoist15:Hacspec_lib.Field.t_PrimeFieldElement 3329us =
             field_element_from_bits hoist14
           in
@@ -222,10 +212,10 @@ let vector_encode_12_
       (vector:
           Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)
         )
-    : array u8 (sz 1152) =
-  let out:array u8 (sz 1152) = Rust_primitives.Hax.repeat 0uy (sz 1152) in
-  let out:array u8 (sz 1152) =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+    : t_Array u8 (sz 1152) =
+  let out:t_Array u8 (sz 1152) = Rust_primitives.Hax.repeat 0uy (sz 1152) in
+  let out:t_Array u8 (sz 1152) =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
               (Hacspec_lib.Vector.impl__into_iter vector
                 <:
                 Core.Array.Iter.t_IntoIter
@@ -237,12 +227,10 @@ let vector_encode_12_
                 (Hacspec_lib.Ring.t_PolynomialRingElement
                     (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3)))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Array.Iter.t_IntoIter
-                (Hacspec_lib.Ring.t_PolynomialRingElement
-                    (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256)) (sz 3))))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate
+        (Core.Array.Iter.t_IntoIter
+            (Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
+                (sz 256)) (sz 3)))
       out
       (fun out (i, re) ->
           Rust_primitives.Hax.update_at out
@@ -266,20 +254,20 @@ let vector_encode_12_
                         usize
                       })
                   <:
-                  slice u8)
+                  t_Slice u8)
                 (Core.Ops.Deref.f_deref (byte_encode (sz 12) re
                       <:
                       Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
                   <:
-                  slice u8)
+                  t_Slice u8)
               <:
-              slice u8)
+              t_Slice u8)
           <:
-          array u8 (sz 1152))
+          t_Array u8 (sz 1152))
   in
   out
 
-let vector_decode_12_ (encoded: array u8 (sz 1152))
+let vector_decode_12_ (encoded: t_Array u8 (sz 1152))
     : Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3) =
   let out:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)
   =
@@ -287,17 +275,15 @@ let vector_decode_12_ (encoded: array u8 (sz 1152))
   in
   let out:Hacspec_lib.Vector.t_Vector (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256) (sz 3)
   =
-    Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
-              (Core.Slice.impl__chunks (Rust_primitives.unsize encoded <: slice u8)
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+              (Core.Slice.impl__chunks (Rust_primitives.unsize encoded <: t_Slice u8)
                   Hacspec_kyber.Parameters.v_BYTES_PER_RING_ELEMENT
                 <:
                 Core.Slice.Iter.t_Chunks u8)
             <:
             Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8))
         <:
-        (Core.Iter.Traits.Collect.impl
-          (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8)))
-          .f_IntoIter)
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks u8))
       out
       (fun out (i, bytes) ->
           Rust_primitives.Hax.update_at out
diff --git a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.fst b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.fst
index efe98b7f2..bd1c00e7a 100644
--- a/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.fst
+++ b/specs/kyber/proofs/fstar/extraction/Hacspec_kyber.fst
@@ -25,22 +25,22 @@ type t_BadRejectionSamplingRandomnessError =
   | BadRejectionSamplingRandomnessError : t_BadRejectionSamplingRandomnessError
 
 type t_KeyPair = {
-  f_pk:array u8 (sz 1184);
-  f_sk:array u8 (sz 2400)
+  f_pk:t_Array u8 (sz 1184);
+  f_sk:t_Array u8 (sz 2400)
 }
 
-let impl__new (pk: array u8 (sz 1184)) (sk: array u8 (sz 2400)) : t_KeyPair =
+let impl__KeyPair__new (pk: t_Array u8 (sz 1184)) (sk: t_Array u8 (sz 2400)) : t_KeyPair =
   { f_pk = pk; f_sk = sk }
 
-let generate_keypair (randomness: array u8 (sz 64))
+let generate_keypair (randomness: t_Array u8 (sz 64))
     : Core.Result.t_Result t_KeyPair t_BadRejectionSamplingRandomnessError =
-  Rust_primitives.Hax.Control_flow_monad.Mexception.run (let ind_cpa_keypair_randomness:slice u8 =
+  Rust_primitives.Hax.Control_flow_monad.Mexception.run (let ind_cpa_keypair_randomness:t_Slice u8 =
         randomness.[ {
             Core.Ops.Range.f_start = sz 0;
             Core.Ops.Range.f_end = Hacspec_kyber.Parameters.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
           } ]
       in
-      let implicit_rejection_value:slice u8 =
+      let implicit_rejection_value:t_Slice u8 =
         randomness.[ {
             Core.Ops.Range.f_start = Hacspec_kyber.Parameters.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
           } ]
@@ -50,7 +50,7 @@ let generate_keypair (randomness: array u8 (sz 64))
           Core.Ops.Try_trait.f_branch (Hacspec_kyber.Ind_cpa.generate_keypair (Hacspec_lib.f_as_array
                     ind_cpa_keypair_randomness
                   <:
-                  array u8 (sz 32))
+                  t_Array u8 (sz 32))
               <:
               Core.Result.t_Result Hacspec_kyber.Ind_cpa.t_KeyPair
                 t_BadRejectionSamplingRandomnessError)
@@ -66,18 +66,20 @@ let generate_keypair (randomness: array u8 (sz 64))
           Core.Ops.Control_flow.ControlFlow_Continue v_val
       in
       Core.Ops.Control_flow.ControlFlow_Continue
-      (let secret_key_serialized:array u8 (sz 2400) =
-          Hacspec_kyber.Ind_cpa.impl__serialize_secret_key ind_cpa_key_pair
-            (Hacspec_lib.f_as_array implicit_rejection_value <: array u8 (sz 32))
+      (let secret_key_serialized:t_Array u8 (sz 2400) =
+          Hacspec_kyber.Ind_cpa.impl__KeyPair__serialize_secret_key ind_cpa_key_pair
+            (Hacspec_lib.f_as_array implicit_rejection_value <: t_Array u8 (sz 32))
         in
         let key_pair:t_KeyPair =
-          impl__new (Hacspec_kyber.Ind_cpa.impl__pk ind_cpa_key_pair <: array u8 (sz 1184))
+          impl__KeyPair__new (Hacspec_kyber.Ind_cpa.impl__KeyPair__pk ind_cpa_key_pair
+              <:
+              t_Array u8 (sz 1184))
             secret_key_serialized
         in
         Core.Result.Result_Ok key_pair))
 
-let public_key_modulus_check (public_key: array u8 (sz 1184)) : bool =
-  let encoded_ring_elements:slice u8 =
+let public_key_modulus_check (public_key: t_Array u8 (sz 1184)) : bool =
+  let encoded_ring_elements:t_Slice u8 =
     public_key.[ {
         Core.Ops.Range.f_start = sz 0;
         Core.Ops.Range.f_end = v_KYBER768_PUBLIC_KEY_SIZE -! sz 32 <: usize
@@ -88,16 +90,15 @@ let public_key_modulus_check (public_key: array u8 (sz 1184)) : bool =
     Hacspec_kyber.Serialize.vector_decode_12_ (Core.Result.impl__unwrap (Core.Convert.f_try_into encoded_ring_elements
 
             <:
-            Core.Result.t_Result (array u8 (sz 1152))
-              (Core.Convert.impl_6 (slice u8) (array u8 (sz 1152))).f_Error)
+            Core.Result.t_Result (t_Array u8 (sz 1152)) Core.Array.t_TryFromSliceError)
         <:
-        array u8 (sz 1152))
+        t_Array u8 (sz 1152))
   in
   encoded_ring_elements =.
-  (Hacspec_kyber.Serialize.vector_encode_12_ decoded_ring_elements <: array u8 (sz 1152))
+  (Hacspec_kyber.Serialize.vector_encode_12_ decoded_ring_elements <: t_Array u8 (sz 1152))
 
-let encapsulate (public_key: array u8 (sz 1184)) (randomness: array u8 (sz 32))
-    : Core.Result.t_Result (array u8 (sz 1088) & array u8 (sz 32))
+let encapsulate (public_key: t_Array u8 (sz 1184)) (randomness: t_Array u8 (sz 32))
+    : Core.Result.t_Result (t_Array u8 (sz 1088) & t_Array u8 (sz 32))
       t_BadRejectionSamplingRandomnessError =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (let _:Prims.unit =
         if ~.(public_key_modulus_check public_key <: bool)
@@ -107,37 +108,37 @@ let encapsulate (public_key: array u8 (sz 1184)) (randomness: array u8 (sz 32))
               <:
               Rust_primitives.Hax.t_Never)
       in
-      let (to_hash: array u8 (sz 64)):array u8 (sz 64) =
+      let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) =
         Hacspec_lib.f_push randomness
           (Rust_primitives.unsize (Hacspec_kyber.Parameters.Hash_functions.v_H (Rust_primitives.unsize
                       public_key
                     <:
-                    slice u8)
+                    t_Slice u8)
                 <:
-                array u8 (sz 32))
+                t_Array u8 (sz 32))
             <:
-            slice u8)
+            t_Slice u8)
       in
-      let hashed:array u8 (sz 64) =
-        Hacspec_kyber.Parameters.Hash_functions.v_G (Rust_primitives.unsize to_hash <: slice u8)
+      let hashed:t_Array u8 (sz 64) =
+        Hacspec_kyber.Parameters.Hash_functions.v_G (Rust_primitives.unsize to_hash <: t_Slice u8)
       in
-      let shared_secret, pseudorandomness:(slice u8 & slice u8) =
-        Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: slice u8)
+      let shared_secret, pseudorandomness:(t_Slice u8 & t_Slice u8) =
+        Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: t_Slice u8)
           v_KYBER768_SHARED_SECRET_SIZE
       in
-      let* ciphertext:array u8 (sz 1088) =
+      let* ciphertext:t_Array u8 (sz 1088) =
         match
           Core.Ops.Try_trait.f_branch (Hacspec_kyber.Ind_cpa.encrypt public_key
                 randomness
-                (Hacspec_lib.f_as_array pseudorandomness <: array u8 (sz 32))
+                (Hacspec_lib.f_as_array pseudorandomness <: t_Array u8 (sz 32))
               <:
-              Core.Result.t_Result (array u8 (sz 1088)) t_BadRejectionSamplingRandomnessError)
+              Core.Result.t_Result (t_Array u8 (sz 1088)) t_BadRejectionSamplingRandomnessError)
         with
         | Core.Ops.Control_flow.ControlFlow_Break residual ->
           let* hoist18:Rust_primitives.Hax.t_Never =
             Core.Ops.Control_flow.ControlFlow.v_Break (Core.Ops.Try_trait.f_from_residual residual
                 <:
-                Core.Result.t_Result (array u8 (sz 1088) & array u8 (sz 32))
+                Core.Result.t_Result (t_Array u8 (sz 1088) & t_Array u8 (sz 32))
                   t_BadRejectionSamplingRandomnessError)
           in
           Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist18)
@@ -147,42 +148,45 @@ let encapsulate (public_key: array u8 (sz 1184)) (randomness: array u8 (sz 32))
       Core.Ops.Control_flow.ControlFlow_Continue
       (Core.Result.Result_Ok (ciphertext, Hacspec_lib.f_as_array shared_secret)))
 
-let decapsulate (ciphertext: array u8 (sz 1088)) (secret_key: array u8 (sz 2400)) : array u8 (sz 32) =
-  let ind_cpa_secret_key, secret_key:(slice u8 & slice u8) =
-    Core.Slice.impl__split_at (Rust_primitives.unsize secret_key <: slice u8)
+let decapsulate (ciphertext: t_Array u8 (sz 1088)) (secret_key: t_Array u8 (sz 2400))
+    : t_Array u8 (sz 32) =
+  let ind_cpa_secret_key, secret_key:(t_Slice u8 & t_Slice u8) =
+    Core.Slice.impl__split_at (Rust_primitives.unsize secret_key <: t_Slice u8)
       Hacspec_kyber.Parameters.v_CPA_PKE_SECRET_KEY_SIZE
   in
-  let ind_cpa_public_key, secret_key:(slice u8 & slice u8) =
+  let ind_cpa_public_key, secret_key:(t_Slice u8 & t_Slice u8) =
     Core.Slice.impl__split_at secret_key Hacspec_kyber.Parameters.v_CPA_PKE_PUBLIC_KEY_SIZE
   in
-  let ind_cpa_public_key_hash, implicit_rejection_value:(slice u8 & slice u8) =
+  let ind_cpa_public_key_hash, implicit_rejection_value:(t_Slice u8 & t_Slice u8) =
     Core.Slice.impl__split_at secret_key Hacspec_kyber.Parameters.Hash_functions.v_H_DIGEST_SIZE
   in
-  let decrypted:array u8 (sz 32) =
-    Hacspec_kyber.Ind_cpa.decrypt (Hacspec_lib.f_as_array ind_cpa_secret_key <: array u8 (sz 1152))
+  let decrypted:t_Array u8 (sz 32) =
+    Hacspec_kyber.Ind_cpa.decrypt (Hacspec_lib.f_as_array ind_cpa_secret_key <: t_Array u8 (sz 1152)
+      )
       ciphertext
   in
-  let (to_hash: array u8 (sz 64)):array u8 (sz 64) =
+  let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) =
     Hacspec_lib.f_push decrypted ind_cpa_public_key_hash
   in
-  let hashed:array u8 (sz 64) =
-    Hacspec_kyber.Parameters.Hash_functions.v_G (Rust_primitives.unsize to_hash <: slice u8)
+  let hashed:t_Array u8 (sz 64) =
+    Hacspec_kyber.Parameters.Hash_functions.v_G (Rust_primitives.unsize to_hash <: t_Slice u8)
   in
-  let success_shared_secret, pseudorandomness:(slice u8 & slice u8) =
-    Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: slice u8)
+  let success_shared_secret, pseudorandomness:(t_Slice u8 & t_Slice u8) =
+    Core.Slice.impl__split_at (Rust_primitives.unsize hashed <: t_Slice u8)
       v_KYBER768_SHARED_SECRET_SIZE
   in
-  let (to_hash: array u8 (sz 1120)):array u8 (sz 1120) =
-    Hacspec_lib.f_push implicit_rejection_value (Rust_primitives.unsize ciphertext <: slice u8)
+  let (to_hash: t_Array u8 (sz 1120)):t_Array u8 (sz 1120) =
+    Hacspec_lib.f_push implicit_rejection_value (Rust_primitives.unsize ciphertext <: t_Slice u8)
   in
-  let (rejection_shared_secret: array u8 (sz 32)):array u8 (sz 32) =
-    Hacspec_kyber.Parameters.Hash_functions.v_J (Rust_primitives.unsize to_hash <: slice u8)
+  let (rejection_shared_secret: t_Array u8 (sz 32)):t_Array u8 (sz 32) =
+    Hacspec_kyber.Parameters.Hash_functions.v_J (Rust_primitives.unsize to_hash <: t_Slice u8)
   in
-  let reencrypted_ciphertext:Core.Result.t_Result (array u8 (sz 1088))
+  let reencrypted_ciphertext:Core.Result.t_Result (t_Array u8 (sz 1088))
     t_BadRejectionSamplingRandomnessError =
-    Hacspec_kyber.Ind_cpa.encrypt (Hacspec_lib.f_as_array ind_cpa_public_key <: array u8 (sz 1184))
+    Hacspec_kyber.Ind_cpa.encrypt (Hacspec_lib.f_as_array ind_cpa_public_key <: t_Array u8 (sz 1184)
+      )
       decrypted
-      (Hacspec_lib.f_as_array pseudorandomness <: array u8 (sz 32))
+      (Hacspec_lib.f_as_array pseudorandomness <: t_Array u8 (sz 32))
   in
   match reencrypted_ciphertext with
   | Core.Result.Result_Ok reencrypted ->
diff --git a/specs/kyber/src/lib.rs b/specs/kyber/src/lib.rs
index c5c867b37..3fc3a0fd9 100644
--- a/specs/kyber/src/lib.rs
+++ b/specs/kyber/src/lib.rs
@@ -42,6 +42,7 @@ pub type SharedSecret = [u8; KYBER768_SHARED_SECRET_SIZE];
 #[derive(Debug)]
 pub struct BadRejectionSamplingRandomnessError;
 
+#[derive(Debug)]
 pub struct KeyPair {
     pk: PublicKey,
     sk: PrivateKey,
diff --git a/specs/kyber/tests/interop_with_libcrux.rs b/specs/kyber/tests/interop_with_libcrux.rs
index 2fe514234..2b24cb9c5 100644
--- a/specs/kyber/tests/interop_with_libcrux.rs
+++ b/specs/kyber/tests/interop_with_libcrux.rs
@@ -9,7 +9,14 @@ fn same_inputs_result_in_same_output() {
     let mut keygen_seed = [0u8; KYBER768_KEY_GENERATION_SEED_SIZE];
     OsRng.fill_bytes(&mut keygen_seed);
 
-    // TODO: Check that both rejection sample the same way.
+    let libcrux_key_pair_result = libcrux::kem::kyber768_generate_keypair_derand(keygen_seed);
+    let spec_key_pair_result = hacspec_kyber::generate_keypair(keygen_seed);
+
+    if libcrux_key_pair_result.is_err() {
+        spec_key_pair_result.expect_err("If rejection sampling failed in libcrux, it should fail in the spec as well.");
+        return
+    }
+
     let libcrux_key_pair = libcrux::kem::kyber768_generate_keypair_derand(keygen_seed).unwrap();
     let spec_key_pair = hacspec_kyber::generate_keypair(keygen_seed).unwrap();