# HG changeset patch
# User chunhan
# Date 1380167401 -28800
# Node ID ed90f7d5e6d735087b1bf53aad3ee6eb4ea74c71
# Parent  68649272054c52f0a2afd217a44ba56f0c0d5472
200 loc to finish s2ss_unlink

diff -r 68649272054c -r ed90f7d5e6d7 S2ss_prop.thy
--- a/S2ss_prop.thy	Wed Sep 25 11:29:13 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 26 11:50:01 2013 +0800
@@ -1456,10 +1456,140 @@
                 simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1)
 done
 
+lemma alive_co2sobj_unlink:
+  "\<lbrakk>alive s obj; valid (UnLink p f # s); obj \<noteq> O_file f\<rbrakk>
+   \<Longrightarrow> alive (UnLink p f # s) obj"
+by (auto simp add:alive_simps split:t_object.splits)
+
+lemma s2ss_unlink:
+  "valid (UnLink p f # s) \<Longrightarrow> s2ss (UnLink p f # s) = (
+     if (proc_fd_of_file s f = {}) 
+     then (case (cf2sfile s f) of 
+             Some sf \<Rightarrow> del_s2ss_file s (s2ss s) f sf
+           | _       \<Rightarrow> {})
+     else s2ss s)"
+apply (frule vd_cons, frule vt_grant_os, clarsimp split:if_splits)
+apply (frule is_file_has_sfile', simp, erule exE, simp)
+apply (rule conjI, rule impI)
+apply (simp add:update_s2ss_sfile_def del_s2ss_file_def)
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:is_file_simps)
+apply simp
+apply (rule conjI)
+apply (rule_tac x = obj in exI,simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp, frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp)
+apply (frule_tac obj = obj in co2sobj_unlink, simp)
+apply (erule_tac x = fa in allE, simp add:is_file_simps)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (frule_tac alive_co2sobj_unlink, simp, simp)
+apply (frule_tac obj = obj in co2sobj_unlink, simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1)
+apply (simp add:co2sobj_unlink)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink is_file_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (tactic {*my_setiff_tac 1*})
+apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'a" in exI, simp add:is_file_simps)
+apply (frule_tac obj = "O_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop 
+  is_file_simps same_inode_files_prop11 split:if_splits)
+apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "f' = f", simp add:same_inode_files_prop9) 
+apply (case_tac "obj= O_file f")
+apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
+apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)
+apply (simp add:co2sobj.simps tainted_eq_Tainted is_file_simps cf2sfiles_prop same_inodes_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer
+
+apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps, simp)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1)
+apply (simp add:co2sobj_unlink)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink is_file_simps)
+apply (rule notI, simp add:co2sobj_unlink tainted_eq_Tainted)
+apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps tainted_eq_Tainted)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)
+apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop 
+  is_file_simps same_inode_files_prop11 split:if_splits)
+apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+
+
+
+
 
 
 
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
-  s2ss_readfile s2ss_writefile s2ss_closefd
+  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink