let is_wf_with_ctr_and_tip (h:hmap) (ctr:int) (tip:rid)
  = (not (rid_freeable root)) /\
    root `is_in` h /\
    tip `is_tip` h /\
    map_invariant h /\
    downward_closed h /\
    rid_ctr_pred h ctr
let is_wf_with_ctr_and_tip (h: hmap) (ctr: int) (tip: rid) =
(not (rid_freeable root)) /\ root `is_in` h /\ tip `is_tip` h /\ map_invariant h /\
downward_closed h /\ rid_ctr_pred h ctr
FStar.Monotonic.HyperStack.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Monotonic.Heap.fsti.checked FStar.Map.fsti.checked
FStar.Monotonic.HyperStack.fsti
FStar.Monotonic.HyperHeap.hmap Prims.int FStar.Monotonic.HyperHeap.rid Prims.l_and Prims.b2t Prims.op_Negation FStar.Monotonic.HyperHeap.rid_freeable FStar.Monotonic.HyperHeap.root FStar.Monotonic.HyperStack.is_in FStar.Monotonic.HyperStack.is_tip FStar.Monotonic.HyperStack.map_invariant FStar.Monotonic.HyperStack.downward_closed FStar.Monotonic.HyperStack.rid_ctr_pred Prims.logical
(*
   Copyright 2008-2014 Aseem Rastogi, and 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 FStar.Monotonic.HyperStack

open FStar.Preorder
module Map = FStar.Map

include FStar.Monotonic.HyperHeap


(****** Some predicates ******)

unfold let is_in (r:rid) (h:hmap) = h `Map.contains` r

let is_stack_region r = color r > 0
let is_heap_color c = c <= 0

[@@(deprecated "FStar.HyperStack.ST.is_eternal_region")]
let is_eternal_region r  = is_heap_color (color r) && not (rid_freeable r)

unfold let is_eternal_region_hs r = is_heap_color (color r) && not (rid_freeable r)

type sid = r:rid{is_stack_region r} //stack region ids

(*
 * AR: marking these unfolds, else I think there are pattern firing issues depending on which one we use
 *)
unfold let is_above r1 r2          = r1 `includes` r2
unfold let is_just_below r1 r2     = r1 `extends`  r2
unfold let is_below r1 r2          = r2 `is_above` r1
let is_strictly_below r1 r2 = r1 `is_below` r2 && r1 <> r2
let is_strictly_above r1 r2 = r1 `is_above` r2 && r1 <> r2


[@@"opaque_to_smt"]
unfold private let map_invariant_predicate (m:hmap) :Type0 =
  forall r. Map.contains m r ==>
      (forall s. includes s r ==> Map.contains m s)

[@@"opaque_to_smt"]
unfold private let downward_closed_predicate (h:hmap) :Type0 =
  forall (r:rid). r `is_in` h  //for any region in the memory
        ==> (r=root    //either is the root
            \/ (forall (s:rid). (r `is_above` s  //or, any region beneath it
                           /\ s `is_in` h)   //that is also in the memory
                     ==> ((is_stack_region r = is_stack_region s) /\  //must be of the same flavor as itself
                          ((is_heap_color (color r) /\ rid_freeable r) ==> s == r)))) //and if r is a freeable heap region, s can only be r (no regions strictly below r)

[@@"opaque_to_smt"]
unfold private let tip_top_predicate (tip:rid) (h:hmap) :Type0 =
  forall (r:sid). r `is_in` h <==> r `is_above` tip

[@@"opaque_to_smt"]
unfold private let rid_ctr_pred_predicate (h:hmap) (n:int) :Type0 =
  forall (r:rid). h `Map.contains` r ==> rid_last_component r < n


(****** Mem definition ******)

[@@ remove_unused_type_parameters [0]]
val map_invariant (m:hmap) :Type0  //all regions above a contained region are contained
[@@ remove_unused_type_parameters [0]]
val downward_closed (h:hmap) :Type0  //regions below a non-root region are of the same color
[@@ remove_unused_type_parameters [0;1]]
val tip_top (tip:rid) (h:hmap) :Type0  //all contained stack regions are above tip
[@@ remove_unused_type_parameters [0;1]]
val rid_ctr_pred (h:hmap) (n:int) :Type0  //all live regions have last component less than the rid_ctr

let is_tip (tip:rid) (h:hmap) =
  (is_stack_region tip \/ tip = root) /\  //the tip is a stack region, or the root
  tip `is_in` h                      /\   //the tip is live
  tip_top tip h                          //any other sid activation is a above (or equal to) the tip
val is_wf_with_ctr_and_tip : h: FStar.Monotonic.HyperHeap.hmap -> ctr: Prims.int -> tip: FStar.Monotonic.HyperHeap.rid
  -> Prims.logical
h: FStar.Monotonic.HyperHeap.hmap -> ctr: Prims.int -> tip: FStar.Monotonic.HyperHeap.rid
  -> Prims.logical