1 theory os_rc 

     2 imports Main rc_theory 

     3 begin

     4 

     5 (****** below context is for lemmas of OS and RC ******)

     6 context rc_basic begin

     7 

     8 inductive_cases vs_step': "valid (e # \<tau>)" 

     9 

    10 lemma valid_cons:

    11   "valid (e # \<tau>) \<Longrightarrow> valid \<tau>"

    12 by (drule vs_step', auto)

    13 

    14 lemma valid_os: 

    15   "valid (e # \<tau>) \<Longrightarrow> os_grant \<tau> e"

    16 by (drule vs_step', auto)

    17 

    18 lemma valid_rc:

    19   "valid (e # \<tau>) \<Longrightarrow> rc_grant \<tau> e"

    20 by (drule vs_step', auto)

    21 

    22 lemma vs_history:

    23   "\<lbrakk>s \<preceq> s'; valid s'\<rbrakk> \<Longrightarrow> valid s"

    24 apply (induct s', simp add:no_junior_def)

    25 apply (case_tac "s = a # s'", simp)

    26 apply (drule no_junior_noteq, simp)

    27 by (drule valid_cons)

    28 

    29 lemma parent_file_in_current: 

    30   "\<lbrakk>parent f = Some pf; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"

    31 apply (induct s)

    32 apply (simp add:parent_file_in_init)

    33 apply (frule valid_cons, frule valid_rc, frule valid_os)

    34 apply (case_tac a, auto split:option.splits)

    35 apply (case_tac f, simp+)

    36 done

    37 

    38 lemma parent_file_in_current': 

    39   "\<lbrakk>fn # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"

    40 by (auto intro!:parent_file_in_current[where pf = pf])

    41 

    42 lemma parent_file_in_init': 

    43   "fn # pf \<in> init_files \<Longrightarrow> pf \<in> init_files"

    44 by (auto intro!:parent_file_in_init[where pf = pf])

    45 

    46 lemma ancient_file_in_current:

    47   "\<lbrakk>f \<in> current_files s; valid s; af \<preceq> f\<rbrakk> \<Longrightarrow> af \<in> current_files s"

    48 apply (induct f)

    49 apply (simp add:no_junior_def)

    50 apply (case_tac "af = a # f", simp)

    51 apply (drule no_junior_noteq, simp)

    52 apply (drule parent_file_in_current', simp+)

    53 done

    54 

    55 lemma cannot_del_root:

    56   "\<lbrakk>valid (DeleteFile p [] # s); f \<noteq> []; f \<in> current_files s\<rbrakk> \<Longrightarrow> False"

    57 apply (frule valid_cons, frule valid_os)

    58 apply (case_tac f rule:rev_cases, simp)

    59 apply (drule_tac af = "[y]" in ancient_file_in_current, simp+)

    60 done

    61 

    62 lemma init_file_initialrole_imp_some: "\<exists> r. init_file_initialrole f = Some r"

    63 by (case_tac f, auto split:option.splits)

    64 

    65 lemma file_has_initialrole: "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> (\<exists> r. initialrole s f = Some r)"

    66 apply (induct s arbitrary:f) 

    67 apply (simp, rule init_file_initialrole_imp_some)

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

    69 apply (auto split:if_splits option.splits)

    70 done

    71 

    72 lemma file_has_initialrole':

    73   "\<lbrakk>initialrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

    74 by (rule notI, auto dest:file_has_initialrole)

    75 

    76 lemma file_has_effinitialrole: 

    77   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. effinitialrole s f = Some r"

    78 apply (induct f)

    79 apply (auto simp:effinitialrole_def dest:file_has_initialrole parent_file_in_current')

    80 done

    81 

    82 lemma file_has_effinitialrole':

    83   "\<lbrakk>effinitialrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

    84 by (rule notI, auto dest:file_has_effinitialrole)

    85 

    86 lemma init_file_forcedrole_imp_some: "\<exists> r. init_file_forcedrole f = Some r"

    87 by (case_tac f, auto split:option.splits)

    88 

    89 lemma file_has_forcedrole: "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> (\<exists> r. forcedrole s f = Some r)"

    90 apply (induct s arbitrary:f) 

    91 apply (simp add:init_file_forcedrole_imp_some)

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

    93 done

    94 

    95 lemma file_has_forcedrole':

    96   "\<lbrakk>forcedrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

    97 by (rule notI, auto dest:file_has_forcedrole)

    98 

    99 lemma file_has_effforcedrole: 

   100   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. effforcedrole s f = Some r"

   101 apply (induct f)

   102 apply (auto simp:effforcedrole_def dest:file_has_forcedrole parent_file_in_current')

   103 done

   104 

   105 lemma file_has_effforcedrole':

   106   "\<lbrakk>effforcedrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   107 by (rule notI, auto dest:file_has_effforcedrole)

   108 

   109 lemma current_proc_has_forcedrole:

   110   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. proc_forcedrole s p = Some r"

   111 apply (induct s arbitrary:p) using init_proc_has_frole

   112 apply (simp add:bidirect_in_init_def)

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

   114 apply (auto split:if_splits option.splits intro:file_has_effforcedrole)

   115 done

   116 

   117 lemma current_proc_has_forcedrole':

   118   "\<lbrakk>proc_forcedrole s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"

   119 by (rule notI, auto dest:current_proc_has_forcedrole)

   120 

   121 lemma current_proc_has_owner: "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> u. owner s p = Some u"

   122 apply (induct s arbitrary:p) using init_proc_has_owner

   123 apply (simp add:bidirect_in_init_def)

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

   125 done

   126 

   127 lemma current_proc_has_owner':

   128   "\<lbrakk>owner s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"

   129 by (rule notI, auto dest:current_proc_has_owner)

   130 

   131 (*

   132 lemma effinitial_normal_intro: 

   133   "\<lbrakk>f \<in> current_files \<tau>; valid \<tau>; effinitialrole \<tau> f \<noteq> Some UseForcedRole\<rbrakk> \<Longrightarrow> \<exists>nr. effinitialrole \<tau> f = Some (NormalRole nr)"

   134 apply (drule file_has_effinitialrole, simp)

   135 apply (erule exE, frule effinitialrole_valid, simp)

   136 done

   137 

   138 lemma effforced_normal_intro: 

   139   "\<lbrakk>f \<in> current_files \<tau>; valid \<tau>; effforcedrole \<tau> f \<noteq> Some InheritUserRole; effforcedrole \<tau> f \<noteq> Some InheritProcessRole; effforcedrole \<tau> f \<noteq> Some InheritUpMixed\<rbrakk> 

   140   \<Longrightarrow> \<exists>nr. effforcedrole \<tau> f = Some (NormalRole nr)"

   141 apply (drule file_has_effforcedrole, simp)

   142 apply (erule exE, frule effforcedrole_valid, simp)

   143 done

   144 *)

   145 

   146 lemma owner_in_users: "\<lbrakk>owner s p = Some u; valid s\<rbrakk> \<Longrightarrow> u \<in> init_users"

   147 apply (induct s arbitrary:p) defer

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

   149 apply (auto split:if_splits option.splits intro!:init_owner_valid)

   150 done

   151 

   152 lemma user_has_normalrole: 

   153   "u \<in> init_users \<Longrightarrow> \<exists> nr. defrole u = Some nr" using init_user_has_role

   154 by (auto simp:bidirect_in_init_def)

   155 

   156 lemma user_has_normalrole':

   157   "defrole u = None \<Longrightarrow> u \<notin> init_users"

   158 by (rule notI, auto dest:user_has_normalrole)

   159 

   160 lemma current_proc_has_role: 

   161   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nr. currentrole s p = Some nr"

   162 apply (induct s arbitrary:p) using init_proc_has_role

   163 apply (simp add:bidirect_in_init_def)

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

   165 apply (auto simp:map_comp_def split:if_splits option.splits t_role.splits

   166            dest!:current_proc_has_owner' user_has_normalrole' current_proc_has_forcedrole'

   167                  file_has_forcedrole' file_has_effforcedrole' 

   168                  file_has_initialrole' file_has_effinitialrole'

   169            intro:user_has_normalrole

   170             dest:owner_in_users effinitialrole_valid effforcedrole_valid proc_forcedrole_valid)

   171 done

   172 

   173 lemma current_file_has_type: 

   174   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_file s f = Some t"

   175 apply (induct s)

   176 apply (simp split:option.splits)

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

   178 apply (auto split:option.splits intro:current_proc_has_role)

   179 done

   180 

   181 lemma init_file_has_etype: "f \<in> init_files \<Longrightarrow> \<exists> nt. etype_aux init_file_type_aux f = Some nt"

   182 apply (induct f) defer

   183 apply (frule parent_file_in_init') 

   184 apply (auto split:option.splits t_rc_file_type.splits)

   185 done

   186 

   187 lemma current_file_has_etype[rule_format]:

   188   "f \<in> current_files s \<Longrightarrow> valid s \<longrightarrow> (\<exists> nt. etype_of_file s f = Some nt)"

   189 apply (induct f)

   190 apply (auto simp:etype_of_file_def dest:current_file_has_type parent_file_in_current'

   191            split:option.splits t_rc_file_type.splits)

   192 done

   193 

   194 lemma current_file_has_etype':

   195   "\<lbrakk>etype_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   196 by (rule notI, auto dest:current_file_has_etype)

   197 

   198 (*** etype_of_file simpset ***)

   199 

   200 lemma etype_aux_prop:

   201   "\<forall> x. x \<preceq> f \<longrightarrow> func' x = func x \<Longrightarrow> etype_aux func f = etype_aux func' f"

   202 apply (induct f)

   203 by (auto split:t_rc_file_type.splits option.splits)

   204 

   205 lemma etype_aux_prop1:

   206   "func' = func ((a#f) := b) \<Longrightarrow> etype_aux func f = etype_aux func' f"

   207 by (rule etype_aux_prop, auto simp:no_junior_def)

   208 

   209 lemma etype_aux_prop1':

   210   "etype_aux func f = x \<Longrightarrow> etype_aux (func ((a#f) := b)) f = x"

   211 apply (subgoal_tac "etype_aux func f = etype_aux (func ((a#f) := b)) f")

   212 apply (simp, rule etype_aux_prop1, simp)

   213 done

   214 

   215 lemma etype_aux_prop2:

   216   "\<lbrakk>f \<in> current_files s; f' \<notin> current_files s; valid s\<rbrakk> \<Longrightarrow>

   217   etype_aux (func (f' := b)) f = etype_aux func f"

   218 apply (rule etype_aux_prop)

   219 by (auto dest:ancient_file_in_current)

   220 

   221 lemma etype_aux_prop3:

   222   "parent f = Some pf 

   223    \<Longrightarrow> etype_aux (func (f := Some InheritParent_file_type)) f = etype_aux func pf"

   224 apply (case_tac f, simp+)

   225 by (rule etype_aux_prop, simp add:no_junior_def)

   226 

   227 lemma etype_aux_prop4:

   228   "etype_aux (func (f := Some (NormalFile_type t))) f = Some t"

   229 by (case_tac f, auto)

   230 

   231 lemma etype_of_file_delete:

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

   233    \<Longrightarrow> etype_of_file (DeleteFile p f # s) f' = etype_of_file s f'"

   234 apply (frule valid_cons, frule valid_os)

   235 apply (simp add:etype_of_file_def)

   236 done

   237 

   238 lemma current_proc_has_type: 

   239   "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nt. type_of_process s p = Some nt"

   240 apply (induct s arbitrary:p) using init_proc_has_type

   241 apply (simp add:bidirect_in_init_def)

   242 

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

   244 

   245 apply (subgoal_tac "nat1 \<in> current_procs (a # s)") prefer 2 apply simp

   246 apply (drule_tac p = nat1 in current_proc_has_role, simp, erule exE)

   247 

   248 apply (auto simp:pct_def pot_def pet_def dest:current_proc_has_role 

   249            split:option.splits t_rc_proc_type.splits 

   250            dest!:default_process_create_type_valid default_process_chown_type_valid 

   251                  default_process_execute_type_valid)

   252 done

   253 

   254 lemma current_ipc_has_type: 

   255   "\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nt. type_of_ipc s i = Some nt"

   256 apply (induct s) using init_ipc_has_type

   257 apply (simp add:bidirect_in_init_def)

   258 

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

   260 apply (auto dest:current_proc_has_role)

   261 done

   262 

   263 (*** finite current_*  ***)

   264 

   265 lemma finite_cf: "finite (current_files s)"

   266 apply (induct s) defer apply (case_tac a)

   267 using init_finite by auto

   268 

   269 lemma finite_cp: "finite (current_procs s)"

   270 apply (induct s) defer apply (case_tac a)

   271 using init_finite by auto

   272 

   273 lemma finite_ci: "finite (current_ipcs s)"

   274 apply (induct s) defer apply (case_tac a)

   275 using init_finite by auto

   276 

   277 (*** properties of new-proc new-ipc ... ***)

   278 

   279 lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "

   280 apply (erule finite.induct, simp)

   281 apply (rule ballI)

   282 apply (case_tac "aa = a", simp+)

   283 done

   284 

   285 lemma nn_notin: "finite s \<Longrightarrow> next_nat s \<notin> s"

   286 apply (drule nn_notin_aux)

   287 apply (simp add:next_nat_def)

   288 by (auto)

   289 

   290 lemma np_notin_curp: "new_proc \<tau> \<notin> current_procs \<tau>" using finite_cp

   291 by (simp add:new_proc_def nn_notin)

   292 

   293 lemma np_notin_curp': "new_proc \<tau> \<in> current_procs \<tau> \<Longrightarrow> False"

   294 by (simp add:np_notin_curp)

   295 

   296 lemma ni_notin_curi: "new_ipc \<tau> \<notin> current_ipcs \<tau>" using finite_ci

   297 by (simp add:new_ipc_def nn_notin)

   298 

   299 lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False"

   300 by (simp add:ni_notin_curi)

   301 

   302 end

   303 

   304 context tainting_s_complete begin

   305 

   306 lemma init_notin_curf_deleted:

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

   308 by (induct s, simp, case_tac a, auto)

   309 

   310 lemma init_notin_curi_deleted:

   311   "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"

   312 by (induct s, simp, case_tac a, auto)

   313 

   314 lemma init_notin_curp_deleted:

   315   "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"

   316 by (induct s, simp, case_tac a, auto)

   317   

   318 lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s"

   319 using ni_notin_curi[where \<tau> = s]

   320 by (drule_tac init_notin_curi_deleted, simp+)

   321 

   322 lemma np_init_deled: "new_proc s \<in> init_processes \<Longrightarrow> deleted (Proc (new_proc s)) s"

   323 using np_notin_curp[where \<tau> = s]

   324 by (drule_tac init_notin_curp_deleted, simp+)

   325 

   326 lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"

   327 by (induct f, auto split:if_splits)

   328 

   329 lemma source_proc_in_init:

   330   "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"

   331 apply (induct s arbitrary:p, simp split:if_splits)

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

   333 by (auto simp:np_notin_curp split:if_splits)

   334 

   335 end

   336 

   337 context tainting_s_sound begin

   338 

   339 lemma len_fname_all: "length (fname_all_a len) = len"

   340 by (induct len, auto simp:fname_all_a.simps)

   341 

   342 lemma ncf_notin_curf: "new_childf f s \<notin> current_files s"

   343 apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)

   344 apply (rule notI)

   345 apply (subgoal_tac "(CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s}))) \<in> {fn. fn # f \<in> current_files s}")

   346 defer apply simp

   347 apply (subgoal_tac "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s}))) \<in> fname_length_set {fn. fn # f \<in> current_files s}")

   348 defer apply (auto simp:fname_length_set_def image_def)[1]

   349 apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files s})")  

   350 defer

   351 apply (simp add:fname_length_set_def) 

   352 apply (rule finite_imageI) using finite_cf[where s = s]

   353 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)

   354 apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)

   355 unfolding image_def

   356 apply(auto)[1]

   357 apply (rule_tac x = "x # f" in bexI, simp+)

   358 apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files s})" in nn_notin_aux)

   359 apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s})))" in ballE)

   360 apply (simp add:len_fname_all, simp)

   361 done

   362 

   363 lemma ncf_parent: "parent (new_childf f \<tau>) = Some f"

   364 by (simp add:new_childf_def)

   365 

   366 lemma clone_event_no_limit: 

   367   "\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)"

   368 apply (rule vs_step)

   369 apply (auto intro:clone_no_limit split:option.splits

   370             dest:current_proc_has_role current_proc_has_type)

   371 done 

   372 

   373 

   374 end

   375 

   376 end