port

cryspen · Sep 3, 2024 · 7dc12e9 · 7dc12e9
1 parent 9be19e9
commit 7dc12e9
Show file tree

Hide file tree

Showing 9 changed files with 32 additions and 31 deletions.
diff --git a/libcrux-ml-kem/hax.py b/libcrux-ml-kem/hax.py
@@ -40,6 +40,8 @@ def __call__(self, parser, args, values, option_string=None) -> None:
             "-i",
             include_str,
             "fstar",
+            "--z3rlimit",
+            "80",
             "--interfaces",
             interface_include,
         ]

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.fst
@@ -11,6 +11,8 @@ let _ =
   let open Libcrux_ml_kem.Vector.Traits in
   ()
 
+#push-options "--z3rlimit 150"
+
 let serialize_kem_secret_key
       (v_K v_SERIALIZED_KEY_LEN: usize)
       (#v_Hasher: Type0)
@@ -157,6 +159,8 @@ let serialize_kem_secret_key
   in
   out
 
+#pop-options
+
 let validate_public_key
       (v_K v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize)
       (#v_Vector: Type0)

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
@@ -1,5 +1,5 @@
 module Libcrux_ml_kem.Vector.Portable
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 300 --split_queries always"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Makefile b/libcrux-ml-kem/proofs/fstar/extraction/Makefile
@@ -3,6 +3,7 @@ SLOW_MODULES += Libcrux_ml_kem.Vector.Portable.Serialize.fst
 ADMIT_MODULES = Libcrux_ml_kem.Ind_cca.Unpacked.fst \
               Libcrux_ml_kem.Invert_ntt.fst \
               Libcrux_ml_kem.Ntt.fst \
+              Libcrux_ml_kem.Serialize.fst \
               Libcrux_ml_kem.Sampling.fst \
               Libcrux_ml_kem.Polynomial.fst \
               Libcrux_ml_kem.Vector.Avx2.fst \

diff --git a/libcrux-ml-kem/src/ind_cca.rs b/libcrux-ml-kem/src/ind_cca.rs
@@ -39,6 +39,7 @@ pub(crate) mod instantiations;
 
 /// Serialize the secret key.
 #[inline(always)]
+#[hax_lib::fstar::options("--z3rlimit 150")]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $SERIALIZED_KEY_LEN == Spec.MLKEM.v_CCA_PRIVATE_KEY_SIZE $K /\\
     ${private_key.len()} == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K /\\

diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs
@@ -53,60 +53,60 @@ impl crate::vector::traits::Repr for SIMD256Vector {
 #[hax_lib::attributes]
 impl Operations for SIMD256Vector {
     #[inline(always)]
-    #[ensures(|result| fstar!("impl.f_repr out == Seq.create 16 0s"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Seq.create 16 0s"))]
     fn ZERO() -> Self {
         vec_zero()
     }
 
     #[requires(array.len() == 16)]
-    #[ensures(|result| fstar!("impl.f_repr out == $array"))]
+    #[ensures(|out| fstar!("impl.f_repr out == $array"))]
     fn from_i16_array(array: &[i16]) -> Self {
         vec_from_i16_array(array)
     }
 
-    #[ensures(|result| fstar!("out == impl.f_repr $x"))]
+    #[ensures(|out| fstar!("out == impl.f_repr $x"))]
     fn to_i16_array(x: Self) -> [i16; 16] {
         vec_to_i16_array(x)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn add(lhs: Self, rhs: &Self) -> Self {
         Self {
             elements: arithmetic::add(lhs.elements, rhs.elements),
         }
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn sub(lhs: Self, rhs: &Self) -> Self {
         Self {
             elements: arithmetic::sub(lhs.elements, rhs.elements),
         }
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
     fn multiply_by_constant(v: Self, c: i16) -> Self {
         Self {
             elements: arithmetic::multiply_by_constant(v.elements, c),
         }
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. $constant) (impl.f_repr $vector)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. $constant) (impl.f_repr $vector)"))]
     fn bitwise_and_with_constant(vector: Self, constant: i16) -> Self {
         Self {
             elements: arithmetic::bitwise_and_with_constant(vector.elements, constant),
         }
     }
 
     #[requires(SHIFT_BY >= 0 && SHIFT_BY < 16)]
-    #[ensures(|result| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $vector)"))]
+    #[ensures(|out| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $vector)"))]
     fn shift_right<const SHIFT_BY: i32>(vector: Self) -> Self {
         Self {
             elements: arithmetic::shift_right::<{ SHIFT_BY }>(vector.elements),
         }
     }
 
     #[requires(true)]
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $vector)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $vector)"))]
     fn cond_subtract_3329(vector: Self) -> Self {
         Self {
             elements: arithmetic::cond_subtract_3329(vector.elements),

diff --git a/libcrux-ml-kem/src/vector/neon.rs b/libcrux-ml-kem/src/vector/neon.rs
@@ -26,18 +26,18 @@ impl crate::vector::traits::Repr for SIMD128Vector {
 #[hax_lib::attributes]
 impl Operations for SIMD128Vector {
     #[inline(always)]
-    #[ensures(|result| fstar!("impl.f_repr out == Seq.create 16 0s"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Seq.create 16 0s"))]
     fn ZERO() -> Self {
         ZERO()
     }
 
     #[requires(array.len() == 16)]
-    #[ensures(|result| fstar!("impl.f_repr out == $array"))]
+    #[ensures(|out| fstar!("impl.f_repr out == $array"))]
     fn from_i16_array(array: &[i16]) -> Self {
         from_i16_array(array)
     }
 
-    #[ensures(|result| fstar!("out == impl.f_repr $x"))]
+    #[ensures(|out| fstar!("out == impl.f_repr $x"))]
     fn to_i16_array(x: Self) -> [i16; 16] {
         to_i16_array(x)
     }

diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs
@@ -23,51 +23,52 @@ impl crate::vector::traits::Repr for PortableVector {
 }
 
 #[hax_lib::attributes]
+#[hax_lib::fstar::options("--z3rlimit 300")]
 impl Operations for PortableVector {
-    #[ensures(|result| fstar!("impl.f_repr out == Seq.create 16 0s"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Seq.create 16 0s"))]
     fn ZERO() -> Self {
         zero()
     }
 
     #[requires(array.len() == 16)]
-    #[ensures(|result| fstar!("impl.f_repr out == $array"))]
+    #[ensures(|out| fstar!("impl.f_repr out == $array"))]
     fn from_i16_array(array: &[i16]) -> Self {
         from_i16_array(array)
     }
 
-    #[ensures(|result| fstar!("out == impl.f_repr $x"))]
+    #[ensures(|out| fstar!("out == impl.f_repr $x"))]
     fn to_i16_array(x: Self) -> [i16; 16] {
         to_i16_array(x)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (+.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn add(lhs: Self, rhs: &Self) -> Self {
         add(lhs, rhs)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map2 (-.) (impl.f_repr $lhs) (impl.f_repr $rhs)"))]
     fn sub(lhs: Self, rhs: &Self) -> Self {
         sub(lhs, rhs)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x *. c) (impl.f_repr $v)"))]
     fn multiply_by_constant(v: Self, c: i16) -> Self {
         multiply_by_constant(v, c)
     }
 
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. c) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> x &. c) (impl.f_repr $v)"))]
     fn bitwise_and_with_constant(v: Self, c: i16) -> Self {
         bitwise_and_with_constant(v, c)
     }
 
     #[requires(SHIFT_BY >= 0 && SHIFT_BY < 16)]
-    #[ensures(|result| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("(v_SHIFT_BY >=. 0l /\\ v_SHIFT_BY <. 16l) ==> impl.f_repr out == Spec.Utils.map_array (fun x -> x >>! ${SHIFT_BY}) (impl.f_repr $v)"))]
     fn shift_right<const SHIFT_BY: i32>(v: Self) -> Self {
         shift_right::<{ SHIFT_BY }>(v)
     }
 
     #[requires(true)]
-    #[ensures(|result| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $v)"))]
+    #[ensures(|out| fstar!("impl.f_repr out == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (impl.f_repr $v)"))]
     fn cond_subtract_3329(v: Self) -> Self {
         cond_subtract_3329(v)
     }
@@ -134,31 +135,27 @@ impl Operations for PortableVector {
     }
 
     #[requires(fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $a)"))]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 1 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 1 (impl.f_repr $a) $out"))]
     fn serialize_1(a: Self) -> [u8; 2] {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_lemma $a");
         serialize_1(a)
     }
 
     #[requires(a.len() == 2)]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 2 ==> Spec.MLKEM.deserialize_post 1 $a (impl.f_repr $out)"))]
     fn deserialize_1(a: &[u8]) -> Self {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_lemma $a");
         deserialize_1(a)
     }
 
     #[requires(fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $a)"))]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 4 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 4 (impl.f_repr $a) $out"))]
     fn serialize_4(a: Self) -> [u8; 8] {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_lemma $a");
         serialize_4(a)
     }
 
     #[requires(a.len() == 8)]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 8 ==> Spec.MLKEM.deserialize_post 4 $a (impl.f_repr $out)"))]
     fn deserialize_4(a: &[u8]) -> Self {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_lemma $a");
@@ -175,15 +172,13 @@ impl Operations for PortableVector {
     }
 
     #[requires(fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $a)"))]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 10 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 10 (impl.f_repr $a) $out"))]
     fn serialize_10(a: Self) -> [u8; 20] {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_10_lemma $a");
         serialize_10(a)
     }
 
     #[requires(a.len() == 20)]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 20 ==> Spec.MLKEM.deserialize_post 10 $a (impl.f_repr $out)"))]
     fn deserialize_10(a: &[u8]) -> Self {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_lemma $a");
@@ -200,15 +195,13 @@ impl Operations for PortableVector {
     }
 
     #[requires(fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $a)"))]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("Spec.MLKEM.serialize_pre 12 (impl.f_repr $a) ==> Spec.MLKEM.serialize_post 12 (impl.f_repr $a) $out"))]
     fn serialize_12(a: Self) -> [u8; 24] {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.serialize_12_lemma $a");
         serialize_12(a)
     }
 
     #[requires(a.len() == 24)]
-    // Output name has be `out` https://github.com/hacspec/hax/issues/832
     #[ensures(|out| fstar!("sz (Seq.length $a) =. sz 24 ==> Spec.MLKEM.deserialize_post 12 $a (impl.f_repr $out)"))]
     fn deserialize_12(a: &[u8]) -> Self {
         hax_lib::fstar!("Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_lemma $a");

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 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul