--- a/no_shm_selinux/Enrich2.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -5,12 +5,37 @@
 
 context tainting_s begin
 
-fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)"
+fun new_cf :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file \<Rightarrow> t_file"
+where
+  "new_cf s fs []     = []"
+| "new_cf s fs (f#pf) = new_childf_general pf s fs"
+
+fun enrich_dufs:: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_file) list"
 where
-  "enrich_file [] tf s = ({}, [])"
-| "enrich_file (Open p f flags fd (Some inum) # s) tf s =
-  "
-    
+  "enrich_dufs [] tf s = []"
+| "enrich_dufs (Open p f flags fd (Some inum) # s) tf s' = 
+    (if (f \<in> same_inode_files s' tf) 
+     then [(f, new_cf s' {} f)]
+     else enrich_dufs s tf s')"
+| "enrich_dufs (LinkHard p f f' # s) tf s' = 
+    (if (f' \<in> same_inode_files s' tf) 
+     then (f', new_cf s' (set (map snd (enrich_dufs s tf s'))) f') # enrich_dufs s tf s'
+     else enrich_dufs s tf s')"
+| "enrich_dufs (_ # s) tf s' = enrich_dufs s tf s'"
+
+lemma enrich_dufs_sameinodes:
+  "valid s \<Longrightarrow> set (map snd (enrich_dufs s f s)) = same_inode_files s f"
+thm enrich_dufs.induct
+apply (induct rule:enrich_dufs.induct)
+
+apply (erule enrich_dufs.induct)
+
+fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_inode_num \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)"
+where
+  "enrich_file [] tf ninum s = ({}, [])"
+| "enrich_file (Open p f flags fd (Some inum) # s) tf ninum s = 
+     if (f \<in> same_inode_fies s tf)
+     then Open p f flags fd (Some"