val write_common (#a: Type0) (#n: nat) (arr: t a n) (i: nat{i < n}) (x: a)
    : ST unit
      (requires (fun h0 -> is_mutable arr h0))
      (ensures
        (fun h0 () h1 ->
            modifies (array_footprint arr) h0 h1 /\ is_mutable arr h1 /\ arr `init_at` i /\
            Seq.index (as_seq arr h1) i == Some x))
val write_common (#a: Type0) (#n: nat) (arr: t a n) (i: nat{i < n}) (x: a)
    : ST unit
      (requires (fun h0 -> is_mutable arr h0))
      (ensures
        (fun h0 () h1 ->
            modifies (array_footprint arr) h0 h1 /\ is_mutable arr h1 /\ arr `init_at` i /\
            Seq.index (as_seq arr h1) i == Some x))
let write_common (#a:Type0) (#n:nat) (arr:t 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
  = let A #_ s_ref offset = arr in
    let (s, b) = !s_ref in
    let s = Seq.upd s (offset + i) (Some x) in
    s_ref := (s, b);
    gst_witness (initialized arr 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))]
  = ()

(* scaffolding for init_at *)
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

private let initialized' (#a:Type0) (#n:nat) (arr:t a n) (i:index arr) :heap_predicate
  = fun h -> h `contains_array` arr /\ init_at_arr arr i h

(* a stable initialized predicate *)
let initialized (#a:Type0) (#n:nat) (arr:t a n) (i:index arr) :(p:heap_predicate{stable p})
  = let A #_ #_ #m s_ref off = arr in
    assert (forall (h:heap).
              let s, _ = sel h s_ref in
	      init_at_arr arr i h <==> Some? (Seq.index s (off + i)));
    assert (forall (h1 h2:heap).
              let s1, _ = sel h1 s_ref in
	      let s2, _ = sel h2 s_ref in
              (h1 `contains_array` arr /\ heap_rel h1 h2) ==> (forall (i:nat). i < m ==> (Some? (Seq.index s1 i) ==>
	                                                                          Some? (Seq.index s2 i))));
    initialized' arr i

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

(* scaffolding for frozen predicate *)
let frozen_bit (#a:Type0) (#n:nat) (arr:t a n) (h:heap) :Type0
  = let A s_ref _ = arr in
    snd (sel h s_ref) == Frozen

private type frozen_pred' (#a:Type0) (#n:nat) (arr:t a n) (s:Seq.seq a) :heap_predicate
  = fun h -> h `contains_array` arr /\ some_equivalent_seqs (as_seq arr h) s /\ frozen_bit arr h

open FStar.Ghost

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

(* witnessed predicate for frozen *)
type frozen_with (#a:Type0) (#n:nat) (arr:t a n) (s:erased (Seq.seq a)) :Type0
  = Seq.length (reveal s) == n /\ witnessed (frozen_pred arr s)

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

(*
 * freeze an array
 *)
let 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
  = gst_recall (freezable_pred arr);
    let A #_ s_ref _ = arr in
    let s, b = !s_ref in
    s_ref := (s, Frozen);
    gst_witness (frozen_pred arr (hide (get_some_equivalent s)));
    hide (get_some_equivalent s)

(*
 * read from an array
 *)
let 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))
  = let A #_ s_ref o = arr in
    let (s, _) = !s_ref in
    gst_recall (initialized arr i);
    Some?.v (Seq.index s (o + i))
/
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: Prims.nat{i < n} -> x: a -> FStar.ST.ST Prims.unit
Prims.nat MonotonicArray.t Prims.b2t Prims.op_LessThan FStar.ST.mref MonotonicArray.repr MonotonicArray.seq_pre Prims.op_LessThanOrEqual Prims.op_Addition FStar.Seq.Base.seq FStar.Pervasives.Native.option MonotonicArray.flag Prims.unit FStar.ST.gst_witness MonotonicArray.initialized FStar.ST.op_Colon_Equals FStar.Pervasives.Native.Mktuple2 FStar.Seq.Base.upd FStar.Pervasives.Native.Some FStar.ST.op_Bang FStar.Monotonic.Heap.heap MonotonicArray.is_mutable Prims.l_and FStar.Monotonic.Heap.modifies MonotonicArray.array_footprint MonotonicArray.init_at Prims.eq2 FStar.Seq.Base.index MonotonicArray.as_seq
let write_common (#a: Type0) (#n: nat) (arr: t a n) (i: nat{i < n}) (x: a)
    : ST unit
      (requires (fun h0 -> is_mutable arr h0))
      (ensures
        (fun h0 () h1 ->
            modifies (array_footprint arr) h0 h1 /\ is_mutable arr h1 /\ arr `init_at` i /\
            Seq.index (as_seq arr h1) i == Some x)) =
  
let A #_ s_ref offset = arr in
let s, b = !s_ref in
let s = Seq.upd s (offset + i) (Some x) in
s_ref := (s, b);
gst_witness (initialized arr i);
()