# HG changeset patch
# User chunhan
# Date 1389020871 -28800
# Node ID ded3f83f6cb97c1095fa8c83232c834e5d20defd
# Parent  e832378a2ff2d42d61f7e354746b9f505cdc071e
make clear of Indexing-objects and enrich-objects

diff -r e832378a2ff2 -r ded3f83f6cb9 no_shm_selinux/Enrich.thy
--- a/no_shm_selinux/Enrich.thy	Wed Jan 01 23:00:24 2014 +0800
+++ b/no_shm_selinux/Enrich.thy	Mon Jan 06 23:07:51 2014 +0800
@@ -3,14 +3,28 @@
  Temp
 begin
 
-(* objects that need dynamic indexing, all nature-numbers *)
+(* enriched objects, closely related to static objects, so are only 3 kinds *)
 datatype t_enrich_obj = 
-  E_proc "t_process"
-| E_file "t_file"
-| E_fd   "t_process" "t_fd"
-| E_inum "nat"
+  E_proc "t_process" "t_msgq" "t_msgq"
+| E_file_link "t_file"
+| E_file "t_file" "nat" 
+ (*
+| E_fd   "t_process" "t_fd" 
+| E_inum "nat" *)
 | E_msgq "t_msgq"
+(*
 | E_msg  "t_msgq"    "t_msg"
+*)
+
+
+(* objects that need dynamic indexing, all nature-numbers *)
+datatype t_index_obj = 
+  I_proc "t_process" 
+| I_file "t_file"
+| I_fd   "t_process" "t_fd"
+| I_inum "nat"
+| I_msgq "t_msgq"
+| I_msg  "t_msgq"    "t_msg"
 
 context tainting_s begin
 
@@ -73,6 +87,7 @@
 | "all_files (LinkHard p f f' # s) = all_files s \<union> {f'}"
 | "all_files (e # s) = all_files s"
 
+(*
 fun notin_all:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
 where
   "notin_all s (E_proc p)  = (p \<notin> all_procs s)"
@@ -81,6 +96,37 @@
 | "notin_all s (E_inum i)  = (i \<notin> all_inums s)"
 | "notin_all s (E_msgq q)  = (q \<notin> all_msgqs s)"
 | "notin_all s (E_msg q m) = (m \<notin> all_msgs s q)"
+*)
+
+fun nums_of_recvmsg:: "t_state \<Rightarrow> t_process \<Rightarrow> nat"
+where
+  "nums_of_recvmsg [] p' = 0"
+| "nums_of_recvmsg (RecvMsg p q m # s) p' = 
+     (if p' = p then Suc (nums_of_recvmsg s p) else nums_of_recvmsg s p')"
+| "nums_of_recvmsg (e # s) p' = nums_of_recvmsg s p'"
+
+lemma nums_of_recv_0:
+  "\<lbrakk>p \<notin> current_procs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> nums_of_recvmsg s p = 0"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto)
+done
+
+lemma new_msgq_1:
+  "\<lbrakk>new_msgq s \<le> q; q \<le> new_msgq s - Suc 0\<rbrakk> \<Longrightarrow> False"
+apply (subgoal_tac "new_msgq s \<noteq> 0")
+apply (simp, simp add:new_msgq_def next_nat_def)
+done
+
+fun notin_cur:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
+where
+  "notin_cur s (E_proc p qmin qmax)  = 
+    (p \<notin> current_procs s \<and> qmin = new_msgq s \<and> qmax = new_msgq s + (nums_of_recvmsg s p) - 1)"
+| "notin_cur s (E_file f inum)  = 
+    (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf) \<and> inum \<notin> current_inode_nums s)"
+| "notin_cur s (E_file_link f)  = 
+    (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))"
+| "notin_cur s (E_msgq q)  = (q \<notin> current_msgqs s)"
 
 lemma not_all_procs_cons:
   "p \<notin> all_procs (e # s) \<Longrightarrow> p \<notin> all_procs s"
