Revert changes of vec_permute functions in Lib.IntVector

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
 

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)
 

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 =

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

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

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

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