val index:
    #t:buftype
  -> #a:Type0
  -> #len:size_t{v len > 0}
  -> b:lbuffer_t t a len
  -> i:size_t{v i < v len} ->
  Stack a
    (requires fun h0 -> live h0 b)
    (ensures  fun h0 r h1 ->
      h0 == h1 /\
      r == Seq.index #a #(v len) (as_seq h1 b) (v i))
let index #t #a #len b i =
  match t with
  | MUT -> B.index (b <: buffer a) i
  | IMMUT -> IB.index (b <: ibuffer a) i
  | CONST -> CB.index (b <: cbuffer a) i
val index:
    #t:buftype
  -> #a:Type0
  -> #len:size_t{v len > 0}
  -> b:lbuffer_t t a len
  -> i:size_t{v i < v len} ->
  Stack a
    (requires fun h0 -> live h0 b)
    (ensures  fun h0 r h1 ->
      h0 == h1 /\
      r == Seq.index #a #(v len) (as_seq h1 b) (v i))
let index #t #a #len b i =
match t with
| MUT -> B.index (b <: buffer a) i
| IMMUT -> IB.index (b <: ibuffer a) i
| CONST -> CB.index (b <: cbuffer a) i
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 Prims.b2t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.lbuffer_t Prims.op_LessThan LowStar.Monotonic.Buffer.index LowStar.Buffer.trivial_preorder Lib.Buffer.buffer LowStar.ImmutableBuffer.immutable_preorder Lib.Buffer.ibuffer LowStar.ConstBuffer.index Lib.Buffer.cbuffer
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 = ()

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 index:
    #t:buftype
  -> #a:Type0
  -> #len:size_t{v len > 0}
  -> b:lbuffer_t t a len
  -> i:size_t{v i < v len} ->
  Stack a
    (requires fun h0 -> live h0 b)
    (ensures  fun h0 r h1 ->
      h0 == h1 /\
      r == Seq.index #a #(v len) (as_seq h1 b) (v i))
b: Lib.Buffer.lbuffer_t t a len -> i: Lib.IntTypes.size_t{Lib.IntTypes.v i < Lib.IntTypes.v len}
  -> FStar.HyperStack.ST.Stack a