theory os_rc 

imports Main rc_theory 

begin

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

context rc_basic begin

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

lemma valid_cons:

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

by (drule vs_step', auto)

lemma valid_os: 

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

by (drule vs_step', auto)

lemma valid_rc:

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

by (drule vs_step', auto)

lemma vs_history:

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

apply (induct s', simp add:no_junior_def)

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

apply (drule no_junior_noteq, simp)

by (drule valid_cons)

lemma parent_file_in_current: 

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

apply (induct s)

apply (simp add:parent_file_in_init)

apply (frule valid_cons, frule valid_rc, frule valid_os)

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

apply (case_tac f, simp+)

done

lemma parent_file_in_current': 

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

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

lemma parent_file_in_init': 

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

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

lemma ancient_file_in_current:

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

apply (induct f)

apply (simp add:no_junior_def)

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

apply (drule no_junior_noteq, simp)

apply (drule parent_file_in_current', simp+)

done

lemma cannot_del_root:

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

apply (frule valid_cons, frule valid_os)

apply (case_tac f rule:rev_cases, simp)

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

done

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

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

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

apply (induct s arbitrary:f) 

apply (simp, rule init_file_initialrole_imp_some)

apply (frule valid_cons, frule valid_os, case_tac a)

apply (auto split:if_splits option.splits)

done

lemma file_has_initialrole':

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

by (rule notI, auto dest:file_has_initialrole)

lemma file_has_effinitialrole: 

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

apply (induct f)

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

done

lemma file_has_effinitialrole':

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

by (rule notI, auto dest:file_has_effinitialrole)

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

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

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

apply (induct s arbitrary:f) 

apply (simp add:init_file_forcedrole_imp_some)

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

done

lemma file_has_forcedrole':

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

by (rule notI, auto dest:file_has_forcedrole)

lemma file_has_effforcedrole: 

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

apply (induct f)

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

done

lemma file_has_effforcedrole':

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

by (rule notI, auto dest:file_has_effforcedrole)

lemma current_proc_has_forcedrole:

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

apply (induct s arbitrary:p) using init_proc_has_frole

apply (simp add:bidirect_in_init_def)

apply (frule valid_cons, frule valid_os, case_tac a)

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

done

lemma current_proc_has_forcedrole':

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

by (rule notI, auto dest:current_proc_has_forcedrole)

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

apply (induct s arbitrary:p) using init_proc_has_owner

apply (simp add:bidirect_in_init_def)

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

done

lemma current_proc_has_owner':

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

by (rule notI, auto dest:current_proc_has_owner)

(*

lemma effinitial_normal_intro: 

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

apply (drule file_has_effinitialrole, simp)

apply (erule exE, frule effinitialrole_valid, simp)

done

lemma effforced_normal_intro: 

  "\<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> 

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

apply (drule file_has_effforcedrole, simp)

apply (erule exE, frule effforcedrole_valid, simp)

done

*)

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

apply (induct s arbitrary:p) defer

apply (frule valid_cons, frule valid_os, case_tac a)

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

done

lemma user_has_normalrole: 

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

by (auto simp:bidirect_in_init_def)

lemma user_has_normalrole':

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

by (rule notI, auto dest:user_has_normalrole)

lemma current_proc_has_role: 

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

apply (induct s arbitrary:p) using init_proc_has_role

apply (simp add:bidirect_in_init_def)

apply (frule valid_cons, frule valid_os, case_tac a)

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

           dest!:current_proc_has_owner' user_has_normalrole' current_proc_has_forcedrole'

                 file_has_forcedrole' file_has_effforcedrole' 

                 file_has_initialrole' file_has_effinitialrole'

           intro:user_has_normalrole

            dest:owner_in_users effinitialrole_valid effforcedrole_valid proc_forcedrole_valid)

done

lemma current_file_has_type: 

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

apply (induct s)

apply (simp split:option.splits)

apply (frule valid_cons, frule valid_os, case_tac a)

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

done

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

apply (induct f) defer

apply (frule parent_file_in_init') 

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

done

lemma current_file_has_etype[rule_format]:

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

apply (induct f)

apply (auto simp:etype_of_file_def dest:current_file_has_type parent_file_in_current'

           split:option.splits t_rc_file_type.splits)

done

lemma current_file_has_etype':

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

by (rule notI, auto dest:current_file_has_etype)

(*** etype_of_file simpset ***)

lemma etype_aux_prop:

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

apply (induct f)

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

lemma etype_aux_prop1:

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

by (rule etype_aux_prop, auto simp:no_junior_def)

lemma etype_aux_prop1':

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

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

apply (simp, rule etype_aux_prop1, simp)

done

lemma etype_aux_prop2:

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

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

apply (rule etype_aux_prop)

by (auto dest:ancient_file_in_current)

lemma etype_aux_prop3:

  "parent f = Some pf 

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

apply (case_tac f, simp+)

by (rule etype_aux_prop, simp add:no_junior_def)

lemma etype_aux_prop4:

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

by (case_tac f, auto)

lemma etype_of_file_delete:

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

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

apply (frule valid_cons, frule valid_os)

apply (simp add:etype_of_file_def)

done

lemma current_proc_has_type: 

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

apply (induct s arbitrary:p) using init_proc_has_type

apply (simp add:bidirect_in_init_def)

apply (frule valid_cons, frule valid_os, case_tac a)

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

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

apply (auto simp:pct_def pot_def pet_def dest:current_proc_has_role 

           split:option.splits t_rc_proc_type.splits 

           dest!:default_process_create_type_valid default_process_chown_type_valid 

                 default_process_execute_type_valid)

done

lemma current_ipc_has_type: 

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

apply (induct s) using init_ipc_has_type

apply (simp add:bidirect_in_init_def)

apply (frule valid_cons, frule valid_os, case_tac a)

apply (auto dest:current_proc_has_role)

done

(*** finite current_*  ***)

lemma finite_cf: "finite (current_files s)"

apply (induct s) defer apply (case_tac a)

using init_finite by auto

lemma finite_cp: "finite (current_procs s)"

apply (induct s) defer apply (case_tac a)

using init_finite by auto

lemma finite_ci: "finite (current_ipcs s)"

apply (induct s) defer apply (case_tac a)

using init_finite by auto

end

context tainting_s_complete begin

lemma init_notin_curf_deleted:

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

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

lemma init_notin_curi_deleted:

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

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

lemma init_notin_curp_deleted:

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

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

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

by (induct f, auto split:if_splits)

lemma source_proc_in_init:

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

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

apply (frule valid_os, frule valid_cons, case_tac a)

by (auto split:if_splits)

end

context tainting_s_sound begin

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

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

apply (erule finite.induct, simp)

apply (rule ballI)

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

done

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

apply (drule nn_notin_aux)

apply (simp add:next_nat_def)

by (auto)

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

by (simp add:new_proc_def nn_notin)

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

by (simp add:np_notin_curp)

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

by (simp add:new_ipc_def nn_notin)

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

by (simp add:ni_notin_curi)

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

using ni_notin_curi[where \<tau> = s]

by (drule_tac init_notin_curi_deleted, simp+)

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

using np_notin_curp[where \<tau> = s]

by (drule_tac init_notin_curp_deleted, simp+)

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

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

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

apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)

apply (rule notI)

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}")

defer apply simp

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}")

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

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

defer

apply (simp add:fname_length_set_def) 

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

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

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

unfolding image_def

apply(auto)[1]

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

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

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

apply (simp add:len_fname_all, simp)

done

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

by (simp add:new_childf_def)

lemma clone_event_no_limit: 

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

apply (rule vs_step)

apply (auto intro:clone_no_limit split:option.splits dest!:np_notin_curp'

            dest:current_proc_has_role current_proc_has_type)

done 

end

end