val validate_nlist (n: U32.t) (#k: parser_kind) (#t: Type) (#p: parser k t) (v: validator p)
    : Tot (validator (parse_nlist (U32.v n) p))
let validate_nlist
  (n: U32.t)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (v: validator p)
: Tot (validator (parse_nlist (U32.v n) p))
= fun #rrel #rel input pos ->
  let h0 = HST.get () in
  HST.push_frame ();
  let bpos1 : B.buffer U64.t = B.alloca pos 1ul in
  let br = B.alloca n 1ul in
  let h1 = HST.get () in
  C.Loops.do_while
    (fun h stop ->
      B.modifies (B.loc_buffer bpos1 `B.loc_union` B.loc_buffer br) h1 h /\ (
      let pos1 = B.get h bpos1 0 in
      let r = B.get h br 0 in
      U32.v r <= U32.v n /\
      U64.v pos <= U64.v pos1 /\ (
      if is_success pos1
      then
        let pos1 = uint64_to_uint32 pos1 in
        U32.v pos1 <= U32.v input.len /\
        (valid (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos) <==> valid (parse_nlist (U32.v r) p) h0 input pos1) /\
        ((valid (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos) /\ valid (parse_nlist (U32.v r) p) h0 input pos1) ==> get_valid_pos (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos) == get_valid_pos (parse_nlist (U32.v r) p) h0 input pos1) /\
        (stop == true ==> r == 0ul)
      else
        (stop == true /\ (~ (valid (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos))))
    )))
    (fun _ ->
      let r = B.index br 0ul in
      if r = 0ul
      then true
      else
        let pos1 = B.index bpos1 0ul in
        let pos2 = v input pos1 in
        let _ = B.upd br 0ul (r `U32.sub` 1ul) in
        let _ = B.upd bpos1 0ul pos2 in
        [@inline_let]
        let stop = is_error pos2 in
        [@inline_let]
        let _ =
          if stop
          then valid_nlist_cons_not (U32.v r) p h0 input (uint64_to_uint32 pos1)
          else valid_nlist_cons' (U32.v r) p h0 input (uint64_to_uint32 pos1)
        in
        stop
    )
  ;
  let res = B.index bpos1 0ul in
  [@inline_let] let _ =
    if is_success res
    then valid_nlist_nil p h0 input (uint64_to_uint32 res)
  in
  HST.pop_frame ();
  res
val validate_nlist (n: U32.t) (#k: parser_kind) (#t: Type) (#p: parser k t) (v: validator p)
    : Tot (validator (parse_nlist (U32.v n) p))
let validate_nlist (n: U32.t) (#k: parser_kind) (#t: Type) (#p: parser k t) (v: validator p)
    : Tot (validator (parse_nlist (U32.v n) p)) =
fun #rrel #rel input pos ->
  let h0 = HST.get () in
  HST.push_frame ();
  let bpos1:B.buffer U64.t = B.alloca pos 1ul in
  let br = B.alloca n 1ul in
  let h1 = HST.get () in
  C.Loops.do_while (fun h stop ->
        B.modifies ((B.loc_buffer bpos1) `B.loc_union` (B.loc_buffer br)) h1 h /\
        (let pos1 = B.get h bpos1 0 in
          let r = B.get h br 0 in
          U32.v r <= U32.v n /\ U64.v pos <= U64.v pos1 /\
          (if is_success pos1
            then
              let pos1 = uint64_to_uint32 pos1 in
              U32.v pos1 <= U32.v input.len /\
              (valid (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos) <==>
                valid (parse_nlist (U32.v r) p) h0 input pos1) /\
              ((valid (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos) /\
                  valid (parse_nlist (U32.v r) p) h0 input pos1) ==>
                get_valid_pos (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos) ==
                get_valid_pos (parse_nlist (U32.v r) p) h0 input pos1) /\
              (stop == true ==> r == 0ul)
            else
              (stop == true /\ (~(valid (parse_nlist (U32.v n) p) h0 input (uint64_to_uint32 pos))))
          )))
    (fun _ ->
        let r = B.index br 0ul in
        if r = 0ul
        then true
        else
          let pos1 = B.index bpos1 0ul in
          let pos2 = v input pos1 in
          let _ = B.upd br 0ul (r `U32.sub` 1ul) in
          let _ = B.upd bpos1 0ul pos2 in
          [@@ inline_let ]let stop = is_error pos2 in
          [@@ inline_let ]let _ =
            if stop
            then valid_nlist_cons_not (U32.v r) p h0 input (uint64_to_uint32 pos1)
            else valid_nlist_cons' (U32.v r) p h0 input (uint64_to_uint32 pos1)
          in
          stop);
  let res = B.index bpos1 0ul in
  [@@ inline_let ]let _ =
    if is_success res then valid_nlist_nil p h0 input (uint64_to_uint32 res)
  in
  HST.pop_frame ();
  res
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
FStar.UInt32.t LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Low.Base.validator LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t Prims.unit FStar.HyperStack.ST.pop_frame LowParse.Low.ErrorCode.is_success LowParse.Low.VCList.valid_nlist_nil LowParse.Low.ErrorCode.uint64_to_uint32 Prims.bool LowStar.Monotonic.Buffer.index LowStar.Buffer.trivial_preorder FStar.UInt32.__uint_to_t C.Loops.do_while FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_buffer Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v FStar.UInt64.v LowParse.Slice.__proj__Mkslice__item__len Prims.l_iff LowParse.Low.Base.Spec.valid LowParse.Spec.VCList.parse_nlist_kind LowParse.Spec.VCList.nlist LowParse.Spec.VCList.parse_nlist Prims.l_imp Prims.eq2 LowParse.Low.Base.Spec.get_valid_pos Prims.int Prims.l_or FStar.UInt.size Prims.l_not Prims.logical LowStar.Monotonic.Buffer.get Prims.op_Equality LowParse.Low.VCList.valid_nlist_cons_not LowParse.Low.VCList.valid_nlist_cons' LowParse.Low.ErrorCode.is_error LowStar.Monotonic.Buffer.upd FStar.UInt32.sub FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.mbuffer Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.uint_to_t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.alloca LowStar.Buffer.buffer FStar.HyperStack.ST.push_frame
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)
  ))
= Classical.move_requires (valid_nlist_cons (n - 1) p h sl) pos;
  Classical.move_requires (valid_nlist_cons_recip n p h sl) pos

let valid_nlist_cons_not
  (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 (
    ~ (valid (parse_nlist n p) h sl pos)
  ))
= Classical.move_requires (valid_nlist_cons (n - 1) p h sl) pos;
  Classical.move_requires (valid_nlist_cons_recip n p h sl) pos

#push-options "--z3rlimit 32"

inline_for_extraction
let validate_nlist
  (n: U32.t)
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (v: validator p)
val validate_nlist (n: U32.t) (#k: parser_kind) (#t: Type) (#p: parser k t) (v: validator p)
    : Tot (validator (parse_nlist (U32.v n) p))
n: FStar.UInt32.t -> v: LowParse.Low.Base.validator p
  -> LowParse.Low.Base.validator (LowParse.Spec.VCList.parse_nlist (FStar.UInt32.v n) p)