Mercurial Mercurial > hg > selinux / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no_shm_selinux/Enrich2.thy
changeset 89 ded3f83f6cb9
parent 88 e832378a2ff2
child 90 003cac7b8bf5
equal deleted inserted replaced
88:e832378a2ff2 89:ded3f83f6cb9 
    37 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    37 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    38 apply auto
 
    38 apply auto
 
    39 done
 
    39 done
 
    40 
    40 
    41 lemma enrich_msgq_cur_inof:
 
    41 lemma enrich_msgq_cur_inof:
 
    42   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    42   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    43    \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
 
    43    \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
 
    44 apply (induct s arbitrary:f, simp)
 
    44 apply (induct s arbitrary:f, simp)
 
    45 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    45 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    46 apply (auto split:option.splits)
 
    46 apply (auto split:option.splits)
 
    47 done
 
    47 done
 
    48 
    48 
    49 lemma enrich_msgq_cur_inos:
 
    49 lemma enrich_msgq_cur_inos:
 
    50   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    50   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    51    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
 
    51    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
 
    52 apply (rule ext)
 
    52 apply (rule ext)
 
    53 apply (induct s, simp)
 
    53 apply (induct s, simp)
 
    54 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    54 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    55 apply (auto split:option.splits)
 
    55 apply (auto split:option.splits)
 
    56 done
 
    56 done
 
    57 
    57 
    58 lemma enrich_msgq_cur_inos':
 
    58 lemma enrich_msgq_cur_inos':
 
    59   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    59   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    60    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
 
    60    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
 
    61 apply (simp add:enrich_msgq_cur_inos)
 
    61 apply (simp add:enrich_msgq_cur_inos)
 
    62 done
 
    62 done
 
    63 
    63 
    64 lemma enrich_msgq_cur_inums:
 
    64 lemma enrich_msgq_cur_inums:
 
    65   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    65   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    66    \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
 
    66    \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
 
    67 apply (auto simp:current_inode_nums_def current_file_inums_def 
    67 apply (auto simp:current_inode_nums_def current_file_inums_def 
    68   current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
 
    68   current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
 
    69 done
 
    69 done
 
    70 
    70 
    71 lemma enrich_msgq_cur_itag:
 
    71 lemma enrich_msgq_cur_itag:
 
    72   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    72   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    73    \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
 
    73    \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
 
    74 apply (rule ext)
 
    74 apply (rule ext)
 
    75 apply (induct s, simp)
 
    75 apply (induct s, simp)
 
    76 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    76 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
    77 apply (auto split:option.splits t_socket_type.splits)
 
    77 apply (auto split:option.splits t_socket_type.splits)
 
    78 done
 
    78 done
 
    79 
    79 
    80 lemma enrich_msgq_cur_tcps:
 
    80 lemma enrich_msgq_cur_tcps:
 
    81   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    81   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    82    \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
 
    82    \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
 
    83 apply (rule ext)
 
    83 apply (rule ext)
 
    84 apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
 
    84 apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
 
    85   split:option.splits t_inode_tag.splits)
 
    85   split:option.splits t_inode_tag.splits)
 
    86 done
 
    86 done
 
    87 
    87 
    88 lemma enrich_msgq_cur_udps:
 
    88 lemma enrich_msgq_cur_udps:
 
    89   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    89   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
    90    \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
 
    90    \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
 
    91 apply (rule ext)
 
    91 apply (rule ext)
 
    92 apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
 
    92 apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
 
    93   split:option.splits t_inode_tag.splits)
 
    93   split:option.splits t_inode_tag.splits)
 
    94 done
 
    94 done
 
    95 
    95 
    96 lemma enrich_msgq_cur_msgqs:
 
    96 lemma enrich_msgq_cur_msgqs:
 
    97   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    97   "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
    98    \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
 
    98    \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
 
    99 apply (induct s, simp)
 
    99 apply (induct s, simp)
 
   100 apply (frule vt_grant_os, frule vd_cons)
 
   100 apply (frule vt_grant_os, frule vd_cons)
 
   101 apply (case_tac a, auto)
 
   101 apply (case_tac a, auto)
 
   102 done
 
   102 done
 
   103 
   103 
   104 lemma enrich_msgq_cur_msgs:
 
   104 lemma enrich_msgq_cur_msgs:
 
   105   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   105   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   106    \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)"
 
   106    \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)" 
   107 apply (rule ext, simp, rule conjI, rule impI)
 
   107 apply (rule ext, simp, rule conjI, rule impI)
 
   108 apply (simp add:enrich_msgq_duq_sms)
 
   108 apply (simp add:enrich_msgq_duq_sms)
 
   109 apply (rule impI)
 
   109 apply (rule impI) 
   110 apply (induct s, simp)
 
   110 apply (induct s, simp)
 
   111 apply (frule vt_grant_os, frule vd_cons)
 
   111 apply (frule vt_grant_os, frule vd_cons)
 
   112 apply (case_tac a, auto)
 
   112 apply (case_tac a, auto)
 
   113 done
 
   113 done
 
   114 
   114 
   115 lemma enrich_msgq_cur_procs:
 
   115 lemma enrich_msgq_cur_procs:
 
   116   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   116   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   117    \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
 
   117    \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
 
   118 apply (induct s, simp)
 
   118 apply (induct s, simp)
 
   119 apply (frule vt_grant_os, frule vd_cons)
 
   119 apply (frule vt_grant_os, frule vd_cons)
 
   120 apply (case_tac a, auto)
 
   120 apply (case_tac a, auto)
 
   121 done
 
   121 done
 
   122   
   122   
   123 lemma enrich_msgq_cur_files:
 
   123 lemma enrich_msgq_cur_files:
 
   124   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   124   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   125    \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
 
   125    \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
 
   126 apply (auto simp:current_files_def)
 
   126 apply (auto simp:current_files_def)
 
   127 apply (simp add:enrich_msgq_cur_inof)+
 
   127 apply (simp add:enrich_msgq_cur_inof)+
 
   128 done
 
   128 done
 
   129 
   129 
   130 lemma enrich_msgq_cur_fds:
 
   130 lemma enrich_msgq_cur_fds:
 
   131   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   131   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   132    \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
 
   132    \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
 
   133 apply (induct s, simp)
 
   133 apply (induct s, simp)
 
   134 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   134 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   135 apply auto
 
   135 apply auto
 
   136 done
 
   136 done
 
   137 
   137 
   138 lemma enrich_msgq_filefd:
 
   138 lemma enrich_msgq_filefd:
 
   139   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   139   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   140    \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
 
   140    \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
 
   141 apply (rule ext, rule ext)
 
   141 apply (rule ext, rule ext)
 
   142 apply (induct s, simp)
 
   142 apply (induct s, simp)
 
   143 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   143 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   144 apply auto
 
   144 apply auto
 
   145 done
 
   145 done
 
   146 
   146 
   147 lemma enrich_msgq_flagfd:
 
   147 lemma enrich_msgq_flagfd:
 
   148   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   148   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   149    \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
 
   149    \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
 
   150 apply (rule ext, rule ext)
 
   150 apply (rule ext, rule ext)
 
   151 apply (induct s, simp)
 
   151 apply (induct s, simp)
 
   152 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   152 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   153 apply auto
 
   153 apply auto
 
   154 done
 
   154 done
 
   155 
   155 
   156 lemma enrich_msgq_proc_fds:
 
   156 lemma enrich_msgq_proc_fds:
 
   157   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   157   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   158    \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
 
   158    \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
 
   159 apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
 
   159 apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
 
   160 done
 
   160 done
 
   161 
   161 
   162 lemma enrich_msgq_hungs:
 
   162 lemma enrich_msgq_hungs:
 
   166 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   166 apply (frule vt_grant_os, frule vd_cons, case_tac a)
 
   167 apply (auto simp:files_hung_by_del.simps)
 
   167 apply (auto simp:files_hung_by_del.simps)
 
   168 done
 
   168 done
 
   169   
   169   
   170 lemma enrich_msgq_is_file:
 
   170 lemma enrich_msgq_is_file:
 
   171   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   171   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   172    \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
 
   172    \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
 
   173 apply (rule ext)
 
   173 apply (rule ext)
 
   174 apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
 
   174 apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
 
   175   split:option.splits t_inode_tag.splits)
 
   175   split:option.splits t_inode_tag.splits)
 
   176 done
 
   176 done
 
   177 
   177 
   178 lemma enrich_msgq_is_dir:
 
   178 lemma enrich_msgq_is_dir:
 
   179   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
 
   179   "\<lbrakk>no_del_event s; valid s\<rbrakk>
 
   180    \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
 
   180    \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
 
   181 apply (rule ext)
 
   181 apply (rule ext)
 
   182 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
 
   182 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
 
   183   split:option.splits t_inode_tag.splits)
 
   183   split:option.splits t_inode_tag.splits)
 
   184 done
 
   184 done
 
   202   enrich_msgq_cur_tcps enrich_msgq_cur_udps)
 
   202   enrich_msgq_cur_tcps enrich_msgq_cur_udps)
 
   203 apply (auto split:if_splits)
 
   203 apply (auto split:if_splits)
 
   204 done
 
   204 done
 
   205 
   205 
   206 (* enrich s target_proc duplicated_pro *)
 
   206 (* enrich s target_proc duplicated_pro *)
 
   207 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
 
   207 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> nat \<Rightarrow> t_state"
 
   208 where 
   208 where 
   209   "enrich_proc [] tp dp = []"
 
   209   "enrich_proc [] tp dp n = []"
 
   210 | "enrich_proc (Execve p f fds # s) tp dp = (
 
   210 | "enrich_proc (Execve p f fds # s) tp dp n = (
 
   211      if (tp = p) 
   211      if (tp = p) 
   212      then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
 
   212      then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp n)
 
   213      else Execve p f fds # (enrich_proc s tp dp))"
 
   213      else Execve p f fds # (enrich_proc s tp dp n))"
 
   214 | "enrich_proc (Clone p p' fds # s) tp dp = (
 
   214 | "enrich_proc (Clone p p' fds # s) tp dp n = (
 
   215      if (tp = p') 
   215      if (tp = p') 
   216      then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
 
   216      then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
 
   217      else Clone p p' fds # (enrich_proc s tp dp))"
 
   217      else Clone p p' fds # (enrich_proc s tp dp n))"
 
   218 | "enrich_proc (Open p f flags fd opt # s) tp dp = (
 
   218 | "enrich_proc (Open p f flags fd opt # s) tp dp n= (
 
   219      if (tp = p)
 
   219      if (tp = p)
 
   220      then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
 
   220      then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp n)
 
   221      else Open p f flags fd opt # (enrich_proc s tp dp))"
 
   221      else Open p f flags fd opt # (enrich_proc s tp dp n))"
 
   222 | "enrich_proc (ReadFile p fd # s) tp dp = (
 
   222 | "enrich_proc (ReadFile p fd # s) tp dp n = (
 
   223      if (tp = p) 
   223      if (tp = p) 
   224      then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
 
   224      then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp n)
 
   225      else ReadFile p fd # (enrich_proc s tp dp))"
 
   225      else ReadFile p fd # (enrich_proc s tp dp n))"
 
   226 | "enrich_proc (RecvMsg p q m # s) tp dp = (
 
   226 | "enrich_proc (RecvMsg p q m # s) tp dp n = (
 
   227      if (tp = p) 
   227      if (tp = p) 
   228      then let dq = new_msgq (enrich_proc s tp dp) in
 
   228      then RecvMsg dp n m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp (n+1)) q n)
 
   229           RecvMsg dp dq m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp) q dq)
 
   229      else RecvMsg p q m # (enrich_proc s tp dp n))"
 
   230      else RecvMsg p q m # (enrich_proc s tp dp))"
 
       
   231 (*
 
   230 (*
 
   232 | "enrich_proc (CloseFd p fd # s) tp dp = (
 
   231 | "enrich_proc (CloseFd p fd # s) tp dp = (
 
   233      if (tp = p \<and> fd \<in> proc_file_fds s p)
 
   232      if (tp = p \<and> fd \<in> proc_file_fds s p)
 
   234      then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
 
   233      then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
 
   235      else CloseFd p fd # (enrich_proc s tp dp))"
 
   234      else CloseFd p fd # (enrich_proc s tp dp))"
 
   250      else Kill p p' # (enrich_proc s tp dp))"
 
   249      else Kill p p' # (enrich_proc s tp dp))"
 
   251 | "enrich_proc (Exit p # s) tp dp = (
 
   250 | "enrich_proc (Exit p # s) tp dp = (
 
   252      if (tp = p) then Exit p # s
 
   251      if (tp = p) then Exit p # s
 
   253      else Exit p # (enrich_proc s tp dp))"
 
   252      else Exit p # (enrich_proc s tp dp))"
 
   254 *)
 
   253 *)
 
   255 | "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
 
   254 | "enrich_proc (e # s) tp dp n = e # (enrich_proc s tp dp n)"
 
   256 
   255 
   257 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
 
   256 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
 
   258 where
 
   257 where
 
   259   "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
 
   258   "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
 
   260 
   259 
   302 apply (case_tac a)
 
   301 apply (case_tac a)
 
   303 apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
 
   302 apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
 
   304 done
 
   303 done
 
   305 
   304 
   306 lemma enrich_proc_dup_in:
 
   305 lemma enrich_proc_dup_in:
 
   307   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
 
   306   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   308    \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
 
   307    \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p' i)"
 
   309 apply (induct s, simp add:is_created_proc_def)
 
   308 apply (induct s, simp add:is_created_proc_def)
 
   310 apply (frule vt_grant_os, frule vd_cons)
 
   309 apply (frule vt_grant_os, frule vd_cons)
 
   311 apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
 
   310 apply (case_tac a)
 
   312 done
 
   311 apply ( auto simp:is_created_proc_def Let_def enrich_msgq_cur_procs
 
       
   312   dest:not_all_procs_prop3)
 
       
   313 sorry
 
   313 
   314 
   314 lemma enrich_proc_dup_ffd:
 
   315 lemma enrich_proc_dup_ffd:
 
   315   "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
 
   316   "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
 
   316    \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
 
   317    \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f"
 
   317 apply (induct s, simp add:is_created_proc_def)
 
   318 apply (induct s, simp add:is_created_proc_def)
 
   318 apply (frule vt_grant_os, frule vd_cons)
 
   319 apply (frule vt_grant_os, frule vd_cons)
 
   319 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
 
   320 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
 
   320   dest:not_all_procs_prop3 split:if_splits option.splits)
 
   321   dest:not_all_procs_prop3 split:if_splits option.splits)
 
   321 done 
   322 sorry
 
   322 
   323 
   323 lemma enrich_proc_dup_ffd':
 
   324 lemma enrich_proc_dup_ffd':
 
   324   "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
 
   325   "\<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;
 
   325     no_del_event s; valid s\<rbrakk>
 
   326     no_del_event s; valid s\<rbrakk>
 
   326    \<Longrightarrow> file_of_proc_fd s p fd = Some f"
 
   327    \<Longrightarrow> file_of_proc_fd s p fd = Some f"
 
   327 apply (induct s, simp add:is_created_proc_def)
 
   328 apply (induct s, simp add:is_created_proc_def)
 
   328 apply (frule vt_grant_os, frule vd_cons)
 
   329 apply (frule vt_grant_os, frule vd_cons)
 
   329 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
 
   330 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
 
   330   dest:not_all_procs_prop3 split:if_splits option.splits)
 
   331   dest:not_all_procs_prop3 split:if_splits option.splits)
 
   331 done 
   332 sorry
 
   332 
       
   333 lemma enrich_proc_dup_ffds':
 
       
   334   "\<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>
 
       
   335    \<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
 
       
   336 apply (auto simp:enrich_proc_dup_ffds_eq_fds)
 
       
   337 apply (simp add:proc_file_fds_def)
 
       
   338 done
 
       
   339 
   333 
   340 lemma enrich_proc_dup_ffd_eq:
 
   334 lemma enrich_proc_dup_ffd_eq:
 
   341   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   335   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   342   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = file_of_proc_fd s p fd"
 
   336   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = file_of_proc_fd s p fd"
 
   343 apply (case_tac "file_of_proc_fd s p fd")
 
   337 apply (case_tac "file_of_proc_fd s p fd")
 
   344 apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
 
   338 apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p' i) p' fd")
 
   345 apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
 
   339 apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
 
   346 done
 
   340 apply (drule_tac i = i in enrich_proc_dup_ffd, simp+)
 
       
   341 done
 
       
   342 
       
   343 lemma enrich_proc_cur_msgqs:
 
       
   344   "\<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}"
 
       
   345 apply (induct s, simp)
 
       
   346 apply (auto)[1]
 
       
   347 apply (drule new_msgq_1, simp, simp)
 
       
   348 apply (frule vt_grant_os, frule vd_cons)
 
       
   349 sorry
 
       
   350 
       
   351 lemma enrich_proc_not_alive:
 
       
   352   "\<lbrakk>enrich_not_alive s (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj; 
       
   353     is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
       
   354   \<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"
 
       
   355 apply (case_tac obj, simp_all)
 
       
   356 prefer 5
 
       
   357 apply (simp add:enrich_proc_cur_msgqs)
 
       
   358 apply (rule impI, rule notI)
 
       
   359 apply simp
 
       
   360 apply (auto)[1]
 
       
   361 defer
 
       
   362 apply simp
 
       
   363 apply (rule impI, rule notI)
 
       
   364 defer
 
       
   365 apply (subgoal_tac "new_msgq s \<noteq> 0")
 
       
   366 apply simp
 
       
   367 apply arith
 
       
   368 apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
       
   369   enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
 
       
   370 defer
 
       
   371 apply (rule impI, rule notI)
 
       
   372 sorry
 
   347 
   373 
   348 
   374 
   349 lemma enrich_proc_dup_fflags:
 
   375 lemma enrich_proc_dup_fflags:
 
   350   "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
 
   376   "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
 
   351    \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
 
   377    \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
 
   352        flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
 
   378        flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
 
   353 apply (induct s arbitrary:p, simp add:is_created_proc_def)
 
   379 apply (induct s arbitrary:p, simp add:is_created_proc_def)
 
   354 apply (frule vt_grant_os, frule vd_cons)
 
   380 apply (frule vt_grant_os, frule vd_cons)
 
   355 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
 
   381 apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def Let_def
 
   356   dest:not_all_procs_prop3 split:if_splits option.splits)
 
   382   dest:not_all_procs_prop3 split:if_splits option.splits)
 
   357 done
 
   383 sorry
 
   358 
   384 
   359 lemma enrich_proc_dup_ffds:
 
   385 lemma enrich_proc_dup_ffds:
 
   360   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   386   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   361    \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
 
   387    \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
 
   362 apply (auto simp:proc_file_fds_def)
 
   388 apply (auto simp:proc_file_fds_def)
 
   372 apply (induct s arbitrary:p)
 
   398 apply (induct s arbitrary:p)
 
   373 apply (simp add: is_created_proc_def)
 
   399 apply (simp add: is_created_proc_def)
 
   374 apply (frule not_all_procs_prop3)
 
   400 apply (frule not_all_procs_prop3)
 
   375 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 
   401 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 
   376 apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
   402 apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
   377   simp:proc_file_fds_def is_created_proc_def)
 
   403   simp:proc_file_fds_def is_created_proc_def Let_def)
 
       
   404 sorry
 
       
   405 
       
   406 lemma enrich_proc_dup_ffds':
 
       
   407   "\<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>
 
       
   408    \<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
 
       
   409 apply (auto simp:enrich_proc_dup_ffds_eq_fds)
 
       
   410 apply (simp add:proc_file_fds_def)
 
   378 done
 
   411 done
 
   379 
   412 
   380 lemma enrich_proc_cur_inof:
 
   413 lemma enrich_proc_cur_inof:
 
   381   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
 
   414   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
 
   382 apply (induct s arbitrary:f)
 
   415 apply (induct s arbitrary:f)
 
   383 apply simp
 
   416 apply simp
 
   384 apply (frule vd_cons, frule vt_grant_os, frule vt_grant)
 
   417 apply (frule vd_cons, frule vt_grant_os, frule vt_grant)
 
   385 apply (case_tac a, auto)
 
   418 apply (case_tac a, auto)
 
   386 apply (auto split:option.splits simp del:grant.simps)
 
   419 apply (auto split:option.splits simp del:grant.simps simp add:Let_def)
 
   387 done
 
   420 sorry
 
   388 
   421 
   389 lemma not_all_procs_sock:
 
   422 lemma not_all_procs_sock:
 
   390   "\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
 
   423   "\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
 
   391 apply (frule not_all_procs_prop3)
 
   424 apply (frule not_all_procs_prop3)
 
   392 apply (case_tac "inum_of_socket s (p', fd)", simp_all)
 
   425 apply (case_tac "inum_of_socket s (p', fd)", simp_all)
 
   397   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   430   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   398    \<Longrightarrow> inum_of_socket (enrich_proc s p p') (tp, fd) = inum_of_socket s (tp, fd)"
 
   431    \<Longrightarrow> inum_of_socket (enrich_proc s p p') (tp, fd) = inum_of_socket s (tp, fd)"
 
   399 apply (induct s arbitrary:tp)
 
   432 apply (induct s arbitrary:tp)
 
   400 apply simp
 
   433 apply simp
 
   401 apply (frule vd_cons, frule vt_grant_os)
 
   434 apply (frule vd_cons, frule vt_grant_os)
 
   402 apply (case_tac a, auto split:option.splits simp:not_all_procs_sock)
 
   435 apply (case_tac a, auto split:option.splits simp:not_all_procs_sock Let_def)
 
   403 apply (simp add:proc_file_fds_def, erule exE)
 
   436 apply (simp add:proc_file_fds_def, erule exE)
 
   404 apply (case_tac "inum_of_socket s (nat1, fd)", simp_all)
 
   437 apply (case_tac "inum_of_socket s (nat1, fd)", simp_all)
 
   405 apply (drule filefd_socket_conflict, simp_all add:current_sockets_def)
 
   438 apply (drule filefd_socket_conflict, simp_all add:current_sockets_def)
 
   406 done
 
   439 sorry
 
   407 
   440 
   408 lemma enrich_proc_cur_inums:
 
   441 lemma enrich_proc_cur_inums:
 
   409   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   442   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
 
   410    \<Longrightarrow> current_inode_nums (enrich_proc s p p') = current_inode_nums s"
 
   443    \<Longrightarrow> current_inode_nums (enrich_proc s p p') = current_inode_nums s"
 
   411 apply (auto simp:current_inode_nums_def current_file_inums_def 
   444 apply (auto simp:current_inode_nums_def current_file_inums_def 
   416   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   449   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   417    \<Longrightarrow> itag_of_inum (enrich_proc s p p') i = itag_of_inum s i"
 
   450    \<Longrightarrow> itag_of_inum (enrich_proc s p p') i = itag_of_inum s i"
 
   418 apply (induct s)
 
   451 apply (induct s)
 
   419 apply simp
 
   452 apply simp
 
   420 apply (frule vd_cons, frule vt_grant_os)
 
   453 apply (frule vd_cons, frule vt_grant_os)
 
   421 apply (case_tac a, auto split:option.splits t_socket_type.splits)
 
   454 apply (case_tac a, auto split:option.splits t_socket_type.splits simp:Let_def)
 
   422 done
 
   455 sorry
 
   423 
   456 
   424 lemma enrich_proc_cur_tcps:
 
   457 lemma enrich_proc_cur_tcps:
 
   425   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   458   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   426    \<Longrightarrow> is_tcp_sock (enrich_proc s p p') = is_tcp_sock s"
 
   459    \<Longrightarrow> is_tcp_sock (enrich_proc s p p') = is_tcp_sock s"
 
   427 apply (rule ext, case_tac x)
 
   460 apply (rule ext, case_tac x)
 
   431 
   464 
   432 lemma enrich_proc_cur_udps:
 
   465 lemma enrich_proc_cur_udps:
 
   433   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   466   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   434    \<Longrightarrow> is_udp_sock (enrich_proc s p p') = is_udp_sock s"
 
   467    \<Longrightarrow> is_udp_sock (enrich_proc s p p') = is_udp_sock s"
 
   435 apply (rule ext, case_tac x)
 
   468 apply (rule ext, case_tac x)
 
   436 apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
 
   469 apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos 
   437   split:option.splits t_inode_tag.splits)
 
   470   split:option.splits t_inode_tag.splits)
 
   438 done
 
   471 done
 
   439 
   472 
   440 lemma enrich_proc_cur_msgqs:
 
   473 lemma enrich_proc_cur_msgqs:
 
   441   "valid s \<Longrightarrow> current_msgqs (enrich_proc s p p') = current_msgqs s"
 
   474   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (enrich_proc s p p')"
 
   442 apply (induct s, simp)
 
   475 apply (induct s, simp)
 
   443 apply (frule vt_grant_os, frule vd_cons)
 
   476 apply (frule vt_grant_os, frule vd_cons)
 
   444 apply (case_tac a, auto)
 
   477 apply (case_tac a, auto simp:Let_def)
 
   445 done
 
   478 sorry
 
   446 
   479 
   447 lemma enrich_proc_cur_msgs:
 
   480 lemma enrich_proc_cur_msgs:
 
   448   "valid s \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q "
 
   481   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q"
 
   449 apply (induct s, simp)
 
   482 apply (induct s, simp)
 
   450 apply (frule vt_grant_os, frule vd_cons)
 
   483 apply (frule_tac p = p and p' = p' in enrich_proc_cur_msgqs, simp)
 
   451 apply (case_tac a, auto)
 
   484 apply (frule vt_grant_os, frule vd_cons)
 
   452 done
 
   485 apply (case_tac a, auto simp:Let_def)
 
       
   486 sorry
 
   453 
   487 
   454 lemma enrich_proc_cur_procs:
 
   488 lemma enrich_proc_cur_procs:
 
   455   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk> 
   489   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk> 
   456    \<Longrightarrow> current_procs (enrich_proc s p p') = current_procs s \<union> {p'}"
 
   490    \<Longrightarrow> current_procs (enrich_proc s p p') = current_procs s \<union> {p'}"
 
   457 apply (induct s, simp add:is_created_proc_def)
 
   491 apply (induct s, simp add:is_created_proc_def)
 
   458 apply (frule vt_grant_os, frule vd_cons)
 
   492 apply (frule vt_grant_os, frule vd_cons)
 
   459 apply (case_tac a, auto simp:is_created_proc_simps)
 
   493 apply (case_tac a, auto simp:is_created_proc_simps Let_def)
 
   460 done
 
   494 sorry
 
   461 
   495 
   462 lemma enrich_proc_cur_files:
 
   496 lemma enrich_proc_cur_files:
 
   463   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
 
   497   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
 
   464 apply (auto simp:current_files_def)
 
   498 apply (auto simp:current_files_def)
 
   465 apply (simp add: enrich_proc_cur_inof)+
 
   499 apply (simp add: enrich_proc_cur_inof)+
 
   470    \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
 
   504    \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
 
   471 apply (induct s, simp add:is_created_proc_def)
 
   505 apply (induct s, simp add:is_created_proc_def)
 
   472 apply (frule vt_grant_os, frule vd_cons)
 
   506 apply (frule vt_grant_os, frule vd_cons)
 
   473 apply (frule not_all_procs_prop3)
 
   507 apply (frule not_all_procs_prop3)
 
   474 apply (case_tac a)
 
   508 apply (case_tac a)
 
       
   509 sorry
 
       
   510 (*
 
   475 apply (auto simp:is_created_proc_simps)
 
   511 apply (auto simp:is_created_proc_simps)
 
   476 done
 
   512 done
 
       
   513 *)
 
   477 
   514 
   478 lemma enrich_proc_cur_fds1':
 
   515 lemma enrich_proc_cur_fds1':
 
   479   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<noteq> p'\<rbrakk>
 
   516   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<noteq> p'\<rbrakk>
 
   480    \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
 
   517    \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
 
   481 apply (induct s, simp add:is_created_proc_def)
 
   518 apply (induct s, simp add:is_created_proc_def)
 
   482 apply (frule vt_grant_os, frule vd_cons)
 
   519 apply (frule vt_grant_os, frule vd_cons)
 
   483 apply (frule not_all_procs_prop3)
 
   520 apply (frule not_all_procs_prop3) sorry  (*
 
   484 apply (case_tac a)
 
   521 apply (case_tac a)
 
   485 apply (auto simp:is_created_proc_simps)
 
   522 apply (auto simp:is_created_proc_simps)
 
   486 done
 
   523 done
 
       
   524 *)
 
   487 
   525 
   488 lemma enrich_proc_cur_fds:
 
   526 lemma enrich_proc_cur_fds:
 
   489   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
 
   527   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
 
   490    \<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)"
 
   528    \<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)"
 
   491 apply (simp add:enrich_proc_cur_fds1' enrich_proc_dup_ffds_eq_fds split:if_splits)
 
   529 apply (simp add:enrich_proc_cur_fds1' enrich_proc_dup_ffds_eq_fds split:if_splits)
 
   495   "\<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>
 
   533   "\<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>
 
   496   \<Longrightarrow> enrich_not_alive (enrich_proc s p p') (E_proc p') obj"
 
   534   \<Longrightarrow> enrich_not_alive (enrich_proc s p p') (E_proc p') obj"
 
   497 apply (case_tac obj)
 
   535 apply (case_tac obj)
 
   498 apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
   536 apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
   499   enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
 
   537   enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
 
   500 done
 
   538 defer
 
       
   539 apply (rule impI, rule notI)
 
       
   540 sorry
 
   501 
   541 
   502 lemma enrich_proc_filefd:
 
   542 lemma enrich_proc_filefd:
 
   503   "\<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>
 
   543   "\<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>
 
   504   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 
   544   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 
   505 apply (induct s arbitrary:tp, simp add:is_created_proc_def)
 
   545 apply (induct s arbitrary:tp, simp add:is_created_proc_def)
 
   506 apply (frule vt_grant_os, frule vd_cons)
 
   546 apply (frule vt_grant_os, frule vd_cons)
 
   507 apply (frule not_all_procs_prop3)
 
   547 apply (frule not_all_procs_prop3)
 
   508 apply (case_tac a)
 
   548 apply (case_tac a)
 
   509 apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs split:if_splits)
 
   549 apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs split:if_splits)
 
   510 done
 
   550 sorry
 
   511 
   551 
   512 lemma enrich_proc_flagfd:
 
   552 lemma enrich_proc_flagfd:
 
   513   "\<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>
 
   553   "\<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>
 
   514   \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 
   554   \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 
   515 apply (induct s arbitrary:tp, simp add:is_created_proc_def)
 
   555 apply (induct s arbitrary:tp, simp add:is_created_proc_def)
 
   516 apply (frule vt_grant_os, frule vd_cons)
 
   556 apply (frule vt_grant_os, frule vd_cons)
 
   517 apply (frule not_all_procs_prop3)
 
   557 apply (frule not_all_procs_prop3)
 
   518 apply (case_tac a)
 
   558 apply (case_tac a)
 
   519 apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs current_fflag_has_ffd split:if_splits option.splits)
 
   559 apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs current_fflag_has_ffd split:if_splits option.splits)
 
   520 done
 
   560 sorry
 
   521 
   561 
   522 lemma enrich_proc_hungs:
 
   562 lemma enrich_proc_hungs:
 
   523   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
 
   563   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
 
   524 apply (induct s, simp)
 
   564 apply (induct s, simp)
 
   525 apply (frule vt_grant_os, frule vd_cons)
 
   565 apply (frule vt_grant_os, frule vd_cons)
 
   526 apply (case_tac a, auto simp:files_hung_by_del.simps)
 
   566 apply (case_tac a, auto simp:files_hung_by_del.simps)
 
   527 done
 
   567 sorry
 
   528 
   568 
   529 lemma enrich_proc_is_file:
 
   569 lemma enrich_proc_is_file:
 
   530   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   570   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   531    \<Longrightarrow> is_file (enrich_proc s p p') = is_file s"
 
   571    \<Longrightarrow> is_file (enrich_proc s p p') = is_file s"
 
   532 apply (rule ext, case_tac x)
 
   572 apply (rule ext, case_tac x)
selinux