val lbuffer_or_unit_copy (#a : Type0) (#len : size_t{size_v len > 0}) (#b : bool)
                         (o i : type_or_unit (lbuffer a len) b) :
  Stack unit
  (requires (fun h0 ->
    B.live h0 (lbuffer_or_unit_to_buffer o) /\
    B.live h0 (lbuffer_or_unit_to_buffer i) /\
    disjoint (lbuffer_or_unit_to_buffer o) (lbuffer_or_unit_to_buffer i)))
  (ensures (fun h0 _ h1 ->
     let o_loc = if b then B.loc_buffer (o <: buffer a) else B.loc_none in
     B.modifies o_loc h0 h1 /\
     lbuffer_or_unit_to_seq h1 o == lbuffer_or_unit_to_seq h0 i /\
     B.live h1 (lbuffer_or_unit_to_buffer o)))
val lbuffer_or_unit_copy (#a : Type0) (#len : size_t{size_v len > 0}) (#b : bool)
                         (o i : type_or_unit (lbuffer a len) b) :
  Stack unit
  (requires (fun h0 ->
    B.live h0 (lbuffer_or_unit_to_buffer o) /\
    B.live h0 (lbuffer_or_unit_to_buffer i) /\
    disjoint (lbuffer_or_unit_to_buffer o) (lbuffer_or_unit_to_buffer i)))
  (ensures (fun h0 _ h1 ->
     let o_loc = if b then B.loc_buffer (o <: buffer a) else B.loc_none in
     B.modifies o_loc h0 h1 /\
     lbuffer_or_unit_to_seq h1 o == lbuffer_or_unit_to_seq h0 i /\
     B.live h1 (lbuffer_or_unit_to_buffer o)))
let lbuffer_or_unit_copy #a #len #b o i =
  if b then copy #MUT #a #len (lbuffer_or_unit_to_buffer o) (lbuffer_or_unit_to_buffer i)
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 ()

let lbuffer_or_unit_malloc #a #len #b r init =
  if b then B.malloc r init len else ()

let lbuffer_or_unit_free #a #len #b buf =
  if b then B.free (lbuffer_or_unit_to_buffer buf) 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

    o: Impl.Noise.TypeOrUnit.type_or_unit (Lib.Buffer.lbuffer a len) b ->
    i: Impl.Noise.TypeOrUnit.type_or_unit (Lib.Buffer.lbuffer a len) b
  -> FStar.HyperStack.ST.Stack Prims.unit
Lib.IntTypes.size_t Prims.b2t Prims.op_GreaterThan Lib.IntTypes.size_v Prims.bool Impl.Noise.TypeOrUnit.type_or_unit Lib.Buffer.lbuffer Lib.Buffer.copy Lib.Buffer.MUT Impl.Noise.TypeOrUnit.lbuffer_or_unit_to_buffer Prims.unit
let lbuffer_or_unit_copy #a #len #b o i =
  
if b then copy #MUT #a #len (lbuffer_or_unit_to_buffer o) (lbuffer_or_unit_to_buffer i)