Skip to content

Commit

Permalink
chore: regenerate F* files
Browse files Browse the repository at this point in the history
  • Loading branch information
@W95Psp
W95Psp committed Sep 26, 2024
1 parent 232fbde commit a089e86
Show file tree
Hide file tree
Showing 63 changed files with 2,302 additions and 1,838 deletions.
76 changes: 68 additions & 8 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ module Libcrux_intrinsics.Avx2_extract
open Core
open FStar.Mul

val mm256_movemask_ps (a: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)

unfold type t_Vec128 = bit_vec 128
val vec128_as_i16x8 (x: bit_vec 128) : t_Array i16 (sz 8)
let get_lane128 (v: bit_vec 128) (i:nat{i < 8}) = Seq.index (vec128_as_i16x8 v) i
Expand All @@ -11,6 +13,8 @@ unfold type t_Vec256 = bit_vec 256
val vec256_as_i16x16 (x: bit_vec 256) : t_Array i16 (sz 16)
let get_lane (v: bit_vec 256) (i:nat{i < 16}) = Seq.index (vec256_as_i16x16 v) i

val mm256_abs_epi32 (a: 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
Expand All @@ -22,16 +26,30 @@ val mm256_add_epi16 (lhs rhs: t_Vec256)

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

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

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

val mm256_blend_epi16 (v_CONTROL: i32) (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_blend_epi32 (v_CONTROL: i32) (lhs rhs: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_bsrli_epi128 (v_SHIFT_BY: i32) (x: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_castsi128_si256 (vector: t_Vec128)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_castsi256_ps (a: t_Vec256) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

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

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

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

val mm256_cvtepi16_epi32 (vector: t_Vec128)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

Expand All @@ -41,9 +59,14 @@ val mm256_inserti128_si256 (v_CONTROL: i32) (vector: t_Vec256) (vector_i128: t_V
val mm256_loadu_si256_i16 (input: t_Slice i16)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_loadu_si256_i32 (input: t_Slice i32)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_loadu_si256_u8 (input: t_Slice u8)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

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

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)
Expand All @@ -59,6 +82,8 @@ val mm256_mulhi_epi16 (lhs rhs: t_Vec256)

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

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

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

val mm256_permute2x128_si256 (v_IMM8: i32) (a b: t_Vec256)
Expand All @@ -75,15 +100,22 @@ val mm256_set1_epi64x (a: i64) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prim

include BitVec.Intrinsics {mm256_set_epi32}

val mm256_set_epi64x (input3 input2 input1 input0: i64)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

include BitVec.Intrinsics {mm256_set_epi8}

val mm256_set_m128i (hi lo: t_Vec128) : Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_setzero_si256: Prims.unit -> Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_shuffle_epi32 (v_CONTROL: i32) (vector: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

include BitVec.Intrinsics {mm256_shuffle_epi8}

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

val mm256_slli_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

Expand All @@ -107,8 +139,23 @@ val mm256_srai_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256)
val mm256_srli_epi32 (v_SHIFT_BY: i32) (vector: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_srlv_epi32 (vector counts: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_srlv_epi64 (vector counts: t_Vec256)
: Prims.Pure t_Vec256 Prims.l_True (fun _ -> Prims.l_True)

val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: t_Vec256)
: Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)
: Prims.Pure (t_Slice i16)
Prims.l_True
(ensures
fun output_future ->
let output_future:t_Slice i16 = output_future in
(Core.Slice.impl__len #i16 output_future <: usize) =.
(Core.Slice.impl__len #i16 output <: usize))

val mm256_storeu_si256_i32 (output: t_Slice i32) (vector: t_Vec256)
: Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True)

val mm256_storeu_si256_u8 (output: t_Slice u8) (vector: t_Vec256)
: Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
Expand All @@ -122,6 +169,10 @@ val mm256_sub_epi16 (lhs rhs: t_Vec256)
vec256_as_i16x16 result ==
Spec.Utils.map2 ( -. ) (vec256_as_i16x16 lhs) (vec256_as_i16x16 rhs))

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

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

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

Expand Down Expand Up @@ -174,20 +225,26 @@ val mm_set1_epi16 (constant: i16)
let result:t_Vec128 = result in
vec128_as_i16x8 result == Spec.Utils.create (sz 8) constant)

val mm_set_epi32 (input3 input2 input1 input0: i32)
: Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)

include BitVec.Intrinsics {mm_set_epi8}

include BitVec.Intrinsics {mm_shuffle_epi8}

val mm_sllv_epi32 (vector counts: t_Vec128)
: Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)

val mm_srli_epi64 (v_SHIFT_BY: i32) (vector: t_Vec128)
: Prims.Pure t_Vec128 Prims.l_True (fun _ -> Prims.l_True)

include BitVec.Intrinsics {mm_storeu_bytes_si128}

val mm_storeu_si128 (output: t_Slice i16) (vector: t_Vec128)
: Prims.Pure (t_Slice i16)
Prims.l_True
(ensures
fun output_future ->
let output_future:t_Slice i16 = output_future in
(Core.Slice.impl__len #i16 output_future <: usize) =.
(Core.Slice.impl__len #i16 output <: usize))
: Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)

val mm_storeu_si128_i32 (output: t_Slice i32) (vector: t_Vec128)
: Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True)

val mm_sub_epi16 (lhs rhs: t_Vec128)
: Prims.Pure t_Vec128
Expand All @@ -198,6 +255,9 @@ val mm_sub_epi16 (lhs rhs: t_Vec128)
vec128_as_i16x8 result ==
Spec.Utils.map2 ( -. ) (vec128_as_i16x8 lhs) (vec128_as_i16x8 rhs))

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

include BitVec.Intrinsics {mm256_and_si256 as mm256_and_si256}
val lemma_mm256_and_si256 lhs rhs
: Lemma ( vec256_as_i16x16 (mm256_and_si256 lhs rhs)
Expand Down
163 changes: 147 additions & 16 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,43 @@ open Core
open FStar.Mul

let inz (value: u8) =
let v__orig_value:u8 = value in
let value:u16 = cast (value <: u8) <: u16 in
let result:u16 =
((value |. (Core.Num.impl__u16__wrapping_add (~.value <: u16) 1us <: u16) <: u16) >>! 8l <: u16) &.
1us
let result:u8 =
cast ((Core.Num.impl__u16__wrapping_add (~.value <: u16) 1us <: u16) >>! 8l <: u16) <: u8
in
cast (result <: u16) <: u8
let res:u8 = result &. 1uy in
let _:Prims.unit =
if v v__orig_value = 0
then
(assert (value == zero);
lognot_lemma value;
assert ((~.value +. 1us) == zero);
assert ((Core.Num.impl__u16__wrapping_add (~.value <: u16) 1us <: u16) == zero);
logor_lemma value zero;
assert ((value |. (Core.Num.impl__u16__wrapping_add (~.value <: u16) 1us <: u16) <: u16) ==
value);
assert (v result == v ((value >>! 8l)));
assert ((v value / pow2 8) == 0);
assert (result == 0uy);
logand_lemma 1uy result;
assert (res == 0uy))
else
(assert (v value <> 0);
lognot_lemma value;
assert (v (~.value) = pow2 16 - 1 - v value);
assert (v (~.value) + 1 = pow2 16 - v value);
assert (v (value) <= pow2 8 - 1);
assert ((v (~.value) + 1) = (pow2 16 - pow2 8) + (pow2 8 - v value));
assert ((v (~.value) + 1) = (pow2 8 - 1) * pow2 8 + (pow2 8 - v value));
assert ((v (~.value) + 1) / pow2 8 = (pow2 8 - 1));
assert (v ((Core.Num.impl__u16__wrapping_add (~.value <: u16) 1us <: u16) >>! 8l) =
pow2 8 - 1);
assert (result = ones);
logand_lemma 1uy result;
assert (res = 1uy))
in
res

let is_non_zero (value: u8) = Core.Hint.black_box #u8 (inz value <: u8)

Expand All @@ -18,43 +49,143 @@ let compare (lhs rhs: t_Slice u8) =
let r:u8 =
Rust_primitives.Hax.Folds.fold_range (sz 0)
(Core.Slice.impl__len #u8 lhs <: usize)
(fun r temp_1_ ->
(fun r i ->
let r:u8 = r in
let _:usize = temp_1_ in
true)
let i:usize = i in
v i <= Seq.length lhs /\
(if (Seq.slice lhs 0 (v i) = Seq.slice rhs 0 (v i)) then r == 0uy else ~(r == 0uy)))
r
(fun r i ->
let r:u8 = r in
let i:usize = i in
r |. ((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8) <: u8)
let nr:u8 = r |. ((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8) in
let _:Prims.unit =
if r =. 0uy
then
(if (Seq.index lhs (v i) = Seq.index rhs (v i))
then
(logxor_lemma (Seq.index lhs (v i)) (Seq.index rhs (v i));
assert (((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8) = zero);
logor_lemma r ((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8);
assert (nr = r);
assert (forall j. Seq.index (Seq.slice lhs 0 (v i)) j == Seq.index lhs j);
assert (forall j. Seq.index (Seq.slice rhs 0 (v i)) j == Seq.index rhs j);
eq_intro (Seq.slice lhs 0 ((v i) + 1)) (Seq.slice rhs 0 ((v i) + 1)))
else
(logxor_lemma (Seq.index lhs (v i)) (Seq.index rhs (v i));
assert (((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8) <> zero);
logor_lemma r ((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8);
assert (v nr > 0);
assert (Seq.index (Seq.slice lhs 0 ((v i) + 1)) (v i) <>
Seq.index (Seq.slice rhs 0 ((v i) + 1)) (v i));
assert (Seq.slice lhs 0 ((v i) + 1) <> Seq.slice rhs 0 ((v i) + 1))))
else
(logor_lemma r ((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8);
assert (v nr >= v r);
assert (Seq.slice lhs 0 (v i) <> Seq.slice rhs 0 (v i));
if (Seq.slice lhs 0 ((v i) + 1) = Seq.slice rhs 0 ((v i) + 1))
then
(assert (forall j.
j < (v i) + 1 ==>
Seq.index (Seq.slice lhs 0 ((v i) + 1)) j ==
Seq.index (Seq.slice rhs 0 ((v i) + 1)) j);
eq_intro (Seq.slice lhs 0 (v i)) (Seq.slice rhs 0 (v i));
assert (False)))
in
let r:u8 = nr in
r)
in
is_non_zero r

let compare_ciphertexts_in_constant_time (lhs rhs: t_Slice u8) =
Core.Hint.black_box #u8 (compare lhs rhs <: u8)

#push-options "--ifuel 0 --z3rlimit 50"

let select_ct (lhs rhs: t_Slice u8) (selector: u8) =
let mask:u8 = Core.Num.impl__u8__wrapping_sub (is_non_zero selector <: u8) 1uy in
let _:Prims.unit =
assert (if selector = 0uy then mask = ones else mask = zero);
lognot_lemma mask;
assert (if selector = 0uy then ~.mask = zero else ~.mask = ones)
in
let out:t_Array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in
let out:t_Array u8 (sz 32) =
Rust_primitives.Hax.Folds.fold_range (sz 0)
Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE
(fun out temp_1_ ->
(fun out i ->
let out:t_Array u8 (sz 32) = out in
let _:usize = temp_1_ in
true)
let i:usize = i in
v i <= v Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE /\
(forall j.
j < v i ==>
(if (selector =. 0uy)
then Seq.index out j == Seq.index lhs j
else Seq.index out j == Seq.index rhs j)) /\
(forall j. j >= v i ==> Seq.index out j == 0uy))
out
(fun out i ->
let out:t_Array u8 (sz 32) = out in
let i:usize = i in
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
i
(((lhs.[ i ] <: u8) &. mask <: u8) |. ((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8) <: u8)
<:
t_Array u8 (sz 32))
let _:Prims.unit = assert ((out.[ i ] <: u8) = 0uy) in
let outi:u8 =
((lhs.[ i ] <: u8) &. mask <: u8) |. ((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8)
in
let _:Prims.unit =
if (selector = 0uy)
then
(logand_lemma (lhs.[ i ] <: u8) mask;
assert (((lhs.[ i ] <: u8) &. mask <: u8) == (lhs.[ i ] <: u8));
logand_lemma (rhs.[ i ] <: u8) (~.mask);
assert (((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8) == zero);
logor_lemma ((lhs.[ i ] <: u8) &. mask <: u8)
((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8);
assert ((((lhs.[ i ] <: u8) &. mask <: u8) |.
((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8)
<:
u8) ==
(lhs.[ i ] <: u8));
logor_lemma (out.[ i ] <: u8) (lhs.[ i ] <: u8);
assert (((out.[ i ] <: u8) |.
(((lhs.[ i ] <: u8) &. mask <: u8) |.
((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8)
<:
u8)
<:
u8) ==
(lhs.[ i ] <: u8));
assert (outi = (lhs.[ i ] <: u8)))
else
(logand_lemma (lhs.[ i ] <: u8) mask;
assert (((lhs.[ i ] <: u8) &. mask <: u8) == zero);
logand_lemma (rhs.[ i ] <: u8) (~.mask);
assert (((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8) == (rhs.[ i ] <: u8));
logor_lemma (rhs.[ i ] <: u8) zero;
assert ((logor zero (rhs.[ i ] <: u8)) == (rhs.[ i ] <: u8));
assert ((((lhs.[ i ] <: u8) &. mask <: u8) |.
((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8)) ==
(rhs.[ i ] <: u8));
logor_lemma (out.[ i ] <: u8) (rhs.[ i ] <: u8);
assert (((out.[ i ] <: u8) |.
(((lhs.[ i ] <: u8) &. mask <: u8) |.
((rhs.[ i ] <: u8) &. (~.mask <: u8) <: u8)
<:
u8)
<:
u8) ==
(rhs.[ i ] <: u8));
assert (outi = (rhs.[ i ] <: u8)))
in
let out:t_Array u8 (sz 32) =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i outi
in
out)
in
let _:Prims.unit = if (selector =. 0uy) then (eq_intro out lhs) else (eq_intro out rhs) in
out

#pop-options

let select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8) =
Core.Hint.black_box #(t_Array u8 (sz 32)) (select_ct lhs rhs selector <: t_Array u8 (sz 32))

Expand Down
Loading

0 comments on commit a089e86

Please sign in to comment.