1 (*<*)

     2 theory S2ss_prop

     3 imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop

     4 begin

     5 (*>*)

     6 

     7 context tainting_s begin

     8 

     9 (* simpset for s2ss*)

    10 

    11 lemma co2sobj_some_case:

    12   "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);

    13     \<And> f. obj = O_file f \<Longrightarrow> P (O_file f);

    14     \<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>

    15    \<Longrightarrow> P obj" (*  \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h); *)

    16 by (case_tac obj, auto)

    17 

    18 lemma co2sobj_execve_alive:

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

    20    \<Longrightarrow> alive (Execve p f fds # s) obj"

    21 apply (erule co2sobj_some_case)

    22 by (auto simp:alive_simps simp del:alive.simps)

    23 

    24 lemma s2ss_execve':

    25   "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (

    26      if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))

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

    28              Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}

    29            | _ \<Rightarrow> {} )

    30      else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of

    31              (Some sp, Some sp') \<Rightarrow> s2ss s - {S_proc sp' (O_proc p \<in> tainted s)}

    32                                     \<union> {S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s)}

    33            | _ \<Rightarrow> {} ) )"

    34 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)

    35 

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

    37 apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)

    38 apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp)

    39 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)")

    40 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)

    41 apply (erule exE, simp)

    42 apply (simp add:s2ss_def, rule set_eqI, rule iffI)

    43 apply (drule CollectD, (erule exE|erule conjE)+)

    44 apply (case_tac "obj = O_proc p")

    45 apply (simp add:co2sobj_execve split:if_splits)

    46 apply (simp add:co2sobj_execve, rule disjI2)

    47 apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1]

    48 apply (simp, erule disjE)

    49 apply (rule_tac x = "O_proc p" in exI, simp)

    50 apply (erule exE| erule conjE)+

    51 apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")

    52 apply (rule_tac x = "O_proc p'" in exI)

    53 apply (simp add:alive_execve co2sobj_execve cp2sproc_execve)

    54 apply (case_tac "obj = O_proc p", simp)

    55 apply (frule co2sobj_execve_alive, simp, simp)

    56 apply (frule_tac obj = obj in co2sobj_execve, simp)

    57 apply (rule_tac x = obj in exI, simp, simp)

    58 

    59 apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp)

    60 apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") 

    61 apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)

    62 apply (erule exE, erule conjE, simp)

    63 apply (simp add:s2ss_def, rule set_eqI, rule iffI)

    64 apply (drule CollectD, (erule exE|erule conjE)+)

    65 apply (case_tac "obj = O_proc p", simp)

    66 apply (rule disjI1, simp split:if_splits)

    67 apply (simp add:co2sobj_execve, rule disjI2)

    68 apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)

    69 apply (rule notI, simp, case_tac obj)

    70 apply (erule_tac x = nat in allE, simp, (simp split:option.splits)+)

    71 apply (erule disjE, simp)

    72 apply (rule_tac x = "O_proc p" in exI, simp)

    73 apply (erule exE|erule conjE)+

    74 apply (rule_tac x = obj in exI)

    75 apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)

    76 apply (frule_tac obj = obj in co2sobj_execve, simp, simp)

    77 apply (rule impI, simp, simp)

    78 done

    79 

    80 lemma s2ss_clone_alive:

    81   "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds # s)\<rbrakk>

    82    \<Longrightarrow> alive (Clone p p' fds # s) obj"

    83 by (erule co2sobj_some_case, auto simp:alive_clone)

    84 

    85 lemma s2ss_clone:

    86   "valid (Clone p p' fds # s) \<Longrightarrow> s2ss (Clone p p' fds # s) = (

    87      case (cp2sproc (Clone p p' fds # s) p') of

    88        Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> tainted s)}

    89      | _       \<Rightarrow> {})"

    90 apply (frule vd_cons, frule vt_grant_os, split option.splits)

    91 apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)

    92 apply (rule allI, rule impI, simp add:s2ss_def)

    93 apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)

    94 apply (case_tac "obj = O_proc p'", simp)

    95 apply (case_tac "O_proc p' \<in> tainted s", drule tainted_in_current, simp+)

    96 apply (rule disjI1, simp split:if_splits)

    97 apply (simp, rule disjI2)

    98 apply (frule co2sobj_clone, simp)

    99 apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)

   100 

   101 apply (simp, erule disjE, simp)

   102 apply (rule_tac x = "O_proc p'" in exI, simp)

   103 apply (rule impI, rule notI, drule tainted_in_current, simp+)

   104 apply (erule exE| erule conjE)+

   105 apply (case_tac "obj = O_proc p'", simp)

   106 apply (rule_tac x = obj in exI)

   107 apply (frule s2ss_clone_alive, simp+)

   108 apply (auto simp:co2sobj_clone alive_simps)

   109 done

   110 

   111 (*

   112 definition s2ss_shm_no_backup:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state"

   113 where

   114   "s2ss_shm_no_backup s pfrom \<equiv> {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and>

   115      (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)))}"

   116 

   117 definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" 

   118 where

   119   "update_s2ss_shm s pfrom \<equiv> s2ss s 

   120      \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}

   121      - (s2ss_shm_no_backup s pfrom)"

   122 

   123 lemma s2ss_shm_no_bk_elim:

   124   "\<lbrakk>S_proc sp False \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some (S_proc sp False); 

   125     valid s; info_flow_shm s pfrom p\<rbrakk>

   126    \<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)"

   127 apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)

   128 apply (erule_tac x = p in allE, auto)

   129 apply (rule_tac x = p' in exI, auto)

   130 done

   131 

   132 lemma s2ss_shm_no_bk_intro1:

   133   "\<lbrakk>co2sobj s' obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   134 apply (case_tac obj)

   135 apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)

   136 done

   137 

   138 lemma s2ss_shm_no_bk_intro2:

   139   "\<lbrakk>co2sobj s' obj = Some x; obj \<in> tainted s'; valid s'\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   140 apply (case_tac obj)

   141 

   142 apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)

   143 done

   144 

   145 lemma s2ss_shm_no_bk_intro3:

   146   "\<lbrakk>co2sobj s (O_proc p) = Some x; \<not> info_flow_shm s pfrom p; p \<in> current_procs s

   147    \<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   148 apply (auto simp add:s2ss_shm_no_backup_def split:option.splits)

   149 apply (rule_tac x = p in exI, simp)

   150 done

   151 

   152 lemma s2ss_shm_no_bk_intro4:

   153   "\<lbrakk>co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p; 

   154     \<not> info_flow_shm s pfrom p'; p' \<in> current_procs s; co2sobj s (O_proc p') = Some x\<rbrakk>

   155    \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

   156 apply (rule notI)

   157 apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)

   158 done  

   159 *)

   160 

   161 lemma tainted_ptrace':

   162   "tainted (Ptrace p p' # s) = 

   163      (if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s)

   164       then tainted s \<union> {O_proc p'}

   165       else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)

   166            then tainted s \<union> {O_proc p}

   167                 else tainted s)"

   168 by auto

   169 

   170 lemma co2sobj_some_caseD:

   171   "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);

   172     \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); 

   173     \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_dir f\<rbrakk> \<Longrightarrow> P (O_dir f); 

   174     \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk>

   175    \<Longrightarrow> P obj"

   176 by (case_tac obj, auto)

   177 

   178 definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

   179 where

   180   "update_s2ss_obj s ss obj sobj sobj' = 

   181      (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)

   182       then ss \<union> {sobj'}

   183       else ss - {sobj} \<union> {sobj'})"

   184 

   185 ML {*

   186 fun my_setiff_tac i = 

   187      (etac @{thm CollectE} i 

   188       ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i

   189               THEN etac @{thm disjE} i)

   190       ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i

   191               THEN etac @{thm conjE} i 

   192               THEN (REPEAT (etac @{thm CollectE} i))))

   193 THEN (REPEAT ((        etac @{thm exE} 

   194                ORELSE' etac @{thm conjE}

   195                ORELSE' etac @{thm bexE}) i))

   196 THEN (rtac @{thm CollectI} i

   197       ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i))

   198 

   199 *}

   200 

   201 ML {*

   202 fun my_seteq_tac i = 

   203      (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1)

   204 THEN (rtac @{thm set_eqI} i)

   205 THEN (rtac @{thm iffI} i)

   206 THEN my_setiff_tac i

   207 *}

   208 

   209 ML {*fun my_clarify_tac i = 

   210 REPEAT ((  rtac @{thm impI}

   211    ORELSE' rtac @{thm allI}

   212    ORELSE' rtac @{thm ballI}

   213    ORELSE' rtac @{thm conjI}

   214    ORELSE' etac @{thm conjE}

   215    ORELSE' etac @{thm exE}

   216    ORELSE' etac @{thm bexE}

   217    ORELSE' etac @{thm disjE}) i)

   218 *}

   219 

   220 lemma co2sobj_sproc_imp:

   221   "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"

   222 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   223 

   224 lemma co2sobj_sfile_imp:

   225   "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"

   226 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   227 

   228 lemma co2sobj_sdir_imp:

   229   "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"

   230 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   231 

   232 lemma co2sobj_smsgq_imp:

   233   "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"

   234 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   235 

   236 lemma s2ss_execve:

   237   "valid (Execve p f fds # s) \<Longrightarrow> 

   238      (case (cp2sproc s p, cp2sproc (Execve p f fds # s) p) of

   239         (Some sp, Some sp') \<Rightarrow> s2ss (Execve p f fds # s) = 

   240             update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp (O_proc p \<in> tainted s))

   241                           (S_proc sp' (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))

   242       | _ \<Rightarrow> s2ss (Execve p f fds # s) = {})"

   243 apply (frule vd_cons, frule vt_grant_os)

   244 apply (clarsimp simp only:os_grant.simps)

   245 apply (case_tac "cp2sproc s p")

   246 apply (drule current_proc_has_sp', simp, simp)

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

   248 apply (drule current_proc_has_sp', simp, simp, simp)

   249 apply (simp add:update_s2ss_obj_def)

   250 apply (tactic {*my_clarify_tac 1*})

   251 apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)

   252 apply (simp add:s2ss_execve')

   253 apply (rule impI)

   254 apply (erule_tac x = pa in allE, simp)

   255 apply (rule impI)

   256 apply (simp add:s2ss_execve')

   257 apply (rule impI)

   258 apply (tactic {*my_clarify_tac 1*})

   259 apply (simp split:option.splits)

   260 apply (erule_tac x = "O_proc p'" in allE, simp)

   261 done

   262 

   263 lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp

   264 

   265 lemma s2ss_ptrace1:

   266   "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> tainted s; O_proc p' \<notin> tainted s\<rbrakk>

   267    \<Longrightarrow> (case (cp2sproc s p') of 

   268           Some sp' \<Rightarrow> s2ss (Ptrace p p' # s) = 

   269                      update_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp' False) (S_proc sp' True)

   270         | _        \<Rightarrow> s2ss (Ptrace p p' # s) = {})"

   271 apply (frule vd_cons, frule vt_grant_os)

   272 apply (clarsimp simp only:os_grant.simps)

   273 apply (case_tac "cp2sproc s p'")

   274 apply (drule current_proc_has_sp', simp+)

   275 apply (case_tac "cp2sproc s p")

   276 apply (drule current_proc_has_sp', simp+)

   277 

   278 apply (simp add:update_s2ss_obj_def)

   279 apply (tactic {*my_clarify_tac 1*})

   280 apply (simp add:s2ss_def)

   281 apply (tactic {*my_seteq_tac 1*})

   282 apply (case_tac "obj = O_proc p'")

   283 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   284 apply (rule disjI2, simp, rule_tac x = obj in exI)

   285 apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)

   286 apply (tactic {*my_setiff_tac 1*})

   287 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)

   288 apply (tactic {*my_setiff_tac 1*})

   289 apply (case_tac "obj = O_proc p'")

   290 apply (rule_tac x = obj' in exI)

   291 apply (simp add:co2sobj_ptrace alive_other split:t_object.splits if_splits)

   292 apply (auto simp:co2sobj.simps)[1]

   293 apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)

   294 apply (auto simp:co2sobj.simps)[1]

   295 

   296 apply (rule impI)

   297 apply (simp add:s2ss_def)

   298 apply (tactic {*my_seteq_tac 1*})

   299 apply (case_tac "obj = O_proc p'")

   300 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   301 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)

   302 apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)

   303 apply (rule notI, simp)

   304 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)

   305 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)

   306 apply (tactic {*my_setiff_tac 1*})

   307 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj.simps cp2sproc_other)

   308 apply (tactic {*my_setiff_tac 1*})

   309 apply (case_tac "obj = O_proc p'")

   310 apply (simp add:co2sobj.simps cp2sproc_other)

   311 apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)

   312 apply (auto simp:co2sobj.simps)[1]

   313 done

   314 

   315 lemma s2ss_ptrace2:

   316   "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> tainted s; O_proc p \<notin> tainted s\<rbrakk>

   317    \<Longrightarrow> (case (cp2sproc s p) of 

   318           Some sp \<Rightarrow> s2ss (Ptrace p p' # s) = 

   319                     update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)

   320         | _       \<Rightarrow> s2ss (Ptrace p p' # s) = {})"

   321 apply (frule vd_cons, frule vt_grant_os)

   322 apply (clarsimp simp only:os_grant.simps)

   323 apply (case_tac "cp2sproc s p'")

   324 apply (drule current_proc_has_sp', simp+)

   325 apply (case_tac "cp2sproc s p")

   326 apply (drule current_proc_has_sp', simp+)

   327 

   328 apply (simp add:update_s2ss_obj_def)

   329 apply (tactic {*my_clarify_tac 1*})

   330 apply (simp add:s2ss_def)

   331 apply (tactic {*my_seteq_tac 1*})

   332 apply (case_tac "obj = O_proc p")

   333 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   334 apply (rule disjI2, simp, rule_tac x = obj in exI)

   335 apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)

   336 apply (tactic {*my_setiff_tac 1*})

   337 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)

   338 apply (tactic {*my_setiff_tac 1*})

   339 apply (case_tac "obj = O_proc p")

   340 apply (rule_tac x = obj' in exI)

   341 apply (simp add:co2sobj_ptrace alive_other split:t_object.splits if_splits)

   342 apply (auto simp:co2sobj.simps)[1]

   343 apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)

   344 apply (auto simp:co2sobj.simps)[1]

   345 

   346 apply (rule impI)

   347 apply (simp add:s2ss_def)

   348 apply (tactic {*my_seteq_tac 1*})

   349 apply (case_tac "obj = O_proc p")

   350 apply (rule disjI1, simp add:co2sobj.simps cp2sproc_other)

   351 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)

   352 apply (simp add:co2sobj_ptrace is_file_simps is_dir_simps alive_other split:t_object.splits if_splits)

   353 apply (rule notI, simp)

   354 apply (frule_tac obj = obj in co2sobj_sproc_imp, erule exE, simp)

   355 apply (erule_tac x = obj in allE, simp add:co2sobj_ptrace cp2sproc_other split:option.splits)

   356 apply (tactic {*my_setiff_tac 1*})

   357 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps cp2sproc_other)

   358 apply (tactic {*my_setiff_tac 1*})

   359 apply (case_tac "obj = O_proc p")

   360 apply (simp add:co2sobj.simps cp2sproc_other)

   361 apply (rule_tac x = obj in exI, simp add:co2sobj_ptrace alive_other split:t_object.splits)

   362 apply (auto simp:co2sobj.simps)[1]

   363 done

   364 

   365 lemma s2ss_ptrace3:

   366   "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> tainted s) = (O_proc p \<in> tainted s)\<rbrakk>

   367    \<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s"

   368 unfolding s2ss_def

   369 apply (frule vd_cons, frule vt_grant_os, rule set_eqI, rule iffI)

   370 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   371 apply (rule_tac x = obj in exI)

   372 apply (frule alive_other, simp+)

   373 apply (frule_tac obj = obj in co2sobj_ptrace, simp)

   374 apply (auto split:t_object.splits option.splits if_splits)[1]

   375 

   376 apply (tactic {*my_setiff_tac 1*})

   377 apply (rule_tac x = obj in exI)

   378 apply (frule alive_other, simp+)

   379 apply (frule_tac obj = obj in co2sobj_ptrace, simp)

   380 apply (case_tac "cp2sproc s p'")

   381 apply (drule current_proc_has_sp', simp, simp)

   382 apply (case_tac "cp2sproc s p")

   383 apply (drule current_proc_has_sp', simp, simp)

   384 apply (case_tac "O_proc p' \<in> tainted s")

   385 apply (auto split:t_object.splits option.splits if_splits simp:co2sobj.simps)

   386 done

   387 

   388 lemma s2ss_ptrace:

   389   "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (

   390      if (O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s) 

   391      then (case (cp2sproc s p') of 

   392              Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp False) (S_proc sp True)

   393            | _       \<Rightarrow> {})

   394      else if (O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s)

   395           then (case (cp2sproc s p) of 

   396                   Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)

   397                 | _       \<Rightarrow> {})

   398           else s2ss s                                   )"

   399 apply (case_tac "O_proc p \<in> tainted s \<and> O_proc p' \<notin> tainted s")

   400 apply (drule s2ss_ptrace1, simp, simp, simp split:option.splits)

   401 apply (case_tac "O_proc p' \<in> tainted s \<and> O_proc p \<notin> tainted s")

   402 apply (drule s2ss_ptrace2, simp, simp, simp split:option.splits)

   403 apply (drule s2ss_ptrace3, auto)

   404 done

   405 

   406 lemma s2ss_kill':

   407   "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = (

   408      if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p'))

   409      then s2ss s 

   410      else (case (co2sobj s (O_proc p')) of

   411              Some sp \<Rightarrow> s2ss s - {sp}

   412            | _       \<Rightarrow> {}))"

   413 apply (frule vt_grant_os, frule vd_cons)

   414 unfolding s2ss_def

   415 apply (simp split:if_splits, rule conjI)

   416 apply (rule impI, (erule exE|erule conjE)+)

   417 apply (split option.splits)

   418 apply (drule current_proc_has_sp', simp, simp)

   419 apply (simp split: option.splits, (erule conjE)+)

   420 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   421 apply (rule_tac x = obj in exI)

   422 apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)

   423 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

   424 apply (erule co2sobj_some_caseD)

   425 apply (case_tac "pa = p'")

   426 apply (rule_tac x = "O_proc p''" in exI)

   427 apply (simp add:cp2sproc_kill alive_kill

   428   split:t_object.splits if_splits option.splits)

   429 apply (rule_tac x = "O_proc pa" in exI)

   430 apply (clarsimp simp add:cp2sproc_kill alive_kill

   431   split:t_object.splits if_splits option.splits)

   432 apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+

   433 

   434 apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp)

   435 apply (rule set_eqI, rule iffI)

   436 apply (erule CollectE, erule exE, erule conjE, rule DiffI)

   437 apply (rule CollectI, rule_tac x = obj in exI)

   438 apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits)

   439 apply (rule notI, simp, case_tac obj)

   440 apply (erule_tac x = nat in allE)

   441 apply (simp add:co2sobj_kill cp2sproc_kill split:option.splits)

   442 apply (simp split:option.splits)+

   443 apply (erule co2sobj_some_caseD)

   444 apply (case_tac "pa = p'")

   445 apply (rule_tac x = "O_proc p''" in exI)

   446 apply (simp add:cp2sproc_kill alive_kill

   447   split:t_object.splits if_splits option.splits)

   448 apply (rule_tac x = "O_proc pa" in exI)

   449 apply (clarsimp simp add:cp2sproc_kill alive_kill

   450   split:t_object.splits if_splits option.splits)

   451 apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+

   452 done

   453 

   454 definition del_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

   455 where

   456   "del_s2ss_obj s ss obj sobj \<equiv> 

   457      if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)

   458      then ss

   459      else ss - {sobj}"

   460 

   461 lemma del_update_s2ss_obj:

   462   "update_s2ss_obj s ss obj sobj sobj' = del_s2ss_obj s ss obj sobj \<union> {sobj'}"

   463 by (auto simp:update_s2ss_obj_def del_s2ss_obj_def split:if_splits)

   464 

   465 lemma s2ss_kill:

   466   "valid (Kill p p' # s) \<Longrightarrow> (

   467       case (cp2sproc s p') of 

   468         Some sp \<Rightarrow> s2ss (Kill p p' # s) = del_s2ss_obj s (s2ss s) (O_proc p') (S_proc sp (O_proc p' \<in> tainted s))

   469       | _       \<Rightarrow> s2ss (Kill p p' # s) = {})"

   470 apply (frule vd_cons, frule vt_grant_os)

   471 apply (clarsimp simp only:os_grant.simps)

   472 apply (split option.splits, rule conjI, rule impI)

   473 apply (drule current_proc_has_sp', simp, simp)

   474 apply (rule allI, rule impI)

   475 apply (simp add:del_s2ss_obj_def split:option.splits)

   476 apply (tactic {*my_clarify_tac 1*})

   477 apply (frule co2sobj_sproc_imp, erule exE)

   478 apply (simp add:s2ss_kill')

   479 apply (rule impI)

   480 apply (erule_tac x = pa in allE, simp)

   481 apply (rule impI)

   482 apply (simp add:s2ss_kill')

   483 apply (rule impI)

   484 apply (tactic {*my_clarify_tac 1*})

   485 apply (simp split:option.splits)

   486 apply (erule_tac x = "O_proc p''" in allE, simp)

   487 done

   488 

   489 lemma s2ss_exit':

   490   "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = (

   491      if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))

   492      then s2ss s 

   493      else (case (co2sobj s (O_proc p)) of

   494              Some sp \<Rightarrow> s2ss s - {sp}

   495            | _       \<Rightarrow> {}))"

   496 apply (frule vt_grant_os, frule vd_cons)

   497 unfolding s2ss_def

   498 apply (simp split:if_splits, rule conjI)

   499 apply (rule impI, (erule exE|erule conjE)+)

   500 apply (split option.splits)

   501 apply (drule current_proc_has_sp', simp, simp)

   502 apply (simp split: option.splits, (erule conjE)+)

   503 apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)

   504 apply (rule_tac x = obj in exI)

   505 apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)

   506 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

   507 apply (erule co2sobj_some_caseD)

   508 apply (case_tac "pa = p")

   509 apply (rule_tac x = "O_proc p'" in exI)

   510 apply (simp add:cp2sproc_exit alive_exit

   511   split:t_object.splits if_splits option.splits)

   512 apply (rule_tac x = "O_proc pa" in exI)

   513 apply (clarsimp simp add:cp2sproc_exit alive_exit

   514   split:t_object.splits if_splits option.splits)

   515 apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+

   516 

   517 apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp)

   518 apply (rule set_eqI, rule iffI)

   519 apply (erule CollectE, erule exE, erule conjE, rule DiffI)

   520 apply (rule CollectI, rule_tac x = obj in exI)

   521 apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits)

   522 apply (rule notI, simp, case_tac obj)

   523 apply (erule_tac x = nat in allE)

   524 apply (simp add:co2sobj_exit cp2sproc_exit split:option.splits)

   525 apply (simp split:option.splits)+

   526 apply (erule co2sobj_some_caseD)

   527 apply (case_tac "pa = p")

   528 apply (rule_tac x = "O_proc p'" in exI)

   529 apply (simp add:cp2sproc_exit alive_exit

   530   split:t_object.splits if_splits option.splits)

   531 apply (rule_tac x = "O_proc pa" in exI)

   532 apply (clarsimp simp add:cp2sproc_exit alive_exit

   533   split:t_object.splits if_splits option.splits)

   534 apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+

   535 done

   536 

   537 lemma s2ss_exit:

   538   "valid (Exit p # s) \<Longrightarrow> (

   539       case (cp2sproc s p) of 

   540         Some sp \<Rightarrow> s2ss (Exit p # s) = del_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp (O_proc p \<in> tainted s))

   541       | _       \<Rightarrow> s2ss (Exit p # s) = {})"

   542 apply (frule vd_cons, frule vt_grant_os)

   543 apply (clarsimp simp only:os_grant.simps)

   544 apply (split option.splits, rule conjI, rule impI)

   545 apply (drule current_proc_has_sp', simp, simp)

   546 apply (rule allI, rule impI)

   547 apply (simp add:del_s2ss_obj_def split:option.splits)

   548 apply (tactic {*my_clarify_tac 1*})

   549 apply (frule co2sobj_sproc_imp, erule exE)

   550 apply (simp add:s2ss_exit')

   551 apply (rule impI)

   552 apply (erule_tac x = pa in allE, simp)

   553 apply (rule impI)

   554 apply (simp add:s2ss_exit')

   555 apply (rule impI)

   556 apply (tactic {*my_clarify_tac 1*})

   557 apply (simp split:option.splits)

   558 apply (erule_tac x = "O_proc p'" in allE, simp)

   559 done

   560 

   561 lemma alive_has_sobj':

   562   "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"

   563 apply (case_tac obj)

   564 apply (auto split:option.splits)

   565 oops

   566 

   567 declare co2sobj.simps [simp del]

   568 

   569 lemma co2sobj_open_none:

   570   "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (

   571       if (obj = O_proc p) 

   572       then (case (cp2sproc (Open p f flag fd None # s) p) of

   573               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))

   574            | _       \<Rightarrow> None)

   575       else co2sobj s obj)"

   576 apply (frule vt_grant_os, frule vd_cons)

   577 apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)

   578 apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')

   579 done

   580 

   581 lemma co2sobj_open_some:

   582   "\<lbrakk>valid (Open p f flag fd (Some i) # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (

   583       if (obj = O_proc p) 

   584       then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of

   585               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))

   586            | _       \<Rightarrow> None)

   587       else if (obj = O_file f) 

   588            then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of

   589                    Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))

   590                  | _       \<Rightarrow> None)

   591            else co2sobj s obj)"

   592 apply (frule vt_grant_os, frule vd_cons)

   593 apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)

   594 apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')

   595 done

   596 

   597 lemma alive_co2sobj_some_open_none:

   598   "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk>

   599    \<Longrightarrow> alive (Open p f flag fd None # s) obj"

   600 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

   601 

   602 lemma alive_co2sobj_some_open_none':

   603   "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; 

   604     valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj"

   605 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

   606 

   607 lemma co2sobj_proc_obj:

   608   "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk>

   609    \<Longrightarrow> \<exists> p'. obj = O_proc p'"

   610 by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

   611 

   612 lemma s2ss_open_none:

   613   "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = (

   614       case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of

   615         (Some sp, Some sp') \<Rightarrow> 

   616            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   617            then s2ss s \<union> {sp'}

   618            else s2ss s - {sp} \<union> {sp'} 

   619       | _                   \<Rightarrow> {} )"

   620 unfolding s2ss_def

   621 apply (frule vt_grant_os, frule vd_cons)

   622 apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)

   623 apply (drule current_proc_has_sp', simp, simp)

   624 apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)")

   625 apply (simp add:co2sobj.simps split:option.splits)

   626 apply (drule current_proc_has_sp', simp, simp)

   627 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp)

   628 apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp)

   629 apply (rule conjI, rule impI, erule exE, (erule conjE)+)

   630 apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp)

   631 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)

   632 apply (rule impI)

   633 apply (case_tac "obj = O_proc p", simp)

   634 apply (rule Meson.disj_comm, rule disjCI, rule conjI)

   635 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)

   636 apply (simp add:co2sobj_open_none split:option.splits)

   637 apply (rule notI)

   638 apply (frule co2sobj_proc_obj, simp, erule exE)

   639 apply (erule_tac x = p' in allE, simp)

   640 

   641 apply (simp split:if_splits)

   642 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)

   643 apply (erule exE, erule conjE, case_tac "obj = O_proc p")

   644 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)

   645 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)

   646 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)

   647 apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p")

   648 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)

   649 apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)

   650 done

   651 

   652 lemma alive_co2sobj_some_open_some:

   653   "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk>

   654    \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj"

   655 by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps)

   656 

   657 lemma alive_co2sobj_some_open_some':

   658   "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; 

   659     valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj"

   660 by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

   661 

   662 lemma s2ss_open_some:

   663   "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = (

   664       case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p),

   665             co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of

   666         (Some sp, Some sp', Some sf) \<Rightarrow> 

   667            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   668            then s2ss s \<union> {sp', sf} 

   669            else s2ss s - {sp} \<union> {sp', sf} 

   670       | _                   \<Rightarrow> {} )"

   671 unfolding s2ss_def

   672 apply (frule vt_grant_os, frule vd_cons)

   673 apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)

   674 apply (drule current_proc_has_sp', simp, simp)

   675 apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)")

   676 apply (simp add:co2sobj.simps split:option.splits)

   677 apply (drule current_proc_has_sp', simp, simp)

   678 apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)")

   679 apply (simp add:co2sobj.simps split:option.splits)

   680 apply (clarsimp split del:if_splits)

   681 

   682 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   683 apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE)

   684 apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)

   685 apply (rule UnI1, rule CollectI, rule_tac x = obj in exI)

   686 apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)

   687 apply (simp add:co2sobj_open split:t_object.splits)

   688 apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)

   689 apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI)

   690 apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)

   691 apply (simp add:co2sobj_open split:t_object.splits)

   692 apply (frule_tac obj = obj in co2sobj_open_some, simp+)

   693 apply (simp add:alive_co2sobj_some_open_some', simp)

   694 apply (rule notI)

   695 apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE)

   696 apply (erule_tac x = p' in allE, simp)

   697 

   698 apply (simp split:if_splits, erule disjE)

   699 apply (rule_tac x = "O_proc p" in exI, simp)

   700 apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)

   701 apply (erule exE, erule conjE)

   702 apply (case_tac "obj = O_proc p", simp)

   703 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some)

   704 apply (case_tac "obj = O_file f", simp add:is_file_in_current)

   705 apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)

   706 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)

   707 apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)

   708 apply (erule conjE, erule exE, erule conjE)

   709 apply (case_tac "obj = O_proc p", simp)

   710 apply (case_tac "obj = O_file f", simp add:is_file_in_current)

   711 apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)

   712 done

   713 

   714 lemma s2ss_open':

   715   "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = (

   716      if opt = None

   717      then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of

   718         (Some sp, Some sp') \<Rightarrow> 

   719            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   720            then s2ss s \<union> {sp'}

   721            else s2ss s - {sp} \<union> {sp'} 

   722       | _                   \<Rightarrow> {} )

   723      else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p),

   724             co2sobj (Open p f flag fd opt # s) (O_file f)) of

   725         (Some sp, Some sp', Some sf) \<Rightarrow> 

   726            if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)

   727            then s2ss s \<union> {sp', sf} 

   728            else s2ss s - {sp} \<union> {sp', sf} 

   729       | _                   \<Rightarrow> {} ) )"

   730 apply (case_tac opt)

   731 apply (simp add:s2ss_open_some s2ss_open_none)+

   732 done

   733 

   734 lemma co2sobj_proc_eq_some:

   735   "\<lbrakk>co2sobj s (O_proc p) = Some sp; co2sobj s obj = Some sp\<rbrakk>

   736    \<Longrightarrow> \<exists> p'. obj = O_proc p'"

   737 apply (case_tac obj, case_tac[!] sp)

   738 by (auto simp:co2sobj.simps split:option.splits)

   739 

   740 lemma s2ss_open:

   741   "valid (Open p f flag fd opt # s) \<Longrightarrow> 

   742     (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p), 

   743            co2sobj (Open p f flag fd opt # s) (O_file f)) of

   744        (Some sp, Some sp', Some sf) \<Rightarrow> s2ss (Open p f flag fd opt # s) = (

   745        if opt = None

   746        then update_s2ss_obj s (s2ss s) (O_proc p) sp sp'

   747        else update_s2ss_obj s (s2ss s) (O_proc p) sp sp' \<union> {sf})

   748      | _ \<Rightarrow> s2ss (Open p f flag fd opt # s) = {})"

   749 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)

   750 apply (case_tac "co2sobj s (O_proc p)")

   751 apply (simp add:co2sobj.simps split:option.splits)

   752 apply (drule current_proc_has_sp', simp, simp)

   753 apply (drule current_proc_has_sp', simp, simp)

   754 apply (case_tac "co2sobj (Open p f flag fd opt # s) (O_proc p)")

   755 apply (simp add:co2sobj.simps split:option.splits)

   756 apply (drule current_proc_has_sp', simp, simp)

   757 apply (drule current_proc_has_sp', simp, simp)

   758 apply (case_tac "co2sobj (Open p f flag fd opt # s) (O_file f)")

   759 apply (simp add:co2sobj.simps split:option.splits)

   760 apply (simp split:option.splits add:s2ss_open' update_s2ss_obj_def)

   761 apply (auto)

   762 apply (erule_tac x = "O_proc p'" in allE, simp)

   763 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

   764 apply (erule_tac x = "p'" in allE, simp)

   765 apply (erule_tac x = "O_proc p'" in allE, simp)

   766 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

   767 apply (erule_tac x = "p'" in allE, simp)

   768 apply (erule_tac x = "O_proc p'" in allE, simp)

   769 apply (frule_tac obj = obj' in co2sobj_proc_eq_some, simp, erule exE, simp)

   770 apply (erule_tac x = "p'" in allE, simp)

   771 done

   772 

   773 lemma s2ss_readfile:

   774   "valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = (

   775      case (file_of_proc_fd s p fd) of 

   776        Some f \<Rightarrow> if (O_file f \<in> tainted s \<and> O_proc p \<notin> tainted s)

   777                  then (case (cp2sproc s p) of 

   778                          Some sp \<Rightarrow> update_s2ss_obj s (s2ss s) (O_proc p) (S_proc sp False) (S_proc sp True)

   779                        | _       \<Rightarrow> {})

   780                  else s2ss s

   781      | _      \<Rightarrow> {})"

   782 apply (frule vt_grant_os, frule vd_cons, clarsimp simp only:os_grant.simps)

   783 apply (case_tac "cp2sproc s p")

   784 apply (drule current_proc_has_sp', simp+)

   785 apply (rule conjI, rule impI, erule conjE)

   786 

   787 apply (simp add:update_s2ss_obj_def)

   788 apply (tactic {*my_clarify_tac 1*})

   789 apply (frule co2sobj_sproc_imp, erule exE, simp split:option.splits)

   790 apply (simp add:s2ss_def)

   791 apply (tactic {*my_seteq_tac 1*})

   792 apply (case_tac "obj = O_proc p")

   793 apply (rule disjI1, simp add:co2sobj_readfile)

   794 apply (rule disjI2, simp)

   795 apply (rule_tac x = obj in exI)

   796 apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)

   797 apply (tactic {*my_setiff_tac 1*})

   798 apply (rule_tac x= "O_proc p" in exI, simp add:alive_other co2sobj_readfile)

   799 apply (tactic {*my_setiff_tac 1*})

   800 apply (case_tac "obj = O_proc p")

   801 apply (rule_tac x = "O_proc pa" in exI, simp add:alive_other co2sobj_readfile)

   802 apply (simp add:co2sobj.simps)

   803 apply (rule_tac x = obj in exI)

   804 apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]

   805 apply (tactic {*my_clarify_tac 1*})

   806 apply (simp add:s2ss_def)

   807 apply (tactic {*my_seteq_tac 1*})

   808 apply (case_tac "obj = O_proc p")

   809 apply (rule disjI1, simp add:co2sobj_readfile)

   810 apply (rule disjI2, rule DiffI)

   811 apply (simp, rule_tac x = obj in exI)

   812 apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)

   813 apply (rule notI, erule_tac x = obj in allE)

   814 apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]

   815 apply (tactic {*my_setiff_tac 1*})

   816 apply (rule_tac x = "O_proc p" in exI, simp add:alive_other co2sobj_readfile)

   817 apply (tactic {*my_setiff_tac 1*})

   818 apply (rule_tac x = obj in exI)

   819 apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits)[1]

   820 apply (simp add:co2sobj.simps)

   821 

   822 apply (simp add:s2ss_def, rule impI)

   823 apply (tactic {*my_seteq_tac 1*})

   824 apply (rule_tac x = obj in exI)

   825 apply (simp add:alive_other co2sobj_readfile split:t_object.splits option.splits if_splits)

   826 apply (simp add:co2sobj.simps)

   827 apply (tactic {*my_setiff_tac 1*})

   828 apply (rule_tac x = obj in exI)

   829 apply (auto simp add:alive_other co2sobj_readfile split:t_object.splits option.splits if_splits)

   830 apply (simp add:co2sobj.simps)

   831 done

   832 

   833 lemma same_inode_files_prop9:

   834   "is_file s f \<Longrightarrow> f \<in> same_inode_files s f"

   835 by (simp add:same_inode_files_def)

   836 

   837 lemma cf2sfiles_prop:

   838   "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> cf2sfiles s f = cf2sfiles s f'"

   839 apply (auto simp:cf2sfiles_def)

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

   841 apply (erule same_inode_files_prop4, simp)

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

   843 apply (drule same_inode_files_prop5)

   844 apply (erule same_inode_files_prop4, simp)

   845 done

   846 

   847 lemma co2sobj_writefile_unchange:

   848   "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;

   849     O_proc p \<in> tainted s \<longrightarrow> O_file f \<in> tainted s\<rbrakk> 

   850    \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"

   851 apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)

   852 apply (simp add:co2sobj.simps)

   853 apply (case_tac "O_proc p \<in> tainted s")

   854 apply (simp add:same_inodes_tainted)+

   855 done

   856 

   857 lemma s2ss_writefile':

   858   "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (

   859      case (file_of_proc_fd s p fd) of

   860        Some f \<Rightarrow> if (O_proc p \<in> tainted s \<and> O_file f \<notin> tainted s)

   861                  then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>

   862                                  co2sobj s (O_file f') = co2sobj s (O_file f))

   863                        then s2ss s \<union> {S_file (cf2sfiles s f) True}

   864                        else s2ss s - {S_file (cf2sfiles s f) False} 

   865                                    \<union> {S_file (cf2sfiles s f) True})

   866                  else s2ss s

   867      | _      \<Rightarrow> {})"

   868 apply (frule vd_cons, frule vt_grant_os)

   869 apply (clarsimp split:option.splits)

   870 unfolding s2ss_def

   871 apply (rule conjI|rule impI|erule exE|erule conjE)+

   872 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   873 apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)

   874 apply (simp split:t_object.splits if_splits)

   875 apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)

   876 apply (rule disjI1, simp add:cf2sfiles_prop)

   877 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)

   878 apply (simp add:co2sobj.simps)

   879 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)

   880 apply (simp add:co2sobj.simps)

   881 apply (simp add:co2sobj.simps)

   882 apply (simp add:co2sobj.simps)

   883 apply (rule disjI2, rule_tac x = obj in exI, simp)

   884 apply (rule disjI2, rule_tac x = obj in exI, simp)

   885 apply (simp add:co2sobj.simps)

   886 

   887 apply (erule disjE)

   888 apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)

   889 apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)

   890 apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)

   891 apply (erule exE, erule conjE, erule conjE)

   892 apply (erule_tac obj = obj in co2sobj_some_caseD)

   893 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   894 apply (case_tac "fa \<in> same_inode_files s aa")

   895 apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)

   896 apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)

   897 apply (rule conjI, rule impI, simp add:same_inode_files_prop5)

   898 apply (rule impI, simp add:co2sobj.simps same_inodes_tainted)

   899 apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)

   900 apply (rule impI, simp add:same_inode_files_prop5)

   901 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)

   902 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   903 

   904 apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)

   905 apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)

   906 apply (simp add:co2sobj_writefile split:t_object.splits if_splits)

   907 apply (simp add:co2sobj.simps same_inodes_tainted)

   908 apply (case_tac "O_proc p \<in> tainted s", simp, simp)

   909 apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)

   910 apply (rule_tac x = obj in exI)

   911 apply (simp add:co2sobj_writefile_unchange alive_simps)

   912 

   913 apply (rule impI| rule conjI|erule conjE)+

   914 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   915 apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)

   916 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   917   rule notI, simp add:co2sobj.simps split:option.splits)

   918 apply (simp split:if_splits)

   919 apply (rule disjI1, simp add:cf2sfiles_prop)

   920 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)

   921 apply (rule notI, simp add:co2sobj.simps split:option.splits)

   922 apply (erule_tac x = list in allE, simp add:same_inode_files_prop5)

   923 apply (simp add:co2sobj.simps)

   924 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   925   rule notI, simp add:co2sobj.simps split:option.splits)

   926 apply (simp add:co2sobj.simps)

   927 apply (simp add:co2sobj.simps)

   928 apply (simp add:co2sobj.simps)

   929 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   930   rule notI, simp add:co2sobj.simps split:option.splits)

   931 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   932   rule notI, simp add:co2sobj.simps split:option.splits)

   933 apply (simp add:co2sobj.simps)

   934 apply (erule disjE)

   935 apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)

   936 apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)

   937 apply (erule exE|erule conjE)+

   938 apply (erule co2sobj_some_caseD)

   939 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   940 apply (case_tac "fa \<in> same_inode_files s aa")

   941 apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted)

   942 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)

   943 apply (rule impI, simp add:same_inode_files_prop5)

   944 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)

   945 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   946 apply (rule impI, rule impI)

   947 

   948 apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)

   949 apply (rule_tac x = obj in exI)

   950 apply (simp add:co2sobj_writefile_unchange alive_simps)

   951 apply (erule CollectE, erule exE, erule conjE)

   952 apply (rule CollectI, rule_tac x = obj in exI)

   953 apply (simp add:co2sobj_writefile_unchange alive_simps)

   954 done

   955 

   956 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"

   957 where

   958  "update_s2ss_sfile_tainted s ss f tag \<equiv>

   959     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> 

   960               co2sobj s (O_file f') = Some (S_file (cf2sfiles s f) False))

   961        then ss \<union> {S_file (cf2sfiles s f) True}

   962        else ss - {S_file (cf2sfiles s f) False} 

   963                \<union> {S_file (cf2sfiles s f) True}"

   964 

   965 lemma s2ss_writefile:

   966   "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (

   967      case (file_of_proc_fd s p fd) of

   968        Some f \<Rightarrow> if (O_proc p \<in> tainted s \<and> O_file f \<notin> tainted s)

   969                  then update_s2ss_sfile_tainted s (s2ss s) f True

   970                  else s2ss s

   971      | _      \<Rightarrow> {})"

   972 apply (drule s2ss_writefile')

   973 apply (simp)

   974 apply (case_tac "file_of_proc_fd s p fd", simp)

   975 apply (simp add:update_s2ss_sfile_tainted_def)

   976 apply auto

   977 apply (erule_tac x = f' in allE, simp add:co2sobj.simps)+

   978 done

   979 

   980 definition update_s2ss_sfile_del :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"

   981 where 

   982   "update_s2ss_sfile_del s ss f sf \<equiv> 

   983      if (same_inode_files s f = {f})

   984      then ss

   985      else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> tainted s)}"

   986 

   987 definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"

   988 where

   989   "del_s2ss_file s ss f sf = 

   990      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)

   991       then ss

   992       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))

   993            then update_s2ss_sfile_del s ss f sf

   994            else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> tainted s)}) f sf)"

   995 

   996 

   997 lemma alive_co2sobj_closefd1:

   998   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 

   999     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>

  1000    \<Longrightarrow> alive (CloseFd p fd # s) obj"

  1001 apply (erule co2sobj_some_caseD)

  1002 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

  1003 

  1004 lemma alive_co2sobj_closefd3:

  1005   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;

  1006     file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>

  1007    \<Longrightarrow> alive (CloseFd p fd # s) obj"

  1008 apply (erule co2sobj_some_caseD)

  1009 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

  1010 

  1011 lemma alive_co2sobj_closefd2:

  1012   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>

  1013    \<Longrightarrow> alive (CloseFd p fd # s) obj"

  1014 apply (erule co2sobj_some_caseD)

  1015 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

  1016 

  1017 lemma alive_co2sobj_closefd':

  1018   "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; 

  1019     valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"

  1020 apply (erule co2sobj_some_caseD)

  1021 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)

  1022 

  1023 ML {*asm_full_simp_tac*}

  1024 

  1025 lemma same_inode_files_prop10:

  1026   "\<lbrakk>same_inode_files s f \<noteq> {f}; is_file s f\<rbrakk> \<Longrightarrow> \<exists> f'. f' \<in> same_inode_files s f \<and> f' \<noteq> f"

  1027 by (auto simp:same_inode_files_def split:if_splits)

  1028 

  1029 lemma same_inode_files_prop11:

  1030   "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f"

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

  1032 

  1033 lemma same_inode_files_prop11':

  1034   "f \<in> same_inode_files s f' \<Longrightarrow> is_file s f'"

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

  1036 

  1037 lemma s2ss_closefd:

  1038   "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (

  1039      case (file_of_proc_fd s p fd) of

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

  1041                  then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of

  1042                          (Some sf, Some sp, Some sp') \<Rightarrow> 

  1043                             (del_s2ss_file s (

  1044                                update_s2ss_obj s (s2ss s) (O_proc p) 

  1045                                  (S_proc sp (O_proc p \<in> tainted s))

  1046                                  (S_proc sp' (O_proc p \<in> tainted s))) f sf)

  1047                       | _ \<Rightarrow> {})

  1048                  else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of 

  1049                          (Some sp, Some sp') \<Rightarrow> 

  1050                             (update_s2ss_obj s (s2ss s) (O_proc p)

  1051                                (S_proc sp (O_proc p \<in> tainted s))

  1052                                (S_proc sp' (O_proc p \<in> tainted s)))

  1053                       | _ \<Rightarrow> {})

  1054       | _     \<Rightarrow> s2ss s)"

  1055 apply (frule vd_cons, frule vt_grant_os)

  1056 apply (clarsimp simp only:os_grant.simps)

  1057 apply (frule current_proc_has_sp, simp, erule exE)

  1058 apply (case_tac "file_of_proc_fd s p fd")

  1059 

  1060 apply (simp add:s2ss_def)

  1061 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)

  1062 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')

  1063 apply (frule co2sobj_closefd, simp)

  1064 apply (frule cp2sproc_closefd, simp)

  1065 apply (simp add:proc_file_fds_def split:t_object.splits)

  1066 apply (simp split:if_splits add:co2sobj.simps)

  1067 apply (erule CollectE, erule exE, erule conjE, rule CollectI)

  1068 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)

  1069 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)

  1070 apply (frule cp2sproc_closefd, simp)

  1071 apply (auto simp add:proc_file_fds_def co2sobj.simps 

  1072             split:t_object.splits option.splits if_splits)[1]

  1073 

  1074 apply (case_tac "cp2sproc (CloseFd p fd # s) p")

  1075 apply (drule current_proc_has_sp', simp, simp)

  1076 apply (case_tac "cf2sfile s a")

  1077 apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current)

  1078 apply (simp)

  1079 

  1080 apply (rule conjI, rule impI, erule conjE)

  1081 apply (simp add:del_s2ss_file_def)

  1082 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+

  1083 

  1084 apply (simp add:update_s2ss_obj_def)

  1085 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+

  1086 apply (tactic {*my_seteq_tac 1*})

  1087 apply simp

  1088 apply (case_tac "obj = O_proc p")

  1089 apply (simp add:co2sobj.simps)

  1090 apply (rule disjI2, rule_tac x = obj in exI)

  1091 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)

  1092 apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)

  1093 apply (tactic {*my_setiff_tac 1*})

  1094 apply (rule_tac x = "O_proc p" in exI)

  1095 apply (simp add:co2sobj.simps)

  1096 apply (tactic {*my_setiff_tac 1*})

  1097 apply (case_tac "obj = O_proc p")

  1098 apply (rule_tac x = obj' in exI)

  1099 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)

  1100 apply (simp add:co2sobj.simps)

  1101 apply (case_tac "obj = O_file a")

  1102 apply (rule_tac x = "O_file f'" in exI)

  1103 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)

  1104 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)

  1105 apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)

  1106 apply (rule_tac x = obj in exI)

  1107 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)

  1108 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1109 apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1]

  1110 

  1111 apply (rule impI)+

  1112 apply (tactic {*my_seteq_tac 1*})

  1113 apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps)

  1114 apply (rule disjI2)

  1115 apply (case_tac "obj = O_file a", simp add:alive_simps)

  1116 apply (rule DiffI, simp)

  1117 apply (rule_tac x = obj in exI)

  1118 apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)

  1119 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1120 apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)

  1121 apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)

  1122 apply (erule_tac x = "O_proc pa" in allE, simp)

  1123 apply (tactic {*my_setiff_tac 1*})

  1124 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps)

  1125 apply (tactic {*my_setiff_tac 1*})

  1126 apply (case_tac "obj = O_proc p", simp add:co2sobj.simps)

  1127 apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)

  1128 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)

  1129 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)

  1130 apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)

  1131 apply (rule_tac x = obj in exI)

  1132 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)

  1133 apply (frule_tac obj = obj in co2sobj_closefd, simp)

  1134 apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1]

  1135