val parse32_bounded_varint (min: U32.t) (max: U32.t{U32.v min <= U32.v max})
    : Tot (LP.parser32 (VI.parse_bounded_varint (U32.v min) (U32.v max)))
let parse32_bounded_varint
  (min: U32.t)
  (max: U32.t { U32.v min <= U32.v max })
: Tot (LP.parser32 (VI.parse_bounded_varint (U32.v min) (U32.v max)))
= LP.parse32_synth'
   (VI.parse_varint `LP.parse_filter` VI.varint_in_bounds (U32.v min) (U32.v max))
   (VI.synth_bounded_varint (U32.v min) (U32.v max))
   (LP.parse32_filter
     parse32_varint
     (VI.varint_in_bounds (U32.v min) (U32.v max))
     (fun x -> Cast.uint32_to_uint64 min `U64.lte` x && x `U64.lte` Cast.uint32_to_uint64 max)
   )
   ()
val parse32_bounded_varint (min: U32.t) (max: U32.t{U32.v min <= U32.v max})
    : Tot (LP.parser32 (VI.parse_bounded_varint (U32.v min) (U32.v max)))
let parse32_bounded_varint (min: U32.t) (max: U32.t{U32.v min <= U32.v max})
    : Tot (LP.parser32 (VI.parse_bounded_varint (U32.v min) (U32.v max))) =
LP.parse32_synth' (VI.parse_varint `LP.parse_filter` (VI.varint_in_bounds (U32.v min) (U32.v max)))
  (VI.synth_bounded_varint (U32.v min) (U32.v max))
  (LP.parse32_filter parse32_varint
      (VI.varint_in_bounds (U32.v min) (U32.v max))
      (fun x -> (Cast.uint32_to_uint64 min) `U64.lte` x && x `U64.lte` (Cast.uint32_to_uint64 max)))
  ()
QUIC.TotSpec.fst.checked
QUIC.UInt62.fst.checked QUIC.Spec.VarInt.fst.checked QUIC.Spec.PacketNumber.fst.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.Public.fst.checked QUIC.Spec.Header.Parse.fst.checked QUIC.Spec.Header.fst.checked QUIC.Spec.fst.checked QUIC.Secret.Seq.fsti.checked prims.fst.checked LowParse.SLow.BitSum.fst.checked LowParse.SLow.fst.checked LowParse.Bytes32.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.Endianness.fsti.checked
QUIC.TotSpec.fst
FStar.UInt32.t Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowParse.SLow.Combinators.parse32_synth' LowParse.Spec.Combinators.parse_filter_kind QUIC.Spec.VarInt.parse_varint_kind LowParse.Spec.Combinators.parse_filter_refine QUIC.UInt62.t QUIC.Spec.VarInt.varint_in_bounds LowParse.Spec.BoundedInt.bounded_int32 LowParse.Spec.Combinators.parse_filter QUIC.Spec.VarInt.parse_varint QUIC.Spec.VarInt.synth_bounded_varint LowParse.SLow.Combinators.parse32_filter QUIC.TotSpec.parse32_varint Prims.op_AmpAmp FStar.UInt64.lte FStar.Int.Cast.uint32_to_uint64 Prims.bool Prims.eq2 LowParse.SLow.Base.parser32 QUIC.Spec.VarInt.parse_bounded_varint
module QUIC.TotSpec

friend QUIC.Spec
friend QUIC.Spec.Header
friend QUIC.Spec.Header.Parse
friend QUIC.Spec.Header.Public
friend QUIC.Spec.PacketNumber
friend QUIC.Spec.VarInt

module PN = QUIC.Spec.PacketNumber
module VI = QUIC.Spec.VarInt
module Public = QUIC.Spec.Header.Public
module Parse = QUIC.Spec.Header.Parse
module Header = QUIC.Spec.Header
module Lemmas = QUIC.Spec.Lemmas
module Spec = QUIC.Spec

module LP = LowParse.SLow
module LPB = LowParse.SLow.BitSum

module U8 = FStar.UInt8
module U62 = QUIC.UInt62
module U64 = FStar.UInt64
module BF = LowParse.BitFields
module B32 = LowParse.Bytes32
module Cast = FStar.Int.Cast
module U32 = FStar.UInt32
module Seq = QUIC.Secret.Seq

#push-options "--z3rlimit 128"

let parse32_varint'
  (b: B32.bytes)
: Tot (option (U62.t & U32.t))
= assert_norm (pow2 8 == 256);
  assert_norm (pow2 6 == 64);
  assert (pow2 62 == U64.v U62.bound);
  assert_norm (pow2 24 == 16777216);
  assert_norm (pow2 32 == 4294967296);
  match LP.parse32_u8 b with
  | None -> None
  | Some (hd, consumed) ->
    let tag = BF.uint8.BF.get_bitfield hd 6 8 in
    let msb = Cast.uint8_to_uint64 (BF.uint8.BF.get_bitfield hd 0 6) in
    let b' = B32.slice b consumed (B32.len b) in
    if tag = 0uy
    then
      Some ((msb <: U62.t), consumed)
    else if tag = 1uy
    then begin match LP.parse32_u8 b' with
    | None -> None
    | Some (lsb, consumed') ->
      let v : U62.t = (msb `U64.mul` 256uL) `U64.add` Cast.uint8_to_uint64 lsb in
      if 64uL `U64.lte` v
      then Some (v, consumed `U32.add` consumed')
      else None
      end
    else if tag = 2uy
    then begin match (LP.parse32_bounded_integer 3) b' with
    | None -> None
    | Some (lsb, consumed') ->
      let v : U62.t =
        (msb `U64.mul` 16777216uL) `U64.add` Cast.uint32_to_uint64 lsb
      in
      if 16384uL `U64.lte` v
      then Some (v, consumed `U32.add` consumed')
      else None
    end else begin match (LP.parse32_u32 `LP.parse32_nondep_then` LP.parse32_bounded_integer 3) b' with
    | None -> None
    | Some ((hi, lo), consumed') ->
      let v : U62.t =
        Cast.uint32_to_uint64 lo `U64.add` (16777216uL `U64.mul` (Cast.uint32_to_uint64 hi `U64.add` (4294967296uL `U64.mul` msb)))
      in
      if 1073741824uL `U64.lte` v
      then Some (v, consumed `U32.add` consumed')
      else None
    end

let parse32_varint'_correct
  (input: B32.bytes)
: Lemma
  (LP.parser32_correct VI.parse_varint input (parse32_varint' input))
= VI.parse_varint_eq (B32.reveal input)

#pop-options

let parse32_varint
: LP.parser32 VI.parse_varint
= fun input ->
    parse32_varint'_correct input; 
    parse32_varint' input

let parse32_bounded_varint
  (min: U32.t)
  (max: U32.t { U32.v min <= U32.v max })
val parse32_bounded_varint (min: U32.t) (max: U32.t{U32.v min <= U32.v max})
    : Tot (LP.parser32 (VI.parse_bounded_varint (U32.v min) (U32.v max)))
min: FStar.UInt32.t -> max: FStar.UInt32.t{FStar.UInt32.v min <= FStar.UInt32.v max}
  -> LowParse.SLow.Base.parser32 (QUIC.Spec.VarInt.parse_bounded_varint (FStar.UInt32.v min)
          (FStar.UInt32.v max))