From b115aec87c11cd6f1fc97a3aa475d248fe1bc4d9 Mon Sep 17 00:00:00 2001 From: mamonet Date: Sat, 25 May 2024 18:49:31 +0300 Subject: [PATCH] Revert changes of vec_permute functions in Lib.IntVector --- code/gf128/Hacl.Spec.GF128.Lemmas.fst | 2 +- code/gf128/Hacl.Spec.GF128.Lemmas.fsti | 6 +-- code/gf128/Hacl.Spec.GF128.Vec.fst | 8 ++-- code/gf128/Hacl.Spec.Gf128.FieldNI.fst | 3 +- lib/Lib.IntVector.fst | 66 ++++++++++++++++++++++++++ lib/Lib.IntVector.fsti | 62 ------------------------ specs/Spec.GF128.fst | 5 +- 7 files changed, 78 insertions(+), 74 deletions(-) diff --git a/code/gf128/Hacl.Spec.GF128.Lemmas.fst b/code/gf128/Hacl.Spec.GF128.Lemmas.fst index 6349cbf548..fada53033a 100644 --- a/code/gf128/Hacl.Spec.GF128.Lemmas.fst +++ b/code/gf128/Hacl.Spec.GF128.Lemmas.fst @@ -11,7 +11,7 @@ open FStar.Tactics.CanonCommSemiring friend Lib.IntTypes let add_identity a = - FStar.UInt.logxor_commutative #128 (v a) (v #U128 #SEC (zero #S.gf128)); + FStar.UInt.logxor_commutative #128 (v a) (v #U128 #SEC (zero #S.gf128_le)); FStar.UInt.logxor_lemma_1 #128 (v a); v_extensionality (zero ^. a) a diff --git a/code/gf128/Hacl.Spec.GF128.Lemmas.fsti b/code/gf128/Hacl.Spec.GF128.Lemmas.fsti index 7877df184b..3b03ad44a3 100644 --- a/code/gf128/Hacl.Spec.GF128.Lemmas.fsti +++ b/code/gf128/Hacl.Spec.GF128.Lemmas.fsti @@ -8,12 +8,12 @@ module S = Spec.GF128 #set-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0" -let elem = S.elem +let elem = S.elem_le let zero : elem = zero let one : elem = one -let ( +% ) (a b:elem) : elem = fadd #S.gf128 a b -let ( *% ) (a b:elem) : elem = fmul_be #S.gf128 a b +let ( +% ) (a b:elem) : elem = fadd #S.gf128_le a b +let ( *% ) (a b:elem) : elem = S.fmul_le a b val add_identity: a:elem -> Lemma (zero +% a == a) diff --git a/code/gf128/Hacl.Spec.GF128.Vec.fst b/code/gf128/Hacl.Spec.GF128.Vec.fst index 8763b481f5..b83f8dc689 100644 --- a/code/gf128/Hacl.Spec.GF128.Vec.fst +++ b/code/gf128/Hacl.Spec.GF128.Vec.fst @@ -24,7 +24,7 @@ let elem2 = lseq elem 2 let elem4 = lseq elem 4 let fadd4 (a:elem4) (b:elem4) : elem4 = map2 fadd a b -let fmul4 (a:elem4) (b:elem4) : elem4 = map2 (fun x y -> reverse (fmul (reverse x) (reverse y))) a b +let fmul4 (a:elem4) (b:elem4) : elem4 = map2 Scalar.fmul_le a b let load_elem4 (b:lbytes 64) : elem4 = let b1 = load_felem_be #gf128 (sub b 0 16) in @@ -43,9 +43,9 @@ let normalize4 (pre:elem4) (acc:elem4) : elem = fadd (fadd (fadd a.[0] a.[1]) a.[2]) a.[3] let load_precompute_r (r:elem) : elem4 = - let r2 = reverse (reverse r `fmul` reverse r) in - let r3 = reverse (reverse r `fmul` reverse r2) in - let r4 =reverse (reverse r `fmul` reverse r3) in + let r2 = r `Scalar.fmul_le` r in + let r3 = r `Scalar.fmul_le` r2 in + let r4 =r `Scalar.fmul_le` r3 in create4 r4 r3 r2 r let gf128_update4_add_mul (pre:elem4) (b:lbytes 64) (acc:elem) : Tot elem = diff --git a/code/gf128/Hacl.Spec.Gf128.FieldNI.fst b/code/gf128/Hacl.Spec.Gf128.FieldNI.fst index 09da428715..7708fc6e49 100644 --- a/code/gf128/Hacl.Spec.Gf128.FieldNI.fst +++ b/code/gf128/Hacl.Spec.Gf128.FieldNI.fst @@ -605,8 +605,7 @@ let lemma_gf128_irred_le (_:unit) : Lemma val gf128_clmul_wide_reduce_lemma: x:vec128 -> y:vec128 -> Lemma (let (hi, lo) = clmul_wide x y in - to_elem (gf128_reduce hi lo) == - GF.reverse (GF.fmul #S.gf128_le (GF.reverse (to_elem x)) (GF.reverse (to_elem y)))) + to_elem (gf128_reduce hi lo) == S.fmul_le (to_elem x) (to_elem y)) let gf128_clmul_wide_reduce_lemma x y = lemma_clmul_wide x y; let (hi, lo) = clmul_wide x y in diff --git a/lib/Lib.IntVector.fst b/lib/Lib.IntVector.fst index 2f050d5a39..6ec4dd4315 100644 --- a/lib/Lib.IntVector.fst +++ b/lib/Lib.IntVector.fst @@ -332,6 +332,71 @@ let vec_interleave_high_n_lemma_uint64_4_2 v1 v2 = admit() let vec_shift_right_uint128_small2 v1 s = admit() +(* Generic Permutations: Possible on Intel, but not on ARM. + So we comment this out and only leave interleaving and rotate_lanes functions in the API *) +(* +inline_for_extraction +val vec_permute2: #t:v_inttype -> v1:vec_t t 2 + -> i1:vec_index 2 -> i2:vec_index 2 -> + vec_t t 2 + +inline_for_extraction +val vec_permute2_lemma: #t:v_inttype -> v1:vec_t t 2 + -> i1:vec_index 2 -> i2:vec_index 2 -> + Lemma (ensures (vec_v (vec_permute2 v1 i1 i2) == create2 (vec_v v1).[v i1] (vec_v v1).[v i2])) + [SMTPat (vec_v (vec_permute2 v1 i1 i2))] + + +inline_for_extraction +val vec_permute4: #t:v_inttype -> v1:vec_t t 4 + -> i1:vec_index 4 -> i2:vec_index 4 -> i3:vec_index 4 -> i4:vec_index 4 -> + vec_t t 4 + +inline_for_extraction +val vec_permute4_lemma: #t:v_inttype -> v1:vec_t t 4 + -> i1:vec_index 4 -> i2:vec_index 4 -> i3:vec_index 4 -> i4:vec_index 4 -> + Lemma (ensures (vec_v (vec_permute4 v1 i1 i2 i3 i4) == create4 (vec_v v1).[v i1] (vec_v v1).[v i2] (vec_v v1).[v i3] (vec_v v1).[v i4])) + [SMTPat (vec_v (vec_permute4 v1 i1 i2 i3 i4))] + +inline_for_extraction +val vec_permute8: #t:v_inttype -> v1:vec_t t 8 + -> i1:vec_index 8 -> i2:vec_index 8 -> i3:vec_index 8 -> i4:vec_index 8 + -> i5:vec_index 8 -> i6:vec_index 8 -> i7:vec_index 8 -> i8:vec_index 8 -> + v2:vec_t t 8{vec_v v2 == create8 (vec_v v1).[v i1] (vec_v v1).[v i2] (vec_v v1).[v i3] (vec_v v1).[v i4] + (vec_v v1).[v i5] (vec_v v1).[v i6] (vec_v v1).[v i7] (vec_v v1).[v i8]} + +inline_for_extraction +val vec_permute16: #t:v_inttype -> v1:vec_t t 16 + -> i1:vec_index 16 -> i2:vec_index 16 -> i3:vec_index 16 -> i4:vec_index 16 + -> i5:vec_index 16 -> i6:vec_index 16 -> i7:vec_index 16 -> i8:vec_index 16 + -> i9:vec_index 16 -> i10:vec_index 16 -> i11:vec_index 16 -> i12:vec_index 16 + -> i13:vec_index 16 -> i14:vec_index 16 -> i15:vec_index 16 -> i16:vec_index 16 -> + v2:vec_t t 16{let vv1 = vec_v v1 in + vec_v v2 == create16 vv1.[v i1] vv1.[v i2] vv1.[v i3] vv1.[v i4] + vv1.[v i5] vv1.[v i6] vv1.[v i7] vv1.[v i8] + vv1.[v i9] vv1.[v i10] vv1.[v i11] vv1.[v i12] + vv1.[v i13] vv1.[v i14] vv1.[v i15] vv1.[v i16]} + +inline_for_extraction +val vec_permute32: #t:v_inttype -> v1:vec_t t 32 + -> i1:vec_index 16 -> i2:vec_index 16 -> i3:vec_index 16 -> i4:vec_index 16 + -> i5:vec_index 16 -> i6:vec_index 16 -> i7:vec_index 16 -> i8:vec_index 16 + -> i9:vec_index 16 -> i10:vec_index 16 -> i11:vec_index 16 -> i12:vec_index 16 + -> i13:vec_index 16 -> i14:vec_index 16 -> i15:vec_index 16 -> i16:vec_index 16 + -> i17:vec_index 16 -> i18:vec_index 16 -> i19:vec_index 16 -> i20:vec_index 16 + -> i21:vec_index 16 -> i22:vec_index 16 -> i23:vec_index 16 -> i24:vec_index 16 + -> i25:vec_index 16 -> i26:vec_index 16 -> i27:vec_index 16 -> i28:vec_index 16 + -> i29:vec_index 16 -> i30:vec_index 16 -> i31:vec_index 16 -> i32:vec_index 16 -> + v2:vec_t t 32{let vv1 = vec_v v1 in + vec_v v2 == create32 vv1.[v i1] vv1.[v i2] vv1.[v i3] vv1.[v i4] + vv1.[v i5] vv1.[v i6] vv1.[v i7] vv1.[v i8] + vv1.[v i9] vv1.[v i10] vv1.[v i11] vv1.[v i12] + vv1.[v i13] vv1.[v i14] vv1.[v i15] vv1.[v i16] + vv1.[v i17] vv1.[v i18] vv1.[v i19] vv1.[v i20] + vv1.[v i21] vv1.[v i22] vv1.[v i23] vv1.[v i24] + vv1.[v i25] vv1.[v i26] vv1.[v i27] vv1.[v i28] + vv1.[v i29] vv1.[v i30] vv1.[v i31] vv1.[v i32]} + let vec_permute2 #t v i1 i2 = match t with | U64 -> vec128_shuffle64 v i1 i2 @@ -349,6 +414,7 @@ let vec_permute4_lemma #t v i1 i2 i3 i4 = () let vec_permute8 #t v i1 i2 i3 i4 i5 i6 i7 i8 = admit() let vec_permute16 #t = admit() let vec_permute32 #t = admit() +*) let vec_rotate_right_lanes (#t:v_inttype) (#w:width) (x:vec_t t w) (y:rotval t) = match t,w with diff --git a/lib/Lib.IntVector.fsti b/lib/Lib.IntVector.fsti index b7813f15f4..1c49773c3b 100644 --- a/lib/Lib.IntVector.fsti +++ b/lib/Lib.IntVector.fsti @@ -257,68 +257,6 @@ val vec_shift_right_uint128_small2: v1:vec_t U64 4 -> s:shiftval U128{uint_v s % (((vec_v v1).[2] >>. s) |. ((vec_v v1).[3] <<. (64ul -! s))) ((vec_v v1).[3] >>. s)) -inline_for_extraction -val vec_permute2: #t:v_inttype -> v1:vec_t t 2 - -> i1:vec_index 2 -> i2:vec_index 2 -> - vec_t t 2 - -inline_for_extraction -val vec_permute2_lemma: #t:v_inttype -> v1:vec_t t 2 - -> i1:vec_index 2 -> i2:vec_index 2 -> - Lemma (ensures (vec_v (vec_permute2 v1 i1 i2) == Lib.Sequence.create2 (vec_v v1).[v i1] (vec_v v1).[v i2])) - [SMTPat (vec_v (vec_permute2 v1 i1 i2))] - - -inline_for_extraction -val vec_permute4: #t:v_inttype -> v1:vec_t t 4 - -> i1:vec_index 4 -> i2:vec_index 4 -> i3:vec_index 4 -> i4:vec_index 4 -> - vec_t t 4 - -inline_for_extraction -val vec_permute4_lemma: #t:v_inttype -> v1:vec_t t 4 - -> i1:vec_index 4 -> i2:vec_index 4 -> i3:vec_index 4 -> i4:vec_index 4 -> - Lemma (ensures (vec_v (vec_permute4 v1 i1 i2 i3 i4) == Lib.Sequence.create4 (vec_v v1).[v i1] (vec_v v1).[v i2] (vec_v v1).[v i3] (vec_v v1).[v i4])) - [SMTPat (vec_v (vec_permute4 v1 i1 i2 i3 i4))] - -inline_for_extraction -val vec_permute8: #t:v_inttype -> v1:vec_t t 8 - -> i1:vec_index 8 -> i2:vec_index 8 -> i3:vec_index 8 -> i4:vec_index 8 - -> i5:vec_index 8 -> i6:vec_index 8 -> i7:vec_index 8 -> i8:vec_index 8 -> - v2:vec_t t 8{vec_v v2 == Lib.Sequence.create8 (vec_v v1).[v i1] (vec_v v1).[v i2] (vec_v v1).[v i3] (vec_v v1).[v i4] - (vec_v v1).[v i5] (vec_v v1).[v i6] (vec_v v1).[v i7] (vec_v v1).[v i8]} - -inline_for_extraction -val vec_permute16: #t:v_inttype -> v1:vec_t t 16 - -> i1:vec_index 16 -> i2:vec_index 16 -> i3:vec_index 16 -> i4:vec_index 16 - -> i5:vec_index 16 -> i6:vec_index 16 -> i7:vec_index 16 -> i8:vec_index 16 - -> i9:vec_index 16 -> i10:vec_index 16 -> i11:vec_index 16 -> i12:vec_index 16 - -> i13:vec_index 16 -> i14:vec_index 16 -> i15:vec_index 16 -> i16:vec_index 16 -> - v2:vec_t t 16{let vv1 = vec_v v1 in - vec_v v2 == Lib.Sequence.create16 vv1.[v i1] vv1.[v i2] vv1.[v i3] vv1.[v i4] - vv1.[v i5] vv1.[v i6] vv1.[v i7] vv1.[v i8] - vv1.[v i9] vv1.[v i10] vv1.[v i11] vv1.[v i12] - vv1.[v i13] vv1.[v i14] vv1.[v i15] vv1.[v i16]} - -inline_for_extraction -val vec_permute32: #t:v_inttype -> v1:vec_t t 32 - -> i1:vec_index 16 -> i2:vec_index 16 -> i3:vec_index 16 -> i4:vec_index 16 - -> i5:vec_index 16 -> i6:vec_index 16 -> i7:vec_index 16 -> i8:vec_index 16 - -> i9:vec_index 16 -> i10:vec_index 16 -> i11:vec_index 16 -> i12:vec_index 16 - -> i13:vec_index 16 -> i14:vec_index 16 -> i15:vec_index 16 -> i16:vec_index 16 - -> i17:vec_index 16 -> i18:vec_index 16 -> i19:vec_index 16 -> i20:vec_index 16 - -> i21:vec_index 16 -> i22:vec_index 16 -> i23:vec_index 16 -> i24:vec_index 16 - -> i25:vec_index 16 -> i26:vec_index 16 -> i27:vec_index 16 -> i28:vec_index 16 - -> i29:vec_index 16 -> i30:vec_index 16 -> i31:vec_index 16 -> i32:vec_index 16 -> - v2:vec_t t 32{let vv1 = vec_v v1 in - vec_v v2 == Lib.Sequence.create32 vv1.[v i1] vv1.[v i2] vv1.[v i3] vv1.[v i4] - vv1.[v i5] vv1.[v i6] vv1.[v i7] vv1.[v i8] - vv1.[v i9] vv1.[v i10] vv1.[v i11] vv1.[v i12] - vv1.[v i13] vv1.[v i14] vv1.[v i15] vv1.[v i16] - vv1.[v i17] vv1.[v i18] vv1.[v i19] vv1.[v i20] - vv1.[v i21] vv1.[v i22] vv1.[v i23] vv1.[v i24] - vv1.[v i25] vv1.[v i26] vv1.[v i27] vv1.[v i28] - vv1.[v i29] vv1.[v i30] vv1.[v i31] vv1.[v i32]} - inline_for_extraction val vec_rotate_right_lanes: #t:v_inttype -> #w:width -> v1:vec_t t w -> s:size_t{v s <= w} -> vec_t t w diff --git a/specs/Spec.GF128.fst b/specs/Spec.GF128.fst index d604df9d9f..8902130f5f 100644 --- a/specs/Spec.GF128.fst +++ b/specs/Spec.GF128.fst @@ -21,6 +21,7 @@ let store_elem (e:elem) : lbytes 16 = store_felem_be #gf128 e let irred_le = mk_int #U128 #SEC 0x87 let gf128_le = gf U128 irred_le let elem_le = felem gf128_le +let fmul_le (a b:elem_le) = reverse (fmul (reverse a) (reverse b)) (* GCM types and specs *) let size_block : size_nat = 16 @@ -46,13 +47,13 @@ let gf128_init (h:lbytes size_block) : Tot (elem & elem) = zero, r let gf128_update1 (r:elem) (b:lbytes size_block) (acc:elem) : Tot elem = - (acc `fadd` encode b) `fmul_be` r + (acc `fadd` encode b) `fmul_le` r let gf128_finish (s:key) (acc:elem) : Tot tag = decode (acc `fadd` load_elem s) let gf128_update_last (r:elem) (l:size_nat{l < size_block}) (b:lbytes l) (acc:elem) = - if l = 0 then acc else (acc `fadd` encode_last l b) `fmul_be` r + if l = 0 then acc else (acc `fadd` encode_last l b) `fmul_le` r let gf128_update (text:bytes) (acc:elem) (r:elem) : Tot elem = repeat_blocks #uint8 #elem size_block text