val valid_nlist_cons_recip
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (n > 0 /\ valid (parse_nlist n p) h sl pos))
      (ensures
        (valid p h sl pos /\
          (let pos1 = get_valid_pos p h sl pos in
            valid (parse_nlist (n - 1) p) h sl (get_valid_pos p h sl pos) /\
            valid_content_pos (parse_nlist n p)
              h
              sl
              pos
              (contents p h sl pos :: contents (parse_nlist (n - 1) p) h sl pos1)
              (get_valid_pos (parse_nlist (n - 1) p) h sl pos1))))
let valid_nlist_cons_recip
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    n > 0 /\
    valid (parse_nlist n p) h sl pos
  ))
  (ensures (
    valid p h sl pos /\ (
    let pos1 = get_valid_pos p h sl pos in
    valid (parse_nlist (n - 1) p) h sl (get_valid_pos p h sl pos) /\
    valid_content_pos
      (parse_nlist n p)
      h
      sl
      pos
      (contents p h sl pos :: contents (parse_nlist (n - 1) p) h sl pos1)
      (get_valid_pos (parse_nlist (n - 1) p) h sl pos1)
  )))
= valid_facts (parse_nlist n p) h sl pos;
  parse_nlist_eq n p (bytes_of_slice_from h sl pos);
  valid_facts p h sl pos;
  let pos1 = get_valid_pos p h sl pos in
  valid_facts (parse_nlist (n - 1) p) h sl pos1
val valid_nlist_cons_recip
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (n > 0 /\ valid (parse_nlist n p) h sl pos))
      (ensures
        (valid p h sl pos /\
          (let pos1 = get_valid_pos p h sl pos in
            valid (parse_nlist (n - 1) p) h sl (get_valid_pos p h sl pos) /\
            valid_content_pos (parse_nlist n p)
              h
              sl
              pos
              (contents p h sl pos :: contents (parse_nlist (n - 1) p) h sl pos1)
              (get_valid_pos (parse_nlist (n - 1) p) h sl pos1))))
let valid_nlist_cons_recip
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (n > 0 /\ valid (parse_nlist n p) h sl pos))
      (ensures
        (valid p h sl pos /\
          (let pos1 = get_valid_pos p h sl pos in
            valid (parse_nlist (n - 1) p) h sl (get_valid_pos p h sl pos) /\
            valid_content_pos (parse_nlist n p)
              h
              sl
              pos
              (contents p h sl pos :: contents (parse_nlist (n - 1) p) h sl pos1)
              (get_valid_pos (parse_nlist (n - 1) p) h sl pos1)))) =
valid_facts (parse_nlist n p) h sl pos;
parse_nlist_eq n p (bytes_of_slice_from h sl pos);
valid_facts p h sl pos;
let pos1 = get_valid_pos p h sl pos in
valid_facts (parse_nlist (n - 1) p) h sl pos1
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
Prims.nat 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.Low.Base.Spec.valid_facts LowParse.Spec.VCList.parse_nlist_kind Prims.op_Subtraction LowParse.Spec.VCList.nlist LowParse.Spec.VCList.parse_nlist LowParse.Low.Base.Spec.get_valid_pos Prims.unit LowParse.Spec.VCList.parse_nlist_eq LowParse.Slice.bytes_of_slice_from Prims.l_and Prims.b2t Prims.op_GreaterThan LowParse.Low.Base.Spec.valid Prims.squash LowParse.Low.Base.Spec.valid_content_pos Prims.Cons LowParse.Low.Base.Spec.contents 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))
  (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)

#push-options "--z3rlimit 16"

let valid_nlist_cons
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    valid p h sl pos /\
    valid (parse_nlist n p) h sl (get_valid_pos p h sl pos)
  ))
  (ensures (
    valid p h sl pos /\
    valid (parse_nlist n p) h sl (get_valid_pos p h sl pos) /\ (
    let pos1 = get_valid_pos p h sl pos in
    valid_content_pos
      (parse_nlist (n + 1) p)
      h
      sl
      pos
      (contents p h sl pos :: contents (parse_nlist n p) h sl pos1)
      (get_valid_pos (parse_nlist n p) h sl pos1)
  )))
= let pos1 = get_valid_pos p h sl pos in
  valid_facts p h sl pos;
  valid_facts (parse_nlist n p) h sl pos1;
  valid_facts (parse_nlist (n + 1) p) h sl pos;
  parse_nlist_eq (n + 1) p (bytes_of_slice_from h sl pos)

let valid_nlist_cons_recip
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    n > 0 /\
    valid (parse_nlist n p) h sl pos
  ))
  (ensures (
    valid p h sl pos /\ (
    let pos1 = get_valid_pos p h sl pos in
    valid (parse_nlist (n - 1) p) h sl (get_valid_pos p h sl pos) /\
    valid_content_pos
      (parse_nlist n p)
      h
      sl
      pos
      (contents p h sl pos :: contents (parse_nlist (n - 1) p) h sl pos1)
      (get_valid_pos (parse_nlist (n - 1) p) h sl pos1)
val valid_nlist_cons_recip
      (n: nat)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (#rrel #rel: _)
      (sl: slice rrel rel)
      (pos: U32.t)
    : Lemma (requires (n > 0 /\ valid (parse_nlist n p) h sl pos))
      (ensures
        (valid p h sl pos /\
          (let pos1 = get_valid_pos p h sl pos in
            valid (parse_nlist (n - 1) p) h sl (get_valid_pos p h sl pos) /\
            valid_content_pos (parse_nlist n p)
              h
              sl
              pos
              (contents p h sl pos :: contents (parse_nlist (n - 1) p) h sl pos1)
              (get_valid_pos (parse_nlist (n - 1) p) h sl pos1))))

    n: Prims.nat ->
    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
        n > 0 /\ LowParse.Low.Base.Spec.valid (LowParse.Spec.VCList.parse_nlist n p) h sl pos)
      (ensures
        LowParse.Low.Base.Spec.valid p h sl pos /\
        (let pos1 = LowParse.Low.Base.Spec.get_valid_pos p h sl pos in
          LowParse.Low.Base.Spec.valid (LowParse.Spec.VCList.parse_nlist (n - 1) p)
            h
            sl
            (LowParse.Low.Base.Spec.get_valid_pos p h sl pos) /\
          LowParse.Low.Base.Spec.valid_content_pos (LowParse.Spec.VCList.parse_nlist n p)
            h
            sl
            pos
            (LowParse.Low.Base.Spec.contents p h sl pos ::
              LowParse.Low.Base.Spec.contents (LowParse.Spec.VCList.parse_nlist (n - 1) p) h sl pos1
            )
            (LowParse.Low.Base.Spec.get_valid_pos (LowParse.Spec.VCList.parse_nlist (n - 1) p)
                h
                sl
                pos1)))