Add proofs for encapsulate/decapsulate in Ind_cca

cryspen · Sep 24, 2024 · bc1ba13 · bc1ba13
1 parent db5ff02
commit bc1ba13
Show file tree

Hide file tree

Showing 4 changed files with 96 additions and 25 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst
@@ -192,8 +192,6 @@ let validate_public_key
   in
   public_key =. public_key_serialized
 
-#push-options "--admit_smt_queries true"
-
 #push-options "--z3rlimit 500"
 
 let decapsulate
@@ -210,6 +208,10 @@ let decapsulate
       (private_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey v_SECRET_KEY_SIZE)
       (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE)
      =
+  let _:Prims.unit =
+    assert (v v_CIPHERTEXT_SIZE ==
+        v v_IMPLICIT_REJECTION_HASH_INPUT_SIZE - v Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE)
+  in
   let ind_cpa_secret_key, secret_key:(t_Slice u8 & t_Slice u8) =
     Core.Slice.impl__split_at #u8
       (private_key.Libcrux_ml_kem.Types.f_value <: t_Slice u8)
@@ -221,6 +223,20 @@ let decapsulate
   let ind_cpa_public_key_hash, implicit_rejection_value:(t_Slice u8 & t_Slice u8) =
     Core.Slice.impl__split_at #u8 secret_key Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE
   in
+  let _:Prims.unit =
+    assert (ind_cpa_secret_key == slice private_key.f_value (sz 0) v_CPA_SECRET_KEY_SIZE);
+    assert (ind_cpa_public_key ==
+        slice private_key.f_value v_CPA_SECRET_KEY_SIZE (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE)
+      );
+    assert (ind_cpa_public_key_hash ==
+        slice private_key.f_value
+          (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE)
+          (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE));
+    assert (implicit_rejection_value ==
+        slice private_key.f_value
+          (v_CPA_SECRET_KEY_SIZE +! v_PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE)
+          (length private_key.f_value))
+  in
   let decrypted:t_Array u8 (sz 32) =
     Libcrux_ml_kem.Ind_cpa.decrypt v_K
       v_CIPHERTEXT_SIZE
@@ -234,6 +250,7 @@ let decapsulate
   let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) =
     Libcrux_ml_kem.Utils.into_padded_array (sz 64) (decrypted <: t_Slice u8)
   in
+  let _:Prims.unit = eq_intro (Seq.slice to_hash 0 32) decrypted in
   let to_hash:t_Array u8 (sz 64) =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash
       ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE }
@@ -249,6 +266,11 @@ let decapsulate
         <:
         t_Slice u8)
   in
+  let _:Prims.unit =
+    lemma_slice_append to_hash decrypted ind_cpa_public_key_hash;
+    assert (decrypted == Spec.MLKEM.ind_cpa_decrypt v_K ind_cpa_secret_key ciphertext.f_value);
+    assert (to_hash == concat decrypted ind_cpa_public_key_hash)
+  in
   let hashed:t_Array u8 (sz 64) =
     Libcrux_ml_kem.Hash_functions.f_G #v_Hasher
       #v_K
@@ -260,11 +282,21 @@ let decapsulate
       (hashed <: t_Slice u8)
       Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE
   in
+  let _:Prims.unit =
+    assert ((shared_secret, pseudorandomness) ==
+        split hashed Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE);
+    assert (length implicit_rejection_value =
+        v_SECRET_KEY_SIZE -! v_CPA_SECRET_KEY_SIZE -! v_PUBLIC_KEY_SIZE -!
+        Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE);
+    assert (length implicit_rejection_value = Spec.MLKEM.v_SHARED_SECRET_SIZE);
+    assert (Spec.MLKEM.v_SHARED_SECRET_SIZE <=. Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE v_K)
+  in
   let (to_hash: t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE):t_Array u8
     v_IMPLICIT_REJECTION_HASH_INPUT_SIZE =
     Libcrux_ml_kem.Utils.into_padded_array v_IMPLICIT_REJECTION_HASH_INPUT_SIZE
       implicit_rejection_value
   in
+  let _:Prims.unit = eq_intro (Seq.slice to_hash 0 32) implicit_rejection_value in
   let to_hash:t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash
       ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE }
