val downward_closed_predicate (h: hmap) : Type0
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))))
val downward_closed_predicate (h: hmap) : Type0
let downward_closed_predicate (h: hmap) : Type0 =
forall (r: rid).
  r `is_in` h ==>
  (r = root \/
    (forall (s: rid).
        (r `is_above` s /\ s `is_in` h) ==>
        ((is_stack_region r = is_stack_region s) /\
          ((is_heap_color (color r) /\ rid_freeable r) ==> s == r))))
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.l_Forall FStar.Monotonic.HyperHeap.rid Prims.l_imp Prims.b2t FStar.Monotonic.HyperStack.is_in Prims.l_or Prims.op_Equality FStar.Monotonic.HyperHeap.root Prims.l_and FStar.Monotonic.HyperStack.is_above Prims.bool FStar.Monotonic.HyperStack.is_stack_region FStar.Monotonic.HyperStack.is_heap_color FStar.Monotonic.HyperHeap.color FStar.Monotonic.HyperHeap.rid_freeable Prims.eq2
(*
   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"]
val downward_closed_predicate (h: hmap) : Type0
h: FStar.Monotonic.HyperHeap.hmap -> Type0