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)))
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)
   )
   ()
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
/
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
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))
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
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)))
  ()