diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti
index 6ea0e7eda..97f19a565 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti
@@ -61,6 +61,9 @@ val unpack_public_key
         v_T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE v_K)
       (ensures
         fun unpacked_public_key_future ->
+          let unpacked_public_key_future:t_MlKemPublicKeyUnpacked v_K v_Vector =
+            unpacked_public_key_future
+          in
           let unpacked_public_key_future:t_MlKemPublicKeyUnpacked v_K v_Vector =
             unpacked_public_key_future
           in
@@ -70,13 +73,16 @@ val unpack_public_key
           (valid ==>
             Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
               #v_Vector
-              unpacked_public_key_future.f_ind_cpa_public_key.f_A ==
+              unpacked_public_key_future.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
             matrix_A) /\
           Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
             #v_Vector
-            unpacked_public_key_future.f_ind_cpa_public_key.f_t_as_ntt ==
-          deserialized_pk /\ unpacked_public_key_future.f_ind_cpa_public_key.f_seed_for_A == seed /\
-          unpacked_public_key_future.f_public_key_hash == public_key_hash)
+            unpacked_public_key_future.f_ind_cpa_public_key
+              .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
+          deserialized_pk /\
+          unpacked_public_key_future.f_ind_cpa_public_key
+            .Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A ==
+          seed /\ unpacked_public_key_future.f_public_key_hash == public_key_hash)
 
 /// Get the serialized public key.
 val impl_3__serialized_mut
@@ -88,26 +94,28 @@ val impl_3__serialized_mut
       (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
     : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
       (requires
-        Spec.MLKEM.is_rank v_K /\
-        v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
-        v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
-        (forall (i: nat).
-            i < v v_K ==>
-            Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
-                  i)))
+        (let self___ = self in
+          Spec.MLKEM.is_rank v_K /\
+          v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
+          v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
+          (forall (i: nat).
+              i < v v_K ==>
+              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
+                      .f_ind_cpa_public_key
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
+                    i))))
       (ensures
         fun serialized_future ->
           let serialized_future:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE =
             serialized_future
           in
+          let self___ = self in
           serialized_future.f_value ==
           Seq.append (Spec.MLKEM.vector_encode_12 #v_K
                 (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                     #v_Vector
-                    self.f_ind_cpa_public_key.f_t_as_ntt))
-            self.f_ind_cpa_public_key.f_seed_for_A)
+                    self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
+            self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)
 
 /// Get the serialized public key.
 val impl_3__serialized
@@ -118,24 +126,26 @@ val impl_3__serialized
       (self: t_MlKemPublicKeyUnpacked v_K v_Vector)
     : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
       (requires
-        Spec.MLKEM.is_rank v_K /\
-        v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
-        v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
-        (forall (i: nat).
-            i < v v_K ==>
-            Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
-                  i)))
+        (let self___ = self in
+          Spec.MLKEM.is_rank v_K /\
+          v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
+          v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
+          (forall (i: nat).
+              i < v v_K ==>
+              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
+                      .f_ind_cpa_public_key
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
+                    i))))
       (ensures
         fun res ->
           let res:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = res in
-          res.f_value ==
+          let self___ = self in
+          res.Libcrux_ml_kem.Types.f_value ==
           Seq.append (Spec.MLKEM.vector_encode_12 #v_K
                 (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                     #v_Vector
-                    self.f_ind_cpa_public_key.f_t_as_ntt))
-            self.f_ind_cpa_public_key.f_seed_for_A)
+                    self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
+            self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl
@@ -187,26 +197,30 @@ val impl_4__serialized_public_key_mut
       (serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
     : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
       (requires
-        Spec.MLKEM.is_rank v_K /\
-        v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
-        v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
-        (forall (i: nat).
-            i < v v_K ==>
-            Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
-                  i)))
+        (let self___ = self in
+          Spec.MLKEM.is_rank v_K /\
+          v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
+          v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
+          (forall (i: nat).
+              i < v v_K ==>
+              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
+                      .f_public_key
+                      .f_ind_cpa_public_key
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
+                    i))))
       (ensures
         fun serialized_future ->
           let serialized_future:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE =
             serialized_future
           in
+          let self___ = self in
           serialized_future.f_value ==
           Seq.append (Spec.MLKEM.vector_encode_12 #v_K
                 (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                     #v_Vector
-                    self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt))
-            self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)
+                    self___.f_public_key.f_ind_cpa_public_key
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
+            self___.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)
 
 /// Get the serialized public key.
 val impl_4__serialized_public_key
@@ -217,24 +231,28 @@ val impl_4__serialized_public_key
       (self: t_MlKemKeyPairUnpacked v_K v_Vector)
     : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
       (requires
-        Spec.MLKEM.is_rank v_K /\
-        v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
-        v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
-        (forall (i: nat).
-            i < v v_K ==>
-            Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
-                  i)))
+        (let self___ = self in
+          Spec.MLKEM.is_rank v_K /\
+          v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
+          v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
+          (forall (i: nat).
+              i < v v_K ==>
+              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
+                      .f_public_key
+                      .f_ind_cpa_public_key
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
+                    i))))
       (ensures
         fun res ->
           let res:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = res in
+          let self___ = self in
           res.f_value ==
           Seq.append (Spec.MLKEM.vector_encode_12 #v_K
                 (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                     #v_Vector
-                    self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt))
-            self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)
+                    self___.f_public_key.f_ind_cpa_public_key
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
+            self___.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)
 
 /// Get the serialized private key.
 val impl_4__serialized_private_key_mut
