val parse32_bounded_vldata_strong
      (min: nat)
      (min32: U32.t{U32.v min32 == min})
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (max32: U32.t{U32.v max32 == max})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
    : Tot
    (parser32 #_ #(parse_bounded_vldata_strong_t min max s) (parse_bounded_vldata_strong min max s))
let parse32_bounded_vldata_strong
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
: Tot (parser32 #_ #(parse_bounded_vldata_strong_t min max s) (parse_bounded_vldata_strong min max s))
= parse32_bounded_vldata_strong' min min32 max max32 (log256' max) s p32
val parse32_bounded_vldata_strong
      (min: nat)
      (min32: U32.t{U32.v min32 == min})
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (max32: U32.t{U32.v max32 == max})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
    : Tot
    (parser32 #_ #(parse_bounded_vldata_strong_t min max s) (parse_bounded_vldata_strong min max s))
let parse32_bounded_vldata_strong
      (min: nat)
      (min32: U32.t{U32.v min32 == min})
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (max32: U32.t{U32.v max32 == max})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
    : Tot
    (parser32 #_ #(parse_bounded_vldata_strong_t min max s) (parse_bounded_vldata_strong min max s)) =
parse32_bounded_vldata_strong' min min32 max max32 (log256' max) s p32
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
Prims.nat FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v Prims.l_and Prims.op_LessThanOrEqual Prims.op_GreaterThan Prims.op_LessThan LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.parser32 LowParse.SLow.VLData.parse32_bounded_vldata_strong' LowParse.Spec.BoundedInt.log256' LowParse.Spec.VLData.parse_bounded_vldata_strong_kind LowParse.Spec.VLData.parse_bounded_vldata_strong_t LowParse.Spec.VLData.parse_bounded_vldata_strong
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 } )
: Tot (parser32 (parse_vldata_payload sz f p i))
= fun (input: bytes32) -> parse32_fldata p32 (U32.v i) i input

inline_for_extraction
let parse32_vldata_gen
  (sz: integer_size)
  (f: (bounded_integer sz -> GTot bool))
  (f' : (x: bounded_integer sz) -> Tot (y: bool {y == f x}))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
: Tot (parser32 (parse_vldata_gen sz f p))
= [@inline_let]
  let _ = parse_vldata_gen_eq_def sz f p in
  parse32_and_then
    (parse32_filter (parse32_bounded_integer sz) f f')
    (parse_vldata_payload sz f p)
    ()
    (parse32_vldata_payload sz f p32)

inline_for_extraction
let parse32_vldata
  (sz: integer_size)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
: Tot (parser32 (parse_vldata sz p))
= parse32_vldata_gen sz (unconstrained_bounded_integer sz) (fun _ -> true) p32

#set-options "--z3rlimit 32"

inline_for_extraction
let parse32_bounded_vldata'
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
: Tot (parser32 (parse_bounded_vldata' min max l p))
= [@inline_let]
  let _ = parse_bounded_vldata_correct min max l p in
  [@inline_let]
  let sz : integer_size = l in
  (fun input -> parse32_vldata_gen sz (in_bounds min max) (fun i -> not (U32.lt i min32 || U32.lt max32 i)) p32 input)

inline_for_extraction
let parse32_bounded_vldata
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
: Tot (parser32 (parse_bounded_vldata min max p))
= parse32_bounded_vldata' min min32 max max32 (log256' max) p32

inline_for_extraction
let parse32_bounded_vldata_strong_aux
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (input: bytes32)
: Tot (option (parse_bounded_vldata_strong_t min max #k #t #p s * U32.t))
= let res =
    parse32_strengthen
      #(parse_bounded_vldata_strong_kind min max l k)
      #t
      #(parse_bounded_vldata' min max l #k #t p)
      (parse32_bounded_vldata' min min32 max max32 l #k #t #p p32)
      (parse_bounded_vldata_strong_pred min max #k #t #p s)
      (parse_bounded_vldata_strong_correct min max l #k #t #p s)
      input
  in
  match res with
  | None -> None
  | Some (x, consumed) ->
    let x1 : t = x in
    Some ((x1 <: parse_bounded_vldata_strong_t min max #k #t #p s), consumed)

let parse32_bounded_vldata_strong_correct
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (input: bytes32)
: Lemma
  ( let res : option (parse_bounded_vldata_strong_t min max s * U32.t) = 
      parse32_bounded_vldata_strong_aux min min32 max max32 l s p32 input
    in
    parser32_correct (parse_bounded_vldata_strong' min max l s) input res)
= let res =
    parse32_strengthen
      #(parse_bounded_vldata_strong_kind min max l k)
      #t
      #(parse_bounded_vldata' min max l #k #t p)
      (parse32_bounded_vldata' min min32 max max32 l #k #t #p p32)
      (parse_bounded_vldata_strong_pred min max #k #t #p s)
      (parse_bounded_vldata_strong_correct min max l #k #t #p s)
      input
  in
  match res with
  | None -> ()
  | Some (x, consumed) ->
    let x1 : t = x in
    let res = Some ((x1 <: parse_bounded_vldata_strong_t min max #k #t #p s), consumed) in
    assert (parser32_correct (parse_bounded_vldata_strong' min max l s) input res)

inline_for_extraction
let parse32_bounded_vldata_strong'
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (l: nat { l >= log256' max /\ l <= 4 } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
: Tot (parser32 #_ #(parse_bounded_vldata_strong_t min max s) (parse_bounded_vldata_strong' min max l s))
= make_parser32
    (parse_bounded_vldata_strong' min max l s)
    (fun input ->
       parse32_bounded_vldata_strong_correct min min32 max max32 l s p32 input;
       parse32_bounded_vldata_strong_aux min min32 max max32 l s p32 input
    )

inline_for_extraction
let parse32_bounded_vldata_strong
  (min: nat)
  (min32: U32.t { U32.v min32 == min } )
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 } )
  (max32: U32.t { U32.v max32 == max } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
val parse32_bounded_vldata_strong
      (min: nat)
      (min32: U32.t{U32.v min32 == min})
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (max32: U32.t{U32.v max32 == max})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
    : Tot
    (parser32 #_ #(parse_bounded_vldata_strong_t min max s) (parse_bounded_vldata_strong min max s))

    min: Prims.nat ->
    min32: FStar.UInt32.t{FStar.UInt32.v min32 == min} ->
    max: Prims.nat{min <= max /\ max > 0 /\ max < 4294967296} ->
    max32: FStar.UInt32.t{FStar.UInt32.v max32 == max} ->
    s: LowParse.Spec.Base.serializer p ->
    p32: LowParse.SLow.Base.parser32 p
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.VLData.parse_bounded_vldata_strong min max s)