val parse32_vldata_gen
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (f': (x: bounded_integer sz -> Tot (y: bool{y == f x})))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
    : Tot (parser32 (parse_vldata_gen sz f p))
let parse32_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (f' : (x: bounded_integer sz) -> Tot (y: bool {y == f x}))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
: Tot (parser32 (parse_vldata_gen sz f p))
= [@inline_let]
  let _ = parse_vldata_gen_eq_def sz f p in
  parse32_and_then
    (parse32_filter (parse32_bounded_integer sz) f f')
    (parse_vldata_payload sz f p)
    ()
    (parse32_vldata_payload sz f p32)
val parse32_vldata_gen
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (f': (x: bounded_integer sz -> Tot (y: bool{y == f x})))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
    : Tot (parser32 (parse_vldata_gen sz f p))
let parse32_vldata_gen
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (f': (x: bounded_integer sz -> Tot (y: bool{y == f x})))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
    : Tot (parser32 (parse_vldata_gen sz f p)) =
[@@ inline_let ]let _ = parse_vldata_gen_eq_def sz f p in
parse32_and_then (parse32_filter (parse32_bounded_integer sz) f f')
  (parse_vldata_payload sz f p)
  ()
  (parse32_vldata_payload sz f p32)
LowParse.SLow.VLData.fst.checked
prims.fst.checked LowParse.Spec.VLData.fsti.checked LowParse.SLow.FLData.fst.checked LowParse.SLow.BoundedInt.fsti.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.VLData.fst
LowParse.Spec.BoundedInt.integer_size LowParse.Spec.BoundedInt.bounded_integer Prims.bool Prims.eq2 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.SLow.Base.parser32 LowParse.SLow.Combinators.parse32_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.SLow.Combinators.parse32_filter LowParse.SLow.BoundedInt.parse32_bounded_integer LowParse.Spec.VLData.parse_vldata_payload_kind LowParse.Spec.VLData.parse_vldata_payload LowParse.SLow.VLData.parse32_vldata_payload Prims.unit LowParse.Spec.VLData.parse_vldata_gen_eq_def LowParse.Spec.VLData.parse_vldata_gen_kind LowParse.Spec.VLData.parse_vldata_gen
module LowParse.SLow.VLData
include LowParse.Spec.VLData
include LowParse.SLow.FLData
include LowParse.SLow.BoundedInt // for bounded_integer

module Seq = FStar.Seq
module U32 = FStar.UInt32
module B32 = LowParse.Bytes32

(* Parsers and serializers for the payload *)

inline_for_extraction
let parse32_vldata_payload
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
  (i: bounded_integer sz { f i == true } )
: Tot (parser32 (parse_vldata_payload sz f p i))
= fun (input: bytes32) -> parse32_fldata p32 (U32.v i) i input

inline_for_extraction
let parse32_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (f' : (x: bounded_integer sz) -> Tot (y: bool {y == f x}))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
val parse32_vldata_gen
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (f': (x: bounded_integer sz -> Tot (y: bool{y == f x})))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (p32: parser32 p)
    : Tot (parser32 (parse_vldata_gen sz f p))

    sz: LowParse.Spec.BoundedInt.integer_size ->
    f: (_: LowParse.Spec.BoundedInt.bounded_integer sz -> Prims.GTot Prims.bool) ->
    f': (x: LowParse.Spec.BoundedInt.bounded_integer sz -> y: Prims.bool{y == f x}) ->
    p32: LowParse.SLow.Base.parser32 p
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.VLData.parse_vldata_gen sz f p)