let uint_v #t #l = Lib.IntTypes.uint_v #t #l
let uint_v #t #l =
Lib.IntTypes.uint_v #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.b2t Lib.IntTypes.unsigned Lib.IntTypes.secrecy_level Lib.IntTypes.uint_v Lib.IntTypes.int_t Prims.int Lib.IntTypes.range
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
val uint_v : u15: Lib.IntTypes.int_t t l -> x: Prims.int{Lib.IntTypes.range x t}
u15: Lib.IntTypes.int_t t l -> x: Prims.int{Lib.IntTypes.range x t}