val equiv_on_h : c_0: Swap.command -> c_1: Swap.command -> h: FStar.DM4F.Heap.heap -> Prims.logical
let equiv_on_h (c_0:command) (c_1:command) (h:heap) = 
       let (), h_0 = reify (c_0 ()) h in
       let (), h_1 = reify (c_1 ()) h in
       no_alloc h h_0 /\
       no_alloc h h_1 /\
       heap_eq h h_0 h_1
(*
   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

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

let heap_eq (h:heap) (h_0:heap) (h_1:heap) =
   forall (a:Type) (r:ref a).  h `contains` r ==> sel h_0 r == sel h_1 r

type command = unit -> STNull unit

let no_alloc (h:heap) (h':heap) = forall (a:Type0). forall (r: ref a). h `contains` r <==> h' `contains` r

(** [fp_body f rs ws h_0 h_1] means as long as h_0 and h_1 coincide on [rs], then the
    resulting heaps coincide on [ws]. *)
let fp_body (f: command) (rs: addr_set) (ws: addr_set) (h_0:heap) (h_1:heap) = // /\ heap_contains h_0 (rs `S.union` ws) /\ heap_contains h_1 (rs `S.union` ws)}) =
  let (), h'_0 = reify (f ()) h_0 in
  let (), h'_1 = reify (f ()) h_1 in
  modifies ws h_0 h'_0 /\
  modifies ws h_1 h'_1 /\
  no_alloc h_0 h'_0 /\
  no_alloc h_1 h'_1 /\  
  (heap_equiv_on h_0 h_1 rs ==> heap_equiv_on h'_0 h'_1 ws)

(** [footprint f rs ws] generalizes the heaps in fp_body **)
let footprint (f: command) (rs: addr_set) (ws: addr_set) =
  forall (h_0: heap) (h_1: heap).{:pattern (reify (f ()) h_0);
                                    (reify (f ()) h_1)} fp_body f rs ws h_0 h_1

(* [cmd r w] is a command whose footprint is r,w  *)
type cmd (r:addr_set) (w:addr_set) = c:command{footprint c r w}


let seq' (#r1 #w1 #r2 #w2 : addr_set) (c1:cmd r1 w1) (c2:cmd r2 w2) (_:unit) : STNull unit =
  (c1 <: command) (); (c2 <: command) ()

let seq'_lem (#r1 #w1 #r2 #w2 : addr_set) (c1:cmd r1 w1) (c2:cmd r2 w2) 
 : Lemma (footprint (seq' c1 c2) (r1 `S.union` r2) (w1 `S.union` w2))
 = let aux (h:heap) (h':heap)
      : Lemma (fp_body (seq' c1 c2) (r1 `S.union` r2) (w1 `S.union` w2) h h') 
      = let c1 = c1 <: command in
        let c2 = c2 <: command in  
        let _, h1 = reify (c1 ()) h in 
        let _, h2 = reify (c2 ()) h1 in 
        let _, h1' = reify (c1 ()) h' in 
        let _, h2' = reify (c2 ()) h1' in 
        () in
   FStar.Classical.forall_intro_2 aux

let (>>) (#r1 #w1 #r2 #w2 : addr_set) (c1:cmd r1 w1) (c2:cmd r2 w2) 
  : cmd (r1 `S.union` r2) (w1 `S.union` w2)
  = seq'_lem c1 c2;
    seq' c1 c2
/
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
c_0: Swap.command -> c_1: Swap.command -> h: FStar.DM4F.Heap.heap -> Prims.logical
Swap.command FStar.DM4F.Heap.heap Prims.l_and Swap.no_alloc Swap.heap_eq Prims.logical FStar.Pervasives.Native.tuple2 Prims.unit
let equiv_on_h (c_0 c_1: command) (h: heap) =
  
let (), h_0 = reify (c_0 ()) h in
let (), h_1 = reify (c_1 ()) h in
no_alloc h h_0 /\ no_alloc h h_1 /\ heap_eq h h_0 h_1