@@ -383,10 +401,10 @@ val encapsulate
               public_key.f_public_key_hash
               (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                   #v_Vector
-                  public_key.f_ind_cpa_public_key.f_t_as_ntt)
+                  public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt)
               (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
                   #v_Vector
-                  public_key.f_ind_cpa_public_key.f_A)
+                  public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A)
               randomness
           in
           ciphertext_result.f_value == ciphertext /\ shared_secret_array == shared_secret)
@@ -418,13 +436,15 @@ val decapsulate
           Spec.MLKEM.ind_cca_unpack_decapsulate v_K
             key_pair.f_public_key.f_public_key_hash
             key_pair.f_private_key.f_implicit_rejection_value
-            ciphertext.f_value
+            ciphertext.Libcrux_ml_kem.Types.f_value
             (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                 #v_Vector
-                key_pair.f_private_key.f_ind_cpa_private_key.f_secret_as_ntt)
+                key_pair.f_private_key.f_ind_cpa_private_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt)
             (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
                 #v_Vector
-                key_pair.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)
+                key_pair.f_public_key.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt)
             (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
                 #v_Vector
-                key_pair.f_public_key.f_ind_cpa_public_key.f_A))
+                key_pair.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A))
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
index cf7a49d91..baac26d0c 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
@@ -636,21 +636,27 @@ let generate_keypair_unpacked
       Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed
     in
     assert (valid ==>
-        ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key.f_t_as_ntt) ==
-          t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\
-        (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key.f_A == matrix_A_as_ntt
-        ) /\
-        ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector private_key.f_secret_as_ntt) ==
+        ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
+              #v_Vector
+              public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt) ==
+          t_as_ntt) /\ (public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A == seed_for_A) /\
+        (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
+            #v_Vector
+            public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
+          matrix_A_as_ntt) /\
+        ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
+              #v_Vector
+              private_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt) ==
           secret_as_ntt));
     assert ((forall (i: nat).
             i < v v_K ==>
             Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index private_key
-                    .f_secret_as_ntt
+                    .Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt
                   i)) /\
         (forall (i: nat).
             i < v v_K ==>
             Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                    .f_t_as_ntt
+                    .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                   i)))
   in
   private_key, public_key
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
index 4759bf3b3..2354ccac2 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
@@ -213,11 +213,17 @@ val generate_keypair_unpacked
             Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector) =
             temp_0_
           in
+          let public_key_future:Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K
+            v_Vector =
+            public_key_future
+          in
           let (((t_as_ntt, seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid =
             Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed
           in
           (valid ==>
-            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key_future.f_t_as_ntt ==
+            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
+                #v_Vector
+                public_key_future.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
               t_as_ntt) /\ (public_key_future.f_seed_for_A == seed_for_A) /\
             (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key_future.f_A ==
               matrix_A_as_ntt) /\
@@ -233,7 +239,7 @@ val generate_keypair_unpacked
           (forall (i: nat).
               i < v v_K ==>
               Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key_future
-                      .f_t_as_ntt
+                      .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                     i)))
 
 /// Serialize the secret key from the unpacked key pair generation.
@@ -354,8 +360,12 @@ val encrypt_unpacked
           Spec.MLKEM.ind_cpa_encrypt_unpacked v_K
             message
             randomness
-            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key.f_t_as_ntt)
-            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key.f_A))
+            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
+                #v_Vector
+                public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt)
+            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
+                #v_Vector
+                public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A))
 
 val build_unpacked_public_key_mut
       (v_K v_T_AS_NTT_ENCODED_SIZE: usize)
@@ -370,6 +380,10 @@ val build_unpacked_public_key_mut
         length public_key == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K)
       (ensures
         fun unpacked_public_key_future ->
+          let unpacked_public_key_future:Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked
+            v_K v_Vector =
+            unpacked_public_key_future
+          in
           let unpacked_public_key_future:Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked
             v_K v_Vector =
             unpacked_public_key_future
@@ -379,9 +393,11 @@ val build_unpacked_public_key_mut
           let matrix_A_as_ntt, valid = Spec.MLKEM.sample_matrix_A_ntt #v_K seed_for_A in
           (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
               #v_Vector
-              unpacked_public_key_future.f_t_as_ntt ==
+              unpacked_public_key_future.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
             t_as_ntt /\ valid ==>
-            Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector unpacked_public_key_future.f_A ==
+            Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
+              #v_Vector
+              unpacked_public_key_future.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
             Spec.MLKEM.matrix_transpose matrix_A_as_ntt))
 
 val build_unpacked_public_key
@@ -402,9 +418,13 @@ val build_unpacked_public_key
           let t_as_ntt_bytes, seed_for_A = split public_key v_T_AS_NTT_ENCODED_SIZE in
           let t_as_ntt = Spec.MLKEM.vector_decode_12 #v_K t_as_ntt_bytes in
           let matrix_A_as_ntt, valid = Spec.MLKEM.sample_matrix_A_ntt #v_K seed_for_A in
