val len_offset_ok : a: Zeta.LowStar.Parser.byte_array -> len: FStar.UInt32.t -> offset: FStar.UInt32.t -> Prims.logical
let len_offset_ok (a:byte_array)
                  (len:U32.t)
                  (offset:U32.t) =
  B.length a == U32.v len /\
  U32.v offset < U32.v len
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

inline_for_extraction
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
       )
/
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
a: Zeta.LowStar.Parser.byte_array -> len: FStar.UInt32.t -> offset: FStar.UInt32.t -> Prims.logical
Zeta.LowStar.Parser.byte_array FStar.UInt32.t Prims.l_and Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n LowStar.Monotonic.Buffer.length Zeta.Steel.Parser.byte LowStar.Buffer.trivial_preorder FStar.UInt32.v Prims.op_LessThan Prims.logical
let len_offset_ok (a: byte_array) (len offset: U32.t) =
  
B.length a == U32.v len /\ U32.v offset < U32.v len