val suffix : arr: MonotonicArray.t a n -> i: Prims.nat{i <= n} -> MonotonicArray.t a (n - i)
let suffix (#a:Type0) (#n:nat) (arr:t a n) (i:nat{i <= n}) = sub arr i (n - 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


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

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)  //the footprint of array was unused in h0, hopefully this enables the clients to maintain separation

(*
 * create an array that you intend to freeze some time in future
 *)
val 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

(*
 * create an array, that always remains mutable
 *)
val 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

(*
 * type of a valid index into an array
 *)
type index (#a:Type0) (#n:nat) (arr:t a n) = i:nat{i < n}

(*
 * Ghost view of an array as a sequence of options
 *)
val as_seq (#a:Type0) (#n:nat) (arr:t a n) (h:heap)
  :GTot (Seq.seq (option a))

val 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))]

(* scaffolding for init_at *)
val init_at_arr (#a:Type0) (#n:nat) (arr:t a n) (i:index arr) (h:heap) : Type0

(* a stable initialized predicate *)
val initialized (#a:Type0) (#n:nat) (arr:t a n) (i:index arr) : (p:heap_predicate{stable p})

(* witnessed predicate for initialized *)
val init_at (#a:Type0) (#n:nat) (arr:t a n) (i:index arr) : Type0

(* scaffolding for frozen predicate *)
val frozen_bit (#a:Type0) (#n:nat) (arr:t a n) (h:heap) : Type0

open FStar.Ghost

(* a stable frozen predicate *)
val frozen_pred (#a:Type0) (#n:nat) (arr:t a n) (s:erased (Seq.seq a)) :(p:heap_predicate{stable p})

(* witnessed predicate for frozen *)
val frozen_with (#a:Type0) (#n:nat) (arr:t a n) (s:erased (Seq.seq a)) :Type0

(***** serious stuff starts now *****)

(*
 * freeze an array
 *)
val freeze (#a:Type0) (#n:nat) (arr:farray a n)
  :ST (erased (Seq.seq a))
      (requires (fun h0       -> is_full_array arr /\  //can only freeze full arrays
                              (forall (i:nat). i < n ==> init_at_arr arr i h0)))  //all elements must be init_at
      (ensures  (fun h0 es h1 -> some_equivalent_seqs (as_seq arr h0) (reveal es) /\  //the returned ghost sequence is the current view of array in the heap
                              frozen_with arr es                          /\  //witnessing the stable predicate
                              (~ (is_mutable arr h1))                     /\  //the array is no longer mutable
			      modifies (array_footprint arr) h0 h1))  //only array footprint is changed

(*
 * read from an array
 *)
val read (#a:Type0) (#n:nat) (arr:t a n) (i:index arr{arr `init_at` i})  //the index must be `init_at`
  :ST a (requires (fun h0      -> True))
        (ensures  (fun h0 r h1 -> h0 == h1 /\ Some r == Seq.index (as_seq arr h0) i))

val write (#a:Type0) (#n:nat) (arr:array a n) (i:nat{i < n}) (x:a)
  :ST unit (requires (fun h0       -> True))  //the array must be mutable
           (ensures  (fun h0 () h1 -> modifies (array_footprint arr) h0 h1 /\  //only array is modified
				   arr `init_at` i                      /\  //witness the stable init predicate
				   Seq.index (as_seq arr h1) i == Some x))  //update the ghost view of the array

(*
 * write into an array
 *)
val fwrite (#a:Type0) (#n:nat) (arr:farray a n) (i:nat{i < n}) (x:a)
  :ST unit (requires (fun h0       -> is_mutable arr h0))  //the array must be mutable
           (ensures  (fun h0 () h1 -> modifies (array_footprint arr) h0 h1 /\  //only array is modified
	                           is_mutable arr h1                    /\  //the array remains mutable
				   arr `init_at` i                      /\  //witness the stable init predicate
				   Seq.index (as_seq arr h1) i == Some x))  //update the ghost view of the array

(*
 * subarray
 *)
val sub (#a:Type0) (#n:nat) (arr:t a n) (i:nat) (len:nat{i + len <= n}) :t a len
/
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 -> i: Prims.nat{i <= n} -> MonotonicArray.t a (n - i)
Prims.nat MonotonicArray.t Prims.b2t Prims.op_LessThanOrEqual MonotonicArray.sub Prims.op_Subtraction
let suffix (#a: Type0) (#n: nat) (arr: t a n) (i: nat{i <= n}) =
  
sub arr i (n - i)