@@ -118,17 +164,24 @@
   "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s"
 apply (induct s, simp)
 by (case_tac a, auto)
-
-fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
+  
+fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_index_obj \<Rightarrow> bool"
 where
-  "enrich_not_alive s obj (E_file f)  = (f \<notin> current_files s \<and> obj \<noteq> E_file f)"
-| "enrich_not_alive s obj (E_proc p)  = (p \<notin> current_procs s \<and> obj \<noteq> E_proc p)"
-| "enrich_not_alive s obj (E_fd p fd) = 
-  ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> obj \<noteq> E_fd p fd \<and> obj \<noteq> E_proc p)"
-| "enrich_not_alive s obj (E_msgq q)  = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q)"
-| "enrich_not_alive s obj (E_inum i)  = (i \<notin> current_inode_nums s \<and> obj \<noteq> E_inum i)"
-| "enrich_not_alive s obj (E_msg q m) = 
-  ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msg q m \<and> obj \<noteq> E_msgq q)"
+  "enrich_not_alive s obj (I_file f)  = 
+  (f \<notin> current_files s \<and> (\<forall> inum. obj \<noteq> E_file f inum) \<and> obj \<noteq> E_file_link f)"
+| "enrich_not_alive s obj (I_proc p)  = (p \<notin> current_procs s \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))"
+| "enrich_not_alive s obj (I_fd p fd) = 
+  ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))"
+| "enrich_not_alive s obj (I_msgq q)  = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q \<and> 
+     (case obj of
+        E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax)
+      | _        \<Rightarrow> True) )"
+| "enrich_not_alive s obj (I_inum i)  = (i \<notin> current_inode_nums s \<and> (\<forall> f. obj \<noteq> E_file f i))"
+| "enrich_not_alive s obj (I_msg q m) = 
+  ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msgq q \<and>
+     (case obj of
+        E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax)
+      | _        \<Rightarrow> True) )"
 
 lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf"
 apply (case_tac f)
@@ -310,7 +363,7 @@
    (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *)
     and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd"
     and nodel: "no_del_event (e # s)"
-    and notin_all: "notin_all (e # s) obj'"
+    and notin_cur: "notin_cur (e # s) obj'"
   shows "valid (e # s')"
 proof-
   from vd' have os: "os_grant s e" and grant: "grant s e" and vd: "valid s"
@@ -372,9 +425,9 @@
     have p_in: "p \<in> current_procs s'" using os alive
       apply (erule_tac x = "O_proc p" in allE)
       by (auto simp:Clone)
-    have p'_not_in: "p' \<notin> current_procs s'" using  alive' notin_all os Clone
-      apply (erule_tac x = "E_proc p'" in allE)
-      apply (auto dest:not_all_procs_prop3)
+    have p'_not_in: "p' \<notin> current_procs s'" using  alive' notin_cur os Clone
+      apply (erule_tac x = "I_proc p'" in allE)
+      apply (auto dest:not_all_procs_prop3 simp del:nums_of_recvmsg.simps)
       done
     have fd_in: "fds \<subseteq> proc_file_fds s' p" using os alive ffd_remain
       by (auto simp:Clone proc_file_fds_def)
@@ -482,8 +535,8 @@
         apply (erule_tac x = "O_file f" in allE)
         by (auto simp:Open None)
       have fd_not_in: "fd \<notin> current_proc_fds s' p"
