val parse_vldata_payload
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (i: bounded_integer sz {f i == true})
    : Tot (parser (parse_vldata_payload_kind sz k) t)
let parse_vldata_payload
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (i: bounded_integer sz { f i == true } )
: Tot (parser (parse_vldata_payload_kind sz k) t)
= weaken (parse_vldata_payload_kind sz k) (parse_fldata p (U32.v i))
val parse_vldata_payload
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (i: bounded_integer sz {f i == true})
    : Tot (parser (parse_vldata_payload_kind sz k) t)
let parse_vldata_payload
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (i: bounded_integer sz {f i == true})
    : Tot (parser (parse_vldata_payload_kind sz k) t) =
weaken (parse_vldata_payload_kind sz k) (parse_fldata p (U32.v i))
LowParse.Spec.VLData.fsti.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked LowParse.Spec.AllIntegers.fst.checked LowParse.Math.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.VLData.fsti
LowParse.Spec.BoundedInt.integer_size LowParse.Spec.BoundedInt.bounded_integer Prims.bool LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser Prims.eq2 LowParse.Spec.Base.weaken LowParse.Spec.VLData.parse_vldata_payload_kind LowParse.Spec.FLData.parse_fldata_kind FStar.UInt32.v LowParse.Spec.FLData.parse_fldata
module LowParse.Spec.VLData
include LowParse.Spec.FLData
include LowParse.Spec.AllIntegers // for bounded_integer, in_bounds, etc.

module Seq = FStar.Seq
module U32 = FStar.UInt32
module M = LowParse.Math

#reset-options "--z3rlimit 64 --max_fuel 64 --max_ifuel 64 --z3refresh --z3cliopt smt.arith.nl=false"

let parse_vldata_payload_size
  (sz: integer_size)
: Pure nat
  (requires True)
  (ensures (fun y -> y == pow2 (FStar.Mul.op_Star 8 sz) - 1 ))
= match sz with
  | 1 -> 255
  | 2 -> 65535
  | 3 -> 16777215
  | 4 -> 4294967295

#reset-options

// unfold
let parse_vldata_payload_kind
  (sz: integer_size)
  (k: parser_kind)
: parser_kind
= strong_parser_kind 0 (parse_vldata_payload_size sz) (
    match k.parser_kind_metadata with
    | Some ParserKindMetadataFail -> Some ParserKindMetadataFail
    | _ -> None
  )

let parse_vldata_payload
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (i: bounded_integer sz { f i == true } )
val parse_vldata_payload
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (i: bounded_integer sz {f i == true})
    : Tot (parser (parse_vldata_payload_kind sz k) t)

    sz: LowParse.Spec.BoundedInt.integer_size ->
    f: (_: LowParse.Spec.BoundedInt.bounded_integer sz -> Prims.GTot Prims.bool) ->
    p: LowParse.Spec.Base.parser k t ->
    i: LowParse.Spec.BoundedInt.bounded_integer sz {f i == true}
  -> LowParse.Spec.Base.parser (LowParse.Spec.VLData.parse_vldata_payload_kind sz k) t