val parse_vldata_gen_kind (sz: integer_size) (k: parser_kind) : Tot parser_kind
let parse_vldata_gen_kind
  (sz: integer_size)
  (k: parser_kind)
: Tot parser_kind
= strong_parser_kind sz (sz + parse_vldata_payload_size sz) (
    match k.parser_kind_metadata with
    | Some ParserKindMetadataFail -> Some ParserKindMetadataFail
    | _ -> None
  )
val parse_vldata_gen_kind (sz: integer_size) (k: parser_kind) : Tot parser_kind
let parse_vldata_gen_kind (sz: integer_size) (k: parser_kind) : Tot parser_kind =
strong_parser_kind sz
  (sz + parse_vldata_payload_size sz)
  (match k.parser_kind_metadata with
    | Some ParserKindMetadataFail -> Some ParserKindMetadataFail
    | _ -> None)
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.Base.parser_kind LowParse.Spec.Base.strong_parser_kind Prims.op_Addition LowParse.Spec.VLData.parse_vldata_payload_size LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_metadata FStar.Pervasives.Native.Some LowParse.Spec.Base.parser_kind_metadata_some LowParse.Spec.Base.ParserKindMetadataFail FStar.Pervasives.Native.option FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_t
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 } )
: Tot (parser (parse_vldata_payload_kind sz k) t)
= weaken (parse_vldata_payload_kind sz k) (parse_fldata p (U32.v i))

#set-options "--z3rlimit 64"

let parse_fldata_and_then_cases_injective
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Lemma
  (and_then_cases_injective (parse_vldata_payload sz f p))
= parser_kind_prop_equiv k p;
  let g
    (len1 len2: (len: bounded_integer sz { f len == true } ))
    (b1 b2: bytes)
  : Lemma
    (requires (and_then_cases_injective_precond (parse_vldata_payload sz f p) len1 len2 b1 b2))
    (ensures (len1 == len2))
  = assert (injective_precond p (Seq.slice b1 0 (U32.v len1)) (Seq.slice b2 0 (U32.v len2)));
    assert (injective_postcond p (Seq.slice b1 0 (U32.v len1)) (Seq.slice b2 0 (U32.v len2)));
    assert (len1 == len2)
  in
  let g'
    (len1 len2: (len: bounded_integer sz { f len == true } ))
    (b1: bytes)
  : Lemma
    (forall (b2: bytes) . and_then_cases_injective_precond (parse_vldata_payload sz f p) len1 len2 b1 b2 ==> len1 == len2)
  = Classical.forall_intro (Classical.move_requires (g len1 len2 b1))
  in
  Classical.forall_intro_3 g'

#reset-options

// unfold
let parse_vldata_gen_kind
  (sz: integer_size)
  (k: parser_kind)
val parse_vldata_gen_kind (sz: integer_size) (k: parser_kind) : Tot parser_kind
sz: LowParse.Spec.BoundedInt.integer_size -> k: LowParse.Spec.Base.parser_kind
  -> LowParse.Spec.Base.parser_kind