val load_acc_lemma4: b:block_v 4 -> acc0:pfelem -> r:pfelem -> Lemma
  (normalize_n r (load_acc b acc0) ==
   repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)
let load_acc_lemma4 b acc0 r =
  let b0 = Seq.slice b 0 size_block in
  let b1 = Seq.slice b size_block (2 * size_block) in
  let b2 = Seq.slice b (2 * size_block) (3 * size_block) in
  let b3 = Seq.slice b (3 * size_block) (4 * size_block) in

  let c0 = pfadd (pow2 128) (nat_from_bytes_le b0) in
  let c1 = pfadd (pow2 128) (nat_from_bytes_le b1) in
  let c2 = pfadd (pow2 128) (nat_from_bytes_le b2) in
  let c3 = pfadd (pow2 128) (nat_from_bytes_le b3) in

  FStar.Math.Lemmas.modulo_lemma c1 prime;
  FStar.Math.Lemmas.modulo_lemma c2 prime;
  FStar.Math.Lemmas.modulo_lemma c3 prime;

  let f = S.poly1305_update1 r size_block in
  let nb = (4 * size_block) / size_block in
  let repeat_f = repeat_blocks_f size_block b f nb in

  lemma_repeat_blocks_multi size_block b f acc0;
  Loops.unfold_repeati nb repeat_f acc0 3;
  Loops.unfold_repeati nb repeat_f acc0 2;
  Loops.unfold_repeati nb repeat_f acc0 1;
  Loops.unfold_repeati nb repeat_f acc0 0;
  Loops.eq_repeati0 nb repeat_f acc0;
  Lemmas.poly_update_multi_lemma_load4_simplify acc0 r c0 c1 c2 c3
val load_acc_lemma4: b:block_v 4 -> acc0:pfelem -> r:pfelem -> Lemma
  (normalize_n r (load_acc b acc0) ==
   repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)
let load_acc_lemma4 b acc0 r =
let b0 = Seq.slice b 0 size_block in
let b1 = Seq.slice b size_block (2 * size_block) in
let b2 = Seq.slice b (2 * size_block) (3 * size_block) in
let b3 = Seq.slice b (3 * size_block) (4 * size_block) in
let c0 = pfadd (pow2 128) (nat_from_bytes_le b0) in
let c1 = pfadd (pow2 128) (nat_from_bytes_le b1) in
let c2 = pfadd (pow2 128) (nat_from_bytes_le b2) in
let c3 = pfadd (pow2 128) (nat_from_bytes_le b3) in
FStar.Math.Lemmas.modulo_lemma c1 prime;
FStar.Math.Lemmas.modulo_lemma c2 prime;
FStar.Math.Lemmas.modulo_lemma c3 prime;
let f = S.poly1305_update1 r size_block in
let nb = (4 * size_block) / size_block in
let repeat_f = repeat_blocks_f size_block b f nb in
lemma_repeat_blocks_multi size_block b f acc0;
Loops.unfold_repeati nb repeat_f acc0 3;
Loops.unfold_repeati nb repeat_f acc0 2;
Loops.unfold_repeati nb repeat_f acc0 1;
Loops.unfold_repeati nb repeat_f acc0 0;
Loops.eq_repeati0 nb repeat_f acc0;
Lemmas.poly_update_multi_lemma_load4_simplify acc0 r c0 c1 c2 c3
Hacl.Spec.Poly1305.Equiv.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked Lib.Vec.Lemmas.fsti.checked Lib.Sequence.Lemmas.fsti.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Lemmas.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Hacl.Spec.Poly1305.Equiv.fst
Hacl.Spec.Poly1305.Equiv.block_v Hacl.Spec.Poly1305.Vec.pfelem Hacl.Spec.Poly1305.Lemmas.poly_update_multi_lemma_load4_simplify Prims.unit Lib.LoopCombinators.eq_repeati0 Spec.Poly1305.felem Lib.LoopCombinators.unfold_repeati Lib.Sequence.lemma_repeat_blocks_multi Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Hacl.Spec.Poly1305.Vec.size_block Prims.nat Prims.b2t Prims.op_LessThan Lib.Sequence.repeat_blocks_f Prims.int Prims.op_Division FStar.Mul.op_Star Lib.Sequence.lseq Lib.IntTypes.int_t Spec.Poly1305.poly1305_update1 FStar.Math.Lemmas.modulo_lemma Hacl.Spec.Poly1305.Vec.prime Hacl.Spec.Poly1305.Vec.pfadd Prims.pow2 Lib.ByteSequence.nat_from_bytes_le FStar.Seq.Base.seq FStar.Seq.Base.slice
module Hacl.Spec.Poly1305.Equiv

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

