fstar

cryspen · Nov 11, 2024 · 595517c · 595517c
1 parent 9c7d46a
commit 595517c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
@@ -233,7 +233,7 @@ val compress_then_serialize_ring_element_v
     : Prims.Pure (t_Slice u8)
       (requires
         Spec.MLKEM.is_rank v_K /\
-        v v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
+        v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
         Seq.length out == v v_OUT_LEN /\ coefficients_field_modulus_range re)
       (ensures
         fun out_future ->

diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs
@@ -326,7 +326,7 @@ fn compress_then_serialize_5<Vector: Operations>(
 #[inline(always)]
 #[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\ 
-    v $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\
+    $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\
     Seq.length $out == v $OUT_LEN /\\ coefficients_field_modulus_range $re"))]
 #[hax_lib::ensures(|_|
     fstar!("${out_future.len()} == ${out.len()} /\\