1 theory obj2sobj_prop 

     2 imports Main rc_theory os_rc deleted_prop

     3 begin

     4 

     5 context tainting_s_complete begin

     6 

     7 (** file 2 sfile   **)

     8 

     9 lemma init_son_deleted_D:

    10   "\<lbrakk>deleted (File pf) s; f # pf \<in> init_files; valid s\<rbrakk> \<Longrightarrow> deleted (File (f # pf)) s"

    11 apply (induct s, simp)

    12 by (frule valid_cons, frule valid_os, case_tac a, auto dest:init_notin_curf_deleted)

    13 

    14 lemma init_parent_undeleted_I:

    15   "\<lbrakk>\<not> deleted (File (f # pf)) s; f # pf \<in> init_files; valid s\<rbrakk> \<Longrightarrow> \<not> deleted (File pf) s"

    16 by (rule notI, simp add:init_son_deleted_D)

    17 

    18 lemma source_dir_in_init:

    19   "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"

    20 by (induct f, auto split:if_splits)

    21 

    22 lemma source_dir_of_init: "\<lbrakk>source_dir [] f = Some sd; f \<in> init_files\<rbrakk> \<Longrightarrow> f = sd"

    23 by (induct f, auto)

    24 

    25 lemma source_dir_of_init': "f \<in> init_files \<Longrightarrow> source_dir [] f = Some f"

    26 by (induct f, auto)

    27 

    28 lemma init_not_curf_imp_deleted:

    29   "\<lbrakk>f \<in> init_files; f \<notin> current_files s; valid s\<rbrakk> \<Longrightarrow> deleted (File f) s"

    30 apply (induct s, simp)

    31 apply (frule valid_cons, frule valid_os, case_tac a, auto)

    32 done

    33 

    34 lemma source_dir_of_init'': 

    35   "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> source_dir s f = Some f"

    36 by (induct f, auto)

    37 

    38 

    39 lemma source_dir_createf:

    40   "valid (CreateFile p (f#pf) # s) \<Longrightarrow> 

    41   source_dir (CreateFile p (f#pf) # s) = (source_dir s) ((f#pf)  := source_dir s pf)"

    42 apply (frule valid_os, frule valid_cons)

    43 apply (rule ext, induct_tac x)

    44 apply (auto dest:init_not_curf_imp_deleted)

    45 done

    46 

    47 lemma source_dir_createf':

    48   "valid (CreateFile p f # s) \<Longrightarrow> 

    49   source_dir (CreateFile p f # s) = (source_dir s) (f := (case (parent f) of

    50                                                             Some pf \<Rightarrow> source_dir s pf

    51                                                           | _       \<Rightarrow> None))"

    52 apply (frule valid_os, case_tac f, simp+)

    53 apply (drule source_dir_createf, auto)

    54 done

    55 

    56 lemma source_dir_other:

    57   "\<lbrakk>valid (e # s); \<forall> p f. e \<noteq> CreateFile p f; \<forall> p f. e \<noteq> DeleteFile p f\<rbrakk>

    58    \<Longrightarrow> source_dir (e#s) = source_dir s"

    59 apply (rule ext, induct_tac x, simp)

    60 apply (auto dest:not_deleted_cons_D)

    61 apply (case_tac [!] e, auto)

    62 done

    63 

    64 lemma source_dir_deletef:

    65   "valid (DeleteFile p f # s) \<Longrightarrow> source_dir (DeleteFile p f # s) f' =  

    66      (if (source_dir s f') = Some f then parent f else (source_dir s f'))"

    67 apply (frule valid_os, frule valid_cons)

    68 apply (case_tac "f \<in> init_files")

    69 apply (induct_tac f', simp)

    70 apply (auto dest!:init_parent_undeleted_I intro:parent_file_in_init'

    71             intro!: source_dir_of_init'')[1]

    72 apply (induct_tac f', auto)

    73 done

    74 

    75 lemma source_dir_deletef':

    76   "valid (DeleteFile p f # s) \<Longrightarrow> source_dir (DeleteFile p f # s) = (\<lambda> f'.   

    77      (if (source_dir s f') = Some f then parent f else (source_dir s f')) )"

    78 by (auto dest:source_dir_deletef)

    79 

    80 lemmas source_dir_simps = source_dir_of_init' source_dir_of_init'' source_dir_createf' 

    81   source_dir_deletef' source_dir_other

    82 

    83 declare source_dir.simps [simp del]

    84 

    85 lemma source_dir_is_ancient:

    86   "source_dir s f = Some sd ==> sd \<preceq> f"

    87 apply (induct f)

    88 by (auto simp:source_dir.simps no_junior_def split:if_splits)

    89 

    90 lemma no_junior_trans: "\<lbrakk>f \<preceq> f'; f' \<preceq> f''\<rbrakk> \<Longrightarrow> f \<preceq> f''"

    91 by (auto elim:no_juniorE)

    92 

    93 lemma ancient_has_parent:

    94   "[| f \<preceq> f'; f \<noteq> f'|] ==> \<exists> sonf. parent sonf = Some f \<and> sonf \<preceq> f' "

    95 apply (induct f')

    96 apply (simp add:no_junior_def)

    97 apply (case_tac "f = f'")

    98 apply (rule_tac x = "a # f'" in exI, simp add:no_junior_def)

    99 apply (frule no_junior_noteq, simp)

   100 apply clarsimp

   101 apply (rule_tac x = sonf in exI, simp add:no_junior_trans)

   102 done

   103 

   104 lemma source_dir_prop:

   105   "[|\<forall>fn. fn # f' \<notin> current_files s; source_dir s f = Some f'; f \<in> current_files s; valid s|]

   106   ==> f = f'"

   107   apply (drule source_dir_is_ancient)

   108   apply (case_tac "f = f'", simp)

   109   apply (drule ancient_has_parent, simp, clarsimp)

   110   apply (drule_tac ancient_file_in_current, simp+)

   111   apply (case_tac sonf, auto)

   112   done

   113 

   114 lemma current_file_has_sd:

   115   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sd. source_dir s f = Some sd"

   116 apply (induct s arbitrary:f, simp add:source_dir_of_init')

   117 apply (frule valid_cons, frule valid_os, case_tac a, auto simp:source_dir_simps)

   118 apply (case_tac list, simp)

   119 apply (rule_tac f = f in cannot_del_root, simp+)

   120 done

   121 

   122 lemma current_file_has_sd':

   123   "\<lbrakk>source_dir s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   124 by (rule notI, auto dest:current_file_has_sd)

   125 

   126 lemma current_file_has_sfile:

   127   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> et sd. cf2sfile s f = Some (et, sd)"

   128 apply (frule current_file_has_sd, simp+)

   129 apply (frule current_file_has_etype, auto)

   130 done

   131 

   132 lemma current_file_has_sfile':

   133   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   134 by (auto dest:current_file_has_sfile)

   135   

   136 (*

   137 lemma not_deleted_sf_remains:

   138   "\<lbrakk>f \<in> current_files s; \<not> deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> "

   139 *)

   140 

   141 lemma current_proc_has_sproc:

   142   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r fr pt u. cp2sproc s p = Some (r, fr, pt, u)"

   143 apply (frule current_proc_has_role, simp+)

   144 apply (frule current_proc_has_type, simp)

   145 apply (frule current_proc_has_forcedrole, simp)

   146 apply (frule current_proc_has_owner, auto)

   147 done

   148 

   149 lemma current_proc_has_sproc':

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

   151 by (auto dest!:current_proc_has_sproc)

   152 

   153 lemma current_ipc_has_sipc: 

   154   "\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. ci2sipc s i = Some t"

   155 by (drule current_ipc_has_type, auto)

   156 

   157 lemma init_file_has_sobj:

   158   "f \<in> init_files \<Longrightarrow> \<exists> t sd. init_obj2sobj (File f) = SFile (t, sd) (Some f)"

   159 by (frule init_file_has_etype, clarsimp)

   160 

   161 lemma init_proc_has_sobj:

   162   assumes pinit:"p \<in> init_processes"

   163   shows "\<exists> r fr pt u. init_obj2sobj (Proc p) = SProc (r, fr, pt, u) (Some p)"

   164 proof -

   165   from pinit obtain r where "init_currentrole p = Some r" 

   166     using init_proc_has_role by (auto simp:bidirect_in_init_def)

   167   moreover from pinit obtain fr where "init_proc_forcedrole p = Some fr"

   168     using init_proc_has_frole by (auto simp:bidirect_in_init_def)

   169   moreover from pinit obtain pt where "init_process_type p = Some pt"

   170     using init_proc_has_type by (auto simp:bidirect_in_init_def)

   171   moreover from pinit obtain u where "init_owner p = Some u"

   172     using init_proc_has_owner by (auto simp:bidirect_in_init_def)

   173   ultimately show ?thesis by auto 

   174 qed

   175 

   176 lemma init_ipc_has_sobj:

   177   "i \<in> init_ipcs \<Longrightarrow> \<exists> t. init_obj2sobj (IPC i) = SIPC t (Some i)"

   178 using init_ipc_has_type

   179 by (auto simp:bidirect_in_init_def)

   180 

   181 lemma init_obj_has_sobj:

   182   "exists [] obj \<Longrightarrow> init_obj2sobj obj \<noteq> Unknown"

   183 apply (case_tac obj)

   184 apply (simp_all only:exists.simps current_procs.simps current_ipcs.simps current_files.simps) 

   185 apply (auto dest!:init_proc_has_sobj init_file_has_sobj init_ipc_has_sobj)

   186 done

   187 

   188 lemma exists_obj_has_sobj:

   189   "\<lbrakk>exists s obj; valid s\<rbrakk> \<Longrightarrow> obj2sobj s obj \<noteq> Unknown"

   190 apply (case_tac obj)

   191 apply (auto dest!:current_ipc_has_sipc current_proc_has_sproc' current_file_has_sfile' 

   192             split:option.splits)

   193 done

   194 

   195 lemma current_proc_has_srp:

   196   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> srp. source_proc s p = Some srp"

   197 apply (induct s arbitrary:p, simp)

   198 by (frule valid_cons, frule valid_os, case_tac a, auto)

   199 

   200 lemma current_proc_has_sobj:

   201   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r fr t u srp. obj2sobj s (Proc p) = SProc (r,fr,t,u) (Some srp)"

   202 apply (frule current_proc_has_sproc')

   203 apply (auto dest:current_proc_has_srp)

   204 done

   205 

   206 lemma current_file_has_sobj:

   207   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> t sd srf. obj2sobj s (File f) = SFile (t, sd) srf"

   208 by (auto dest:current_file_has_sfile)

   209 

   210 lemma current_ipc_has_sobj:

   211   "\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t sri. obj2sobj s (IPC i) = SIPC t sri"

   212 by (auto dest:current_ipc_has_sipc)

   213 

   214 lemma sobj_has_proc_role:

   215   "obj2sobj s (Proc p) = SProc (r, fr, t, u) srp \<Longrightarrow> currentrole s p = Some r"

   216 by (auto split:option.splits)

   217 

   218 lemma chown_role_aux_valid:

   219   "\<lbrakk>currentrole s p = Some r; proc_forcedrole s p = Some fr\<rbrakk>

   220   \<Longrightarrow> chown_role_aux r fr u = currentrole (ChangeOwner p u # s) p"

   221 by (auto split:t_role.splits simp:chown_role_aux_def dest:proc_forcedrole_valid)

   222 

   223 lemma chown_role_aux_valid':

   224   "cp2sproc s p = Some (r, fr, t, u') \<Longrightarrow> chown_role_aux r fr u = currentrole (ChangeOwner p u # s) p"

   225 by (rule chown_role_aux_valid, auto split:option.splits)

   226 

   227 lemma chown_type_aux_valid:

   228   "\<lbrakk>currentrole s p = Some r; currentrole (ChangeOwner p u # s) p = Some nr; type_of_process s p = Some t\<rbrakk>

   229   \<Longrightarrow> type_of_process (ChangeOwner p u # s) p = Some (chown_type_aux r nr t)" 

   230 apply (auto split:option.splits t_rc_proc_type.splits 

   231              dest:default_process_create_type_valid

   232              simp:chown_type_aux_def pot_def pct_def)

   233 done

   234 

   235 lemma chown_type_aux_valid':

   236   "\<lbrakk>cp2sproc s p = Some (r, fr, t, u'); currentrole (ChangeOwner p u # s) p = Some nr\<rbrakk> 

   237    \<Longrightarrow> type_of_process (ChangeOwner p u # s) p = Some (chown_type_aux r nr t)"

   238 by (rule chown_type_aux_valid, auto split:option.splits)

   239 

   240 lemma exec_type_aux_valid:

   241   "\<lbrakk>currentrole s p = Some r; type_of_process s p = Some t\<rbrakk>

   242   \<Longrightarrow> type_of_process (Execute p f # s) p = Some (exec_type_aux r t)" 

   243 apply (auto split:option.splits t_rc_proc_type.splits 

   244              dest:default_process_execute_type_valid

   245              simp:exec_type_aux_def pet_def)

   246 done

   247 

   248 lemma exec_type_aux_valid':

   249   "cp2sproc s p = Some (r, fr, t, u') \<Longrightarrow> type_of_process (Execute p f # s) p = Some (exec_type_aux r t)" 

   250 by (rule exec_type_aux_valid, auto split:option.splits)

   251 

   252 lemma non_initf_frole_inherit:

   253   "\<lbrakk>f \<notin> init_files; f \<noteq> []\<rbrakk> \<Longrightarrow> forcedrole s f = Some InheritParentRole"

   254 apply (induct s) defer

   255 apply (case_tac a, auto) 

   256 apply (induct f, auto split:option.splits dest:init_frole_has_file)

   257 done

   258 

   259 lemma non_initf_irole_inherit:

   260   "\<lbrakk>f \<notin> init_files; f \<noteq> []\<rbrakk> \<Longrightarrow> initialrole s f = Some InheritParentRole"

   261 apply (induct s) defer

   262 apply (case_tac a, auto) 

   263 apply (induct f, auto split:option.splits dest:init_irole_has_file)

   264 done

   265 

   266 lemma deleted_file_frole_inherit:

   267   "\<lbrakk>deleted (File f) s; f \<in> current_files s\<rbrakk> \<Longrightarrow> forcedrole s f = Some InheritParentRole"

   268 apply (induct s, simp)

   269 apply (case_tac a, auto) 

   270 done

   271 

   272 lemma deleted_file_irole_inherit:

   273   "\<lbrakk>deleted (File f) s; f \<in> current_files s\<rbrakk> \<Longrightarrow> initialrole s f = Some InheritParentRole"

   274 apply (induct s, simp)

   275 apply (case_tac a, auto) 

   276 done

   277 

   278 lemma sd_deter_efrole:

   279   "\<lbrakk>source_dir s f = Some sd; valid s; f \<in> current_files s\<rbrakk> 

   280   \<Longrightarrow> effforcedrole s f = effforcedrole s sd"

   281 apply (induct f)

   282 apply (drule source_dir_is_ancient, simp add:no_junior_def)

   283 apply (simp add:source_dir.simps split:if_splits)

   284 apply (frule parent_file_in_current', simp)

   285 apply (case_tac "a # f \<in> init_files", simp)

   286 apply (drule_tac deleted_file_frole_inherit, simp, simp add:effforcedrole_def)

   287 apply (drule_tac s = s in non_initf_frole_inherit, simp, simp add:effforcedrole_def)

   288 done

   289 

   290 lemma sd_deter_eirole:

   291   "\<lbrakk>source_dir s f = Some sd; valid s; f \<in> current_files s\<rbrakk> 

   292   \<Longrightarrow> effinitialrole s f = effinitialrole s sd"

   293 apply (induct f)

   294 apply (drule source_dir_is_ancient, simp add:no_junior_def)

   295 apply (simp add:source_dir.simps split:if_splits)

   296 apply (frule parent_file_in_current', simp)

   297 apply (case_tac "a # f \<in> init_files", simp)

   298 apply (drule_tac deleted_file_irole_inherit, simp, simp add:effinitialrole_def)

   299 apply (drule_tac s = s in non_initf_irole_inherit, simp, simp add:effinitialrole_def)

   300 done

   301 

   302 lemma undel_initf_keeps_frole:

   303   "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>

   304    \<Longrightarrow> forcedrole s f = init_file_forcedrole f"

   305 apply (induct s, simp)

   306 apply (frule valid_cons, frule valid_os, case_tac a)

   307 apply (auto dest:init_notin_curf_deleted)

   308 done

   309 

   310 lemma undel_initf_keeps_efrole:

   311   "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>

   312    \<Longrightarrow> effforcedrole s f = erole_functor init_file_forcedrole InheritUpMixed f"

   313 apply (induct f)

   314 apply (drule undel_initf_keeps_frole, simp, simp)

   315 apply (simp add:effforcedrole_def)

   316 apply (frule parent_file_in_init', frule init_parent_undeleted_I, simp+)

   317 apply (drule undel_initf_keeps_frole, simp, simp)

   318 apply (simp add:effforcedrole_def)

   319 done

   320 

   321 lemma undel_initf_keeps_irole:

   322   "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>

   323    \<Longrightarrow> initialrole s f = init_file_initialrole f"

   324 apply (induct s, simp)

   325 apply (frule valid_cons, frule valid_os, case_tac a)

   326 apply (auto dest:init_notin_curf_deleted)

   327 done

   328 

   329 lemma undel_initf_keeps_eirole:

   330   "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk>

   331    \<Longrightarrow> effinitialrole s f = erole_functor init_file_initialrole UseForcedRole f"

   332 apply (induct f)

   333 apply (drule undel_initf_keeps_irole, simp, simp)

   334 apply (simp add:effinitialrole_def)

   335 apply (frule parent_file_in_init', frule init_parent_undeleted_I, simp+)

   336 apply (drule undel_initf_keeps_irole, simp, simp)

   337 apply (simp add:effinitialrole_def)

   338 done

   339 

   340 lemma source_dir_not_deleted:

   341   "source_dir s f = Some sd \<Longrightarrow> \<not> deleted (File sd) s"

   342 by (induct f, auto simp:source_dir.simps split:if_splits)

   343 

   344 lemma exec_role_aux_valid:

   345   "\<lbrakk>currentrole s p = Some r; source_dir s f = Some sd; owner s p = Some u; 

   346   f \<in> current_files s; valid s\<rbrakk>

   347   \<Longrightarrow> exec_role_aux r sd u = currentrole (Execute p f # s) p"

   348 apply (frule sd_deter_eirole, simp+, frule sd_deter_efrole, simp+)

   349 apply (frule source_dir_in_init, drule source_dir_not_deleted)

   350 apply (simp add:undel_initf_keeps_eirole undel_initf_keeps_efrole)

   351 apply (frule file_has_effinitialrole, simp, frule file_has_effforcedrole, simp)

   352 apply (auto split:option.splits t_role.splits simp:map_comp_def exec_role_aux_def

   353              dest:effforcedrole_valid effinitialrole_valid)

   354 done

   355 

   356 lemma exec_role_aux_valid':

   357   "\<lbrakk>cp2sproc s p = Some (r, fr, t, u); source_dir s f = Some sd; f \<in> current_files s; valid s\<rbrakk>

   358   \<Longrightarrow> exec_role_aux r sd u = currentrole (Execute p f # s) p"

   359 by (rule exec_role_aux_valid, auto split:option.splits)

   360 

   361 lemma cp2sproc_nil_init:

   362   "init_obj2sobj (Proc p) = (case (cp2sproc [] p) of 

   363                                Some sp \<Rightarrow> SProc sp (Some p)

   364                              | _       \<Rightarrow> Unknown)"

   365 by (auto split:option.splits)

   366 

   367 lemma cf2sfile_nil_init:

   368   "init_obj2sobj (File f) = (case (cf2sfile [] f) of 

   369                                Some sf \<Rightarrow> SFile sf (Some f)

   370                              | _       \<Rightarrow> Unknown)"

   371 apply (auto split:option.splits simp:etype_of_file_def)

   372 apply (case_tac "f \<in> init_files", simp add:source_dir_of_init')

   373 apply (induct f, simp+)

   374 apply (case_tac "f \<in> init_files", simp add:source_dir_of_init')

   375 apply (induct f, simp+)

   376 done

   377 

   378 lemma ci2sipc_nil_init:

   379   "init_obj2sobj (IPC i) = (case (ci2sipc [] i) of 

   380                               Some si \<Rightarrow> SIPC si (Some i)

   381                             | _       \<Rightarrow> Unknown)"

   382 by simp

   383 

   384 lemma obj2sobj_nil_init:

   385   "exists [] obj \<Longrightarrow> obj2sobj [] obj = init_obj2sobj obj" 

   386 apply (case_tac obj) 

   387 apply (auto simp:cf2sfile_nil_init cp2sproc_nil_init ci2sipc_nil_init 

   388                  source_dir_of_init' etype_of_file_def

   389            split:if_splits option.splits)

   390 done

   391 

   392 (**** cp2sproc simpset ****)

   393 

   394 lemma current_proc_has_role':

   395   "\<lbrakk>currentrole s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"

   396 by (rule notI, auto dest:current_proc_has_role)

   397 

   398 lemma cp2sproc_chown:

   399   assumes vs: "valid (ChangeOwner p u # s)"

   400   shows "cp2sproc (ChangeOwner p u # s) = (cp2sproc s) 

   401      (p := (case (cp2sproc s p) of

   402               Some (r,fr,pt,u') \<Rightarrow> (case (chown_role_aux r fr u) of 

   403                                       Some nr \<Rightarrow> Some (nr,fr,chown_type_aux r nr pt,u)

   404                                     | _       \<Rightarrow> None)

   405             | _                 \<Rightarrow> None)

   406       )" (is "?lhs = ?rhs")

   407 proof-

   408   have os: "os_grant s (ChangeOwner p u)" and vs': "valid s" using vs

   409     by (auto dest:valid_cons valid_os)

   410   have "\<And> x. x \<noteq> p \<Longrightarrow> ?lhs x = ?rhs x"

   411     by (auto simp:type_of_process.simps split:option.splits t_role.splits)

   412   moreover have "?lhs p = ?rhs p"

   413   proof-

   414     from os have p_in: "p \<in> current_procs s" by (simp+)

   415     then obtain r fr t u' where csp: "cp2sproc s p = Some (r, fr, t, u')" using vs'

   416       by (drule_tac current_proc_has_sproc, auto)  

   417     from os have "u \<in> init_users" by simp

   418     hence "defrole u \<noteq> None" using init_user_has_role by (auto simp:bidirect_in_init_def)

   419     then obtain nr where nrole:"chown_role_aux r fr u = Some nr"

   420       by (case_tac fr, auto simp:chown_role_aux_def)

   421     have nr_eq: "currentrole (ChangeOwner p u # s) p = chown_role_aux r fr u" 

   422       using csp by (auto simp:chown_role_aux_valid'[where u = u])  

   423     moreover have "type_of_process (ChangeOwner p u # s) p = Some (chown_type_aux r nr t)"

   424       using csp nrole nr_eq 

   425       by (rule_tac fr = fr and u' = u' in chown_type_aux_valid', simp+)

   426     moreover have "proc_forcedrole (ChangeOwner p u # s) p = Some fr"

   427       using csp by (auto split:option.splits)

   428     moreover have "owner (ChangeOwner p u # s) p = Some u" by simp

   429     ultimately have "cp2sproc (ChangeOwner p u # s) p = Some (nr, fr, chown_type_aux r nr t, u)" 

   430       using nrole by (simp)

   431     thus ?thesis using csp nrole by simp

   432   qed

   433   ultimately show ?thesis by (rule_tac ext, auto)

   434 qed

   435 

   436 lemma cp2sproc_crole:

   437   "valid (ChangeRole p r # s) \<Longrightarrow> cp2sproc (ChangeRole p r # s) = (cp2sproc s) 

   438      (p := (case (cp2sproc s p) of

   439               Some (r',fr,pt,u) \<Rightarrow> Some (r,fr,pt,u)

   440             | _                 \<Rightarrow> None)

   441       )"

   442 apply (frule valid_cons, frule valid_os, simp)

   443 apply (frule current_proc_has_sproc, simp)

   444 apply (rule ext, auto split:option.splits)

   445 done

   446 

   447 lemma cp2sproc_exec:

   448   assumes vs: "valid (Execute p f # s)"

   449   shows "cp2sproc (Execute p f # s) = (cp2sproc s) 

   450      (p := (case (cp2sproc s p, source_dir s f) of 

   451               (Some (r,fr,pt,u), Some sd) \<Rightarrow> (

   452      case (exec_role_aux r sd u, erole_functor init_file_forcedrole InheritUpMixed sd) of

   453        (Some r', Some fr') \<Rightarrow> Some (r', fr', exec_type_aux r pt, u)

   454      | _                   \<Rightarrow> None           )

   455             | _                \<Rightarrow> None))" (is "?lhs = ?rhs")

   456 proof-

   457   have os: "os_grant s (Execute p f)" and vs': "valid s" using vs

   458     by (auto dest:valid_cons valid_os)

   459   have "\<And> x. x \<noteq> p \<Longrightarrow> ?lhs x = ?rhs x"

   460     by (auto simp:type_of_process.simps split:option.splits t_role.splits)

   461   moreover have "?lhs p = ?rhs p"

   462   proof-

   463     from os have p_in: "p \<in> current_procs s" by (simp+)

   464     then obtain r fr t u where csp: "cp2sproc s p = Some (r, fr, t, u)" using vs'

   465       by (drule_tac current_proc_has_sproc, auto)  

   466     from os have f_in: "f \<in> current_files s" by simp

   467     then obtain sd where sdir: "source_dir s f = Some sd" using vs'

   468       by (drule_tac current_file_has_sd, auto)

   469     have "currentrole (Execute p f # s) p \<noteq> None" using vs p_in

   470       by (rule_tac notI, drule_tac current_proc_has_role', simp+)

   471     then obtain nr where nrole: "currentrole (Execute p f # s) p = Some nr" by auto

   472     have "proc_forcedrole (Execute p f # s) p \<noteq> None" using vs p_in

   473       by (rule_tac notI, drule_tac current_proc_has_forcedrole', simp+)

   474     then obtain nfr where nfrole: "proc_forcedrole (Execute p f # s) p = Some nfr" by auto

   475     have nr_eq: "currentrole (Execute p f # s) p = exec_role_aux r sd u" 

   476       using csp f_in sdir vs' by (simp only:exec_role_aux_valid')

   477     moreover have "type_of_process (Execute p f # s) p = Some (exec_type_aux r t)"

   478       using csp by (simp only:exec_type_aux_valid')

   479     moreover have nfr_eq: "proc_forcedrole (Execute p f # s) p = 

   480                            erole_functor init_file_forcedrole InheritUpMixed sd" 

   481       using sdir vs' f_in

   482       apply (frule_tac source_dir_in_init, drule_tac source_dir_not_deleted)

   483       by (simp add:undel_initf_keeps_efrole sd_deter_efrole)

   484     moreover have "owner (Execute p f # s) p = Some u" using csp

   485       by (auto split:option.splits)

   486     ultimately have "cp2sproc (Execute p f # s) p = Some (nr, nfr, exec_type_aux r t, u)" 

   487       using nrole nfrole by (simp)

   488     moreover have "exec_role_aux r sd u = Some nr" using nrole nr_eq by simp

   489     moreover have "erole_functor init_file_forcedrole InheritUpMixed sd = Some nfr"

   490       using nfrole nfr_eq by simp

   491     ultimately show ?thesis using csp sdir by simp 

   492   qed

   493   ultimately show ?thesis by (rule_tac ext, auto)

   494 qed

   495 

   496 lemma cp2sproc_clone:

   497   "valid (Clone p p' # s) \<Longrightarrow> cp2sproc (Clone p p' # s) = (cp2sproc s) (p' := 

   498       (case (cp2sproc s p) of

   499          Some (r, fr, pt, u) \<Rightarrow> Some (r, fr, clone_type_aux r pt, u)

   500        | _                   \<Rightarrow> None))"

   501 apply (frule valid_cons, frule valid_os)

   502 apply (rule ext, auto split:option.splits t_rc_proc_type.splits 

   503                        simp:pct_def clone_type_aux_def

   504                        dest:current_proc_has_type default_process_create_type_valid)

   505 done

   506 

   507 lemma cp2sproc_other:

   508   "\<lbrakk>valid (e # s); \<forall> p f. e \<noteq> Execute p f; \<forall> p p'. e \<noteq> Clone p p';

   509     \<forall> p r. e \<noteq> ChangeRole p r; \<forall> p u. e \<noteq> ChangeOwner p u\<rbrakk> \<Longrightarrow> cp2sproc (e#s) = cp2sproc s"

   510 by (case_tac e, auto)

   511 

   512 lemmas cp2sproc_simps = cp2sproc_exec cp2sproc_chown cp2sproc_crole cp2sproc_clone cp2sproc_other

   513 

   514 lemma obj2sobj_file: "obj2sobj s obj = SFile sf fopt \<Longrightarrow> \<exists> f. obj = File f"

   515 by (case_tac obj, case_tac [!] s, auto split:option.splits if_splits)

   516 

   517 lemma obj2sobj_proc: "obj2sobj s obj = SProc sp popt \<Longrightarrow> \<exists> p. obj = Proc p"

   518 by (case_tac obj, case_tac [!] s, auto split:option.splits if_splits)

   519 

   520 lemma obj2sobj_ipc: "obj2sobj s obj = SIPC si iopt \<Longrightarrow> \<exists> i. obj = IPC i"

   521 by (case_tac obj, case_tac [!] s, auto split:option.splits if_splits)

   522 

   523 lemma obj2sobj_file': 

   524   "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown\<rbrakk> \<Longrightarrow> \<exists> sf srf. sobj = SFile sf srf"

   525 by (case_tac sobj, case_tac [!] s, auto split:option.splits if_splits)

   526 

   527 lemma obj2sobj_proc': 

   528   "\<lbrakk>obj2sobj s (Proc p) = sobj; sobj \<noteq> Unknown\<rbrakk> \<Longrightarrow> \<exists> sp srp. sobj = SProc sp srp"

   529 by (case_tac sobj, case_tac [!] s, auto split:option.splits if_splits)

   530 

   531 lemma obj2sobj_ipc': 

   532   "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown\<rbrakk> \<Longrightarrow> \<exists> si sri. sobj =  SIPC si sri"

   533 by (case_tac sobj, case_tac [!] s, auto split:option.splits if_splits)

   534 

   535 lemma obj2sobj_file_remains_cons:

   536   assumes vs: "valid (e#s)" and exf: "f \<in> current_files s"

   537   and SF: "obj2sobj s (File f) = SFile sf srf" 

   538   and notdeled: "\<not> deleted (File f) (e#s)"

   539   shows "obj2sobj (e#s) (File f) = SFile sf srf"

   540 proof-

   541   from vs have os:"os_grant s e" and vs': "valid s" 

   542     by (auto dest:valid_cons valid_os)

   543   from notdeled exf have exf': "f \<in> current_files (e#s)" by (case_tac e, auto)

   544   have "etype_of_file (e # s) f = etype_of_file s f"

   545     using os vs vs' exf exf' 

   546     apply (case_tac e, auto simp:etype_of_file_def split:option.splits) 

   547     by (auto dest:ancient_file_in_current intro!:etype_aux_prop)

   548   moreover have "source_dir (e # s) f = source_dir s f"

   549     using os vs vs' exf exf'

   550     by (case_tac e, auto simp:source_dir_simps dest:source_dir_prop)

   551   ultimately show ?thesis using vs SF notdeled 

   552     by (auto split:if_splits option.splits dest:not_deleted_cons_D)

   553 qed

   554 

   555 lemma obj2sobj_file_remains_cons':

   556   "\<lbrakk>valid (e#s); f \<in> current_files s; obj2sobj s (File f) = SFile sf srf; no_del_event (e#s)\<rbrakk>

   557    \<Longrightarrow> obj2sobj (e#s) (File f) = SFile sf srf"

   558 by (auto intro!:obj2sobj_file_remains_cons nodel_imp_un_deleted

   559        simp del:obj2sobj.simps)

   560 

   561 lemma obj2sobj_file_remains':

   562   "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown; valid (e#s); f \<in> current_files s;

   563     no_del_event (e#s)\<rbrakk> \<Longrightarrow> obj2sobj (e#s) (File f) = sobj"

   564 apply (frule obj2sobj_file', simp, (erule exE)+)

   565 apply (simp del:obj2sobj.simps)

   566 apply (erule obj2sobj_file_remains_cons', simp+)

   567 done

   568 

   569 lemma obj2sobj_file_remains_app:

   570   "\<lbrakk>obj2sobj s (File f) = SFile sf srf; valid (s' @ s); f \<in> current_files s;

   571     \<not> deleted (File f) (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = SFile sf srf"

   572 apply (induct s', simp)

   573 apply (simp only:cons_app_simp_aux)

   574 apply (frule valid_cons, frule not_deleted_cons_D)

   575 apply (drule_tac s = "s'@s" in obj2sobj_file_remains_cons, auto simp del:obj2sobj.simps)

   576 apply (drule_tac obj = "File f" in not_deleted_imp_exists', simp+)

   577 done

   578 

   579 lemma obj2sobj_file_remains_app':

   580   "\<lbrakk>obj2sobj s (File f) = SFile sf srf; valid (s' @ s); f \<in> current_files s;

   581     no_del_event (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = SFile sf srf"

   582 by (auto intro!:obj2sobj_file_remains_app nodel_imp_un_deleted

   583        simp del:obj2sobj.simps)

   584 

   585 lemma obj2sobj_file_remains'':

   586   "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown; valid (s'@s); f \<in> current_files s;

   587     no_del_event (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = sobj"

   588 apply (frule obj2sobj_file', simp, (erule exE)+)

   589 apply (simp del:obj2sobj.simps)

   590 apply (erule obj2sobj_file_remains_app', simp+)

   591 done

   592 

   593 lemma obj2sobj_file_remains''':

   594   "\<lbrakk>obj2sobj s (File f) = sobj; sobj \<noteq> Unknown; valid (s'@s); f \<in> current_files s;

   595     \<not>deleted (File f) (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (File f) = sobj"

   596 apply (frule obj2sobj_file', simp, (erule exE)+)

   597 apply (simp del:obj2sobj.simps)

   598 by (erule obj2sobj_file_remains_app, simp+)

   599 

   600 lemma obj2sobj_ipc_remains_cons:

   601   "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk>

   602   \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"

   603 apply (frule valid_cons, frule valid_os, case_tac e)

   604 by (auto simp:ni_init_deled ni_notin_curi split:option.splits

   605         dest!:current_proc_has_role')

   606 

   607 lemma obj2sobj_ipc_remains_cons':

   608   "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk>

   609   \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"

   610 by (auto intro!:obj2sobj_ipc_remains_cons nodel_imp_un_deleted

   611        simp del:obj2sobj.simps)

   612 

   613 lemma obj2sobj_ipc_remains':

   614   "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown; valid (e#s); i \<in> current_ipcs s; 

   615     no_del_event (e#s)\<rbrakk> \<Longrightarrow> obj2sobj (e#s) (IPC i) = sobj"

   616 apply (frule obj2sobj_ipc', simp, (erule exE)+)

   617 apply (simp del:obj2sobj.simps)

   618 apply (erule obj2sobj_ipc_remains_cons', simp+)

   619 done

   620 

   621 lemma obj2sobj_ipc_remains_app:

   622   "\<lbrakk>obj2sobj s (IPC i) = SIPC si sri; valid (s'@s); i \<in> current_ipcs s; \<not> deleted (IPC i) (s'@s)\<rbrakk>

   623   \<Longrightarrow> obj2sobj (s'@s) (IPC i) = SIPC si sri"

   624 apply (induct s', simp)

   625 apply (simp only:cons_app_simp_aux)

   626 apply (frule valid_cons, frule not_deleted_cons_D)

   627 apply (drule_tac s = "s'@s" in obj2sobj_ipc_remains_cons, auto simp del:obj2sobj.simps)

   628 apply (drule_tac obj = "IPC i" in not_deleted_imp_exists', simp+)

   629 done

   630 

   631 lemma obj2sobj_ipc_remains_app':

   632   "\<lbrakk>obj2sobj s (IPC i) = SIPC si sri; valid (s'@s); i \<in> current_ipcs s; no_del_event (s'@s)\<rbrakk>

   633   \<Longrightarrow> obj2sobj (s'@s) (IPC i) = SIPC si sri"

   634 by (auto intro!:obj2sobj_ipc_remains_app nodel_imp_un_deleted

   635        simp del:obj2sobj.simps)

   636 

   637 lemma obj2sobj_ipc_remains'':

   638   "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown; valid (s'@s); i \<in> current_ipcs s; 

   639     no_del_event (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (IPC i) = sobj"

   640 apply (frule obj2sobj_ipc', simp, (erule exE)+)

   641 apply (simp del:obj2sobj.simps)

   642 apply (erule obj2sobj_ipc_remains_app', simp+)

   643 done

   644 

   645 lemma obj2sobj_ipc_remains''':

   646   "\<lbrakk>obj2sobj s (IPC i) = sobj; sobj \<noteq> Unknown; valid (s'@s); i \<in> current_ipcs s; 

   647     \<not> deleted (IPC i) (s'@s)\<rbrakk> \<Longrightarrow> obj2sobj (s'@s) (IPC i) = sobj"

   648 apply (frule obj2sobj_ipc', simp, (erule exE)+)

   649 apply (simp del:obj2sobj.simps)

   650 apply (erule obj2sobj_ipc_remains_app, simp+)

   651 done

   652 

   653 end

   654 

   655 context tainting_s_sound begin

   656 

   657 lemma cp2sproc_clone':

   658   "valid (Clone p p' # s) \<Longrightarrow> cp2sproc (Clone p p' # s) = (cp2sproc s) (p' := cp2sproc s p)"

   659 by (drule cp2sproc_clone, auto split:option.splits simp:clone_type_unchange clone_type_aux_def)

   660 

   661 lemmas cp2sproc_simps' =  cp2sproc_exec cp2sproc_chown cp2sproc_crole cp2sproc_clone' cp2sproc_other

   662 

   663 lemma clone_sobj_keeps_same:

   664   "valid (Clone p p' # s) \<Longrightarrow> obj2sobj (Clone p p' # s) (Proc p') = obj2sobj s (Proc p)"

   665 apply (frule valid_cons, frule valid_os, clarsimp)

   666 apply (auto split:option.splits t_rc_proc_type.splits

   667              dest:current_proc_has_role current_proc_has_forcedrole 

   668                   current_proc_has_type current_proc_has_owner default_process_create_type_valid

   669              simp:pct_def clone_type_unchange)

   670 done

   671 

   672 end

   673 

   674 end