val parse_list_bare_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Lemma
  (ensures (injective (parse_list_bare p)))
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))
val parse_list_bare_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Lemma
  (ensures (injective (parse_list_bare p)))
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 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 ()
  else
    (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))
in
Classical.forall_intro_2 (fun b -> Classical.move_requires (aux b))
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 FStar.Classical.forall_intro_2 LowParse.Bytes.bytes Prims.l_imp LowParse.Spec.Base.injective_precond Prims.list LowParse.Spec.List.parse_list_bare LowParse.Spec.Base.injective_postcond FStar.Classical.move_requires Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims.op_Addition FStar.Seq.Base.length LowParse.Bytes.byte Prims.op_Equality Prims.int Prims.bool LowParse.Spec.Base.consumed_length Prims._assert FStar.Seq.Properties.lemma_split FStar.Seq.Base.slice FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.parse Prims.eq2 Prims.nat LowParse.Spec.Base.injective LowParse.Spec.Base.parser_kind_prop_equiv
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
val parse_list_bare_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Lemma
  (ensures (injective (parse_list_bare p)))
p: LowParse.Spec.Base.parser k t
  -> FStar.Pervasives.Lemma
    (ensures LowParse.Spec.Base.injective (LowParse.Spec.List.parse_list_bare p))