arith

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Variant.fsti

@@ -0,0 +1,243 @@
+module Libcrux_ml_kem.Variant
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
+open Core
+open FStar.Mul
+
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Libcrux_ml_kem.Hash_functions in
+  ()
+
+/// Implements [`Variant`], to perform the ML-KEM-specific actions
+/// during encapsulation and decapsulation.
+/// Specifically,
+/// * during key generation, the seed hash is domain separated (this is a difference from the FIPS 203 IPD and Kyber)
+/// * during encapsulation, the initial randomness is used without prior hashing,
+/// * the derivation of the shared secret does not include a hash of the ML-KEM ciphertext.
+type t_MlKem = | MlKem : t_MlKem
+
+/// This trait collects differences in specification between ML-KEM
+/// (FIPS 203) and the Round 3 CRYSTALS-Kyber submission in the
+/// NIST PQ competition.
+/// cf. FIPS 203, Appendix C
+class t_Variant (v_Self: Type0) = {
+  f_kdf_pre:
+      v_K: usize ->
+      v_CIPHERTEXT_SIZE: usize ->
+      #v_Hasher: Type0 ->
+      {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      shared_secret: t_Slice u8 ->
+      ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE
+    -> pred: Type0{(Core.Slice.impl__len #u8 shared_secret <: usize) =. sz 32 ==> pred};
+  f_kdf_post:
+      v_K: usize ->
+      v_CIPHERTEXT_SIZE: usize ->
+      #v_Hasher: Type0 ->
+      {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      shared_secret: t_Slice u8 ->
+      ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE ->
+      res: t_Array u8 (sz 32)
+    -> pred: Type0{pred ==> res == shared_secret};
+  f_kdf:
+      v_K: usize ->
+      v_CIPHERTEXT_SIZE: usize ->
+      #v_Hasher: Type0 ->
+      {| i1: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      x0: t_Slice u8 ->
+      x1: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE
+    -> Prims.Pure (t_Array u8 (sz 32))
+        (f_kdf_pre v_K v_CIPHERTEXT_SIZE #v_Hasher #i1 x0 x1)
+        (fun result -> f_kdf_post v_K v_CIPHERTEXT_SIZE #v_Hasher #i1 x0 x1 result);
+  f_entropy_preprocess_pre:
+      v_K: usize ->
+      #v_Hasher: Type0 ->
+      {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      randomness: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 randomness <: usize) =. sz 32 ==> pred};
+  f_entropy_preprocess_post:
+      v_K: usize ->
+      #v_Hasher: Type0 ->
+      {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      randomness: t_Slice u8 ->
+      res: t_Array u8 (sz 32)
+    -> pred: Type0{pred ==> res == randomness};
+  f_entropy_preprocess:
+      v_K: usize ->
+      #v_Hasher: Type0 ->
+      {| i3: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      x0: t_Slice u8
+    -> Prims.Pure (t_Array u8 (sz 32))
+        (f_entropy_preprocess_pre v_K #v_Hasher #i3 x0)
+        (fun result -> f_entropy_preprocess_post v_K #v_Hasher #i3 x0 result);
+  f_cpa_keygen_seed_pre:
+      v_K: usize ->
+      #v_Hasher: Type0 ->
+      {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      seed: t_Slice u8
+    -> pred: Type0{(Core.Slice.impl__len #u8 seed <: usize) =. sz 32 ==> pred};
+  f_cpa_keygen_seed_post:
+      v_K: usize ->
+      #v_Hasher: Type0 ->
+      {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      t_Slice u8 ->
+      t_Array u8 (sz 64)
+    -> Type0;
+  f_cpa_keygen_seed:
+      v_K: usize ->
+      #v_Hasher: Type0 ->
+      {| i4: Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K |} ->
+      x0: t_Slice u8
+    -> Prims.Pure (t_Array u8 (sz 64))
+        (f_cpa_keygen_seed_pre v_K #v_Hasher #i4 x0)
+        (fun result -> f_cpa_keygen_seed_post v_K #v_Hasher #i4 x0 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: t_Variant t_MlKem =
+  {
+    f_kdf_pre
+    =
+    (fun
+        (v_K: usize)
+        (v_CIPHERTEXT_SIZE: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i1:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (shared_secret: t_Slice u8)
+        (_: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE)
+        ->
+        (Core.Slice.impl__len #u8 shared_secret <: usize) =. sz 32);
+    f_kdf_post
+    =
+    (fun
+        (v_K: usize)
+        (v_CIPHERTEXT_SIZE: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i1:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (shared_secret: t_Slice u8)
+        (_: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE)
+        (res: t_Array u8 (sz 32))
+        ->
+        res == shared_secret);
+    f_kdf
+    =
+    (fun
+        (v_K: usize)
+        (v_CIPHERTEXT_SIZE: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i1:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (shared_secret: t_Slice u8)
+        (_: Libcrux_ml_kem.Types.t_MlKemCiphertext v_CIPHERTEXT_SIZE)
+        ->
+        let out:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in
+        let out:t_Array u8 (sz 32) = Core.Slice.impl__copy_from_slice #u8 out shared_secret in
+        out);
+    f_entropy_preprocess_pre
+    =
+    (fun
+        (v_K: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (randomness: t_Slice u8)
+        ->
+        (Core.Slice.impl__len #u8 randomness <: usize) =. sz 32);
+    f_entropy_preprocess_post
+    =
+    (fun
+        (v_K: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (randomness: t_Slice u8)
+        (res: t_Array u8 (sz 32))
+        ->
+        res == randomness);
+    f_entropy_preprocess
+    =
+    (fun
+        (v_K: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (randomness: t_Slice u8)
+        ->
+        let out:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in
+        let out:t_Array u8 (sz 32) = Core.Slice.impl__copy_from_slice #u8 out randomness in
+        out);
+    f_cpa_keygen_seed_pre
+    =
+    (fun
+        (v_K: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i4:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (key_generation_seed: t_Slice u8)
+        ->
+        (Core.Slice.impl__len #u8 key_generation_seed <: usize) =. sz 32);
+    f_cpa_keygen_seed_post
+    =
+    (fun
+        (v_K: usize)
+        (#v_Hasher: Type0)
+        (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i4:
+          Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+        (key_generation_seed: t_Slice u8)
+        (out: t_Array u8 (sz 64))
+        ->
+        true);
+    f_cpa_keygen_seed
+    =
+    fun
+      (v_K: usize)
+      (#v_Hasher: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()]
+        i4:
+        Libcrux_ml_kem.Hash_functions.t_Hash v_Hasher v_K)
+      (key_generation_seed: t_Slice u8)
+      ->
+      let seed:t_Array u8 (sz 33) = Rust_primitives.Hax.repeat 0uy (sz 33) in
+      let seed:t_Array u8 (sz 33) =
+        Rust_primitives.Hax.Monomorphized_update_at.update_at_range seed
+          ({
+              Core.Ops.Range.f_start = sz 0;
+              Core.Ops.Range.f_end = Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
+            }
+            <:
+            Core.Ops.Range.t_Range usize)
+          (Core.Slice.impl__copy_from_slice #u8
+              (seed.[ {
+                    Core.Ops.Range.f_start = sz 0;
+                    Core.Ops.Range.f_end
+                    =
+                    Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
+                  }
+                  <:
+                  Core.Ops.Range.t_Range usize ]
+                <:
+                t_Slice u8)
+              key_generation_seed
+            <:
+            t_Slice u8)
+      in
+      let seed:t_Array u8 (sz 33) =
+        Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed
+          Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE
+          (cast (v_K <: usize) <: u8)
+      in
+      Libcrux_ml_kem.Hash_functions.f_G #v_Hasher
+        #v_K
+        #FStar.Tactics.Typeclasses.solve
+        (seed <: t_Slice u8)
+  }

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.Arithmetic.fst

@@ -85,7 +85,7 @@ let sub (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
   in
   result
 
-#push-options "--z3rlimit 100"
+#push-options "--z3rlimit 200"
 
 let barrett_reduce (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
   let t0:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
@@ -184,7 +184,7 @@ let cond_subtract_3329_ (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
 
 #pop-options
 
-#push-options "--z3rlimit 100"
+#push-options "--z3rlimit 200"
 
 let montgomery_multiply_by_constant
       (vector: Libcrux_intrinsics.Avx2_extract.t_Vec256)

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst

@@ -0,0 +1,59 @@
+module Libcrux_ml_kem.Vector.Portable
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
+open Core
+open FStar.Mul
+
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Libcrux_ml_kem.Vector.Portable.Vector_type in
+  let open Libcrux_ml_kem.Vector.Traits in
+  ()
+
+let deserialize_11_ (a: t_Slice u8) = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_11_ a
+
+let deserialize_5_ (a: t_Slice u8) = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_5_ a
+
+let serialize_11_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  Libcrux_ml_kem.Vector.Portable.Serialize.serialize_11_ a
+
+let serialize_5_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  Libcrux_ml_kem.Vector.Portable.Serialize.serialize_5_ a
+
+let deserialize_1_ (a: t_Slice u8) =
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_lemma a in
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_bounded_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_1_ a
+
+let deserialize_10_ (a: t_Slice u8) =
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_lemma a in
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_bounded_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_10_ a
+
+let deserialize_12_ (a: t_Slice u8) =
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_lemma a in
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_bounded_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_12_ a
+
+let deserialize_4_ (a: t_Slice u8) =
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_lemma a in
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_bounded_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.deserialize_4_ a
+
+let serialize_1_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  let _:Prims.unit = assert (forall i. Rust_primitives.bounded (Seq.index a.f_elements i) 1) in
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.serialize_1_ a
+
+let serialize_10_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_10_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.serialize_10_ a
+
+let serialize_12_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_12_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.serialize_12_ a
+
+let serialize_4_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  let _:Prims.unit = assert (forall i. Rust_primitives.bounded (Seq.index a.f_elements i) 4) in
+  let _:Prims.unit = Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_lemma a in
+  Libcrux_ml_kem.Vector.Portable.Serialize.serialize_4_ a

libcrux-ml-kem/src/vector/avx2/arithmetic.rs

@@ -137,7 +137,7 @@ const BARRETT_MULTIPLIER: i16 = 20159;
 /// See Section 3.2 of the implementation notes document for an explanation
 /// of this code.
 #[inline(always)]
-#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"))]
+#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 200"))]
 #[cfg_attr(hax, hax_lib::requires(fstar!("Spec.Utils.is_i16b_array 28296 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 ${vector})")))]
 #[cfg_attr(hax, hax_lib::ensures(|result| fstar!("Spec.Utils.is_i16b_array 3328 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 ${result}) /\\
                 (forall i. i < 16 ==> v (get_lane $result i) % 3329 == 
@@ -170,7 +170,7 @@ pub(crate) fn barrett_reduce(vector: Vec256) -> Vec256 {
 }
 
 #[inline(always)]
-#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 100"))]
+#[cfg_attr(hax, hax_lib::fstar::options("--z3rlimit 200"))]
 #[cfg_attr(hax, hax_lib::requires(fstar!("Spec.Utils.is_i16b 1664 constant")))]
 #[cfg_attr(hax, hax_lib::ensures(|result| fstar!("Spec.Utils.is_i16b_array 3328 (Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 ${result}) /\\
                 (forall i. i < 16 ==> v (get_lane $result i) % 3329 ==