val validate_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (v: validator p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (validator (parse_fldata p sz))
let validate_fldata
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (v: validator p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
: Tot (validator (parse_fldata p sz))
= if k.parser_kind_subkind = Some ParserConsumesAll
  then validate_fldata_consumes_all v sz sz32 ()
  else validate_fldata_gen v sz sz32
val validate_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (v: validator p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (validator (parse_fldata p sz))
let validate_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (v: validator p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (validator (parse_fldata p sz)) =
if k.parser_kind_subkind = Some ParserConsumesAll
then validate_fldata_consumes_all v sz sz32 ()
else validate_fldata_gen v sz sz32
LowParse.Low.FLData.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.FLData.fst.checked LowParse.Low.Combinators.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
LowParse.Low.FLData.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Low.Base.validator 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.op_Equality FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserConsumesAll LowParse.Low.FLData.validate_fldata_consumes_all Prims.bool LowParse.Low.FLData.validate_fldata_gen LowParse.Spec.FLData.parse_fldata_kind LowParse.Spec.FLData.parse_fldata
module LowParse.Low.FLData
include LowParse.Low.Combinators
include LowParse.Spec.FLData

module B = LowStar.Buffer
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module Cast = FStar.Int.Cast
module U64 = FStar.UInt64

let valid_fldata_gen
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (
    U32.v pos + sz < 4294967296 /\
    valid_exact p h input pos (pos `U32.add` U32.uint_to_t sz)
  ))
  (ensures (
    U32.v pos + sz < 4294967296 /\ (
    let pos' = pos `U32.add` U32.uint_to_t sz in
    valid_content_pos (parse_fldata p sz) h input pos (contents_exact p h input pos pos') pos'
  )))
= valid_facts (parse_fldata p sz) h input pos;
  let pos' = pos `U32.add` U32.uint_to_t sz in
  let input' = { base = input.base; len = pos'; } in
  valid_facts p h input' pos;
  valid_exact_equiv p h input pos pos';
  contents_exact_eq p h input pos pos'

let valid_fldata_gen_elim
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (
    valid (parse_fldata p sz) h input pos
  ))
  (ensures (
    U32.v pos + sz < 4294967296 /\ (
    let pos' = pos `U32.add` U32.uint_to_t sz in
    valid_exact p h input pos (pos `U32.add` U32.uint_to_t sz) /\
    valid_content_pos (parse_fldata p sz) h input pos (contents_exact p h input pos pos') pos'
  )))
= valid_facts (parse_fldata p sz) h input pos;
  let pos' = pos `U32.add` U32.uint_to_t sz in
  let input' = { base = input.base; len = pos'; } in
  valid_facts p h input' pos;
  valid_exact_equiv p h input pos pos';
  contents_exact_eq p h input pos pos'

inline_for_extraction
let validate_fldata_gen
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (v: validator p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
: Tot (validator (parse_fldata p sz))
= fun #rrel #rel input pos ->
  let h = HST.get () in
  [@inline_let] let _ = valid_facts (parse_fldata p sz) h input (uint64_to_uint32 pos) in
  if (Cast.uint32_to_uint64 input.len `U64.sub` pos) `U64.lt` Cast.uint32_to_uint64 sz32
  then validator_error_not_enough_data
  else
    [@inline_let] let input' = { base = input.base; len = uint64_to_uint32 pos `U32.add` sz32; } in
    [@inline_let] let _ = valid_facts p h input' (uint64_to_uint32 pos) in
    let pos' = v input' pos in
    if is_error pos'
    then
      if pos' = validator_error_not_enough_data
      then validator_error_generic (* the size was fixed ahead of time, so if the parser runs out of data, then that size was wrong in the first place. *) 
      else pos' // error propagation
    else
    if pos' `U64.sub` pos <> Cast.uint32_to_uint64 sz32
    then validator_error_generic
    else pos'

inline_for_extraction
let validate_fldata_consumes_all
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (v: validator p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
  (sq: squash (k.parser_kind_subkind == Some ParserConsumesAll))
: Tot (validator (parse_fldata p sz))
= fun #rrel #rel input pos ->
  let h = HST.get () in
  [@inline_let] let _ =
    valid_facts (parse_fldata p sz) h input (uint64_to_uint32 pos);
    parse_fldata_consumes_all_correct p sz (bytes_of_slice_from h input (uint64_to_uint32 pos))
  in
  if (Cast.uint32_to_uint64 input.len `U64.sub` pos) `U64.lt` Cast.uint32_to_uint64 sz32
  then validator_error_not_enough_data
  else
    [@inline_let] let input' = { base = input.base; len = uint64_to_uint32 pos `U32.add` sz32; } in
    [@inline_let] let _ = valid_facts p h input' (uint64_to_uint32 pos) in
    let pos' = v input' pos in
    if is_error pos'
    then
      if pos' = validator_error_not_enough_data
      then validator_error_generic (* the size was fixed ahead of time, so if the parser runs out of data, then that size was wrong in the first place. *) 
      else pos' // error propagation
    else pos'

inline_for_extraction
let validate_fldata
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (v: validator p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
val validate_fldata
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (v: validator p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (validator (parse_fldata p sz))
v: LowParse.Low.Base.validator p -> sz: Prims.nat -> sz32: FStar.UInt32.t{FStar.UInt32.v sz32 == sz}
  -> LowParse.Low.Base.validator (LowParse.Spec.FLData.parse_fldata p sz)