diff -r b718662f61fa -r ec73b98d4a64 S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Sep 26 12:54:52 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 26 22:08:32 2013 +0800
@@ -1720,11 +1720,124 @@
 apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
 done
 
+lemma s2ss_mkdir: "valid (Mkdir p f inum # s) \<Longrightarrow> s2ss (Mkdir p f inum # s) = (
+  case (cf2sfile (Mkdir p f inum # s) f) of
+    Some sf \<Rightarrow> (s2ss s) \<union> {S_dir sf}
+  | _       \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons, clarsimp)
+apply (case_tac "cf2sfile (Mkdir p f inum # s) f")
+apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)
 
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*}, simp)
+apply (case_tac "obj = O_dir f")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_simps)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (rule_tac x = "O_dir f" in exI, simp add:alive_mkdir co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_dir f", simp add:is_dir_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)
+done
+
+definition update_s2ss_sfile_link:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where
+ "update_s2ss_sfile_link s ss f sf \<equiv>
+    if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
+       then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}
+       else ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)} 
+               \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}"
+
+lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (
+  case (cf2sfile (LinkHard p f f' # s) f') of
+    Some sf \<Rightarrow> update_s2ss_sfile_link s (s2ss s) f sf
+  | _       \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons, clarsimp)
+apply (split option.splits)
+apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)
+apply (rule allI, rule impI)
 
+apply (simp add:update_s2ss_sfile_link_def)
+apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f'")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
+  same_inode_files_linkhard split:if_splits)
+apply (case_tac "O_file f' \<in> Tainted s")
+apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted 
+  same_inodes_Tainted split:if_splits)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
+apply (simp add:alive_linkhard)
+apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'a" in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule conjI, rule impI, simp add:is_file_in_current)
+apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f'", simp)
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
+  same_inode_files_linkhard split:if_splits)
+apply (case_tac "O_file f' \<in> Tainted s")
+apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)
+apply (erule_tac obj = obj in co2sobj_some_caseD, simp)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_linkhard alive_linkhard)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted 
+  same_inodes_Tainted split:if_splits)
+apply (simp, rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)
+apply (erule_tac x = fa in allE, rule notI)
+apply (simp add:co2sobj_linkhard is_file_simps)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (frule_tac obj = "O_file f" in co2sobj_linkhard)
+apply (simp add:alive_linkhard)
+apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
+done
 
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
-  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir
+  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
+  s2ss