val parse_vldata_gen_eq_def
  (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) /\
  parse_vldata_gen_kind sz k == and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k) /\
  parse_vldata_gen sz f p ==
  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))
let parse_vldata_gen_eq_def
  (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) /\
  parse_vldata_gen_kind sz k == and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k) /\
  parse_vldata_gen sz f p ==
  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))
= parse_fldata_and_then_cases_injective sz f p;
  parse_vldata_gen_kind_correct sz k
val parse_vldata_gen_eq_def
  (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) /\
  parse_vldata_gen_kind sz k == and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k) /\
  parse_vldata_gen sz f p ==
  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))
let parse_vldata_gen_eq_def
      (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) /\
      parse_vldata_gen_kind sz k ==
      and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz))
        (parse_vldata_payload_kind sz k) /\
      parse_vldata_gen sz f p ==
      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)) =
parse_fldata_and_then_cases_injective sz f p;
parse_vldata_gen_kind_correct sz k
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.VLData.parse_vldata_gen_kind_correct Prims.unit LowParse.Spec.VLData.parse_fldata_and_then_cases_injective Prims.l_True Prims.squash Prims.l_and LowParse.Spec.Combinators.and_then_cases_injective Prims.eq2 LowParse.Spec.VLData.parse_vldata_payload LowParse.Spec.VLData.parse_vldata_gen_kind LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.VLData.parse_vldata_payload_kind LowParse.Spec.VLData.parse_vldata_gen LowParse.Spec.Combinators.and_then LowParse.Spec.Combinators.parse_filter_refine LowParse.Spec.Combinators.parse_filter LowParse.Spec.BoundedInt.parse_bounded_integer Prims.Nil FStar.Pervasives.pattern
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)
: 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)

let parse_vldata_gen_eq_def
  (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) /\
  parse_vldata_gen_kind sz k == and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k) /\
  parse_vldata_gen sz f p ==
  and_then
    #_
    #(parse_filter_refine #(bounded_integer sz) f)
    (parse_filter #_ #(bounded_integer sz) (parse_bounded_integer sz) f)
    #_
    #t
val parse_vldata_gen_eq_def
  (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) /\
  parse_vldata_gen_kind sz k == and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k) /\
  parse_vldata_gen sz f p ==
  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))

    sz: LowParse.Spec.BoundedInt.integer_size ->
    f: (_: LowParse.Spec.BoundedInt.bounded_integer sz -> Prims.GTot Prims.bool) ->
    p: LowParse.Spec.Base.parser k t
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Combinators.and_then_cases_injective (LowParse.Spec.VLData.parse_vldata_payload sz
            f
            p) /\
      LowParse.Spec.VLData.parse_vldata_gen_kind sz k ==
      LowParse.Spec.Combinators.and_then_kind (LowParse.Spec.Combinators.parse_filter_kind (LowParse.Spec.BoundedInt.parse_bounded_integer_kind
                sz))
        (LowParse.Spec.VLData.parse_vldata_payload_kind sz k) /\
      LowParse.Spec.VLData.parse_vldata_gen sz f p ==
      LowParse.Spec.Combinators.and_then (LowParse.Spec.Combinators.parse_filter (LowParse.Spec.BoundedInt.parse_bounded_integer
                sz)
            f)
        (LowParse.Spec.VLData.parse_vldata_payload sz f p))