diff -r e7f850d1e08e -r f2e620d799cf S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Aug 29 13:29:32 2013 +0800
+++ b/S2ss_prop.thy	Sat Aug 31 00:35:36 2013 +0800
@@ -6,9 +6,243 @@
 
 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
+
+(* 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 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_simps same_inode_files_simps current_files_simps
+  split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1)
+apply (simp add:cf2sfiles_def)
+
+lemma cf2sfiles_unlink:
+
+lemma cf2sfiles_closefd:
+
+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 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 (rule impI, simp add:cf2sfiles_def) defer
+
+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
+
+end
+
 (* 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))
-     then (case (cp2sproc (Execve p f fds # s)  s2ss s \<union> {} "
\ No newline at end of file
+     then (case (cp2sproc (Execve p f fds # s) p) of
+             Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
+           | _ \<Rightarrow> s2ss s)
+     else (case (cp2sproc (Execve p f fds # s) p) of
+             Some sp \<Rightarrow> s2ss s - {S_proc sp (O_proc p \<in> Tainted s)}
+                              \<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, 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)
+apply (simp, (erule conjE)+)
+apply (split option.splits, rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
+apply (rule allI, rule impI)
+apply (rule set_eqI, rule iffI)
+
+apply (simp split:option.splits)
+apply (frule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp)
+thm current_proc_has_sp
+
+
+apply (simp split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
+apply (simp add:s2ss_def)
+apply (rule allI|rule impI)+
+apply (rule set_eqI, rule iffI)
+apply (auto simp:alive_simps)
+apply (case_tac obj, auto split:option.splits simp:cp2sproc_execve)
+apply (auto split:if_splits)
\ No newline at end of file