val parse32_varint' (b: B32.bytes) : Tot (option (U62.t & U32.t))
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
val parse32_varint' (b: B32.bytes) : Tot (option (U62.t & U32.t))
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
      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
    else
      if tag = 2uy
      then
        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
      else
        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
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.Bytes.bytes LowParse.SLow.Int.parse32_u8 FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 QUIC.UInt62.t FStar.UInt32.t FStar.UInt8.t Prims.op_Equality FStar.UInt8.__uint_to_t FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.bool FStar.UInt64.lte FStar.UInt64.__uint_to_t FStar.UInt32.add FStar.Pervasives.Native.option FStar.UInt64.add FStar.UInt64.mul FStar.Int.Cast.uint8_to_uint64 LowParse.SLow.BoundedInt.parse32_bounded_integer LowParse.Spec.BoundedInt.bounded_integer FStar.Int.Cast.uint32_to_uint64 LowParse.SLow.Combinators.parse32_nondep_then LowParse.Spec.Int.parse_u32_kind LowParse.Spec.Int.parse_u32 LowParse.SLow.Int.parse32_u32 LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.parse_bounded_integer Prims.eq2 FStar.Seq.Base.seq FStar.Bytes.reveal FStar.Seq.Base.slice FStar.UInt32.v FStar.Bytes.len FStar.Bytes.slice FStar.UInt64.t Prims.b2t Prims.int Prims.l_or FStar.UInt.size FStar.UInt64.v FStar.UInt8.v LowParse.BitFields.__proj__Mkuint_t__item__get_bitfield LowParse.BitFields.uint8 FStar.UInt.uint_t LowParse.BitFields.__proj__Mkuint_t__item__v LowParse.BitFields.get_bitfield Prims.unit FStar.Pervasives.assert_norm Prims.pow2 Prims._assert Prims.op_GreaterThan FStar.UInt64.n QUIC.UInt62.bound
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)
val parse32_varint' (b: B32.bytes) : Tot (option (U62.t & U32.t))
b: FStar.Bytes.bytes -> FStar.Pervasives.Native.option (QUIC.UInt62.t * FStar.UInt32.t)