val 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
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
val 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
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
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 Prims.l_and Prims.l_or Prims.b2t FStar.Pervasives.Native.uu___is_Some
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 } )
val 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

    sz: Prims.nat ->
    t: Type ->
    f:
      (s: LowParse.Bytes.bytes{FStar.Seq.Base.length s == sz}
          -> Prims.GTot (FStar.Pervasives.Native.option t)) ->
    s1: LowParse.Bytes.bytes{FStar.Seq.Base.length s1 == sz} ->
    s2: LowParse.Bytes.bytes{FStar.Seq.Base.length s2 == sz}
  -> Prims.GTot Type0