-          (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector result.f_t_as_ntt == t_as_ntt /\
-            valid ==>
-            Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector result.f_A ==
+          (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
+              #v_Vector
+              result.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
+            t_as_ntt /\ valid ==>
+            Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
+              #v_Vector
+              result.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
             Spec.MLKEM.matrix_transpose matrix_A_as_ntt))
 
 val encrypt
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fsti
index 89285a5c8..eebdfcedb 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fsti
@@ -34,8 +34,8 @@ val serialized_public_key
         forall (i: nat).
           i < 4 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -68,9 +68,10 @@ val key_pair_serialized_public_key_mut
       (requires
         forall (i: nat).
           i < 4 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -83,9 +84,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 4 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fsti
index 223ba7022..b59106cca 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Neon.Unpacked.fsti
@@ -38,8 +38,8 @@ val serialized_public_key
         forall (i: nat).
           i < 4 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -72,9 +72,10 @@ val key_pair_serialized_public_key_mut
       (requires
         forall (i: nat).
           i < 4 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -87,9 +88,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 4 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fsti
index 08eb4ee09..45033e1d8 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Portable.Unpacked.fsti
@@ -38,8 +38,8 @@ val serialized_public_key
         forall (i: nat).
           i < 4 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -72,9 +72,10 @@ val key_pair_serialized_public_key_mut
       (requires
         forall (i: nat).
           i < 4 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -87,9 +88,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 4 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fsti
index 79eadab70..351562191 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fsti
@@ -34,8 +34,8 @@ val serialized_public_key
         forall (i: nat).
           i < 2 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -68,9 +68,10 @@ val key_pair_serialized_public_key_mut
       (requires
         forall (i: nat).
           i < 2 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -83,9 +84,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 2 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fsti
index 0d78e304b..654e7f647 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fsti
@@ -38,8 +38,8 @@ val serialized_public_key
         forall (i: nat).
           i < 2 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -72,9 +72,10 @@ val key_pair_serialized_public_key_mut
       (requires
         forall (i: nat).
           i < 2 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -87,9 +88,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 2 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fsti
index 8b44e885d..0971ec8be 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fsti
@@ -38,8 +38,8 @@ val serialized_public_key
         forall (i: nat).
           i < 2 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -72,9 +72,10 @@ val key_pair_serialized_public_key_mut
       (requires
         forall (i: nat).
           i < 2 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -87,9 +88,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 2 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fsti
index 63c57415e..39a6dac29 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Avx2.Unpacked.fsti
@@ -34,8 +34,8 @@ val serialized_public_key
         forall (i: nat).
           i < 3 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -69,9 +69,9 @@ val key_pair_serialized_public_key_mut
         (forall (i: nat).
             i < 3 ==>
             Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
-                    .f_public_key
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
+                    .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                    .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                    .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                   i)))
       (fun _ -> Prims.l_True)
 
@@ -84,9 +84,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 3 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fsti
index 0aa06a36b..12d585a78 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Neon.Unpacked.fsti
@@ -39,8 +39,8 @@ val serialized_public_key
         forall (i: nat).
           i < 3 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -74,9 +74,9 @@ val key_pair_serialized_public_key_mut
         (forall (i: nat).
             i < 3 ==>
             Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
-                    .f_public_key
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
+                    .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                    .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                    .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                   i)))
       (fun _ -> Prims.l_True)
 
@@ -89,9 +89,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 3 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fsti
index edc6849b2..961c4e8c8 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem768.Portable.Unpacked.fsti
@@ -39,8 +39,8 @@ val serialized_public_key
         forall (i: nat).
           i < 3 ==>
           Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
@@ -74,9 +74,9 @@ val key_pair_serialized_public_key_mut
         (forall (i: nat).
             i < 3 ==>
             Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
-                    .f_public_key
-                    .f_ind_cpa_public_key
-                    .f_t_as_ntt
+                    .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                    .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                    .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                   i)))
       (fun _ -> Prims.l_True)
 
