val createL:
    #a:Type0
  -> init:list a{normalize (List.Tot.length init <= max_size_t)} ->
  StackInline (lbuffer a (size (normalize_term (List.Tot.length init))))
    (requires fun h0 -> B.alloca_of_list_pre #a init)
    (ensures  fun h0 b h1 -> live h1 b /\ stack_allocated b h0 h1 (Seq.of_list init))
let createL #a init =
  B.alloca_of_list init
val createL:
    #a:Type0
  -> init:list a{normalize (List.Tot.length init <= max_size_t)} ->
  StackInline (lbuffer a (size (normalize_term (List.Tot.length init))))
    (requires fun h0 -> B.alloca_of_list_pre #a init)
    (ensures  fun h0 b h1 -> live h1 b /\ stack_allocated b h0 h1 (Seq.of_list init))
let createL #a init =
B.alloca_of_list init
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
Prims.list FStar.Pervasives.normalize Prims.b2t Prims.op_LessThanOrEqual FStar.List.Tot.Base.length Lib.IntTypes.max_size_t LowStar.Buffer.alloca_of_list LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.Pervasives.normalize_term Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null Lib.Buffer.lbuffer Lib.IntTypes.size Lib.IntTypes.size_nat
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

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

let upd #a #len b i v =
  let h0 = ST.get() in
  B.upd (b <: buffer a) i v;
  let h1 = ST.get() in
  assert (B.modifies (loc b) h0 h1);
  assert (modifies (loc b) h0 h1)

let bget_as_seq #t #a #len h b i = ()

let recall #t #a #len b =
  match t with
  | IMMUT -> B.recall (b <: ibuffer a)
  | MUT -> B.recall (b <: buffer a)
  | CONST -> B.recall (CB.cast (b <: cbuffer a))

let create #a clen init =
  B.alloca init (normalize_term clen)

#set-options "--max_fuel 1"
val createL:
    #a:Type0
  -> init:list a{normalize (List.Tot.length init <= max_size_t)} ->
  StackInline (lbuffer a (size (normalize_term (List.Tot.length init))))
    (requires fun h0 -> B.alloca_of_list_pre #a init)
    (ensures  fun h0 b h1 -> live h1 b /\ stack_allocated b h0 h1 (Seq.of_list init))

    init:
      Prims.list a
        {FStar.Pervasives.normalize (FStar.List.Tot.Base.length init <= Lib.IntTypes.max_size_t)}
  -> FStar.HyperStack.ST.StackInline
    (Lib.Buffer.lbuffer a
        (Lib.IntTypes.size (FStar.Pervasives.normalize_term (FStar.List.Tot.Base.length init))))