val 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
              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')))
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
val 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
              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')))
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
              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'))) =
if fuel = 0
then ()
else
  (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)
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 Prims.op_Equality Prims.int LowParse.Spec.Combinators.parse_dtuple2_eq' LowParse.Spec.ListUpTo.parse_list_up_to_kind LowParse.Spec.Base.weaken LowParse.Spec.ListUpTo.parse_list_up_to_payload_kind LowParse.Spec.ListUpTo.parse_list_up_to_payload_t Prims.op_Subtraction LowParse.Spec.ListUpTo.parse_list_up_to_payload LowParse.Spec.ListUpTo.parse_list_up_to_fuel Prims.unit LowParse.Spec.Combinators.parse_synth_eq LowParse.Spec.Combinators.and_then_kind Prims.dtuple2 LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t Prims.op_Addition LowParse.Spec.Combinators.parse_dtuple2 LowParse.Spec.ListUpTo.synth_list_up_to_fuel Prims.l_True Prims.squash Prims.eq2 FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse FStar.Pervasives.Native.None FStar.Pervasives.Native.Mktuple2 LowParse.Spec.ListUpTo.llist LowParse.Spec.ListUpTo.refine_with_cond LowParse.Spec.ListUpTo.negate_cond Prims.Nil FStar.Seq.Base.slice LowParse.Bytes.byte FStar.Seq.Base.length Prims.Cons 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
val 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
              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')))

    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
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.parse (LowParse.Spec.ListUpTo.parse_list_up_to_fuel cond p fuel) b ==
      (match fuel = 0 with
        | true -> FStar.Pervasives.Native.None
        | _ ->
          (match LowParse.Spec.Base.parse p b with
            | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
            | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ x consumed) ->
              (match cond x with
                | true ->
                  FStar.Pervasives.Native.Some (FStar.Pervasives.Native.Mktuple2 [] x, consumed)
                | _ ->
                  (match
                      LowParse.Spec.Base.parse (LowParse.Spec.ListUpTo.parse_list_up_to_fuel cond
                            p
                            (fuel - 1))
                        (FStar.Seq.Base.slice b consumed (FStar.Seq.Base.length b))
                    with
                    | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
                    | FStar.Pervasives.Native.Some
                      #_
                      (FStar.Pervasives.Native.Mktuple2
                          #_
                          #_
                          (FStar.Pervasives.Native.Mktuple2 #_ #_ y z)
                          consumed') ->
                      FStar.Pervasives.Native.Some
                      (FStar.Pervasives.Native.Mktuple2 (x :: y) z, consumed + consumed'))
                  <:
                  FStar.Pervasives.Native.option (LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t cond
                        fuel *
                      LowParse.Spec.Base.consumed_length b))
              <:
              FStar.Pervasives.Native.option (LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t cond
                    fuel *
                  LowParse.Spec.Base.consumed_length b))
          <:
          FStar.Pervasives.Native.option (LowParse.Spec.ListUpTo.parse_list_up_to_fuel_t cond fuel *
              LowParse.Spec.Base.consumed_length b)))