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_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
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 Lib.LoopCombinators.eq_repeati0 Spec.Poly1305.felem Prims.unit 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 Lib.Sequence.lseq Lib.IntTypes.int_t Spec.Poly1305.poly1305_update1
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)
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)

    b: Hacl.Spec.Poly1305.Equiv.block_v 1 ->
    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)