val 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')))
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'
val 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')))
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'
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 Prims.nat LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t FStar.Monotonic.HyperStack.mem LowParse.Low.Base.Spec.contents_exact_eq Prims.unit LowParse.Low.Base.Spec.valid_exact_equiv LowParse.Low.Base.Spec.valid_facts LowParse.Slice.Mkslice LowParse.Slice.__proj__Mkslice__item__base FStar.UInt32.add FStar.UInt32.uint_to_t LowParse.Spec.FLData.parse_fldata_kind LowParse.Spec.FLData.parse_fldata LowParse.Low.Base.Spec.valid Prims.squash Prims.l_and Prims.b2t Prims.op_LessThan Prims.op_Addition FStar.UInt32.v LowParse.Low.Base.Spec.valid_exact LowParse.Low.Base.Spec.valid_content_pos LowParse.Low.Base.Spec.contents_exact Prims.Nil FStar.Pervasives.pattern
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'
val 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')))

    p: LowParse.Spec.Base.parser k t ->
    sz: Prims.nat ->
    input: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires LowParse.Low.Base.Spec.valid (LowParse.Spec.FLData.parse_fldata p sz) h input pos)
      (ensures
        FStar.UInt32.v pos + sz < 4294967296 /\
        (let pos' = FStar.UInt32.add pos (FStar.UInt32.uint_to_t sz) in
          LowParse.Low.Base.Spec.valid_exact p
            h
            input
            pos
            (FStar.UInt32.add pos (FStar.UInt32.uint_to_t sz)) /\
          LowParse.Low.Base.Spec.valid_content_pos (LowParse.Spec.FLData.parse_fldata p sz)
            h
            input
            pos
            (LowParse.Low.Base.Spec.contents_exact p h input pos pos')
            pos'))