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

(*
 * this is a precondition for writing, essentially, it will be false once you freeze the array
 *)
let is_mutable (#a:Type0) (#n:nat) (arr:t a n) (h:heap)
  = let A #_ s_ref _ = arr in
    let f = snd (sel h s_ref) in
    f == Mutable \/ f == MutableUntilFrozen

(*
 * create an array that you intend to freeze some time in future
 *)
let fcreate (a:Type0) (n:nat)
  :ST (farray a n) (requires (fun _         -> True))
                   (ensures  (fun h0 arr h1 -> fresh_arr arr h0 h1      /\  //it's fresh
		                            modifies Set.empty h0 h1 /\  //no existing refs are changed
					    is_mutable arr h1        /\  //the array is mutable
					    is_full_array arr))         //and has the full view of the underlying sequence
  = let arr = A #a #n #n (alloc ((Seq.create n None), MutableUntilFrozen)) 0 in
    gst_witness (freezable_pred arr);
    arr

(*
 * create an array, that always remains mutable
 *)
let create (a:Type0) (n:nat)
  :ST (array a n) (requires (fun _         -> True))
                  (ensures  (fun h0 arr h1 -> fresh_arr arr h0 h1      /\  //it's fresh
		                           modifies Set.empty h0 h1 /\  //no existing refs are changed
					   is_full_array arr))         //and has the full view of the underlying sequence
  = let arr = A #a #n #n (alloc ((Seq.create n None), Mutable)) 0 in
    gst_witness (mutable_pred arr);
    arr

(*
 * Ghost view of an array as a sequence of options
 *)
let as_seq (#a:Type0) (#n:nat) (arr:t a n) (h:heap)
  :GTot (Seq.seq (option a))
  = let A #_ #_ #_ s_ref off = arr in
    let s = fst (sel h s_ref) in
    Seq.slice s off (off + n)

let lemma_as_seq_length (#a:Type0) (#n:nat) (arr:t a n) (h:heap)
  :Lemma (requires True)
         (ensures  (Seq.length (as_seq arr h) = n))
	 [SMTPat (Seq.length (as_seq arr h))]
  = ()
/
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
arr: MonotonicArray.t a n -> i: MonotonicArray.index arr -> h: FStar.Monotonic.Heap.heap -> Type0
Prims.nat MonotonicArray.t MonotonicArray.index FStar.Monotonic.Heap.heap ArrayUtils.init_at_seq FStar.Seq.Base.seq FStar.Pervasives.Native.option MonotonicArray.as_seq
let init_at_arr (#a: Type0) (#n: nat) (arr: t a n) (i: index arr) (h: heap) : Type0 =
  
let s = as_seq arr h in
init_at_seq s i