@@ -89,9 +89,10 @@ val key_pair_serialized_public_key
       (requires
         forall (i: nat).
           i < 3 ==>
-          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
-                  .f_ind_cpa_public_key
-                  .f_t_as_ntt
+          Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
+                  .Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
+                  .Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
                 i))
       (fun _ -> Prims.l_True)
 
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.Unpacked.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.Unpacked.fsti
deleted file mode 100644
index 1910c0b08..000000000
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.Unpacked.fsti
+++ /dev/null
@@ -1,48 +0,0 @@
-module Libcrux_ml_kem.Types.Unpacked
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
-open FStar.Mul
-
-let _ =
-  (* This module has implicit dependencies, here we make them explicit. *)
-  (* The implicit dependencies arise from typeclasses instances. *)
-  let open Libcrux_ml_kem.Vector.Traits in
-  ()
-
-/// An unpacked ML-KEM IND-CPA Private Key
-type t_IndCpaPrivateKeyUnpacked
-  (v_K: usize) (v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-  = { f_secret_as_ntt:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K }
-
-/// An unpacked ML-KEM IND-CPA Private Key
-type t_IndCpaPublicKeyUnpacked
-  (v_K: usize) (v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-  = {
-  f_t_as_ntt:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K;
-  f_seed_for_A:t_Array u8 (sz 32);
-  f_A:t_Array (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K) v_K
-}
-
-/// An unpacked ML-KEM IND-CCA Private Key
-type t_MlKemPrivateKeyUnpacked
-  (v_K: usize) (v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-  = {
-  f_ind_cpa_private_key:t_IndCpaPrivateKeyUnpacked v_K v_Vector;
-  f_implicit_rejection_value:t_Array u8 (sz 32)
-}
-
-/// An unpacked ML-KEM IND-CCA Private Key
-type t_MlKemPublicKeyUnpacked
-  (v_K: usize) (v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-  = {
-  f_ind_cpa_public_key:t_IndCpaPublicKeyUnpacked v_K v_Vector;
-  f_public_key_hash:t_Array u8 (sz 32)
-}
-
-/// An unpacked ML-KEM KeyPair
-type t_MlKemKeyPairUnpacked
-  (v_K: usize) (v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
-  = {
-  f_private_key:t_MlKemPrivateKeyUnpacked v_K v_Vector;
-  f_public_key:t_MlKemPublicKeyUnpacked v_K v_Vector
-}
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Portable.fsti
deleted file mode 100644
index fe64003c4..000000000
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Portable.fsti
+++ /dev/null
@@ -1,30 +0,0 @@
-module Libcrux_ml_kem.Vector.Avx2.Portable
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-open Core
-open FStar.Mul
-
-val deserialize_11_int (bytes: t_Slice u8)
-    : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
-
-val serialize_11_int (v: t_Slice i16)
-    : Prims.Pure (u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
-
-type t_PortableVector = { f_elements:t_Array i16 (sz 16) }
-
-val from_i16_array (array: t_Array i16 (sz 16))
-    : Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True)
-
-val serialize_11_ (v: t_PortableVector)
-    : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True)
-
-val to_i16_array (v: t_PortableVector)
-    : Prims.Pure (t_Array i16 (sz 16)) Prims.l_True (fun _ -> Prims.l_True)
-
-val zero: Prims.unit -> Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True)
-
-val deserialize_11_ (bytes: t_Slice u8)
-    : Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.Edited.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.Edited.fsti
deleted file mode 100644
index 4ed69770d..000000000
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Serialize.Edited.fsti
+++ /dev/null
@@ -1,100 +0,0 @@
-module Libcrux_ml_kem.Vector.Portable.Serialize.Edited
-// #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
-// open Core
-// open FStar.Mul
-
-// val deserialize_10_int (bytes: t_Slice u8)
-//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_11_int (bytes: t_Slice u8)
-//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_12_int (bytes: t_Slice u8)
-//     : Prims.Pure (i16 & i16) Prims.l_True (fun _ -> Prims.l_True)
-
-// val deserialize_4_int (bytes: t_Slice u8)
-//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_5_int (bytes: t_Slice u8)
-//     : Prims.Pure (i16 & i16 & i16 & i16 & i16 & i16 & i16 & i16)
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val serialize_10_int (v: t_Slice i16)
-//     : Prims.Pure (u8 & u8 & u8 & u8 & u8)
-//       (requires (Core.Slice.impl__len #i16 v <: usize) =. sz 4)
-//       (ensures
-//         fun tuple ->
-//           let tuple:(u8 & u8 & u8 & u8 & u8) = tuple in
-//           BitVecEq.int_t_array_bitwise_eq' (v <: t_Array i16 (sz 4)) 10 (MkSeq.create5 tuple) 8)
-
-// val serialize_11_int (v: t_Slice i16)
-//     : Prims.Pure (u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8)
-//       (requires Seq.length v == 8 /\ (forall i. Rust_primitives.bounded (Seq.index v i) 11))
-//       (ensures
-//         fun tuple ->
-//           let tuple:(u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8 & u8) = tuple in
-//           BitVecEq.int_t_array_bitwise_eq' (v <: t_Array i16 (sz 8)) 11 (MkSeq.create11 tuple) 8)
-
-// val serialize_12_int (v: t_Slice i16)
-//     : Prims.Pure (u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_4_int (v: t_Slice i16)
-//     : Prims.Pure (u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_5_int (v: t_Slice i16)
-//     : Prims.Pure (u8 & u8 & u8 & u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-//     : Prims.Pure (t_Array u8 (sz 2)) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_10_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-//     : Prims.Pure (t_Array u8 (sz 20)) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_11_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-//     : Prims.Pure (t_Array u8 (sz 22)) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_12_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-//     : Prims.Pure (t_Array u8 (sz 24)) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_4_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-//     : Prims.Pure (t_Array u8 (sz 8)) Prims.l_True (fun _ -> Prims.l_True)
-
-// val serialize_5_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
-//     : Prims.Pure (t_Array u8 (sz 10)) Prims.l_True (fun _ -> Prims.l_True)
-
-// val deserialize_1_ (v: t_Slice u8)
-//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_10_ (bytes: t_Slice u8)
-//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_11_ (bytes: t_Slice u8)
-//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_12_ (bytes: t_Slice u8)
-//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_4_ (bytes: t_Slice u8)
-//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
-
-// val deserialize_5_ (bytes: t_Slice u8)
-//     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-//       Prims.l_True
-//       (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/src/constant_time_ops.rs b/libcrux-ml-kem/src/constant_time_ops.rs
index 649be46ae..e2390dccf 100644
--- a/libcrux-ml-kem/src/constant_time_ops.rs
+++ b/libcrux-ml-kem/src/constant_time_ops.rs
@@ -23,9 +23,9 @@ fn inz(value: u8) -> u8 {
         assert($value == zero);
         lognot_lemma $value;
         assert((~.$value +. (mk_u16 1)) == zero);
-        assert((Core.Num.impl__u16__wrapping_add (~.$value <: u16) (mk_u16 1) <: u16) == zero);
+        assert(($u16::wrapping_add (~.$value <: u16) (mk_u16 1) <: u16) == zero);
         logor_lemma $value zero;
-        assert(($value |. (Core.Num.impl__u16__wrapping_add (~.$value <: u16) (mk_u16 1) <: u16) <: u16) == $value);
+        assert(($value |. ($u16::wrapping_add (~.$value <: u16) (mk_u16 1) <: u16) <: u16) == $value);
         assert (v $result == v (($value >>! (mk_i32 8))));
         assert ((v $value / pow2 8) == 0);
         assert ($result == (mk_u8 0));
@@ -40,7 +40,7 @@ fn inz(value: u8) -> u8 {
         assert ((v (~.$value) + 1) = (pow2 16 - pow2 8) + (pow2 8 - v $value));
         assert ((v (~.$value) + 1) = (pow2 8 - 1) * pow2 8 + (pow2 8 - v $value));
         assert ((v (~.$value) + 1)/pow2 8 = (pow2 8 - 1));
-        assert (v ((Core.Num.impl__u16__wrapping_add (~.$value <: u16) (mk_u16 1) <: u16) >>! (mk_i32 8)) = pow2 8 - 1);
+        assert (v (($u16::wrapping_add (~.$value <: u16) (mk_u16 1) <: u16) >>! (mk_i32 8)) = pow2 8 - 1);
         assert ($result = ones);
         logand_lemma (mk_u8 1) $result;
         assert ($res = (mk_u8 1)))"#
diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs
index 916ff78a3..955ed5e77 100644
--- a/libcrux-ml-kem/src/ind_cca.rs
+++ b/libcrux-ml-kem/src/ind_cca.rs
@@ -487,13 +487,14 @@ pub(crate) mod unpacked {
         $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\
         $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K"#)
     )]
-    #[hax_lib::ensures(|result|
-        fstar!(r#"let (public_key_hash, (seed, (deserialized_pk, (matrix_A, valid)))) =
+    #[hax_lib::ensures(|result| {
+        let unpacked_public_key_future = future(unpacked_public_key);
+        {fstar!(r#"let (public_key_hash, (seed, (deserialized_pk, (matrix_A, valid)))) =
             Spec.MLKEM.ind_cca_unpack_public_key $K ${public_key}.f_value in (valid ==>
-            Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_A == matrix_A) /\
-        Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key}_future.f_ind_cpa_public_key.f_t_as_ntt == deserialized_pk /\
-        ${unpacked_public_key}_future.f_ind_cpa_public_key.f_seed_for_A == seed /\
-        ${unpacked_public_key}_future.f_public_key_hash == public_key_hash"#))
+            Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key_future.ind_cpa_public_key.A} == matrix_A) /\
+        Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key_future.ind_cpa_public_key.t_as_ntt} == deserialized_pk /\
+        ${unpacked_public_key_future.ind_cpa_public_key.seed_for_A} == seed /\
+        ${unpacked_public_key_future.public_key_hash} == public_key_hash"#)}})
     ]
     #[inline(always)]
     pub(crate) fn unpack_public_key<
@@ -531,18 +532,20 @@ pub(crate) mod unpacked {
     impl<const K: usize, Vector: Operations> MlKemPublicKeyUnpacked<K, Vector> {
         /// Get the serialized public key.
         #[inline(always)]
-        #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
+        #[requires(fstar!(r#"let ${self_} = self in
+        Spec.MLKEM.is_rank $K /\
             $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\
             $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\
             (forall (i:nat). i < v $K ==>
                 Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                    self.f_ind_cpa_public_key.f_t_as_ntt i))"#))]
+                    ${self_.ind_cpa_public_key.t_as_ntt} i))"#))]
         #[ensures(|_|
