let repeat_blocks_f = Lib.Sequence.repeat_blocks_f
let repeat_blocks_f =
Lib.Sequence.repeat_blocks_f
Vale.Poly1305.Equiv.fst.checked
Vale.Poly1305.Math.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Impl.Poly1305.Lemmas.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Poly1305.Equiv.fst
Lib.Sequence.repeat_blocks_f Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_GreaterThan Lib.Sequence.seq Lib.Sequence.lseq Prims.eq2 Prims.int Prims.op_Division Lib.Sequence.length Prims.op_LessThan
module Vale.Poly1305.Equiv
open FStar.Mul

module BSeq = Lib.ByteSequence

// REVIEW: S and V use different smtencoding flags,
// so some equalities between S and V definitions aren't as obvious to Z3 as we might want.

unfold let pow2_128 = Vale.Def.Words_s.pow2_128
unfold let nat64 = Vale.Def.Words_s.nat64
unfold let iand #n = Vale.Def.Types_s.iand #n
unfold let size_nat = Lib.IntTypes.size_nat
unfold let uint_v #t #l = Lib.IntTypes.uint_v #t #l
unfold let uint8 = Lib.IntTypes.uint8
unfold let u64 = Lib.IntTypes.u64
unfold let logand #t #l = Lib.IntTypes.logand #t #l
unfold let repeati = Lib.LoopCombinators.repeati
val repeat_blocks_f : bs: (n: Prims.nat{n <= Prims.pow2 32 - 1}){bs > 0} ->
    inp: Lib.Sequence.seq _ ->
    f: (_: Lib.Sequence.lseq _ bs -> _: _ -> _) ->
    nb: Prims.nat{nb == Lib.Sequence.length inp / bs} ->
    i: Prims.nat{i < nb} ->
    acc: _
  -> _

    bs: (n: Prims.nat{n <= Prims.pow2 32 - 1}){bs > 0} ->
    inp: Lib.Sequence.seq _ ->
    f: (_: Lib.Sequence.lseq _ bs -> _: _ -> _) ->
    nb: Prims.nat{nb == Lib.Sequence.length inp / bs} ->
    i: Prims.nat{i < nb} ->
    acc: _
  -> _