--- a/Co2sobj_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Co2sobj_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -10,13 +10,28 @@
 
 declare get_parentfs_ctxts.simps [simp del]
 
-lemma cf2sfile_open_none:
+lemma cf2sfile_open_none1:
   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b"
 apply (frule vd_cons, frule vt_grant_os)
-apply (frule noroot_events)
-by (auto split:if_splits option.splits    dest!:current_has_sec'
+apply (frule noroot_events, case_tac f, simp)
+apply (auto split:if_splits option.splits    dest!:current_has_sec' dest:parentf_in_current'
           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
+done
+
+lemma cf2sfile_open_none2:
+  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f' b = cf2sfile s f' b"
+apply (frule vd_cons, frule vt_grant_os)
+apply (induct f', simp add:cf2sfile_def)
+apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps)
+done
+
+lemma cf2sfile_open_none:
+  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"
+apply (rule ext, rule ext)
+apply (simp add:cf2sfile_open_none1 cf2sfile_open_none2)
+done
 
 lemma sroot_only:
   "cf2sfile s [] = (\<lambda> b. if b then None else Some sroot)"
@@ -26,12 +41,10 @@
   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>
    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"
 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext)
-apply (induct f', simp add:sroot_only)
-apply simp
+apply (case_tac "f = f'", simp)
+apply (induct f', simp add:sroot_only, simp)
 apply (frule parentf_in_current', simp+)
-apply (auto simp:cf2sfile_def split:if_splits option.splits)
-apply (auto  split:if_splits option.splits    dest!:current_has_sec'
-          simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)
 done
 
@@ -56,6 +69,11 @@
                   | _ \<Rightarrow> None)
      | None \<Rightarrow> None)"
 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)
+apply (case_tac f, simp)
+apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
+               get_parentfs_ctxts_simps)
+apply (rule impI)
+thm not_deleted_imp_exists
 apply (auto split:if_splits option.splits    dest!:current_has_sec'
           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 
                get_parentfs_ctxts_simps)

--- a/Current_sockets_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Current_sockets_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -242,6 +242,21 @@
 apply (case_tac t_sock_trans_state, case_tac [!] how)
 by auto
 
+lemma is_tcp_sock_imp_curernt_proc:
+  "\<lbrakk>is_tcp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:is_tcp_sock_nil is_init_tcp_sock_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by (auto simp:is_tcp_sock_simps split:if_splits option.splits t_socket_type.splits)
+
+lemma is_udp_sock_imp_curernt_proc:
+  "\<lbrakk>is_udp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:is_udp_sock_nil is_init_udp_sock_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by (auto simp:is_udp_sock_simps split:if_splits option.splits t_socket_type.splits)
+
+
 (***** below should be adjusted after starting static analysis of sockets ! ??? ****)
 
 (*

--- a/Delete_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Delete_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -1,5 +1,5 @@
 theory Deleted_prop
-imports Main Flask Flask_type Init_prop Alive_prop
+imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop
 begin
 
 context flask begin
@@ -10,21 +10,132 @@
 lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s" 
 by (auto dest:deleted_cons_I)
 
-lemma not_deleted_imp_exists:
+lemma not_deleted_init_file:
+  "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"
+apply (induct s, simp add:is_init_file_prop1)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a) prefer 6 apply (case_tac option)
+apply (auto simp:is_file_simps split:option.splits)
+done
+
+lemma not_deleted_init_dir:
+  "\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f"
+apply (induct s, simp add:is_init_dir_prop1)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a) prefer 6 apply (case_tac option)
+apply (auto simp:is_dir_simps split:option.splits)
+done
+
+lemma not_deleted_init_proc:
+  "\<lbrakk>\<not> deleted (O_proc p) s; p \<in> init_procs\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+(**** ???*)
+lemma current_fd_imp_current_proc:
+  "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:init_fds_of_proc_prop1)
+apply (frule vd_cons, drule vt_grant_os, case_tac a)
+by (auto split:if_splits option.splits)
+
+lemma not_deleted_init_fd_aux:
+  "\<lbrakk>\<not> deleted (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> 
+   \<Longrightarrow> fd \<in> current_proc_fds s p \<and> \<not> deleted (O_proc p) s"
+apply (induct s arbitrary: p, simp)
+apply (frule vd_cons, drule vt_grant_os)
+apply (case_tac a, auto dest:current_fd_imp_current_proc)
+done
+
+lemma not_deleted_init_fd2:
+  "\<lbrakk>\<not> deleted (O_fd p fd) s; fd \<in> init_fds_of_proc p; valid s\<rbrakk> \<Longrightarrow> \<not> deleted (O_proc p) s"
+by (auto dest:not_deleted_init_fd_aux)
+
+lemma not_deleted_init_fd1:
+  "\<lbrakk>\<not> deleted (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"
+by (auto dest:not_deleted_init_fd_aux)
+
+lemma not_deleted_init_tcp_aux:
+  "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
+   \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
+apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a) prefer 6 apply (case_tac option)
+by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 
+         dest:is_tcp_sock_imp_curernt_proc)
+
+lemma not_deleted_init_tcp1:
+  "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
+   \<Longrightarrow> is_tcp_sock s (p,fd)"
+by (auto dest:not_deleted_init_tcp_aux)
+
+lemma not_deleted_init_tcp2:
+  "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
+   \<Longrightarrow> \<not> deleted (O_proc p) s"
+by (auto dest:not_deleted_init_tcp_aux)
+
+lemma not_deleted_init_udp_aux:
+  "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
+   \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
+apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a) prefer 6 apply (case_tac option)
+by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits 
+         dest:is_udp_sock_imp_curernt_proc)
+
+lemma not_deleted_init_udp1:
+  "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
+   \<Longrightarrow> is_udp_sock s (p,fd)"
+by (auto dest:not_deleted_init_udp_aux)
+
+lemma not_deleted_init_udp2:
+  "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
+   \<Longrightarrow> \<not> deleted (O_proc p) s"
+by (auto dest:not_deleted_init_udp_aux)
+
+lemma not_deleted_init_shm:
+  "\<lbrakk>\<not> deleted (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+lemma not_deleted_init_msgq:
+  "\<lbrakk>\<not> deleted (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+lemma current_msg_imp_current_msgq:
+  "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"
+apply (induct s)
+apply (simp add:init_msgs_valid)
+apply (frule vd_cons, drule vt_grant_os)
+apply (case_tac a, auto split:if_splits)
+done
+
+lemma not_deleted_init_msg:
+  "\<lbrakk>\<not> deleted (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)"
+apply (induct s, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto dest:current_msg_imp_current_msgq)
+apply (case_tac "msgs_of_queue s q", simp+)
+done
+
+lemma not_deleted_imp_alive:
   "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"
