--- a/no_shm_selinux/Enrich.thy	Fri Dec 20 10:58:00 2013 +0800
+++ b/no_shm_selinux/Enrich.thy	Fri Dec 20 13:48:25 2013 +0800
@@ -27,8 +27,12 @@
      else Clone p p' fds # (enrich_proc s tp dp))"
 | "enrich_proc (Open p f flags fd opt # s) tp dp = (
      if (tp = p)
-     then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp)
+     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
      else Open p f flags fd opt # (enrich_proc s tp dp))"
+| "enrich_proc (ReadFile p fd # s) tp dp = (
+     if (tp = p) 
+     then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
+     else ReadFile p fd # (enrich_proc s tp dp))"
 | "enrich_proc (CloseFd p fd # s) tp dp = (
      if (tp = p \<and> fd \<in> proc_file_fds s p)
      then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
@@ -1356,34 +1360,47 @@
       apply (auto simp add:proc_file_fds_def)[1]
       apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def)
       done
-    moreover have "\<And>f flags fd inum.
-       \<lbrakk>valid (Open p f flags fd inum # enrich_proc s p p'); is_created_proc s p\<rbrakk>
-       \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd inum # Open p f flags fd inum # enrich_proc s p p')"
-      sorry
+    moreover have "\<And>f flags fd opt. \<lbrakk>valid (Open p f flags fd opt # enrich_proc s p p'); 
+      is_created_proc s p; valid (Open p f flags fd opt # s); p' \<notin> all_procs s\<rbrakk>
+       \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')"
+    proof-
+      fix f flags fd inum
+      assume a1: "valid (Open p f flags fd inum # enrich_proc s p p')" and a2: "is_created_proc s p"
+        and a3: "valid (Open p f flags fd inum # s)" and a4: "p' \<notin> all_procs s"
+      show "valid (Open p' f (remove_create_flag flags) fd inum # Open p f flags fd inum # enrich_proc s p p')"
+      proof (cases "
+        apply (rule_tac valid.intros(2))
+        apply (simp_all add:a1)
+
+
+
+
+
+      sorry 
     moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p; 
-      valid (CloseFd p fd # s); p' \<notin> all_procs s\<rbrakk>
-           \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
+      valid (CloseFd p fd # s); p' \<notin> all_procs s; fd \<in> proc_file_fds s p\<rbrakk>
+      \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
     proof-
       fix fd
       assume a1: "valid (CloseFd p fd # enrich_proc s p p')" and a2: "is_created_proc s p" 
         and a3: "p' \<notin> all_procs s" and a4: "valid (CloseFd p fd # s)"
+        and a5: "fd \<in> proc_file_fds s p"
       from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3)
       have "p' \<in> current_procs (enrich_proc s p p')" 
         using a2 a3 vd
         by (auto intro:enrich_proc_dup_in)
-      moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'"
+      moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'"      
+        using a5 a2 a3 vd pre'
+        apply (simp)
+        apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds)
+        apply (erule set_mp)
+        apply (simp add:enrich_proc_dup_ffds)
+        done
       ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
-        apply (rule valid.intros(2))
+        apply (rule_tac valid.intros(2))
         apply (simp_all add:a1 a0 a2 pre')
-      
-
-
-      sorry 
-(*
-       thus ?thesis using created_cons vd_cons all_procs_cons
-      apply (case_tac e)
-      apply (auto simp:is_created_proc_simps split:if_splits)
-        *)
+        done
+    qed
     ultimately show ?thesis using created_cons vd_cons all_procs_cons
       apply (case_tac e)
       apply (auto simp:is_created_proc_simps split:if_splits)