Add spec for Ind_cpa unpacked functions

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst

@@ -101,8 +101,6 @@ let sample_ring_element_cbd
   let _:Prims.unit = admit () (* Panic freedom *) in
   result
 
-#push-options "--admit_smt_queries true"
-
 let sample_vector_cbd_then_ntt
       (v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)
       (#v_Vector #v_Hasher: Type0)
@@ -185,13 +183,13 @@ let sample_vector_cbd_then_ntt
           in
           re_as_ntt)
   in
-  let hax_temp_output:u8 = domain_separator in
+  let result:u8 = domain_separator in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  let hax_temp_output:u8 = result in
   re_as_ntt, hax_temp_output
   <:
   (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
 
-#pop-options
-
 let sample_vector_cbd_then_ntt_out
       (v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)
       (#v_Vector #v_Hasher: Type0)
@@ -577,7 +575,11 @@ let decrypt_unpacked
       secret_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt
       u_as_ntt
   in
-  Libcrux_ml_kem.Serialize.compress_then_serialize_message #v_Vector message
+  let result:t_Array u8 (sz 32) =
+    Libcrux_ml_kem.Serialize.compress_then_serialize_message #v_Vector message
+  in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 let decrypt
       (v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
@@ -717,7 +719,9 @@ let encrypt_unpacked
         <:
         t_Slice u8)
   in
-  ciphertext
+  let result:t_Array u8 v_CIPHERTEXT_SIZE = ciphertext in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 #pop-options
 

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti

@@ -23,8 +23,17 @@ val sample_ring_element_cbd
     : Prims.Pure (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
       (requires
         Spec.MLKEM.is_rank v_K /\ v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\
-        v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\ range (v domain_separator + v v_K) u8_inttype)
-      (fun _ -> Prims.l_True)
+        v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\ v domain_separator < 2 * v v_K /\
+        range (v domain_separator + v v_K) u8_inttype)
+      (ensures
+        fun temp_0_ ->
+          let err1, ds:(t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K &
+            u8) =
+            temp_0_
+          in
+          v ds == v domain_separator + v v_K /\
+          Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector err1 ==
+          Spec.MLKEM.sample_vector_cbd1 #v_K (Seq.slice prf_input 0 32) (sz (v domain_separator)))
 
 /// Sample a vector of ring elements from a centered binomial distribution and
 /// convert them into their NTT representations.
@@ -233,7 +242,13 @@ val decrypt_unpacked
         v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\
         v_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
         v_VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE v_K)
-      (fun _ -> Prims.l_True)
+      (ensures
+        fun result ->
+          let result:t_Array u8 (sz 32) = result in
+          result ==
+          Spec.MLKEM.ind_cpa_decrypt_unpacked v_K
+            ciphertext
+            (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector secret_key.f_secret_as_ntt))
 
 val decrypt
       (v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
@@ -310,7 +325,15 @@ val encrypt_unpacked
         v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\
         v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\
         length randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE)
-      (fun _ -> Prims.l_True)
+      (ensures
+        fun result ->
+          let result:t_Array u8 v_CIPHERTEXT_SIZE = result in
+          result ==
+          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))
 
 val encrypt
       (v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_LEN v_C2_LEN v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR v_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE:
@@ -396,6 +419,14 @@ val generate_keypair_unpacked
             Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector) =
             temp_0_
           in
+          let ((t_as_ntt, seed_for_A), 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.f_t_as_ntt) ==
+              t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\
+            ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector private_key.f_secret_as_ntt) ==
+              secret_as_ntt)) /\
           (forall (i: nat).
               i < v v_K ==>
               Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index private_key_future

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fsti

@@ -17,12 +17,12 @@ val inv_ntt_layer_int_vec_step_reduce
     : Prims.Pure (v_Vector & v_Vector)
       (requires
         Spec.Utils.is_i16b 1664 zeta_r /\
-        (forall i.
+        (forall (i: nat).
             i < 16 ==>
             Spec.Utils.is_intb (pow2 15 - 1)
               (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array b) i) -
                 v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i))) /\
