val serialize_list_singleton
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
  (a: t)
: Lemma
  (requires (serialize_list_precond k))
  (ensures (serialize (serialize_list p s) [a] == serialize s a))
let serialize_list_singleton
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
  (a: t)
: Lemma
  (requires (serialize_list_precond k))
  (ensures (serialize (serialize_list p s) [a] == serialize s a))
= Seq.append_empty_r (serialize s a)
val serialize_list_singleton
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
  (a: t)
: Lemma
  (requires (serialize_list_precond k))
  (ensures (serialize (serialize_list p s) [a] == serialize s a))
let serialize_list_singleton (#k: parser_kind) (#t: Type) (p: parser k t) (s: serializer p) (a: t)
    : Lemma (requires (serialize_list_precond k))
      (ensures (serialize (serialize_list p s) [a] == serialize s a)) =
Seq.append_empty_r (serialize s a)
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.Base.serializer FStar.Seq.Base.append_empty_r LowParse.Bytes.byte LowParse.Spec.Base.serialize Prims.unit Prims.b2t LowParse.Spec.List.serialize_list_precond Prims.squash Prims.eq2 LowParse.Bytes.bytes LowParse.Spec.List.parse_list_kind Prims.list LowParse.Spec.List.parse_list LowParse.Spec.List.serialize_list Prims.Cons Prims.Nil FStar.Pervasives.pattern
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

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

let parse_list_eq
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (b: bytes)
: Lemma
  (parse (parse_list p) b == (
    if Seq.length b = 0
    then 
      Some ([], (0 <: consumed_length b))
    else
      match parse p b with
      | None -> None
      | Some (v, n) ->
        if n = 0
        then None (* elements cannot be empty *)
        else
          match parse (parse_list p) (Seq.slice b n (Seq.length b)) with
	  | Some (l, n') -> Some (v :: l, (n + n' <: consumed_length b))
	  | _ -> None
  ))
= ()

let parse_list_eq'
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (b: bytes)
: Lemma
  (requires (k.parser_kind_low > 0))
  (ensures (parse (parse_list p) b == (
    if Seq.length b = 0
    then 
      Some ([], (0 <: consumed_length b))
    else
      match parse p b with
      | None -> None
      | Some (v, n) ->
        begin match parse (parse_list p) (Seq.slice b n (Seq.length b)) with
	  | Some (l, n') -> Some (v :: l, (n + n' <: consumed_length b))
	  | _ -> None
        end
  )))
= ()

let rec tot_parse_list_aux
  (#k: parser_kind)
  (#t: Type)
  (p: tot_parser k t)
  (b: bytes)
: Pure (option (list t * (consumed_length b)))
    (requires True)
    (ensures (fun y -> y == parse_list_aux #k p b))
    (decreases (Seq.length b))
= if Seq.length b = 0
  then 
    Some ([], (0 <: consumed_length b))
  else
    match p b with
    | None -> None
    | Some (v, n) ->
      if n = 0
      then None (* elements cannot be empty *)
      else
        match tot_parse_list_aux p (Seq.slice b n (Seq.length b)) with
	| Some (l, n') -> Some (v :: l, (n + n' <: consumed_length b))
	| _ -> None

let tot_parse_list #k #t p =
  parser_kind_prop_ext parse_list_kind (parse_list #k p) (tot_parse_list_aux p);
  tot_parse_list_aux p

let bare_serialize_list_correct
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
: Lemma
  (requires (serialize_list_precond k))
  (ensures (serializer_correct (parse_list p) (bare_serialize_list p s)))
= parser_kind_prop_equiv k p;
  let f () : Lemma (serialize_list_precond k) = () in
  let rec prf
    (l: list t)
  : Lemma
    (parse (parse_list p) (bare_serialize_list p s l) == Some (l, Seq.length (bare_serialize_list p s l)))
  = match l with
    | [] -> ()
    | a :: q ->
      let pa = parse p (bare_serialize_list p s l) in
      f ();
      parser_kind_prop_equiv k p;
      assert (no_lookahead_on p (serialize s a) (bare_serialize_list p s l));
      seq_slice_append_l (serialize s a) (bare_serialize_list p s q);
      assert (no_lookahead_on_precond p (serialize s a) (bare_serialize_list p s l));
      assert (no_lookahead_on_postcond p (serialize s a) (bare_serialize_list p s l));
      assert (Some? pa);
      assert (injective_precond p (serialize s a) (bare_serialize_list p s l));
      assert (injective_postcond p (serialize s a) (bare_serialize_list p s l));
      let (Some (a', lena)) = pa in
      assert (a == a');
      assert (lena == Seq.length (serialize s a));
      assert (lena > 0);
      prf q;
      seq_slice_append_r (serialize s a) (bare_serialize_list p s q)
  in
  Classical.forall_intro prf

let serialize_list
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
: Pure (serializer (parse_list p))
  (requires (
    serialize_list_precond k
  ))
  (ensures (fun _ -> True))
= bare_serialize_list_correct p s;
  bare_serialize_list p s

let serialize_list_nil
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
: Lemma
  (requires (
    serialize_list_precond k
  ))
  (ensures (serialize (serialize_list p s) [] == Seq.empty))
= ()

let serialize_list_cons
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
  (a: t)
  (q: list t)
: Lemma
  (requires (
    serialize_list_precond k
  ))
  (ensures (
    serialize (serialize_list p s) (a :: q) == Seq.append (serialize s a) (serialize (serialize_list p s) q)
  ))
= ()

let serialize_list_singleton
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
  (a: t)
: Lemma
  (requires (serialize_list_precond k))
val serialize_list_singleton
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (s: serializer p)
  (a: t)
: Lemma
  (requires (serialize_list_precond k))
  (ensures (serialize (serialize_list p s) [a] == serialize s a))
p: LowParse.Spec.Base.parser k t -> s: LowParse.Spec.Base.serializer p -> a: t
  -> FStar.Pervasives.Lemma (requires LowParse.Spec.List.serialize_list_precond k)
      (ensures
        LowParse.Spec.Base.serialize (LowParse.Spec.List.serialize_list p s) [a] ==
        LowParse.Spec.Base.serialize s a)