9 

     9 (* simpset for s2ss*)

    10 lemma current_proc_has_sp:

    11   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"

    12 by (auto simp:cp2sproc_def split:option.splits dest!:current_has_sec')

    13 

    14 lemma current_proc_has_sp':

    15   "\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"

    16 by (auto dest:current_proc_has_sp)

    17 

    18 lemma is_dir_has_sdir':

    19   "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

    20 apply (case_tac f)

    21 apply (rule_tac x = sroot in exI)

    22 apply (simp add:sroot_only)

    23 apply (drule is_dir_has_sfile, auto)

    24 done

    25 

    26 lemma is_file_has_sfile':

    27   "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

    28 by (drule is_file_has_sfile, auto)

    29 

    30 (* simpset for same_inode_files: Current_files_prop.thy *)

    31 

    32 lemma same_inode_files_nil:

    33   "same_inode_files [] = init_same_inode_files"

    34 by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)

    35 

    36 lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"

    37 by (auto simp add:current_inode_nums_def current_file_inums_def)

    38 

    39 lemma same_inode_files_open:

    40   "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.

    41      if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"

    42 apply (frule vt_grant_os, frule vd_cons, rule ext)

    43 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits

    44             dest:iof's_im_in_cim iof's_im_in_cim')

    45 apply (drule is_file_in_current)

    46 apply (simp add:current_files_def)

    47 done

    48 

    49 lemma same_inode_files_linkhard:

    50   "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. 

    51      if (f' = f \<or> f' \<in> same_inode_files s oldf) 

    52      then same_inode_files s oldf \<union> {f}

    53      else same_inode_files s f')"

    54 apply (frule vt_grant_os, frule vd_cons, rule ext)

    55 apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits

    56             dest:iof's_im_in_cim iof's_im_in_cim')

    57 apply (drule is_file_in_current)

    58 apply (simp add:current_files_def is_file_def)

    59 apply (simp add:is_file_def)

    60 done

    61 

    62 lemma inum_of_file_none_prop:

    63   "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

    64 by (simp add:current_files_def)

    65 

    66 lemma same_inode_files_closefd:

    67   "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> 

    68    same_inode_files (CloseFd p fd # s) f' = (

    69      case (file_of_proc_fd s p fd) of 

    70        Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))

    71                  then same_inode_files s f' - {f}

    72                  else same_inode_files s f' )

    73      | None   \<Rightarrow> same_inode_files s f' )"

    74 apply (frule vt_grant_os, frule vd_cons)

    75 apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd 

    76            split:if_splits option.splits

    77             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)

    78 done

    79 

    80 lemma same_inode_files_unlink:

    81   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> 

    82    \<Longrightarrow> same_inode_files (UnLink p f # s) f' = (

    83      if (proc_fd_of_file s f = {}) 

    84      then same_inode_files s f' - {f}

    85      else same_inode_files s f')"

    86 apply (frule vt_grant_os, frule vd_cons)

    87 apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink 

    88            split:if_splits option.splits

    89             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)

    90 done

    91 

    92 lemma same_inode_files_mkdir:

    93   "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"

    94 apply (frule vt_grant_os, frule vd_cons, rule ext)

    95 apply (auto simp:same_inode_files_def is_file_simps current_files_simps 

    96            split:if_splits option.splits

    97             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)

    98 apply (simp add:current_files_def is_file_def)

    99 done

   100 

   101 lemma same_inode_files_other:

   102   "\<lbrakk>valid (e # s); 

   103     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   104     \<forall> p fd. e \<noteq> CloseFd p fd;

   105     \<forall> p f. e \<noteq> UnLink p f;

   106     \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s)  = same_inode_files s"

   107 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)

   108 apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def

   109            split:if_splits option.splits

   110             dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)

   111 apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+

   112 done

   113  

   114 lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard

   115   same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other

   116 

   117 lemma same_inode_files_prop1:

   118   "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"

   119 by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)

   120 

   121 lemma same_inode_files_prop2:

   122   "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"

   123 by (auto dest:same_inode_files_prop1)

   124 

   125 lemma same_inode_files_prop3:

   126   "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"

   127 apply (rule notI)

   128 apply (simp add:same_inode_files_def is_file_def is_dir_def 

   129           split:if_splits option.splits t_inode_tag.splits)

   130 done

   131 

   132 lemma same_inode_files_prop4:

   133   "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"

   134 by (auto simp:same_inode_files_def split:if_splits)

   135 

   136 lemma same_inode_files_prop5:

   137   "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"

   138 by (auto simp:same_inode_files_def is_file_def split:if_splits)

   139 

   140 lemma same_inode_files_prop6:

   141   "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"

   142 by (auto simp:same_inode_files_def is_file_def split:if_splits)

   143 

   144 lemma same_inode_files_prop7:

   145   "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"

   146 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   147 

   148 lemma same_inode_files_prop8:

   149   "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"

   150 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   151 

   152 (* simpset for cf2sfiles *)

   153 

   154 lemma cf2sfiles_open:

   155   "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>

   156    \<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = (

   157      if (f' = f \<and> opt \<noteq> None) 

   158      then (case cf2sfile (Open p f flag fd opt # s) f of 

   159              Some sf \<Rightarrow> {sf}  

   160            | _       \<Rightarrow> {} )

   161      else cf2sfiles s f')"

   162 apply (frule vt_grant_os, frule vd_cons)

   163 apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open

   164   split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open)

   165 apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+

   166 done

   167 

   168 lemma cf2sfiles_other:

   169   "\<lbrakk>valid (e # s);

   170     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   171     \<forall> p fd. e \<noteq> CloseFd p fd;

   172     \<forall> p f. e \<noteq> UnLink p f;

   173     \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> cf2sfiles (e # s) = cf2sfiles s"

   174 apply (frule vt_grant_os, frule vd_cons, rule ext)

   175 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI)

   176 apply (drule Set.CollectD, erule bexE, rule CollectI)

   177 apply (rule_tac x = f' in bexI, case_tac e)

   178 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps

   179   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')

   180 apply (drule_tac f' = f' in cf2sfile_rmdir)

   181 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+

   182 

   183 apply (rule_tac x = f' in bexI, case_tac e)

   184 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps

   185   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')

   186 apply (drule_tac f' = f' in cf2sfile_rmdir)

   187 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+

   188 done

   189 

   190 lemma cf2sfile_linkhard1':

   191   "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>

   192    \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"

   193 apply (drule same_inode_files_prop1)

   194 by (simp add:cf2sfile_linkhard1)

   195 

   196 lemma cf2sfiles_linkhard:

   197   "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. 

   198      if (f' = f \<or> f' \<in> same_inode_files s oldf)

   199      then (case (cf2sfile (LinkHard p oldf f # s) f) of

   200              Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}

   201            | _       \<Rightarrow> {})

   202      else cf2sfiles s f')"

   203 apply (frule vt_grant_os, frule vd_cons, rule ext)

   204 apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard 

   205   split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1)

   206 done

   207 

   208 lemma cf2sfile_unlink':

   209   "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>

   210    \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"

   211 apply (drule same_inode_files_prop1)

   212 by (simp add:cf2sfile_unlink)

   213 

   214 lemma cf2sfiles_unlink:

   215   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = ( 

   216      if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 

   217          (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then 

   218         (case (cf2sfile s f) of 

   219            Some sf \<Rightarrow> cf2sfiles s f' - {sf}

   220          | _       \<Rightarrow> {})

   221      else cf2sfiles s f')"

   222 apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits)

   223 apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp)

   224 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   225 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)

   226 apply (simp add:current_files_unlink, simp, erule conjE)

   227 apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink)

   228 apply (simp add:current_files_unlink same_inode_files_prop1, simp)

   229 apply (rule_tac x = f'a in bexI, simp, simp)

   230 apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)

   231 apply (erule conjE|erule exE|erule bexE)+

   232 apply (case_tac "f'a = f", simp)

   233 apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink)

   234 apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)

   235 apply (rule_tac x = f'a in bexI, simp, simp)

   236 

   237 apply (rule impI)+

   238 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   239 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)

   240 apply (simp add:current_files_unlink, simp, (erule conjE)+)

   241 apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink)

   242 apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp)

   243 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)

   244 apply (simp add:current_files_unlink, simp)

   245 apply (case_tac "f'a = f", simp)

   246 apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp)

   247 apply (erule bexE, erule conjE)

   248 apply (rule_tac x = f'' in bexI)

   249 apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)

   250 apply (simp, simp, erule same_inode_files_prop4, simp)

   251 apply (rule_tac x = f'a in bexI)

   252 apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)

   253 apply (simp, simp)

   254 

   255 

   256 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   257 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)

   258 apply (simp add:current_files_unlink, simp)

   259 apply (rule_tac x = f'a in bexI)

   260 apply (frule_tac f' = f'a in cf2sfile_unlink)

   261 apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)

   262 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)

   263 apply (simp add:current_files_unlink, simp)

   264 apply (rule_tac x = f'a in bexI)

   265 apply (frule_tac f' = f'a in cf2sfile_unlink)

   266 apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)

   267 done

   268 

   269 lemma cf2sfiles_closefd:

   270   "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (

   271      case (file_of_proc_fd s p fd) of

   272        Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and> 

   273                     (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) 

   274                  then (case (cf2sfile s f) of 

   275                          Some sf \<Rightarrow> cf2sfiles s f' - {sf}

   276                        | _       \<Rightarrow> {})

   277                  else cf2sfiles s f'

   278      | _       \<Rightarrow> cf2sfiles s f')"

   279 

   280 apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd")

   281 apply (simp_all add:current_files_simps split:if_splits)

   282 

   283 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   284 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   285 apply (simp add:current_files_closefd, simp)

   286 apply (rule_tac x = f'a in bexI)

   287 apply (frule_tac f = f'a in cf2sfile_closefd)

   288 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)

   289 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   290 apply (simp add:current_files_closefd, simp)

   291 apply (rule_tac x = f'a in bexI)

   292 apply (frule_tac f = f'a in cf2sfile_closefd)

   293 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)

   294 

   295 apply (rule conjI, clarify, frule file_of_pfd_is_file, simp)

   296 apply (frule is_file_has_sfile', simp, erule exE, simp)

   297 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   298 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   299 apply (simp add:current_files_closefd, simp, erule conjE)

   300 apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd)

   301 apply (simp add:current_files_closefd same_inode_files_prop1, simp)

   302 apply (rule_tac x = f'a in bexI, simp, simp)

   303 apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)

   304 apply (erule conjE|erule exE|erule bexE)+

   305 apply (case_tac "f'a = a", simp)

   306 apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp)

   307 apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)

   308 apply (rule_tac x = f'a in bexI, simp, simp)

   309 

   310 apply (rule impI)+

   311 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   312 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   313 apply (simp add:current_files_closefd, simp, (erule conjE)+)

   314 apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd)

   315 apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp)

   316 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   317 apply (simp add:current_files_closefd, simp)

   318 apply (case_tac "f'a = a", simp)

   319 apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp)

   320 apply (erule bexE, erule conjE)

   321 apply (rule_tac x = f'' in bexI)

   322 apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)

   323 apply (simp, simp, erule same_inode_files_prop4, simp)

   324 apply (rule_tac x = f'a in bexI)

   325 apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)

   326 apply (simp, simp)

   327 

   328 apply (rule conjI, clarify)

   329 

   330 apply (rule impI)

   331 apply (case_tac "a \<in> files_hung_by_del s", simp_all)

   332 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   333 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   334 apply (simp add:current_files_closefd, simp)

   335 apply (rule_tac x = f'a in bexI)

   336 apply (frule_tac f = f'a in cf2sfile_closefd)

   337 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)

   338 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   339 apply (simp add:current_files_closefd, simp)

   340 apply (rule_tac x = f'a in bexI)

   341 apply (frule_tac f = f'a in cf2sfile_closefd)

   342 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)

   343 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)

   344 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   345 apply (simp add:current_files_closefd, simp)

   346 apply (rule_tac x = f'a in bexI)

   347 apply (frule_tac f = f'a in cf2sfile_closefd)

   348 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)

   349 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)

   350 apply (simp add:current_files_closefd, simp)

   351 apply (rule_tac x = f'a in bexI)

   352 apply (frule_tac f = f'a in cf2sfile_closefd)

   353 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)

   354 done

   355 

   356 lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other

   357   cf2sfiles_unlink cf2sfiles_closefd

   358   

   359 

   360 (* simpset for co2sobj *)

   361 

   362 lemma co2sobj_execve:

   363   "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (

   364       if (obj = O_proc p)

   365       then (case (cp2sproc (Execve p f fds # s) p) of

   366               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))

   367             | _       \<Rightarrow> None) 

   368       else co2sobj s obj )"

   369 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   370 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   371 apply (case_tac "cp2sproc (Execve p f fds # s) p")

   372 apply (drule current_proc_has_sp', simp, simp)

   373 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)

   374 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)

   375 apply (frule_tac ff = list in cf2sfile_other', simp_all)

   376 apply (simp add:is_dir_in_current)

   377 done

   378 

   379 lemma co2sobj_clone:

   380   "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (

   381       if (obj = O_proc p')

   382       then (case (cp2sproc (Clone p p' fds shms # s) p') of

   383               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   384             | _       \<Rightarrow> None)

   385       else co2sobj s obj )"

   386 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   387 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   388 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")

   389 apply (drule current_proc_has_sp', simp, simp)

   390 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)

   391 apply (rule conjI, rule impI, simp)

   392 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)

   393 

   394 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)

   395 apply (frule_tac ff = list in cf2sfile_other', simp_all)

   396 apply (simp add:is_dir_in_current)

   397 done

   398 

   399 lemma co2sobj_ptrace:

   400   "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (

   401      case obj of

   402        O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'') 

   403                      then (case (cp2sproc s p'') of 

   404                              Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s))

   405                            | _       \<Rightarrow> None)

   406                      else if (info_flow_shm s p p'')

   407                           then (case (cp2sproc s p'') of 

   408                                   Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s))

   409                                 | _       \<Rightarrow> None)

   410                           else co2sobj s (O_proc p'')

   411     | _          \<Rightarrow> co2sobj s obj)"

   412 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   413 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)

   414 

   415 apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits

   416   dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   417 

   418 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)

   419 apply (frule_tac ff = list in cf2sfile_other', simp_all)

   420 apply (simp add:is_dir_in_current)

   421 done

   422 

   423 lemma co2sobj_open:

   424   "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk> 

   425    \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of 

   426      O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)

   427                   then (case (cf2sfile (Open p f flag fd opt # s) f) of

   428                           Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))

   429                         | _       \<Rightarrow> None)

   430                   else co2sobj s (O_file f')

   431    | O_proc p' \<Rightarrow> if (p' = p) 

   432                   then (case (cp2sproc (Open p f flag fd opt # s) p) of

   433                           Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   434                         | _       \<Rightarrow> None)

   435                   else co2sobj s (O_proc p')

   436    | _         \<Rightarrow> co2sobj s obj )"

   437 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   438 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits

   439            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   440 

   441 apply (simp split:if_splits t_object.splits)

   442 apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+)

   443 apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f")

   444 apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)

   445 apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps)

   446 apply (simp add:tainted_eq_Tainted)

   447 apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current)

   448 apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits)

   449 

   450 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   451 

   452 apply (frule is_dir_in_current)

   453 apply (frule_tac f' = list in cf2sfile_open)

   454 apply (simp add:current_files_simps split:option.splits)

   455 apply (simp split:if_splits option.splits)

   456 done

   457 

   458 lemma co2sobj_readfile:

   459   "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (

   460      case obj of

   461        O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of

   462                        Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s)

   463                                   then (case (cp2sproc s p') of

   464                                           Some sp \<Rightarrow> Some (S_proc sp True)

   465                                         | _       \<Rightarrow> None)

   466                                   else co2sobj s obj)

   467                     | _       \<Rightarrow> None)

   468      | _         \<Rightarrow> co2sobj s obj)"

   469 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   470 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits

   471            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   472 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   473 

   474 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 

   475              simp:current_files_simps cf2sfiles_simps cf2sfile_simps 

   476              dest:is_file_in_current is_dir_in_current)

   477 done

   478 

   479 lemma co2sobj_writefile:

   480   "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (

   481      case obj of

   482        O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of

   483                        Some f \<Rightarrow> (if (f \<in> same_inode_files s f') 

   484                                   then Some (S_file (cf2sfiles s f') 

   485                                                     (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))

   486                                   else co2sobj s obj)

   487                     | _       \<Rightarrow> None)

   488      | _         \<Rightarrow> co2sobj s obj)"

   489 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   490 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   491 

   492 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   493              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   494                   same_inode_files_prop6

   495              dest:is_file_in_current is_dir_in_current)

   496 

   497 (* should delete has_same_inode !?!?*)

   498 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   499 

   500 lemma co2sobj_closefd:

   501   "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (

   502       case obj of 

   503         O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of 

   504                         Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>

   505                                        f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f. 

   506                                        f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))

   507                                    then (case (cf2sfile s f, co2sobj s (O_file f')) of

   508                                            (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)

   509                                          | _                              \<Rightarrow> None)

   510                                    else co2sobj s obj)

   511                      | _       \<Rightarrow> co2sobj s obj)

   512       | O_proc p' \<Rightarrow> (if (p = p') 

   513                       then (case (cp2sproc (CloseFd p fd # s) p) of

   514                               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   515                             | _       \<Rightarrow> None)

   516                       else co2sobj s obj)

   517       | _         \<Rightarrow> co2sobj s obj) "

   518 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   519 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   520 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   521            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   522 

   523 apply (frule is_file_in_current)

   524 apply (case_tac "file_of_proc_fd s p fd")

   525 apply (simp add:tainted_eq_Tainted)

   526 apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp)

   527 apply (frule_tac f' = list in cf2sfiles_closefd, simp)

   528 apply (simp add:is_file_simps current_files_simps)

   529 apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits

   530   dest!:current_file_has_sfile' dest:hung_file_in_current)[1]

   531 

   532 apply (simp add:is_dir_simps, frule is_dir_in_current)

   533 apply (frule_tac f = list in cf2sfile_closefd)

   534 apply (clarsimp simp:current_files_closefd split:option.splits)

   535 apply (drule file_of_pfd_is_file', simp+)

   536 done

   537 

   538 lemma co2sobj_unlink:

   539   "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (

   540       case obj of

   541         O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 

   542                         (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))

   543                      then (case (cf2sfile s f, co2sobj s (O_file f')) of

   544                              (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)

   545                            | _                              \<Rightarrow> None)

   546                      else co2sobj s obj

   547       | _         \<Rightarrow> co2sobj s obj)"

   548 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   549 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   550 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   551            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   552 apply (frule is_file_in_current)

   553 apply (frule_tac f' = list in cf2sfile_unlink, simp)

   554 apply (frule_tac f' = list in cf2sfiles_unlink, simp)

   555 apply (simp add:is_file_simps current_files_simps)

   556 apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits

   557   dest!:current_file_has_sfile')[1]

   558 

   559 apply (simp add:is_dir_simps, frule is_dir_in_current)

   560 apply (frule_tac f' = list in cf2sfile_unlink)

   561 apply (clarsimp simp:current_files_unlink split:option.splits)

   562 apply (drule file_dir_conflict, simp+)

   563 done

   564 

   565 lemma co2sobj_rmdir:

   566   "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"

   567 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   568 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   569 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   570            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   571 apply (simp add:is_file_simps dir_is_empty_def)

   572 apply (case_tac "f = list", drule file_dir_conflict, simp, simp)

   573 apply (simp add:cf2sfiles_other)

   574 apply (auto simp:cf2sfile_simps dest:is_dir_in_current)

   575 done

   576 

   577 lemma co2sobj_mkdir:

   578   "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (

   579       if (obj = O_dir f) 

   580       then (case (cf2sfile (Mkdir p f i # s) f) of 

   581               Some sf \<Rightarrow> Some (S_dir sf)

   582             | _       \<Rightarrow> None)

   583       else co2sobj s obj)"

   584 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   585 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   586 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   587            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   588 apply (frule_tac cf2sfiles_other, simp+)

   589 apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir)

   590 apply (frule current_file_has_sfile, simp, erule exE, simp)

   591 apply (drule cf2sfile_mkdir1, simp+)

   592 done

   593 

   594 lemma same_inodes_Tainted:

   595   "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"

   596 apply (frule same_inode_files_prop8, frule same_inode_files_prop7)

   597 apply (auto intro:has_same_inode_Tainted)

   598 done

   599 

   600 lemma co2sobj_linkhard:

   601   "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> 

   602    \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (

   603     case obj of

   604       O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)

   605                    then (case (cf2sfile (LinkHard p oldf f # s) f) of

   606                            Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s))

   607                          | _       \<Rightarrow> None)

   608                    else co2sobj s obj

   609     | _         \<Rightarrow> co2sobj s obj)"

   610 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   611 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   612 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   613            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   614 apply (frule_tac cf2sfiles_linkhard, simp+)

   615 apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard)

   616 apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted

   617   split:option.splits if_splits dest:Tainted_in_current 

   618   dest!:current_has_sec' current_file_has_sfile')[1]

   619 

   620 apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current)

   621 apply (frule is_dir_in_current)

   622 apply (frule current_file_has_sfile, simp)

   623 apply (drule cf2sfile_linkhard1, simp+)

   624 done

   625 

   626 lemma co2sobj_truncate:

   627   "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (

   628       case obj of

   629         O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)

   630                      then Some (S_file (cf2sfiles s f') (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))

   631                      else co2sobj s obj

   632       | _         \<Rightarrow> co2sobj s obj)"

   633 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   634 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   635 

   636 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   637              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   638                   same_inode_files_prop6

   639              dest:is_file_in_current is_dir_in_current)

   640 

   641 (* should delete has_same_inode !?!?*)

   642 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   643 

   644 lemma co2sobj_kill:

   645   "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"

   646 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   647 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   648 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   649              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   650                   same_inode_files_prop6

   651              dest:is_file_in_current is_dir_in_current)

   652 done

   653 

   654 lemma co2sobj_exit:

   655   "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"

   656 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   657 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   658 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   659              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   660                   same_inode_files_prop6

   661              dest:is_file_in_current is_dir_in_current)

   662 done

   663 

   664 lemma co2sobj_createmsgq:

   665   "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (

   666       case obj of

   667         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of

   668                                          Some sq \<Rightarrow> Some (S_msgq sq)

   669                                        | _       \<Rightarrow> None)

   670                      else co2sobj s obj

   671       | _        \<Rightarrow> co2sobj s obj)"

   672 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   673 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   674 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   675              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   676                   same_inode_files_prop6

   677              dest!:current_has_smsgq'

   678              dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)

   679 done

   680 

   681 lemma co2sobj_sendmsg:

   682   "\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (

   683       case obj of

   684         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of

   685                                          Some sq \<Rightarrow> Some (S_msgq sq)

   686                                        | _       \<Rightarrow> None)

   687                      else co2sobj s obj

   688       | _        \<Rightarrow> co2sobj s obj)"

   689 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   690 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   691 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   692              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   693                   same_inode_files_prop6

   694              dest!:current_has_smsgq'

   695              dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)

   696 done

   697 

   698 lemma co2sobj_recvmsg:

   699   "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (

   700       case obj of

   701         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of

   702                                          Some sq \<Rightarrow> Some (S_msgq sq)

   703                                        | _       \<Rightarrow> None)

   704                      else co2sobj s obj

   705       | O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s)

   706                      then (case (cp2sproc s p') of

   707                              Some sp \<Rightarrow> Some (S_proc sp True)

   708                            | _       \<Rightarrow> None)

   709                      else co2sobj s obj

   710       | _         \<Rightarrow> co2sobj s obj)"

   711 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   712 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   713 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   714              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   715                   same_inode_files_prop6

   716              dest!:current_has_smsgq'

   717              dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)

   718 done

   719 

   720 lemma co2sobj_removemsgq:

   721   "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk> 

   722    \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"

   723 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   724 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   725 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   726              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   727                   same_inode_files_prop6

   728              dest!:current_has_smsgq'

   729              dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)

   730 done

   733   "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = co2sobj s obj"

    12   "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (

    13       case obj of 

    14         O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of

    15                                         Some sh \<Rightarrow> Some (S_shm sh)

    16                                       | _       \<Rightarrow> None)

    17                     else co2sobj s obj

    18       | _        \<Rightarrow> co2sobj s obj)"