@@ -285,15 +317,23 @@ let decapsulate
         <:
         t_Slice u8)
   in
-  let _:Prims.unit = assert (v (sz 32) < pow2 32) in
-  let _:Prims.unit = assert (i4.f_PRF_pre (sz 32) to_hash) in
+  let _:Prims.unit =
+    assert_norm (pow2 32 == 0x100000000);
+    assert (v (sz 32) < pow2 32);
+    assert (i4.f_PRF_pre (sz 32) to_hash);
+    lemma_slice_append to_hash implicit_rejection_value ciphertext.f_value
+  in
   let (implicit_rejection_shared_secret: t_Array u8 (sz 32)):t_Array u8 (sz 32) =
     Libcrux_ml_kem.Hash_functions.f_PRF #v_Hasher
       #v_K
       #FStar.Tactics.Typeclasses.solve
       (sz 32)
       (to_hash <: t_Slice u8)
   in
+  let _:Prims.unit =
+    assert (implicit_rejection_shared_secret == Spec.Utils.v_PRF (sz 32) to_hash);
+    assert (Seq.length ind_cpa_public_key == v v_PUBLIC_KEY_SIZE)
+  in
   let expected_ciphertext:t_Array u8 v_CIPHERTEXT_SIZE =
     Libcrux_ml_kem.Ind_cpa.encrypt v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_SIZE v_C2_SIZE
       v_VECTOR_U_COMPRESSION_FACTOR v_VECTOR_V_COMPRESSION_FACTOR v_C1_BLOCK_SIZE v_ETA1
@@ -331,8 +371,6 @@ let decapsulate
 
 #pop-options
 
-#pop-options
-
 #push-options "--z3rlimit 150"
 
 let encapsulate
@@ -359,6 +397,7 @@ let encapsulate
   let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) =
     Libcrux_ml_kem.Utils.into_padded_array (sz 64) (randomness <: t_Slice u8)
   in
+  let _:Prims.unit = eq_intro (Seq.slice to_hash 0 32) randomness in
   let to_hash:t_Array u8 (sz 64) =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from to_hash
       ({ Core.Ops.Range.f_start = Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE }
@@ -379,6 +418,11 @@ let encapsulate
         <:
         t_Slice u8)
   in
+  let _:Prims.unit =
+    assert (Seq.slice to_hash 0 (v Libcrux_ml_kem.Constants.v_H_DIGEST_SIZE) == randomness);
+    lemma_slice_append to_hash randomness (Spec.Utils.v_H public_key.f_value);
+    assert (to_hash == concat randomness (Spec.Utils.v_H public_key.f_value))
+  in
   let hashed:t_Array u8 (sz 64) =
     Libcrux_ml_kem.Hash_functions.f_G #v_Hasher
       #v_K
@@ -412,13 +456,9 @@ let encapsulate
       shared_secret
       ciphertext
   in
-  let result:(Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32)) =
-    ciphertext, shared_secret_array
-    <:
-    (Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32))
-  in
-  let _:Prims.unit = admit () (* Panic freedom *) in
-  result
+  ciphertext, shared_secret_array
+  <:
+  (Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32))
 
 #pop-options
 

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fsti
@@ -100,9 +100,9 @@ class t_Variant (v_Self: Type0) = {
       v_K: usize ->
       #v_Hasher: Type0 ->
       {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
-      t_Slice u8 ->
-      t_Array u8 (sz 32)
-    -> Type0;
+      randomness: t_Slice u8 ->
+      result: t_Array u8 (sz 32)
+    -> pred: Type0{pred ==> result == randomness};
   f_entropy_preprocess:
       v_K: usize ->
       #v_Hasher: Type0 ->
@@ -183,9 +183,9 @@ let impl: t_Variant t_MlKem =
           i3:
           Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
         (randomness: t_Slice u8)
-        (out: t_Array u8 (sz 32))
+        (result: t_Array u8 (sz 32))
         ->
-        true);
+        result == randomness);
     f_entropy_preprocess
     =
     fun

diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst
@@ -240,7 +240,8 @@ val ind_cpa_encrypt (r:rank) (public_key: t_MLKEMPublicKey r)
                     (message: t_Array u8 v_SHARED_SECRET_SIZE)
                     (randomness:t_Array u8 v_SHARED_SECRET_SIZE) :
                     (t_MLKEMCiphertext r & bool)
