Use $ in more fstar macros to remove hardcoded names that are not com…

…patible with new hax naming.
cryspen · Jan 29, 2025 · 4932e37 · 4932e37
1 parent 7755d48
commit 4932e37
Show file tree

Hide file tree

Showing 8 changed files with 83 additions and 69 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,15 +289,15 @@ 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);
                 }
 
                 /// 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>()
                 }