-            fstar!(r#"${serialized}_future.f_value == 
+            fstar!(r#"let ${self_} = self in            
+            ${serialized}_future.f_value == 
                 Seq.append (Spec.MLKEM.vector_encode_12 #$K
                     (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector
-                        self.f_ind_cpa_public_key.f_t_as_ntt))
-                self.f_ind_cpa_public_key.f_seed_for_A)"#)
+                        ${self_.ind_cpa_public_key.t_as_ntt}))
+                ${self_.ind_cpa_public_key.seed_for_A})"#)
         )]
         pub fn serialized_mut<
             const RANKED_BYTES_PER_RING_ELEMENT: usize,
@@ -560,17 +563,19 @@ pub(crate) mod unpacked {
 
         /// Get the serialized public key.
         #[inline(always)]
-        #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
+        #[requires(fstar!(r#"let ${self_} = self in
+        Spec.MLKEM.is_rank $K /\
             $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\
             $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\
             (forall (i:nat). i < v $K ==>
                 Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index
-                    self.f_ind_cpa_public_key.f_t_as_ntt i))"#))]
+                    ${self_.ind_cpa_public_key.t_as_ntt} i))"#))]
         #[ensures(|res|
-            fstar!(r#"${res}.f_value == Seq.append (Spec.MLKEM.vector_encode_12 #$K
+            fstar!(r#"let ${self_} = self in
+            ${res.value} == Seq.append (Spec.MLKEM.vector_encode_12 #$K
                             (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector
-                                self.f_ind_cpa_public_key.f_t_as_ntt))
-                        self.f_ind_cpa_public_key.f_seed_for_A)"#)
+                                ${self_.ind_cpa_public_key.t_as_ntt}))
+                        ${self_.ind_cpa_public_key.seed_for_A})"#)
         )]
         pub fn serialized<
             const RANKED_BYTES_PER_RING_ELEMENT: usize,
@@ -696,18 +701,20 @@ pub(crate) mod unpacked {
 
         /// Get the serialized public key.
         #[inline(always)]
-        #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
+        #[requires(fstar!(r#"let ${self_} = self in
+        Spec.MLKEM.is_rank $K /\
             $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\
             $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\
             (forall (i:nat). i < v $K ==>
                 Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                    self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"#))]
+                    ${self_.public_key.ind_cpa_public_key.t_as_ntt} i))"#))]
         #[ensures(|_|
