val parse_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser (parse_vldata_gen_kind sz k) t)
let parse_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser (parse_vldata_gen_kind sz k) t)
= parse_fldata_and_then_cases_injective sz f p;
  parse_vldata_gen_kind_correct sz k;
  and_then
    #_
    #(parse_filter_refine #(bounded_integer sz) f)
    (parse_filter #_ #(bounded_integer sz) (parse_bounded_integer sz) f)
    #_
    #t
    (parse_vldata_payload sz f p)
val parse_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser (parse_vldata_gen_kind sz k) t)
let parse_vldata_gen
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
    : Tot (parser (parse_vldata_gen_kind sz k) t) =
parse_fldata_and_then_cases_injective sz f p;
parse_vldata_gen_kind_correct sz k;
and_then #_
  #(parse_filter_refine #(bounded_integer sz) f)
  (parse_filter #_ #(bounded_integer sz) (parse_bounded_integer sz) f)
  #_
  #t
  (parse_vldata_payload sz f p)
LowParse.Spec.VLData.fst.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.fsti.checked
LowParse.Spec.VLData.fst
LowParse.Spec.BoundedInt.integer_size LowParse.Spec.BoundedInt.bounded_integer Prims.bool LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Combinators.and_then LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.Combinators.parse_filter_refine LowParse.Spec.Combinators.parse_filter LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.VLData.parse_vldata_payload_kind LowParse.Spec.VLData.parse_vldata_payload Prims.unit LowParse.Spec.VLData.parse_vldata_gen_kind_correct LowParse.Spec.VLData.parse_fldata_and_then_cases_injective LowParse.Spec.VLData.parse_vldata_gen_kind
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_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
val parse_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser (parse_vldata_gen_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
  -> LowParse.Spec.Base.parser (LowParse.Spec.VLData.parse_vldata_gen_kind sz k) t