# HG changeset patch
# User chunhan
# Date 1384935856 -28800
# Node ID db0e8601c22943eb4cb9f6758d41895eb48239e9
# Parent  002c34a6ff4fed12c2228b5aea37cc4029ea13ec
update socket/filefds conflict

diff -r 002c34a6ff4f -r db0e8601c229 Alive_prop.thy
--- a/Alive_prop.thy	Wed Nov 20 15:19:58 2013 +0800
+++ b/Alive_prop.thy	Wed Nov 20 16:24:16 2013 +0800
@@ -109,9 +109,8 @@
 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
                  is_tcp_sock_simps is_udp_sock_simps
-            dest:is_dir_in_current split:if_splits option.splits)
-apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto)
-
+            dest:is_dir_in_current split:if_splits option.splits
+  dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
 done
 
 lemma alive_clone:
@@ -121,21 +120,19 @@
             | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
                              else if (p'' = p') then False
                                   else alive s obj
-            | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
-                                      else if (p'' = p') then False
-                                           else alive s (O_tcp_sock (p'', fd)))
-            | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
-                                      else if (p'' = p') then False
-                                           else alive s (O_udp_sock (p'', fd)))
+            | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False
+                                      else alive s (O_tcp_sock (p'', fd)))
+            | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False
+                                       else alive s (O_udp_sock (p'', fd)))
             | _ \<Rightarrow> alive s obj )"  
 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 
                  is_tcp_sock_simps is_udp_sock_simps
            intro:is_tcp_in_current is_udp_in_current
-            dest:is_dir_in_current split:if_splits option.splits)
+            dest:is_dir_in_current split:if_splits option.splits
+  dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
 done
 
-
 lemma alive_kill:
   "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (
      \<lambda> obj. case obj of 
diff -r 002c34a6ff4f -r db0e8601c229 Init_prop.thy
--- a/Init_prop.thy	Wed Nov 20 15:19:58 2013 +0800
+++ b/Init_prop.thy	Wed Nov 20 16:24:16 2013 +0800
@@ -66,6 +66,9 @@
 apply (case_tac s, auto)
 done
 
+lemma init_socket_prop6: "(p, fd) \<in> init_sockets \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest: init_socket_has_inode)
+
 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5
 
 lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files"
@@ -114,8 +117,12 @@
 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
          dest:init_socket_has_inode inos_has_sock_tag)
 
+lemma is_init_udp_sock_prop5:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_udp_sock_prop1 intro:init_socket_prop6)
+
 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3
-  is_init_udp_sock_prop4
+  is_init_udp_sock_prop4 is_init_udp_sock_prop5
 
 lemma is_tcp_sock_nil:
   "is_tcp_sock [] k = is_init_tcp_sock k"
@@ -141,8 +148,12 @@
 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
          dest:init_socket_has_inode inos_has_sock_tag)
 
+lemma is_init_tcp_sock_prop5:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_tcp_sock_prop1 intro:init_socket_prop6)
+
 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3
-  is_init_tcp_sock_prop4
+  is_init_tcp_sock_prop4 is_init_tcp_sock_prop5
 
 lemma init_parent_file_prop1: 
   "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"
@@ -221,7 +232,16 @@
 lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"
 by (auto dest:init_filefd_valid simp:is_init_file_def)
 
-lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5
+lemma init_filefd_prop6: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_tcp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_tcp_sock_prop1)
+
+lemma init_filefd_prop7: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_udp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_udp_sock_prop1)
+
+lemma init_filefd_prop8: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> (p, fd) \<notin> init_sockets"
+by (auto dest!:init_filefd_valid)
+
+lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5 init_filefd_prop6 init_filefd_prop7 init_filefd_prop8
 
 lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"
 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)
diff -r 002c34a6ff4f -r db0e8601c229 Proc_fd_of_file_prop.thy
--- a/Proc_fd_of_file_prop.thy	Wed Nov 20 15:19:58 2013 +0800
+++ b/Proc_fd_of_file_prop.thy	Wed Nov 20 16:24:16 2013 +0800
@@ -49,20 +49,42 @@
   "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p"
 by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)
 
-lemma tcp_filefd_conflict:
-  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False"
-apply (induct s, simp)
-apply (auto simp:is_tcp_sock_simps)
+lemma filefd_socket_conflict:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; (p, fd) \<in> current_sockets s; valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s arbitrary:p)
+apply (simp add:current_sockets_simps init_filefd_prop8)
+apply (frule vt_grant_os, frule vd_cons, frule file_fds_subset_pfds, case_tac a)
+apply (auto simp:current_sockets_simps split:if_splits option.splits 
+            dest:cn_in_curp cn_in_curfd proc_fd_in_fds)
+done
 
+lemma is_tcp_in_current: "is_tcp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"
+by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)
+
+lemma is_udp_in_current: "is_udp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"
+by (auto simp:is_udp_sock_def current_sockets_def split:option.splits)
 
 lemma tcp_not_file_fd:
-  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
-apply (auto simp:proc_file_fds_def)
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (drule is_tcp_in_current)
+apply (drule filefd_socket_conflict, simp+)
+done
 
 lemma udp_not_file_fd:
-  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (drule is_udp_in_current)
+apply (drule filefd_socket_conflict, simp+)
+done
 
-lemma
+lemma tcp_notin_file_fds:
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+by (auto simp:proc_file_fds_def intro:tcp_not_file_fd)
+
+lemma udp_notin_file_fds:
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+by (auto simp:proc_file_fds_def intro:udp_not_file_fd)
 
 (******************* rebuild proc_fd_of_file simpset ***********************)
 (*