val serialize32_varint_payload (x: U62.t) : Tot B32.bytes
let serialize32_varint_payload
  (x: U62.t)
: Tot B32.bytes
=
  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);
  if x `U64.lt` 64uL
  then B32.empty_bytes
  else if x `U64.lt` 16384uL
  then LP.serialize32_u8 (Cast.uint64_to_uint8 x)
  else if x `U64.lt` 1073741824uL
  then (LP.serialize32_bounded_integer 3) (Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
  else (LP.serialize32_u32 `LP.serialize32_nondep_then` LP.serialize32_bounded_integer 3) (Cast.uint64_to_uint32 (x `U64.div` 16777216uL), Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
val serialize32_varint_payload (x: U62.t) : Tot B32.bytes
let serialize32_varint_payload (x: U62.t) : Tot B32.bytes =
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);
if x `U64.lt` 64uL
then B32.empty_bytes
else
  if x `U64.lt` 16384uL
  then LP.serialize32_u8 (Cast.uint64_to_uint8 x)
  else
    if x `U64.lt` 1073741824uL
    then (LP.serialize32_bounded_integer 3) (Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
    else
      (LP.serialize32_u32 `LP.serialize32_nondep_then` (LP.serialize32_bounded_integer 3)) (Cast.uint64_to_uint32
            (x `U64.div` 16777216uL),
          Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
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
QUIC.UInt62.t FStar.UInt64.lt FStar.UInt64.__uint_to_t FStar.Bytes.empty_bytes Prims.bool LowParse.SLow.Int.serialize32_u8 FStar.Int.Cast.uint64_to_uint8 LowParse.SLow.BoundedInt.serialize32_bounded_integer FStar.Int.Cast.uint64_to_uint32 FStar.UInt64.rem LowParse.SLow.Combinators.serialize32_nondep_then LowParse.Spec.Int.parse_u32_kind FStar.UInt32.t LowParse.Spec.Int.parse_u32 LowParse.Spec.Int.serialize_u32 LowParse.SLow.Int.serialize32_u32 LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.BoundedInt.serialize_bounded_integer FStar.Pervasives.Native.Mktuple2 FStar.UInt64.div FStar.Bytes.bytes Prims.unit 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
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 })
: 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)
   )
   ()

let serialize32_varint_payload
  (x: U62.t)
: Tot B32.bytes
val serialize32_varint_payload (x: U62.t) : Tot B32.bytes
x: QUIC.UInt62.t -> FStar.Bytes.bytes