-        (forall i.
+        (forall (i: nat).
             i < 16 ==>
             Spec.Utils.is_intb (pow2 15 - 1)
               (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) +

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti

@@ -18,12 +18,12 @@ val ntt_layer_int_vec_step
       (requires
         Spec.Utils.is_i16b 1664 zeta_r /\
         (let t = Libcrux_ml_kem.Vector.Traits.montgomery_multiply_fe b zeta_r in
-          (forall i.
+          (forall (i: nat).
               i < 16 ==>
               Spec.Utils.is_intb (pow2 15 - 1)
                 (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) -
                   v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))) /\
-          (forall i.
+          (forall (i: nat).
               i < 16 ==>
               Spec.Utils.is_intb (pow2 15 - 1)
                 (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) +
@@ -131,15 +131,15 @@ val ntt_at_layer_4_plus
    let ntt_layer_7_pre (#v_Vector: Type0)
         {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
         (re_0 re_1: v_Vector) =
-    (forall i. i < 16 ==>
+    (forall (i:nat). i < 16 ==>
       Spec.Utils.is_intb (pow2 15 - 1)
       (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_1) i) * v (-1600s))) /\
     (let t = Libcrux_ml_kem.Vector.Traits.f_multiply_by_constant re_1 (-1600s) in
-    (forall i. i < 16 ==> 
+    (forall (i:nat). i < 16 ==> 
       Spec.Utils.is_intb (pow2 15 - 1) 
         (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) - 
           v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))) /\
-    (forall i. i < 16 ==> 
+    (forall (i:nat). i < 16 ==> 
       Spec.Utils.is_intb (pow2 15 - 1) 
         (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) + 
           v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))))
@@ -150,7 +150,7 @@ val ntt_at_layer_7_
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (requires
-        forall i.
+        forall (i: nat).
           i < 8 ==>
           ntt_layer_7_pre (re.f_coefficients.[ sz i ]) (re.f_coefficients.[ sz i +! sz 8 ]))
       (fun _ -> Prims.l_True)
@@ -161,7 +161,7 @@ val ntt_binomially_sampled_ring_element
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (requires
-        forall i.
+        forall (i: nat).
           i < 8 ==>
           ntt_layer_7_pre (re.f_coefficients.[ sz i ]) (re.f_coefficients.[ sz i +! sz 8 ]))
       (fun _ -> Prims.l_True)

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fst

@@ -316,14 +316,18 @@ let sample_from_binomial_distribution
       (randomness: t_Slice u8)
      =
   let _:Prims.unit = assert ((v (cast v_ETA <: u32) == 2) \/ (v (cast v_ETA <: u32) == 3)) in
-  match cast (v_ETA <: usize) <: u32 with
-  | 2ul -> sample_from_binomial_distribution_2_ #v_Vector randomness
-  | 3ul -> sample_from_binomial_distribution_3_ #v_Vector randomness
-  | _ ->
-    Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code"
+  let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector =
+    match cast (v_ETA <: usize) <: u32 with
+    | 2ul -> sample_from_binomial_distribution_2_ #v_Vector randomness
+    | 3ul -> sample_from_binomial_distribution_3_ #v_Vector randomness
+    | _ ->
+      Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code"
 
-        <:
-        Rust_primitives.Hax.t_Never)
+          <:
+          Rust_primitives.Hax.t_Never)
+  in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 #push-options "--admit_smt_queries true"
 

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti

@@ -117,7 +117,13 @@ val sample_from_binomial_distribution
       (requires
         (v_ETA =. sz 2 || v_ETA =. sz 3) &&
         (Core.Slice.impl__len #u8 randomness <: usize) =. (v_ETA *! sz 64 <: usize))
-      (fun _ -> Prims.l_True)
+      (ensures
+        fun result ->
+          let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = result in
+          forall (i: nat).
+            i < 8 ==>
+            Libcrux_ml_kem.Ntt.ntt_layer_7_pre (result.f_coefficients.[ sz i ])
+              (result.f_coefficients.[ sz i +! sz 8 ]))
 
 val sample_from_xof
       (v_K: usize)

libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst

@@ -213,6 +213,17 @@ let decode_then_decompress_v (#r:rank): t_Array u8 (v_C2_SIZE r) -> polynomial
 
 (** IND-CPA Functions *)
 
+val ind_cpa_generate_keypair_unpacked (r:rank) (randomness:t_Array u8 v_CPA_KEY_GENERATION_SEED_SIZE) :
+                             ((((vector r) & (t_Array u8 (sz 32))) & (vector r)) & bool)
+let ind_cpa_generate_keypair_unpacked r randomness =
+    let hashed = v_G randomness in
+    let (seed_for_A, seed_for_secret_and_error) = split hashed (sz 32) in
+    let (matrix_A_as_ntt, sufficient_randomness) = sample_matrix_A_ntt #r seed_for_A in
+    let secret_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error (sz 0) in
+    let error_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error r in
+    let t_as_ntt = compute_As_plus_e_ntt #r matrix_A_as_ntt secret_as_ntt error_as_ntt in
+    (((t_as_ntt,seed_for_A), secret_as_ntt), sufficient_randomness)
+
 /// This function implements most of <strong>Algorithm 12</strong> of the
 /// NIST FIPS 203 specification; this is the MLKEM CPA-PKE key generation algorithm.
 ///
@@ -223,16 +234,30 @@ let decode_then_decompress_v (#r:rank): t_Array u8 (v_C2_SIZE r) -> polynomial
 val ind_cpa_generate_keypair (r:rank) (randomness:t_Array u8 v_CPA_KEY_GENERATION_SEED_SIZE) :
                              (t_MLKEMCPAKeyPair r & bool)
 let ind_cpa_generate_keypair r randomness =
-    let hashed = v_G randomness in
-    let (seed_for_A, seed_for_secret_and_error) = split hashed (sz 32) in
-    let (matrix_A_as_ntt, sufficient_randomness) = sample_matrix_A_ntt #r seed_for_A in
-    let secret_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error (sz 0) in
-    let error_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error r in
-    let t_as_ntt = compute_As_plus_e_ntt #r matrix_A_as_ntt secret_as_ntt error_as_ntt in
+    let (((t_as_ntt,seed_for_A), secret_as_ntt), sufficient_randomness) =
+      ind_cpa_generate_keypair_unpacked r randomness in
     let public_key_serialized = Seq.append (vector_encode_12 #r t_as_ntt) seed_for_A in
     let secret_key_serialized = vector_encode_12 #r secret_as_ntt in
     ((secret_key_serialized,public_key_serialized), sufficient_randomness)
 
+val ind_cpa_encrypt_unpacked (r:rank)
+                    (message: t_Array u8 v_SHARED_SECRET_SIZE)
+                    (randomness:t_Array u8 v_SHARED_SECRET_SIZE)
+                    (t_as_ntt:vector r)
+                    (matrix_A_as_ntt:matrix r) :
+                    t_MLKEMCiphertext r
+
+let ind_cpa_encrypt_unpacked r message randomness t_as_ntt matrix_A_as_ntt =
+    let r_as_ntt = sample_vector_cbd_then_ntt #r randomness (sz 0) in
+    let error_1 = sample_vector_cbd2 #r randomness r in
+    let error_2 = sample_poly_cbd2 #r randomness (r +! r) in
+    let u = vector_add (vector_inv_ntt (matrix_vector_mul_ntt (matrix_transpose matrix_A_as_ntt) r_as_ntt)) error_1 in
+    let mu = decode_then_decompress_message message in
+    let v = poly_add (poly_add (vector_dot_product_ntt t_as_ntt r_as_ntt) error_2) mu in  
+    let c1 = compress_then_encode_u #r u in
+    let c2 = compress_then_encode_v #r v in
+    concat c1 c2
+
 /// This function implements <strong>Algorithm 13</strong> of the
 /// NIST FIPS 203 specification; this is the MLKEM CPA-PKE encryption algorithm.
 
@@ -246,15 +271,19 @@ let ind_cpa_encrypt r public_key message randomness =
     let (t_as_ntt_bytes, seed_for_A) = split public_key (v_T_AS_NTT_ENCODED_SIZE r) in
     let t_as_ntt = vector_decode_12 #r t_as_ntt_bytes in 
     let matrix_A_as_ntt, sufficient_randomness = sample_matrix_A_ntt #r seed_for_A in
-    let r_as_ntt = sample_vector_cbd_then_ntt #r randomness (sz 0) in
-    let error_1 = sample_vector_cbd2 #r randomness r in
-    let error_2 = sample_poly_cbd2 #r randomness (r +! r) in
-    let u = vector_add (vector_inv_ntt (matrix_vector_mul_ntt (matrix_transpose matrix_A_as_ntt) r_as_ntt)) error_1 in
-    let mu = decode_then_decompress_message message in
-    let v = poly_add (poly_add (vector_dot_product_ntt t_as_ntt r_as_ntt) error_2) mu in  
-    let c1 = compress_then_encode_u #r u in
-    let c2 = compress_then_encode_v #r v in
-    (concat c1 c2, sufficient_randomness)
+    let c = ind_cpa_encrypt_unpacked r message randomness t_as_ntt matrix_A_as_ntt in
+    (c, sufficient_randomness)
+
+val ind_cpa_decrypt_unpacked (r:rank)
+                    (ciphertext: t_MLKEMCiphertext r) (secret_as_ntt:vector r): 
+                    t_MLKEMSharedSecret
+
+let ind_cpa_decrypt_unpacked r ciphertext secret_as_ntt =
+    let (c1,c2) = split ciphertext (v_C1_SIZE r) in
+    let u = decode_then_decompress_u #r c1 in
+    let v = decode_then_decompress_v #r c2 in
+    let w = poly_sub v (poly_inv_ntt (vector_dot_product_ntt secret_as_ntt (vector_ntt u))) in
+    compress_then_encode_message w
 
 /// This function implements <strong>Algorithm 14</strong> of the
 /// NIST FIPS 203 specification; this is the MLKEM CPA-PKE decryption algorithm.
@@ -265,12 +294,8 @@ val ind_cpa_decrypt (r:rank) (secret_key: t_MLKEMCPAPrivateKey r)
 
 [@ "opaque_to_smt"]
 let ind_cpa_decrypt r secret_key ciphertext =
-    let (c1,c2) = split ciphertext (v_C1_SIZE r) in
-    let u = decode_then_decompress_u #r c1 in
-    let v = decode_then_decompress_v #r c2 in
     let secret_as_ntt = vector_decode_12 #r secret_key in
-    let w = poly_sub v (poly_inv_ntt (vector_dot_product_ntt secret_as_ntt (vector_ntt u))) in
-    compress_then_encode_message w
+    ind_cpa_decrypt_unpacked r ciphertext secret_as_ntt
 
 (** IND-CCA Functions *)
 

libcrux-ml-kem/src/ind_cpa.rs

@@ -158,7 +158,13 @@ pub(crate) fn serialize_secret_key<const K: usize, const OUT_LEN: usize, Vector:
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\
     $ETA2 == Spec.MLKEM.v_ETA2 $K /\\
+    v $domain_separator < 2 * v $K /\\
     range (v $domain_separator + v $K) u8_inttype"))]
+#[hax_lib::ensures(|(err1,ds)|
+    fstar!("v $ds == v $domain_separator + v $K /\\
+                Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector $err1 ==
+                Spec.MLKEM.sample_vector_cbd1 #$K (Seq.slice $prf_input 0 32) (sz (v $domain_separator))")
+)]
 fn sample_ring_element_cbd<
     const K: usize,
     const ETA2_RANDOMNESS_SIZE: usize,
@@ -187,7 +193,7 @@ fn sample_ring_element_cbd<
 /// Sample a vector of ring elements from a centered binomial distribution and
 /// convert them into their NTT representations.
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $ETA_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
     $ETA == Spec.MLKEM.v_ETA1 $K /\\
@@ -299,7 +305,10 @@ 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!("
+#[hax_lib::ensures(|_| fstar!("let (((t_as_ntt,seed_for_A), 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}.f_t_as_ntt) == t_as_ntt) /\\
+        (${public_key}.f_seed_for_A == seed_for_A) /\\
+        ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${private_key}.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 ==>
@@ -476,6 +485,7 @@ fn compress_then_serialize_u<
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
+#[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::fstar::options("--z3rlimit 200")]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
       $ETA1 == Spec.MLKEM.v_ETA1 $K /\\
@@ -489,6 +499,11 @@ fn compress_then_serialize_u<
       $BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\
       $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
       length $randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE"))]
+#[hax_lib::ensures(|result|
+    fstar!("$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)")
+)]
 pub(crate) fn encrypt_unpacked<
     const K: usize,
     const CIPHERTEXT_SIZE: usize,
@@ -721,11 +736,16 @@ fn deserialize_secret_key<const K: usize, Vector: Operations>(
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
+#[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
     $U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\
     $V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\
     $VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE $K"))]
+#[hax_lib::ensures(|result|
+    fstar!("$result == Spec.MLKEM.ind_cpa_decrypt_unpacked $K $ciphertext
+        (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${secret_key}.f_secret_as_ntt)")
+)]
 pub(crate) fn decrypt_unpacked<
     const K: usize,
     const CIPHERTEXT_SIZE: usize,