-            fstar!(r#"${serialized}_future.f_value == 
+            fstar!(r#"let ${self_} = self in
+            ${serialized}_future.f_value == 
                 Seq.append (Spec.MLKEM.vector_encode_12 #$K
                     (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector
-                        self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt))
-                self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)"#)
+                        ${self_.public_key.ind_cpa_public_key.t_as_ntt}))
+                ${self_.public_key.ind_cpa_public_key.seed_for_A})"#)
         )]
         pub fn serialized_public_key_mut<
             const RANKED_BYTES_PER_RING_ELEMENT: usize,
@@ -722,17 +729,19 @@ pub(crate) mod unpacked {
 
         /// Get the serialized public key.
         #[inline(always)]
-        #[requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
+        #[requires(fstar!(r#"let ${self_} = self in
+        Spec.MLKEM.is_rank $K /\
             $RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT $K /\
             $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\
             (forall (i:nat). i < v $K ==>
                 Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index
-                    self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"#))]
+                    ${self_.public_key.ind_cpa_public_key.t_as_ntt} i))"#))]
         #[ensures(|res|
-            fstar!(r#"${res}.f_value == Seq.append (Spec.MLKEM.vector_encode_12 #$K
+            fstar!(r#"let ${self_} = self in
+            ${res}.f_value == Seq.append (Spec.MLKEM.vector_encode_12 #$K
                             (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector
-                                self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt))
-                        self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)"#)
+                                ${self_.public_key.ind_cpa_public_key.t_as_ntt}))
+                        ${self_.public_key.ind_cpa_public_key.seed_for_A})"#)
         )]
         pub fn serialized_public_key<
             const RANKED_BYTES_PER_RING_ELEMENT: usize,
@@ -961,8 +970,8 @@ pub(crate) mod unpacked {
     #[hax_lib::ensures(|(ciphertext_result, shared_secret_array)|
         fstar!(r#"let (ciphertext, shared_secret) =
             Spec.MLKEM.ind_cca_unpack_encapsulate $K ${public_key}.f_public_key_hash
-            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}.f_ind_cpa_public_key.f_t_as_ntt)
-            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}.f_ind_cpa_public_key.f_A)
+            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key.ind_cpa_public_key.t_as_ntt})
+            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key.ind_cpa_public_key.A})
             $randomness in
         ${ciphertext_result}.f_value == ciphertext /\
         $shared_secret_array == shared_secret"#))
@@ -1039,12 +1048,12 @@ pub(crate) mod unpacked {
         $IMPLICIT_REJECTION_HASH_INPUT_SIZE == Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE $K"#))]
     #[hax_lib::ensures(|result|
         fstar!(r#"$result ==
-            Spec.MLKEM.ind_cca_unpack_decapsulate $K ${key_pair}.f_public_key.f_public_key_hash
-            ${key_pair}.f_private_key.f_implicit_rejection_value
-            ${ciphertext}.f_value
-            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${key_pair}.f_private_key.f_ind_cpa_private_key.f_secret_as_ntt)
-            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)
-            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${key_pair}.f_public_key.f_ind_cpa_public_key.f_A)"#))
+            Spec.MLKEM.ind_cca_unpack_decapsulate $K ${key_pair.public_key.public_key_hash}
+            ${key_pair.private_key.implicit_rejection_value}
+            ${ciphertext.value}
+            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${key_pair.private_key.ind_cpa_private_key.secret_as_ntt})
+            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${key_pair.public_key.ind_cpa_public_key.t_as_ntt})
+            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${key_pair.public_key.ind_cpa_public_key.A})"#))
     ]
     pub(crate) fn decapsulate<
         const K: usize,
diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
index 5c41ca234..489a15cdb 100644
--- a/libcrux-ml-kem/src/ind_cpa.rs
+++ b/libcrux-ml-kem/src/ind_cpa.rs
@@ -470,16 +470,19 @@ fn sample_vector_cbd_then_ntt_out<
     $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\
     $ETA1 == Spec.MLKEM.v_ETA1 $K /\
     length $key_generation_seed == Spec.MLKEM.v_CPA_KEY_GENERATION_SEED_SIZE"#))]
-#[hax_lib::ensures(|_| fstar!(r#"let ((((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid) = Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in 
-    (valid ==> (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}_future.f_t_as_ntt == t_as_ntt) /\
+#[hax_lib::ensures(|_|
+    {
+    let public_key_future = future(public_key);
+    {fstar!(r#"let ((((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid) = Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in 
+    (valid ==> (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key_future.t_as_ntt} == t_as_ntt) /\
         (${public_key}_future.f_seed_for_A == seed_for_A) /\
         (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}_future.f_A == matrix_A_as_ntt) /\
         (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${private_key}_future.f_secret_as_ntt == secret_as_ntt)) /\
     (forall (i:nat). i < v $K ==>
         Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${private_key}_future.f_secret_as_ntt i)) /\
     (forall (i:nat). i < v $K ==>
-        Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${public_key}_future.f_t_as_ntt i))
-"#))]
+        Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${public_key_future.t_as_ntt} i))
+"#)}})]
 #[inline(always)]
 pub(crate) fn generate_keypair_unpacked<
     const K: usize,
