val 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 (n > 0 /\ valid p h sl pos))
      (ensures
        (let pos1 = get_valid_pos p h sl pos in
          (valid (parse_nlist n p) h sl pos <==> valid (parse_nlist (n - 1) p) h sl pos1) /\
          ((valid (parse_nlist n p) h sl pos /\ valid (parse_nlist (n - 1) p) h sl pos1) ==>
            get_valid_pos (parse_nlist n p) h sl pos ==
            get_valid_pos (parse_nlist (n - 1) p) h sl pos1)))
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 (
    n > 0 /\
    valid p h sl pos
  ))
  (ensures (
    let pos1 = get_valid_pos p h sl pos in
    (valid (parse_nlist n p) h sl pos <==> valid (parse_nlist (n - 1) p) h sl pos1) /\
    ((valid (parse_nlist n p) h sl pos /\ valid (parse_nlist (n - 1) p) h sl pos1) ==> get_valid_pos (parse_nlist n p) h sl pos == get_valid_pos (parse_nlist (n - 1) p) h sl pos1)
  ))
= Classical.move_requires (valid_nlist_cons (n - 1) p h sl) pos;
  Classical.move_requires (valid_nlist_cons_recip n p h sl) pos
val 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 (n > 0 /\ valid p h sl pos))
      (ensures
        (let pos1 = get_valid_pos p h sl pos in
          (valid (parse_nlist n p) h sl pos <==> valid (parse_nlist (n - 1) p) h sl pos1) /\
          ((valid (parse_nlist n p) h sl pos /\ valid (parse_nlist (n - 1) p) h sl pos1) ==>
            get_valid_pos (parse_nlist n p) h sl pos ==
            get_valid_pos (parse_nlist (n - 1) p) h sl pos1)))
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 (n > 0 /\ valid p h sl pos))
      (ensures
        (let pos1 = get_valid_pos p h sl pos in
          (valid (parse_nlist n p) h sl pos <==> valid (parse_nlist (n - 1) p) h sl pos1) /\
          ((valid (parse_nlist n p) h sl pos /\ valid (parse_nlist (n - 1) p) h sl pos1) ==>
            get_valid_pos (parse_nlist n p) h sl pos ==
            get_valid_pos (parse_nlist (n - 1) p) h sl pos1))) =
Classical.move_requires (valid_nlist_cons (n - 1) p h sl) pos;
Classical.move_requires (valid_nlist_cons_recip n p 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
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 FStar.Classical.move_requires Prims.l_and Prims.b2t Prims.op_GreaterThan LowParse.Low.Base.Spec.valid LowParse.Spec.VCList.parse_nlist_kind LowParse.Spec.VCList.nlist LowParse.Spec.VCList.parse_nlist Prims.op_Subtraction LowParse.Low.Base.Spec.get_valid_pos LowParse.Low.Base.Spec.valid_content_pos Prims.Cons LowParse.Low.Base.Spec.contents LowParse.Low.VCList.valid_nlist_cons_recip Prims.unit Prims.op_Addition LowParse.Low.VCList.valid_nlist_cons Prims.squash Prims.l_iff Prims.l_imp Prims.eq2 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)
  )))
= 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

#pop-options

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