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 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
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.lanes Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Spec.Poly1305.Field32xN.felem_fits5 FStar.Pervasives.Native.Mktuple5 Prims.nat Prims.l_and Prims.eq2 Hacl.Spec.Poly1305.Field32xN.precomp_r5 Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma Hacl.Spec.Poly1305.Field32xN.carry_wide_felem5 Prims.unit Hacl.Spec.Poly1305.Field32xN.Lemmas.mul_felem5_eval_lemma Hacl.Spec.Poly1305.Field32xN.felem_wide5 Hacl.Spec.Poly1305.Field32xN.mul_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)]
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)]

    f1:
      Hacl.Spec.Poly1305.Field32xN.felem5 w
        {Hacl.Spec.Poly1305.Field32xN.felem_fits5 f1 (3, 3, 3, 3, 3)} ->
    r:
      Hacl.Spec.Poly1305.Field32xN.felem5 w
        {Hacl.Spec.Poly1305.Field32xN.felem_fits5 r (2, 2, 2, 2, 2)} ->
    r5:
      Hacl.Spec.Poly1305.Field32xN.felem5 w
        { Hacl.Spec.Poly1305.Field32xN.felem_fits5 r5 (10, 10, 10, 10, 10) /\
          r5 == Hacl.Spec.Poly1305.Field32xN.precomp_r5 r }
  -> FStar.Pervasives.Lemma
      (ensures
        Hacl.Spec.Poly1305.Field32xN.feval5 (Hacl.Spec.Poly1305.Field32xN.fmul_r5 f1 r r5) ==
        Lib.Sequence.map2 Hacl.Spec.Poly1305.Vec.pfmul
          (Hacl.Spec.Poly1305.Field32xN.feval5 f1)
          (Hacl.Spec.Poly1305.Field32xN.feval5 r))
      [SMTPat (Hacl.Spec.Poly1305.Field32xN.fmul_r5 f1 r r5)]