val write_varint: LL.serializer32 serialize_varint
val write_varint: LL.serializer32 serialize_varint
let write_varint
  x #rrel #rel b pos
=
  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);
  let fb = get_first_byte x in
  let gpos' = Ghost.hide (pos `U32.add` U32.uint_to_t (Seq.length (serialize serialize_varint x))) in
  let len1 = LL.frame_serializer32 LI.serialize32_u8 fb b (Ghost.hide pos) gpos' pos in
  let pos1 = pos `U32.add` len1 in
  if x `U64.lt` 64uL
  then len1
  else begin
    let len2 =
      if x `U64.lt` 16384uL
      then
        LL.frame_serializer32 LI.serialize32_u8 (Cast.uint64_to_uint8 x) b (Ghost.hide pos) gpos' pos1
      else if x `U64.lt` 1073741824uL
      then
        LL.frame_serializer32 (LL.serialize32_bounded_integer_3 ()) (Cast.uint64_to_uint32 (x `U64.rem` 16777216uL)) b (Ghost.hide pos) gpos' pos1
      else
        LL.frame_serializer32 (LC.serialize32_nondep_then LI.serialize32_u32 (LL.serialize32_bounded_integer_3 ())) (Cast.uint64_to_uint32 (x `U64.div` 16777216uL), Cast.uint64_to_uint32 (x `U64.rem` 16777216uL)) b (Ghost.hide pos) gpos' pos1
    in
    let res = len1 `U32.add` len2 in
    let h' = HST.get () in
    seq_slice_i_j_k (B.as_seq h' b) (U32.v pos) (U32.v pos1) (U32.v pos + U32.v res);
    res
  end
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

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

let jump_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 pos1
  else if kd = 1uy
  then begin
    [@inline_let]
    let _ =
      LL.valid_facts parse_u8 h sl pos1
    in
    LI.jump_u8 sl pos1
  end else if kd = 2uy
  then begin
    [@inline_let]
    let _ =
      LL.valid_facts (parse_bounded_integer 3) h sl pos1
    in
    LL.jump_bounded_integer 3 sl pos1
  end else begin
    [@inline_let]
    let _ =
      LL.valid_facts (parse_u32 `nondep_then` parse_bounded_integer 3) h sl pos1
    in
    LC.jump_nondep_then (LI.jump_u32) (LL.jump_bounded_integer 3) sl pos1
  end

module B = LowStar.Buffer

let seq_slice_i_j_k
  (#a: Type)
  (s: Seq.seq a)
  (i j k: nat)
: Lemma
  (requires (i <= j /\ j <= k /\ k <= Seq.length s))
  (ensures (Seq.slice s i k `Seq.equal` (Seq.slice s i j `Seq.append` Seq.slice s j k)))
= ()
/
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.Low.Base.serializer32 QUIC.Spec.VarInt.serialize_varint
QUIC.UInt62.t LowStar.Monotonic.Buffer.srel LowParse.Bytes.byte LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t FStar.UInt64.lt FStar.UInt64.__uint_to_t Prims.bool Prims.unit QUIC.Impl.VarInt.seq_slice_i_j_k LowStar.Monotonic.Buffer.as_seq FStar.UInt32.v Prims.op_Addition FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.UInt32.add LowParse.Low.Base.frame_serializer32 LowParse.Spec.Int.parse_u8_kind FStar.UInt8.t LowParse.Spec.Int.parse_u8 LowParse.Spec.Int.serialize_u8 LowParse.Low.Int.serialize32_u8 FStar.Int.Cast.uint64_to_uint8 FStar.Ghost.hide LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.BoundedInt.serialize_bounded_integer LowParse.Low.BoundedInt.serialize32_bounded_integer_3 FStar.Int.Cast.uint64_to_uint32 FStar.UInt64.rem LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Int.parse_u32_kind FStar.Pervasives.Native.tuple2 LowParse.Spec.Combinators.nondep_then LowParse.Spec.Int.parse_u32 LowParse.Spec.Combinators.serialize_nondep_then LowParse.Spec.Int.serialize_u32 LowParse.Low.Combinators.serialize32_nondep_then LowParse.Low.Int.serialize32_u32 FStar.Pervasives.Native.Mktuple2 FStar.UInt64.div FStar.Ghost.erased FStar.UInt32.uint_to_t FStar.Seq.Base.length LowParse.Spec.Base.serialize QUIC.Spec.VarInt.parse_varint_kind QUIC.Spec.VarInt.parse_varint QUIC.Spec.VarInt.serialize_varint QUIC.Spec.VarInt.get_first_byte FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 Prims._assert Prims.l_or Prims.b2t Prims.op_GreaterThan FStar.UInt.size FStar.UInt64.n FStar.UInt64.v QUIC.UInt62.bound
let write_varint x #rrel #rel b pos =
  
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);
let fb = get_first_byte x in
let gpos' =
  Ghost.hide (pos `U32.add` (U32.uint_to_t (Seq.length (serialize serialize_varint x))))
in
let len1 = LL.frame_serializer32 LI.serialize32_u8 fb b (Ghost.hide pos) gpos' pos in
let pos1 = pos `U32.add` len1 in
if x `U64.lt` 64uL
then len1
else
  let len2 =
    if x `U64.lt` 16384uL
    then
      LL.frame_serializer32 LI.serialize32_u8 (Cast.uint64_to_uint8 x) b (Ghost.hide pos) gpos' pos1
    else
      if x `U64.lt` 1073741824uL
      then
        LL.frame_serializer32 (LL.serialize32_bounded_integer_3 ())
          (Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
          b
          (Ghost.hide pos)
          gpos'
          pos1
      else
        LL.frame_serializer32 (LC.serialize32_nondep_then LI.serialize32_u32
              (LL.serialize32_bounded_integer_3 ()))
          (Cast.uint64_to_uint32 (x `U64.div` 16777216uL),
            Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
          b
          (Ghost.hide pos)
          gpos'
          pos1
  in
  let res = len1 `U32.add` len2 in
  let h' = HST.get () in
  seq_slice_i_j_k (B.as_seq h' b) (U32.v pos) (U32.v pos1) (U32.v pos + U32.v res);
  res