val valid_nlist_nil_recip
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (valid (parse_nlist 0 p) h sl pos))
      (ensures (valid_content_pos (parse_nlist 0 p) h sl pos [] pos))
let valid_nlist_nil_recip
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (valid (parse_nlist 0 p) h sl pos))
  (ensures (valid_content_pos (parse_nlist 0 p) h sl pos [] pos))
= valid_facts (parse_nlist 0 p) h sl pos;
  parse_nlist_eq 0 p (bytes_of_slice_from h sl pos)
val valid_nlist_nil_recip
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (valid (parse_nlist 0 p) h sl pos))
      (ensures (valid_content_pos (parse_nlist 0 p) h sl pos [] pos))
let valid_nlist_nil_recip
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (valid (parse_nlist 0 p) h sl pos))
      (ensures (valid_content_pos (parse_nlist 0 p) h sl pos [] pos)) =
valid_facts (parse_nlist 0 p) h sl pos;
parse_nlist_eq 0 p (bytes_of_slice_from h sl pos)
LowParse.Low.VCList.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.VCList.fsti.checked LowParse.Low.List.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked C.Loops.fst.checked
LowParse.Low.VCList.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser FStar.Monotonic.HyperStack.mem LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t LowParse.Spec.VCList.parse_nlist_eq LowParse.Slice.bytes_of_slice_from Prims.unit LowParse.Low.Base.Spec.valid_facts LowParse.Spec.VCList.parse_nlist_kind LowParse.Spec.VCList.nlist LowParse.Spec.VCList.parse_nlist LowParse.Low.Base.Spec.valid Prims.squash LowParse.Low.Base.Spec.valid_content_pos Prims.Nil FStar.Pervasives.pattern
module LowParse.Low.VCList
include LowParse.Spec.VCList
include LowParse.Low.List

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

let valid_nlist_nil
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (live_slice h sl /\ U32.v pos <= U32.v sl.len))
  (ensures (valid_content_pos (parse_nlist 0 p) h sl pos [] pos))
= valid_facts (parse_nlist 0 p) h sl pos;
  parse_nlist_eq 0 p (bytes_of_slice_from h sl pos)

let valid_nlist_nil_recip
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (valid (parse_nlist 0 p) h sl pos))
val valid_nlist_nil_recip
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (valid (parse_nlist 0 p) h sl pos))
      (ensures (valid_content_pos (parse_nlist 0 p) h sl pos [] pos))

    p: LowParse.Spec.Base.parser k t ->
    h: FStar.Monotonic.HyperStack.mem ->
    sl: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
      (requires LowParse.Low.Base.Spec.valid (LowParse.Spec.VCList.parse_nlist 0 p) h sl pos)
      (ensures
        LowParse.Low.Base.Spec.valid_content_pos (LowParse.Spec.VCList.parse_nlist 0 p)
          h
          sl
          pos
          []
          pos)