-
+
+[@ "opaque_to_smt"]
 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 
@@ -262,6 +263,7 @@ val ind_cpa_decrypt (r:rank) (secret_key: t_MLKEMCPAPrivateKey r)
                     (ciphertext: t_MLKEMCiphertext r): 
                     t_MLKEMSharedSecret
 
+[@ "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

diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs
@@ -163,10 +163,7 @@ fn generate_keypair<
     MlKemKeyPair::from(private_key, MlKemPublicKey::from(public_key))
 }
 
-// For some reason F* manages to assert the post-condition but fails to verify it
-// as a part of function signature 
 #[hax_lib::fstar::options("--z3rlimit 150")]
-#[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 /\\
     $PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE $K /\\
@@ -205,7 +202,11 @@ fn encapsulate<
 ) -> (MlKemCiphertext<CIPHERTEXT_SIZE>, MlKemSharedSecret) {
     let randomness = Scheme::entropy_preprocess::<K, Hasher>(&randomness);
     let mut to_hash: [u8; 2 * H_DIGEST_SIZE] = into_padded_array(&randomness);
+    hax_lib::fstar!("eq_intro (Seq.slice $to_hash 0 32) $randomness");
     to_hash[H_DIGEST_SIZE..].copy_from_slice(&Hasher::H(public_key.as_slice()));
+    hax_lib::fstar!("assert (Seq.slice to_hash 0 (v $H_DIGEST_SIZE) == $randomness);
+        lemma_slice_append $to_hash $randomness (Spec.Utils.v_H ${public_key}.f_value);
+        assert ($to_hash == concat $randomness (Spec.Utils.v_H ${public_key}.f_value))");
     let hashed = Hasher::G(&to_hash);
     let (shared_secret, pseudorandomness) = hashed.split_at(SHARED_SECRET_SIZE);
 
@@ -233,7 +234,6 @@ fn encapsulate<
 
 /// This code verifies on some machines, runs out of memory on others
 #[hax_lib::fstar::options("--z3rlimit 500")]
-#[hax_lib::fstar::verification_status(lax)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $SECRET_KEY_SIZE == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\
     $CPA_SECRET_KEY_SIZE == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\
@@ -276,10 +276,17 @@ pub(crate) fn decapsulate<
     private_key: &MlKemPrivateKey<SECRET_KEY_SIZE>,
     ciphertext: &MlKemCiphertext<CIPHERTEXT_SIZE>,
 ) -> MlKemSharedSecret {
+    hax_lib::fstar!("assert (v $CIPHERTEXT_SIZE == v $IMPLICIT_REJECTION_HASH_INPUT_SIZE - v $SHARED_SECRET_SIZE)");
     let (ind_cpa_secret_key, secret_key) = private_key.value.split_at(CPA_SECRET_KEY_SIZE);
     let (ind_cpa_public_key, secret_key) = secret_key.split_at(PUBLIC_KEY_SIZE);
     let (ind_cpa_public_key_hash, implicit_rejection_value) = secret_key.split_at(H_DIGEST_SIZE);
 
+    hax_lib::fstar!("assert ($ind_cpa_secret_key == slice ${private_key}.f_value (sz 0) $CPA_SECRET_KEY_SIZE);
+        assert ($ind_cpa_public_key == slice ${private_key}.f_value $CPA_SECRET_KEY_SIZE ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE));
+        assert ($ind_cpa_public_key_hash == slice ${private_key}.f_value ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE)
+            ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE));
+        assert ($implicit_rejection_value == slice ${private_key}.f_value ($CPA_SECRET_KEY_SIZE +! $PUBLIC_KEY_SIZE +! Spec.MLKEM.v_H_DIGEST_SIZE)
+            (length ${private_key}.f_value))");
     let decrypted = crate::ind_cpa::decrypt::<
         K,
         CIPHERTEXT_SIZE,
@@ -290,18 +297,31 @@ pub(crate) fn decapsulate<
     >(ind_cpa_secret_key, &ciphertext.value);
 
     let mut to_hash: [u8; SHARED_SECRET_SIZE + H_DIGEST_SIZE] = into_padded_array(&decrypted);
