val read_varint: LL.leaf_reader parse_varint
let read_varint #rrel #rel sl pos =
  let h = HST.get () in
  [@inline_let]
  let _ =
    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);
    LL.valid_facts parse_varint h sl pos;
    parse_varint_eq (LL.bytes_of_slice_from h sl pos);
    LL.valid_facts parse_u8 h sl pos
  in
  let pos1 = LI.jump_u8 sl pos in
  let b = LI.read_u8 sl pos in
  let kd = uint8.get_bitfield b 6 8 in
  let msb8 = uint8.get_bitfield b 0 6 in
  let msb = Cast.uint8_to_uint64 (msb8) in
  if kd = 0uy
  then msb
  else if kd = 1uy
  then begin
    [@inline_let]
    let _ =
      LL.valid_facts parse_u8 h sl pos1
    in
    let lsb = LI.read_u8 sl pos1 in
    synth_u14 msb lsb
  end else if kd = 2uy
  then begin
    [@inline_let]
    let _ =
      LL.valid_facts (parse_bounded_integer 3) h sl pos1
    in
    let lsb = LL.read_bounded_integer 3 sl pos1 in
    synth_u30 msb lsb
  end else begin
    [@inline_let]
    let _ =
      LL.valid_facts (parse_u32 `nondep_then` parse_bounded_integer 3) h sl pos1
    in
    let pos_hi = LC.accessor_fst LL.parse_u32 () (LL.parse_bounded_integer 3) sl pos1 in
    let hi = LI.read_u32 sl pos_hi in
    let pos_lo = LC.accessor_snd LI.jump_u32 (LL.parse_bounded_integer 3) sl pos1 in
    let lo = LL.read_bounded_integer 3 sl pos_lo in
    synth_u62 msb (hi, lo)
  end
val read_varint: LL.leaf_reader parse_varint
let read_varint #rrel #rel sl pos =
let h = HST.get () in
[@@ inline_let ]let _ =
  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);
  LL.valid_facts parse_varint h sl pos;
  parse_varint_eq (LL.bytes_of_slice_from h sl pos);
  LL.valid_facts parse_u8 h sl pos
in
let pos1 = LI.jump_u8 sl pos in
let b = LI.read_u8 sl pos in
let kd = uint8.get_bitfield b 6 8 in
let msb8 = uint8.get_bitfield b 0 6 in
let msb = Cast.uint8_to_uint64 (msb8) in
if kd = 0uy
then msb
else
  if kd = 1uy
  then
    [@@ inline_let ]let _ = LL.valid_facts parse_u8 h sl pos1 in
    let lsb = LI.read_u8 sl pos1 in
    synth_u14 msb lsb
  else
    if kd = 2uy
    then
      [@@ inline_let ]let _ = LL.valid_facts (parse_bounded_integer 3) h sl pos1 in
      let lsb = LL.read_bounded_integer 3 sl pos1 in
      synth_u30 msb lsb
    else
      [@@ inline_let ]let _ =
        LL.valid_facts (parse_u32 `nondep_then` (parse_bounded_integer 3)) h sl pos1
      in
      let pos_hi = LC.accessor_fst LL.parse_u32 () (LL.parse_bounded_integer 3) sl pos1 in
      let hi = LI.read_u32 sl pos_hi in
      let pos_lo = LC.accessor_snd LI.jump_u32 (LL.parse_bounded_integer 3) sl pos1 in
      let lo = LL.read_bounded_integer 3 sl pos_lo in
      synth_u62 msb (hi, lo)
