val load_felem5_4_compact: lo:uint64xN 4 -> hi:uint64xN 4 -> felem5 4
let load_felem5_4_compact lo hi =
  let mask26 = mask26 4 in
  let t3 = vec_or (vec_shift_right lo 48ul) (vec_shift_left hi 16ul) in
  let o0 = vec_and lo mask26 in
  let o1 = vec_and (vec_shift_right lo 26ul) mask26 in
  let o2 = vec_and (vec_shift_right t3 4ul) mask26 in
  let o3 = vec_and (vec_shift_right t3 30ul) mask26 in
  let o4 = vec_shift_right hi 40ul in
  (o0, o1, o2, o3, o4)
val load_felem5_4_compact: lo:uint64xN 4 -> hi:uint64xN 4 -> felem5 4
let load_felem5_4_compact lo hi =
let mask26 = mask26 4 in
let t3 = vec_or (vec_shift_right lo 48ul) (vec_shift_left hi 16ul) in
let o0 = vec_and lo mask26 in
let o1 = vec_and (vec_shift_right lo 26ul) mask26 in
let o2 = vec_and (vec_shift_right t3 4ul) mask26 in
let o3 = vec_and (vec_shift_right t3 30ul) mask26 in
let o4 = vec_shift_right hi 40ul in
(o0, o1, o2, o3, o4)
Hacl.Spec.Poly1305.Field32xN.Lemmas.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Field32xN.fst.checked Hacl.Poly1305.Field32xN.Lemmas2.fst.checked Hacl.Poly1305.Field32xN.Lemmas1.fst.checked Hacl.Poly1305.Field32xN.Lemmas0.fst.checked Hacl.Impl.Poly1305.Lemmas.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.Poly1305.Field32xN.Lemmas.fst
Hacl.Spec.Poly1305.Field32xN.uint64xN FStar.Pervasives.Native.Mktuple5 Lib.IntVector.vec_t Lib.IntTypes.U64 Prims.eq2 Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.SEC Lib.IntVector.vec_v Lib.Sequence.map Lib.IntTypes.shift_right_i FStar.UInt32.uint_to_t FStar.UInt32.t Lib.IntVector.vec_shift_right FStar.UInt32.__uint_to_t Lib.IntVector.vec_and Lib.Sequence.map2 Lib.IntTypes.logor Lib.IntVector.vec_shift_left Lib.IntVector.vec_or Lib.Sequence.create Lib.IntTypes.mk_int Hacl.Spec.Poly1305.Field32xN.mask26 Hacl.Spec.Poly1305.Field32xN.felem5
module Hacl.Spec.Poly1305.Field32xN.Lemmas

open Lib.IntTypes
open Lib.IntVector
open Lib.Sequence
open FStar.Mul

open Hacl.Spec.Poly1305.Field32xN
open Hacl.Poly1305.Field32xN.Lemmas0
open Hacl.Poly1305.Field32xN.Lemmas1
open Hacl.Poly1305.Field32xN.Lemmas2

module Vec = Hacl.Spec.Poly1305.Vec

#set-options "--z3rlimit 100 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1 --using_facts_from '* -FStar.Seq'"


val lemma_feval_is_fas_nat_i:
  #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)}
  -> i:size_nat{i < w} ->
  Lemma ((feval5 f).[i] == (fas_nat5 f).[i])

let lemma_feval_is_fas_nat_i #w f i =
  assert_norm (pow2 128 < Vec.prime);
  assert ((feval5 f).[i] == (as_nat5 (transpose f).[i]) % Vec.prime);
  FStar.Math.Lemmas.modulo_lemma (as_nat5 (transpose f).[i]) Vec.prime

val lemma_feval_is_fas_nat:
    #w:lanes
  -> f:felem5 w{felem_less5 f (pow2 128)} ->
  Lemma (forall (i:nat). i < w ==> (fas_nat5 f).[i] == (feval5 f).[i])

