val parse_nlist_tailrec_correct (n: nat) (#k: parser_kind) (#t: Type) (p: parser k t) (b: bytes)
    : Lemma
    (match parse_nlist_tailrec n p ([], 0) b, parse (parse_nlist n p) b with
      | None, None -> True
      | Some (l', consumed'), Some (l, consumed) -> consumed' == consumed /\ l == L.rev l'
      | _ -> False)
let parse_nlist_tailrec_correct
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (b: bytes)
: Lemma
  (match parse_nlist_tailrec n p ([], 0) b, parse (parse_nlist n p) b with
    | None, None -> True
    | Some (l', consumed'), Some (l, consumed) ->
      consumed' == consumed /\ l == L.rev l'
    | _ -> False)
= parse_nlist_tailrec_correct' n p ([], 0) b;
  match parse (parse_nlist n p) b with
  | None -> ()
  | Some (l, _) ->
    L.append_l_nil (L.rev l);
    L.rev_involutive l
val parse_nlist_tailrec_correct (n: nat) (#k: parser_kind) (#t: Type) (p: parser k t) (b: bytes)
    : Lemma
    (match parse_nlist_tailrec n p ([], 0) b, parse (parse_nlist n p) b with
      | None, None -> True
      | Some (l', consumed'), Some (l, consumed) -> consumed' == consumed /\ l == L.rev l'
      | _ -> False)
let parse_nlist_tailrec_correct (n: nat) (#k: parser_kind) (#t: Type) (p: parser k t) (b: bytes)
    : Lemma
    (match parse_nlist_tailrec n p ([], 0) b, parse (parse_nlist n p) b with
      | None, None -> True
      | Some (l', consumed'), Some (l, consumed) -> consumed' == consumed /\ l == L.rev l'
      | _ -> False) =
parse_nlist_tailrec_correct' n p ([], 0) b;
match parse (parse_nlist n p) b with
| None -> ()
| Some (l, _) ->
  L.append_l_nil (L.rev l);
  L.rev_involutive l
LowParse.SLow.VCList.fst.checked
prims.fst.checked LowParse.Spec.VCList.fsti.checked LowParse.SLow.List.fst.checked LowParse.Math.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked C.Loops.fst.checked
LowParse.SLow.VCList.fst
Prims.nat LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Bytes.bytes LowParse.Spec.Base.parse LowParse.Spec.VCList.nlist LowParse.Spec.VCList.parse_nlist LowParse.Spec.Base.consumed_length FStar.List.Tot.Properties.rev_involutive Prims.unit FStar.List.Tot.Properties.append_l_nil FStar.List.Tot.Base.rev LowParse.SLow.VCList.parse_nlist_tailrec_correct' FStar.Pervasives.Native.Mktuple2 Prims.list Prims.Nil Prims.l_True Prims.squash FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.SLow.VCList.parse_nlist_tailrec Prims.l_and Prims.eq2 Prims.l_False FStar.Pervasives.pattern
module LowParse.SLow.VCList
include LowParse.Spec.VCList
include LowParse.SLow.List

module Seq = FStar.Seq
module U32 = FStar.UInt32
module Classical = FStar.Classical
module L = FStar.List.Tot
module B32 = LowParse.Bytes32

let rec parse_nlist_tailrec
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (accu: list t * nat)
  (b: bytes)
: GTot (option (list t * nat))
= if n = 0
  then Some accu
  else
    match parse p b with
    | Some (elem, consumed) ->
      let (l0, consumed0) = accu in
      let b' = Seq.slice b consumed (Seq.length b) in
      parse_nlist_tailrec (n - 1) p (elem :: l0, consumed0 + consumed) b'
    | _ -> None

let rec parse_nlist_tailrec_correct'
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (accu: list t * nat)
  (b: bytes)
: Lemma
  (match parse_nlist_tailrec n p accu b, parse (parse_nlist n p) b with
    | None, None -> True
    | Some (l', consumed'), Some (l, consumed) ->
      let (l0, consumed0) = accu in
      consumed' == consumed0 + consumed /\ l' == L.rev l `L.append` l0
    | _ -> False)
= parse_nlist_eq n p b;
  if n = 0
  then ()
  else begin
    match parse p b with
    | None -> ()
    | Some (elem1, consumed1) ->
      let (l0, consumed0) = accu in
      let b' = Seq.slice b consumed1 (Seq.length b) in
      parse_nlist_tailrec_correct' (n - 1) p (elem1 :: l0, consumed0 + consumed1) b' ;
      match parse (parse_nlist (n - 1) p) b' with
      | None -> ()
      | Some (l2, consumed2) ->
        L.rev_rev' (elem1 :: l2);
        L.rev_rev' l2;
        L.append_assoc (L.rev l2) [elem1] l0
  end

let parse_nlist_tailrec_correct
  (n: nat)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (b: bytes)
: Lemma
  (match parse_nlist_tailrec n p ([], 0) b, parse (parse_nlist n p) b with
    | None, None -> True
    | Some (l', consumed'), Some (l, consumed) ->
      consumed' == consumed /\ l == L.rev l'
val parse_nlist_tailrec_correct (n: nat) (#k: parser_kind) (#t: Type) (p: parser k t) (b: bytes)
    : Lemma
    (match parse_nlist_tailrec n p ([], 0) b, parse (parse_nlist n p) b with
      | None, None -> True
      | Some (l', consumed'), Some (l, consumed) -> consumed' == consumed /\ l == L.rev l'
      | _ -> False)
n: Prims.nat -> p: LowParse.Spec.Base.parser k t -> b: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
    (ensures
      ((match
            LowParse.SLow.VCList.parse_nlist_tailrec n p ([], 0) b,
            LowParse.Spec.Base.parse (LowParse.Spec.VCList.parse_nlist n p) b
          with
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (FStar.Pervasives.Native.None #_)
            (FStar.Pervasives.Native.None #_) ->
            Prims.l_True
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ l' consumed'))
            (FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ l consumed)) ->
            consumed' == consumed /\ l == FStar.List.Tot.Base.rev l'
          | _ -> Prims.l_False)
        <:
        Type0))