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 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))
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 Lib.Sequence.eq_intro Hacl.Spec.Poly1305.Vec.pfelem Hacl.Spec.Poly1305.Field32xN.feval5 Lib.Sequence.map2 Hacl.Spec.Poly1305.Vec.pfadd Prims.unit FStar.Classical.forall_intro Prims.b2t Prims.op_LessThan Prims.eq2 Lib.Sequence.op_String_Access Hacl.Spec.Poly1305.Field32xN.fadd5 Hacl.Poly1305.Field32xN.Lemmas0.fadd5_eval_lemma_i
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)]
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)]

    f1:
      Hacl.Spec.Poly1305.Field32xN.felem5 w
        {Hacl.Spec.Poly1305.Field32xN.felem_fits5 f1 (2, 2, 2, 2, 2)} ->
    f2:
      Hacl.Spec.Poly1305.Field32xN.felem5 w
        {Hacl.Spec.Poly1305.Field32xN.felem_fits5 f2 (1, 1, 1, 1, 1)}
  -> FStar.Pervasives.Lemma
      (ensures
        Hacl.Spec.Poly1305.Field32xN.feval5 (Hacl.Spec.Poly1305.Field32xN.fadd5 f1 f2) ==
        Lib.Sequence.map2 Hacl.Spec.Poly1305.Vec.pfadd
          (Hacl.Spec.Poly1305.Field32xN.feval5 f1)
          (Hacl.Spec.Poly1305.Field32xN.feval5 f2))
      [SMTPat (Hacl.Spec.Poly1305.Field32xN.fadd5 f1 f2)]