1 theory del_vs_del_s

     2 imports Main rc_theory os_rc obj2sobj_prop all_sobj_prop 

     3 begin

     4 

     5 context tainting_s_complete begin

     6 

     7 lemma deleted_has_del_event_proc:

     8   "\<lbrakk>deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p'. Kill p' p # s' \<preceq> s \<and> \<not> deleted (Proc p) s'"

     9 apply (induct s, simp)

    10 apply (frule valid_cons, frule valid_os)

    11 by (case_tac a, auto simp:no_junior_def)

    12 

    13 lemma deleted_has_del_event_ipc:

    14   "\<lbrakk>deleted (IPC i) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p. DeleteIPC p i # s' \<preceq> s \<and> \<not> deleted (IPC i) s'"

    15 apply (induct s, simp)

    16 apply (frule valid_cons, frule valid_os)

    17 by (case_tac a, auto simp:no_junior_def)

    18 

    19 lemma deleted_has_del_event_file:

    20   "\<lbrakk>deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p. DeleteFile p f # s' \<preceq> s \<and> \<not> deleted (File f) s'"

    21 apply (induct s, simp)

    22 apply (frule valid_cons, frule valid_os)

    23 by (case_tac a, auto simp:no_junior_def)

    24 

    25 (*

    26 lemma noJ_Anc: "x \<prec> y = (x \<preceq> y \<and> x \<noteq> y)"

    27 apply (simp add: no_junior_expand)

    28 by (auto simp:is_ancestor_def)

    29 

    30 lemma noJ_Anc': "x \<prec> y \<Longrightarrow> (x \<preceq> y \<and> x \<noteq> y)"

    31 by (simp add:noJ_Anc)

    32 

    33 lemma noJ_Anc'': "\<lbrakk>x \<preceq> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<prec> y"

    34 by (simp add:noJ_Anc)

    35 

    36 lemma deled_imp_no_childfs:

    37   "\<lbrakk>valid (DeleteFile p f # s); f \<prec> childf\<rbrakk> \<Longrightarrow> childf \<notin> current_files s"

    38 apply (frule valid_cons, drule valid_os, rule notI, clarsimp dest!:noJ_Anc')

    39 apply (drule ancient_has_parent, simp, clarsimp)

    40 apply (drule_tac af = sonf and f = childf in ancient_file_in_current, simp+)

    41 apply (case_tac sonf, simp)

    42 apply (erule_tac x = a in allE, simp)

    43 done

    44 

    45 lemma deled_imp_childfs_deleted:

    46   "\<lbrakk>valid (DeleteFile p f # s); f \<prec> childf; childf \<in> init_files\<rbrakk>

    47   \<Longrightarrow> deleted (File childf) s"

    48 apply (drule deled_imp_no_childfs, simp+)

    49 apply (erule_tac P = "childf \<in> current_files s" in swap)

    50 by (drule not_deleted_imp_exists, simp+)

    51 

    52 lemma initf_deled_imp_childf_deled:

    53   "\<lbrakk>deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p. DeleteFile p f # s' \<preceq> s \<and> \<not> deleted (File f) s' \<and> (\<forall> childf \<in> init_files. f \<prec> childf \<longrightarrow> deleted (File childf) s')"

    54 apply (drule deleted_has_del_event_file, simp, clarify)

    55 apply (rule_tac x = s' in exI, rule_tac x = p in exI, simp)

    56 apply (rule ballI, rule impI, frule vs_history, simp)

    57 by (erule deled_imp_childfs_deleted, simp+)

    58 

    59 lemma initf_deled_imp_childf_deled:

    60   "\<lbrakk>deleted (File f) s; valid s; f \<prec> childf; childf \<in> init_files\<rbrakk> 

    61   \<Longrightarrow> \<exists> s'. s' \<preceq> s \<and> valid s' \<and> deleted (File childf) s'"

    62 apply (drule deleted_has_del_event_file, simp, clarify)

    63 apply (frule vs_history, simp, frule valid_cons)

    64 apply (drule deled_imp_childfs_deleted, simp, simp)

    65 apply (rule_tac x = s' in exI, auto elim:no_juniorE)

    66 done

    67 

    68 lemma deleted_has_del_event_allchildf:

    69   "\<lbrakk>deleted (File f) s; valid s; f \<preceq> childf; childf \<in> init_files\<rbrakk>

    70   \<Longrightarrow> \<exists> s' p. DeleteFile p childf # s' \<preceq> s \<and> \<not> deleted (File childf) s'"

    71 apply (case_tac "f = childf")

    72 apply (drule deleted_has_del_event_file, simp, simp)

    73 apply (drule noJ_Anc'', simp)

    74 apply (drule initf_deled_imp_childf_deled, simp+, clarify)

    75 apply (drule deleted_has_del_event_file, simp+, clarify)

    76 apply (rule_tac x = s'a in exI, rule conjI, rule_tac x = p in exI)

    77 apply (erule no_junior_trans, simp+)

    78 done

    79 *)

    80 

    81 lemma del_imp_del_s_file:

    82   assumes initf: "f \<in> init_files"

    83   and deled: "deleted (File f) s"

    84   and vs: "valid s"

    85   shows "file_deletable_s f"

    86 proof -

    87   from deled vs obtain s' p' where

    88     his: "DeleteFile p' f # s' \<preceq> s" and fstdel: "\<not> deleted (File f) s'"

    89     by (drule_tac deleted_has_del_event_file, auto)

    90   from his vs have "valid (DeleteFile p' f # s')" by (simp add:vs_history)

    91   hence exp': "p' \<in> current_procs s'" and exf: "f \<in> current_files s'"

    92     and rc: "rc_grant s' (DeleteFile p' f)" and vs': "valid s'"

    93     by (auto dest:valid_os valid_rc valid_cons)

    94 

    95   from initf obtain t where etype: "etype_of_file [] f = Some t"

    96     by (drule_tac init_file_has_etype, simp add:etype_of_file_def, blast)

    97   from initf have sd: "source_dir [] f = Some f"

    98     by (simp add:source_dir_of_init') 

    99   hence "obj2sobj [] (File f) = SFile (t, f) (Some f)"

   100     using etype initf by (auto simp:obj2sobj.simps)

   101   with fstdel vs' initf exf etype

   102   have SF: "obj2sobj s' (File f) = SFile (t, f) (Some f)"

   103     using obj2sobj_file_remains'''[where s = "[]" and s' = s']

   104     by (auto simp:obj2sobj.simps)

   105 

   106   from exp' vs' obtain r' fr' pt' u' srp' where

   107     SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'"

   108     by (frule_tac current_proc_has_sobj, simp, blast)

   109   with exp' vs' all_sobjs_I[where s = s' and obj = "Proc p'"]

   110   have SP'_in: "SProc (r',fr',pt',u') srp' \<in> all_sobjs" by simp

   111 

   112   show ?thesis unfolding file_deletable_s_def

   113     apply (rule_tac x = t in exI, 

   114            rule_tac x = "(r',fr',pt',u')" in exI,

   115            rule_tac x = srp' in exI)

   116     apply (simp add:SP'_in) 

   117     using rc SP' SF etype

   118     by (auto simp:obj2sobj.simps cp2sproc.simps split:option.splits if_splits)

   119 qed

   120 

   121 lemma del_imp_del_s_proc:

   122   assumes initp: "p \<in> init_processes"

   123   and deled: "deleted (Proc p) s"

   124   and vs: "valid s"

   125   shows "proc_deletable_s p"

   126 proof-

   127   from deled vs obtain s' p' where

   128     his: "Kill p' p # s' \<preceq> s" and fstdel: "\<not> deleted (Proc p) s'"

   129     by (drule_tac deleted_has_del_event_proc, auto)

   130   from his vs have "valid (Kill p' p # s')" by (simp add:vs_history)

   131   hence exp': "p' \<in> current_procs s'" and exp: "p \<in> current_procs s'"

   132     and rc: "rc_grant s' (Kill p' p)" and vs': "valid s'"

   133     by (auto dest:valid_os valid_rc valid_cons)

   134 

   135   from initp fstdel vs' have "source_proc s' p = Some p"

   136     apply (induct s', simp)

   137     apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)

   138     by (case_tac a, auto dest:not_deleted_imp_exists simp:np_notin_curp)

   139   with exp initp vs' obtain r fr pt u 

   140     where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)"

   141     apply (frule_tac current_proc_has_sobj, simp)

   142     by (simp add:obj2sobj.simps split:option.splits, blast)

   143   with exp vs' all_sobjs_I[where s = s' and obj = "Proc p"]

   144   have SP_in: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" by simp

   145 

   146   from exp' vs' obtain r' fr' pt' u' srp' where

   147     SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'"

   148     by (frule_tac current_proc_has_sobj, simp, blast)

   149   with exp' vs' all_sobjs_I[where s = s' and obj = "Proc p'"]

   150   have SP'_in: "SProc (r',fr',pt',u') srp' \<in> all_sobjs" by simp

   151 

   152   show ?thesis unfolding proc_deletable_s_def

   153     apply (rule_tac x = r in exI, rule_tac x = fr in exI,

   154            rule_tac x = pt in exI, rule_tac x = u in exI,

   155            rule_tac x = "(r',fr',pt',u')" in exI,

   156            rule_tac x = srp' in exI)

   157     apply (simp add:SP_in SP'_in) 

   158     using rc SP SP'

   159     by (auto simp:obj2sobj.simps cp2sproc.simps split:option.splits)

   160 qed

   161     

   162 lemma del_imp_del_s_ipc:

   163   assumes initi: "i \<in> init_ipcs"

   164   and deled: "deleted (IPC i) s"

   165   and vs: "valid s"

   166   shows "ipc_deletable_s i"

   167 proof-

   168   from deled vs obtain s' p' where

   169     his: "DeleteIPC p' i # s' \<preceq> s" and fstdel: "\<not> deleted (IPC i) s'"

   170     by (drule_tac deleted_has_del_event_ipc, auto)

   171   from his vs have "valid (DeleteIPC p' i # s')" by (simp add:vs_history)

   172   hence exp': "p' \<in> current_procs s'" and exi: "i \<in> current_ipcs s'"

   173     and rc: "rc_grant s' (DeleteIPC p' i)" and vs': "valid s'"

   174     by (auto dest:valid_os valid_rc valid_cons)

   175 

   176   from initi obtain t where type: "init_ipc_type i = Some t" 

   177     using init_ipc_has_type by (auto simp:bidirect_in_init_def)

   178   with fstdel vs' initi exi have SI: "obj2sobj s' (IPC i) = SIPC t (Some i)"

   179     using obj2sobj_ipc_remains'''[where s = "[]" and s' = s']

   180     by (auto simp:obj2sobj.simps)

   181 

   182   from exp' vs' obtain r' fr' pt' u' srp' where

   183     SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'"

   184     by (frule_tac current_proc_has_sobj, simp, blast)

   185   with exp' vs' all_sobjs_I[where s = s' and obj = "Proc p'"]

   186   have SP'_in: "SProc (r',fr',pt',u') srp' \<in> all_sobjs" by simp

   187 

   188   show ?thesis unfolding ipc_deletable_s_def

   189     apply (rule_tac x = t in exI, 

   190            rule_tac x = "(r',fr',pt',u')" in exI,

   191            rule_tac x = srp' in exI)

   192     apply (simp add: SP'_in) 

   193     using rc SP' SI type

   194     by (auto simp:obj2sobj.simps cp2sproc.simps split:option.splits if_splits)

   195 qed

   196 

   197 lemma deleted_imp_deletable_s:

   198   "\<lbrakk>deleted obj s; exists [] obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"

   199 apply (case_tac obj)  

   200 apply (simp add:del_imp_del_s_proc)  

   201 apply (simp add:del_imp_del_s_file) 

   202 apply (simp add:del_imp_del_s_ipc)

   203 done

   204 

   205 (*

   206 lemma all_sobjs_E3:

   207   assumes prem: "sobj \<in> all_sobjs" 

   208   shows "\<exists> s obj. valid s \<and> obj2sobj s obj = sobj \<and> sobj_source_eq_obj sobj obj \<and> 

   209                   initp_intact_but s sobj \<and> exists s obj \<and> no_del_event s"

   210 proof-

   211   obtain t where "etype_of_file [] [] = Some t" 

   212     using root_in_filesystem current_file_has_etype[of "[]" "[]"] vs_nil 

   213     by auto

   214   with root_in_filesystem

   215   have "obj2sobj [] (File []) = SFile (t,[]) (Some [])"

   216     by (auto simp:obj2sobj.simps source_dir_of_init' 

   217             split:option.splits if_splits)

   218   moreover have "initp_intact []"

   219     by (auto simp:initp_intact_def cp2sproc.simps obj2sobj.simps 

   220             split:option.splits)

   221   ultimately show ?thesis

   222     using prem vs_nil root_in_filesystem 

   223     apply (drule_tac s' = "[]" and obj' = "File []" in all_sobjs_E2)

   224     apply (simp+, (erule exE|erule conjE)+)

   225     by (rule_tac x = s in exI, simp, rule_tac x = obj in exI, simp+)

   226 qed

   227 

   228 lemma del_s_imp_del_proc:

   229   assumes initp: "p \<in> init_processes"

   230   and del_s: "proc_deletable_s p"

   231   shows "\<exists> s. valid s \<and> deleted (Proc p) s"

   232 proof-

   233   from del_s obtain r fr pt u sp' srp' 

   234     where Target: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" 

   235     and Killer: "SProc sp' srp' \<in> all_sobjs"

   236     and rc: "(role_of_sproc sp', Proc_type pt, DELETE) \<in> compatible"

   237     using proc_deletable_s_def by auto

   238   

   239   from Target obtain s where vs: "valid s" 

   240     and "obj2sobj s (Proc p) = SProc (r,fr,pt,u) (Some p)" 

   241     and "exists s (Proc p)"  and "no_del_event s"

   242     and "initp_intact_but s (SProc (r,fr,pt,u) (Some p))"

   243     apply (drule_tac all_sobjs_E3, clarsimp)

   244     by (frule obj2sobj_proc, clarsimp)

   245   with Killer obtain s' p' where vs': "valid (s' @ s)" and

   246     SP : "obj2sobj (s' @ s) (Proc p) = SProc (r,fr,pt,u) (Some p)" and

   247     exp: "exists (s' @ s) (Proc p)"  and

   248     SP': "obj2sobj (s' @ s) (Proc p') = SProc sp' srp'" and

   249     exp': "exists (s' @ s) (Proc p')"

   250     apply (drule_tac obj' = "Proc p" and s' = s in all_sobjs_E1, auto)

   251     apply (frule_tac obj = obj in obj2sobj_proc, erule exE)

   252     apply (auto intro:nodel_exists_remains)

   253     apply blast

   254     apply (frule_tac obj = "Proc p" in nodel_exists_remains)

   255 

   256 

   257 lemma deletable_s_imp_deleted:

   258   "deletable_s obj \<Longrightarrow> \<exists> s. valid s \<and> deleted obj s"

   259 apply (case_tac obj)

   260 apply (simp add:deletable_s.simps)

   261 

   262 

   263 lemma valid_kill_imp_proc_del_s:

   264   "\<lbrakk>valid (Kill p' p # s); p \<in> init_processes; \<not> deleted (Proc p) s\<rbrakk> \<Longrightarrow> proc_deletable_s p"

   265 apply (frule valid_os, frule valid_

   266 

   267 

   268 lemma build_phase: "f \<in> init_files \<and> file_deletable_s f \<longrightarrow> (\<exists> s. \<forall> childf. valids s \<and> f \<preceq> childf \<and> childf \<in> init_files \<and> etype_of_file [] f = Some t \<longrightarrow> (\<exists> p. p \<in> current_procs s \<and> currentrole s p = Some r \<and> (r, File_type t, DELETE) \<in> compatible))"

   269  thm all_sobjs_E0

   270 

   271 lemma del_phase: "f \<in> init_files \<and> file_deletable_s f \<and> (\<forall> childf. f \<preceq> childf \<and> childf \<notin> current_files s \<and> valid s"

   272 

   273 *)

   274 

   275 end

   276 

   277 end