-        using os alive' p_in notin_all Open None
-        apply (erule_tac x = "E_fd p fd" in allE)
+        using os alive' p_in notin_cur Open None
+        apply (erule_tac x = "I_fd p fd" in allE)
         apply (case_tac obj')
         apply (auto dest:not_all_procs_prop3)
         done
@@ -530,19 +583,20 @@
       have p_in: "p \<in> current_procs s'" using os alive
         apply (erule_tac x = "O_proc p" in allE)
         by (auto simp:Open Some)
-      have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_all
-        apply (erule_tac x = "E_file f" in allE)
-        apply (case_tac obj')
-        by auto
+      have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_cur nodel
+        apply (erule_tac x = "I_file f" in allE)
+        by (case_tac obj', auto simp:current_files_simps)
       have fd_not_in: "fd \<notin> current_proc_fds s' p"
-        using os alive' p_in Open Some notin_all
-        apply (erule_tac x = "E_fd p fd" in allE)
+        using os alive' p_in Open Some notin_cur
+        apply (erule_tac x = "I_fd p fd" in allE)
         apply (case_tac obj', auto dest:not_all_procs_prop3)
         done
       have inum_not_in: "inum \<notin> current_inode_nums s'"
-        using os alive' Open Some notin_all
-        apply (erule_tac x = "E_inum inum" in allE)
-        by (case_tac obj', auto)
+        using os alive' Open Some notin_cur nodel
+        apply (erule_tac x = "I_inum inum" in allE)
+        apply (case_tac obj', auto)
+        apply (auto simp add:current_inode_nums_def current_file_inums_def split:if_splits)
+        done
       have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os
         by (simp add:Open Some hungs)
       moreover have "grant s' e"  
@@ -780,10 +834,10 @@
     from pf_in_s alive have pf_in: "is_dir s' pf"
       apply (erule_tac x = "O_dir pf" in allE)
       by (auto simp:Rmdir)
-    have empty_in: "dir_is_empty s' f" using os Rmdir notin_all 
+    have empty_in: "dir_is_empty s' f" using os Rmdir notin_cur 
       apply (clarsimp simp add:dir_is_empty_def f_in)
       using alive'
-      apply (erule_tac x = "E_file f'" in allE)
+      apply (erule_tac x = "I_file f'" in allE)
       apply simp
       apply (erule disjE)
       apply (erule_tac x = f' in allE, simp)
@@ -797,6 +851,16 @@
       apply (erule_tac x = pf in allE)
       apply (drule_tac f = pf in is_dir_in_current)
       apply (simp add:noJ_Anc)
+
+      apply (clarsimp)
+      apply (drule_tac f' = f in parent_ancen)
+      apply (simp, rule notI, simp add:noJ_Anc)
+      apply (case_tac "f = pf")
+      using vd' Rmdir
+      apply (simp_all add:is_dir_rmdir)
+      apply (erule_tac x = pf in allE)
+      apply (drule_tac f = pf in is_dir_in_current)
+      apply (simp add:noJ_Anc)
       done
     have "os_grant s' e" using p_in f_in os empty_in
       by (simp add:Rmdir hungs)
@@ -851,13 +915,15 @@
     have p_in: "p \<in> current_procs s'" using os alive
       apply (erule_tac x = "O_proc p" in allE)
       by (auto simp:Mkdir)
-    have f_not_in: "f \<notin> current_files s'" using os alive' Mkdir notin_all
-      apply (erule_tac x = "E_file f" in allE)
-      by (auto)
+    have f_not_in: "f \<notin> current_files s'"
+      using os alive' Mkdir notin_cur
+      apply (erule_tac x = "I_file f" in allE)
+      by (auto simp:current_files_simps)
     have inum_not_in: "inum \<notin> current_inode_nums s'"
-      using os alive' Mkdir notin_all
-      apply (erule_tac x = "E_inum inum" in allE)
-      by (auto)
+      using os alive' Mkdir notin_cur
+      apply (erule_tac x = "I_inum inum" in allE)
+      apply (auto simp:current_inode_nums_def current_file_inums_def split:if_splits)
+      done
     have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in
       by (simp add:Mkdir hungs)
     moreover have "grant s' e"  
@@ -903,9 +969,11 @@
     have p_in: "p \<in> current_procs s'" using os alive
       apply (erule_tac x = "O_proc p" in allE)
       by (auto simp:LinkHard)
-    have f'_not_in: "f' \<notin> current_files s'" using os alive' LinkHard notin_all
-      apply (erule_tac x = "E_file f'" in allE)
-      by (auto simp:LinkHard)
+    have f'_not_in: "f' \<notin> current_files s'" 
+      using os alive' LinkHard notin_cur vd'
+      apply (erule_tac x = "I_file f'" in allE)
+      apply (auto simp:LinkHard current_files_simps)
+      done
     have f_in: "is_file s' f" using os alive
       apply (erule_tac x = "O_file f" in allE)
       by (auto simp:LinkHard)
@@ -1004,9 +1072,13 @@
     have p_in: "p \<in> current_procs s'" using os alive
       apply (erule_tac x = "O_proc p" in allE)
       by (auto simp:CreateMsgq)
-    have q_not_in: "q \<notin> current_msgqs s'" using os alive' CreateMsgq notin_all
-      apply (erule_tac x = "E_msgq q" in allE)
-      by auto
+    have q_not_in: "q \<notin> current_msgqs s'" 
+      using os alive' CreateMsgq notin_cur nodel vd
+      apply (erule_tac x = "I_msgq q" in allE)
+      apply (auto split:t_enrich_obj.splits)
+      apply (drule nums_of_recv_0, simp+)
+      apply (drule new_msgq_1, simp+)
+      done      
     have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq)
     moreover have "grant s' e" 
     proof-
@@ -1062,9 +1134,12 @@
     have q_in: "q \<in> current_msgqs s'" using os alive
       apply (erule_tac x = "O_msgq q" in allE)
       by (simp add:SendMsg)
-    have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in
-      apply (erule_tac x = "E_msg q m" in allE)
+    have m_not_in: "m \<notin> set (msgs_of_queue s' q)" 
+      using os alive' notin_cur SendMsg q_in nodel vd
+      apply (erule_tac x = "I_msg q m" in allE)
       apply (case_tac obj', auto dest:not_all_msgqs_prop3)
+      apply (drule nums_of_recv_0, simp+)
+      apply (drule new_msgq_1, simp+)
       done
     have "os_grant s' e" using p_in q_in m_not_in sms_remain os
       by (simp add:SendMsg)
diff -r e832378a2ff2 -r ded3f83f6cb9 no_shm_selinux/Enrich2.thy
--- a/no_shm_selinux/Enrich2.thy	Wed Jan 01 23:00:24 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Mon Jan 06 23:07:51 2014 +0800
@@ -39,7 +39,7 @@
 done
 
 lemma enrich_msgq_cur_inof:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
 apply (induct s arbitrary:f, simp)
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
@@ -47,7 +47,7 @@
 done
 
 lemma enrich_msgq_cur_inos:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
 apply (rule ext)
 apply (induct s, simp)
@@ -56,20 +56,20 @@
 done
 
 lemma enrich_msgq_cur_inos':
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
 apply (simp add:enrich_msgq_cur_inos)
 done
 
 lemma enrich_msgq_cur_inums:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
 apply (auto simp:current_inode_nums_def current_file_inums_def 
   current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
 done
 
 lemma enrich_msgq_cur_itag:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
 apply (rule ext)
 apply (induct s, simp)
@@ -78,7 +78,7 @@
 done
 
 lemma enrich_msgq_cur_tcps:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
 apply (rule ext)
 apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
@@ -86,7 +86,7 @@
 done
 
 lemma enrich_msgq_cur_udps:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
 apply (rule ext)
 apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
@@ -94,7 +94,7 @@
 done
 
 lemma enrich_msgq_cur_msgqs:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
@@ -103,17 +103,17 @@
 
 lemma enrich_msgq_cur_msgs:
   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
-   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)"
+   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)" 
 apply (rule ext, simp, rule conjI, rule impI)
 apply (simp add:enrich_msgq_duq_sms)
-apply (rule impI)
+apply (rule impI) 
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
 apply (case_tac a, auto)
 done
 
 lemma enrich_msgq_cur_procs:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
@@ -121,14 +121,14 @@
 done
   
 lemma enrich_msgq_cur_files:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
 apply (auto simp:current_files_def)
 apply (simp add:enrich_msgq_cur_inof)+
 done
 
 lemma enrich_msgq_cur_fds:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
@@ -136,7 +136,7 @@
 done
 
 lemma enrich_msgq_filefd:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
 apply (rule ext, rule ext)
 apply (induct s, simp)
@@ -145,7 +145,7 @@
 done
 
 lemma enrich_msgq_flagfd:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
 apply (rule ext, rule ext)
 apply (induct s, simp)
@@ -154,7 +154,7 @@
 done
 
 lemma enrich_msgq_proc_fds:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
 apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
 done
@@ -168,7 +168,7 @@
 done
   
 lemma enrich_msgq_is_file:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
 apply (rule ext)
 apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
@@ -176,7 +176,7 @@
 done
 
 lemma enrich_msgq_is_dir:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
 apply (rule ext)
 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
@@ -204,30 +204,29 @@
 done
 
 (* enrich s target_proc duplicated_pro *)
-fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
+fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> nat \<Rightarrow> t_state"
 where 
-  "enrich_proc [] tp dp = []"
-| "enrich_proc (Execve p f fds # s) tp dp = (
+  "enrich_proc [] tp dp n = []"
+| "enrich_proc (Execve p f fds # s) tp dp n = (
      if (tp = p) 
-     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
-     else Execve p f fds # (enrich_proc s tp dp))"
-| "enrich_proc (Clone p p' fds # s) tp dp = (
+     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp n)
+     else Execve p f fds # (enrich_proc s tp dp n))"
+| "enrich_proc (Clone p p' fds # s) tp dp n = (
      if (tp = p') 
      then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
-     else Clone p p' fds # (enrich_proc s tp dp))"
-| "enrich_proc (Open p f flags fd opt # s) tp dp = (
+     else Clone p p' fds # (enrich_proc s tp dp n))"
+| "enrich_proc (Open p f flags fd opt # s) tp dp n= (
      if (tp = p)
-     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 = (
+     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp n)
+     else Open p f flags fd opt # (enrich_proc s tp dp n))"
+| "enrich_proc (ReadFile p fd # s) tp dp n = (
      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 (RecvMsg p q m # s) tp dp = (
+     then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp n)
+     else ReadFile p fd # (enrich_proc s tp dp n))"
+| "enrich_proc (RecvMsg p q m # s) tp dp n = (
      if (tp = p) 
-     then let dq = new_msgq (enrich_proc s tp dp) in
-          RecvMsg dp dq m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp) q dq)
-     else RecvMsg p q m # (enrich_proc s tp dp))"
+     then RecvMsg dp n m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp (n+1)) q n)
+     else RecvMsg p q m # (enrich_proc s tp dp n))"
 (*
 | "enrich_proc (CloseFd p fd # s) tp dp = (
      if (tp = p \<and> fd \<in> proc_file_fds s p)
@@ -252,7 +251,7 @@
      if (tp = p) then Exit p # s
      else Exit p # (enrich_proc s tp dp))"
 *)
-| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
+| "enrich_proc (e # s) tp dp n = e # (enrich_proc s tp dp n)"
 
 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
 where
@@ -304,47 +303,74 @@
 done
 
 lemma enrich_proc_dup_in:
-  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p' i)"
 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_def dest:not_all_procs_prop3)
-done
+apply (case_tac a)
+apply ( auto simp:is_created_proc_def Let_def enrich_msgq_cur_procs
+  dest:not_all_procs_prop3)
+sorry
 
 lemma enrich_proc_dup_ffd:
   "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f"
 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_def proc_file_fds_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
   dest:not_all_procs_prop3 split:if_splits option.splits)
-done 
+sorry
 
 lemma enrich_proc_dup_ffd':
-  "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
+  "\<lbrakk>file_of_proc_fd (enrich_proc s p p' i) p' 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 s p fd = Some f"
 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_def proc_file_fds_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
   dest:not_all_procs_prop3 split:if_splits option.splits)
