val heap_rel : h0: NatHeap.heap -> h1: NatHeap.heap -> Prims.logical
let heap_rel (h0:heap) (h1:heap) = 
  (forall a (r:ref a) . contains r h0 ==> contains r h1) /\
  (forall a (r:ref a{contains r h0}) . sel h0 r == sel h1 r)
(*
   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 ImmutableST

open NatHeap

open FStar.Preorder
open FStar.Monotonic.Witnessed

(* Swapping the reference and heap arguments of (NatHeap.contains_ref) to 
   use it in point-free style in calls to (witness) and (recall). *)

let contains (#a:Type) (r:ref a) (h:heap) = NatHeap.contains h r

val contains_lemma : #a:Type -> 
                     h:heap -> 
	             r:ref a ->
	             Lemma (requires (contains r h)) 
			   (ensures  (NatHeap.contains h r))
	             [SMTPat (contains r h)]
let contains_lemma #a h r = ()


(* Two heaps are related if the latter differs from the former only by new 
   allocated references and all existing content is preserved unchanged. *)
/
prims.fst.checked NatHeap.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Witnessed.fsti.checked
ImmutableST.fst
h0: NatHeap.heap -> h1: NatHeap.heap -> Prims.logical
NatHeap.heap Prims.l_and Prims.l_Forall NatHeap.ref Prims.l_imp ImmutableST.contains Prims.eq2 NatHeap.sel Prims.logical
let heap_rel (h0 h1: heap) =
  
(forall a (r: ref a). contains r h0 ==> contains r h1) /\
(forall a (r: ref a {contains r h0}). sel h0 r == sel h1 r)