QUIC.Impl.VarInt.fst.checked
QUIC.Spec.VarInt.fst.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.BoundedInt.fsti.checked LowParse.Spec.BitFields.fst.checked LowParse.Low.Int.fsti.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.BoundedInt.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.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked
QUIC.Impl.VarInt.fst
LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t Prims.op_Equality FStar.UInt8.t FStar.UInt8.__uint_to_t QUIC.UInt62.t Prims.bool QUIC.Spec.VarInt.synth_u14 LowParse.Low.Int.read_u8 Prims.unit LowParse.Low.Base.Spec.valid_facts LowParse.Spec.Int.parse_u8_kind LowParse.Spec.Int.parse_u8 QUIC.Spec.VarInt.synth_u30 LowParse.Spec.BoundedInt.bounded_integer LowParse.Low.BoundedInt.read_bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.parse_bounded_integer QUIC.Spec.VarInt.synth_u62 FStar.Pervasives.Native.Mktuple2 LowParse.Low.Combinators.accessor_snd LowParse.Spec.Int.parse_u32_kind LowParse.Spec.Int.parse_u32 LowParse.Low.Int.jump_u32 LowParse.Low.Int.read_u32 LowParse.Low.Combinators.accessor_fst LowParse.Spec.Combinators.and_then_kind FStar.Pervasives.Native.tuple2 LowParse.Spec.Combinators.nondep_then FStar.UInt64.t Prims.b2t Prims.int Prims.l_or FStar.UInt.size FStar.UInt64.v FStar.UInt8.v FStar.Int.Cast.uint8_to_uint64 Prims.eq2 FStar.UInt.uint_t LowParse.BitFields.__proj__Mkuint_t__item__v LowParse.BitFields.uint8 LowParse.BitFields.get_bitfield LowParse.BitFields.__proj__Mkuint_t__item__get_bitfield LowParse.Low.Int.jump_u8 QUIC.Spec.VarInt.parse_varint_eq LowParse.Slice.bytes_of_slice_from QUIC.Spec.VarInt.parse_varint_kind QUIC.Spec.VarInt.parse_varint FStar.Pervasives.assert_norm Prims.pow2 Prims._assert Prims.op_GreaterThan FStar.UInt64.n QUIC.UInt62.bound FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module QUIC.Impl.VarInt
friend QUIC.Spec.VarInt

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

module HST = FStar.HyperStack.ST
module LL = LowParse.Low.BoundedInt
module LI = LowParse.Low.Int
module LC = LowParse.Low.Combinators

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

#push-options "--z3rlimit 128"

let validate_varint #rrel #rel sl pos =
  let h = HST.get () in
  let pos0 = pos in
  let pos = LL.uint64_to_uint32 pos in
  [@inline_let]
  let _ =
    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);
    LL.valid_facts parse_varint h sl pos;
    parse_varint_eq (LL.bytes_of_slice_from h sl pos);
    LL.valid_facts parse_u8 h sl pos
  in
  let pos1 = LI.validate_u8 () sl pos0 in
  if LL.is_error pos1
  then pos1
  else
    let b = LI.read_u8 sl pos in
    let kd = uint8.get_bitfield b 6 8 in
    let msb8 = uint8.get_bitfield b 0 6 in
    let msb = Cast.uint8_to_uint64 (msb8) in
    if kd = 0uy
    then pos1
    else
      let pos1' = pos1 in
      let pos1 = LL.uint64_to_uint32 pos1 in
    if kd = 1uy
    then begin
      [@inline_let]
      let _ =
        LL.valid_facts parse_u8 h sl pos1
      in
      let pos2 = LI.validate_u8 () sl pos1' in
      if LL.is_error pos2
      then pos2
      else
        let lsb = LI.read_u8 sl pos1 in
        let z = synth_u14 msb lsb in
        if filter_u14 z
        then pos2
        else LL.validator_error_generic
    end else if kd = 2uy
    then begin
      [@inline_let]
      let _ =
        LL.valid_facts (parse_bounded_integer 3) h sl pos1
      in
      let pos2 = LL.validate_bounded_integer 3 sl pos1' in
      if LL.is_error pos2
      then pos2
      else
        let lsb = LL.read_bounded_integer 3 sl pos1 in
        let z = synth_u30 msb lsb in
        if filter_u30 z
        then pos2
        else LL.validator_error_generic        
    end else begin
      [@inline_let]
      let _ =
        LL.valid_facts (parse_u32 `nondep_then` parse_bounded_integer 3) h sl pos1
      in
      let pos2 = LC.validate_nondep_then (LI.validate_u32 ()) (LL.validate_bounded_integer 3) sl pos1' in
      if LL.is_error pos2
      then pos2
      else
        let pos_hi = LC.accessor_fst LL.parse_u32 () (LL.parse_bounded_integer 3) sl pos1 in
        let hi = LI.read_u32 sl pos_hi in
        let pos_lo = LC.accessor_snd LI.jump_u32 (LL.parse_bounded_integer 3) sl pos1 in
        let lo = LL.read_bounded_integer 3 sl pos_lo in
        let z = synth_u62 msb (hi, lo) in
        if filter_u62 z
        then pos2
        else LL.validator_error_generic
    end
val read_varint: LL.leaf_reader parse_varint
LowParse.Low.Base.leaf_reader QUIC.Spec.VarInt.parse_varint