val serializer_correct_implies_complete
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (f: bare_serializer t)
: Lemma
  (requires (serializer_correct p f))
  (ensures (serializer_complete p f))
let serializer_correct_implies_complete
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (f: bare_serializer t)
: Lemma
  (requires (serializer_correct p f))
  (ensures (serializer_complete p f))
= let prf
    (s: bytes)
  : Lemma
    (requires (Some? (parse p s)))
    (ensures (
      Some? (parse p s) /\ (
      let (Some (x, len)) = parse p s in
      f x == Seq.slice s 0 len
    )))
  = let (Some (x, len)) = parse p s in
    assert (injective_precond p (f x) s);
    assert (injective_postcond p (f x) s)
  in
  Classical.forall_intro (Classical.move_requires prf)
val serializer_correct_implies_complete
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (f: bare_serializer t)
: Lemma
  (requires (serializer_correct p f))
  (ensures (serializer_complete p f))
let serializer_correct_implies_complete
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (f: bare_serializer t)
    : Lemma (requires (serializer_correct p f)) (ensures (serializer_complete p f)) =
let prf (s: bytes)
    : Lemma (requires (Some? (parse p s)))
      (ensures
        (Some? (parse p s) /\
          (let Some (x, len) = parse p s in
            f x == Seq.slice s 0 len))) =
  let Some (x, len) = parse p s in
  assert (injective_precond p (f x) s);
  assert (injective_postcond p (f x) s)
in
Classical.forall_intro (Classical.move_requires prf)
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.Spec.Base.bare_serializer FStar.Classical.forall_intro LowParse.Bytes.bytes Prims.l_imp Prims.b2t FStar.Pervasives.Native.uu___is_Some FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse Prims.l_and Prims.eq2 FStar.Seq.Base.seq LowParse.Bytes.byte FStar.Seq.Base.slice Prims.logical FStar.Classical.move_requires Prims.unit Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert LowParse.Spec.Base.injective_postcond LowParse.Spec.Base.injective_precond FStar.Pervasives.Native.option LowParse.Spec.Base.serializer_correct LowParse.Spec.Base.serializer_complete
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
  ))
= assert (no_lookahead_on p input1 input2);
  assert (injective_postcond p input1 input2)

let serializer_correct_implies_complete
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (f: bare_serializer t)
: Lemma
  (requires (serializer_correct p f))
val serializer_correct_implies_complete
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (f: bare_serializer t)
: Lemma
  (requires (serializer_correct p f))
  (ensures (serializer_complete p f))
p: LowParse.Spec.Base.parser k t -> f: LowParse.Spec.Base.bare_serializer t
  -> FStar.Pervasives.Lemma (requires LowParse.Spec.Base.serializer_correct p f)
      (ensures LowParse.Spec.Base.serializer_complete p f)