val parse_nlist_tailrec_inv
      (n: U32.t)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: (list t * nat))
      (input: bytes32)
      (b: bool)
      (x: option (bytes32 * U32.t * list t * U32.t))
    : GTot Type0
let parse_nlist_tailrec_inv
  (n: U32.t)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (accu: list t * nat)
  (input: bytes32)
  (b: bool)
  (x: option (bytes32 * U32.t * list t * U32.t))
: GTot Type0
= match x with
  | Some (input', i, accu', consumed') ->
    U32.v i <= U32.v n /\
    U32.v consumed' + B32.length input' < 4294967296 /\
    parse_nlist_tailrec (U32.v n) p accu (B32.reveal input) == parse_nlist_tailrec (U32.v n - U32.v i) p (accu', U32.v consumed') (B32.reveal input') /\
    (b == false ==> i == n)
  | None ->
    b == false /\ None? (parse_nlist_tailrec (U32.v n) p accu (B32.reveal input))
val parse_nlist_tailrec_inv
      (n: U32.t)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: (list t * nat))
      (input: bytes32)
      (b: bool)
      (x: option (bytes32 * U32.t * list t * U32.t))
    : GTot Type0
let parse_nlist_tailrec_inv
      (n: U32.t)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: list t * nat)
      (input: bytes32)
      (b: bool)
      (x: option (bytes32 * U32.t * list t * U32.t))
    : GTot Type0 =
match x with
| Some (input', i, accu', consumed') ->
  U32.v i <= U32.v n /\ U32.v consumed' + B32.length input' < 4294967296 /\
  parse_nlist_tailrec (U32.v n) p accu (B32.reveal input) ==
  parse_nlist_tailrec (U32.v n - U32.v i) p (accu', U32.v consumed') (B32.reveal input') /\
  (b == false ==> i == n)
| None -> b == false /\ None? (parse_nlist_tailrec (U32.v n) p accu (B32.reveal input))
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
FStar.UInt32.t LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser FStar.Pervasives.Native.tuple2 Prims.list Prims.nat LowParse.SLow.Base.bytes32 Prims.bool FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple4 Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v Prims.op_LessThan Prims.op_Addition FStar.Bytes.length Prims.eq2 LowParse.SLow.VCList.parse_nlist_tailrec FStar.Bytes.reveal Prims.op_Subtraction FStar.Pervasives.Native.Mktuple2 Prims.l_imp FStar.Pervasives.Native.uu___is_None
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'
    | _ -> 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

let parse_nlist_tailrec_inv
  (n: U32.t)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (accu: list t * nat)
  (input: bytes32)
  (b: bool)
  (x: option (bytes32 * U32.t * list t * U32.t))
val parse_nlist_tailrec_inv
      (n: U32.t)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (accu: (list t * nat))
      (input: bytes32)
      (b: bool)
      (x: option (bytes32 * U32.t * list t * U32.t))
    : GTot Type0

    n: FStar.UInt32.t ->
    p: LowParse.Spec.Base.parser k t ->
    accu: (Prims.list t * Prims.nat) ->
    input: LowParse.SLow.Base.bytes32 ->
    b: Prims.bool ->
    x:
      FStar.Pervasives.Native.option (((LowParse.SLow.Base.bytes32 * FStar.UInt32.t) * Prims.list t) *
          FStar.UInt32.t)
  -> Prims.GTot Type0