val lbuffer_malloc_copy (#a : Type0) (#len : size_t{size_v len > 0})
                        (r : HS.rid) (init : a)
                        (i : lbuffer a len) :
  ST (lbuffer a len)
  (requires (fun h0 ->
    live h0 i /\
    ST.is_eternal_region r))
  (ensures (fun h0 o h1 ->
    let i : buffer a = i in
    let o : buffer a = o in
    B.(modifies loc_none h0 h1) /\
    B.fresh_loc (B.loc_buffer o) h0 h1 /\
    B.(loc_includes (loc_region_only true r) (B.loc_addr_of_buffer o)) /\
    B.freeable o /\
    B.live h1 o /\
    B.as_seq h1 o == B.as_seq h0 i))
val lbuffer_malloc_copy (#a : Type0) (#len : size_t{size_v len > 0})
                        (r : HS.rid) (init : a)
                        (i : lbuffer a len) :
  ST (lbuffer a len)
  (requires (fun h0 ->
    live h0 i /\
    ST.is_eternal_region r))
  (ensures (fun h0 o h1 ->
    let i : buffer a = i in
    let o : buffer a = o in
    B.(modifies loc_none h0 h1) /\
    B.fresh_loc (B.loc_buffer o) h0 h1 /\
    B.(loc_includes (loc_region_only true r) (B.loc_addr_of_buffer o)) /\
    B.freeable o /\
    B.live h1 o /\
    B.as_seq h1 o == B.as_seq h0 i))
let lbuffer_malloc_copy #a #len r init i =
  (**) let h0 = HST.get () in
  let o = B.malloc r init len in
  copy #MUT #a #len o i;
  (**) let h2 = HST.get () in
  (**) B.(modifies_only_not_unused_in loc_none h0 h2);
  o
module Impl.Noise.TypeOrUnit

open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Sequence
open Lib.Buffer
open LowStar.BufferOps

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
open Impl.Noise.Types

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let lbuffer_malloc_also_empty #a #len r init =
  if len >. 0ul then
    B.malloc r init len
  else
    begin
    (**) let h0 = HST.get () in
    (**) assert(Seq.equal (Seq.create (size_v len) init) Seq.empty);
    (**) assert(B.as_seq h0 (null #MUT #a) `Seq.equal` Seq.empty);
    null
    end
/
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Impl.Noise.TypeOrUnit.fst
r: FStar.Monotonic.HyperHeap.rid -> init: a -> i: Lib.Buffer.lbuffer a len
  -> FStar.HyperStack.ST.ST (Lib.Buffer.lbuffer a len)
Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.size_v FStar.Monotonic.HyperHeap.rid Lib.Buffer.lbuffer Prims.unit LowStar.Monotonic.Buffer.modifies_only_not_unused_in LowStar.Monotonic.Buffer.loc_none FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.copy Lib.Buffer.MUT LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.v Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.freeable LowStar.Buffer.malloc
let lbuffer_malloc_copy #a #len r init i =
  
let h0 = HST.get () in
let o = B.malloc r init len in
copy #MUT #a #len o i;
let h2 = HST.get () in
(let open B in modifies_only_not_unused_in loc_none h0 h2);
o