let lemma_feval_is_fas_nat #w f =
  FStar.Classical.forall_intro (lemma_feval_is_fas_nat_i #w f)


val precomp_r5_fits_lemma:
    #w:lanes
  -> r:felem5 w{felem_fits5 r (1, 1, 1, 1, 1)} ->
  Lemma (felem_fits5 (precomp_r5 #w r) (5, 5, 5, 5, 5))
  [SMTPat (precomp_r5 #w r)]

let precomp_r5_fits_lemma #w r =
  FStar.Classical.forall_intro (precomp_r5_as_tup64 #w r)


val precomp_r5_fits_lemma2:
    #w:lanes
  -> r:felem5 w{felem_fits5 r (2, 2, 2, 2, 2)} ->
  Lemma (felem_fits5 (precomp_r5 #w r) (10, 10, 10, 10, 10))
  [SMTPat (precomp_r5 #w r)]

let precomp_r5_fits_lemma2 #w r =
  FStar.Classical.forall_intro (precomp_r5_as_tup64 #w r)


val precomp_r5_zeros: w:lanes -> Lemma
  (let r = (zero w, zero w, zero w, zero w, zero w) in
   precomp_r5 r == (zero w, zero w, zero w, zero w, zero w))

let precomp_r5_zeros w =
  let r = (zero w, zero w, zero w, zero w, zero w) in
  let (r0, r1, r2, r3, r4) = precomp_r5 r in

  let aux (i:nat{i < w}) : Lemma ((vec_v (vec_smul_mod (zero w) (u64 5))).[i] == u64 0) = () in
  Classical.forall_intro aux;
  eq_intro (vec_v (vec_smul_mod (zero w) (u64 5))) (vec_v (zero w));
  vecv_extensionality (vec_smul_mod (zero w) (u64 5)) (zero w)


val fadd5_fits_lemma:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (2,2,2,2,2)}
  -> f2:felem5 w{felem_fits5 f2 (1,1,1,1,1)} ->
  Lemma (felem_fits5 (fadd5 f1 f2) (3,3,3,3,3))
  [SMTPat (fadd5 f1 f2)]

let fadd5_fits_lemma #w f1 f2 =
  let (f10, f11, f12, f13, f14) = f1 in
  let (f20, f21, f22, f23, f24) = f2 in
  let o = fadd5 f1 f2 in
  vec_add_mod_lemma f10 f20;
  vec_add_mod_lemma f11 f21;
  vec_add_mod_lemma f12 f22;
  vec_add_mod_lemma f13 f23;
  vec_add_mod_lemma f14 f24


val fadd5_eval_lemma:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (2,2,2,2,2)}
  -> f2:felem5 w{felem_fits5 f2 (1,1,1,1,1)} ->
  Lemma (feval5 (fadd5 f1 f2) == map2 Vec.pfadd (feval5 f1) (feval5 f2))
  [SMTPat (fadd5 f1 f2)]

let fadd5_eval_lemma #w f1 f2 =
  let o = fadd5 f1 f2 in
  FStar.Classical.forall_intro (fadd5_eval_lemma_i f1 f2);
  eq_intro (feval5 o) (map2 Vec.pfadd (feval5 f1) (feval5 f2))


val mul_felem5_fits_lemma:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (3, 3, 3, 3, 3)}
  -> r:felem5 w{felem_fits5 r (2, 2, 2, 2, 2)}
  -> r5:felem5 w{felem_fits5 r5 (10, 10, 10, 10, 10)} ->
  Lemma (felem_wide_fits5 (mul_felem5 #w f1 r r5) (126, 102, 78, 54, 30))
  [SMTPat (mul_felem5 #w f1 r r5)]

let mul_felem5_fits_lemma #w f1 r r5 =
  let (r0, r1, r2, r3, r4) = r in
  let (f10, f11, f12, f13, f14) = f1 in
  let (r50, r51, r52, r53, r54) = r5 in

  let (a0,a1,a2,a3,a4) = smul_felem5 #w f10 (r0,r1,r2,r3,r4) in
  smul_felem5_fits_lemma #w #3 #(2,2,2,2,2) f10 (r0,r1,r2,r3,r4);
  let (a10,a11,a12,a13,a14) = smul_add_felem5 #w f11 (r54,r0,r1,r2,r3) (a0,a1,a2,a3,a4) in
  smul_add_felem5_fits_lemma #w #3 #(10,2,2,2,2) #(6,6,6,6,6) f11 (r54,r0,r1,r2,r3) (a0,a1,a2,a3,a4);
  let (a20,a21,a22,a23,a24) = smul_add_felem5 #w f12 (r53,r54,r0,r1,r2) (a10,a11,a12,a13,a14) in
  smul_add_felem5_fits_lemma #w #3 #(10,10,2,2,2) #(36,12,12,12,12) f12 (r53,r54,r0,r1,r2) (a10,a11,a12,a13,a14);
  let (a30,a31,a32,a33,a34) = smul_add_felem5 #w f13 (r52,r53,r54,r0,r1) (a20,a21,a22,a23,a24) in
  smul_add_felem5_fits_lemma #w #3 #(10,10,10,2,2) #(66,42,18,18,18) f13 (r52,r53,r54,r0,r1) (a20,a21,a22,a23,a24);
  let (a40,a41,a42,a43,a44) = smul_add_felem5 #w f14 (r51,r52,r53,r54,r0) (a30,a31,a32,a33,a34) in
  smul_add_felem5_fits_lemma #w #3 #(10,10,10,10,2) #(96,72,48,24,24) f14 (r51,r52,r53,r54,r0) (a30,a31,a32,a33,a34)


val mul_felem5_eval_lemma_i:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (3, 3, 3, 3, 3)}
  -> r:felem5 w{felem_fits5 r (2, 2, 2, 2, 2)}
  -> r5:felem5 w{felem_fits5 r5 (10, 10, 10, 10, 10) /\ r5 == precomp_r5 r}
  -> i:nat{i < w} ->
  Lemma ((feval5 (mul_felem5 #w f1 r r5)).[i] == (feval5 f1).[i] `Vec.pfmul` (feval5 r).[i])

let mul_felem5_eval_lemma_i #w f1 r r5 i =
  let (r0, r1, r2, r3, r4) = r in
  let (f10, f11, f12, f13, f14) = f1 in
  let (r50, r51, r52, r53, r54) = r5 in

  let (a0,a1,a2,a3,a4) = smul_felem5 #w f10 (r0,r1,r2,r3,r4) in
  smul_felem5_eval_lemma #w #3 #(2,2,2,2,2) f10 (r0,r1,r2,r3,r4);
  smul_felem5_fits_lemma #w #3 #(2,2,2,2,2) f10 (r0,r1,r2,r3,r4);
  assert ((fas_nat5 (a0,a1,a2,a3,a4)).[i] == (uint64xN_v f10).[i] * (fas_nat5 (r0,r1,r2,r3,r4)).[i]);
  let (a10,a11,a12,a13,a14) = smul_add_felem5 #w f11 (r54,r0,r1,r2,r3) (a0,a1,a2,a3,a4) in
  smul_add_felem5_eval_lemma #w #3 #(10,2,2,2,2) #(6,6,6,6,6) f11 (r54,r0,r1,r2,r3) (a0,a1,a2,a3,a4);
  smul_add_felem5_fits_lemma #w #3 #(10,2,2,2,2) #(6,6,6,6,6) f11 (r54,r0,r1,r2,r3) (a0,a1,a2,a3,a4);
  assert ((fas_nat5 (a10,a11,a12,a13,a14)).[i] == (fas_nat5 (a0,a1,a2,a3,a4)).[i] + (uint64xN_v f11).[i] * (fas_nat5 (r54,r0,r1,r2,r3)).[i]);
  let (a20,a21,a22,a23,a24) = smul_add_felem5 #w f12 (r53,r54,r0,r1,r2) (a10,a11,a12,a13,a14) in
  smul_add_felem5_eval_lemma #w #3 #(10,10,2,2,2) #(36,12,12,12,12) f12 (r53,r54,r0,r1,r2) (a10,a11,a12,a13,a14);
  smul_add_felem5_fits_lemma #w #3 #(10,10,2,2,2) #(36,12,12,12,12) f12 (r53,r54,r0,r1,r2) (a10,a11,a12,a13,a14);
  assert ((fas_nat5 (a20,a21,a22,a23,a24)).[i] == (fas_nat5 (a10,a11,a12,a13,a14)).[i] + (uint64xN_v f12).[i] * (fas_nat5 (r53,r54,r0,r1,r2)).[i]);
  let (a30,a31,a32,a33,a34) = smul_add_felem5 #w f13 (r52,r53,r54,r0,r1) (a20,a21,a22,a23,a24) in
  smul_add_felem5_eval_lemma #w #3 #(10,10,10,2,2) #(66,42,18,18,18) f13 (r52,r53,r54,r0,r1) (a20,a21,a22,a23,a24);
  smul_add_felem5_fits_lemma #w #3 #(10,10,10,2,2) #(66,42,18,18,18) f13 (r52,r53,r54,r0,r1) (a20,a21,a22,a23,a24);
  assert ((fas_nat5 (a30,a31,a32,a33,a34)).[i] == (fas_nat5 (a20,a21,a22,a23,a24)).[i] + (uint64xN_v f13).[i] * (fas_nat5 (r52,r53,r54,r0,r1)).[i]);
  let (a40,a41,a42,a43,a44) = smul_add_felem5 #w f14 (r51,r52,r53,r54,r0) (a30,a31,a32,a33,a34) in
  smul_add_felem5_eval_lemma #w #3 #(10,10,10,10,2) #(96,72,48,24,24) f14 (r51,r52,r53,r54,r0) (a30,a31,a32,a33,a34);
  smul_add_felem5_fits_lemma #w #3 #(10,10,10,10,2) #(96,72,48,24,24) f14 (r51,r52,r53,r54,r0) (a30,a31,a32,a33,a34);
  assert ((fas_nat5 (a40,a41,a42,a43,a44)).[i] == (fas_nat5 (a30,a31,a32,a33,a34)).[i] + (uint64xN_v f14).[i] * (fas_nat5 (r51,r52,r53,r54,r0)).[i]);

  assert ((fas_nat5 (a40,a41,a42,a43,a44)).[i] ==
    (uint64xN_v f10).[i] * (fas_nat5 (r0,r1,r2,r3,r4)).[i] +
    (uint64xN_v f11).[i] * (fas_nat5 (r54,r0,r1,r2,r3)).[i] +
    (uint64xN_v f12).[i] * (fas_nat5 (r53,r54,r0,r1,r2)).[i] +
    (uint64xN_v f13).[i] * (fas_nat5 (r52,r53,r54,r0,r1)).[i] +
    (uint64xN_v f14).[i] * (fas_nat5 (r51,r52,r53,r54,r0)).[i]);
  mul_felem5_eval_as_tup64 #w f1 r r5 i;
  mul_felem5_lemma (as_tup64_i f1 i) (as_tup64_i r i)


val mul_felem5_eval_lemma:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (3, 3, 3, 3, 3)}
  -> r:felem5 w{felem_fits5 r (2, 2, 2, 2, 2)}
  -> r5:felem5 w{felem_fits5 r5 (10, 10, 10, 10, 10) /\ r5 == precomp_r5 r} ->
  Lemma (feval5 (mul_felem5 #w f1 r r5) == map2 (Vec.pfmul) (feval5 f1) (feval5 r))
  [SMTPat (mul_felem5 #w f1 r r5)]

let mul_felem5_eval_lemma #w f1 r r5 =
  let tmp = map2 (Vec.pfmul) (feval5 f1) (feval5 r) in
  FStar.Classical.forall_intro (mul_felem5_eval_lemma_i #w f1 r r5);
  eq_intro (feval5 (mul_felem5 #w f1 r r5)) tmp


val fmul_r5_fits_lemma:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (3, 3, 3, 3, 3)}
  -> r:felem5 w{felem_fits5 r (2, 2, 2, 2, 2)}
  -> r5:felem5 w{felem_fits5 r5 (10, 10, 10, 10, 10)} ->
  Lemma (felem_fits5 (fmul_r5 #w f1 r r5) (1, 2, 1, 1, 2))
  [SMTPat (fmul_r5 #w f1 r r5)]

let fmul_r5_fits_lemma #w f1 r r5 =
  let tmp = mul_felem5 f1 r r5 in
  mul_felem5_fits_lemma #w f1 r r5;
  let res = carry_wide_felem5 tmp in
  carry_wide_felem5_fits_lemma #w tmp


val fmul_r5_eval_lemma:
    #w:lanes
  -> f1:felem5 w{felem_fits5 f1 (3, 3, 3, 3, 3)}
  -> r:felem5 w{felem_fits5 r (2, 2, 2, 2, 2)}
  -> r5:felem5 w{felem_fits5 r5 (10, 10, 10, 10, 10) /\ r5 == precomp_r5 r} ->
  Lemma (feval5 (fmul_r5 #w f1 r r5) == map2 (Vec.pfmul) (feval5 f1) (feval5 r))
  [SMTPat (fmul_r5 #w f1 r r5)]

let fmul_r5_eval_lemma #w f1 r r5 =
  let tmp = mul_felem5 f1 r r5 in
  mul_felem5_eval_lemma #w f1 r r5;
  let res = carry_wide_felem5 tmp in
  carry_wide_felem5_eval_lemma #w tmp


val fadd_mul_r5_fits_lemma:
    #w:lanes
  -> acc:felem5 w{felem_fits5 acc (2, 2, 2, 2, 2)}
  -> f1:felem5 w{felem_fits5 f1 (1, 1, 1, 1, 1)}
  -> r:felem5 w{felem_fits5 r (1, 1, 1, 1, 1)}
  -> r5:felem5 w{felem_fits5 r5 (5, 5, 5, 5, 5)} ->
  Lemma (felem_fits5 (fadd_mul_r5 acc f1 r r5) (1, 2, 1, 1, 2))
  [SMTPat (fadd_mul_r5 acc f1 r r5)]

let fadd_mul_r5_fits_lemma #w acc f1 r r5 =
  let acc1 = fadd5 acc f1 in
  fadd5_fits_lemma #w acc f1;
  let tmp = mul_felem5 acc1 r r5 in
  mul_felem5_fits_lemma #w acc1 r r5;
  let res = carry_wide_felem5 tmp in
  carry_wide_felem5_fits_lemma #w tmp


val fadd_mul_r5_eval_lemma:
    #w:lanes
  -> acc:felem5 w{felem_fits5 acc (2, 2, 2, 2, 2)}
  -> f1:felem5 w{felem_fits5 f1 (1, 1, 1, 1, 1)}
  -> r:felem5 w{felem_fits5 r (1, 1, 1, 1, 1)}
  -> r5:felem5 w{felem_fits5 r5 (5, 5, 5, 5, 5) /\ r5 == precomp_r5 r} ->
  Lemma (feval5 (fadd_mul_r5 acc f1 r r5) ==
    map2 (Vec.pfmul) (map2 (Vec.pfadd) (feval5 acc) (feval5 f1)) (feval5 r))
  [SMTPat (fadd_mul_r5 acc f1 r r5)]

let fadd_mul_r5_eval_lemma #w acc f1 r r5 =
  let acc1 = fadd5 acc f1 in
  fadd5_eval_lemma #w acc f1;
  let tmp = mul_felem5 acc1 r r5 in
  mul_felem5_eval_lemma #w acc1 r r5;
  let res = carry_wide_felem5 tmp in
  carry_wide_felem5_eval_lemma #w tmp


val reduce_felem5_eval_lemma:
    #w:lanes
  -> f:felem5 w{felem_fits5 f (2, 2, 2, 2, 2)} ->
  Lemma
  (felem_fits5 (reduce_felem5 f) (1, 1, 1, 1, 1) /\
   (feval5 f).[0] == (fas_nat5 (reduce_felem5 f)).[0])
  [SMTPat (reduce_felem5 f)]

let reduce_felem5_eval_lemma #w f =
  carry_full_felem5_eval_lemma f;
  carry_full_felem5_fits_lemma f;
  let f = carry_full_felem5 f in
  carry_reduce_felem5_lemma #w f;
  subtract_p5_felem5_lemma #w (carry_full_felem5 f)


val fmul_r2_normalize50:
    acc:felem5 2
  -> r:felem5 2
  -> r2:felem5 2 ->
  Pure (felem5 2)
  (requires
    felem_fits5 acc (3, 3, 3, 3, 3) /\
    felem_fits5 r (1, 1, 1, 1, 1) /\
    felem_fits5 r2 (2, 2, 2, 2, 2) /\
    feval5 r2 == Vec.compute_r2 (feval5 r).[0])
  (ensures fun a ->
    let fr21 = create2 (feval5 r2).[0] (feval5 r).[0] in
    feval5 a == Vec.fmul (feval5 acc) fr21 /\
    felem_fits5 a (1, 2, 1, 1, 2))

let fmul_r2_normalize50 (a0, a1, a2, a3, a4) (r0, r1, r2, r3, r4) (r20, r21, r22, r23, r24) =
  let r210 = vec_interleave_low r20 r0 in
  vec_interleave_low_lemma2 r20 r0;
  let r211 = vec_interleave_low r21 r1 in
  vec_interleave_low_lemma2 r21 r1;
  let r212 = vec_interleave_low r22 r2 in
  vec_interleave_low_lemma2 r22 r2;
  let r213 = vec_interleave_low r23 r3 in
  vec_interleave_low_lemma2 r23 r3;
  let r214 = vec_interleave_low r24 r4 in
  vec_interleave_low_lemma2 r24 r4;

  let acc = (a0, a1, a2, a3, a4) in
  let fr = (r0, r1, r2, r3, r4) in
  let fr2 = (r20, r21, r22, r23, r24) in
  assert ((feval5 fr2).[0] == Vec.pfmul ((feval5 fr).[0]) ((feval5 fr).[0]));

  let fr21 = (r210, r211, r212, r213, r214) in
  eq_intro (feval5 fr21) (create2 (feval5 fr2).[0] (feval5 fr).[0]);
  assert (feval5 fr21 == create2 (feval5 fr2).[0] (feval5 fr).[0]);

  assert (felem_fits5 fr21 (2, 2, 2, 2, 2));
  let fr215 = precomp_r5 #2 fr21 in
  let a = fmul_r5 #2 acc fr21 fr215 in
  fmul_r5_eval_lemma acc fr21 fr215;
  fmul_r5_fits_lemma acc fr21 fr215;
  assert (feval5 a == Vec.fmul (feval5 acc) (feval5 fr21));
  assert (felem_fits5 a (1, 2, 1, 1, 2));
  a


#push-options "--z3rlimit 150"
val fmul_r2_normalize51:
    a:felem5 2
  -> fa1:felem5 2 ->
  Pure (felem5 2)
  (requires
    felem_fits5 a (1, 2, 1, 1, 2) /\
    felem_fits5 fa1 (1, 2, 1, 1, 2) /\
    feval5 fa1 == create2 (feval5 a).[1] (feval5 a).[1])
  (ensures fun out ->
    (feval5 out).[0] == Vec.pfadd (feval5 a).[0] (feval5 a).[1] /\
    felem_fits5 out (2, 4, 2, 2, 4))

let fmul_r2_normalize51 a fa1 =
  let (a0, a1, a2, a3, a4) = a in
  let (a10, a11, a12, a13, a14) = fa1 in
  let o0 = vec_add_mod a0 a10 in
  let o1 = vec_add_mod a1 a11 in
  let o2 = vec_add_mod a2 a12 in
  let o3 = vec_add_mod a3 a13 in
  let o4 = vec_add_mod a4 a14 in
  let out = (o0, o1, o2, o3, o4) in

  let (a0, a1, a2, a3, a4) = as_tup64_i a 0 in
  let (a10, a11, a12, a13, a14) = as_tup64_i fa1 0 in
  let (o0, o1, o2, o3, o4) = as_tup64_i out 0 in

  FStar.Math.Lemmas.modulo_lemma (v a0 + v a10) (pow2 64);
  FStar.Math.Lemmas.modulo_lemma (v a1 + v a11) (pow2 64);
  FStar.Math.Lemmas.modulo_lemma (v a2 + v a12) (pow2 64);
  FStar.Math.Lemmas.modulo_lemma (v a3 + v a13) (pow2 64);
  FStar.Math.Lemmas.modulo_lemma (v a4 + v a14) (pow2 64);
  assert (felem_fits5 out (2, 4, 2, 2, 4));

  calc (==) {
    ((feval5 a).[0] + (feval5 a).[1]) % Vec.prime;
    (==) { }
    (as_nat5 (a0, a1, a2, a3, a4) % Vec.prime + as_nat5 (a10, a11, a12, a13, a14) % Vec.prime) % Vec.prime;
    (==) { FStar.Math.Lemmas.lemma_mod_plus_distr_l
    (as_nat5 (a0, a1, a2, a3, a4)) (as_nat5 (a10, a11, a12, a13, a14)) Vec.prime;
  FStar.Math.Lemmas.lemma_mod_plus_distr_r
    (as_nat5 (a0, a1, a2, a3, a4) % Vec.prime) (as_nat5 (a10, a11, a12, a13, a14)) Vec.prime }
    (as_nat5 (a0, a1, a2, a3, a4) + as_nat5 (a10, a11, a12, a13, a14)) % Vec.prime;
    (==) { }
    (feval5 out).[0];
  };
  out
#pop-options


val fmul_r2_normalize5_lemma:
    acc:felem5 2
  -> r:felem5 2
  -> r2:felem5 2 ->
  Lemma
  (requires
    felem_fits5 acc (3, 3, 3, 3, 3) /\
    felem_fits5 r (1, 1, 1, 1, 1) /\
    felem_fits5 r2 (2, 2, 2, 2, 2) /\
    feval5 r2 == Vec.compute_r2 (feval5 r).[0])
  (ensures
    (let out = fmul_r2_normalize5 acc r r2 in
    felem_fits5 out (2, 1, 1, 1, 1) /\
    (feval5 out).[0] == Vec.normalize_2 (feval5 r).[0] (feval5 acc)))
  [SMTPat (fmul_r2_normalize5 acc r r2)]

let fmul_r2_normalize5_lemma acc r r2 =
  let a = fmul_r2_normalize50 acc r r2 in
  let (a0, a1, a2, a3, a4) = a in

  let a10 = vec_interleave_high a0 a0 in
  vec_interleave_high_lemma2 a0 a0;
  let a11 = vec_interleave_high a1 a1 in
  vec_interleave_high_lemma2 a1 a1;
  let a12 = vec_interleave_high a2 a2 in
  vec_interleave_high_lemma2 a2 a2;
  let a13 = vec_interleave_high a3 a3 in
  vec_interleave_high_lemma2 a3 a3;
  let a14 = vec_interleave_high a4 a4 in
  vec_interleave_high_lemma2 a4 a4;
  let fa1 = (a10, a11, a12, a13, a14) in
  eq_intro (feval5 fa1) (create2 (feval5 a).[1] (feval5 a).[1]);
  assert (feval5 fa1 == create2 (feval5 a).[1] (feval5 a).[1]);
  assert (felem_fits5 fa1 (1, 2, 1, 1, 2));

  let out = fmul_r2_normalize51 a fa1 in
  assert ((feval5 out).[0] == Vec.pfadd (feval5 a).[0] (feval5 a).[1]);

  let res = carry_full_felem5 out in
  carry_full_felem5_lemma out


val fmul_r4_normalize50:
    acc:felem5 4
  -> r:felem5 4
  -> r2:felem5 4
  -> r3:felem5 4
  -> r4:felem5 4 ->
  Pure (felem5 4)
  (requires
    felem_fits5 acc (3, 3, 3, 3, 3) /\
    felem_fits5 r (1, 1, 1, 1, 1) /\
    felem_fits5 r2 (2, 2, 2, 2, 2) /\
    felem_fits5 r3 (2, 2, 2, 2, 2) /\
    felem_fits5 r4 (2, 2, 2, 2, 2) /\
    feval5 r2 == Vec.fmul (feval5 r) (feval5 r) /\
    feval5 r3 == Vec.fmul (feval5 r2) (feval5 r) /\
    feval5 r4 == Vec.compute_r4 (feval5 r).[0])
  (ensures fun out ->
    let fr4321 = create4 (feval5 r4).[0] (feval5 r3).[0] (feval5 r2).[0] (feval5 r).[0] in
    feval5 out == Vec.fmul (feval5 acc) fr4321 /\
    felem_fits5 out (1, 2, 1, 1, 2))

let fmul_r4_normalize50 acc fr fr2 fr3 fr4 =
  let (r10, r11, r12, r13, r14) = fr in
  let (r20, r21, r22, r23, r24) = fr2 in
  let (r30, r31, r32, r33, r34) = fr3 in
  let (r40, r41, r42, r43, r44) = fr4 in
  let (a0, a1, a2, a3, a4) = acc in

  let v12120 = vec_interleave_low r20 r10 in
  vec_interleave_low_lemma_uint64_4 r20 r10;
  let v34340 = vec_interleave_low r40 r30 in
  vec_interleave_low_lemma_uint64_4 r40 r30;
  let r12340 = vec_interleave_low_n 2 v34340 v12120 in
  vec_interleave_low_n_lemma_uint64_4_2 v34340 v12120;

  let v12121 = vec_interleave_low r21 r11 in
  vec_interleave_low_lemma_uint64_4 r21 r11;
  let v34341 = vec_interleave_low r41 r31 in
  vec_interleave_low_lemma_uint64_4 r41 r31;
  let r12341 = vec_interleave_low_n 2 v34341 v12121 in
  vec_interleave_low_n_lemma_uint64_4_2 v34341 v12121;

  let v12122 = vec_interleave_low r22 r12 in
  vec_interleave_low_lemma_uint64_4 r22 r12;
  let v34342 = vec_interleave_low r42 r32 in
  vec_interleave_low_lemma_uint64_4 r42 r32;
  let r12342 = vec_interleave_low_n 2 v34342 v12122 in
  vec_interleave_low_n_lemma_uint64_4_2 v34342 v12122;

  let v12123 = vec_interleave_low r23 r13 in
  vec_interleave_low_lemma_uint64_4 r23 r13;
  let v34343 = vec_interleave_low r43 r33 in
  vec_interleave_low_lemma_uint64_4 r43 r33;
  let r12343 = vec_interleave_low_n 2 v34343 v12123 in
  vec_interleave_low_n_lemma_uint64_4_2 v34343 v12123;

  let v12124 = vec_interleave_low r24 r14 in
  vec_interleave_low_lemma_uint64_4 r24 r14;
  let v34344 = vec_interleave_low r44 r34 in
  vec_interleave_low_lemma_uint64_4 r44 r34;
  let r12344 = vec_interleave_low_n 2 v34344 v12124 in
  vec_interleave_low_n_lemma_uint64_4_2 v34344 v12124;

  let fr1234 = (r12340, r12341, r12342, r12343, r12344) in
  eq_intro (feval5 fr1234) (create4 (feval5 fr4).[0] (feval5 fr3).[0] (feval5 fr2).[0] (feval5 fr).[0]);

  let fr12345 = precomp_r5 #4 fr1234 in
  let out = fmul_r5 #4 acc fr1234 fr12345 in
  fmul_r5_eval_lemma acc fr1234 fr12345;
  fmul_r5_fits_lemma acc fr1234 fr12345;
  out


val lemma_fmul_r4_normalize51:
    #m:scale32{m <= 2}
  -> o:uint64xN 4{felem_fits1 o m} ->
  Lemma
  (let v00 = vec_interleave_high_n 2 o o in
   let v10 = vec_add_mod o v00 in
   let v10h = vec_interleave_high v10 v10 in
   let v20 = vec_add_mod v10 v10h in
   felem_fits1 v20 (4 * m) /\
   (uint64xN_v v20).[0] == (uint64xN_v o).[0] + (uint64xN_v o).[1] + (uint64xN_v o).[2] + (uint64xN_v o).[3])

let lemma_fmul_r4_normalize51 #m o =
  let v00 = vec_interleave_high_n 2 o o in
  vec_interleave_high_n_lemma_uint64_4_2 o o;
  let (o0, o1, o2, o3) = ((vec_v o).[0], (vec_v o).[1], (vec_v o).[2], (vec_v o).[3]) in
  assert (vec_v v00 == create4 o2 o3 o2 o3);
  let v10 = vec_add_mod o v00 in
  FStar.Math.Lemmas.modulo_lemma (v o0 + v o2) (pow2 64);
  FStar.Math.Lemmas.modulo_lemma (v o1 + v o3) (pow2 64);
  assert (v (vec_v v10).[0] == v o0 + v o2);
  assert (v (vec_v v10).[1] == v o1 + v o3);
  let v10h = vec_interleave_high v10 v10 in
  vec_interleave_high_lemma_uint64_4 v10 v10;
  assert (v (vec_v v10h).[0] == v (vec_v v10).[1]);
  let v20 = vec_add_mod v10 v10h in
  FStar.Math.Lemmas.modulo_lemma (v o0 + v o2 + v o1 + v o3) (pow2 64)


val lemma_fmul_r4_normalize51_expand:
    v2:felem5 4
  -> out:felem5 4 ->
  Lemma
  (requires
   (let (v20, v21, v22, v23, v24) = v2 in
    let (o0, o1, o2, o3, o4) = out in
    (uint64xN_v v20).[0] == (uint64xN_v o0).[0] + (uint64xN_v o0).[1] + (uint64xN_v o0).[2] + (uint64xN_v o0).[3] /\
    (uint64xN_v v21).[0] == (uint64xN_v o1).[0] + (uint64xN_v o1).[1] + (uint64xN_v o1).[2] + (uint64xN_v o1).[3] /\
    (uint64xN_v v22).[0] == (uint64xN_v o2).[0] + (uint64xN_v o2).[1] + (uint64xN_v o2).[2] + (uint64xN_v o2).[3] /\
    (uint64xN_v v23).[0] == (uint64xN_v o3).[0] + (uint64xN_v o3).[1] + (uint64xN_v o3).[2] + (uint64xN_v o3).[3] /\
    (uint64xN_v v24).[0] == (uint64xN_v o4).[0] + (uint64xN_v o4).[1] + (uint64xN_v o4).[2] + (uint64xN_v o4).[3]))
  (ensures
    (let (v20, v21, v22, v23, v24) = v2 in
     let (o0, o1, o2, o3, o4) = out in
     (feval5 v2).[0] == Vec.pfadd (Vec.pfadd (Vec.pfadd (feval5 out).[0] (feval5 out).[1]) (feval5 out).[2]) (feval5 out).[3]))

let lemma_fmul_r4_normalize51_expand v2 out =
  let (v20, v21, v22, v23, v24) = as_tup64_i v2 0 in
  let (o0, o1, o2, o3, o4) = out in

  calc (==) {
    as_nat5 (v20, v21, v22, v23, v24) % Vec.prime;
    (==) { }
    (as_nat5 (as_tup64_i out 0) + as_nat5 (as_tup64_i out 1) + as_nat5 (as_tup64_i out 2) + as_nat5 (as_tup64_i out 3)) % Vec.prime;
    (==) { FStar.Math.Lemmas.lemma_mod_plus_distr_l (as_nat5 (as_tup64_i out 0) + as_nat5 (as_tup64_i out 1))
	 (as_nat5 (as_tup64_i out 2) + as_nat5 (as_tup64_i out 3)) Vec.prime }
    ((as_nat5 (as_tup64_i out 0) + as_nat5 (as_tup64_i out 1)) % Vec.prime + as_nat5 (as_tup64_i out 2) + as_nat5 (as_tup64_i out 3)) % Vec.prime;
    (==) { FStar.Math.Lemmas.modulo_distributivity (as_nat5 (as_tup64_i out 0)) (as_nat5 (as_tup64_i out 1)) Vec.prime }
    (((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + as_nat5 (as_tup64_i out 2) + as_nat5 (as_tup64_i out 3)) % Vec.prime;
    (==) { FStar.Math.Lemmas.lemma_mod_plus_distr_l (((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + as_nat5 (as_tup64_i out 2))
	(as_nat5 (as_tup64_i out 3)) Vec.prime }
    ((((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + as_nat5 (as_tup64_i out 2)) % Vec.prime + as_nat5 (as_tup64_i out 3)) % Vec.prime;
    (==) { FStar.Math.Lemmas.lemma_mod_plus_distr_r (((feval5 out).[0] + (feval5 out).[1]) % Vec.prime) (as_nat5 (as_tup64_i out 2)) Vec.prime }
    ((((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + (feval5 out).[2]) % Vec.prime + as_nat5 (as_tup64_i out 3)) % Vec.prime;
    (==) { FStar.Math.Lemmas.lemma_mod_plus_distr_r ((((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + (feval5 out).[2]) % Vec.prime)
	 (as_nat5 (as_tup64_i out 3)) Vec.prime }
    ((((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + (feval5 out).[2]) % Vec.prime + (feval5 out).[3]) % Vec.prime;
   };
  assert ((feval5 v2).[0] ==
    ((((feval5 out).[0] + (feval5 out).[1]) % Vec.prime + (feval5 out).[2]) % Vec.prime + (feval5 out).[3]) % Vec.prime)


val fmul_r4_normalize51: a:felem5 4 ->
  Pure (felem5 4)
  (requires felem_fits5 a (1, 2, 1, 1, 2))
  (ensures  fun res ->
    felem_fits5 res (4, 8, 4, 4, 8) /\
    (feval5 res).[0] == Vec.pfadd (Vec.pfadd (Vec.pfadd (feval5 a).[0] (feval5 a).[1]) (feval5 a).[2]) (feval5 a).[3])

let fmul_r4_normalize51 fa =
  let (o0, o1, o2, o3, o4) = fa in
  let v00 = vec_interleave_high_n 2 o0 o0 in
  let v10 = vec_add_mod o0 v00 in
  let v10h = vec_interleave_high v10 v10 in
  let v20 = vec_add_mod v10 v10h in
  lemma_fmul_r4_normalize51 #1 o0;

  let v01 = vec_interleave_high_n 2 o1 o1 in
  let v11 = vec_add_mod o1 v01 in
  let v11h = vec_interleave_high v11 v11 in 
  let v21 = vec_add_mod v11 v11h in
  lemma_fmul_r4_normalize51 #2 o1;

  let v02 = vec_interleave_high_n 2 o2 o2 in
  let v12 = vec_add_mod o2 v02 in
  let v12h = vec_interleave_high v12 v12 in 
  let v22 = vec_add_mod v12 v12h in
  lemma_fmul_r4_normalize51 #1 o2;

  let v03 = vec_interleave_high_n 2 o3 o3 in
  let v13 = vec_add_mod o3 v03 in
  let v13h = vec_interleave_high v13 v13 in 
  let v23 = vec_add_mod v13 v13h in
  lemma_fmul_r4_normalize51 #1 o3;

  let v04 = vec_interleave_high_n 2 o4 o4 in
  let v14 = vec_add_mod o4 v04 in
  let v14h = vec_interleave_high v14 v14 in 
  let v24 = vec_add_mod v14 v14h in
  lemma_fmul_r4_normalize51 #2 o4;
  let res = (v20, v21, v22, v23, v24) in
  lemma_fmul_r4_normalize51_expand res fa;
  res


val fmul_r4_normalize5_lemma:
    acc:felem5 4
  -> r:felem5 4
  -> r_5:felem5 4
  -> r4:felem5 4 ->
  Lemma
  (requires
    felem_fits5 acc (3, 3, 3, 3, 3) /\
    felem_fits5 r (1, 1, 1, 1, 1) /\
    felem_fits5 r4 (2, 2, 2, 2, 2) /\
    r_5 == precomp_r5 r /\
    feval5 r4 == Vec.compute_r4 (feval5 r).[0])
  (ensures
    (let out = fmul_r4_normalize5 acc r r_5 r4 in
     felem_fits5 out (2, 1, 1, 1, 1) /\
    (feval5 out).[0] == Vec.normalize_4 (feval5 r).[0] (feval5 acc)))
  [SMTPat (fmul_r4_normalize5 acc r r_5 r4)]

#restart-solver
#push-options "--z3rlimit 500"
let fmul_r4_normalize5_lemma acc fr fr_5 fr4 =
  let fr2 = fmul_r5 #4 fr fr fr_5 in
  let fr3 = fmul_r5 #4 fr2 fr fr_5 in
  let out = fmul_r4_normalize50 acc fr fr2 fr3 fr4 in
  let v2 = fmul_r4_normalize51 out in
  let res = carry_full_felem5 v2 in
  carry_full_felem5_lemma v2
#pop-options

val load_felem5_lemma:
    #w:lanes
  -> lo:uint64xN w
  -> hi:uint64xN w ->
  Lemma
  (let f = load_felem5 #w lo hi in
   felem_fits5 f (1, 1, 1, 1, 1) /\
   felem_less5 f (pow2 128) /\
   feval5 f == createi #Vec.pfelem w
     (fun i -> (uint64xN_v hi).[i] * pow2 64 + (uint64xN_v lo).[i]))

let load_felem5_lemma #w lo hi =
  let f = load_felem5 #w lo hi in
  assert_norm (pow2 64 * pow2 64 = pow2 128);
  assert_norm (pow2 128 < Vec.prime);
  let res = createi #Vec.pfelem w
    (fun i -> (uint64xN_v hi).[i] * pow2 64 + (uint64xN_v lo).[i]) in

  match w with
  | 1 ->
    load_felem5_lemma_i #w lo hi 0;
    eq_intro (feval5 f) res
  | 2 ->
    load_felem5_lemma_i #w lo hi 0;
    load_felem5_lemma_i #w lo hi 1;
    eq_intro (feval5 f) res
  | 4 ->
    load_felem5_lemma_i #w lo hi 0;
    load_felem5_lemma_i #w lo hi 1;
    load_felem5_lemma_i #w lo hi 2;
    load_felem5_lemma_i #w lo hi 3;
    eq_intro (feval5 f) res

val load_felem5_4_interleave: lo:uint64xN 4 -> hi:uint64xN 4 -> Lemma
  (let m0 = vec_interleave_low_n 2 lo hi in
   let m1 = vec_interleave_high_n 2 lo hi in
   let m2 = cast U64 4 (vec_shift_right (cast U128 2 m0) 48ul) in
   let m3 = cast U64 4 (vec_shift_right (cast U128 2 m1) 48ul) in
   let m4 = vec_interleave_high m0 m1 in
   let t0 = vec_interleave_low m0 m1 in
   let t3 = vec_interleave_low m2 m3 in
   vec_v m4 == create4 (vec_v lo).[1] (vec_v lo).[3] (vec_v hi).[1] (vec_v hi).[3] /\
   vec_v t0 == create4 (vec_v lo).[0] (vec_v lo).[2] (vec_v hi).[0] (vec_v hi).[2] /\
   t3 == vec_or (vec_shift_right t0 48ul) (vec_shift_left m4 16ul))

let load_felem5_4_interleave lo hi =
  let m0 = vec_interleave_low_n 2 lo hi in
  vec_interleave_low_n_lemma_uint64_4_2 lo hi;
  //assert (vec_v m0 == create4 (vec_v lo).[0] (vec_v lo).[1] (vec_v hi).[0] (vec_v hi).[1]);
  let m1 = vec_interleave_high_n 2 lo hi in
  vec_interleave_high_n_lemma_uint64_4_2 lo hi;
  //assert (vec_v m1 == create4 (vec_v lo).[2] (vec_v lo).[3] (vec_v hi).[2] (vec_v hi).[3]);

  let m4 = vec_interleave_high m0 m1 in
  vec_interleave_high_lemma_uint64_4 m0 m1;
  //assert (vec_v m4 == create4 (vec_v m0).[1] (vec_v m1).[1] (vec_v m0).[3] (vec_v m1).[3]);
  assert (vec_v m4 == create4 (vec_v lo).[1] (vec_v lo).[3] (vec_v hi).[1] (vec_v hi).[3]);
  let t0 = vec_interleave_low m0 m1 in
  vec_interleave_low_lemma_uint64_4 m0 m1;
  //assert (vec_v t0 == create4 (vec_v m0).[0] (vec_v m1).[0] (vec_v m0).[2] (vec_v m1).[2]);
  assert (vec_v t0 == create4 (vec_v lo).[0] (vec_v lo).[2] (vec_v hi).[0] (vec_v hi).[2]);

  let m2 = cast U64 4 (vec_shift_right (cast U128 2 m0) 48ul) in
  vec_shift_right_uint128_small2 m0 48ul;
  assert ((vec_v m2).[0] == (((vec_v lo).[0] >>. 48ul) |. ((vec_v lo).[1] <<. 16ul)));
  assert ((vec_v m2).[2] == (((vec_v hi).[0] >>. 48ul) |. ((vec_v hi).[1] <<. 16ul)));
  let m3 = cast U64 4 (vec_shift_right (cast U128 2 m1) 48ul) in
  vec_shift_right_uint128_small2 m1 48ul;
  assert ((vec_v m3).[0] == (((vec_v lo).[2] >>. 48ul) |. ((vec_v lo).[3] <<. 16ul)));
  assert ((vec_v m3).[2] == (((vec_v hi).[2] >>. 48ul) |. ((vec_v hi).[3] <<. 16ul)));

  let t3 = vec_interleave_low m2 m3 in
  vec_interleave_low_lemma_uint64_4 m2 m3;
  eq_intro (vec_v t3) (vec_v (vec_or (vec_shift_right t0 48ul) (vec_shift_left m4 16ul)));
  vecv_extensionality t3 (vec_or (vec_shift_right t0 48ul) (vec_shift_left m4 16ul))

noextract
val load_felem5_4_compact: lo:uint64xN 4 -> hi:uint64xN 4 -> felem5 4
lo: Hacl.Spec.Poly1305.Field32xN.uint64xN 4 -> hi: Hacl.Spec.Poly1305.Field32xN.uint64xN 4
  -> Hacl.Spec.Poly1305.Field32xN.felem5 4