@@ -537,15 +540,15 @@ pub(crate) fn generate_keypair_unpacked<
         r#"let (((t_as_ntt,seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid =
         Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in
         assert (valid ==>
-            ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector public_key.f_t_as_ntt) ==
-              t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\
-            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector public_key.f_A == matrix_A_as_ntt) /\
-            ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector private_key.f_secret_as_ntt) ==
+            ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key.t_as_ntt}) ==
+              t_as_ntt) /\ (${public_key.seed_for_A} == seed_for_A) /\
+            (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key.A} == matrix_A_as_ntt) /\
+            ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${private_key.secret_as_ntt}) ==
               secret_as_ntt));
         assert ((forall (i: nat). i < v $K ==>
-              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index private_key.f_secret_as_ntt i)) /\
+              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${private_key.secret_as_ntt} i)) /\
           (forall (i: nat). i < v $K ==>
-              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key.f_t_as_ntt i)))"#
+              Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${public_key.t_as_ntt} i)))"#
     );
 
     // For encapsulation, we need to store A not Aˆ, and so we untranspose A
@@ -740,8 +743,8 @@ fn compress_then_serialize_u<
       length $randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE"#))]
 #[hax_lib::ensures(|result|
     fstar!(r#"$result == Spec.MLKEM.ind_cpa_encrypt_unpacked $K $message $randomness
-        (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}.f_t_as_ntt)
-        (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}.f_A)"#)
+        (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key.t_as_ntt})
+        (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key.A})"#)
 )]
 #[inline(always)]
 pub(crate) fn encrypt_unpacked<
@@ -909,8 +912,8 @@ pub(crate) fn encrypt<
     let (t_as_ntt_bytes, seed_for_A) = split public_key $T_AS_NTT_ENCODED_SIZE in
     let t_as_ntt = Spec.MLKEM.vector_decode_12 #$K t_as_ntt_bytes in 
     let matrix_A_as_ntt, valid = Spec.MLKEM.sample_matrix_A_ntt #$K seed_for_A in
-    (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${result}.f_t_as_ntt == t_as_ntt /\
-     valid ==> Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${result}.f_A == Spec.MLKEM.matrix_transpose matrix_A_as_ntt)"#))]
+    (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${result.t_as_ntt} == t_as_ntt /\
+     valid ==> Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${result.A} == Spec.MLKEM.matrix_transpose matrix_A_as_ntt)"#))]
 fn build_unpacked_public_key<
     const K: usize,
     const T_AS_NTT_ENCODED_SIZE: usize,
@@ -931,12 +934,14 @@ fn build_unpacked_public_key<
 #[hax_lib::requires(fstar!(r#"Spec.MLKEM.is_rank $K /\
     $T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE $K /\
     length $public_key == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K"#))]
-#[hax_lib::ensures(|_| fstar!(r#"
+#[hax_lib::ensures(|_| {
+    let unpacked_public_key_future = future(unpacked_public_key);
+    {fstar!(r#"
     let (t_as_ntt_bytes, seed_for_A) = split public_key $T_AS_NTT_ENCODED_SIZE in
     let t_as_ntt = Spec.MLKEM.vector_decode_12 #$K t_as_ntt_bytes in 
     let matrix_A_as_ntt, valid = Spec.MLKEM.sample_matrix_A_ntt #$K seed_for_A in
-    (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key}_future.f_t_as_ntt == t_as_ntt /\
-    valid ==> Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key}_future.f_A == Spec.MLKEM.matrix_transpose matrix_A_as_ntt)"#))]
+    (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${unpacked_public_key_future.t_as_ntt} == t_as_ntt /\
+    valid ==> Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${unpacked_public_key_future.A} == Spec.MLKEM.matrix_transpose matrix_A_as_ntt)"#)}})]
 pub(crate) fn build_unpacked_public_key_mut<
     const K: usize,
     const T_AS_NTT_ENCODED_SIZE: usize,
