Skip to content

Commit

Permalink
Merge pull request #589 from cryspen/dev-arithmetic-proofs
Browse files Browse the repository at this point in the history 
Arithmetic and NTT proofs
  • Loading branch information
@karthikbhargavan
karthikbhargavan authored Sep 18, 2024
2 parents a94aed7 + 89f91b1 commit 5d35b6c
Show file tree
Hide file tree
Showing 167 changed files with 5,402 additions and 3,783 deletions.
2 changes: 1 addition & 1 deletion libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Libcrux_intrinsics.Arm64_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
open Core
open FStar.Mul

Expand Down
28 changes: 14 additions & 14 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,14 @@ Details: Malformed `Quote` item: `quote_of_expr` failed. Expression was:
};
kind = Concrete_ident.Kind.Value }));
span =
{ Span.id = 1879;
{ Span.id = 2213;
data =
[{ Span.Imported.filename =
(Span.Imported.Real
(Span.Imported.LocalPath
"libcrux-intrinsics/src/avx2_extract.rs"));
hi = { Span.Imported.col = 2; line = 240 };
lo = { Span.Imported.col = 0; line = 237 } }
hi = { Span.Imported.col = 2; line = 213 };
lo = { Span.Imported.col = 0; line = 207 } }
]
};
typ =
Expand All @@ -54,43 +54,43 @@ Details: Malformed `Quote` item: `quote_of_expr` failed. Expression was:
(Ast.String
"(AST import) Fatal error: something we considered as impossible occurred! \027[1mPlease report this by submitting an issue on GitHub!\027[0m\nDetails: [import_thir:literal] got an error literal: this means the Rust compiler or Hax's frontend probably reported errors above."));
span =
{ Span.id = 1879;
{ Span.id = 2213;
data =
[{ Span.Imported.filename =
(Span.Imported.Real
(Span.Imported.LocalPath
"libcrux-intrinsics/src/avx2_extract.rs"));
hi = { Span.Imported.col = 2; line = 240 };
lo = { Span.Imported.col = 0; line = 237 } }
hi = { Span.Imported.col = 2; line = 213 };
lo = { Span.Imported.col = 0; line = 207 } }
]
};
typ = Ast.Make.TStr };
{ Ast.Make.e =
(Ast.Make.Literal
(Ast.String
"{ Types.attributes = [];\n contents =\n Types.Literal {\n lit =\n { Types.node =\n (Types.Err Types.ErrorGuaranteed {todo = \"ErrorGuaranteed(())\"});\n span =\n { Types.filename =\n (Types.Real (Types.LocalPath \"libcrux-intrinsics/src/lib.rs\"));\n hi = { Types.col = \"0\"; line = \"1\" };\n lo = { Types.col = \"0\"; line = \"1\" } }\n };\n neg = false};\n hir_id = None;\n span =\n { Types.filename =\n (Types.Real (Types.LocalPath \"libcrux-intrinsics/src/avx2_extract.rs\"));\n hi = { Types.col = \"2\"; line = \"240\" };\n lo = { Types.col = \"0\"; line = \"237\" } };\n ty = Types.Never }"));
"{ Types.attributes = [];\n contents =\n Types.Literal {\n lit =\n { Types.node =\n (Types.Err Types.ErrorGuaranteed {todo = \"ErrorGuaranteed(())\"});\n span =\n { Types.filename =\n (Types.Real (Types.LocalPath \"libcrux-intrinsics/src/lib.rs\"));\n hi = { Types.col = \"0\"; line = \"1\" };\n lo = { Types.col = \"0\"; line = \"1\" } }\n };\n neg = false};\n hir_id = None;\n span =\n { Types.filename =\n (Types.Real (Types.LocalPath \"libcrux-intrinsics/src/avx2_extract.rs\"));\n hi = { Types.col = \"2\"; line = \"213\" };\n lo = { Types.col = \"0\"; line = \"207\" } };\n ty = Types.Never }"));
span =
{ Span.id = 1879;
{ Span.id = 2213;
data =
[{ Span.Imported.filename =
(Span.Imported.Real
(Span.Imported.LocalPath
"libcrux-intrinsics/src/avx2_extract.rs"));
hi = { Span.Imported.col = 2; line = 240 };
lo = { Span.Imported.col = 0; line = 237 } }
hi = { Span.Imported.col = 2; line = 213 };
lo = { Span.Imported.col = 0; line = 207 } }
]
};
typ = Ast.Make.TStr }
];
generic_args = []; bounds_impls = []; trait = None};
span =
{ Span.id = 1879;
{ Span.id = 2213;
data =
[{ Span.Imported.filename =
(Span.Imported.Real
(Span.Imported.LocalPath "libcrux-intrinsics/src/avx2_extract.rs"));
hi = { Span.Imported.col = 2; line = 240 };
lo = { Span.Imported.col = 0; line = 237 } }
hi = { Span.Imported.col = 2; line = 213 };
lo = { Span.Imported.col = 0; line = 207 } }
]
};
typ =
Expand All @@ -116,7 +116,7 @@ Last AST:
[{ Concrete_ident.Imported.data =
(Concrete_ident.Imported.TypeNs "avx2_extract"); disambiguator = 0 };
{ Concrete_ident.Imported.data =
(Concrete_ident.Imported.ValueNs "mm256_srli_epi16");
(Concrete_ident.Imported.ValueNs "mm256_mullo_epi16");
disambiguator = 0 }
]
};
Expand Down
120 changes: 105 additions & 15 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,37 @@
module Libcrux_intrinsics.Avx2_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
open Core
open FStar.Mul

