Reomve Libcrux_ml_kem.Vector.Portable from ADMIT_MODULES

cryspen · Nov 13, 2024 · 69a27e4 · 69a27e4
1 parent d1b75ab
commit 69a27e4
Show file tree

Hide file tree

Showing 13 changed files with 67 additions and 25 deletions.
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fst
@@ -45,6 +45,8 @@ let impl_4__serialized_private_key
       <:
       Rust_primitives.Hax.t_Never)
 
+#push-options "--z3rlimit 200"
+
 let transpose_a
       (v_K: usize)
       (#v_Vector: Type0)
@@ -138,6 +140,8 @@ let transpose_a
   in
   v_A
 
+#pop-options
+
 let impl_4__new
       (v_K: usize)
       (#v_Vector: Type0)
@@ -421,7 +425,7 @@ let impl_4__serialized_public_key
     v_PUBLIC_KEY_SIZE
     self.f_public_key
 
-#push-options "--z3rlimit 200 --ext context_pruning"
+#push-options "--z3rlimit 800 --ext context_pruning"
 
 let generate_keypair
       (v_K v_CPA_PRIVATE_KEY_SIZE v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_BYTES_PER_RING_ELEMENT v_ETA1 v_ETA1_RANDOMNESS_SIZE:

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
@@ -21,6 +21,8 @@ let to_unsigned_field_modulus
   let _:Prims.unit = admit () (* Panic freedom *) in
   result
 
+#push-options "--admit_smt_queries true"
+
 let deserialize_then_decompress_11_
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -72,6 +74,8 @@ let deserialize_then_decompress_11_
   in
   re
 
+#pop-options
+
 let deserialize_then_decompress_4_
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -123,6 +127,8 @@ let deserialize_then_decompress_4_
   in
   re
 
+#push-options "--admit_smt_queries true"
+
 let deserialize_then_decompress_5_
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -186,6 +192,8 @@ let deserialize_then_decompress_5_
   in
   re
 
+#pop-options
+
 let deserialize_then_decompress_message
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
@@ -256,8 +256,12 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
     f_decompress_ciphertext_coefficient_pre
     =
     (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) ->
-        v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l ||
-        v_COEFFICIENT_BITS =. 11l);
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v v_COEFFICIENT_BITS == 11) /\
+        (forall (i: nat).
+            i < 16 ==>
+            v (Seq.index (impl.f_repr vector) i) >= 0 /\
+            v (Seq.index (impl.f_repr vector) i) < pow2 (v v_COEFFICIENT_BITS)));
     f_decompress_ciphertext_coefficient_post
     =
     (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) (out: t_SIMD256Vector) -> true);

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Arithmetic.fst
@@ -310,6 +310,8 @@ let bitwise_and_with_constant
   in
   vec
 
