val lemma_pop_is_popped (m0: mem{poppable m0}) : Lemma (popped m0 (pop m0))
let lemma_pop_is_popped (m0:mem{poppable m0})
  : Lemma (popped m0 (pop m0))
  = let m1 = pop m0 in
    assert (Set.equal (Map.domain m1.h) (remove_elt (Map.domain m0.h) m0.tip))
val lemma_pop_is_popped (m0: mem{poppable m0}) : Lemma (popped m0 (pop m0))
let lemma_pop_is_popped (m0: mem{poppable m0}) : Lemma (popped m0 (pop m0)) =
let m1 = pop m0 in
assert (Set.equal (Map.domain m1.h) (remove_elt (Map.domain m0.h) m0.tip))
FStar.Monotonic.HyperStack.fst.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Heap.fsti.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
FStar.Monotonic.HyperStack.fst
FStar.Monotonic.HyperStack.mem FStar.Monotonic.HyperStack.poppable Prims._assert FStar.Set.equal FStar.Monotonic.HyperHeap.rid FStar.Map.domain FStar.Monotonic.Heap.heap FStar.Monotonic.HyperStack.__proj__HS__item__h FStar.Monotonic.HyperStack.remove_elt FStar.Monotonic.HyperStack.__proj__HS__item__tip FStar.Monotonic.HyperStack.pop Prims.unit Prims.l_True Prims.squash FStar.Monotonic.HyperStack.popped Prims.Nil FStar.Pervasives.pattern
(*
   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

let map_invariant = map_invariant_predicate

let downward_closed = downward_closed_predicate

let tip_top = tip_top_predicate

let rid_ctr_pred = rid_ctr_pred_predicate

noeq type mem' =
  | HS :rid_ctr:int -> h:hmap -> tip:rid -> mem'

let mk_mem rid_ctr h tip = HS rid_ctr h tip

let get_hmap m = m.h
let get_rid_ctr m = m.rid_ctr
let get_tip m = m.tip

let lemma_mk_mem'_projectors _ _ _ = ()

let lemma_mem_projectors_are_in_wf_relation _ = ()

let lemma_is_wf_ctr_and_tip_intro _ _ _ = root_is_not_freeable ()

let lemma_is_wf_ctr_and_tip_elim _ = ()

let lemma_map_invariant _ _ _ = ()

let lemma_downward_closed _ _ _ = ()

let lemma_tip_top _ _ = ()

let lemma_tip_top_smt _ _ = ()

let lemma_rid_ctr_pred _ = ()

let as_ref #_ #_ x = MkRef?.ref x

let lemma_as_ref_inj #_ #_ _ = ()

private val lemma_extends_fresh_disjoint: i:rid -> j:rid -> ipar:rid -> jpar:rid
                               -> (m0:mem) -> (m1:mem) ->
  Lemma (requires (let h0, h1 = get_hmap m0, get_hmap m1 in
                   (map_invariant h0       /\
		    map_invariant h1       /\
                    fresh_region i m0 m1   /\
                    fresh_region j m0 m1   /\
                    h0 `Map.contains` ipar /\
                    h0 `Map.contains` jpar /\
                    extends i ipar         /\
                    extends j jpar         /\
                    i<>j)))
        (ensures (disjoint i j))
let lemma_extends_fresh_disjoint i j ipar jpar m0 m1 = ()

let lemma_sel_same_addr #_ #_ _ _ _ = ()

let lemma_upd_same_addr #_ #_ h r1 r2 x =
  FStar.Monotonic.Heap.lemma_heap_equality_upd_same_addr (Map.sel h.h (frameOf r1)) (as_ref r1) (as_ref r2) x;
  Classical.or_elim #(h `contains` r1) #(~ (h `contains` r1))
                    #(fun _ -> h `contains` r1 /\ h `contains` r2 /\ upd h r1 x == upd h r2 x)
                    (fun _ -> lemma_sel_same_addr h r1 r2) (fun _ -> lemma_sel_same_addr h r2 r1)

let mreference_distinct_sel_disjoint #_ #_ #_ h r1 r2 =
  Heap.lemma_distinct_addrs_distinct_preorders ();
  Heap.lemma_distinct_addrs_distinct_mm ();
  Heap.lemma_sel_same_addr (Map.sel h.h (frameOf r1)) (as_ref r1) (as_ref r2)

private let lemma_pop_is_popped (m0:mem{poppable m0})
val lemma_pop_is_popped (m0: mem{poppable m0}) : Lemma (popped m0 (pop m0))
m0: FStar.Monotonic.HyperStack.mem{FStar.Monotonic.HyperStack.poppable m0}
  -> FStar.Pervasives.Lemma
    (ensures FStar.Monotonic.HyperStack.popped m0 (FStar.Monotonic.HyperStack.pop m0))