val parse_list
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser parse_list_kind (list t))
let parse_list #k #t p =
  parse_list_bare_injective p;
  parse_list_bare_consumes_all p;
  parser_kind_prop_equiv parse_list_kind (parse_list_bare p);
  parse_list_bare p
val parse_list
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser parse_list_kind (list t))
let parse_list #k #t p =
parse_list_bare_injective p;
parse_list_bare_consumes_all p;
parser_kind_prop_equiv parse_list_kind (parse_list_bare p);
parse_list_bare p
LowParse.Spec.List.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.List.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.List.parse_list_bare Prims.unit LowParse.Spec.Base.parser_kind_prop_equiv Prims.list LowParse.Spec.List.parse_list_kind LowParse.Spec.List.parse_list_bare_consumes_all LowParse.Spec.List.parse_list_bare_injective
module LowParse.Spec.List
include LowParse.Spec.Combinators // for seq_slice_append_l

module Seq = FStar.Seq
module L = FStar.List.Tot
module U32 = FStar.UInt32
module Classical = FStar.Classical

(* Parse a list, until there is nothing left to read. This parser will mostly fail EXCEPT if the whole size is known and the slice has been suitably truncated beforehand, or if the elements of the list all have a known constant size. *)

#push-options "--z3rlimit 16"

let parse_list_bare_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Lemma
  (ensures (injective (parse_list_bare p)))
= parser_kind_prop_equiv k p;
  let f () : Lemma
    (injective p)
  = ()
  in
  let rec aux
    (b1: bytes)
    (b2: bytes)
  : Lemma
    (requires (injective_precond (parse_list_bare p) b1 b2))
    (ensures (injective_postcond (parse_list_bare p) b1 b2))
    (decreases (Seq.length b1 + Seq.length b2))
  = if Seq.length b1 = 0
    then begin
      () // assert (Seq.equal b1 b2)
    end else begin
      assert (injective_precond p b1 b2);
      f ();
      assert (injective_postcond p b1 b2);
      let (Some (_, len1)) = parse p b1 in
      let (Some (_, len2)) = parse p b2 in
      assert ((len1 <: nat) == (len2 <: nat));
      let b1' : bytes = Seq.slice b1 len1 (Seq.length b1) in
      let b2' : bytes = Seq.slice b2 len2 (Seq.length b2) in
      aux b1' b2';
      let (Some (_, len1')) = parse (parse_list_bare p) b1' in
      let (Some (_, len2')) = parse (parse_list_bare p) b2' in
      Seq.lemma_split (Seq.slice b1 0 (len1 + len1')) len1;
      Seq.lemma_split (Seq.slice b2 0 (len2 + len2')) len2;
      assert (injective_postcond (parse_list_bare p) b1 b2)
    end
  in
  Classical.forall_intro_2 (fun b -> Classical.move_requires (aux b))

#pop-options
val parse_list
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot (parser parse_list_kind (list t))
p: LowParse.Spec.Base.parser k t
  -> LowParse.Spec.Base.parser LowParse.Spec.List.parse_list_kind (Prims.list t)