val parse_vldata_gen_eq
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes)
    : Lemma
    (let res = parse (parse_vldata_gen sz f p) input in
      match parse (parse_bounded_integer sz) input with
      | None -> res == None
      | Some (len, consumed_len) ->
        consumed_len == sz /\
        (if f len
          then
            if Seq.length input < sz + U32.v len
            then res == None
            else
              let input' = Seq.slice input sz (sz + U32.v len) in
              match parse p input' with
              | Some (x, consumed_x) ->
                if consumed_x = U32.v len then res == Some (x, sz + U32.v len) else res == None
              | _ -> res == None
          else res == None))
let parse_vldata_gen_eq
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input: bytes)
: Lemma
  (let res = parse (parse_vldata_gen sz f p) input in
    match parse (parse_bounded_integer sz) input with
  | None -> res == None
  | Some (len, consumed_len) ->
    consumed_len == sz /\ (
    if f len
    then begin
      if Seq.length input < sz + U32.v len
      then res == None
      else
      let input' = Seq.slice input sz (sz + U32.v len) in
      match parse p input' with
      | Some (x, consumed_x) ->
        if consumed_x = U32.v len
        then res == Some (x, sz + U32.v len)
        else res == None
      | _ -> res == None
    end
    else res == None
  ))
= parse_vldata_gen_eq_def sz f p;
  and_then_eq #_ #(parse_filter_refine f) (parse_filter (parse_bounded_integer sz) f) #_ #t (parse_vldata_payload sz f p) input;
  parse_filter_eq #_ #(bounded_integer sz) (parse_bounded_integer sz) f input;
  parser_kind_prop_equiv (parse_bounded_integer_kind sz) (parse_bounded_integer sz);
  ()
val parse_vldata_gen_eq
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes)
    : Lemma
    (let res = parse (parse_vldata_gen sz f p) input in
      match parse (parse_bounded_integer sz) input with
      | None -> res == None
      | Some (len, consumed_len) ->
        consumed_len == sz /\
        (if f len
          then
            if Seq.length input < sz + U32.v len
            then res == None
            else
              let input' = Seq.slice input sz (sz + U32.v len) in
              match parse p input' with
              | Some (x, consumed_x) ->
                if consumed_x = U32.v len then res == Some (x, sz + U32.v len) else res == None
              | _ -> res == None
          else res == None))
let parse_vldata_gen_eq
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes)
    : Lemma
    (let res = parse (parse_vldata_gen sz f p) input in
      match parse (parse_bounded_integer sz) input with
      | None -> res == None
      | Some (len, consumed_len) ->
        consumed_len == sz /\
        (if f len
          then
            if Seq.length input < sz + U32.v len
            then res == None
            else
              let input' = Seq.slice input sz (sz + U32.v len) in
              match parse p input' with
              | Some (x, consumed_x) ->
                if consumed_x = U32.v len then res == Some (x, sz + U32.v len) else res == None
              | _ -> res == None
          else res == None)) =
parse_vldata_gen_eq_def sz f p;
and_then_eq #_
  #(parse_filter_refine f)
  (parse_filter (parse_bounded_integer sz) f)
  #_
  #t
  (parse_vldata_payload sz f p)
  input;
parse_filter_eq #_ #(bounded_integer sz) (parse_bounded_integer sz) f input;
parser_kind_prop_equiv (parse_bounded_integer_kind sz) (parse_bounded_integer sz);
()
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.BoundedInt.bounded_integer Prims.bool LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Bytes.bytes Prims.unit LowParse.Spec.Base.parser_kind_prop_equiv LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.Combinators.parse_filter_eq LowParse.Spec.Combinators.and_then_eq LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Combinators.parse_filter_refine LowParse.Spec.Combinators.parse_filter LowParse.Spec.VLData.parse_vldata_payload_kind LowParse.Spec.VLData.parse_vldata_payload LowParse.Spec.VLData.parse_vldata_gen_eq_def Prims.l_True Prims.squash LowParse.Spec.Base.parse Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length FStar.Pervasives.Native.None Prims.l_and Prims.nat Prims.l_or Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length LowParse.Bytes.byte Prims.op_LessThan Prims.op_Addition FStar.UInt32.v Prims.op_Equality Prims.int Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.logical FStar.Seq.Base.seq FStar.Seq.Base.slice LowParse.Spec.VLData.parse_vldata_gen 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_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)
: Tot parser_kind
= strong_parser_kind sz (sz + parse_vldata_payload_size sz) (
    match k.parser_kind_metadata with
    | Some ParserKindMetadataFail -> Some ParserKindMetadataFail
    | _ -> None
  )

