let block_v (w:lanes{w * size_block <= max_size_t}) = lbytes (w * size_block)
let block_v (w: lanes{w * size_block <= max_size_t}) =
lbytes (w * size_block)
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.Vec.lanes Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Hacl.Spec.Poly1305.Vec.size_block Lib.IntTypes.max_size_t Lib.ByteSequence.lbytes
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"
val block_v : w: Hacl.Spec.Poly1305.Vec.lanes{w * Hacl.Spec.Poly1305.Vec.size_block <= Lib.IntTypes.max_size_t}
  -> Type0
w: Hacl.Spec.Poly1305.Vec.lanes{w * Hacl.Spec.Poly1305.Vec.size_block <= Lib.IntTypes.max_size_t}
  -> Type0