fstar refresh

cryspen · Nov 11, 2024 · 392604e · 392604e
1 parent a081805
commit 392604e
Show file tree

Hide file tree

Showing 8 changed files with 32 additions and 26 deletions.
diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Arm64_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Avx2_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 

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
@@ -738,7 +738,8 @@ let encrypt_unpacked
   let ciphertext:t_Array u8 v_CIPHERTEXT_SIZE =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from ciphertext
       ({ Core.Ops.Range.f_start = v_C1_LEN } <: Core.Ops.Range.t_RangeFrom usize)
-      (Libcrux_ml_kem.Serialize.compress_then_serialize_ring_element_v v_V_COMPRESSION_FACTOR
+      (Libcrux_ml_kem.Serialize.compress_then_serialize_ring_element_v v_K
+          v_V_COMPRESSION_FACTOR
           v_C2_LEN
           #v_Vector
           v
@@ -881,7 +882,8 @@ let deserialize_then_decompress_u
           let u_as_ntt:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K =
             Rust_primitives.Hax.Monomorphized_update_at.update_at_usize u_as_ntt
               i
-              (Libcrux_ml_kem.Serialize.deserialize_then_decompress_ring_element_u v_U_COMPRESSION_FACTOR
+              (Libcrux_ml_kem.Serialize.deserialize_then_decompress_ring_element_u v_K
+                  v_U_COMPRESSION_FACTOR
                   #v_Vector
                   u_bytes
                 <:

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
@@ -777,7 +777,7 @@ let compress_then_serialize_ring_element_u
   result
 
 let compress_then_serialize_ring_element_v
-      (v_COMPRESSION_FACTOR v_OUT_LEN: usize)
+      (v_K v_COMPRESSION_FACTOR v_OUT_LEN: usize)
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i1:
@@ -862,7 +862,7 @@ let deserialize_then_decompress_10_
   re
 
 let deserialize_then_decompress_ring_element_u
-      (v_COMPRESSION_FACTOR: usize)
+      (v_K v_COMPRESSION_FACTOR: usize)
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i1:

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
@@ -81,13 +81,14 @@ val deserialize_then_decompress_ring_element_v
       (serialized: t_Slice u8)
     : Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (requires
-        (v_COMPRESSION_FACTOR =. sz 4 || v_COMPRESSION_FACTOR =. sz 5) &&
-        (Core.Slice.impl__len #u8 serialized <: usize) =. (sz 32 *! v_COMPRESSION_FACTOR <: usize))
+        Spec.MLKEM.is_rank v_K /\
+        v v_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
+        Seq.length serialized == 32 * v v_COMPRESSION_FACTOR)
       (ensures
         fun result ->
           let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = result in
           Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector result ==
-          Spec.MLKEM.decode_then_decompress_v v_COMPRESSION_FACTOR serialized)
+          Spec.MLKEM.decode_then_decompress_v #v_K serialized)
 
 /// Only use with public values.
 /// This MUST NOT be used with secret inputs, like its caller `deserialize_ring_elements_reduced`.
@@ -224,22 +225,22 @@ val compress_then_serialize_ring_element_u
             (Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector re))
 
 val compress_then_serialize_ring_element_v
-      (v_COMPRESSION_FACTOR v_OUT_LEN: usize)
+      (v_K v_COMPRESSION_FACTOR v_OUT_LEN: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (out: t_Slice u8)
     : Prims.Pure (t_Slice u8)
       (requires
-        (v v_COMPRESSION_FACTOR == 4 \/ v v_COMPRESSION_FACTOR == 5) /\
-        v v_OUT_LEN == 32 * v v_COMPRESSION_FACTOR /\ Seq.length out == v v_OUT_LEN /\
-        coefficients_field_modulus_range re)
+        Spec.MLKEM.is_rank v_K /\
+        v 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 ->
           let out_future:t_Slice u8 = out_future in
           Core.Slice.impl__len #u8 out_future == Core.Slice.impl__len #u8 out /\
           out_future ==
-          Spec.MLKEM.compress_then_encode_v v_COMPRESSION_FACTOR
+          Spec.MLKEM.compress_then_encode_v #v_K
             (Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector re))
 
 val deserialize_then_decompress_10_
@@ -251,7 +252,7 @@ val deserialize_then_decompress_10_
       (fun _ -> Prims.l_True)
 
 val deserialize_then_decompress_ring_element_u
-      (v_COMPRESSION_FACTOR: usize)
+      (v_K v_COMPRESSION_FACTOR: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (serialized: t_Slice u8)
@@ -263,7 +264,7 @@ val deserialize_then_decompress_ring_element_u
         fun result ->
           let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = result in
           Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector result ==
-          Spec.MLKEM.byte_decode_then_decompress (v v_COMPRESSION_FACTOR) serialized)
+          Spec.MLKEM.byte_decode_then_decompress #v_K serialized)
 
 val serialize_uncompressed_ring_element
       (#v_Vector: Type0)

diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
@@ -682,7 +682,7 @@ pub(crate) fn encrypt_unpacked<
     );
 
     // c_2 := Encode_{dv}(Compress_q(v,d_v))
-    compress_then_serialize_ring_element_v::<V_COMPRESSION_FACTOR, C2_LEN, Vector>(
+    compress_then_serialize_ring_element_v::<K, V_COMPRESSION_FACTOR, C2_LEN, Vector>(
         v,
         &mut ciphertext[C1_LEN..],
     );
@@ -808,7 +808,7 @@ fn deserialize_then_decompress_u<
                 Spec.MLKEM.poly_ntt (Spec.MLKEM.byte_decode_then_decompress (v $U_COMPRESSION_FACTOR)
                   (Seq.slice $ciphertext (j * v (Spec.MLKEM.v_C1_BLOCK_SIZE $K))
                     (j * v (Spec.MLKEM.v_C1_BLOCK_SIZE $K) + v (Spec.MLKEM.v_C1_BLOCK_SIZE $K))))") });
-            u_as_ntt[i]  = deserialize_then_decompress_ring_element_u::<U_COMPRESSION_FACTOR, Vector>(u_bytes);
+            u_as_ntt[i]  = deserialize_then_decompress_ring_element_u::<K, U_COMPRESSION_FACTOR, Vector>(u_bytes);
             ntt_vector_u::<U_COMPRESSION_FACTOR, Vector>(&mut u_as_ntt[i]);
         }
     }

diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs
@@ -325,14 +325,16 @@ fn compress_then_serialize_5<Vector: Operations>(
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(panic_free)]
-#[hax_lib::requires(fstar!("(v $COMPRESSION_FACTOR == 4 \\/ v $COMPRESSION_FACTOR == 5) /\\ v $OUT_LEN == 32 * v $COMPRESSION_FACTOR /\\
+#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\ 
+    v $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()} /\\
-        ${out}_future == Spec.MLKEM.compress_then_encode_v $COMPRESSION_FACTOR
+        ${out}_future == Spec.MLKEM.compress_then_encode_v #v_K
             (Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $re)")
 )]
 pub(super) fn compress_then_serialize_ring_element_v<