unfold type t_Vec128 = bit_vec 128
val vec128_as_i16x8 (x:t_Vec128) : t_Array i16 (sz 8)
val vec128_as_i16x8 (x:t_Vec128) : t_Array i16 (sz 8)
let get_lane128 (v:t_Vec128) (i:nat{i < 8}) =
Seq.index (vec128_as_i16x8 v) i

unfold type t_Vec256 = bit_vec 256
val vec256_as_i16x16 (x:t_Vec256) : t_Array i16 (sz 16)
val vec256_as_i16x16 (x:t_Vec256) : t_Array i16 (sz 16)
let get_lane (v:t_Vec256) (i:nat{i < 16}) =
Seq.index (vec256_as_i16x16 v) i

val mm256_add_epi16 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
val mm256_add_epi16 (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256
Prims.l_True
(ensures
fun result ->
let result:t_Vec256 = result in
vec256_as_i16x16 result ==
Spec.Utils.map2 ( +. ) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs))

val mm256_add_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_and_si256 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
val mm256_and_si256 (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256
Prims.l_True
(ensures
fun result ->
let result:t_Vec256 = result in
vec256_as_i16x16 result ==
Spec.Utils.map2 ( &. ) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs))

val mm256_andnot_si256 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

Expand Down Expand Up @@ -45,9 +63,22 @@ val mm256_madd_epi16 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun

