val len_offset_slice_ok : a: Zeta.LowStar.Parser.byte_array ->
    len: FStar.UInt32.t ->
    offset: FStar.UInt32.t ->
    slice_len: FStar.UInt32.t
  -> Prims.logical
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
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
/
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 ->
    slice_len: 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_LessThanOrEqual Prims.op_Addition Prims.logical
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