val parse_strong_prefix
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input1: bytes)
  (input2: bytes)
: Lemma
  (requires (
    k.parser_kind_subkind == Some ParserStrong /\ (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      Seq.slice input1 0 consumed `Seq.equal` Seq.slice input2 0 consumed
    | _ -> False
  )))
  (ensures (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      parse p input2 == Some (x, consumed)
    | _ -> False
  ))
let parse_strong_prefix
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input1: bytes)
  (input2: bytes)
: Lemma
  (requires (
    k.parser_kind_subkind == Some ParserStrong /\ (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      Seq.slice input1 0 consumed `Seq.equal` Seq.slice input2 0 consumed
    | _ -> False
  )))
  (ensures (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      parse p input2 == Some (x, consumed)
    | _ -> False
  ))
= assert (no_lookahead_on p input1 input2);
  assert (injective_postcond p input1 input2)
val parse_strong_prefix
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input1: bytes)
  (input2: bytes)
: Lemma
  (requires (
    k.parser_kind_subkind == Some ParserStrong /\ (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      Seq.slice input1 0 consumed `Seq.equal` Seq.slice input2 0 consumed
    | _ -> False
  )))
  (ensures (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      parse p input2 == Some (x, consumed)
    | _ -> False
  ))
let parse_strong_prefix (#k: parser_kind) (#t: Type) (p: parser k t) (input1 input2: bytes)
    : Lemma
      (requires
        (k.parser_kind_subkind == Some ParserStrong /\
          (match parse p input1 with
            | Some (x, consumed) ->
              consumed <= Seq.length input2 /\
              (Seq.slice input1 0 consumed) `Seq.equal` (Seq.slice input2 0 consumed)
            | _ -> False)))
      (ensures
        (match parse p input1 with
          | Some (x, consumed) ->
            consumed <= Seq.length input2 /\ parse p input2 == Some (x, consumed)
          | _ -> False)) =
assert (no_lookahead_on p input1 input2);
assert (injective_postcond p input1 input2)
LowParse.Spec.Base.fst.checked
prims.fst.checked LowParse.Bytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Base.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Bytes.bytes Prims._assert LowParse.Spec.Base.injective_postcond Prims.unit LowParse.Spec.Base.no_lookahead_on Prims.l_and Prims.eq2 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.ParserStrong LowParse.Spec.Base.parse LowParse.Spec.Base.consumed_length Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length LowParse.Bytes.byte FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.Pervasives.Native.tuple2 Prims.l_False Prims.logical Prims.squash FStar.Pervasives.Native.Mktuple2 Prims.Nil FStar.Pervasives.pattern
module LowParse.Spec.Base
include LowParse.Bytes

module Seq = FStar.Seq
module U8 = FStar.UInt8
module U32 = FStar.UInt32

let parser_kind_prop = parser_kind_prop'

let parser_kind_prop_equiv
  (#t: Type) (k: parser_kind) (f: bare_parser t)
: Lemma
  (parser_kind_prop k f <==> parser_kind_prop' k f)
= ()

let parser_kind_prop_ext
  (#t: Type)
  (k: parser_kind)
  (f1 f2: bare_parser t)
: Lemma
  (requires (forall (input: bytes) . parse f1 input == parse f2 input))
  (ensures (parser_kind_prop k f1 <==> parser_kind_prop k f2))
= no_lookahead_ext f1 f2;
  injective_ext f1 f2

let is_weaker_than_correct
  (k1: parser_kind)
  (k2: parser_kind)
  (#t: Type)
  (f: bare_parser t)
: Lemma
  (requires (parser_kind_prop k2 f /\ k1 `is_weaker_than` k2))
  (ensures (parser_kind_prop k1 f))
= ()

let parse_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input1: bytes)
  (input2: bytes)
: Lemma
  (requires (
    injective_precond p input1 input2
  ))
  (ensures (
    injective_postcond p input1 input2
  ))
= ()

let parse_strong_prefix
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input1: bytes)
  (input2: bytes)
: Lemma
  (requires (
    k.parser_kind_subkind == Some ParserStrong /\ (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      Seq.slice input1 0 consumed `Seq.equal` Seq.slice input2 0 consumed
    | _ -> False
  )))
  (ensures (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      parse p input2 == Some (x, consumed)
    | _ -> False
val parse_strong_prefix
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input1: bytes)
  (input2: bytes)
: Lemma
  (requires (
    k.parser_kind_subkind == Some ParserStrong /\ (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      Seq.slice input1 0 consumed `Seq.equal` Seq.slice input2 0 consumed
    | _ -> False
  )))
  (ensures (
    match parse p input1 with
    | Some (x, consumed) ->
      consumed <= Seq.length input2 /\
      parse p input2 == Some (x, consumed)
    | _ -> False
  ))
p: LowParse.Spec.Base.parser k t -> input1: LowParse.Bytes.bytes -> input2: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
      (requires
        Mkparser_kind'?.parser_kind_subkind k ==
        FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong /\
        ((match LowParse.Spec.Base.parse p input1 with
            | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ _ consumed) ->
              consumed <= FStar.Seq.Base.length input2 /\
              FStar.Seq.Base.equal (FStar.Seq.Base.slice input1 0 consumed)
                (FStar.Seq.Base.slice input2 0 consumed)
            | _ -> Prims.l_False)
          <:
          Prims.logical))
      (ensures
        ((match LowParse.Spec.Base.parse p input1 with
            | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ x consumed) ->
              consumed <= FStar.Seq.Base.length input2 /\
              LowParse.Spec.Base.parse p input2 == FStar.Pervasives.Native.Some (x, consumed)
            | _ -> Prims.l_False)
          <:
          Type0))