3 Temp Enrich Proc_fd_of_file_prop |
3 Temp Enrich Proc_fd_of_file_prop |
4 begin |
4 begin |
5 |
5 |
6 context tainting_s begin |
6 context tainting_s begin |
7 |
7 |
8 fun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state" |
8 fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)" |
9 where |
9 where |
10 "enrich_msgq [] tq dq = []" |
10 "enrich_file [] tf s = ({}, [])" |
11 | "enrich_msgq (CreateMsgq p q # s) tq dq = |
11 | "enrich_file (Open p f flags fd (Some inum) # s) tf s = |
12 (if (tq = q) |
12 " |
13 then (CreateMsgq p dq # CreateMsgq p q # s) |
|
14 else CreateMsgq p q # (enrich_msgq s tq dq))" |
|
15 | "enrich_msgq (SendMsg p q m # s) tq dq = |
|
16 (if (tq = q) |
|
17 then (SendMsg p dq m # SendMsg p q m # (enrich_msgq s tq dq)) |
|
18 else SendMsg p q m # (enrich_msgq s tq dq))" |
|
19 | "enrich_msgq (RecvMsg p q m # s) tq dq = |
|
20 (if (tq = q) |
|
21 then (RecvMsg p dq m # RecvMsg p q m # (enrich_msgq s tq dq)) |
|
22 else RecvMsg p q m # (enrich_msgq s tq dq))" |
|
23 | "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)" |
|
24 |
|
25 lemma enrich_msgq_duq_in: |
|
26 "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> |
|
27 \<Longrightarrow> q' \<in> current_msgqs (enrich_msgq s q q')" |
|
28 apply (induct s, simp) |
|
29 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
30 apply auto |
|
31 done |
|
32 |
|
33 lemma enrich_msgq_duq_sms: |
|
34 "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> |
|
35 \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') q' = msgs_of_queue s q" |
|
36 apply (induct s, simp) |
|
37 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
38 apply auto |
|
39 done |
|
40 |
|
41 lemma enrich_msgq_cur_inof: |
|
42 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
43 \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f" |
|
44 apply (induct s arbitrary:f, simp) |
|
45 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
46 apply (auto split:option.splits) |
|
47 done |
|
48 |
|
49 lemma enrich_msgq_cur_inos: |
|
50 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
51 \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s" |
|
52 apply (rule ext) |
|
53 apply (induct s, simp) |
|
54 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
55 apply (auto split:option.splits) |
|
56 done |
|
57 |
|
58 lemma enrich_msgq_cur_inos': |
|
59 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
60 \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock" |
|
61 apply (simp add:enrich_msgq_cur_inos) |
|
62 done |
|
63 |
|
64 lemma enrich_msgq_cur_inums: |
|
65 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
66 \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s" |
|
67 apply (auto simp:current_inode_nums_def current_file_inums_def |
|
68 current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos) |
|
69 done |
|
70 |
|
71 lemma enrich_msgq_cur_itag: |
|
72 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
73 \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s" |
|
74 apply (rule ext) |
|
75 apply (induct s, simp) |
|
76 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
77 apply (auto split:option.splits t_socket_type.splits) |
|
78 done |
|
79 |
|
80 lemma enrich_msgq_cur_tcps: |
|
81 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
82 \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s" |
|
83 apply (rule ext) |
|
84 apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos |
|
85 split:option.splits t_inode_tag.splits) |
|
86 done |
|
87 |
|
88 lemma enrich_msgq_cur_udps: |
|
89 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
90 \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s" |
|
91 apply (rule ext) |
|
92 apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos |
|
93 split:option.splits t_inode_tag.splits) |
|
94 done |
|
95 |
|
96 lemma enrich_msgq_cur_msgqs: |
|
97 "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> |
|
98 \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}" |
|
99 apply (induct s, simp) |
|
100 apply (frule vt_grant_os, frule vd_cons) |
|
101 apply (case_tac a, auto) |
|
102 done |
|
103 |
|
104 lemma enrich_msgq_cur_msgs: |
|
105 "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> |
|
106 \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') = (msgs_of_queue s) (q' := msgs_of_queue s q)" |
|
107 apply (rule ext, simp, rule conjI, rule impI) |
|
108 apply (simp add:enrich_msgq_duq_sms) |
|
109 apply (rule impI) |
|
110 apply (induct s, simp) |
|
111 apply (frule vt_grant_os, frule vd_cons) |
|
112 apply (case_tac a, auto) |
|
113 done |
|
114 |
|
115 lemma enrich_msgq_cur_procs: |
|
116 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
117 \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s" |
|
118 apply (induct s, simp) |
|
119 apply (frule vt_grant_os, frule vd_cons) |
|
120 apply (case_tac a, auto) |
|
121 done |
|
122 |
|
123 lemma enrich_msgq_cur_files: |
|
124 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
125 \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s" |
|
126 apply (auto simp:current_files_def) |
|
127 apply (simp add:enrich_msgq_cur_inof)+ |
|
128 done |
|
129 |
|
130 lemma enrich_msgq_cur_fds: |
|
131 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
132 \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s" |
|
133 apply (induct s, simp) |
|
134 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
135 apply auto |
|
136 done |
|
137 |
|
138 lemma enrich_msgq_filefd: |
|
139 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
140 \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s" |
|
141 apply (rule ext, rule ext) |
|
142 apply (induct s, simp) |
|
143 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
144 apply auto |
|
145 done |
|
146 |
|
147 lemma enrich_msgq_flagfd: |
|
148 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
149 \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s" |
|
150 apply (rule ext, rule ext) |
|
151 apply (induct s, simp) |
|
152 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
153 apply auto |
|
154 done |
|
155 |
|
156 lemma enrich_msgq_proc_fds: |
|
157 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
158 \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s" |
|
159 apply (auto simp:proc_file_fds_def enrich_msgq_filefd) |
|
160 done |
|
161 |
|
162 lemma enrich_msgq_hungs: |
|
163 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
164 \<Longrightarrow> files_hung_by_del (enrich_msgq s q q') = files_hung_by_del s" |
|
165 apply (induct s, simp) |
|
166 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
167 apply (auto simp:files_hung_by_del.simps) |
|
168 done |
|
169 |
|
170 lemma enrich_msgq_is_file: |
|
171 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
172 \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s" |
|
173 apply (rule ext) |
|
174 apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof |
|
175 split:option.splits t_inode_tag.splits) |
|
176 done |
|
177 |
|
178 lemma enrich_msgq_is_dir: |
|
179 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
180 \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s" |
|
181 apply (rule ext) |
|
182 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof |
|
183 split:option.splits t_inode_tag.splits) |
|
184 done |
|
185 |
|
186 lemma enrich_msgq_sameinode: |
|
187 "\<lbrakk>no_del_event s; valid s\<rbrakk> |
|
188 \<Longrightarrow> (f \<in> same_inode_files (enrich_msgq s q q') f') = (f \<in> same_inode_files s f')" |
|
189 apply (induct s, simp) |
|
190 apply (simp add:same_inode_files_def) |
|
191 apply (auto simp:enrich_msgq_is_file enrich_msgq_cur_inof) |
|
192 done |
|
193 |
|
194 lemma enrich_msgq_tainted_aux1: |
|
195 "\<lbrakk>no_del_event s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; valid s\<rbrakk> |
|
196 \<Longrightarrow> (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}) \<subseteq> tainted (enrich_msgq s q q')" |
|
197 apply (induct s, simp) |
|
198 apply (frule vt_grant_os, frule vd_cons) |
|
199 apply (case_tac a) |
|
200 apply (auto split:option.splits if_splits dest:tainted_in_current |
|
201 simp:enrich_msgq_filefd enrich_msgq_sameinode) |
|
202 done |
|
203 |
|
204 lemma enrich_msgq_tainted_aux2: |
|
205 "\<lbrakk>no_del_event s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; valid s; valid (enrich_msgq s q q')\<rbrakk> |
|
206 \<Longrightarrow> tainted (enrich_msgq s q q') \<subseteq> (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})" |
|
207 apply (induct s, simp) |
|
208 apply (frule vt_grant_os, frule vd_cons) |
|
209 apply (case_tac a) |
|
210 apply (auto split:option.splits if_splits simp:enrich_msgq_filefd enrich_msgq_sameinode |
|
211 dest:tainted_in_current vd_cons) |
|
212 apply (drule_tac vd_cons)+ |
|
213 apply (simp) |
|
214 apply (drule set_mp) |
|
215 apply simp |
|
216 apply simp |
|
217 apply (drule_tac s = s in tainted_in_current) |
|
218 apply simp+ |
|
219 done |
|
220 |
|
221 lemma enrich_msgq_alive: |
|
222 "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> |
|
223 \<Longrightarrow> alive (enrich_msgq s q q') obj" |
|
224 apply (case_tac obj) |
|
225 apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs |
|
226 enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds |
|
227 enrich_msgq_cur_tcps enrich_msgq_cur_udps) |
|
228 apply (rule impI, simp) |
|
229 done |
|
230 |
|
231 lemma enrich_msgq_alive': |
|
232 "\<lbrakk>alive (enrich_msgq s q q') obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> |
|
233 \<Longrightarrow> alive s obj \<or> obj = O_msgq q' \<or> (\<exists> m. obj = O_msg q' m \<and> alive s (O_msg q m))" |
|
234 apply (case_tac obj) |
|
235 apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs |
|
236 enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds |
|
237 enrich_msgq_cur_tcps enrich_msgq_cur_udps) |
|
238 apply (auto split:if_splits) |
|
239 done |
|
240 |
|
241 lemma enrich_msgq_not_alive: |
|
242 "\<lbrakk>enrich_not_alive s (E_msgq q') obj; q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk> |
|
243 \<Longrightarrow> enrich_not_alive (enrich_msgq s q q') (E_msgq q') obj" |
|
244 apply (case_tac obj) |
|
245 apply (auto simp:enrich_msgq_cur_fds enrich_msgq_cur_files |
|
246 enrich_msgq_cur_procs enrich_msgq_cur_inums enrich_msgq_cur_msgqs enrich_msgq_cur_msgs) |
|
247 done |
|
248 |
|
249 lemma enrich_msgq_nodel: |
|
250 "no_del_event (enrich_msgq s q q') = no_del_event s" |
|
251 apply (induct s, simp) |
|
252 by (case_tac a, auto) |
|
253 |
|
254 lemma enrich_msgq_died_proc: |
|
255 "died (O_proc p) (enrich_msgq s q q') = died (O_proc p) s" |
|
256 apply (induct s, simp) |
|
257 by (case_tac a, auto) |
|
258 |
|
259 lemma cf2sfile_execve: |
|
260 "\<lbrakk>ff \<in> current_files (Execve p f fds # s); valid (Execve p f fds # s)\<rbrakk> |
|
261 \<Longrightarrow> cf2sfile (Execve p f fds # s) ff= cf2sfile s ff" |
|
262 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
263 lemma cf2sfile_clone: |
|
264 "\<lbrakk>ff \<in> current_files (Clone p p' fds # s); valid (Clone p p' fds # s)\<rbrakk> |
|
265 \<Longrightarrow> cf2sfile (Clone p p' fds # s) ff= cf2sfile s ff" |
|
266 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
267 lemma cf2sfile_ptrace: |
|
268 "\<lbrakk>ff \<in> current_files (Ptrace p p' # s); valid (Ptrace p p' # s)\<rbrakk> |
|
269 \<Longrightarrow> cf2sfile (Ptrace p p' # s) ff= cf2sfile s ff" |
|
270 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
271 lemma cf2sfile_readfile: |
|
272 "\<lbrakk>ff \<in> current_files (ReadFile p fd # s); valid (ReadFile p fd # s)\<rbrakk> |
|
273 \<Longrightarrow> cf2sfile (ReadFile p fd # s) ff= cf2sfile s ff" |
|
274 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
275 lemma cf2sfile_writefile: |
|
276 "\<lbrakk>ff \<in> current_files (WriteFile p fd # s); valid (WriteFile p fd # s)\<rbrakk> |
|
277 \<Longrightarrow> cf2sfile (WriteFile p fd # s) ff= cf2sfile s ff" |
|
278 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
279 lemma cf2sfile_truncate: |
|
280 "\<lbrakk>ff \<in> current_files (Truncate p f len # s); valid (Truncate p f len # s)\<rbrakk> |
|
281 \<Longrightarrow> cf2sfile (Truncate p f len # s) ff= cf2sfile s ff" |
|
282 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
283 lemma cf2sfile_createmsgq: |
|
284 "\<lbrakk>ff \<in> current_files (CreateMsgq p q # s); valid (CreateMsgq p q # s)\<rbrakk> |
|
285 \<Longrightarrow> cf2sfile (CreateMsgq p q # s) ff= cf2sfile s ff" |
|
286 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
287 lemma cf2sfile_sendmsg: |
|
288 "\<lbrakk>ff \<in> current_files (SendMsg p q m # s); valid (SendMsg p q m # s)\<rbrakk> |
|
289 \<Longrightarrow> cf2sfile (SendMsg p q m # s) ff = cf2sfile s ff" |
|
290 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
291 lemma cf2sfile_recvmsg: |
|
292 "\<lbrakk>ff \<in> current_files (RecvMsg p q m # s); valid (RecvMsg p q m # s)\<rbrakk> |
|
293 \<Longrightarrow> cf2sfile (RecvMsg p q m # s) ff = cf2sfile s ff" |
|
294 by (auto dest:cf2sfile_other' simp:current_files_simps) |
|
295 lemmas cf2sfile_other'' = cf2sfile_recvmsg cf2sfile_sendmsg cf2sfile_createmsgq cf2sfile_truncate |
|
296 cf2sfile_writefile cf2sfile_readfile cf2sfile_ptrace cf2sfile_clone cf2sfile_execve |
|
297 |
|
298 lemma enrich_msgq_prop: |
|
299 "\<lbrakk>valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> |
|
300 \<Longrightarrow> valid (enrich_msgq s q q') \<and> |
|
301 (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and> |
|
302 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and> |
|
303 (\<forall> tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and> |
|
304 (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and> |
|
305 (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q) \<and> |
|
306 (tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}))" |
|
307 proof (induct s) |
|
308 case Nil |
|
309 thus ?case by (auto) |
|
310 next |
|
311 case (Cons e s) |
|
312 hence vd_cons': "valid (e # s)" and curq_cons: "q \<in> current_msgqs (e # s)" |
|
313 and curq'_cons: "q' \<notin> current_msgqs (e # s)" and nodel_cons: "no_del_event (e # s)" |
|
314 and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
|
315 by (auto dest:vd_cons vt_grant_os vt_grant) |
|
316 from curq'_cons nodel_cons have curq': "q' \<notin> current_msgqs s" by (case_tac e, auto) |
|
317 from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto) |
|
318 from nodel curq' vd Cons |
|
319 have pre: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q') \<and> |
|
320 (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and> |
|
321 (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and> |
|
322 (\<forall>tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and> |
|
323 (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and> |
|
324 (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q) \<and> |
|
325 (tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}))" |
|
326 by auto |
|
327 |
|
328 from pre have pre_vd: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q')" by simp |
|
329 from pre have pre_sp: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk> |
|
330 \<Longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp" by auto |
|
331 from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; q \<in> current_msgqs s\<rbrakk> |
|
332 \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" by auto |
|
333 from pre have pre_sq: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> |
|
334 \<Longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq" by auto |
|
335 from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; q \<in> current_msgqs s\<rbrakk> |
|
336 \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by auto |
|
337 hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; q \<in> current_msgqs s\<rbrakk> |
|
338 \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def) |
|
339 from pre have pre_duq: "q \<in> current_msgqs s \<Longrightarrow> cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q" |
|
340 by auto |
|
341 have vd_enrich:"q \<in> current_msgqs s \<Longrightarrow> valid (e # enrich_msgq s q q')" |
|
342 apply (frule pre_vd) |
|
343 apply (erule_tac s = s and obj' = "E_msgq q'" in enrich_valid_intro_cons) |
|
344 apply (simp_all add:pre nodel nodel_cons curq_cons vd_cons' vd enrich_msgq_hungs) |
|
345 apply (clarsimp simp:nodel vd curq' enrich_msgq_alive) |
|
346 apply (rule allI, rule impI, erule enrich_msgq_not_alive) |
|
347 apply (simp_all add:curq' curq'_cons nodel vd enrich_msgq_cur_msgs enrich_msgq_filefd enrich_msgq_flagfd) |
|
348 done |
|
349 |
|
350 have q_neq_q': "q' \<noteq> q" using curq'_cons curq_cons by auto |
|
351 |
|
352 have vd_enrich_cons: "valid (enrich_msgq (e # s) q q')" |
|
353 proof- |
|
354 have "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> valid (enrich_msgq (e # s) q q')" |
|
355 proof- |
|
356 fix p q'' assume ev: "e = CreateMsgq p q''" |
|
357 show "valid (enrich_msgq (e # s) q q')" |
|
358 proof (cases "q'' = q") |
|
359 case False with ev vd_enrich curq_cons |
|
360 show ?thesis by simp |
|
361 next |
|
362 case True |
|
363 have "os_grant (CreateMsgq p q # s) (CreateMsgq p q')" |
|
364 using os ev |
|
365 by (simp add:q_neq_q' curq') |
|
366 moreover have "grant (CreateMsgq p q # s) (CreateMsgq p q')" |
|
367 using grant ev |
|
368 by (auto simp add:sectxt_of_obj_def split:option.splits) |
|
369 ultimately |
|
370 show ?thesis using ev vd_cons' True |
|
371 by (auto intro: valid.intros(2)) |
|
372 qed |
|
373 qed |
|
374 moreover have "\<And> p q'' m. \<lbrakk>e = SendMsg p q'' m; q \<in> current_msgqs s\<rbrakk> |
|
375 \<Longrightarrow> valid (enrich_msgq (e # s) q q')" |
|
376 proof- |
|
377 fix p q'' m assume ev: "e = SendMsg p q'' m" and q_in: "q \<in> current_msgqs s" |
|
378 show "valid (enrich_msgq (e # s) q q')" |
|
379 proof (cases "q'' = q") |
|
380 case False with ev vd_enrich q_in |
|
381 show ?thesis by simp |
|
382 next |
|
383 case True |
|
384 from grant os ev True obtain psec qsec |
|
385 where psec: "sectxt_of_obj s (O_proc p) = Some psec" |
|
386 and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec" |
|
387 by (auto split:option.splits) |
|
388 from psec q_in os ev |
|
389 have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec" |
|
390 by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits) |
|
391 from qsec q_in pre_duq vd |
|
392 have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec" |
|
393 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') |
|
394 show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd |
|
395 curq' psec psec' qsec qsec' grant os q_neq_q' |
|
396 apply (simp, erule_tac valid.intros(2)) |
|
397 apply (auto simp:q_neq_q' enrich_msgq_cur_msgqs enrich_msgq_cur_procs |
|
398 enrich_msgq_cur_msgs sectxt_of_obj_simps) |
|
399 done |
|
400 qed |
|
401 qed |
|
402 moreover have "\<And> p q'' m. \<lbrakk>e = RecvMsg p q'' m; q \<in> current_msgqs s\<rbrakk> |
|
403 \<Longrightarrow> valid (enrich_msgq (e # s) q q')" |
|
404 proof- |
|
405 fix p q'' m assume ev: "e = RecvMsg p q'' m" and q_in: "q \<in> current_msgqs s" |
|
406 show "valid (enrich_msgq (e # s) q q')" |
|
407 proof (cases "q'' = q") |
|
408 case False with ev vd_enrich q_in |
|
409 show ?thesis by simp |
|
410 next |
|
411 case True |
|
412 from grant os ev True obtain psec qsec msec |
|
413 where psec: "sectxt_of_obj s (O_proc p) = Some psec" |
|
414 and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec" |
|
415 and msec: "sectxt_of_obj s (O_msg q (hd (msgs_of_queue s q))) = Some msec" |
|
416 by (auto split:option.splits) |
|
417 from psec q_in os ev |
|
418 have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec" |
|
419 by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits) |
|
420 from qsec q_in pre_duq vd |
|
421 have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec" |
|
422 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') |
|
423 from qsec q_in vd |
|
424 have qsec'': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q) = Some qsec" |
|
425 apply (frule_tac pre_sq, simp_all) |
|
426 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') |
|
427 from msec q_in pre_duq vd qsec qsec' qsec'' curq' nodel |
|
428 have msec': "sectxt_of_obj (enrich_msgq s q q') (O_msg q' (hd (msgs_of_queue s q))) = Some msec" |
|
429 apply (auto simp:cq2smsgq_def enrich_msgq_cur_msgs |
|
430 split:option.splits dest!:current_has_sms') |
|
431 apply (case_tac "msgs_of_queue s q") |
|
432 using os ev True apply simp |
|
433 apply (simp add:cqm2sms.simps split:option.splits) |
|
434 apply (auto simp:cm2smsg_def split:option.splits) |
|
435 done |
|
436 show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd |
|
437 curq' grant os q_neq_q' psec psec' msec msec' qsec qsec' |
|
438 apply (simp, erule_tac valid.intros(2)) |
|
439 apply (auto simp:enrich_msgq_cur_msgqs enrich_msgq_cur_procs |
|
440 enrich_msgq_cur_msgs sectxt_of_obj_simps) |
|
441 done |
|
442 qed |
|
443 qed |
|
444 ultimately |
|
445 show ?thesis using vd_enrich curq_cons vd_cons' |
|
446 apply (case_tac e) |
|
447 apply (auto simp del:enrich_msgq.simps) |
|
448 apply (auto split:if_splits ) |
|
449 done |
|
450 qed |
|
451 |
|
452 have curpsec: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> |
|
453 sectxt_of_obj (enrich_msgq s q q') (O_proc tp) = sectxt_of_obj s (O_proc tp)" |
|
454 using pre_vd vd |
|
455 apply (frule_tac pre_sp, simp) |
|
456 by (auto simp:cp2sproc_def split:option.splits if_splits dest!:current_has_sec') |
|
457 have curfsec: "\<And> f. \<lbrakk>is_file s f; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> |
|
458 sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)" |
|
459 proof- |
|
460 fix f |
|
461 assume a1: "is_file s f" and a2: "q \<in> current_msgqs s" |
|
462 from a2 pre_sf pre_vd |
|
463 have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" |
|
464 and vd_enrich: "valid (enrich_msgq s q q')" |
|
465 by auto |
|
466 hence csf: "cf2sfile (enrich_msgq s q q') f = cf2sfile s f" |
|
467 using a1 by (auto simp:is_file_in_current) |
|
468 from a1 obtain sf where csf_some: "cf2sfile s f = Some sf" |
|
469 apply (case_tac "cf2sfile s f") |
|
470 apply (drule current_file_has_sfile') |
|
471 apply (simp add:vd, simp add:is_file_in_current, simp) |
|
472 done |
|
473 from a1 have a1': "is_file (enrich_msgq s q q') f" |
|
474 using vd nodel by (simp add:enrich_msgq_is_file) |
|
475 show "sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)" |
|
476 using csf csf_some vd_enrich vd a1 a1' |
|
477 apply (auto simp:cf2sfile_def split:option.splits if_splits) |
|
478 apply (case_tac f, simp_all) |
|
479 apply (drule root_is_dir', simp+) |
|
480 done |
|
481 qed |
|
482 have curdsec: "\<And> tf. \<lbrakk>is_dir s tf; q \<in> current_msgqs s\<rbrakk> |
|
483 \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)" |
|
484 proof- |
|
485 fix tf |
|
486 assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s" |
|
487 from a2 pre_sf pre_vd |
|
488 have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" |
|
489 and vd_enrich: "valid (enrich_msgq s q q')" |
|
490 by auto |
|
491 hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf" |
|
492 using a1 by (auto simp:is_dir_in_current) |
|
493 from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf" |
|
494 apply (case_tac "cf2sfile s tf") |
|
495 apply (drule current_file_has_sfile') |
|
496 apply (simp add:vd, simp add:is_dir_in_current, simp) |
|
497 done |
|
498 from a1 have a1': "is_dir (enrich_msgq s q q') tf" |
|
499 using enrich_msgq_is_dir vd nodel by simp |
|
500 from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file) |
|
501 from a1' vd have a3': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) |
|
502 show "sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)" |
|
503 using csf csf_some a3 a3' vd_enrich vd |
|
504 apply (auto simp:cf2sfile_def split:option.splits) |
|
505 apply (case_tac tf) |
|
506 apply (simp add:root_sec_remains, simp) |
|
507 done |
|
508 qed |
|
509 have curpsecs: "\<And> tf ctxts'. \<lbrakk>is_dir s tf; q \<in> current_msgqs s; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk> |
|
510 \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'" |
|
511 proof- |
|
512 fix tf ctxts' |
|
513 assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s" |
|
514 and a4: "get_parentfs_ctxts s tf = Some ctxts'" |
|
515 from a2 pre |
|
516 have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" |
|
517 and vd_enrich': "valid (enrich_msgq s q q')" |
|
518 by auto |
|
519 hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf" |
|
520 using a1 by (auto simp:is_dir_in_current) |
|
521 from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf" |
|
522 apply (case_tac "cf2sfile s tf") |
|
523 apply (drule current_file_has_sfile') |
|
524 apply (simp add:vd, simp add:is_dir_in_current, simp) |
|
525 done |
|
526 from a1 have a1': "is_dir (enrich_msgq s q q') tf" |
|
527 using enrich_msgq_is_dir vd nodel by simp |
|
528 from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file) |
|
529 from a1' vd have a5': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) |
|
530 |
|
531 from a1' pre_vd a2 obtain ctxts |
|
532 where a3: "get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts" |
|
533 apply (case_tac "get_parentfs_ctxts (enrich_msgq s q q') tf") |
|
534 apply (drule get_pfs_secs_prop', simp+) |
|
535 done |
|
536 moreover have "set ctxts = set ctxts'" |
|
537 proof (cases tf) |
|
538 case Nil |
|
539 with a3 a4 vd vd_enrich' |
|
540 show ?thesis |
|
541 by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits) |
|
542 next |
|
543 case (Cons a ff) |
|
544 with csf csf_some a5 a5' vd_enrich' vd a3 a4 |
|
545 show ?thesis |
|
546 apply (auto simp:cf2sfile_def split:option.splits if_splits) |
|
547 done |
|
548 qed |
|
549 ultimately |
|
550 show "\<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'" |
|
551 by auto |
|
552 qed |
|
553 |
|
554 have psec_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> |
|
555 sectxt_of_obj (enrich_msgq (e # s) q q') (O_proc tp) = sectxt_of_obj (e # s) (O_proc tp)" |
|
556 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd |
|
557 apply (case_tac e) |
|
558 apply (auto intro:curpsec simp:sectxt_of_obj_simps) |
|
559 apply (frule curpsec, simp, frule curfsec, simp) |
|
560 apply (auto split:option.splits)[1] |
|
561 apply (frule vd_cons) defer apply (frule vd_cons) |
|
562 apply (auto intro:curpsec simp:sectxt_of_obj_simps) |
|
563 done |
|
564 |
|
565 |
|
566 have sf_cons: "\<And> f. f \<in> current_files (e # s) \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
567 proof- |
|
568 fix f |
|
569 assume a1: "f \<in> current_files (e # s)" |
|
570 hence a1': "f \<in> current_files (enrich_msgq (e # s) q q')" |
|
571 using nodel_cons os vd vd_cons' vd_enrich_cons |
|
572 apply (case_tac e) |
|
573 apply (auto simp:current_files_simps enrich_msgq_cur_files dest:is_file_in_current split:option.splits) |
|
574 done |
|
575 have b1: "\<And> p f' flags fd opt. e = Open p f' flags fd opt \<Longrightarrow> |
|
576 cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
577 proof- |
|
578 fix p f' flags fd opt |
|
579 assume ev: "e = Open p f' flags fd opt" |
|
580 show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
581 proof (cases opt) |
|
582 case None |
|
583 with a1 a1' ev vd_cons' vd_enrich_cons curq_cons |
|
584 show ?thesis |
|
585 apply (simp add:cf2sfile_open_none) |
|
586 apply (simp add:pre_sf current_files_simps) |
|
587 done |
|
588 next |
|
589 case (Some inum) |
|
590 show ?thesis |
|
591 proof (cases "f = f'") |
|
592 case False |
|
593 with a1 a1' ev vd_cons' vd_enrich_cons curq_cons Some |
|
594 show ?thesis |
|
595 apply (simp add:cf2sfile_open) |
|
596 apply (simp add:pre_sf current_files_simps) |
|
597 done |
|
598 next |
|
599 case True |
|
600 with vd_cons' ev os Some |
|
601 obtain pf where pf: "parent f = Some pf" by auto |
|
602 then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" |
|
603 using os vd ev Some True |
|
604 apply (case_tac "get_parentfs_ctxts s pf") |
|
605 apply (drule get_pfs_secs_prop', simp, simp) |
|
606 apply auto |
|
607 done |
|
608 |
|
609 have "sectxt_of_obj (Open p f' flags fd (Some inum) # enrich_msgq s q q') (O_file f') = |
|
610 sectxt_of_obj (Open p f' flags fd (Some inum) # s) (O_file f')" |
|
611 using Some vd_enrich_cons vd_cons' ev pf True os curq_cons |
|
612 by (simp add:sectxt_of_obj_simps curpsec curdsec) |
|
613 moreover |
|
614 have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" |
|
615 using curq_cons ev pf Some True os |
|
616 by (simp add:curdsec) |
|
617 moreover |
|
618 have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts" |
|
619 using curq_cons ev pf Some True os vd psecs |
|
620 apply (case_tac "get_parentfs_ctxts s pf") |
|
621 apply (drule get_pfs_secs_prop', simp+) |
|
622 apply (rule curpsecs, simp+) |
|
623 done |
|
624 then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" |
|
625 and psecs_eq: "set ctxts' = set ctxts" by auto |
|
626 ultimately show ?thesis |
|
627 using a1 a1' ev vd_cons' vd_enrich_cons Some True pf psecs |
|
628 by (simp add:cf2sfile_open split:option.splits) |
|
629 qed |
|
630 qed |
|
631 qed |
|
632 have b2: "\<And> p f' inum. e = Mkdir p f' inum \<Longrightarrow> |
|
633 cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
634 proof- |
|
635 fix p f' inum |
|
636 assume ev: "e = Mkdir p f' inum" |
|
637 show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
638 proof (cases "f' = f") |
|
639 case False |
|
640 with a1 a1' ev vd_cons' vd_enrich_cons curq_cons |
|
641 show ?thesis |
|
642 apply (simp add:cf2sfile_mkdir) |
|
643 apply (simp add:pre_sf current_files_simps) |
|
644 done |
|
645 next |
|
646 case True |
|
647 with vd_cons' ev os |
|
648 obtain pf where pf: "parent f = Some pf" by auto |
|
649 then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" |
|
650 using os vd ev True |
|
651 apply (case_tac "get_parentfs_ctxts s pf") |
|
652 apply (drule get_pfs_secs_prop', simp, simp) |
|
653 apply auto |
|
654 done |
|
655 |
|
656 have "sectxt_of_obj (Mkdir p f' inum # enrich_msgq s q q') (O_dir f') = |
|
657 sectxt_of_obj (Mkdir p f' inum # s) (O_dir f')" |
|
658 using vd_enrich_cons vd_cons' ev pf True os curq_cons |
|
659 by (simp add:sectxt_of_obj_simps curpsec curdsec) |
|
660 moreover |
|
661 have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" |
|
662 using curq_cons ev pf True os |
|
663 by (simp add:curdsec) |
|
664 moreover |
|
665 have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts" |
|
666 using curq_cons ev pf True os vd psecs |
|
667 apply (case_tac "get_parentfs_ctxts s pf") |
|
668 apply (drule get_pfs_secs_prop', simp+) |
|
669 apply (rule curpsecs, simp+) |
|
670 done |
|
671 then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" |
|
672 and psecs_eq: "set ctxts' = set ctxts" by auto |
|
673 ultimately show ?thesis |
|
674 using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs |
|
675 apply (simp add:cf2sfile_mkdir split:option.splits) |
|
676 done |
|
677 qed |
|
678 qed |
|
679 have b3: "\<And> p f' f''. e = LinkHard p f' f'' \<Longrightarrow> |
|
680 cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
681 proof- |
|
682 fix p f' f'' |
|
683 assume ev: "e = LinkHard p f' f''" |
|
684 show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
685 proof (cases "f'' = f") |
|
686 case False |
|
687 with a1 a1' ev vd_cons' vd_enrich_cons curq_cons |
|
688 show ?thesis |
|
689 apply (simp add:cf2sfile_linkhard) |
|
690 apply (simp add:pre_sf current_files_simps) |
|
691 done |
|
692 next |
|
693 case True |
|
694 with vd_cons' ev os |
|
695 obtain pf where pf: "parent f = Some pf" by auto |
|
696 then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" |
|
697 using os vd ev True |
|
698 apply (case_tac "get_parentfs_ctxts s pf") |
|
699 apply (drule get_pfs_secs_prop', simp, simp) |
|
700 apply auto |
|
701 done |
|
702 |
|
703 have "sectxt_of_obj (LinkHard p f' f'' # enrich_msgq s q q') (O_file f) = |
|
704 sectxt_of_obj (LinkHard p f' f'' # s) (O_file f)" |
|
705 using vd_enrich_cons vd_cons' ev pf True os curq_cons |
|
706 by (simp add:sectxt_of_obj_simps curpsec curdsec) |
|
707 moreover |
|
708 have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" |
|
709 using curq_cons ev pf True os |
|
710 by (simp add:curdsec) |
|
711 moreover |
|
712 have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts" |
|
713 using curq_cons ev pf True os vd psecs |
|
714 apply (case_tac "get_parentfs_ctxts s pf") |
|
715 apply (drule get_pfs_secs_prop', simp+) |
|
716 apply (rule curpsecs, simp+) |
|
717 done |
|
718 then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" |
|
719 and psecs_eq: "set ctxts' = set ctxts" by auto |
|
720 ultimately show ?thesis |
|
721 using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs |
|
722 apply (simp add:cf2sfile_linkhard split:option.splits) |
|
723 done |
|
724 qed |
|
725 qed |
|
726 show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" |
|
727 apply (case_tac e) |
|
728 prefer 6 apply (erule b1) |
|
729 prefer 11 apply (erule b2) |
|
730 prefer 11 apply (erule b3) |
|
731 apply (simp_all only:b1 b2 b3) |
|
732 using a1' a1 vd_enrich_cons vd_cons' curq_cons nodel_cons |
|
733 apply (simp_all add:cf2sfile_other'' cf2sfile_simps enrich_msgq.simps no_del_event.simps split:if_splits) |
|
734 apply (simp_all add:pre_sf cf2sfile_other' current_files_simps split:if_splits) |
|
735 apply (drule vd_cons, simp add:cf2sfile_other', drule pre_sf, simp+)+ |
|
736 done |
|
737 qed |
|
738 |
|
739 have sfd_cons:"\<And> tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<Longrightarrow> |
|
740 cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" |
|
741 proof- |
|
742 fix tp fd f |
|
743 assume a1: "file_of_proc_fd (e # s) tp fd = Some f" |
|
744 hence a1': "file_of_proc_fd (enrich_msgq (e # s) q q') tp fd = Some f" |
|
745 using nodel_cons vd_enrich os vd_cons' |
|
746 apply (case_tac e, auto simp:enrich_msgq_filefd simp del:enrich_msgq.simps) |
|
747 done |
|
748 have b1: "\<And> p f' flags fd' opt. e = Open p f' flags fd' opt \<Longrightarrow> |
|
749 cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" |
|
750 proof- |
|
751 fix p f' flags fd' opt |
|
752 assume ev: "e = Open p f' flags fd' opt" |
|
753 have c1': "file_of_proc_fd (Open p f' flags fd' opt # s) tp fd = Some f" |
|
754 using a1' ev a1 by (simp split:if_splits) |
|
755 show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" thm cfd2sfd_open |
|
756 proof (cases "tp = p \<and> fd = fd'") |
|
757 case False |
|
758 show ?thesis using ev vd_enrich_cons vd_cons' a1' a1 False curq_cons |
|
759 apply (simp add:cfd2sfd_open split:if_splits del:file_of_proc_fd.simps) |
|
760 apply (rule conjI, rule impI, simp) |
|
761 apply (rule conjI, rule impI, simp) |
|
762 apply (auto simp: False intro!:pre_sfd' split:if_splits) |
|
763 done |
|
764 next |
|
765 case True |
|
766 have "f' \<in> current_files (Open p f' flags fd' opt # s)" using ev vd_cons' os |
|
767 by (auto simp:current_files_simps is_file_in_current split:option.splits) |
|
768 hence "cf2sfile (Open p f' flags fd' opt # enrich_msgq s q q') f' |
|
769 = cf2sfile (Open p f' flags fd' opt # s) f'" |
|
770 using sf_cons ev by auto |
|
771 moreover have "sectxt_of_obj (enrich_msgq s q q') (O_proc p) = sectxt_of_obj s (O_proc p)" |
|
772 apply (rule curpsec) |
|
773 using os ev curq_cons |
|
774 by (auto split:option.splits) |
|
775 ultimately show ?thesis |
|
776 using ev True a1 a1' vd_enrich_cons vd_cons' |
|
777 apply (simp add:cfd2sfd_open sectxt_of_obj_simps del:file_of_proc_fd.simps) |
|
778 done |
|
779 qed |
|
780 qed |
|
781 show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" |
|
782 apply (case_tac e) |
|
783 prefer 6 apply (erule b1) |
|
784 using a1' a1 vd_enrich_cons vd_cons' curq_cons |
|
785 apply (simp_all only:cfd2sfd_simps enrich_msgq.simps) |
|
786 apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits) |
|
787 done |
|
788 qed |
|
789 |
|
790 have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> |
|
791 cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp" |
|
792 apply (auto simp add:cpfd2sfds_def proc_file_fds_def) |
|
793 apply (rule_tac x = fd in exI, rule conjI, rule_tac x = f in exI) |
|
794 prefer 3 |
|
795 apply (rule_tac x = fd in exI, rule conjI, rule_tac x = f in exI) |
|
796 apply (auto simp:sfd_cons enrich_msgq_filefd nodel_cons vd_cons') |
|
797 done |
|
798 |
|
799 have tainted_cons: "tainted (enrich_msgq (e # s) q q') = |
|
800 (tainted (e # s) \<union> {O_msg q' m | m. O_msg q m \<in> tainted (e # s)})" |
|
801 apply (rule equalityI) |
|
802 using nodel_cons curq_cons curq'_cons vd_cons' vd_enrich_cons |
|
803 apply (rule enrich_msgq_tainted_aux2) |
|
804 using nodel_cons curq_cons curq'_cons vd_cons' |
|
805 apply (rule enrich_msgq_tainted_aux1) |
|
806 done |
|
807 have pre_tainted: "q \<in> current_msgqs s \<Longrightarrow> tainted (enrich_msgq s q q') = |
|
808 (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})" by (simp add:pre) |
|
809 |
|
810 have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" |
|
811 by (auto simp:proc_file_fds_def elim!:sfd_cons) |
|
812 moreover |
|
813 have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp" |
|
814 by (auto simp:cp2sproc_def pfds_cons psec_cons enrich_msgq_died_proc split:option.splits) |
|
815 moreover |
|
816 have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" |
|
817 proof clarify |
|
818 fix tq assume a1: "tq \<in> current_msgqs (e # s)" |
|
819 |
|
820 have curqsec: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> |
|
821 sectxt_of_obj (enrich_msgq s q q') (O_msgq tq) = sectxt_of_obj s (O_msgq tq)" |
|
822 using pre_vd vd |
|
823 apply (frule_tac pre_sq, simp) |
|
824 by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') |
|
825 have cursms: "\<And> q''. \<lbrakk>q'' \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> |
|
826 cqm2sms (enrich_msgq s q q') q'' (msgs_of_queue (enrich_msgq s q q') q'') = |
|
827 cqm2sms s q'' (msgs_of_queue s q'')" |
|
828 using pre_vd vd |
|
829 apply (frule_tac pre_sq, simp) |
|
830 by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') |
|
831 have qsec_cons: "sectxt_of_obj (enrich_msgq (e # s) q q') (O_msgq tq) = sectxt_of_obj (e # s) (O_msgq tq)" |
|
832 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons curq_cons a1 |
|
833 apply (case_tac e) |
|
834 apply (auto intro:curqsec simp:sectxt_of_obj_simps curpsec split:option.splits dest!:current_has_sec') |
|
835 apply (frule vd_cons) defer apply (frule vd_cons) |
|
836 apply (auto intro:curqsec simp:sectxt_of_obj_simps) |
|
837 done |
|
838 have sms_cons: "cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = |
|
839 cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" |
|
840 proof- |
|
841 have b1: "\<And> p q'' m. e = SendMsg p q'' m \<Longrightarrow> |
|
842 cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = |
|
843 cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" |
|
844 apply (case_tac e) |
|
845 using a1 curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons |
|
846 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms pre_tainted |
|
847 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
848 apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*}) |
|
849 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms pre_tainted |
|
850 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
851 done |
|
852 have b2: "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> |
|
853 cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = |
|
854 cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" |
|
855 using a1 curq_cons curq'_cons vd_enrich_cons vd_cons' |
|
856 apply (auto simp:cqm2sms_simps intro:cursms) |
|
857 apply (auto simp:cqm2sms.simps) |
|
858 done |
|
859 have b3: "\<And> p q'' m. e = RecvMsg p q'' m \<Longrightarrow> |
|
860 cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = |
|
861 cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" |
|
862 using a1 curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons |
|
863 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms |
|
864 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
865 apply (frule vd_cons) defer apply (frule vd_cons) |
|
866 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms |
|
867 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
868 done |
|
869 show "cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) = |
|
870 cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)" |
|
871 apply (case_tac e) |
|
872 prefer 15 apply (erule b2) |
|
873 prefer 15 apply (erule b1) |
|
874 prefer 15 apply (erule b3) |
|
875 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons a1 |
|
876 apply (auto intro:cursms simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec |
|
877 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
878 done |
|
879 qed |
|
880 |
|
881 show "cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" |
|
882 using a1 curq_cons |
|
883 apply (simp add:cq2smsgq_def qsec_cons sms_cons) |
|
884 done |
|
885 qed |
|
886 moreover |
|
887 have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q" |
|
888 proof- |
|
889 have duqsec: "q \<in> current_msgqs s \<Longrightarrow> |
|
890 sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = sectxt_of_obj s (O_msgq q)" |
|
891 apply (frule pre_duq) using vd |
|
892 by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') |
|
893 have duqsms: "q \<in> current_msgqs s \<Longrightarrow> |
|
894 cqm2sms (enrich_msgq s q q') q' (msgs_of_queue (enrich_msgq s q q') q') = |
|
895 cqm2sms s q (msgs_of_queue s q)" |
|
896 apply (frule pre_duq) using vd |
|
897 by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms') |
|
898 have qsec_cons: "sectxt_of_obj (enrich_msgq (e # s) q q') (O_msgq q') = sectxt_of_obj (e # s) (O_msgq q)" |
|
899 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons curq_cons |
|
900 apply (case_tac e) |
|
901 apply (auto simp:duqsec sectxt_of_obj_simps curpsec split:option.splits dest!:current_has_sec') |
|
902 apply (frule vd_cons) defer apply (frule vd_cons) |
|
903 apply (auto intro:duqsec simp:sectxt_of_obj_simps) |
|
904 done |
|
905 have sms_cons: "cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = |
|
906 cqm2sms (e # s) q (msgs_of_queue (e # s) q)" |
|
907 proof- |
|
908 have b1: "\<And> p q'' m. e = SendMsg p q'' m \<Longrightarrow> |
|
909 cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = |
|
910 cqm2sms (e # s) q (msgs_of_queue (e # s) q)" |
|
911 apply (case_tac e) |
|
912 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons |
|
913 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted |
|
914 enrich_msgq_cur_procs enrich_msgq_cur_msgqs |
|
915 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
916 apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*}) |
|
917 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted |
|
918 enrich_msgq_cur_procs enrich_msgq_cur_msgqs dest:tainted_in_current |
|
919 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
920 done |
|
921 have b2: "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> |
|
922 cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = |
|
923 cqm2sms (e # s) q (msgs_of_queue (e # s) q)" |
|
924 using curq_cons curq'_cons vd_enrich_cons vd_cons' |
|
925 apply (auto simp:cqm2sms_simps intro:duqsms) |
|
926 apply (auto simp:cqm2sms.simps) |
|
927 done |
|
928 have b3: "\<And> p q'' m. e = RecvMsg p q'' m \<Longrightarrow> |
|
929 cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') = |
|
930 cqm2sms (e # s) q (msgs_of_queue (e # s) q)" |
|
931 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons |
|
932 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted |
|
933 enrich_msgq_cur_procs enrich_msgq_cur_msgqs |
|
934 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
935 apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*}) |
|
936 apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted |
|
937 enrich_msgq_cur_procs enrich_msgq_cur_msgqs dest:tainted_in_current |
|
938 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
939 done |
|
940 show ?thesis |
|
941 apply (case_tac e) |
|
942 prefer 15 apply (erule b2) |
|
943 prefer 15 apply (erule b1) |
|
944 prefer 15 apply (erule b3) |
|
945 using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons |
|
946 apply (auto intro:duqsms simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsms |
|
947 split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps) |
|
948 done |
|
949 qed |
|
950 show ?thesis |
|
951 using curq_cons |
|
952 apply (simp add:cq2smsgq_def qsec_cons sms_cons) |
|
953 done |
|
954 qed |
|
955 ultimately show ?case using vd_enrich_cons sf_cons tainted_cons |
|
956 by auto |
|
957 qed |
|
958 |
|
959 fun enrich_file_link :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_state)" |
|
960 where |
|
961 "enrich_file_link [] tf df = []" |
|
962 |
|
963 fun enrich_file_set :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> t_state" |
|
964 where |
|
965 "enrich_file_set [] tf df = []" |
|
966 | "enrich_file_set [] (Open p f flags fd (Some inum) # s) = |
|
967 |
13 |
968 |
14 |
969 |
15 |
970 |
16 |
971 |
17 |