-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
+sorry
 
 lemma enrich_proc_dup_ffd_eq:
   "\<lbrakk>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') p' fd = file_of_proc_fd s p fd"
+  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = file_of_proc_fd s p fd"
 apply (case_tac "file_of_proc_fd s p fd")
-apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
+apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p' i) p' fd")
 apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
+apply (drule_tac i = i in enrich_proc_dup_ffd, simp+)
 done
 
+lemma enrich_proc_cur_msgqs:
+  "\<lbrakk>valid s\<rbrakk> \<Longrightarrow> current_msgqs (enrich_proc s p p' i) = current_msgqs s \<union> {q'. q' \<ge> new_msgq s \<and> q' \<le> new_msgq s + (nums_of_recvmsg s p) - 1}"
+apply (induct s, simp)
+apply (auto)[1]
+apply (drule new_msgq_1, simp, simp)
+apply (frule vt_grant_os, frule vd_cons)
+sorry
+
+lemma enrich_proc_not_alive:
+  "\<lbrakk>enrich_not_alive s (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) 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' (new_msgq s)) (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj"
+apply (case_tac obj, simp_all)
+prefer 5
+apply (simp add:enrich_proc_cur_msgqs)
+apply (rule impI, rule notI)
+apply simp
+apply (auto)[1]
+defer
+apply simp
+apply (rule impI, rule notI)
+defer
+apply (subgoal_tac "new_msgq s \<noteq> 0")
+apply simp
+apply arith
+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)
+defer
+apply (rule impI, rule notI)
+sorry
+
 
 lemma enrich_proc_dup_fflags:
   "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