diff --git a/libcrux-ml-kem/src/mlkem1024.rs b/libcrux-ml-kem/src/mlkem1024.rs
index 7976f095e..ca8dacc76 100644
--- a/libcrux-ml-kem/src/mlkem1024.rs
+++ b/libcrux-ml-kem/src/mlkem1024.rs
@@ -265,7 +265,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 4 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${public_key}.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn serialized_public_key(
                     public_key: &MlKem1024PublicKeyUnpacked,
                     serialized: &mut MlKem1024PublicKey,
@@ -289,7 +289,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 4 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${key_pair.public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn key_pair_serialized_public_key_mut(key_pair: &MlKem1024KeyPairUnpacked, serialized: &mut MlKem1024PublicKey) {
                     key_pair.serialized_public_key_mut::<RANKED_BYTES_PER_RING_ELEMENT_1024, CPA_PKE_PUBLIC_KEY_SIZE_1024>(serialized);
                 }
@@ -297,7 +297,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 4 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${key_pair.public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn key_pair_serialized_public_key(key_pair: &MlKem1024KeyPairUnpacked) ->MlKem1024PublicKey {
                     key_pair.serialized_public_key::<RANKED_BYTES_PER_RING_ELEMENT_1024, CPA_PKE_PUBLIC_KEY_SIZE_1024>()
                 }
diff --git a/libcrux-ml-kem/src/mlkem512.rs b/libcrux-ml-kem/src/mlkem512.rs
index 52cfa2543..c5d253310 100644
--- a/libcrux-ml-kem/src/mlkem512.rs
+++ b/libcrux-ml-kem/src/mlkem512.rs
@@ -255,7 +255,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 2 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${public_key}.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn serialized_public_key(
                     public_key: &MlKem512PublicKeyUnpacked,
                     serialized: &mut MlKem512PublicKey,
@@ -279,7 +279,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 2 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${key_pair.public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn key_pair_serialized_public_key_mut(key_pair: &MlKem512KeyPairUnpacked, serialized: &mut MlKem512PublicKey) {
                     key_pair.serialized_public_key_mut::<RANKED_BYTES_PER_RING_ELEMENT_512, CPA_PKE_PUBLIC_KEY_SIZE_512>(serialized);
                 }
@@ -287,7 +287,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 2 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${key_pair.public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn key_pair_serialized_public_key(key_pair: &MlKem512KeyPairUnpacked) ->MlKem512PublicKey {
                     key_pair.serialized_public_key::<RANKED_BYTES_PER_RING_ELEMENT_512, CPA_PKE_PUBLIC_KEY_SIZE_512>()
                 }
diff --git a/libcrux-ml-kem/src/mlkem768.rs b/libcrux-ml-kem/src/mlkem768.rs
index a96c83304..25ad7ed28 100644
--- a/libcrux-ml-kem/src/mlkem768.rs
+++ b/libcrux-ml-kem/src/mlkem768.rs
@@ -256,7 +256,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 3 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${public_key}.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn serialized_public_key(public_key: &MlKem768PublicKeyUnpacked, serialized : &mut MlKem768PublicKey) {
                     public_key.serialized_mut::<RANKED_BYTES_PER_RING_ELEMENT_768, CPA_PKE_PUBLIC_KEY_SIZE_768>(serialized);
                 }
@@ -274,7 +274,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"(forall (i:nat). i < 3 ==>
                         Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                            ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i))"#))]
+                            ${key_pair.public_key.ind_cpa_public_key.t_as_ntt} i))"#))]
                 pub fn key_pair_serialized_public_key_mut(key_pair: &MlKem768KeyPairUnpacked, serialized: &mut MlKem768PublicKey) {
                     key_pair.serialized_public_key_mut::<RANKED_BYTES_PER_RING_ELEMENT_768, CPA_PKE_PUBLIC_KEY_SIZE_768>(serialized);
                 }
@@ -282,7 +282,7 @@ macro_rules! instantiate {
                 /// Get the serialized public key.
                 #[hax_lib::requires(fstar!(r#"forall (i:nat). i < 3 ==>
                     Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index 
-                        ${key_pair}.f_public_key.f_ind_cpa_public_key.f_t_as_ntt i)"#))]
+                        ${key_pair.public_key.ind_cpa_public_key.t_as_ntt} i)"#))]
                 pub fn key_pair_serialized_public_key(key_pair: &MlKem768KeyPairUnpacked) ->MlKem768PublicKey {
                     key_pair.serialized_public_key::<RANKED_BYTES_PER_RING_ELEMENT_768, CPA_PKE_PUBLIC_KEY_SIZE_768>()
                 }
diff --git a/libcrux-ml-kem/src/types.rs b/libcrux-ml-kem/src/types.rs
index f20498185..0f47d2555 100644
--- a/libcrux-ml-kem/src/types.rs
+++ b/libcrux-ml-kem/src/types.rs
@@ -13,7 +13,7 @@ macro_rules! impl_generic_struct {
 
         #[hax_lib::attributes]
         impl<const SIZE: usize> AsRef<[u8]> for $name<SIZE> {
-            #[ensures(|result| fstar!(r#"$result = self___.f_value"#))]
+            #[ensures(|result| fstar!(r#"$result = ${self_}.f_value"#))]
             fn as_ref(&self) -> &[u8] {
                 &self.value
             }
diff --git a/libcrux-ml-kem/src/vector/avx2/sampling.rs b/libcrux-ml-kem/src/vector/avx2/sampling.rs
index f8320e1d0..6302fb3be 100644
--- a/libcrux-ml-kem/src/vector/avx2/sampling.rs
+++ b/libcrux-ml-kem/src/vector/avx2/sampling.rs
@@ -34,12 +34,12 @@ pub(crate) fn rejection_sample(input: &[u8], output: &mut [i16]) -> usize {
     hax_lib::fstar!(
         r#"assert (v (cast (${good}.[ sz 0 ] <: u8) <: usize) < 256);
         assert (v (cast (${good}.[ sz 1 ] <: u8) <: usize) < 256);
-        // We need to provide a definition or post-condition for Core.Num.impl__u8__count_ones
-        assume (v (cast (Core.Num.impl__u8__count_ones ${good}.[ sz 0 ]) <: usize) <= 8);
-        assume (v (cast (Core.Num.impl__u8__count_ones ${good}.[ sz 1 ]) <: usize) <= 8);
+        // We need to provide a definition or post-condition for ${u8::count_ones}
+        assume (v (cast (${u8::count_ones} ${good}.[ sz 0 ]) <: usize) <= 8);
+        assume (v (cast (${u8::count_ones} ${good}.[ sz 1 ]) <: usize) <= 8);
         assume (Core.Ops.Index.f_index_pre output ({
-                    Core.Ops.Range.f_start = cast (Core.Num.impl__u8__count_ones ${good}.[ sz 0 ]) <: usize;
-                    Core.Ops.Range.f_end = (cast (Core.Num.impl__u8__count_ones ${good}.[ sz 0 ]) <: usize) +! sz 8 }))"#
+                    Core.Ops.Range.f_start = cast (${u8::count_ones} ${good}.[ sz 0 ]) <: usize;
+                    Core.Ops.Range.f_end = (cast (${u8::count_ones} ${good}.[ sz 0 ]) <: usize) +! sz 8 }))"#
     );
 
     // Each bit (and its corresponding position) represents an element we