val parse_fldata_injective (#k: parser_kind) (#t: Type) (p: parser k t) (sz: nat)
    : Lemma (ensures (injective (parse_fldata' p sz)))
let parse_fldata_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Lemma
  (ensures (injective (parse_fldata' p sz)))
= parser_kind_prop_equiv k p;
  let f
    (b1 b2: bytes)
  : Lemma
    (requires (injective_precond (parse_fldata' p sz) b1 b2))
    (ensures (injective_postcond (parse_fldata' p sz) b1 b2))
  = assert (injective_precond p (Seq.slice b1 0 sz) (Seq.slice b2 0 sz))
  in
  Classical.forall_intro_2 (fun b -> Classical.move_requires (f b))
val parse_fldata_injective (#k: parser_kind) (#t: Type) (p: parser k t) (sz: nat)
    : Lemma (ensures (injective (parse_fldata' p sz)))
let parse_fldata_injective (#k: parser_kind) (#t: Type) (p: parser k t) (sz: nat)
    : Lemma (ensures (injective (parse_fldata' p sz))) =
parser_kind_prop_equiv k p;
let f (b1 b2: bytes)
    : Lemma (requires (injective_precond (parse_fldata' p sz) b1 b2))
      (ensures (injective_postcond (parse_fldata' p sz) b1 b2)) =
  assert (injective_precond p (Seq.slice b1 0 sz) (Seq.slice b2 0 sz))
in
Classical.forall_intro_2 (fun b -> Classical.move_requires (f b))
LowParse.Spec.FLData.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.FLData.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser Prims.nat FStar.Classical.forall_intro_2 LowParse.Bytes.bytes Prims.l_imp LowParse.Spec.Base.injective_precond LowParse.Spec.FLData.parse_fldata' LowParse.Spec.Base.injective_postcond FStar.Classical.move_requires Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert FStar.Seq.Base.slice LowParse.Bytes.byte LowParse.Spec.Base.parser_kind_prop_equiv LowParse.Spec.Base.injective
(* Parse data of some explicitly fixed length *)

module LowParse.Spec.FLData
include LowParse.Spec.Combinators

module Seq = FStar.Seq
module Classical = FStar.Classical

inline_for_extraction
val parse_fldata'
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Tot (bare_parser t)

let parse_fldata' #k #t p sz =
  let () = () in // Necessary to pass arity checking
  fun (s: bytes) ->
  if Seq.length s < sz
  then None
  else
    match parse p (Seq.slice s 0 sz) with
    | Some (v, consumed) ->
      if (consumed <: nat) = (sz <: nat)
      then Some (v, (sz <: consumed_length s))
      else None
    | _ -> None

let parse_fldata_injective
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (sz: nat)
: Lemma
val parse_fldata_injective (#k: parser_kind) (#t: Type) (p: parser k t) (sz: nat)
    : Lemma (ensures (injective (parse_fldata' p sz)))
p: LowParse.Spec.Base.parser k t -> sz: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures LowParse.Spec.Base.injective (LowParse.Spec.FLData.parse_fldata' p sz))