val fresh_arr : arr: MonotonicArray.t a n -> h0: FStar.Monotonic.Heap.heap -> h1: FStar.Monotonic.Heap.heap
  -> Prims.logical
let fresh_arr (#a:Type0) (#n:nat) (arr:t a n) (h0 h1:heap)
  = h1 `contains_array` arr /\  //array is live in h1
    (forall (n:nat). Set.mem n (array_footprint arr) ==> n `addr_unused_in` h0)
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module MonotonicArray

open FStar.Preorder
open FStar.Heap
open FStar.ST

module Set = FStar.Set

open FStar.Seq

open ArrayUtils


(*
 * an array is a mref and an offset into the array (for taking interior pointers)
 * the view of an array is from offset to m
 *)

val t (a:Type0) (n:nat) : Type0

val mutable_pred (#a:Type0) (#n:nat) (x:t a n) : (p:heap_predicate{stable p})

val freezable_pred (#a:Type0) (#n:nat) (x:t a n) : (p:heap_predicate{stable p})

type farray (a:Type0) (n:nat) = x:t a n{witnessed (freezable_pred x)}  //an array that you intend to freeze in future

type array (a:Type0) (n:nat) = x:t a n{witnessed (mutable_pred x)}  //an array that you don't intend to freeze

(*
 * this is true if the current array has full view of the underlying array
 * we currently require freezing only on the full array
 *)
val is_full_array (#a:Type0) (#n:nat) (arr:t a n) : bool

(*
 * footprint of the array in the heap
 *)
val array_footprint (#a:Type0) (#n:nat) (arr:t a n) : GTot (Set.set nat)

(*
 * liveness of an array in the heap
 *)
val contains_array (#a:Type) (#n:nat) (h:heap) (arr:t a n) : Type0

(*
 * this is a precondition for writing, essentially, it will be false once you freeze the array
 *)
val is_mutable (#a:Type0) (#n:nat) (arr:t a n) (h:heap) : Type0
/
prims.fst.checked FStar.ST.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked ArrayUtils.fst.checked
MonotonicArray.fsti
arr: MonotonicArray.t a n -> h0: FStar.Monotonic.Heap.heap -> h1: FStar.Monotonic.Heap.heap
  -> Prims.logical
Prims.nat MonotonicArray.t FStar.Monotonic.Heap.heap Prims.l_and MonotonicArray.contains_array Prims.l_Forall Prims.l_imp Prims.b2t FStar.Set.mem MonotonicArray.array_footprint FStar.Monotonic.Heap.addr_unused_in Prims.logical
let fresh_arr (#a: Type0) (#n: nat) (arr: t a n) (h0 h1: heap) =
  
h1 `contains_array` arr /\
(forall (n: nat). Set.mem n (array_footprint arr) ==> n `addr_unused_in` h0)