+#push-options "--z3rlimit 300"
+
 let cond_subtract_3329_ (vec: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
   let v__vec0:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = vec in
   let vec:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
@@ -356,6 +358,8 @@ let cond_subtract_3329_ (vec: Libcrux_ml_kem.Vector.Portable.Vector_type.t_Porta
   in
   vec
 
+#pop-options
+
 #push-options "--z3rlimit 150"
 
 let montgomery_multiply_by_constant

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
@@ -355,26 +355,30 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     =
     (fun
         (v_COEFFICIENT_BITS: i32)
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
-        v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l ||
-        v_COEFFICIENT_BITS =. 11l);
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v v_COEFFICIENT_BITS == 11) /\
+        (forall (i: nat).
+            i < 16 ==>
+            v (Seq.index (impl.f_repr a) i) >= 0 /\
+            v (Seq.index (impl.f_repr a) i) < pow2 (v v_COEFFICIENT_BITS)));
     f_decompress_ciphertext_coefficient_post
     =
     (fun
         (v_COEFFICIENT_BITS: i32)
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
         true);
     f_decompress_ciphertext_coefficient
     =
     (fun
         (v_COEFFICIENT_BITS: i32)
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
         Libcrux_ml_kem.Vector.Portable.Compress.decompress_ciphertext_coefficient v_COEFFICIENT_BITS
-          v);
+          a);
     f_ntt_layer_1_step_pre
     =
     (fun

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
@@ -167,11 +167,15 @@ class t_Operations (v_Self: Type0) = {
     -> Prims.Pure v_Self
         (f_compress_pre v_COEFFICIENT_BITS x0)
         (fun result -> f_compress_post v_COEFFICIENT_BITS x0 result);
-  f_decompress_ciphertext_coefficient_pre:v_COEFFICIENT_BITS: i32 -> v: v_Self
+  f_decompress_ciphertext_coefficient_pre:v_COEFFICIENT_BITS: i32 -> a: v_Self
     -> pred:
       Type0
-        { v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l ||
-          v_COEFFICIENT_BITS =. 11l ==>
+        { (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+            v v_COEFFICIENT_BITS == 11) /\
+          (forall (i: nat).
+              i < 16 ==>
+              v (Seq.index (f_repr a) i) >= 0 /\
+              v (Seq.index (f_repr a) i) < pow2 (v v_COEFFICIENT_BITS)) ==>
           pred };
   f_decompress_ciphertext_coefficient_post:v_COEFFICIENT_BITS: i32 -> v_Self -> v_Self -> Type0;
   f_decompress_ciphertext_coefficient:v_COEFFICIENT_BITS: i32 -> x0: v_Self

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile
@@ -1,7 +1,6 @@
 SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst
 
 ADMIT_MODULES = Libcrux_ml_kem.Vector.Avx2.fsti \
-              Libcrux_ml_kem.Vector.Portable.fsti \
               Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.fst \
               Libcrux_ml_kem.Ind_cca.Instantiations.Avx2.Unpacked.fst \
               Libcrux_ml_kem.Ind_cca.Instantiations.Neon.Unpacked.fst \
@@ -15,7 +14,6 @@ ADMIT_MODULES = Libcrux_ml_kem.Vector.Avx2.fsti \
               Libcrux_ml_kem.Mlkem512.Avx2.Unpacked.fst \
               Libcrux_ml_kem.Mlkem512.Neon.Unpacked.fst \
               Libcrux_ml_kem.Mlkem512.Portable.Unpacked.fst \
-              Libcrux_ml_kem.Vector.Portable.fst \
               Libcrux_ml_kem.Vector.Avx2.Serialize.fst \
               Libcrux_ml_kem.Vector.Avx2.fst \
               Libcrux_ml_kem.Vector.Avx2.Ntt.fst \

diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs
@@ -625,6 +625,7 @@ pub(crate) mod unpacked {
         }
     }
 
+    #[hax_lib::fstar::options("--z3rlimit 200")]
     #[hax_lib::ensures(|result|
         fstar!("forall (i: nat). i < v $K ==>
             (forall (j: nat). j < v $K ==>
@@ -667,7 +668,7 @@ pub(crate) mod unpacked {
 
     /// Generate Unpacked Keys
     #[inline(always)]
-    #[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")]
+    #[hax_lib::fstar::options("--z3rlimit 800 --ext context_pruning")]
     #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
         $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
         $ETA1 == Spec.MLKEM.v_ETA1 $K /\\

diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs
@@ -375,6 +375,7 @@ fn deserialize_then_decompress_10<Vector: Operations>(
 }
 
 #[inline(always)]
+#[hax_lib::fstar::verification_status(lax)]
 #[hax_lib::requires(
     serialized.len() == 352
 )]
@@ -440,6 +441,7 @@ fn deserialize_then_decompress_4<Vector: Operations>(
 }
 
 #[inline(always)]
+#[hax_lib::fstar::verification_status(lax)]
 #[hax_lib::requires(
     serialized.len() == 160
 )]

diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs
@@ -181,8 +181,12 @@ impl Operations for SIMD256Vector {
         }
     }
 