let parse_vldata_gen_kind_correct
  (sz: integer_size)
  (k: parser_kind)
: Lemma
  ( (parse_vldata_gen_kind sz k) == (and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k)))
= let kl = parse_vldata_gen_kind sz k in
  let kr = and_then_kind (parse_filter_kind (parse_bounded_integer_kind sz)) (parse_vldata_payload_kind sz k) in
  assert_norm (kl == kr)

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)

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
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input: bytes)
: Lemma
  (let res = parse (parse_vldata_gen sz f p) input in
    match parse (parse_bounded_integer sz) input with
  | None -> res == None
  | Some (len, consumed_len) ->
    consumed_len == sz /\ (
    if f len
    then begin
      if Seq.length input < sz + U32.v len
      then res == None
      else
      let input' = Seq.slice input sz (sz + U32.v len) in
      match parse p input' with
      | Some (x, consumed_x) ->
        if consumed_x = U32.v len
        then res == Some (x, sz + U32.v len)
        else res == None
      | _ -> res == None
    end
    else res == None
val parse_vldata_gen_eq
      (sz: integer_size)
      (f: (bounded_integer sz -> GTot bool))
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes)
    : Lemma
    (let res = parse (parse_vldata_gen sz f p) input in
      match parse (parse_bounded_integer sz) input with
      | None -> res == None
      | Some (len, consumed_len) ->
        consumed_len == sz /\
        (if f len
          then
            if Seq.length input < sz + U32.v len
            then res == None
            else
              let input' = Seq.slice input sz (sz + U32.v len) in
              match parse p input' with
              | Some (x, consumed_x) ->
                if consumed_x = U32.v len then res == Some (x, sz + U32.v len) else res == None
              | _ -> res == None
          else res == None))

    sz: LowParse.Spec.BoundedInt.integer_size ->
    f: (_: LowParse.Spec.BoundedInt.bounded_integer sz -> Prims.GTot Prims.bool) ->
    p: LowParse.Spec.Base.parser k t ->
    input: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
    (ensures
      (let res = LowParse.Spec.Base.parse (LowParse.Spec.VLData.parse_vldata_gen sz f p) input in
        (match
            LowParse.Spec.Base.parse (LowParse.Spec.BoundedInt.parse_bounded_integer sz) input
          with
          | FStar.Pervasives.Native.None #_ -> res == FStar.Pervasives.Native.None
          | FStar.Pervasives.Native.Some
            #_
            (FStar.Pervasives.Native.Mktuple2 #_ #_ len consumed_len) ->
            consumed_len == sz /\
            (match f len with
              | true ->
                (match FStar.Seq.Base.length input < sz + FStar.UInt32.v len with
                  | true -> res == FStar.Pervasives.Native.None
                  | _ ->
                    let input' = FStar.Seq.Base.slice input sz (sz + FStar.UInt32.v len) in
                    (match LowParse.Spec.Base.parse p input' with
                      | FStar.Pervasives.Native.Some
                        #_
                        (FStar.Pervasives.Native.Mktuple2 #_ #_ x consumed_x) ->
                        (match consumed_x = FStar.UInt32.v len with
                          | true -> res == FStar.Pervasives.Native.Some (x, sz + FStar.UInt32.v len)
                          | _ -> res == FStar.Pervasives.Native.None)
                        <:
                        Prims.logical
                      | _ -> res == FStar.Pervasives.Native.None)
                    <:
                    Prims.logical)
                <:
                Prims.logical
              | _ -> res == FStar.Pervasives.Native.None))
        <:
        Type0))