val parser : p: Zeta.Steel.Parser.spec_parser t -> Type0
let parser (#t:Type0) (p:spec_parser t) =
    len:U32.t ->
    offset:U32.t ->
    slice_len:U32.t ->
    a:byte_array { len_offset_slice_ok a len offset slice_len } ->
    HST.Stack (option (t & U32.t))
       (requires fun h ->
         B.live h a
       )
       (ensures fun h o h' ->
         let b = B.as_seq h a in
         B.modifies B.loc_none h h' /\
         begin match p (slice b offset slice_len), o with
         | None, None -> True
         | Some (x, n), Some (y, n') -> x == y /\ n == U32.v n'
         | _ -> False
         end
       )
module Zeta.LowStar.Parser
include Zeta.Steel.Parser

module B = LowStar.Buffer
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32

let byte_array = B.buffer byte

let len_offset_slice_ok (a:byte_array)
                        (len offset slice_len:U32.t) =
  B.length a == U32.v len /\
  U32.v offset + U32.v slice_len <= B.length a
/
Zeta.Steel.Parser.fst.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked
Zeta.LowStar.Parser.fst
p: Zeta.Steel.Parser.spec_parser t -> Type0
Zeta.Steel.Parser.spec_parser FStar.UInt32.t Zeta.LowStar.Parser.byte_array Zeta.LowStar.Parser.len_offset_slice_ok FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.live Zeta.Steel.Parser.byte LowStar.Buffer.trivial_preorder Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none FStar.Pervasives.Native.Mktuple2 Prims.nat Zeta.Steel.Parser.slice Prims.l_True Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.UInt32.v Prims.l_False Prims.logical FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq
let parser (#t: Type0) (p: spec_parser t) =
  

    len: U32.t ->
    offset: U32.t ->
    slice_len: U32.t ->
    a: byte_array{len_offset_slice_ok a len offset slice_len}
  -> HST.Stack (option (t & U32.t))
      (requires fun h -> B.live h a)
      (ensures
        fun h o h' ->
          let b = B.as_seq h a in
          B.modifies B.loc_none h h' /\
          (match p (slice b offset slice_len), o with
            | None, None -> True
            | Some (x, n), Some (y, n') -> x == y /\ n == U32.v n'
            | _ -> False))