val varint_len (x: U62.t) : Tot (y: U32.t{U32.v y <= 8})
let varint_len
  (x: U62.t)
: Tot (y: U32.t {U32.v y <= 8})
= if x `U62.lt` 64uL
  then 1ul
  else if x `U62.lt` 16384uL
  then 2ul
  else if x `U62.lt` 1073741824uL
  then 4ul
  else 8ul
val varint_len (x: U62.t) : Tot (y: U32.t{U32.v y <= 8})
let varint_len (x: U62.t) : Tot (y: U32.t{U32.v y <= 8}) =
if x `U62.lt` 64uL
then 1ul
else if x `U62.lt` 16384uL then 2ul else if x `U62.lt` 1073741824uL then 4ul else 8ul
QUIC.Impl.Base.fst.checked
QUIC.UInt62.fst.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
QUIC.Impl.Base.fst
QUIC.UInt62.t FStar.UInt64.lt FStar.UInt64.__uint_to_t FStar.UInt32.__uint_to_t Prims.bool FStar.UInt32.t Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v
module QUIC.Impl.Base

module U32 = FStar.UInt32
module U62 = QUIC.UInt62

(* Length computations need to be transparent because the precondition
to QUIC.Impl.encrypt requires the user to provide a destination buffer
large enough to contain the byte representation of the header *)

let varint_len
  (x: U62.t)
val varint_len (x: U62.t) : Tot (y: U32.t{U32.v y <= 8})
x: QUIC.UInt62.t -> y: FStar.UInt32.t{FStar.UInt32.v y <= 8}