val parse_varint_payload_u62 (msb: varint_msb_t) : Tot (parser parse_varint_payload_kind U62.t)
let parse_varint_payload_u62
  (msb: varint_msb_t)
: Tot (parser parse_varint_payload_kind U62.t)
= 
  weaken parse_varint_payload_kind
    ((((p7) `parse_synth` synth_u62 msb)
    `parse_filter` filter_u62)
    `parse_synth` id_u62)
val parse_varint_payload_u62 (msb: varint_msb_t) : Tot (parser parse_varint_payload_kind U62.t)
let parse_varint_payload_u62 (msb: varint_msb_t) : Tot (parser parse_varint_payload_kind U62.t) =
weaken parse_varint_payload_kind
  ((((p7) `parse_synth` (synth_u62 msb)) `parse_filter` filter_u62) `parse_synth` id_u62)
QUIC.Spec.VarInt.fst.checked
QUIC.UInt62.fst.checked prims.fst.checked LowParse.Spec.BoundedInt.fsti.checked LowParse.Spec.BitFields.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.Classical.fsti.checked
QUIC.Spec.VarInt.fst
QUIC.Spec.VarInt.varint_msb_t LowParse.Spec.Base.weaken QUIC.Spec.VarInt.parse_varint_payload_kind LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Int.parse_u32_kind LowParse.Spec.BoundedInt.parse_bounded_integer_kind QUIC.UInt62.t LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.parse_filter_refine QUIC.Spec.VarInt.filter_u62 LowParse.Spec.Combinators.parse_filter FStar.Pervasives.Native.tuple2 FStar.UInt32.t LowParse.Spec.BoundedInt.bounded_integer QUIC.Spec.VarInt.p7 QUIC.Spec.VarInt.synth_u62 QUIC.Spec.VarInt.id_u62 LowParse.Spec.Base.parser
module QUIC.Spec.VarInt

module U64 = FStar.UInt64
module LP = LowParse.Spec.BoundedInt // for bounded_int32

open LowParse.Spec.BoundedInt
open LowParse.Spec.BitFields

inline_for_extraction
let parse_varint_payload_kind = {
  parser_kind_low = 0;
  parser_kind_high = Some 7;
  parser_kind_subkind = Some ParserStrong;
  parser_kind_metadata = None;
}

module Cast = FStar.Int.Cast
module U62 = QUIC.UInt62
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8

inline_for_extraction
let varint_msb_t = (x: U64.t { U64.v x < 64 })

#push-options "--z3rlimit 32"

inline_for_extraction
let synth_u14
  (msb: varint_msb_t)
  (lsb: U8.t)
: Tot U62.t
= [@inline_let] let _ =
    assert_norm (pow2 8 == 256);
    assert (pow2 62 == U64.v U62.bound)
  in
  (msb `U64.mul` 256uL) `U64.add` Cast.uint8_to_uint64 lsb  

let synth_u14_injective
  (msb: varint_msb_t)
: Lemma
  (synth_injective (synth_u14 msb))
  [SMTPat (synth_injective (synth_u14 msb))]
= ()

inline_for_extraction
let synth_u30
  (msb: varint_msb_t)
  (lsb: bounded_integer 3)
: Tot U62.t
= [@inline_let] let _ =
    assert_norm (pow2 8 == 256);
    assert (pow2 62 == U64.v U62.bound);
    assert_norm (pow2 24 == 16777216)
   in
   (msb `U64.mul` 16777216uL) `U64.add` Cast.uint32_to_uint64 lsb

let synth_u30_injective
  (msb: varint_msb_t)
: Lemma
  (synth_injective (synth_u30 msb))
  [SMTPat (synth_injective (synth_u30 msb))]
= ()

inline_for_extraction
let synth_u62
  (msb: varint_msb_t)
  (lsb: (U32.t & bounded_integer 3))
: Tot U62.t
= [@inline_let] let _ =
  assert_norm (pow2 8 == 256);
  assert (pow2 62 == U64.v U62.bound);
  assert_norm (pow2 24 == 16777216);
  assert_norm (pow2 32 == 4294967296)
  in
  match lsb with
  | (hi, lo) ->
  Cast.uint32_to_uint64 lo `U64.add` (16777216uL `U64.mul` (Cast.uint32_to_uint64 hi `U64.add` (4294967296uL `U64.mul` msb)))

let synth_u62_msb
  (msb: varint_msb_t)
  (lsb: (U32.t & bounded_integer 3))
: Lemma
  (U64.v (synth_u62 msb lsb) / 72057594037927936 == U64.v msb)
= ()

let synth_u62_injective
  (msb: varint_msb_t)
: Lemma
  (synth_injective (synth_u62 msb))
  [SMTPat (synth_injective (synth_u62 msb))]
= ()

inline_for_extraction
let filter_u14
  (y: U62.t)
: Tot bool
= 64uL `U64.lte` y

inline_for_extraction
let filter_u30
  (y: U62.t)
: Tot bool
= 16384uL `U64.lte` y

inline_for_extraction
let filter_u62
  (y: U62.t)
: Tot bool
= 1073741824uL `U64.lte` y
    
inline_for_extraction
let id_u14
  (y: parse_filter_refine filter_u14)
: Tot U62.t
= y

let parse_varint_payload_u14
  (msb: varint_msb_t)
: Tot (parser parse_varint_payload_kind U62.t)
= 
  weaken parse_varint_payload_kind
    (((parse_u8 `parse_synth` synth_u14 msb)
    `parse_filter` filter_u14)
    `parse_synth` id_u14)
    
inline_for_extraction
let id_u30
  (y: parse_filter_refine filter_u30)
: Tot U62.t
= y

let parse_varint_payload_u30
  (msb: varint_msb_t)
: Tot (parser parse_varint_payload_kind U62.t)
= 
  weaken parse_varint_payload_kind
    (((parse_bounded_integer 3 `parse_synth` synth_u30 msb)
    `parse_filter` filter_u30)
    `parse_synth` id_u30)

inline_for_extraction
let id_u62
  (y: parse_filter_refine filter_u62)
: Tot U62.t
= y

let p7 = parse_u32 `nondep_then` parse_bounded_integer 3

let parse_varint_payload_u62
  (msb: varint_msb_t)
: Tot (parser parse_varint_payload_kind U62.t)
val parse_varint_payload_u62 (msb: varint_msb_t) : Tot (parser parse_varint_payload_kind U62.t)
msb: QUIC.Spec.VarInt.varint_msb_t
  -> LowParse.Spec.Base.parser QUIC.Spec.VarInt.parse_varint_payload_kind QUIC.UInt62.t