val heap_equiv_on : h_0: FStar.DM4F.Heap.heap -> h_1: FStar.DM4F.Heap.heap -> rs: Swap.addr_set -> Prims.logical
let heap_equiv_on (h_0:heap) (h_1:heap) (rs:addr_set) =
  forall (a:Type0). forall (r: ref a).
    S.mem (addr_of r) rs /\
    h_0 `contains` r /\
    h_1 `contains` r ==>
    sel h_0 r == sel h_1 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 Swap
open FStar.List.Tot
open FStar.DM4F.Heap
open FStar.DM4F.Heap.ST
#reset-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0 --z3rlimit 100"

// Heap relies on sets with decidable equality... we follow suit.
module S = FStar.Set

// We reason about a set of addresses so as to reuse the [modifies] clause.
type addr_set = S.set nat
/
prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.DM4F.Heap.ST.fsti.checked FStar.DM4F.Heap.fsti.checked FStar.Classical.fsti.checked
Swap.fst
h_0: FStar.DM4F.Heap.heap -> h_1: FStar.DM4F.Heap.heap -> rs: Swap.addr_set -> Prims.logical
FStar.DM4F.Heap.heap Swap.addr_set Prims.l_Forall FStar.DM4F.Heap.ref Prims.l_imp Prims.l_and Prims.b2t FStar.Set.mem Prims.nat FStar.DM4F.Heap.addr_of FStar.DM4F.Heap.contains Prims.eq2 FStar.DM4F.Heap.sel Prims.logical
let heap_equiv_on (h_0 h_1: heap) (rs: addr_set) =
  
forall (a: Type0).
  forall (r: ref a).
    S.mem (addr_of r) rs /\ h_0 `contains` r /\ h_1 `contains` r ==> sel h_0 r == sel h_1 r