1
+ − 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)
6
+ − 138
by (case_tac a, auto dest:not_deleted_imp_exists)
1
+ − 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