val 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)
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
val 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)
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
  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
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 FStar.Pervasives.Native.tuple2 Prims.list LowParse.Bytes.bytes Prims.op_Equality Prims.int Prims.bool LowParse.Spec.Base.parse LowParse.Spec.Base.consumed_length LowParse.Spec.VCList.nlist Prims.op_Subtraction LowParse.Spec.VCList.parse_nlist FStar.List.Tot.Properties.append_assoc FStar.List.Tot.Base.rev Prims.Cons Prims.Nil Prims.unit FStar.List.Tot.Properties.rev_rev' LowParse.SLow.VCList.parse_nlist_tailrec_correct' FStar.Pervasives.Native.Mktuple2 Prims.op_Addition FStar.Seq.Base.seq LowParse.Bytes.byte FStar.Seq.Base.slice FStar.Seq.Base.length LowParse.Spec.VCList.parse_nlist_eq Prims.l_True Prims.squash FStar.Pervasives.Native.option LowParse.SLow.VCList.parse_nlist_tailrec Prims.l_and Prims.eq2 FStar.List.Tot.Base.append 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
val 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)

    n: Prims.nat ->
    p: LowParse.Spec.Base.parser k t ->
    accu: (Prims.list t * Prims.nat) ->
    b: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
    (ensures
      ((match
            LowParse.SLow.VCList.parse_nlist_tailrec n p accu 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)) ->
            let _ = accu in
            (let FStar.Pervasives.Native.Mktuple2 #_ #_ l0 consumed0 = _ in
              consumed' == consumed0 + consumed /\ l' == FStar.List.Tot.Base.rev l @ l0)
            <:
            Type0
          | _ -> Prims.l_False)
        <:
        Type0))