@@ -352,9 +378,9 @@
        flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
 apply (induct s arbitrary:p, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def Let_def
   dest:not_all_procs_prop3 split:if_splits option.splits)
-done
+sorry
 
 lemma enrich_proc_dup_ffds:
   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -374,7 +400,14 @@
 apply (frule not_all_procs_prop3)
 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
-  simp:proc_file_fds_def is_created_proc_def)
+  simp:proc_file_fds_def is_created_proc_def Let_def)
+sorry
+
+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:
@@ -383,8 +416,8 @@
 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
+apply (auto split:option.splits simp del:grant.simps simp add:Let_def)
+sorry
 
 lemma not_all_procs_sock:
   "\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
@@ -399,11 +432,11 @@
 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 (case_tac a, auto split:option.splits simp:not_all_procs_sock Let_def)
 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
+sorry
 
 lemma enrich_proc_cur_inums:
   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -418,8 +451,8 @@
 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
+apply (case_tac a, auto split:option.splits t_socket_type.splits simp:Let_def)
+sorry
 
 lemma enrich_proc_cur_tcps:
   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
@@ -433,31 +466,32 @@
   "\<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
+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"
+  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (enrich_proc s p p')"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto)
-done
+apply (case_tac a, auto simp:Let_def)
+sorry
 
 lemma enrich_proc_cur_msgs:
-  "valid s \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q "
+  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q"
 apply (induct s, simp)
+apply (frule_tac p = p and p' = p' in enrich_proc_cur_msgqs, simp)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto)
-done
+apply (case_tac a, auto simp:Let_def)
+sorry
 
 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
+apply (case_tac a, auto simp:is_created_proc_simps Let_def)
+sorry
 
 lemma enrich_proc_cur_files:
   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
@@ -472,18 +506,22 @@
 apply (frule vt_grant_os, frule vd_cons)
 apply (frule not_all_procs_prop3)
 apply (case_tac a)
+sorry
+(*
 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 (frule not_all_procs_prop3) sorry  (*
 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>
@@ -497,7 +535,9 @@
 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
+defer
+apply (rule impI, rule notI)
+sorry
 
 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>
@@ -507,7 +547,7 @@
 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
+sorry
 
 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>
@@ -517,14 +557,14 @@
 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
+sorry
 
 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
+sorry
 
 lemma enrich_proc_is_file:
   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>