val recall_contents:
    #a:Type0
  -> #len:size_t{v len <= max_size_t}
  -> b:glbuffer a len
  -> s:Seq.lseq a (v len) ->
  ST unit
    (requires fun h0 -> (live h0 b \/ recallable b) /\ witnessed b s)
    (ensures  fun h0 _ h1 -> h0 == h1 /\ live h0 b /\ as_seq h0 b == s)
let recall_contents #a #len b s =
  B.recall_p (CB.to_ibuffer b) (cpred s)
val recall_contents:
    #a:Type0
  -> #len:size_t{v len <= max_size_t}
  -> b:glbuffer a len
  -> s:Seq.lseq a (v len) ->
  ST unit
    (requires fun h0 -> (live h0 b \/ recallable b) /\ witnessed b s)
    (ensures  fun h0 _ h1 -> h0 == h1 /\ live h0 b /\ as_seq h0 b == s)
let recall_contents #a #len b s =
B.recall_p (CB.to_ibuffer b) (cpred s)
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.IntTypes.size_t Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Lib.Buffer.glbuffer Lib.Sequence.lseq LowStar.Monotonic.Buffer.recall_p LowStar.ImmutableBuffer.immutable_preorder LowStar.ConstBuffer.to_ibuffer Lib.Buffer.cpred Prims.unit
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"

let createL #a init =
  B.alloca_of_list init

let createL_global #a init =
  CB.of_ibuffer (IB.igcmalloc_of_list #a root init)

let createL_mglobal #a init =
  B.mgcmalloc_of_list #a FStar.Monotonic.HyperHeap.root init
val recall_contents:
    #a:Type0
  -> #len:size_t{v len <= max_size_t}
  -> b:glbuffer a len
  -> s:Seq.lseq a (v len) ->
  ST unit
    (requires fun h0 -> (live h0 b \/ recallable b) /\ witnessed b s)
    (ensures  fun h0 _ h1 -> h0 == h1 /\ live h0 b /\ as_seq h0 b == s)
b: Lib.Buffer.glbuffer a len -> s: Lib.Sequence.lseq a (Lib.IntTypes.v len)
  -> FStar.HyperStack.ST.ST Prims.unit