val sub:
    #t:buftype
  -> #a:Type0
  -> #len:size_t
  -> b:lbuffer_t t a len
  -> start:size_t
  -> n:size_t{v start + v n <= v len} ->
  Stack (lbuffer_t t a n)
    (requires fun h0 -> live h0 b)
    (ensures  fun h0 r h1 -> h0 == h1 /\ live h1 r /\ r == gsub b start n)
let sub #t #a #len b start n =
  match t with
  | MUT -> B.sub (b <: buffer a) start n
  | IMMUT -> IB.isub (b <: ibuffer a) start n
  | CONST -> CB.sub (b <: cbuffer a) start n
val sub:
    #t:buftype
  -> #a:Type0
  -> #len:size_t
  -> b:lbuffer_t t a len
  -> start:size_t
  -> n:size_t{v start + v n <= v len} ->
  Stack (lbuffer_t t a n)
    (requires fun h0 -> live h0 b)
    (ensures  fun h0 r h1 -> h0 == h1 /\ live h1 r /\ r == gsub b start n)
let sub #t #a #len b start n =
match t with
| MUT -> B.sub (b <: buffer a) start n
| IMMUT -> IB.isub (b <: ibuffer a) start n
| CONST -> CB.sub (b <: cbuffer a) start n
Lib.Buffer.fst.checked
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fst.checked Lib.RawIntTypes.fsti.checked Lib.Memzero0.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Lib.Buffer.fst
Lib.Buffer.buftype Lib.IntTypes.size_t Lib.Buffer.lbuffer_t Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB LowStar.Buffer.sub Lib.Buffer.buffer FStar.Ghost.hide FStar.UInt32.t LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder LowStar.ImmutableBuffer.isub Lib.Buffer.ibuffer LowStar.ImmutableBuffer.immutable_preorder LowStar.ConstBuffer.sub Lib.Buffer.cbuffer LowStar.ConstBuffer.const_buffer
module Lib.Buffer

open FStar.Mul

open Lib.IntTypes
open Lib.RawIntTypes

friend Lib.Sequence
friend Lib.LoopCombinators

module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module Seq = Lib.Sequence
module ByteSeq = Lib.ByteSequence

#reset-options "--z3rlimit 350 --max_fuel 0 --max_ifuel 0"

let modifies_includes l1 l2 h0 h1 = ()
let modifies_trans l1 l2 h0 h1 h2 = ()
let live_sub #t #a #len b start n h = ()
let modifies_sub #t #a #len b start n h0 h1 = ()

let as_seq_gsub #t #a #len h b start n = ()
val sub:
    #t:buftype
  -> #a:Type0
  -> #len:size_t
  -> b:lbuffer_t t a len
  -> start:size_t
  -> n:size_t{v start + v n <= v len} ->
  Stack (lbuffer_t t a n)
    (requires fun h0 -> live h0 b)
    (ensures  fun h0 r h1 -> h0 == h1 /\ live h1 r /\ r == gsub b start n)

    b: Lib.Buffer.lbuffer_t t a len ->
    start: Lib.IntTypes.size_t ->
    n: Lib.IntTypes.size_t{Lib.IntTypes.v start + Lib.IntTypes.v n <= Lib.IntTypes.v len}
  -> FStar.HyperStack.ST.Stack (Lib.Buffer.lbuffer_t t a n)