let uint_from_bytes_le #t #l = Lib.ByteSequence.uint_from_bytes_le #t #l
let uint_from_bytes_le #t #l =
Lib.ByteSequence.uint_from_bytes_le #t #l
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.IntTypes.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.l_not Lib.IntTypes.uu___is_U1 Lib.IntTypes.secrecy_level Lib.ByteSequence.uint_from_bytes_le Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.numbytes
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
unfold let repeat_blocks = Lib.Sequence.repeat_blocks
unfold let repeat_blocks_f = Lib.Sequence.repeat_blocks_f
unfold let sub #a #len = Lib.Sequence.sub #a #len
val uint_from_bytes_le : b: Lib.Sequence.lseq (Lib.IntTypes.int_t Lib.IntTypes.U8 l) (Lib.IntTypes.numbytes t)
  -> Lib.IntTypes.int_t t l
b: Lib.Sequence.lseq (Lib.IntTypes.int_t Lib.IntTypes.U8 l) (Lib.IntTypes.numbytes t)
  -> Lib.IntTypes.int_t t l