Fix failure in generic serialize module

cryspen · Nov 12, 2024 · 22dc07b · 22dc07b
1 parent ae7ab07
commit 22dc07b
Show file tree

Hide file tree

Showing 2 changed files with 4 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
@@ -234,7 +234,8 @@ val compress_then_serialize_ring_element_v
       (requires
         Spec.MLKEM.is_rank 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)
+        Seq.length out == v v_OUT_LEN /\ v v_OUT_LEN == 32 * v v_COMPRESSION_FACTOR /\
+        coefficients_field_modulus_range re)
       (ensures
         fun out_future ->
           let out_future:t_Slice u8 = out_future in

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