diff -r 8557d7872fdb -r db15ef2ee18c S2ss_prop.thy
--- a/S2ss_prop.thy	Wed Sep 04 09:58:30 2013 +0800
+++ b/S2ss_prop.thy	Wed Sep 04 15:13:54 2013 +0800
@@ -6,731 +6,16 @@
 
 context tainting_s begin
 
-
-lemma current_proc_has_sp:
-  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"
-by (auto simp:cp2sproc_def split:option.splits dest!:current_has_sec')
-
-lemma current_proc_has_sp':
-  "\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
-by (auto dest:current_proc_has_sp)
-
-lemma is_dir_has_sdir':
-  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"
-apply (case_tac f)
-apply (rule_tac x = sroot in exI)
-apply (simp add:sroot_only)
-apply (drule is_dir_has_sfile, auto)
-done
-
-lemma is_file_has_sfile':
-  "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"
-by (drule is_file_has_sfile, auto)
-
-(* simpset for same_inode_files: Current_files_prop.thy *)
-
-lemma same_inode_files_nil:
-  "same_inode_files [] = init_same_inode_files"
-by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
-
-lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"
-by (auto simp add:current_inode_nums_def current_file_inums_def)
-
-lemma same_inode_files_open:
-  "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.
-     if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
-            dest:iof's_im_in_cim iof's_im_in_cim')
-apply (drule is_file_in_current)
-apply (simp add:current_files_def)
-done
-
-lemma same_inode_files_linkhard:
-  "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. 
-     if (f' = f \<or> f' \<in> same_inode_files s oldf) 
-     then same_inode_files s oldf \<union> {f}
-     else same_inode_files s f')"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
-            dest:iof's_im_in_cim iof's_im_in_cim')
-apply (drule is_file_in_current)
-apply (simp add:current_files_def is_file_def)
-apply (simp add:is_file_def)
-done
-
-lemma inum_of_file_none_prop:
-  "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
-by (simp add:current_files_def)
-
-lemma same_inode_files_closefd:
-  "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> 
-   same_inode_files (CloseFd p fd # s) f' = (
-     case (file_of_proc_fd s p fd) of 
-       Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
-                 then same_inode_files s f' - {f}
-                 else same_inode_files s f' )
-     | None   \<Rightarrow> same_inode_files s f' )"
-apply (frule vt_grant_os, frule vd_cons)
-apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd 
-           split:if_splits option.splits
-            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
-done
-
-lemma same_inode_files_unlink:
-  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> 
-   \<Longrightarrow> same_inode_files (UnLink p f # s) f' = (
-     if (proc_fd_of_file s f = {}) 
-     then same_inode_files s f' - {f}
-     else same_inode_files s f')"
-apply (frule vt_grant_os, frule vd_cons)
-apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink 
-           split:if_splits option.splits
-            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
-done
-
-lemma same_inode_files_mkdir:
-  "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:same_inode_files_def is_file_simps current_files_simps 
-           split:if_splits option.splits
-            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)
-apply (simp add:current_files_def is_file_def)
-done
-
-lemma same_inode_files_other:
-  "\<lbrakk>valid (e # s); 
-    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
-    \<forall> p fd. e \<noteq> CloseFd p fd;
-    \<forall> p f. e \<noteq> UnLink p f;
-    \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s)  = same_inode_files s"
-apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)
-apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def
-           split:if_splits option.splits
-            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)
-apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+
-done
- 
-lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard
-  same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other
-
-lemma same_inode_files_prop1:
-  "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"
-by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)
-
-lemma same_inode_files_prop2:
-  "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"
-by (auto dest:same_inode_files_prop1)
-
-lemma same_inode_files_prop3:
-  "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"
-apply (rule notI)
-apply (simp add:same_inode_files_def is_file_def is_dir_def 
-          split:if_splits option.splits t_inode_tag.splits)
-done
-
-lemma same_inode_files_prop4:
-  "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"
-by (auto simp:same_inode_files_def split:if_splits)
-
-lemma same_inode_files_prop5:
-  "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
-by (auto simp:same_inode_files_def is_file_def split:if_splits)
-
-lemma same_inode_files_prop6:
-  "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"
-by (auto simp:same_inode_files_def is_file_def split:if_splits)
-
-lemma same_inode_files_prop7:
-  "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
-
-lemma same_inode_files_prop8:
-  "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
-
-(* simpset for cf2sfiles *)
-
-lemma cf2sfiles_open:
-  "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
-   \<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = (
-     if (f' = f \<and> opt \<noteq> None) 
-     then (case cf2sfile (Open p f flag fd opt # s) f of 
-             Some sf \<Rightarrow> {sf}  
-           | _       \<Rightarrow> {} )
-     else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons)
-apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open
-  split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open)
-apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+
-done
-
-lemma cf2sfiles_other:
-  "\<lbrakk>valid (e # s);
-    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
-    \<forall> p fd. e \<noteq> CloseFd p fd;
-    \<forall> p f. e \<noteq> UnLink p f;
-    \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> cf2sfiles (e # s) = cf2sfiles s"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI)
-apply (drule Set.CollectD, erule bexE, rule CollectI)
-apply (rule_tac x = f' in bexI, case_tac e)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
-  split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
-apply (drule_tac f' = f' in cf2sfile_rmdir)
-apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
-
-apply (rule_tac x = f' in bexI, case_tac e)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
-  split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
-apply (drule_tac f' = f' in cf2sfile_rmdir)
-apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
-done
-
-lemma cf2sfile_linkhard1':
-  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>
-   \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
-apply (drule same_inode_files_prop1)
-by (simp add:cf2sfile_linkhard1)
-
-lemma cf2sfiles_linkhard:
-  "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. 
-     if (f' = f \<or> f' \<in> same_inode_files s oldf)
-     then (case (cf2sfile (LinkHard p oldf f # s) f) of
-             Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}
-           | _       \<Rightarrow> {})
-     else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard 
-  split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1)
-done
-
-lemma cf2sfile_unlink':
-  "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>
-   \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
-apply (drule same_inode_files_prop1)
-by (simp add:cf2sfile_unlink)
-
-lemma cf2sfiles_unlink:
-  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = ( 
-     if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
-         (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then 
-        (case (cf2sfile s f) of 
-           Some sf \<Rightarrow> cf2sfiles s f' - {sf}
-         | _       \<Rightarrow> {})
-     else cf2sfiles s f')"
-apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits)
-apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp, erule conjE)
-apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink)
-apply (simp add:current_files_unlink same_inode_files_prop1, simp)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
-apply (erule conjE|erule exE|erule bexE)+
-apply (case_tac "f'a = f", simp)
-apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink)
-apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (rule_tac x = f'a in bexI, simp, simp)
-
-apply (rule impI)+
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp, (erule conjE)+)
-apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink)
-apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (case_tac "f'a = f", simp)
-apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = f'' in bexI)
-apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (simp, simp, erule same_inode_files_prop4, simp)
-apply (rule_tac x = f'a in bexI)
-apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
-apply (simp, simp)
-
-
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f' = f'a in cf2sfile_unlink)
-apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
-apply (simp add:current_files_unlink, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f' = f'a in cf2sfile_unlink)
-apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
-done
-
-lemma cf2sfiles_closefd:
-  "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (
-     case (file_of_proc_fd s p fd) of
-       Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and> 
-                    (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) 
-                 then (case (cf2sfile s f) of 
-                         Some sf \<Rightarrow> cf2sfiles s f' - {sf}
-                       | _       \<Rightarrow> {})
-                 else cf2sfiles s f'
-     | _       \<Rightarrow> cf2sfiles s f')"
-
-apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd")
-apply (simp_all add:current_files_simps split:if_splits)
-
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-
-apply (rule conjI, clarify, frule file_of_pfd_is_file, simp)
-apply (frule is_file_has_sfile', simp, erule exE, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp, erule conjE)
-apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd)
-apply (simp add:current_files_closefd same_inode_files_prop1, simp)
-apply (rule_tac x = f'a in bexI, simp, simp)
-apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
-apply (erule conjE|erule exE|erule bexE)+
-apply (case_tac "f'a = a", simp)
-apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp)
-apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (rule_tac x = f'a in bexI, simp, simp)
-
-apply (rule impI)+
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp, (erule conjE)+)
-apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (case_tac "f'a = a", simp)
-apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = f'' in bexI)
-apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (simp, simp, erule same_inode_files_prop4, simp)
-apply (rule_tac x = f'a in bexI)
-apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
-apply (simp, simp)
-
-apply (rule conjI, clarify)
-
-apply (rule impI)
-apply (case_tac "a \<in> files_hung_by_del s", simp_all)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
-apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
-apply (simp add:current_files_closefd, simp)
-apply (rule_tac x = f'a in bexI)
-apply (frule_tac f = f'a in cf2sfile_closefd)
-apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
-done
-
-lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other
-  cf2sfiles_unlink cf2sfiles_closefd
-  
-
-(* simpset for co2sobj *)
-
-lemma co2sobj_execve:
-  "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
-      if (obj = O_proc p)
-      then (case (cp2sproc (Execve p f fds # s) p) of
-              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))
-            | _       \<Rightarrow> None) 
-      else co2sobj s obj )"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (case_tac "cp2sproc (Execve p f fds # s) p")
-apply (drule current_proc_has_sp', simp, simp)
-apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
-apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
-apply (frule_tac ff = list in cf2sfile_other', simp_all)
-apply (simp add:is_dir_in_current)
-done
-
-lemma co2sobj_clone:
-  "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (
-      if (obj = O_proc p')
-      then (case (cp2sproc (Clone p p' fds shms # s) p') of
-              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
-            | _       \<Rightarrow> None)
-      else co2sobj s obj )"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
-apply (drule current_proc_has_sp', simp, simp)
-apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
-apply (rule conjI, rule impI, simp)
-apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)
-
-apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
-apply (frule_tac ff = list in cf2sfile_other', simp_all)
-apply (simp add:is_dir_in_current)
-done
-
-lemma co2sobj_ptrace:
-  "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
-     case obj of
-       O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'') 
-                     then (case (cp2sproc s p'') of 
-                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
-                           | _       \<Rightarrow> None)
-                     else if (info_flow_shm s p p'')
-                          then (case (cp2sproc s p'') of 
-                                  Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s))
-                                | _       \<Rightarrow> None)
-                          else co2sobj s (O_proc p'')
-    | _          \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)
-
-apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits
-  dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-
-apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
-apply (frule_tac ff = list in cf2sfile_other', simp_all)
-apply (simp add:is_dir_in_current)
-done
-
-lemma co2sobj_open:
-  "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk> 
-   \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of 
-     O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
-                  then (case (cf2sfile (Open p f flag fd opt # s) f) of
-                          Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
-                        | _       \<Rightarrow> None)
-                  else co2sobj s (O_file f')
-   | O_proc p' \<Rightarrow> if (p' = p) 
-                  then (case (cp2sproc (Open p f flag fd opt # s) p) of
-                          Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
-                        | _       \<Rightarrow> None)
-                  else co2sobj s (O_proc p')
-   | _         \<Rightarrow> co2sobj s obj )"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-
-apply (simp split:if_splits t_object.splits)
-apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+)
-apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f")
-apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)
-apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps)
-apply (simp add:tainted_eq_Tainted)
-apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current)
-apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits)
-
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (frule is_dir_in_current)
-apply (frule_tac f' = list in cf2sfile_open)
-apply (simp add:current_files_simps split:option.splits)
-apply (simp split:if_splits option.splits)
-done
-
-lemma co2sobj_readfile:
-  "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
-     case obj of
-       O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
-                       Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s)
-                                  then (case (cp2sproc s p') of
-                                          Some sp \<Rightarrow> Some (S_proc sp True)
-                                        | _       \<Rightarrow> None)
-                                  else co2sobj s obj)
-                    | _       \<Rightarrow> None)
-     | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps 
-             dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_writefile:
-  "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
-     case obj of
-       O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
-                       Some f \<Rightarrow> (if (f \<in> same_inode_files s f') 
-                                  then Some (S_file (cf2sfiles s f') 
-                                                    (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
-                                  else co2sobj s obj)
-                    | _       \<Rightarrow> None)
-     | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest:is_file_in_current is_dir_in_current)
-
-(* should delete has_same_inode !?!?*)
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
-
-lemma co2sobj_closefd:
-  "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
-      case obj of 
-        O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of 
-                        Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
-                                       f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f. 
-                                       f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-                                   then (case (cf2sfile s f, co2sobj s (O_file f')) of
-                                           (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
-                                         | _                              \<Rightarrow> None)
-                                   else co2sobj s obj)
-                     | _       \<Rightarrow> co2sobj s obj)
-      | O_proc p' \<Rightarrow> (if (p = p') 
-                      then (case (cp2sproc (CloseFd p fd # s) p) of
-                              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
-                            | _       \<Rightarrow> None)
-                      else co2sobj s obj)
-      | _         \<Rightarrow> co2sobj s obj) "
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-
-apply (frule is_file_in_current)
-apply (case_tac "file_of_proc_fd s p fd")
-apply (simp add:tainted_eq_Tainted)
-apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp)
-apply (frule_tac f' = list in cf2sfiles_closefd, simp)
-apply (simp add:is_file_simps current_files_simps)
-apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits
-  dest!:current_file_has_sfile' dest:hung_file_in_current)[1]
-
-apply (simp add:is_dir_simps, frule is_dir_in_current)
-apply (frule_tac f = list in cf2sfile_closefd)
-apply (clarsimp simp:current_files_closefd split:option.splits)
-apply (drule file_of_pfd_is_file', simp+)
-done
-
-lemma co2sobj_unlink:
-  "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
-      case obj of
-        O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
-                        (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-                     then (case (cf2sfile s f, co2sobj s (O_file f')) of
-                             (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
-                           | _                              \<Rightarrow> None)
-                     else co2sobj s obj
-      | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (frule is_file_in_current)
-apply (frule_tac f' = list in cf2sfile_unlink, simp)
-apply (frule_tac f' = list in cf2sfiles_unlink, simp)
-apply (simp add:is_file_simps current_files_simps)
-apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits
-  dest!:current_file_has_sfile')[1]
-
-apply (simp add:is_dir_simps, frule is_dir_in_current)
-apply (frule_tac f' = list in cf2sfile_unlink)
-apply (clarsimp simp:current_files_unlink split:option.splits)
-apply (drule file_dir_conflict, simp+)
-done
-
-lemma co2sobj_rmdir:
-  "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (simp add:is_file_simps dir_is_empty_def)
-apply (case_tac "f = list", drule file_dir_conflict, simp, simp)
-apply (simp add:cf2sfiles_other)
-apply (auto simp:cf2sfile_simps dest:is_dir_in_current)
-done
-
-lemma co2sobj_mkdir:
-  "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
-      if (obj = O_dir f) 
-      then (case (cf2sfile (Mkdir p f i # s) f) of 
-              Some sf \<Rightarrow> Some (S_dir sf)
-            | _       \<Rightarrow> None)
-      else co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (frule_tac cf2sfiles_other, simp+)
-apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir)
-apply (frule current_file_has_sfile, simp, erule exE, simp)
-apply (drule cf2sfile_mkdir1, simp+)
-done
-
-lemma same_inodes_Tainted:
-  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"
-apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
-apply (auto intro:has_same_inode_Tainted)
-done
-
-lemma co2sobj_linkhard:
-  "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> 
-   \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (
-    case obj of
-      O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
-                   then (case (cf2sfile (LinkHard p oldf f # s) f) of
-                           Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s))
-                         | _       \<Rightarrow> None)
-                   else co2sobj s obj
-    | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
-apply (frule_tac cf2sfiles_linkhard, simp+)
-apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard)
-apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted
-  split:option.splits if_splits dest:Tainted_in_current 
-  dest!:current_has_sec' current_file_has_sfile')[1]
-
-apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current)
-apply (frule is_dir_in_current)
-apply (frule current_file_has_sfile, simp)
-apply (drule cf2sfile_linkhard1, simp+)
-done
-
-lemma co2sobj_truncate:
-  "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
-      case obj of
-        O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
-                     then Some (S_file (cf2sfiles s f') (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
-                     else co2sobj s obj
-      | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest:is_file_in_current is_dir_in_current)
-
-(* should delete has_same_inode !?!?*)
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
-
-lemma co2sobj_kill:
-  "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_exit:
-  "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_createmsgq:
-  "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
-      case obj of
-        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of
-                                         Some sq \<Rightarrow> Some (S_msgq sq)
-                                       | _       \<Rightarrow> None)
-                     else co2sobj s obj
-      | _        \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest!:current_has_smsgq'
-             dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)
-done
-
-lemma co2sobj_sendmsg:
-  "\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (
-      case obj of
-        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of
-                                         Some sq \<Rightarrow> Some (S_msgq sq)
-                                       | _       \<Rightarrow> None)
-                     else co2sobj s obj
-      | _        \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest!:current_has_smsgq'
-             dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)
-done
-
-lemma co2sobj_recvmsg:
-  "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
-      case obj of
-        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
-                                         Some sq \<Rightarrow> Some (S_msgq sq)
-                                       | _       \<Rightarrow> None)
-                     else co2sobj s obj
-      | O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s)
-                     then (case (cp2sproc s p') of
-                             Some sp \<Rightarrow> Some (S_proc sp True)
-                           | _       \<Rightarrow> None)
-                     else co2sobj s obj
-      | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest!:current_has_smsgq'
-             dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)
-done
-
-lemma co2sobj_removemsgq:
-  "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk> 
-   \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6
-             dest!:current_has_smsgq'
-             dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)
-done
+(* simpset for s2ss*)
 
 lemma co2sobj_createshm:
-  "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = co2sobj s obj"
+  "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
+      case obj of 
+        O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
+                                        Some sh \<Rightarrow> Some (S_shm sh)
+                                      | _       \<Rightarrow> None)
+                    else co2sobj s obj
+      | _        \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
@@ -740,115 +25,6 @@
              dest:is_file_in_current is_dir_in_current)
 done
 
-lemma co2sobj_detach:
-  "\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
-      case obj of
-        O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of
-                                         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
-                                       | _       \<Rightarrow> None)
-                     else co2sobj s obj
-      | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
-                  same_inode_files_prop6 ch2sshm_simps
-             dest!:current_shm_has_sh'
-             dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_deleteshm:
-  "\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
-      case obj of
-        O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of
-                        Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s))
-                      | _       \<Rightarrow> None)
-      | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
-                  same_inode_files_prop6 ch2sshm_simps
-             dest!:current_shm_has_sh' 
-             dest:is_file_in_current is_dir_in_current)
-done
-
-lemma co2sobj_attach:
-  "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
-      case obj of
-        O_proc p' \<Rightarrow> if (p' = p)
-                     then (case (cp2sproc (Attach p h flag # s) p) of
-                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> 
-              (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)))
-                           | _       \<Rightarrow> None)
-                     else if (\<exists> flag'. (p', flag') \<in> procs_of_shm s h)
-                          then (case (cp2sproc s p') of 
-                                  Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or>
-              (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR)))
-                                | _       \<Rightarrow> None)
-                          else co2sobj s obj
-      | _         \<Rightarrow> co2sobj s obj)"
-apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-
-apply (rule conjI|rule impI|erule exE)+
-apply (simp split:option.splits)
-apply (rule impI, frule current_proc_has_sp, simp)
-apply ((erule exE)+, auto simp:cp2sproc_attach tainted_eq_Tainted)[1]
-apply (rule impI|rule conjI)+
-apply (subgoal_tac "p \<in> current_procs (Attach p h flag # s)")
-apply (drule_tac p = p in current_proc_has_sp, simp, erule exE)
-apply (auto simp:tainted_eq_Tainted)[1]
-apply (simp, rule impI)
-apply (subgoal_tac "nat \<in> current_procs (Attach p h flag # s)")
-apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)
-apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)
-apply (auto simp:cp2sproc_attach tainted_eq_Tainted)[1]
-apply simp
-
-apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 
-             simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
-                  same_inode_files_prop6 
-             dest:is_file_in_current is_dir_in_current)
-done
-
-
-lemma co2sobj_other:
-  "\<lbrakk>valid (e # s); alive (e # s) obj; 
-    \<forall> p f fds. e \<noteq> Execve p f fds;
-    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
-    \<forall> p p'. e \<noteq> Ptrace p p';
-    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
-    \<forall> p fd. e \<noteq> ReadFile p fd;
-    \<forall> p fd. e \<noteq> WriteFile p fd;
-    \<forall> p fd. e \<noteq> CloseFd p fd;
-    \<forall> p f. e \<noteq> UnLink p f;
-    \<forall> p f. e \<noteq> Rmdir p f;
-    \<forall> p f i. e \<noteq> Mkdir p f i;
-    \<forall> p f f'. e \<noteq> LinkHard p f f';
-    \<forall> p f len. e \<noteq> Truncate p f len;
-    \<forall> p q. e \<noteq> CreateMsgq p q;
-    \<forall> p q m. e \<noteq> SendMsg p q m;
-    \<forall> p q m. e \<noteq> RecvMsg p q m;
-    \<forall> p q. e \<noteq> RemoveMsgq p q;
-    \<forall> p h. e \<noteq> CreateShM p h;
-    \<forall> p h flag. e \<noteq> Attach p h flag;
-    \<forall> p h. e \<noteq> Detach p h;
-    \<forall> p h. e \<noteq> DeleteShM p h
-   \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
-apply (frule vt_grant, case_tac e)
-apply (auto intro:co2sobj_kill co2sobj_exit)
-done
-
-lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile
-  co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard
-  co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
-  co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm
-
-(* simpset for s2ss*)
-
 lemma s2ss_execve:
   "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
      if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
@@ -860,6 +36,32 @@
                               \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
            | _ \<Rightarrow> s2ss s) )"
 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)
+apply (rule conjI, rule impI, (erule exE|erule conjE)+)
+apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)
+apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp)
+apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)")
+apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)
+apply (erule exE, simp)
+apply (simp add:s2ss_def, rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits)
+
+apply (case_tac obj, simp_all add:co2sobj_execve alive_simps)
+thm alive_execve
+thm co2sobj_execve
+apply (simp add:co2sobj_execve, rule disjI2)
+apply (rule_tac x = obj in exI, simp split:t_object.splits)
+thm co2sobj_execve
+apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1]
+apply (simp add:co2sobj_execve)
+apply clarsimp
+thm current_proc_has_sp
+
+apply (auto simp:s2ss_def co2sobj_execve split:option.splits)
+
+
+
 apply (rule conjI, clarify)
 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)
 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE)