let u64 = Lib.IntTypes.u64
let u64 =
Lib.IntTypes.u64
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.u64
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
val u64 : n: Lib.IntTypes.range_t Lib.IntTypes.U64 -> u15: Lib.IntTypes.uint64{Lib.IntTypes.v u15 == n}
n: Lib.IntTypes.range_t Lib.IntTypes.U64 -> u15: Lib.IntTypes.uint64{Lib.IntTypes.v u15 == n}