val mm256_mul_epu32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_mulhi_epi16 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
val mm256_mulhi_epi16 (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256
Prims.l_True
(ensures
fun result ->
let result:t_Vec256 = result in
vec256_as_i16x16 result ==
Spec.Utils.map2 (fun x y -> cast (((cast x <: i32) *. (cast y <: i32)) >>! 16l) <: i16)
(vec256_as_i16x16 lhs)
(vec256_as_i16x16 rhs))

unfold let mm256_mullo_epi16 = BitVec.Intrinsics.mm256_mullo_epi16
let lemma_mm256_mullo_epi16 v1 v2 :
Lemma (vec256_as_i16x16 (mm256_mullo_epi16 v1 v2) ==
Spec.Utils.map2 mul_mod (vec256_as_i16x16 v1) (vec256_as_i16x16 v2))
[SMTPat (vec256_as_i16x16 (mm256_mullo_epi16 v1 v2))] = admit()

val mm256_mullo_epi32 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

Expand All @@ -62,13 +93,23 @@ val mm256_permute4x64_epi64 (v_CONTROL: i32) (vector: t_Vec256)
val mm256_permutevar8x32_epi32 (vector control: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_set1_epi16 (constant: i16) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
val mm256_set1_epi16 (constant: i16)
: Prims.Pure t_Vec256
Prims.l_True
(ensures
fun result ->
let result:t_Vec256 = result in
vec256_as_i16x16 result == Spec.Utils.create (sz 16) constant)

val mm256_set1_epi32 (constant: i32) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_set1_epi64x (a: i64) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

unfold let mm256_set_epi16 = BitVec.Intrinsics.mm256_set_epi16
let lemma_mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0 :
Lemma (vec256_as_i16x16 (mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0) ==
Spec.Utils.create16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15)
[SMTPat (vec256_as_i16x16 (mm256_set_epi16 v15 v14 v13 v12 v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 v0))] = admit()

val mm256_set_epi32 (input7 input6 input5 input4 input3 input2 input1 input0: i32)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
Expand Down Expand Up @@ -98,7 +139,13 @@ val mm256_sllv_epi32 (vector counts: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_srai_epi16 (v_SHIFT_BY: i32) (vector: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
: Prims.Pure t_Vec256
(requires v_SHIFT_BY >=. 0l && v_SHIFT_BY <. 16l)
(ensures
fun result ->
let result:t_Vec256 = result in
vec256_as_i16x16 result ==
Spec.Utils.map_array (fun x -> x >>! v_SHIFT_BY) (vec256_as_i16x16 vector))

val mm256_srai_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
Expand All @@ -117,7 +164,14 @@ val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: t_Vec256)
val mm256_storeu_si256_u8 (output: t_Slice u8) (vector: t_Vec256)
: Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

val mm256_sub_epi16 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
val mm256_sub_epi16 (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256
Prims.l_True
(ensures
fun result ->
let result:t_Vec256 = result in
vec256_as_i16x16 result ==
Spec.Utils.map2 ( -. ) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs))

val mm256_unpackhi_epi32 (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
Expand All @@ -132,19 +186,48 @@ val mm256_unpacklo_epi64 (a b: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun

val mm256_xor_si256 (lhs rhs: t_Vec256) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm_add_epi16 (lhs rhs: t_Vec128) : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)
val mm_add_epi16 (lhs rhs: t_Vec128)
: Prims.Pure t_Vec128
Prims.l_True
(ensures
fun result ->
let result:t_Vec128 = result in
vec128_as_i16x8 result ==
Spec.Utils.map2 ( +. ) (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs))

val mm_loadu_si128 (input: t_Slice u8) : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)

unfold let mm_movemask_epi8 = BitVec.Intrinsics.mm_movemask_epi8

val mm_mulhi_epi16 (lhs rhs: t_Vec128) : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)

val mm_mullo_epi16 (lhs rhs: t_Vec128) : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)
val mm_mulhi_epi16 (lhs rhs: t_Vec128)
: Prims.Pure t_Vec128
Prims.l_True
(ensures
fun result ->
let result:t_Vec128 = result in
vec128_as_i16x8 result ==
Spec.Utils.map2 (fun x y -> cast (((cast x <: i32) *. (cast y <: i32)) >>! 16l) <: i16)
(vec128_as_i16x8 lhs)
(vec128_as_i16x8 rhs))

val mm_mullo_epi16 (lhs rhs: t_Vec128)
: Prims.Pure t_Vec128
Prims.l_True
(ensures
fun result ->
let result:t_Vec128 = result in
vec128_as_i16x8 result ==
Spec.Utils.map2 mul_mod (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs))

unfold let mm_packs_epi16 = BitVec.Intrinsics.mm_packs_epi16

val mm_set1_epi16 (constant: i16) : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)
val mm_set1_epi16 (constant: i16)
: Prims.Pure t_Vec128
Prims.l_True
(ensures
fun result ->
let result:t_Vec128 = result in
vec128_as_i16x8 result == Spec.Utils.create (sz 8) constant)

val mm_set_epi8
(byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0:
Expand All @@ -166,4 +249,11 @@ val mm_storeu_si128 (output: t_Slice i16) (vector: t_Vec128)
(Core.Slice.impl__len #i16 output_future <: usize) =.
(Core.Slice.impl__len #i16 output <: usize))

val mm_sub_epi16 (lhs rhs: t_Vec128) : Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)
val mm_sub_epi16 (lhs rhs: t_Vec128)
: Prims.Pure t_Vec128
Prims.l_True
(ensures
fun result ->
let result:t_Vec128 = result in
vec128_as_i16x8 result ==
Spec.Utils.map2 ( -. ) (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs))
Loading

0 comments on commit 5d35b6c

Please sign in to comment.