val 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))
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
val 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))
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
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 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.SLow.Base.parser32 Prims.eq2 LowParse.SLow.Base.bytes32 LowParse.SLow.FLData.parse32_fldata FStar.UInt32.v FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 FStar.UInt32.t LowParse.SLow.Base.parser32_correct LowParse.Spec.VLData.parse_vldata_payload_kind LowParse.Spec.VLData.parse_vldata_payload
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 } )
val 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))

    sz: LowParse.Spec.BoundedInt.integer_size ->
    f: (_: LowParse.Spec.BoundedInt.bounded_integer sz -> Prims.GTot Prims.bool) ->
    p32: LowParse.SLow.Base.parser32 p ->
    i: LowParse.Spec.BoundedInt.bounded_integer sz {f i == true}
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.VLData.parse_vldata_payload sz f p i)