val parse_bounded_vldata_elim_forall
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (l: nat{l >= log256' max /\ l <= 4})
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (xbytes: bytes)
    : Lemma (requires (Some? (parse (parse_bounded_vldata' min max l p) xbytes)))
      (ensures
        (let Some (x, consumed) = parse (parse_bounded_vldata' min max l p) xbytes in
          let sz:integer_size = l in
          let plen = parse (parse_bounded_integer sz) xbytes in
          Some? plen /\
          (let Some (len, consumed_len) = plen in
            (consumed_len <: nat) == (sz <: nat) /\ in_bounds min max len /\
            U32.v len <= Seq.length xbytes - sz /\
            (let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
              let pp = parse p input' in
              Some? pp /\
              (let Some (x', consumed_p) = pp in
                x' == x /\ (consumed_p <: nat) == U32.v len /\ (consumed <: nat) == sz + U32.v len))
          )))
let parse_bounded_vldata_elim_forall
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (xbytes: bytes)
: Lemma
  (requires (Some? (parse (parse_bounded_vldata' min max l p) xbytes)))
  (ensures (
    let (Some (x, consumed)) = parse (parse_bounded_vldata' min max l p) xbytes in
    let sz : integer_size = l in
    let plen = parse (parse_bounded_integer sz) xbytes in
    Some? plen /\ (
    let (Some (len, consumed_len)) = plen in
    (consumed_len <: nat) == (sz <: nat) /\
    in_bounds min max len /\
    U32.v len <= Seq.length xbytes - sz /\ (
    let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
    let pp = parse p input' in
    Some? pp /\ (
    let (Some (x', consumed_p)) = pp in
    x' == x /\
    (consumed_p <: nat) == U32.v len /\
    (consumed <: nat) == sz + U32.v len
  )))))
= let (Some (x, consumed)) = parse (parse_bounded_vldata' min max l p) xbytes in
  parse_bounded_vldata_elim min max l p xbytes x consumed
val parse_bounded_vldata_elim_forall
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (l: nat{l >= log256' max /\ l <= 4})
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (xbytes: bytes)
    : Lemma (requires (Some? (parse (parse_bounded_vldata' min max l p) xbytes)))
      (ensures
        (let Some (x, consumed) = parse (parse_bounded_vldata' min max l p) xbytes in
          let sz:integer_size = l in
          let plen = parse (parse_bounded_integer sz) xbytes in
          Some? plen /\
          (let Some (len, consumed_len) = plen in
            (consumed_len <: nat) == (sz <: nat) /\ in_bounds min max len /\
            U32.v len <= Seq.length xbytes - sz /\
            (let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
              let pp = parse p input' in
              Some? pp /\
              (let Some (x', consumed_p) = pp in
                x' == x /\ (consumed_p <: nat) == U32.v len /\ (consumed <: nat) == sz + U32.v len))
          )))
let parse_bounded_vldata_elim_forall
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (l: nat{l >= log256' max /\ l <= 4})
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (xbytes: bytes)
    : Lemma (requires (Some? (parse (parse_bounded_vldata' min max l p) xbytes)))
      (ensures
        (let Some (x, consumed) = parse (parse_bounded_vldata' min max l p) xbytes in
          let sz:integer_size = l in
          let plen = parse (parse_bounded_integer sz) xbytes in
          Some? plen /\
          (let Some (len, consumed_len) = plen in
            (consumed_len <: nat) == (sz <: nat) /\ in_bounds min max len /\
            U32.v len <= Seq.length xbytes - sz /\
            (let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
              let pp = parse p input' in
              Some? pp /\
              (let Some (x', consumed_p) = pp in
                x' == x /\ (consumed_p <: nat) == U32.v len /\ (consumed <: nat) == sz + U32.v len))
          ))) =
let Some (x, consumed) = parse (parse_bounded_vldata' min max l p) xbytes in
parse_bounded_vldata_elim min max l p xbytes x consumed
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
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_GreaterThan Prims.op_LessThan Prims.op_GreaterThanOrEqual LowParse.Spec.BoundedInt.log256' LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Bytes.bytes LowParse.Spec.Base.consumed_length LowParse.Spec.VLData.parse_bounded_vldata_elim Prims.unit FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.parse LowParse.Spec.VLData.parse_bounded_vldata' FStar.Pervasives.Native.uu___is_Some Prims.squash LowParse.Spec.BoundedInt.bounded_integer Prims.eq2 LowParse.Spec.BoundedInt.in_bounds FStar.UInt32.v Prims.op_Subtraction FStar.Seq.Base.length LowParse.Bytes.byte Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_Addition Prims.logical FStar.Seq.Base.seq FStar.Seq.Base.slice LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.BoundedInt.integer_size 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
  ))
= 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);
  ()

let parse_vldata_gen_eq_some_elim
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input: bytes)
: Lemma
  (requires (Some? (parse (parse_vldata_gen sz f p) input)))
  (ensures (
    let pbi = parse (parse_bounded_integer sz) input in
    Some? pbi /\ (
    let Some (len, consumed_len) = pbi in
    consumed_len == sz /\
    f len /\
    Seq.length input >= sz + U32.v len /\ (
    let input' = Seq.slice input sz (sz + U32.v len) in
    let pp = parse p input' in
    Some? pp /\ (
    let Some (x, consumed_x) = pp in
    consumed_x = U32.v len /\
    parse (parse_vldata_gen sz f p) input == Some (x, sz + U32.v len)
  )))))
= parse_vldata_gen_eq sz f p input

let unconstrained_bounded_integer
  (sz: integer_size)
  (i: bounded_integer sz)
: GTot bool
= true

let parse_vldata
  (sz: integer_size)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser _ t)
= parse_vldata_gen sz (unconstrained_bounded_integer sz) p

let parse_vldata_eq
  (sz: integer_size)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input: bytes)
: Lemma
  (parse (parse_vldata sz p) input == (match parse (parse_bounded_integer sz) input with
  | None -> None
  | Some (len, _) ->
    begin
      if Seq.length input < sz + U32.v len
      then 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 Some (x, sz + U32.v len)
        else None
      | _ -> None
    end
  ))
= parse_vldata_gen_eq sz (unconstrained_bounded_integer _) p input

(** Explicit bounds on size *)

#reset-options

inline_for_extraction
let parse_bounded_vldata_strong_kind
  (min: nat)
  (max: nat)
  (l: nat)
  (k: parser_kind)
: Pure parser_kind
  (requires (min <= max /\ max > 0 /\ max < 4294967296 /\ l >= log256' max /\ l <= 4 ))
  (ensures (fun _ -> True))
= [@inline_let]
  let kmin = k.parser_kind_low in
  [@inline_let]
  let min' = if kmin > min then kmin else min in
  [@inline_let]
  let max' = match k.parser_kind_high with
  | None -> max
  | Some kmax -> if kmax < max then kmax else max
  in
  [@inline_let]
  let max' = if max' < min' then min' else max' in
  (* the size of the length prefix must conform to the max bound given by the user, not on the metadata *)
  strong_parser_kind (l + min') (l + max') (
    match k.parser_kind_metadata with
    | Some ParserKindMetadataFail -> Some ParserKindMetadataFail
    | _ -> None
  )

let parse_bounded_vldata_elim'
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (xbytes: bytes)
  (x: t)
  (consumed: consumed_length xbytes)
: Lemma
  (requires (parse (parse_vldata_gen l (in_bounds min max) p) xbytes == Some (x, consumed)))
  (ensures (
    let sz : integer_size = l in
    let plen = parse (parse_bounded_integer sz) xbytes in
    Some? plen /\ (
    let (Some (len, consumed_len)) = plen in
    (consumed_len <: nat) == (sz <: nat) /\
    in_bounds min max len /\
    U32.v len <= Seq.length xbytes - sz /\ (
    let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
    let pp = parse p input' in
    Some? pp /\ (
    let (Some (x', consumed_p)) = pp in
    x' == x /\
    (consumed_p <: nat) == U32.v len /\
    (consumed <: nat) == sz + U32.v len
  )))))
= parse_vldata_gen_eq l (in_bounds min max) p xbytes;
  parser_kind_prop_equiv (parse_bounded_integer_kind l) (parse_bounded_integer l)

let parse_bounded_vldata_correct
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Lemma
  (parser_kind_prop (parse_bounded_vldata_strong_kind min max l k) (parse_vldata_gen l (in_bounds min max) p))
= parser_kind_prop_equiv (parse_bounded_vldata_strong_kind min max l k) (parse_vldata_gen l (in_bounds min max) p);
  let sz : integer_size = l in
  let p' = parse_vldata_gen sz (in_bounds min max) p in
  parser_kind_prop_equiv (get_parser_kind p') p';
  parser_kind_prop_equiv k p;
  let k' = parse_bounded_vldata_strong_kind min max l k in
  let prf
    (input: bytes)
  : Lemma
    (requires (Some? (parse p' input)))
    (ensures (
      let pi = parse p' input in
      Some? pi /\ (
      let (Some (_, consumed)) = pi in
      k'.parser_kind_low <= (consumed <: nat) /\
      (consumed <: nat) <= Some?.v k'.parser_kind_high
    )))
  = let (Some (data, consumed)) = parse p' input in
    parse_bounded_vldata_elim' min max l p input data consumed
  in
  Classical.forall_intro (Classical.move_requires prf)

let parse_bounded_vldata'
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser (parse_bounded_vldata_strong_kind min max l k) t)
= parse_bounded_vldata_correct min max l p;
  strengthen (parse_bounded_vldata_strong_kind min max l k) (parse_vldata_gen l (in_bounds min max) p)

let parse_bounded_vldata
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser (parse_bounded_vldata_strong_kind min max (log256' max) k) t)
= parse_bounded_vldata' min max (log256' max) p

let parse_bounded_vldata_elim
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (xbytes: bytes)
  (x: t)
  (consumed: consumed_length xbytes)
: Lemma
  (requires (parse (parse_bounded_vldata' min max l p) xbytes == Some (x, consumed)))
  (ensures (
    let sz : integer_size = l in
    let plen = parse (parse_bounded_integer sz) xbytes in
    Some? plen /\ (
    let (Some (len, consumed_len)) = plen in
    (consumed_len <: nat) == (sz <: nat) /\
    in_bounds min max len /\
    U32.v len <= Seq.length xbytes - sz /\ (
    let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
    let pp = parse p input' in
    Some? pp /\ (
    let (Some (x', consumed_p)) = pp in
    x' == x /\
    (consumed_p <: nat) == U32.v len /\
    (consumed <: nat) == sz + U32.v len
  )))))
= parse_bounded_vldata_elim' min max l p xbytes x consumed

let parse_bounded_vldata_elim_forall
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (xbytes: bytes)
: Lemma
  (requires (Some? (parse (parse_bounded_vldata' min max l p) xbytes)))
  (ensures (
    let (Some (x, consumed)) = parse (parse_bounded_vldata' min max l p) xbytes in
    let sz : integer_size = l in
    let plen = parse (parse_bounded_integer sz) xbytes in
    Some? plen /\ (
    let (Some (len, consumed_len)) = plen in
    (consumed_len <: nat) == (sz <: nat) /\
    in_bounds min max len /\
    U32.v len <= Seq.length xbytes - sz /\ (
    let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
    let pp = parse p input' in
    Some? pp /\ (
    let (Some (x', consumed_p)) = pp in
    x' == x /\
    (consumed_p <: nat) == U32.v len /\
    (consumed <: nat) == sz + U32.v len
val parse_bounded_vldata_elim_forall
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (l: nat{l >= log256' max /\ l <= 4})
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (xbytes: bytes)
    : Lemma (requires (Some? (parse (parse_bounded_vldata' min max l p) xbytes)))
      (ensures
        (let Some (x, consumed) = parse (parse_bounded_vldata' min max l p) xbytes in
          let sz:integer_size = l in
          let plen = parse (parse_bounded_integer sz) xbytes in
          Some? plen /\
          (let Some (len, consumed_len) = plen in
            (consumed_len <: nat) == (sz <: nat) /\ in_bounds min max len /\
            U32.v len <= Seq.length xbytes - sz /\
            (let input' = Seq.slice xbytes (sz <: nat) (sz + U32.v len) in
              let pp = parse p input' in
              Some? pp /\
              (let Some (x', consumed_p) = pp in
                x' == x /\ (consumed_p <: nat) == U32.v len /\ (consumed <: nat) == sz + U32.v len))
          )))

    min: Prims.nat ->
    max: Prims.nat{min <= max /\ max > 0 /\ max < 4294967296} ->
    l: Prims.nat{l >= LowParse.Spec.BoundedInt.log256' max /\ l <= 4} ->
    p: LowParse.Spec.Base.parser k t ->
    xbytes: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
      (requires
        Some? (LowParse.Spec.Base.parse (LowParse.Spec.VLData.parse_bounded_vldata' min max l p)
              xbytes))
      (ensures
        (let _ =
            LowParse.Spec.Base.parse (LowParse.Spec.VLData.parse_bounded_vldata' min max l p) xbytes
          in
          (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ x consumed) =
              _
            in
            let sz = l in
            let plen =
              LowParse.Spec.Base.parse (LowParse.Spec.BoundedInt.parse_bounded_integer sz) xbytes
            in
            Some? plen /\
            (let _ = plen in
              (let
                FStar.Pervasives.Native.Some
                  #_
                  (FStar.Pervasives.Native.Mktuple2 #_ #_ len consumed_len) =
                  _
                in
                consumed_len == sz /\ LowParse.Spec.BoundedInt.in_bounds min max len /\
                FStar.UInt32.v len <= FStar.Seq.Base.length xbytes - sz /\
                (let input' = FStar.Seq.Base.slice xbytes sz (sz + FStar.UInt32.v len) in
                  let pp = LowParse.Spec.Base.parse p input' in
                  Some? pp /\
                  (let _ = pp in
                    (let
                      FStar.Pervasives.Native.Some
                        #_
                        (FStar.Pervasives.Native.Mktuple2 #_ #_ x' consumed_p) =
                        _
                      in
                      x' == x /\ consumed_p == FStar.UInt32.v len /\
                      consumed == sz + FStar.UInt32.v len)
                    <:
                    Prims.logical)))
              <:
              Prims.logical))
          <:
          Type0))