+    hax_lib::fstar!("eq_intro (Seq.slice $to_hash 0 32) $decrypted");
     to_hash[SHARED_SECRET_SIZE..].copy_from_slice(ind_cpa_public_key_hash);
 
+    hax_lib::fstar!("lemma_slice_append to_hash $decrypted $ind_cpa_public_key_hash;
+        assert ($decrypted == Spec.MLKEM.ind_cpa_decrypt $K $ind_cpa_secret_key ${ciphertext}.f_value);
+        assert ($to_hash == concat $decrypted $ind_cpa_public_key_hash)");
     let hashed = Hasher::G(&to_hash);
     let (shared_secret, pseudorandomness) = hashed.split_at(SHARED_SECRET_SIZE);
 
+    hax_lib::fstar!("assert (($shared_secret , $pseudorandomness) == split $hashed $SHARED_SECRET_SIZE);
+        assert (length $implicit_rejection_value = $SECRET_KEY_SIZE -! $CPA_SECRET_KEY_SIZE -! $PUBLIC_KEY_SIZE -! $H_DIGEST_SIZE);
+        assert (length $implicit_rejection_value = Spec.MLKEM.v_SHARED_SECRET_SIZE);
+        assert (Spec.MLKEM.v_SHARED_SECRET_SIZE <=. Spec.MLKEM.v_IMPLICIT_REJECTION_HASH_INPUT_SIZE $K)");
     let mut to_hash: [u8; IMPLICIT_REJECTION_HASH_INPUT_SIZE] =
         into_padded_array(implicit_rejection_value);
+    hax_lib::fstar!("eq_intro (Seq.slice $to_hash 0 32) $implicit_rejection_value");
     to_hash[SHARED_SECRET_SIZE..].copy_from_slice(ciphertext.as_ref());
-    hax_lib::fstar!("assert (v (sz 32) < pow2 32)");
-    hax_lib::fstar!("assert (i4.f_PRF_pre (sz 32) to_hash)");
+    hax_lib::fstar!("assert_norm (pow2 32 == 0x100000000);
+        assert (v (sz 32) < pow2 32);
+        assert (i4.f_PRF_pre (sz 32) $to_hash);
+        lemma_slice_append $to_hash $implicit_rejection_value ${ciphertext}.f_value");
     let implicit_rejection_shared_secret: [u8; SHARED_SECRET_SIZE] = Hasher::PRF(&to_hash);
 
+    hax_lib::fstar!("assert ($implicit_rejection_shared_secret == Spec.Utils.v_PRF (sz 32) $to_hash);
+        assert (Seq.length $ind_cpa_public_key == v $PUBLIC_KEY_SIZE)");
     let expected_ciphertext = crate::ind_cpa::encrypt::<
         K,
         CIPHERTEXT_SIZE,
@@ -551,6 +571,9 @@ pub(crate) trait Variant {
         ciphertext: &MlKemCiphertext<CIPHERTEXT_SIZE>,
     ) -> [u8; 32];
     #[requires(randomness.len() == 32)]
+    #[ensures(|result|
+        fstar!("$result == $randomness"))
+    ]
     fn entropy_preprocess<const K: usize, Hasher: Hash<K>>(randomness: &[u8]) -> [u8; 32];
 }
 
@@ -578,6 +601,9 @@ impl Variant for Kyber {
 
     #[inline(always)]
     #[requires(randomness.len() == 32)]
+    #[ensures(|result|
+        fstar!("$result == Spec.Utils.v_H $randomness"))
+    ]
     fn entropy_preprocess<const K: usize, Hasher: Hash<K>>(randomness: &[u8]) -> [u8; 32] {
         Hasher::H(&randomness)
     }
@@ -605,6 +631,9 @@ impl Variant for MlKem {
 
     #[inline(always)]
     #[requires(randomness.len() == 32)]
+    #[ensures(|result|
+        fstar!("$result == $randomness"))
+    ]
     fn entropy_preprocess<const K: usize, Hasher: Hash<K>>(randomness: &[u8]) -> [u8; 32] {
         randomness.try_into().unwrap()
     }