-apply (induct s, simp add:init_alive_prop)
-apply (frule vd_cons)
-apply (case_tac a, auto simp:alive_simps split:t_object.splits)
-pr 19
+apply (case_tac obj)
+apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc
+  not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm 
+  not_deleted_init_msgq 
+           intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 
+  current_msg_imp_current_msgq)
 done
 
 lemma cons_app_simp_aux:
   "(a # b) @ c = a # (b @ c)" by auto
 
-lemma not_deleted_imp_exists':
-  "\<lbrakk>\<not> deleted obj (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"
+lemma not_deleted_imp_alive_app:
+  "\<lbrakk>\<not> deleted obj (s'@s); alive s obj\<rbrakk> \<Longrightarrow> alive (s'@s) obj"
 apply (induct s', simp, simp only:cons_app_simp_aux)
-apply (frule not_deleted_cons_D)
+apply (frule not_deleted_cons_D, simp)
 apply (case_tac a, case_tac [!] obj, auto)
 done
 

--- a/Flask.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Flask.thy	Thu May 09 11:19:44 2013 +0800
@@ -158,6 +158,7 @@
 
   and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"
   and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
+  and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
 
   and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p"
   and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
@@ -735,11 +736,15 @@
                                   (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or>
                                   deleted obj s)"
 | "deleted obj (CloseFd p fd # s) = ((obj = O_fd p fd) \<or> (obj = O_tcp_sock (p,fd) \<and> is_tcp_sock s (p,fd)) \<or>
-                                     (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> deleted obj s)"
+                                     (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> 
+                                     (\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> 
+                                           f \<in> files_hung_by_del s) \<or> deleted obj s)"
 | "deleted obj (Execve p f fds # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd \<and> fd \<notin> fds) \<or> 
                                        (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or>
                                        (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or>
                                        deleted obj s)"
+| "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or> 
+                                            deleted obj s)"
 | "deleted obj (UnLink p f # s) = ((obj = O_file f) \<or> deleted obj s)"
 | "deleted obj (Rmdir p f # s)  = ((obj = O_dir  f) \<or> deleted obj s)"
 | "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> 

--- a/Init_prop.thy	Wed May 08 10:00:38 2013 +0800
+++ b/Init_prop.thy	Thu May 09 11:19:44 2013 +0800
@@ -90,6 +90,10 @@
 lemma is_dir_nil: "is_dir [] = is_init_dir"
 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
 
+lemma is_udp_sock_nil:
+  "is_udp_sock [] k = is_init_udp_sock k"
+by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits)
+
 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"
 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
@@ -100,7 +104,22 @@
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2
+lemma is_init_udp_sock_prop3:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"
+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_prop4:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+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
+
+lemma is_tcp_sock_nil:
+  "is_tcp_sock [] k = is_init_tcp_sock k"
+by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits)
 
 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)"
 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 
@@ -112,8 +131,18 @@
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2
+lemma is_init_tcp_sock_prop3:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"
+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_prop4:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+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
 
 lemma init_parent_file_prop1: 
   "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"