val make_constant_size_parser_injective
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot (option t)))
    : Lemma (requires (make_constant_size_parser_precond sz t f))
      (ensures (injective (make_constant_size_parser_aux sz t f)))
let make_constant_size_parser_injective
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: Lemma
  (requires (
    make_constant_size_parser_precond sz t f
  ))
  (ensures (
    injective (make_constant_size_parser_aux sz t f)
  ))
= let p : bare_parser t = make_constant_size_parser_aux sz t f in
  let prf1
    (b1 b2: bytes)
  : Lemma
    (requires (injective_precond p b1 b2))
    (ensures (injective_postcond p b1 b2))
  = assert (Some? (parse p b1));
    assert (Some? (parse p b2));
    let (Some (v1, len1)) = parse p b1 in
    let (Some (v2, len2)) = parse p b2 in
    assert ((len1 <: nat) == (len2 <: nat));
    assert ((len1 <: nat) == sz);
    assert ((len2 <: nat) == sz);
    assert (make_constant_size_parser_precond_precond sz t f (Seq.slice b1 0 len1) (Seq.slice b2 0 len2));
    assert (make_constant_size_parser_precond' sz t f)
  in
  Classical.forall_intro_2 (fun (b1: bytes) -> Classical.move_requires (prf1 b1))
val make_constant_size_parser_injective
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot (option t)))
    : Lemma (requires (make_constant_size_parser_precond sz t f))
      (ensures (injective (make_constant_size_parser_aux sz t f)))
let make_constant_size_parser_injective
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot (option t)))
    : Lemma (requires (make_constant_size_parser_precond sz t f))
      (ensures (injective (make_constant_size_parser_aux sz t f))) =
let p:bare_parser t = make_constant_size_parser_aux sz t f in
let prf1 (b1 b2: bytes)
    : Lemma (requires (injective_precond p b1 b2)) (ensures (injective_postcond p b1 b2)) =
  assert (Some? (parse p b1));
  assert (Some? (parse p b2));
  let Some (v1, len1) = parse p b1 in
  let Some (v2, len2) = parse p b2 in
  assert ((len1 <: nat) == (len2 <: nat));
  assert ((len1 <: nat) == sz);
  assert ((len2 <: nat) == sz);
  assert (make_constant_size_parser_precond_precond sz
        t
        f
        (Seq.slice b1 0 len1)
        (Seq.slice b2 0 len2));
  assert (make_constant_size_parser_precond' sz t f)
in
Classical.forall_intro_2 (fun (b1: bytes) -> Classical.move_requires (prf1 b1))
LowParse.Spec.Combinators.fsti.checked
prims.fst.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Combinators.fsti
Prims.nat LowParse.Bytes.bytes Prims.eq2 FStar.Seq.Base.length LowParse.Bytes.byte FStar.Pervasives.Native.option FStar.Classical.forall_intro_2 Prims.l_imp LowParse.Spec.Base.injective_precond LowParse.Spec.Base.injective_postcond FStar.Classical.move_requires Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern LowParse.Spec.Base.consumed_length Prims._assert LowParse.Spec.Combinators.make_constant_size_parser_precond' LowParse.Spec.Combinators.make_constant_size_parser_precond_precond FStar.Seq.Base.slice FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.parse Prims.b2t FStar.Pervasives.Native.uu___is_Some LowParse.Spec.Base.bare_parser LowParse.Spec.Combinators.make_constant_size_parser_aux LowParse.Spec.Combinators.make_constant_size_parser_precond LowParse.Spec.Base.injective
module LowParse.Spec.Combinators
include LowParse.Spec.Base

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

module T = FStar.Tactics

#reset-options "--using_facts_from '* -FStar.Tactis -FStar.Reflection'"

(** Constant-size parsers *)

let make_constant_size_parser_aux
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: Tot (bare_parser t)
= fun (s: bytes) ->
  if Seq.length s < sz
  then None
  else begin
    let s' : bytes = Seq.slice s 0 sz in
    match f s' with
    | None -> None
    | Some v ->
      let (sz: consumed_length s) = sz in
      Some (v, sz)
  end

let make_constant_size_parser_precond_precond
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
  (s1: bytes { Seq.length s1 == sz } )
  (s2: bytes { Seq.length s2 == sz } )
: GTot Type0
= (Some? (f s1) \/ Some? (f s2)) /\ f s1 == f s2

let make_constant_size_parser_precond
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: GTot Type0
= forall (s1: bytes {Seq.length s1 == sz}) (s2: bytes {Seq.length s2 == sz}) . {:pattern (f s1); (f s2)}
    make_constant_size_parser_precond_precond sz t f s1 s2 ==> Seq.equal s1 s2

let make_constant_size_parser_precond'
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: GTot Type0
= forall (s1: bytes {Seq.length s1 == sz}) (s2: bytes {Seq.length s2 == sz}) . {:pattern (f s1); (f s2)}
    make_constant_size_parser_precond_precond sz t f s1 s2 ==> s1 == s2

let make_constant_size_parser_injective
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: Lemma
  (requires (
    make_constant_size_parser_precond sz t f
  ))
  (ensures (
    injective (make_constant_size_parser_aux sz t f)
val make_constant_size_parser_injective
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot (option t)))
    : Lemma (requires (make_constant_size_parser_precond sz t f))
      (ensures (injective (make_constant_size_parser_aux sz t f)))

    sz: Prims.nat ->
    t: Type ->
    f:
      (s: LowParse.Bytes.bytes{FStar.Seq.Base.length s == sz}
          -> Prims.GTot (FStar.Pervasives.Native.option t))
  -> FStar.Pervasives.Lemma
      (requires LowParse.Spec.Combinators.make_constant_size_parser_precond sz t f)
      (ensures
        LowParse.Spec.Base.injective (LowParse.Spec.Combinators.make_constant_size_parser_aux sz t f
          ))