+    const K: usize,
     const COMPRESSION_FACTOR: usize,
     const OUT_LEN: usize,
     Vector: Operations,
@@ -399,9 +401,10 @@ fn deserialize_then_decompress_11<Vector: Operations>(
 )]
 #[hax_lib::ensures(|result|
     fstar!("Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $result == 
-        Spec.MLKEM.byte_decode_then_decompress (v $COMPRESSION_FACTOR) $serialized")
+        Spec.MLKEM.byte_decode_then_decompress #v_K $serialized")
 )]
 pub(super) fn deserialize_then_decompress_ring_element_u<
+    const K: usize, 
     const COMPRESSION_FACTOR: usize,
     Vector: Operations,
 >(
@@ -457,13 +460,13 @@ fn deserialize_then_decompress_5<Vector: Operations>(
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(panic_free)]
-#[hax_lib::requires(
-    (COMPRESSION_FACTOR == 4 || COMPRESSION_FACTOR == 5) &&
-    serialized.len() == 32 * COMPRESSION_FACTOR
+#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\ 
+    v $COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\\
+    Seq.length serialized == 32 * v v_COMPRESSION_FACTOR")
 )]
 #[hax_lib::ensures(|result|
     fstar!("Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $result == 
-        Spec.MLKEM.decode_then_decompress_v $COMPRESSION_FACTOR $serialized")
+        Spec.MLKEM.decode_then_decompress_v #v_K $serialized")
 )]
 pub(super) fn deserialize_then_decompress_ring_element_v<
     const COMPRESSION_FACTOR: usize,

diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti
@@ -1,5 +1,5 @@
 module Libcrux_platform.Platform
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul