val contains_array (#a:Type) (#n:nat) (h:heap) (arr:t a n) : Type0
val contains_array (#a:Type) (#n:nat) (h:heap) (arr:t a n) : Type0
let contains_array (#a:Type) (#n:nat) (h:heap) (arr:t a n)
  = let A #_ #_ #_ s_ref _ = arr in
    h `Heap.contains` s_ref
(*
   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

private type flag =
  | Mutable
  | MutableUntilFrozen
  | Frozen

(*
 * representation of an array, a sequence of options and a flag, with an invariant that
 * if the flag is Frozen, the sequence is all Some
 *)
private type repr (a:Type0) (n:nat) :Type0 =
  t:(Seq.seq (option a) * flag){Seq.length (fst t) = n /\ ((snd t == Frozen) ==> all_some (fst t))}

(*
 * relation (preorder) between sequences
 * if b1 is set, b2 is also set, and the sequences remain same (frozen)
 * in any case, once a sequence entry is Some, it remains Some
 *)
private type seq_rel (a:Type0) (n:nat) :relation (repr a n)
  = fun (t1:repr a n) (t2:repr a n) -> let s1, f1 = t1 in
                                    let s2, f2 = t2 in
				    (f1 == Mutable ==> f2 == Mutable)               /\
				    (f1 == Frozen ==> f2 == Frozen)                 /\
				    (f1 == MutableUntilFrozen ==> (f2 =!= Mutable)) /\
				    (f1 == Frozen  ==> s1 == s2)                    /\  //once the seq is frozen, it remains so
				    (forall (i:nat). i < n ==> (init_at_seq s1 i ==> init_at_seq s2 i))  //once an index is init, it remains so
                                                                                                         //last clause corresponds to `remains_init` in the POPL'18 paper
(* typing the relation above as preorder *)
private let seq_pre (a:Type0) (n:nat) :preorder (repr a n) = seq_rel a n

(*
 * 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
 *)

noeq type t (a:Type0) (n:nat) =
  | A: #m:nat -> s_ref:mref (repr a m) (seq_pre a m) -> offset:nat{offset + n <= m} -> t a n

type mutable_pred' (#a:Type0) (#n:nat) (x:t a n) :heap_predicate
  = fun h ->
    let A #_ #_ #_ s_ref _ = x in
    h `Heap.contains` s_ref /\ (snd (sel h s_ref) == Mutable)

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

type freezable_pred' (#a:Type0) (#n:nat) (x:t a n) :heap_predicate
  = fun h ->
    let A #_ #_ #_ s_ref _ = x in
    h `Heap.contains` s_ref /\ (snd (sel h s_ref) == MutableUntilFrozen \/ (snd (sel h s_ref) == Frozen))

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

(*
 * this is true if the current array has full view of the underlying array
 * we currently require freezing only on the full array
 *)
let is_full_array (#a:Type0) (#n:nat) (arr:t a n) :bool =
  let A #_ #_ #m _ off = arr in
  off = 0 && n = m

(*
 * footprint of the array in the heap
 *)
let array_footprint (#a:Type0) (#n:nat) (arr:t a n) :GTot (Set.set nat)
  = let A s_ref _ = arr in
    Set.singleton (addr_of s_ref)

(*
 * liveness of an array in the heap
/
prims.fst.checked FStar.ST.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked ArrayUtils.fst.checked
MonotonicArray.fst
h: FStar.Monotonic.Heap.heap -> arr: MonotonicArray.t a n -> Type0
Prims.nat FStar.Monotonic.Heap.heap MonotonicArray.t FStar.ST.mref MonotonicArray.repr MonotonicArray.seq_pre Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.Monotonic.Heap.contains
let contains_array (#a: Type) (#n: nat) (h: heap) (arr: t a n) =
  
let A #_ #_ #_ s_ref _ = arr in
h `Heap.contains` s_ref