Update serialize.rs

cryspen · Sep 23, 2024 · ec66aac · ec66aac
1 parent c7c3b3e
commit ec66aac
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 16 deletions.
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
@@ -197,8 +197,6 @@ let sample_vector_cbd_then_ntt
  let _:Prims.unit = admit () (* Panic freedom *) in
  result
 
-#push-options "--z3rlimit 200"
-
 let compress_then_serialize_u
  (v_K v_OUT_LEN v_COMPRESSION_FACTOR v_BLOCK_LEN: usize)
  (#v_Vector: Type0)
@@ -265,8 +263,6 @@ let compress_then_serialize_u
  let hax_temp_output:Prims.unit = result in
  out
 
-#pop-options
-
 #push-options "--admit_smt_queries true"
 
 let deserialize_then_decompress_u

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst
@@ -617,8 +617,6 @@ let deserialize_then_decompress_5_
  in
  re
 
-#push-options "--admit_smt_queries true"
-
 let deserialize_then_decompress_message
  (#v_Vector: Type0)
  (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -669,9 +667,9 @@ let deserialize_then_decompress_message
  in
  re)
  in
- re
-
-#pop-options
+ let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = re in
+ let _:Prims.unit = admit () (* Panic freedom *) in
+ result
 
 let deserialize_then_decompress_ring_element_u
  (v_COMPRESSION_FACTOR: usize)
@@ -715,8 +713,6 @@ let deserialize_then_decompress_ring_element_v
  <:
  Rust_primitives.Hax.t_Never)
 
-#push-options "--admit_smt_queries true"
-
 let deserialize_to_reduced_ring_element
  (#v_Vector: Type0)
  (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -763,9 +759,9 @@ let deserialize_to_reduced_ring_element
  in
  re)
  in
- re
-
-#pop-options
+ let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = re in
+ let _:Prims.unit = admit () (* Panic freedom *) in
+ result
 
 let deserialize_ring_elements_reduced
  (v_K: usize)

diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs
@@ -54,7 +54,7 @@ pub(super) fn compress_then_serialize_message<Vector: Operations>(
 }
 
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
 pub(super) fn deserialize_then_decompress_message<Vector: Operations>(
  serialized: [u8; SHARED_SECRET_SIZE],
 ) -> PolynomialRingElement<Vector> {
@@ -111,7 +111,7 @@ pub(super) fn deserialize_to_uncompressed_ring_element<Vector: Operations>(
 ///
 /// This MUST NOT be used with secret inputs, like its caller `deserialize_ring_elements_reduced`.
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(
  serialized.len() == BYTES_PER_RING_ELEMENT
 )]