val parse_list_up_to_fuel_indep
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
      (b: bytes)
      (xy: parse_list_up_to_fuel_t cond fuel)
      (consumed: consumed_length b)
      (fuel': nat{L.length (fst xy) < fuel'})
    : Lemma (requires (parse (parse_list_up_to_fuel cond p fuel) b == Some (xy, consumed)))
      (ensures (parse (parse_list_up_to_fuel cond p fuel') b == Some ((fst xy, snd xy), consumed)))
      (decreases fuel)
let rec parse_list_up_to_fuel_indep
  (#k: parser_kind)
  (#t: Type)
  (cond: (t -> Tot bool))
  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
  (fuel: nat)
  (b: bytes)
  (xy: parse_list_up_to_fuel_t cond fuel)
  (consumed: consumed_length b)
  (fuel' : nat { L.length (fst xy) < fuel' })
: Lemma
  (requires (
    parse (parse_list_up_to_fuel cond p fuel) b == Some (xy, consumed)
  ))
  (ensures (
    parse (parse_list_up_to_fuel cond p fuel') b == Some ((fst xy, snd xy), consumed)
  ))
  (decreases fuel)
= assert (fuel > 0);
  assert (fuel' > 0);
  parse_list_up_to_fuel_eq cond p fuel b;
  parse_list_up_to_fuel_eq cond p fuel' b;
  let Some (x, consumed_x) = parse p b in
  if cond x
  then ()
  else
    let b' = Seq.slice b consumed_x (Seq.length b) in
    let Some (yz, consumed_yz) = parse (parse_list_up_to_fuel cond p (fuel - 1)) b' in
    parse_list_up_to_fuel_indep cond p (fuel - 1) b' yz consumed_yz (fuel' - 1)
val parse_list_up_to_fuel_indep
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
      (b: bytes)
      (xy: parse_list_up_to_fuel_t cond fuel)
      (consumed: consumed_length b)
      (fuel': nat{L.length (fst xy) < fuel'})
    : Lemma (requires (parse (parse_list_up_to_fuel cond p fuel) b == Some (xy, consumed)))
      (ensures (parse (parse_list_up_to_fuel cond p fuel') b == Some ((fst xy, snd xy), consumed)))
      (decreases fuel)
let rec parse_list_up_to_fuel_indep
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
      (b: bytes)
      (xy: parse_list_up_to_fuel_t cond fuel)
      (consumed: consumed_length b)
      (fuel': nat{L.length (fst xy) < fuel'})
    : Lemma (requires (parse (parse_list_up_to_fuel cond p fuel) b == Some (xy, consumed)))
      (ensures (parse (parse_list_up_to_fuel cond p fuel') b == Some ((fst xy, snd xy), consumed)))
      (decreases fuel) =
assert (fuel > 0);
assert (fuel' > 0);
parse_list_up_to_fuel_eq cond p fuel b;
parse_list_up_to_fuel_eq cond p fuel' b;
let Some (x, consumed_x) = parse p b in
if cond x
then ()
else
  let b' = Seq.slice b consumed_x (Seq.length b) in
  let Some (yz, consumed_yz) = parse (parse_list_up_to_fuel cond p (fuel - 1)) b' in
  parse_list_up_to_fuel_indep cond p (fuel - 1) b' yz consumed_yz (fuel' - 1)
LowParse.Spec.ListUpTo.fst.checked
prims.fst.checked LowParse.Spec.Seq.fst.checked LowParse.Spec.Fuel.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.ListUpTo.fst
LowParse.Spec.Base.parser_kind Prims.bool LowParse.Spec.Base.parser Prims.b2t Prims.op_disEquality FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserConsumesAll Prims.nat LowParse.Bytes.bytes LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t LowParse.Spec.Base.consumed_length Prims.op_LessThan FStar.List.Tot.Base.length LowParse.Spec.ListUpTo.refine_with_cond LowParse.Spec.ListUpTo.negate_cond FStar.Pervasives.Native.fst LowParse.Spec.ListUpTo.llist Prims.op_Subtraction LowParse.Spec.ListUpTo.parse_list_up_to_fuel_indep Prims.unit FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.parse LowParse.Spec.ListUpTo.parse_list_up_to_fuel FStar.Seq.Base.seq LowParse.Bytes.byte FStar.Seq.Base.slice FStar.Seq.Base.length LowParse.Spec.ListUpTo.parse_list_up_to_fuel_eq Prims._assert Prims.op_GreaterThan Prims.eq2 FStar.Pervasives.Native.Mktuple2 Prims.squash FStar.Pervasives.Native.snd Prims.Nil FStar.Pervasives.pattern
module LowParse.Spec.ListUpTo
open LowParse.Spec.Base
open LowParse.Spec.Fuel
open LowParse.Spec.Combinators

let llist
  (t: Type)
  (fuel: nat)
: Tot Type
= (l: list t { L.length l < fuel })

let parse_list_up_to_fuel_t
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
: Tot Type
= (llist (refine_with_cond (negate_cond cond)) fuel) & refine_with_cond cond

(* Universe-polymorphic unit type *)
type up_unit : Type u#r = | UP_UNIT

let parse_list_up_to_payload_t
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (x: t)
: Tot Type
= if cond x
  then up_unit
  else parse_list_up_to_fuel_t cond fuel

let synth_list_up_to_fuel
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (xy: dtuple2 t (parse_list_up_to_payload_t cond fuel))
: Tot (parse_list_up_to_fuel_t cond (fuel + 1))
= let (| x, yz |) = xy in
  if cond x
  then ([], x)
  else
    let (y, z) = (yz <: parse_list_up_to_fuel_t cond fuel) in
    (x :: y, z)

let synth_list_up_to_injective
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
: Lemma
  (synth_injective (synth_list_up_to_fuel cond fuel))
  [SMTPat (synth_injective (synth_list_up_to_fuel cond fuel))]
= ()

inline_for_extraction
let parse_list_up_to_payload_kind (k: parser_kind) : Tot (k' : parser_kind {k' `is_weaker_than` k }) = {
  parser_kind_low = 0;
  parser_kind_high = None;
  parser_kind_subkind = k.parser_kind_subkind;
  parser_kind_metadata = None;
}

let parse_list_up_to_payload
  (#t: Type)
  (cond: (t -> Tot bool))
  (fuel: nat)
  (k: parser_kind { k.parser_kind_subkind <> Some ParserConsumesAll })
  (ptail: parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
  (x: t)
: Tot (parser (parse_list_up_to_payload_kind k) (parse_list_up_to_payload_t cond fuel x))
= if cond x
  then weaken (parse_list_up_to_payload_kind k) (parse_ret UP_UNIT)
  else weaken (parse_list_up_to_payload_kind k) ptail

let rec parse_list_up_to_fuel
  (#k: parser_kind)
  (#t: Type)
  (cond: (t -> Tot bool))
  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
  (fuel: nat)
: Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
  (decreases fuel)
= if fuel = 0
  then fail_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)
  else
    parse_dtuple2
      (weaken (parse_list_up_to_kind k) p)
      #(parse_list_up_to_payload_kind k)
      #(parse_list_up_to_payload_t cond (fuel - 1))
      (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
      `parse_synth`
      synth_list_up_to_fuel cond (fuel - 1)

let parse_list_up_to_fuel_eq
  (#k: parser_kind)
  (#t: Type)
  (cond: (t -> Tot bool))
  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
  (fuel: nat)
  (b: bytes)
: Lemma
  (parse (parse_list_up_to_fuel cond p fuel) b == (
    if fuel = 0
    then None
    else match parse p b with
    | None -> None
    | Some (x, consumed) ->
      if cond x
      then Some (([], x), consumed)
      else begin match parse (parse_list_up_to_fuel cond p (fuel - 1)) (Seq.slice b consumed (Seq.length b)) with
      | None -> None
      | Some ((y, z), consumed') -> Some ((x::y, z), consumed + consumed')
      end
  ))
= if fuel = 0
  then ()
  else begin
    parse_synth_eq
      (parse_dtuple2
        (weaken (parse_list_up_to_kind k) p)
        #(parse_list_up_to_payload_kind k)
        #(parse_list_up_to_payload_t cond (fuel - 1))
        (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1))))
      (synth_list_up_to_fuel cond (fuel - 1))
      b;
    parse_dtuple2_eq'
      (weaken (parse_list_up_to_kind k) p)
      #(parse_list_up_to_payload_kind k)
      #(parse_list_up_to_payload_t cond (fuel - 1))
      (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
      b
  end

let rec parse_list_up_to_fuel_indep
  (#k: parser_kind)
  (#t: Type)
  (cond: (t -> Tot bool))
  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
  (fuel: nat)
  (b: bytes)
  (xy: parse_list_up_to_fuel_t cond fuel)
  (consumed: consumed_length b)
  (fuel' : nat { L.length (fst xy) < fuel' })
: Lemma
  (requires (
    parse (parse_list_up_to_fuel cond p fuel) b == Some (xy, consumed)
  ))
  (ensures (
    parse (parse_list_up_to_fuel cond p fuel') b == Some ((fst xy, snd xy), consumed)
  ))
val parse_list_up_to_fuel_indep
      (#k: parser_kind)
      (#t: Type)
      (cond: (t -> Tot bool))
      (p: parser k t {k.parser_kind_subkind <> Some ParserConsumesAll})
      (fuel: nat)
      (b: bytes)
      (xy: parse_list_up_to_fuel_t cond fuel)
      (consumed: consumed_length b)
      (fuel': nat{L.length (fst xy) < fuel'})
    : Lemma (requires (parse (parse_list_up_to_fuel cond p fuel) b == Some (xy, consumed)))
      (ensures (parse (parse_list_up_to_fuel cond p fuel') b == Some ((fst xy, snd xy), consumed)))
      (decreases fuel)

    cond: (_: t -> Prims.bool) ->
    p:
      LowParse.Spec.Base.parser k t
        { Mkparser_kind'?.parser_kind_subkind k <>
          FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserConsumesAll } ->
    fuel: Prims.nat ->
    b: LowParse.Bytes.bytes ->
    xy: LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t cond fuel ->
    consumed: LowParse.Spec.Base.consumed_length b ->
    fuel': Prims.nat{FStar.List.Tot.Base.length (FStar.Pervasives.Native.fst xy) < fuel'}
  -> FStar.Pervasives.Lemma
      (requires
        LowParse.Spec.Base.parse (LowParse.Spec.ListUpTo.parse_list_up_to_fuel cond p fuel) b ==
        FStar.Pervasives.Native.Some (xy, consumed))
      (ensures
        LowParse.Spec.Base.parse (LowParse.Spec.ListUpTo.parse_list_up_to_fuel cond p fuel') b ==
        FStar.Pervasives.Native.Some
        (FStar.Pervasives.Native.Mktuple2 (FStar.Pervasives.Native.fst xy)
            (FStar.Pervasives.Native.snd xy),
          consumed))
      (decreases fuel)