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_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
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.felem5 Hacl.Spec.Poly1305.Field32xN.uint64xN Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_lemma Hacl.Spec.Poly1305.Field32xN.carry_full_felem5 Prims.unit Prims._assert Prims.eq2 Hacl.Spec.Poly1305.Vec.pfelem Lib.Sequence.op_String_Access Hacl.Spec.Poly1305.Field32xN.feval5 Hacl.Spec.Poly1305.Vec.pfadd Hacl.Spec.Poly1305.Field32xN.Lemmas.fmul_r2_normalize51 Hacl.Spec.Poly1305.Field32xN.felem_fits5 FStar.Pervasives.Native.Mktuple5 Prims.nat Lib.Sequence.lseq Lib.Sequence.create2 Lib.Sequence.eq_intro FStar.Pervasives.Native.tuple5 Lib.IntVector.vec_interleave_high_lemma2 Lib.IntTypes.U64 Lib.IntVector.vec_t Lib.IntVector.vec_interleave_high Hacl.Spec.Poly1305.Field32xN.Lemmas.fmul_r2_normalize50
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)]
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)]

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