val lbuffer_or_unit_malloc (#a : Type0) (#len : size_t{size_v len > 0}) (#b : bool)
                           (r : HS.rid) (init : a) :
  ST (type_or_unit (lbuffer a len) b)
  (requires (fun _ ->
    ST.is_eternal_region r))
  (ensures (fun h0 p h1 ->
     B.(modifies loc_none h0 h1) /\
     B.fresh_loc (lbuffer_or_unit_to_loc p) h0 h1 /\
     B.(loc_includes (loc_region_only true r) (lbuffer_or_unit_to_loc p)) /\
     lbuffer_or_unit_freeable p /\
     B.live h1 (lbuffer_or_unit_to_buffer p)))
val lbuffer_or_unit_malloc (#a : Type0) (#len : size_t{size_v len > 0}) (#b : bool)
                           (r : HS.rid) (init : a) :
  ST (type_or_unit (lbuffer a len) b)
  (requires (fun _ ->
    ST.is_eternal_region r))
  (ensures (fun h0 p h1 ->
     B.(modifies loc_none h0 h1) /\
     B.fresh_loc (lbuffer_or_unit_to_loc p) h0 h1 /\
     B.(loc_includes (loc_region_only true r) (lbuffer_or_unit_to_loc p)) /\
     lbuffer_or_unit_freeable p /\
     B.live h1 (lbuffer_or_unit_to_buffer p)))
let lbuffer_or_unit_malloc #a #len #b r init =
  if b then B.malloc r init len else ()
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

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

let lbuffer_malloc_copy_also_empty #a #len r init i =
  if len >. 0ul then
    lbuffer_malloc_copy r init i
  else
    begin
    (**) let h0 = HST.get () in
    (**) assert(as_seq h0 i `Seq.equal` (Seq.empty #a));
    (**) assert(B.as_seq h0 (null #MUT #a) `Seq.equal` Seq.empty);
    null
    end

let lbuffer_or_unit_frame_lem #a #len #b l h0 h1 opt_buf = ()

let lbuffer_or_unit_alloca #a #len #b zero =
  if b then B.alloca zero len else ()
/
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
  -> FStar.HyperStack.ST.ST (Impl.Noise.TypeOrUnit.type_or_unit (Lib.Buffer.lbuffer a len) b)
Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.size_v Prims.bool FStar.Monotonic.HyperHeap.rid LowStar.Buffer.malloc 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 Impl.Noise.TypeOrUnit.type_or_unit Lib.Buffer.lbuffer
let lbuffer_or_unit_malloc #a #len #b r init =
  
if b then B.malloc r init len