diff -r e79e3a8a4ceb -r cebdef333899 no_shm_selinux/Enrich2.thy
--- a/no_shm_selinux/Enrich2.thy	Thu Dec 26 10:56:50 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Mon Dec 30 12:01:09 2013 +0800
@@ -5,6 +5,15 @@
 
 context tainting_s begin
 
+(* \<And> *)
+lemma current_proc_fds_in_curp:
+  "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:init_fds_of_proc_prop1)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto split:if_splits option.splits)
+done
+
 lemma get_parentfs_ctxts_prop:
   "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk>
    \<Longrightarrow> ctxt \<in> set (ctxts)"
@@ -35,19 +44,195 @@
 apply (simp add:parentf_is_dir_prop2)
 done
 
+lemma enrich_proc_dup_ffds':
+  "\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
+apply (auto simp:enrich_proc_dup_ffds_eq_fds)
+apply (simp add:proc_file_fds_def)
+done
+
+lemma enrich_proc_cur_inof:
+  "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
+apply (induct s arbitrary:f)
+apply simp
+apply (frule vd_cons, frule vt_grant_os, frule vt_grant)
+apply (case_tac a, auto)
+apply (auto split:option.splits simp del:grant.simps)
+done
+
+lemma not_all_procs_sock:
+  "\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
+apply (frule not_all_procs_prop3)
+apply (case_tac "inum_of_socket s (p', fd)", simp_all)
+apply (drule cn_in_curp', simp+)
+done
+
+lemma enrich_proc_cur_inos:
+  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
+   \<Longrightarrow> inum_of_socket (enrich_proc s p p') (tp, fd) = inum_of_socket s (tp, fd)"
+apply (induct s arbitrary:tp)
+apply simp
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:option.splits simp:not_all_procs_sock)
+apply (simp add:proc_file_fds_def, erule exE)
+apply (case_tac "inum_of_socket s (nat1, fd)", simp_all)
+apply (drule filefd_socket_conflict, simp_all add:current_sockets_def)
+done
+
+lemma enrich_proc_cur_inums:
+  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_inode_nums (enrich_proc s p p') = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_file_inums_def 
+  current_sock_inums_def enrich_proc_cur_inof enrich_proc_cur_inos)
+done
+
+lemma enrich_proc_cur_itag:
+  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
+   \<Longrightarrow> itag_of_inum (enrich_proc s p p') i = itag_of_inum s i"
+apply (induct s)
+apply simp
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:option.splits t_socket_type.splits)
+done
+
+lemma enrich_proc_cur_tcps:
+  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
+   \<Longrightarrow> is_tcp_sock (enrich_proc s p p') = is_tcp_sock s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_tcp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_proc_cur_udps:
+  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
+   \<Longrightarrow> is_udp_sock (enrich_proc s p p') = is_udp_sock s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_proc_cur_msgqs:
+  "valid s \<Longrightarrow> current_msgqs (enrich_proc s p p') = current_msgqs s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+
+lemma enrich_proc_cur_msgs:
+  "valid s \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q "
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+
+lemma enrich_proc_cur_procs:
+  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk> 
+   \<Longrightarrow> current_procs (enrich_proc s p p') = current_procs s \<union> {p'}"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_simps)
+done
+
+lemma enrich_proc_cur_files:
+  "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
+apply (auto simp:current_files_def)
+apply (simp add: enrich_proc_cur_inof)+
+done
+
+lemma enrich_proc_cur_fds1:
+  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<in> current_procs s\<rbrakk>
+   \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps)
+done
+
+lemma enrich_proc_cur_fds1':
+  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<noteq> p'\<rbrakk>
+   \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps)
+done
+
+lemma enrich_proc_cur_fds:
+  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
+   \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = (if (tp = p') then proc_file_fds s p else current_proc_fds s tp)"
+apply (simp add:enrich_proc_cur_fds1' enrich_proc_dup_ffds_eq_fds split:if_splits)
+done
+
+lemma enrich_proc_not_alive:
+  "\<lbrakk>enrich_not_alive s (E_proc p') obj; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+  \<Longrightarrow> enrich_not_alive (enrich_proc s p p') (E_proc p') obj"
+apply (case_tac obj)
+apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
+  enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
+done
+
+lemma enrich_proc_filefd:
+  "\<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
+apply (induct s arbitrary:tp, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs split:if_splits)
+done
+
+lemma enrich_proc_flagfd:
+  "\<lbrakk>flags_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+  \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some f"
+apply (induct s arbitrary:tp, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs current_fflag_has_ffd split:if_splits option.splits)
+done
+
+lemma enrich_proc_hungs:
+  "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:files_hung_by_del.simps)
+done
+
+lemma enrich_proc_is_file:
+  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
+   \<Longrightarrow> is_file (enrich_proc s p p') = is_file s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_file_def enrich_proc_cur_itag enrich_proc_cur_inof
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_proc_is_dir:
+  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
+   \<Longrightarrow> is_dir (enrich_proc s p p') = is_dir s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_dir_def enrich_proc_cur_itag enrich_proc_cur_inof
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_proc_alive:
+  "\<lbrakk>alive s obj; valid s; is_created_proc s p; p' \<notin> all_procs s; no_del_event s\<rbrakk>
+   \<Longrightarrow> alive (enrich_proc s p p') obj"
+apply (case_tac obj)
+apply (simp_all add:enrich_proc_is_file enrich_proc_is_dir enrich_proc_cur_msgqs 
+  enrich_proc_cur_msgs enrich_proc_cur_procs enrich_proc_cur_fds
+  enrich_proc_cur_tcps enrich_proc_cur_udps)
+apply (rule impI, simp)
+apply (drule current_proc_fds_in_curp, simp, simp add:not_all_procs_prop3)
+done
+
 lemma enrich_proc_prop:
-  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
+  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s; no_del_event s\<rbrakk>
    \<Longrightarrow> valid (enrich_proc s p p') \<and> 
-       (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> 
-       (\<forall> obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and>
-       (files_hung_by_del (enrich_proc s p p') = files_hung_by_del s) \<and> 
        (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
        (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> 
        (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> 
-       (\<forall> tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and>
-       (\<forall> tp fd flags. flags_of_proc_fd s tp fd = Some flags \<longrightarrow> 
-                      flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and>
-       (\<forall> q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and>
        (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>
        (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
        (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
@@ -58,41 +243,34 @@
   case (Cons e s)
   hence vd_cons': "valid (e # s)" and created_cons: "is_created_proc (e # s) p"
     and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" 
-    and os: "os_grant s e" and grant: "grant s e"
+    and os: "os_grant s e" and grant: "grant s e" 
+    and nodel_cons: "no_del_event (e # s)"
     by (auto dest:vd_cons' vt_grant_os vt_grant)
   from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto)
+  from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto)
   from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and>
-     (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and>
-     (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and>
-     files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and>
      (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
      (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
      (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and>
-     (\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and>
-     (\<forall>tp fd flags.
-         flags_of_proc_fd s tp fd = Some flags \<longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and>
-     (\<forall>q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and>
      (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>     
      (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
      (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
-    using vd all_procs by auto
-  have alive_pre: "is_created_proc s p \<Longrightarrow> (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj)"
-    using pre by simp
-  hence curf_pre: "is_created_proc s p \<Longrightarrow> (\<forall>f. f \<in> current_files s \<longrightarrow> f \<in> current_files (enrich_proc s p p'))"
-    using vd apply auto
-    apply (drule is_file_or_dir, simp)
-    apply (erule disjE)
-    apply (erule_tac x = "O_file f" in allE, simp add:is_file_in_current)
-    apply (erule_tac x = "O_dir f" in allE, simp add:is_dir_in_current)
-    done
+    using vd all_procs nodel by auto
   have vd_enrich_cons: "valid (enrich_proc (e # s) p p')"
   proof-
     from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
     have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" 
       apply (frule pre')
-      apply (erule_tac s = s in enrich_valid_intro_cons)
-      apply (simp_all add:os grant vd pre)
-      done  
+      apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)
+      apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
+      apply (clarsimp simp:enrich_proc_alive nodel all_procs vd)
+      apply (rule allI, rule impI, erule enrich_proc_not_alive)
+      apply (simp_all add:nodel all_procs vd enrich_proc_hungs enrich_proc_cur_msgs)
+      apply ((rule allI| rule impI)+, erule enrich_proc_filefd)
+      apply (simp_all add:nodel all_procs vd)
+      apply ((rule allI| rule impI)+, erule enrich_proc_flagfd)
+      apply (simp_all add:nodel all_procs vd)
+      done
     moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p; 
       valid (Execve p f fds # s); p' \<notin> all_procs s\<rbrakk>
       \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
@@ -103,25 +281,18 @@
       have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
         and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
         and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
-        and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> 
-                                   file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
         and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
         and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
-        using pre a2 by auto
+        using pre a2
+        by auto
       show "valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
       proof-
         from a0 a3 have a0': "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3)
         from a3 have grant: "grant s (Execve p f fds)" and os: "os_grant s (Execve p f fds)"
           by (auto dest:vt_grant_os vt_grant simp del:os_grant.simps)
-        have f_in: "is_file (enrich_proc s p p') f" 
-        proof-
-          from pre a2
-          have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
-            by (auto)
-          show ?thesis using a3 a4
-            apply (erule_tac x = "O_file f" in allE)
-            by (auto dest:vt_grant_os)
-        qed
+        have f_in: "is_file (enrich_proc s p p') f"
+          using vd nodel os all_procs
+          by (auto dest:vt_grant_os simp:enrich_proc_is_file)
         moreover have a5: "proc_file_fds s p \<subseteq> proc_file_fds (Execve p f fds # enrich_proc s p p') p'" 
           using a3 a0'
           apply (frule_tac vt_grant_os)
@@ -174,7 +345,8 @@
             apply (simp_all add:is_file_simps)
             apply (rule allI, rule impI, erule_tac x = fa in allE, simp)
             apply (drule_tac ff = fa in cf2sfile_other')
-            by (auto simp:a2 curf_pre)
+            apply (auto simp:a2 enrich_proc_cur_files nodel)
+            done
           ultimately show ?thesis 
             using p1' p2' p3
             apply (simp split:option.splits)
@@ -204,8 +376,6 @@
       have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
         and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
         and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
-        and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> 
-                                   file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
         and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
         and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
         using pre a2 by auto
@@ -218,7 +388,7 @@
         using a1 a3
         by (auto simp:is_file_open dest:vt_grant_os)
       have a7: "fd \<notin> current_proc_fds (enrich_proc s p p') p'"
-        using a2 a4 vd
+        using a2 a4 vd nodel
         apply (simp add:enrich_proc_dup_ffds_eq_fds)
         apply (rule notI)
         apply (drule_tac p = p in file_fds_subset_pfds)
@@ -233,15 +403,9 @@
       show "valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')"
       proof (cases opt)
         case None
-        have f_in: "is_file (enrich_proc s p p') f" 
-        proof-
-          from pre a2
-          have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
-            by (auto)
-          show ?thesis using a3 a4 None
-            apply (erule_tac x = "O_file f" in allE)
-            by (auto dest:vt_grant_os)
-        qed
+        have f_in: "is_file (enrich_proc s p p') f"
+          using vd nodel os all_procs None
+          by (auto dest:vt_grant_os simp:enrich_proc_is_file) 
         from grant None obtain up rp tp uf rf tf 
           where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"
           and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 
@@ -338,7 +502,7 @@
             apply simp
             apply (drule_tac f' = fa in cf2sfile_open)
             apply (simp add:current_files_simps)
-            using curf_pre a2
+            using enrich_proc_cur_files a2 nodel
             apply simp
             apply simp
             using cf2sf
@@ -379,7 +543,7 @@
         using a2 a3 vd
         by (auto intro:enrich_proc_dup_in)
       moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'"      
-        using a5 a2 a3 vd pre'
+        using a5 a2 a3 vd pre' nodel
         apply (simp)
         apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds)
         apply (erule set_mp)
@@ -402,8 +566,6 @@
       have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
         and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
         and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
-        and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> 
-                                   file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
         and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
         and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
         using pre a2 by auto
@@ -411,12 +573,12 @@
       show "valid (ReadFile p' fd # ReadFile p fd # enrich_proc s p p')"
       proof-
         have "os_grant (ReadFile p fd # enrich_proc s p p') (ReadFile p' fd)"
-          using a1 a2 a4 vd os
+          using a1 a2 a4 vd os nodel
           apply (clarsimp simp:current_files_simps enrich_proc_dup_in enrich_proc_dup_ffds_eq_fds)
           apply (simp add:proc_file_fds_def)
           apply (rule conjI)
           apply (rule_tac x = f in exI, simp add:enrich_proc_dup_ffd)
-          using curf_pre
+          using enrich_proc_cur_files
           apply (simp)
           apply (drule enrich_proc_dup_fflags)
           apply simp_all
@@ -435,10 +597,9 @@
             by auto
           from os have f_in_s: "f \<in> current_files s" using p1 by simp
           from p1 vd have isfile_s: "is_file s f" by (erule_tac file_of_pfd_is_file, simp)
-          with alive_pre a2 have isfile_s': "is_file (enrich_proc s p p') f"
-            apply simp
-            apply (erule_tac x = "O_file f" in allE, simp)
-            done          
+          hence isfile_s': "is_file (enrich_proc s p p') f"
+            using vd nodel all_procs a2
+            by (auto simp:enrich_proc_is_file) 
           from p0 obtain flag' where p0': "flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag'"
             and p0'': "(flag' = flag) \<or> (flag' = remove_create_flag flag)"
             using a2 a4 vd
@@ -487,79 +648,89 @@
       apply (auto simp:is_created_proc_simps split:if_splits)
       done
   qed
-  moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj"
+  moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> 
+    cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
   proof clarify
-    fix obj
-    assume a0: "alive (e # s) obj"
-    have a1: "is_created_proc s p \<Longrightarrow> \<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
-      using pre by auto
-    show "alive (enrich_proc (e # s) p p') obj" (*
-    proof (cases e)
-      case (Execve tp f fds)
-      with created_cons a1
-      have b1: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" 
-        by (auto simp:is_created_proc_simps)
+    fix tp fd 
+    assume a1: "fd \<in> proc_file_fds (e # s) tp"
+    from a1 obtain f where a1': "file_of_proc_fd (e # s) tp fd = Some f" 
+      by (auto simp:proc_file_fds_def)
+    from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; is_created_proc s p\<rbrakk> \<Longrightarrow>
+      cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by auto
+    hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p\<rbrakk> \<Longrightarrow>
+      cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
+    hence pre_sfd'': "\<And> tp fd f proc. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p = proc\<rbrakk> \<Longrightarrow>
+      cfd2sfd (enrich_proc s proc p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
+    from a1' all_procs_cons vd_cons' have a2: "tp \<noteq> p'"
+      apply (drule_tac not_all_procs_prop3)
+      apply (drule proc_fd_in_procs, simp)
+      by (rule notI, simp)
+    have a3: "p' \<noteq> p" using all_procs_cons created_cons
+      apply (drule_tac not_all_procs_prop3)
+      apply (rule notI, simp add:is_created_proc_def)
+      done      
+    have a4: "file_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some f" 
+      using a1' nodel_cons all_procs_cons a1' created_cons vd_cons'
+      apply (frule_tac enrich_proc_filefd, simp_all)
+      done
+    show "cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+    proof-
+      have b1: "\<And> proc f' fds. e = Execve proc f' fds
+        \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+        using a4 vd_enrich_cons a1' vd_cons' created_cons
+        apply (simp split:if_splits del:file_of_proc_fd.simps add:a2) 
+        apply (simp only:cfd2sfd_execve)
+        apply (drule_tac s = "Execve proc f' fds # enrich_proc s proc p'" in vd_cons)
+        apply (simp split:if_splits add:a2)
+        apply (drule_tac p' = proc and fd' = fd and s = "enrich_proc s proc p'" in cfd2sfd_execve, simp+)
+        apply (erule_tac pre_sfd'', simp add:is_created_proc_simps, simp)
+        apply (drule_tac p' = tp and fd' = fd in cfd2sfd_execve, simp+)
+        apply (erule_tac pre_sfd'', simp add:is_created_proc_simps, simp)
+        apply (simp only:cfd2sfd_execve)
+        apply (rule_tac pre_sfd')
+        apply (auto split:if_splits simp:is_created_proc_simps)
+        done 
+      have b2: "\<And> proc proc' fds. e = Clone proc proc' fds
+       \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+        using a4 vd_enrich_cons a1' vd_cons' created_cons
+        apply (simp split:if_splits del:file_of_proc_fd.simps) 
+        apply (simp add:cfd2sfd_clone add:a2)
+        apply (simp add:cfd2sfd_clone split:if_splits)
+        apply (erule pre_sfd'', simp add:is_created_proc_simps, simp)
+        apply (erule pre_sfd', simp add:is_created_proc_simps)
+        done 
+      have b3: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 
+         \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+        apply (simp split:if_splits)
+        thm cfd2sfd_open
+        sorry
+      have b4: "\<And> proc fd'. e = ReadFile proc fd' 
+         \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+        using a4 vd_enrich_cons a1' vd_cons' created_cons
+        apply (simp split:if_splits del:file_of_proc_fd.simps) 
+        apply (frule_tac s = "ReadFile proc fd' # enrich_proc s proc p'" in vd_cons)
+        apply (simp add:cfd2sfd_other)
+        apply (erule pre_sfd'', simp add:is_created_proc_simps, simp)
+        apply (simp add:cfd2sfd_other)
+        apply (erule pre_sfd', simp add:is_created_proc_simps)
+        done 
       show ?thesis
-        using created_cons all_procs_cons vd_enrich_cons Execve b1 os a0
-        apply (simp add:alive_execve split:if_splits)
-        apply (frule_tac vd_cons) defer
-        apply (frule_tac vd_cons)
-        using vd_cons' Execve vd os
-        apply (auto simp:is_file_simps is_dir_simps is_created_proc_simps alive.simps
-          split:t_object.splits if_splits 
-          dest:set_mp file_fds_subset_pfds)
-        apply (erule_tac x = "O_proc nat" in allE, simp)
-        apply (erule_tac x = "O_file list" in allE, simp)
-        apply (drule set_mp, simp)
-        apply (drule_tac s = s and p = tp in file_fds_subset_pfds)
-        apply (erule_tac x = "O_fd tp nat2" in allE, simp)
-        apply (auto)[1]
-        apply (erule_tac x = "O_fd nat1 nat2" in allE, auto dest:set_mp file_fds_subset_pfds)[1]
-        apply (erule_tac x = "O_dir list" in allE, simp)
-    sorry
-  show ?thesis *) sorry
-  moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj"
-    thm enrich_not_alive.simps
-    sorry
-  moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)"
-  proof-
-    have "is_created_proc s p \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
-      and ffd_remain: "is_created_proc s p \<Longrightarrow> 
-      \<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> 
-                                   file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
-      using pre by auto
-    with created_cons all_procs_cons os vd_cons' vd
-    show ?thesis
-      apply (frule_tac not_all_procs_prop3)
-      apply (case_tac e)
-      apply (auto simp:files_hung_by_del.simps is_created_proc_simps)
-      apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def procfd_of_file_eq_fpfd''
-        dest:procfd_of_file_imp_fpfd procfd_of_file_imp_fpfd' procfd_of_file_non_empty
-      )
-      apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def split:if_splits)[1]
-      
-      apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def files_hung_by_del.simps
-        split:option.splits)[1]
-      apply (auto split:option.splits)[1]
-      thm is_created_proc_simps
-    sorry
+        apply (case_tac e)
+        apply (erule b1, erule b2) 
+        prefer 4 apply (erule b3) prefer 4 apply (erule b4)
+        using vd created_cons nodel_cons a1' a4 vd_enrich_cons vd_cons'
+        apply (auto intro!:pre_sfd' simp:cfd2sfd_simps is_created_proc_simps 
+          simp del:file_of_proc_fd.simps split:if_splits dest:vd_cons enrich_proc_filefd)
+        apply (simp_all)
+        done
+    qed
+  qed
   moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
     sorry
   moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
     sorry
   moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
     sorry
-  moreover have "\<forall>tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<longrightarrow> 
-    file_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some f"
-    sorry
-  moreover have "\<forall>tp fd flags. flags_of_proc_fd (e # s) tp fd = Some flags \<longrightarrow>
-        flags_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some flags"
-    sorry
-  moreover have "\<forall>q. msgs_of_queue (enrich_proc (e # s) p p') q = msgs_of_queue (e # s) q"
-    sorry 
-  moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> 
-    cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
-    sorry 
   moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"
   proof-
     from pre have b0: "is_created_proc s p \<Longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p" by simp
@@ -574,14 +745,26 @@
       show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p"
       proof (cases "tp = p")
         case True
-        show ?thesis using True a1 a2 a3 a4 b0
+        show ?thesis using True a1 a2 a3 a4 b0 vd
           thm not_all_procs_prop3
           apply (frule_tac not_all_procs_prop2)
           apply (frule not_all_procs_prop3)
-          apply (auto simp add:cp2sproc_execve is_created_proc_def split:option.splits dest!:current_has_sec' 
-            dest:vt_grant_os)
+          apply (simp add:is_created_proc_simps)
+          apply (frule vd_cons) (*
+          apply (frule_tac vt_grant_os) 
+          apply (frule_tac \<tau> = "enrich_proc s p p'" in vt_grant_os) *)
+          apply (frule_tac s = "enrich_proc s p p'" in vd_cons)
+          apply (frule_tac \<tau> = s in vt_grant_os)
+          apply (case_tac "p' = p", simp) (*
+          apply (auto simp add:cp2sproc_execve sectxt_of_obj_simps enrich_proc_dup_in
+            split:option.splits dest!:current_has_sec' dest:vt_grant is_file)
+          apply (simp_all add:is_created_proc_def)
+          apply (auto simp:cp2sproc_def)
+          apply (simp_all add:enrich_proc_dup_in)
+
+          
           apply (auto simp:sectxt_of_obj_simps split:option.splits dest:valid.cases)
-          
+  *)        
           sorry
       next
         case False
@@ -604,7 +787,8 @@
       sorry
     show ?thesis using vd_enrich_cons
       apply (case_tac e)
-      apply (simp_all only:b1 b2 b3 b4 b5 b6 b7)
+      using vd_cons' created_cons all_procs_cons
+      apply (auto intro!:b1 b2 b3 b4 b5 b6 b7 simp del:enrich_proc.simps)
       using created_cons vd_enrich_cons vd_cons' b0
       apply (auto simp:cp2sproc_other is_created_proc_def)
       done
@@ -612,7 +796,7 @@
   moreover have "\<forall> fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> 
     cfd2sfd (enrich_proc (e # s) p p') p' fd = cfd2sfd (e # s) p fd"
     sorry
-  ultimately show ?case
+  ultimately show ?case using vd_enrich_cons
     by simp
 qed
   
@@ -624,8 +808,6 @@
 lemma enrich_proc_valid:
   "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> " 
 
- 
-
 lemma enrich_proc_tainted: 
   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
    \<Longrightarrow> tainted (enrich_proc s p p') = (if (O_proc p \<in> tainted s) 
@@ -669,7 +851,7 @@
 
 
 lemma enrich_proc_tainted:
-  ""
+
 
 
 end