module Loops = Lib.LoopCombinators
module VecLemmas = Lib.Vec.Lemmas
module SeqLemmas = Lib.Sequence.Lemmas
module Lemmas = Hacl.Spec.Poly1305.Lemmas
module S = Spec.Poly1305

include Hacl.Spec.Poly1305.Vec

#set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

let block_v (w:lanes{w * size_block <= max_size_t}) = lbytes (w * size_block)

///
///  val load_acc_lemma: #w:lanes -> b:block_v w -> acc0:pfelem -> r:pfelem -> Lemma
///   (normalize_n r (load_acc b acc0) == repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)
///

val load_acc_lemma1: b:block_v 1 -> acc0:pfelem -> r:pfelem -> Lemma
  (normalize_n r (load_acc #1 b acc0) ==
   repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)

let load_acc_lemma1 b acc0 r =
  let f = S.poly1305_update1 r size_block in
  let nb = size_block / size_block in
  let repeat_f = repeat_blocks_f size_block b f nb in

  lemma_repeat_blocks_multi size_block b f acc0;
  Loops.unfold_repeati nb repeat_f acc0 0;
  Loops.eq_repeati0 nb repeat_f acc0


val load_acc_lemma2: b:block_v 2 -> acc0:pfelem -> r:pfelem -> Lemma
  (normalize_n r (load_acc b acc0) ==
   repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)

let load_acc_lemma2 b acc0 r =
  let b0 = Seq.slice b 0 size_block in
  let b1 = Seq.slice b size_block (2 * size_block) in
  let c0 = pfadd (pow2 128) (nat_from_bytes_le b0) in
  let c1 = pfadd (pow2 128) (nat_from_bytes_le b1) in

  FStar.Math.Lemmas.modulo_lemma c1 prime;

  let f = S.poly1305_update1 r size_block in
  let nb = (2 * size_block) / size_block in
  let repeat_f = repeat_blocks_f size_block b f nb in

  lemma_repeat_blocks_multi size_block b f acc0;
  Loops.unfold_repeati nb repeat_f acc0 1;
  Loops.unfold_repeati nb repeat_f acc0 0;
  Loops.eq_repeati0 nb repeat_f acc0;
  Lemmas.poly_update_multi_lemma_load2_simplify acc0 r c0 c1


val load_acc_lemma4: b:block_v 4 -> acc0:pfelem -> r:pfelem -> Lemma
  (normalize_n r (load_acc b acc0) ==
   repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)
val load_acc_lemma4: b:block_v 4 -> acc0:pfelem -> r:pfelem -> Lemma
  (normalize_n r (load_acc b acc0) ==
   repeat_blocks_multi size_block b (S.poly1305_update1 r size_block) acc0)

    b: Hacl.Spec.Poly1305.Equiv.block_v 4 ->
    acc0: Hacl.Spec.Poly1305.Vec.pfelem ->
    r: Hacl.Spec.Poly1305.Vec.pfelem
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.Poly1305.Vec.normalize_n r (Hacl.Spec.Poly1305.Vec.load_acc b acc0) ==
      Lib.Sequence.repeat_blocks_multi Hacl.Spec.Poly1305.Vec.size_block
        b
        (Spec.Poly1305.poly1305_update1 r Hacl.Spec.Poly1305.Vec.size_block)
        acc0)