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 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)
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.uint64xN Lib.IntVector.vecv_extensionality Lib.IntTypes.U64 Lib.IntVector.vec_smul_mod Hacl.Spec.Poly1305.Field32xN.zero Lib.IntTypes.u64 Prims.unit Lib.Sequence.eq_intro Lib.IntTypes.uint_t Lib.IntTypes.SEC Lib.IntVector.vec_v FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan Prims.eq2 Prims.l_or FStar.Seq.Base.index Lib.Sequence.to_seq Lib.IntTypes.range_t Lib.IntTypes.v Lib.Sequence.op_String_Access Prims.l_True Prims.squash Lib.IntTypes.int_t Lib.IntTypes.mk_int Prims.int Lib.IntTypes.range Lib.Sequence.index Prims.Nil FStar.Pervasives.pattern Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Spec.Poly1305.Field32xN.precomp_r5 FStar.Pervasives.Native.tuple5 FStar.Pervasives.Native.Mktuple5
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))
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))
w: Hacl.Spec.Poly1305.Field32xN.lanes
  -> FStar.Pervasives.Lemma
    (ensures
      (let r =
          Hacl.Spec.Poly1305.Field32xN.zero w,
          Hacl.Spec.Poly1305.Field32xN.zero w,
          Hacl.Spec.Poly1305.Field32xN.zero w,
          Hacl.Spec.Poly1305.Field32xN.zero w,
          Hacl.Spec.Poly1305.Field32xN.zero w
        in
        Hacl.Spec.Poly1305.Field32xN.precomp_r5 r ==
        FStar.Pervasives.Native.Mktuple5 (Hacl.Spec.Poly1305.Field32xN.zero w)
          (Hacl.Spec.Poly1305.Field32xN.zero w)
          (Hacl.Spec.Poly1305.Field32xN.zero w)
          (Hacl.Spec.Poly1305.Field32xN.zero w)
          (Hacl.Spec.Poly1305.Field32xN.zero w)))