val bound:(bound: U64.t{U64.v bound == pow2 62})
let bound : (bound: U64.t { U64.v bound == pow2 62 }) =
  [@inline_let] let v = 4611686018427387904uL in
  [@inline_let] let _ = assert_norm (U64.v v == pow2 62) in
  v
val bound:(bound: U64.t{U64.v bound == pow2 62})
let bound:(bound: U64.t{U64.v bound == pow2 62}) =
[@@ inline_let ]let v = 4611686018427387904uL in
[@@ inline_let ]let _ = assert_norm (U64.v v == pow2 62) in
v
QUIC.UInt62.fst.checked
QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.fsti.checked
QUIC.UInt62.fst
Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt64.n Prims.b2t Prims.op_GreaterThan FStar.UInt64.v Prims.pow2 FStar.UInt64.t FStar.UInt64.__uint_to_t
module QUIC.UInt62
module U64 = FStar.UInt64
include FStar.UInt64

inline_for_extraction
val bound:(bound: U64.t{U64.v bound == pow2 62})
bound: FStar.UInt64.t{FStar.UInt64.v bound == Prims.pow2 62}