SIMD Traits Spec and Pre-Condition Style

libcrux-ml-dsa/Cargo.toml

@@ -20,7 +20,8 @@ libcrux-sha3 = { version = "0.0.2-beta.2", path = "../libcrux-sha3" }
 libcrux-intrinsics = { version = "0.0.2-beta.2", path = "../libcrux-intrinsics" }
 libcrux-platform = { version = "0.0.2-beta.2", path = "../sys/platform" }
 libcrux-macros = { version = "0.0.2-beta.2", path = "../macros" }
-hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/"}
+#hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/"}
+hax-lib = { git = "https://github.com/hacspec/hax/", branch = "prop-predicates" }
 
 [dev-dependencies]
 rand = { version = "0.8" }

libcrux-ml-dsa/hax.py

@@ -120,7 +120,7 @@ def __call__(self, parser, args, values, option_string=None) -> None:
         admit_env = {}
         if args.admit:
             admit_env = {"OTHERFLAGS": "--admit_smt_queries true"}
-        shell(["make", "-C", "proofs/fstar/extraction/"], env=admit_env)
+        shell(["make", "-C", "proofs/fstar/extraction/", "-j4"], env=admit_env)
         return None
 
 

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fst

@@ -7,13 +7,35 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Libcrux_ml_dsa.Simd.Avx2.Vector_type in
+  let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 =
+let impl: Libcrux_ml_dsa.Simd.Traits.t_Repr Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 =
   {
     _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve;
     _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
+    f_repr_pre = (fun (self: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) -> true);
+    f_repr_post
+    =
+    (fun (self: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) (out: t_Array i32 (mk_usize 8)) ->
+        true);
+    f_repr
+    =
+    fun (self: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) ->
+      let result:t_Array i32 (mk_usize 8) = Rust_primitives.Hax.repeat (mk_i32 0) (mk_usize 8) in
+      let result:t_Array i32 (mk_usize 8) =
+        Libcrux_ml_dsa.Simd.Avx2.Vector_type.to_coefficient_array self result
+      in
+      result
+  }
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256 =
+  {
+    _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve;
+    _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
+    _super_6182285156695963586 = FStar.Tactics.Typeclasses.solve;
     f_zero_pre = (fun (_: Prims.unit) -> true);
     f_zero_post = (fun (_: Prims.unit) (out: Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256) -> true);
     f_zero = (fun (_: Prims.unit) -> Libcrux_ml_dsa.Simd.Avx2.Vector_type.zero ());

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.fsti

@@ -7,8 +7,12 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Libcrux_ml_dsa.Simd.Avx2.Vector_type in
+  let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl:Libcrux_ml_dsa.Simd.Traits.t_Repr Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256
+
 /// Implementing the [`Operations`] for AVX2.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl:Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256
+val impl_1:Libcrux_ml_dsa.Simd.Traits.t_Operations Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_Vec256

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.fst

@@ -7,14 +7,35 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Libcrux_ml_dsa.Simd.Portable.Vector_type in
+  let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Libcrux_ml_dsa.Simd.Traits.t_Operations
+let impl: Libcrux_ml_dsa.Simd.Traits.t_Repr Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
+  {
+    _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve;
+    _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
+    f_repr_pre = (fun (self: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) -> true);
+    f_repr_post
+    =
+    (fun
+        (self: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients)
+        (out: t_Array i32 (mk_usize 8))
+        ->
+        true);
+    f_repr
+    =
+    fun (self: Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients) ->
+      self.Libcrux_ml_dsa.Simd.Portable.Vector_type.f_values
+  }
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: Libcrux_ml_dsa.Simd.Traits.t_Operations
 Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients =
   {
     _super_13011033735201511749 = FStar.Tactics.Typeclasses.solve;
     _super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
+    _super_6182285156695963586 = FStar.Tactics.Typeclasses.solve;
     f_zero_pre = (fun (_: Prims.unit) -> true);
     f_zero_post
     =

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.fsti

@@ -7,8 +7,12 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Libcrux_ml_dsa.Simd.Portable.Vector_type in
+  let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-val impl:Libcrux_ml_dsa.Simd.Traits.t_Operations
+val impl:Libcrux_ml_dsa.Simd.Traits.t_Repr Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_1:Libcrux_ml_dsa.Simd.Traits.t_Operations
 Libcrux_ml_dsa.Simd.Portable.Vector_type.t_Coefficients

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fst

@@ -0,0 +1,131 @@
+module Libcrux_ml_dsa.Simd.Traits
+#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 Hax_lib.Abstraction in
+  let open Hax_lib.Prop in
+  ()
+
+let int_is_i32 (i: Hax_lib.Int.t_Int) =
+  i <=
+  (Hax_lib.Abstraction.f_lift #i32 #FStar.Tactics.Typeclasses.solve Core.Num.impl_i32__MAX
+    <:
+    Hax_lib.Int.t_Int) &&
+  i >=
+  (Hax_lib.Abstraction.f_lift #i32 #FStar.Tactics.Typeclasses.solve Core.Num.impl_i32__MIN
+    <:
+    Hax_lib.Int.t_Int)
+
+let add_pre (lhs rhs: t_Array i32 (mk_usize 8)) =
+  Hax_lib.Prop.v_forall #usize
+    #Hax_lib.Prop.t_Prop
+    (fun i ->
+        let i:usize = i in
+        Hax_lib.Prop.implies #bool
+          #bool
+          (i <. v_COEFFICIENTS_IN_SIMD_UNIT <: bool)
+          (fun temp_0_ ->
+              let _:Prims.unit = temp_0_ in
+              int_is_i32 ((Hax_lib.Abstraction.f_lift #i32
+                      #FStar.Tactics.Typeclasses.solve
+                      (lhs.[ i ] <: i32)
+                    <:
+                    Hax_lib.Int.t_Int) +
+                  (Hax_lib.Abstraction.f_lift #i32
+                      #FStar.Tactics.Typeclasses.solve
+                      (rhs.[ i ] <: i32)
+                    <:
+                    Hax_lib.Int.t_Int)
+                  <:
+                  Hax_lib.Int.t_Int)
+              <:
+              bool)
+        <:
+        Hax_lib.Prop.t_Prop)
+
+let add_post (lhs rhs future_lhs: t_Array i32 (mk_usize 8)) =
+  Hax_lib.Prop.v_forall #usize
+    #Hax_lib.Prop.t_Prop
+    (fun i ->
+        let i:usize = i in
+        Hax_lib.Prop.implies #bool
+          #bool
+          (i <. v_COEFFICIENTS_IN_SIMD_UNIT <: bool)
+          (fun temp_0_ ->
+              let _:Prims.unit = temp_0_ in
+              (Hax_lib.Abstraction.f_lift #i32
+                  #FStar.Tactics.Typeclasses.solve
+                  (future_lhs.[ i ] <: i32)
+                <:
+                Hax_lib.Int.t_Int) =
+              ((Hax_lib.Abstraction.f_lift #i32 #FStar.Tactics.Typeclasses.solve (lhs.[ i ] <: i32)
+                  <:
+                  Hax_lib.Int.t_Int) +
+                (Hax_lib.Abstraction.f_lift #i32 #FStar.Tactics.Typeclasses.solve (rhs.[ i ] <: i32)
+                  <:
+                  Hax_lib.Int.t_Int)
+                <:
+                Hax_lib.Int.t_Int)
+              <:
+              bool)
+        <:
+        Hax_lib.Prop.t_Prop)
+
+let sub_pre (lhs rhs: t_Array i32 (mk_usize 8)) =
+  Hax_lib.Prop.v_forall #usize
+    #Hax_lib.Prop.t_Prop
+    (fun i ->
+        let i:usize = i in
+        Hax_lib.Prop.implies #bool
+          #bool
+          (i <. v_COEFFICIENTS_IN_SIMD_UNIT <: bool)
+          (fun temp_0_ ->
+              let _:Prims.unit = temp_0_ in
+              int_is_i32 ((Hax_lib.Abstraction.f_lift #i32
+                      #FStar.Tactics.Typeclasses.solve
+                      (lhs.[ i ] <: i32)
+                    <:
+                    Hax_lib.Int.t_Int) -
+                  (Hax_lib.Abstraction.f_lift #i32
+                      #FStar.Tactics.Typeclasses.solve
+                      (rhs.[ i ] <: i32)
+                    <:
+                    Hax_lib.Int.t_Int)
+                  <:
+                  Hax_lib.Int.t_Int)
+              <:
+              bool)
+        <:
+        Hax_lib.Prop.t_Prop)
+
+let sub_post (lhs rhs future_lhs: t_Array i32 (mk_usize 8)) =
+  Hax_lib.Prop.v_forall #usize
+    #Hax_lib.Prop.t_Prop
+    (fun i ->
+        let i:usize = i in
+        Hax_lib.Prop.implies #bool
+          #bool
+          (i <. v_COEFFICIENTS_IN_SIMD_UNIT <: bool)
+          (fun temp_0_ ->
+              let _:Prims.unit = temp_0_ in
+              (Hax_lib.Abstraction.f_lift #i32
+                  #FStar.Tactics.Typeclasses.solve
+                  (future_lhs.[ i ] <: i32)
+                <:
+                Hax_lib.Int.t_Int) =
+              ((Hax_lib.Abstraction.f_lift #i32 #FStar.Tactics.Typeclasses.solve (lhs.[ i ] <: i32)
+                  <:
+                  Hax_lib.Int.t_Int) -
+                (Hax_lib.Abstraction.f_lift #i32 #FStar.Tactics.Typeclasses.solve (rhs.[ i ] <: i32)
+                  <:
+                  Hax_lib.Int.t_Int)
+                <:
+                Hax_lib.Int.t_Int)
+              <:
+              bool)
+        <:
+        Hax_lib.Prop.t_Prop)

libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Traits.fsti

@@ -3,6 +3,13 @@ module Libcrux_ml_dsa.Simd.Traits
 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 Hax_lib.Abstraction in
+  let open Hax_lib.Prop in
+  ()
+
 let v_COEFFICIENTS_IN_SIMD_UNIT: usize = mk_usize 8
 
 let v_SIMD_UNITS_IN_RING_ELEMENT: usize =
@@ -12,30 +19,97 @@ let v_FIELD_MODULUS: i32 = mk_i32 8380417
 
 let v_INVERSE_OF_MODULUS_MOD_MONTGOMERY_R: u64 = mk_u64 58728449
 
+class t_Repr (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_13011033735201511749:Core.Marker.t_Copy v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self;
+  f_repr_pre:self_: v_Self -> pred: Type0{true ==> pred};
+  f_repr_post:v_Self -> t_Array i32 (mk_usize 8) -> Type0;
+  f_repr:x0: v_Self
+    -> Prims.Pure (t_Array i32 (mk_usize 8)) (f_repr_pre x0) (fun result -> f_repr_post x0 result)
+}
+
+val int_is_i32 (i: Hax_lib.Int.t_Int) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
+val add_pre (lhs rhs: t_Array i32 (mk_usize 8))
+    : Prims.Pure Hax_lib.Prop.t_Prop Prims.l_True (fun _ -> Prims.l_True)
+
+val add_post (lhs rhs future_lhs: t_Array i32 (mk_usize 8))
+    : Prims.Pure Hax_lib.Prop.t_Prop Prims.l_True (fun _ -> Prims.l_True)
+
+val sub_pre (lhs rhs: t_Array i32 (mk_usize 8))
+    : Prims.Pure Hax_lib.Prop.t_Prop Prims.l_True (fun _ -> Prims.l_True)
+
+val sub_post (lhs rhs future_lhs: t_Array i32 (mk_usize 8))
+    : Prims.Pure Hax_lib.Prop.t_Prop Prims.l_True (fun _ -> Prims.l_True)
+
 class t_Operations (v_Self: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_13011033735201511749:Core.Marker.t_Copy v_Self;
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_6182285156695963586:t_Repr v_Self;
   f_zero_pre:Prims.unit -> Type0;
-  f_zero_post:Prims.unit -> v_Self -> Type0;
+  f_zero_post:x: Prims.unit -> result: v_Self
+    -> pred:
+      Type0
+        { pred ==>
+          (let _:Prims.unit = x in
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve result <: t_Array i32 (mk_usize 8)) =.
+            (Rust_primitives.Hax.repeat (mk_i32 0) (mk_usize 8) <: t_Array i32 (mk_usize 8))) };
   f_zero:x0: Prims.unit -> Prims.Pure v_Self (f_zero_pre x0) (fun result -> f_zero_post x0 result);
-  f_from_coefficient_array_pre:t_Slice i32 -> v_Self -> Type0;
-  f_from_coefficient_array_post:t_Slice i32 -> v_Self -> v_Self -> Type0;
+  f_from_coefficient_array_pre:array: t_Slice i32 -> out: v_Self
+    -> pred:
+      Type0{(Core.Slice.impl__len #i32 array <: usize) =. v_COEFFICIENTS_IN_SIMD_UNIT ==> pred};
+  f_from_coefficient_array_post:array: t_Slice i32 -> out: v_Self -> out_future: v_Self
+    -> pred:
+      Type0
+        { pred ==>
+          (f_repr #v_Self #FStar.Tactics.Typeclasses.solve out_future <: t_Array i32 (mk_usize 8)) =.
+          array };
   f_from_coefficient_array:x0: t_Slice i32 -> x1: v_Self
     -> Prims.Pure v_Self
         (f_from_coefficient_array_pre x0 x1)
         (fun result -> f_from_coefficient_array_post x0 x1 result);
-  f_to_coefficient_array_pre:v_Self -> t_Slice i32 -> Type0;
-  f_to_coefficient_array_post:v_Self -> t_Slice i32 -> t_Slice i32 -> Type0;
+  f_to_coefficient_array_pre:value: v_Self -> out: t_Slice i32
+    -> pred: Type0{(Core.Slice.impl__len #i32 out <: usize) =. v_COEFFICIENTS_IN_SIMD_UNIT ==> pred};
+  f_to_coefficient_array_post:value: v_Self -> out: t_Slice i32 -> out_future: t_Slice i32
+    -> pred:
+      Type0
+        { pred ==>
+          out_future =.
+          (f_repr #v_Self #FStar.Tactics.Typeclasses.solve value <: t_Array i32 (mk_usize 8)) };
   f_to_coefficient_array:x0: v_Self -> x1: t_Slice i32
     -> Prims.Pure (t_Slice i32)
         (f_to_coefficient_array_pre x0 x1)
         (fun result -> f_to_coefficient_array_post x0 x1 result);
-  f_add_pre:v_Self -> v_Self -> Type0;
-  f_add_post:v_Self -> v_Self -> v_Self -> Type0;
+  f_add_pre:lhs: v_Self -> rhs: v_Self
+    -> pred:
+      Type0
+        { add_pre (f_repr #v_Self #FStar.Tactics.Typeclasses.solve lhs <: t_Array i32 (mk_usize 8))
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve rhs <: t_Array i32 (mk_usize 8)) ==>
+          pred };
+  f_add_post:lhs: v_Self -> rhs: v_Self -> lhs_future: v_Self
+    -> pred:
+      Type0
+        { pred ==>
+          add_post (f_repr #v_Self #FStar.Tactics.Typeclasses.solve lhs <: t_Array i32 (mk_usize 8))
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve rhs <: t_Array i32 (mk_usize 8))
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve lhs_future <: t_Array i32 (mk_usize 8))
+        };
   f_add:x0: v_Self -> x1: v_Self
     -> Prims.Pure v_Self (f_add_pre x0 x1) (fun result -> f_add_post x0 x1 result);
-  f_subtract_pre:v_Self -> v_Self -> Type0;
-  f_subtract_post:v_Self -> v_Self -> v_Self -> Type0;
+  f_subtract_pre:lhs: v_Self -> rhs: v_Self
+    -> pred:
+      Type0
+        { sub_pre (f_repr #v_Self #FStar.Tactics.Typeclasses.solve lhs <: t_Array i32 (mk_usize 8))
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve rhs <: t_Array i32 (mk_usize 8)) ==>
+          pred };
+  f_subtract_post:lhs: v_Self -> rhs: v_Self -> lhs_future: v_Self
+    -> pred:
+      Type0
+        { pred ==>
+          sub_post (f_repr #v_Self #FStar.Tactics.Typeclasses.solve lhs <: t_Array i32 (mk_usize 8))
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve rhs <: t_Array i32 (mk_usize 8))
+            (f_repr #v_Self #FStar.Tactics.Typeclasses.solve lhs_future <: t_Array i32 (mk_usize 8))
+        };
   f_subtract:x0: v_Self -> x1: v_Self
     -> Prims.Pure v_Self (f_subtract_pre x0 x1) (fun result -> f_subtract_post x0 x1 result);
   f_infinity_norm_exceeds_pre:v_Self -> i32 -> Type0;
@@ -111,8 +185,21 @@ class t_Operations (v_Self: Type0) = {
     -> Prims.Pure v_Self
         (f_gamma1_deserialize_pre x0 x1 x2)
         (fun result -> f_gamma1_deserialize_post x0 x1 x2 result);
-  f_commitment_serialize_pre:v_Self -> t_Slice u8 -> Type0;
-  f_commitment_serialize_post:v_Self -> t_Slice u8 -> t_Slice u8 -> Type0;
+  f_commitment_serialize_pre:simd_unit: v_Self -> serialized: t_Slice u8
+    -> pred:
+      Type0
+        { (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 4 ||
+          (Core.Slice.impl__len #u8 serialized <: usize) =. mk_usize 6 ==>
+          pred };
+  f_commitment_serialize_post:
+      simd_unit: v_Self ->
+      serialized: t_Slice u8 ->
+      serialized_future: t_Slice u8
+    -> pred:
+      Type0
+        { pred ==>
+          (Core.Slice.impl__len #u8 serialized_future <: usize) =.
+          (Core.Slice.impl__len #u8 serialized <: usize) };
   f_commitment_serialize:x0: v_Self -> x1: t_Slice u8
     -> Prims.Pure (t_Slice u8)
         (f_commitment_serialize_pre x0 x1)