-    #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 ||
-        COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)]
+    #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/
+        v $COEFFICIENT_BITS == 5 \\/
+        v $COEFFICIENT_BITS == 10 \\/
+        v $COEFFICIENT_BITS == 11) /\\
+    (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $vector) i) >= 0 /\\
+        v (Seq.index (impl.f_repr $vector) i) < pow2 (v $COEFFICIENT_BITS))"))]
     #[inline(always)]
     fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(vector: Self) -> Self {
         Self {

diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs
@@ -198,10 +198,14 @@ impl Operations for PortableVector {
         compress::<COEFFICIENT_BITS>(a)
     }
 
-    #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 ||
-               COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)]
-    fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(v: Self) -> Self {
-        decompress_ciphertext_coefficient::<COEFFICIENT_BITS>(v)
+    #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/
+        v $COEFFICIENT_BITS == 5 \\/
+        v $COEFFICIENT_BITS == 10 \\/
+        v $COEFFICIENT_BITS == 11) /\\
+    (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\
+        v (Seq.index (impl.f_repr $a) i) < pow2 (v $COEFFICIENT_BITS))"))]
+    fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(a: Self) -> Self {
+        decompress_ciphertext_coefficient::<COEFFICIENT_BITS>(a)
     }
 
     #[requires(fstar!("Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ 

diff --git a/libcrux-ml-kem/src/vector/portable/arithmetic.rs b/libcrux-ml-kem/src/vector/portable/arithmetic.rs
@@ -135,6 +135,7 @@ pub fn shift_right<const SHIFT_BY: i32>(mut vec: PortableVector) -> PortableVect
 /// Note: This function is not secret independent
 /// Only use with public values.
 #[inline(always)]
+#[hax_lib::fstar::options("--z3rlimit 300")]
 #[hax_lib::requires(fstar!("Spec.Utils.is_i16b_array (pow2 12 - 1) ${vec}.f_elements"))]
 #[hax_lib::ensures(|result| fstar!("${result}.f_elements == Spec.Utils.map_array 
                 (fun x -> if x >=. 3329s then x -! 3329s else x) (${vec}.f_elements)"))]

diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs
@@ -88,9 +88,13 @@ pub trait Operations: Copy + Clone + Repr {
             v $COEFFICIENT_BITS == 11) ==>
                 (forall (i:nat). i < 16 ==> bounded (Seq.index (f_repr $result) i) (v $COEFFICIENT_BITS))"))]
     fn compress<const COEFFICIENT_BITS: i32>(a: Self) -> Self;
-    #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 ||
-        COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)]
-    fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(v: Self) -> Self;
+    #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/
+        v $COEFFICIENT_BITS == 5 \\/
+        v $COEFFICIENT_BITS == 10 \\/
+        v $COEFFICIENT_BITS == 11) /\\
+    (forall (i:nat). i < 16 ==> v (Seq.index (f_repr $a) i) >= 0 /\\
+        v (Seq.index (f_repr $a) i) < pow2 (v $COEFFICIENT_BITS))"))]
+    fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(a: Self) -> Self;
 
     // NTT
     #[requires(fstar!("Spec.Utils.is_i16b 1664 zeta0 /\\ Spec.Utils.is_i16b 1664 zeta1 /\\ 
@@ -189,7 +193,7 @@ pub trait Operations: Copy + Clone {
     fn montgomery_multiply_by_constant(v: Self, c: i16) -> Self;
     fn compress_1(v: Self) -> Self;
     fn compress<const COEFFICIENT_BITS: i32>(v: Self) -> Self;
-    fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(v: Self) -> Self;
+    fn decompress_ciphertext_coefficient<const COEFFICIENT_BITS: i32>(a: Self) -> Self;
     fn ntt_layer_1_step(a: Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self;
     fn ntt_layer_2_step(a: Self, zeta0: i16, zeta1: i16) -> Self;
     fn ntt_layer_3_step(a: Self, zeta: i16) -> Self;