175 \<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P; |
175 \<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P; |
176 \<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk> |
176 \<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk> |
177 \<Longrightarrow> P" |
177 \<Longrightarrow> P" |
178 by (erule Info_flow_shm.cases, auto) |
178 by (erule Info_flow_shm.cases, auto) |
179 |
179 |
180 |
|
181 lemma Info_flow_shm_prop1: |
180 lemma Info_flow_shm_prop1: |
182 "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s" |
181 "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s" |
183 by (rule notI, drule Info_flow_shm.intros(1), simp) |
182 by (rule notI, drule Info_flow_shm.intros(1), simp) |
184 |
|
185 lemma Info_flow_shm_intro4: |
|
186 "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p" |
|
187 by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros) |
|
188 |
|
189 (********* simpset for inductive Info_flow_shm **********) |
|
190 |
|
191 lemma Info_flow_shm_attach1: |
|
192 "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> |
|
193 ((Info_flow_shm s pa pb) \<or> |
|
194 (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> |
|
195 (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or> |
|
196 (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> |
|
197 (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))" |
|
198 proof (induct rule:Info_flow_shm.induct) |
|
199 case (ifs_self proc \<tau>) |
|
200 show ?case |
|
201 proof (rule impI) |
|
202 assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s" |
|
203 hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os) |
|
204 hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros) |
|
205 from ifs_self pre have "proc \<in> current_procs s" by simp |
|
206 hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros) |
|
207 show "Info_flow_shm s proc proc \<or> |
|
208 (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and> |
|
209 (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or> |
|
210 (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> |
|
211 (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))" |
|
212 using p4 p3 by auto |
|
213 qed |
|
214 next |
|
215 case (ifs_flow \<tau> pa pb h' pc) |
|
216 thus ?case |
|
217 proof (rule_tac impI) |
|
218 assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> (\<tau> = Attach p h flag # s) \<longrightarrow> Info_flow_shm s pa pb \<or> |
|
219 \<not> Info_flow_shm s pa pb \<and> pa = p \<and> |
|
220 pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or> |
|
221 \<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')" |
|
222 and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s" |
|
223 from p2 and p4 have p2': "Info_flow_shm s pa pb \<or> |
|
224 (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> |
|
225 (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or> |
|
226 (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> |
|
227 (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))" |
|
228 by (erule_tac impE, simp) |
|
229 from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os) |
|
230 from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros) |
|
231 from p3 p4 have p8: "if (h' = h) |
|
232 then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or> |
|
233 (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or> |
|
234 (one_flow_shm s h pb pc) |
|
235 else one_flow_shm s h' pb pc " by (auto simp add:one_flow_shm_attach) |
|
236 |
|
237 have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp |
|
238 moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk> |
|
239 \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc" |
|
240 sorry |
|
241 moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk> |
|
242 \<Longrightarrow> Info_flow_shm s pa pc" |
|
243 sorry |
|
244 moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk> |
|
245 \<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'" |
|
246 sorry |
|
247 ultimately |
|
248 |
|
249 |
|
250 |
|
251 show "Info_flow_shm s pa pc \<or> |
|
252 (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> |
|
253 (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or> |
|
254 (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and> |
|
255 (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))" |
|
256 apply auto |
|
257 sorry |
|
258 qed |
|
259 qed |
|
260 |
183 |
261 lemma Info_flow_shm_intro3: |
184 lemma Info_flow_shm_intro3: |
262 "\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk> |
185 "\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk> |
263 \<Longrightarrow> Info_flow_shm s p to" |
186 \<Longrightarrow> Info_flow_shm s p to" |
264 apply (case_tac "from = to", simp) |
187 apply (case_tac "from = to", simp) |
265 apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def) |
188 apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def) |
266 by (rule_tac x = flag in exI, simp) |
189 by (rule_tac x = flag in exI, simp) |
267 |
190 |
268 lemma Info_flow_shm_attach1: |
191 lemma Info_flow_shm_intro4: |
|
192 "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p" |
|
193 by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros) |
|
194 |
|
195 (********* simpset for inductive Info_flow_shm **********) |
|
196 |
|
197 lemma Info_flow_shm_attach1_aux: |
269 "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> |
198 "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> |
270 (if Info_flow_shm s pa pb then True else |
199 (if Info_flow_shm s pa pb then True else |
271 (if (pa = p \<and> flag = SHM_RDWR) |
200 (if (pa = p \<and> flag = SHM_RDWR) |
272 then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) |
201 then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) |
273 else if (pb = p) |
202 else if (pb = p) |
350 (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)" |
279 (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)" |
351 using p7 by auto |
280 using p7 by auto |
352 qed |
281 qed |
353 qed |
282 qed |
354 |
283 |
355 |
284 lemma Info_flow_shm_attach1: |
356 |
285 "\<lbrakk>valid (Attach p h flag # s); Info_flow_shm (Attach p h flag # s) pa pb\<rbrakk> |
357 |
286 \<Longrightarrow> (if Info_flow_shm s pa pb then True else |
358 |
287 (if (pa = p \<and> flag = SHM_RDWR) |
359 |
288 then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) |
360 |
289 else if (pb = p) |
361 |
290 then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') |
362 |
291 else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> |
|
292 Info_flow_shm s p' pb) \<or> |
|
293 (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb) |
|
294 ) )" |
|
295 apply (drule_tac p = p and h = h and flag = flag in Info_flow_shm_attach1_aux) |
|
296 by auto |
|
297 |
|
298 lemma Info_flow_shm_attach_aux[rule_format]: |
|
299 "Info_flow_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> Info_flow_shm (Attach p h flag # s) pa pb" |
|
300 apply (erule Info_flow_shm.induct) |
|
301 apply (rule impI, rule Info_flow_shm.intros(1), simp) |
|
302 apply (rule impI, simp, rule_tac h = ha in Info_flow_shm.intros(2), simp) |
|
303 apply (auto simp add:one_flow_shm_simps) |
|
304 done |
|
305 |
|
306 lemma Info_flow_shm_attach2: |
|
307 "\<lbrakk>valid (Attach p h flag # s); if Info_flow_shm s pa pb then True else |
|
308 (if (pa = p \<and> flag = SHM_RDWR) |
|
309 then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) |
|
310 else if (pb = p) |
|
311 then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') |
|
312 else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> |
|
313 Info_flow_shm s p' pb) \<or> |
|
314 (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))\<rbrakk> |
|
315 \<Longrightarrow> Info_flow_shm (Attach p h flag # s) pa pb" |
|
316 apply (frule vt_grant_os, frule vd_cons) |
|
317 apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def intro:Info_flow_shm_attach_aux) |
|
318 apply (rule_tac p' = p' in Info_flow_trans) |
|
319 apply (rule_tac p' = p and h = h in Info_flow_shm.intros(2)) |
|
320 apply (rule Info_flow_shm.intros(1), simp) |
|
321 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def) |
|
322 apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp) |
|
323 apply (simp add:Info_flow_shm_attach_aux) |
|
324 |
|
325 apply (rule_tac p' = p' in Info_flow_trans) |
|
326 apply (rule_tac p' = p in Info_flow_trans) |
|
327 apply (simp add:Info_flow_shm_attach_aux) |
|
328 apply (rule_tac p' = p and h = h in Info_flow_shm.intros(2)) |
|
329 apply (rule Info_flow_shm.intros(1), simp) |
|
330 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def) |
|
331 apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp) |
|
332 apply (simp add:Info_flow_shm_attach_aux) |
|
333 |
|
334 apply (rule_tac p' = p in Info_flow_trans) |
|
335 apply (rule_tac p' = p' in Info_flow_trans) |
|
336 apply (simp add:Info_flow_shm_attach_aux) |
|
337 apply (rule_tac p' = p' and h = h in Info_flow_shm.intros(2)) |
|
338 apply (rule Info_flow_shm.intros(1), simp add:procs_of_shm_prop2) |
|
339 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def) |
|
340 apply (rule notI, simp) |
|
341 apply (simp add:Info_flow_shm_attach_aux) |
|
342 |
|
343 apply (rule_tac p' = p in Info_flow_trans) |
|
344 apply (rule_tac p' = p' in Info_flow_trans) |
|
345 apply (simp add:Info_flow_shm_attach_aux) |
|
346 apply (rule_tac p' = p' and h = h in Info_flow_shm.intros(2)) |
|
347 apply (rule Info_flow_shm.intros(1), simp add:procs_of_shm_prop2) |
|
348 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def) |
|
349 apply (rule notI, simp) |
|
350 apply (simp add:Info_flow_shm_attach_aux) |
|
351 done |
363 |
352 |
364 lemma Info_flow_shm_attach: |
353 lemma Info_flow_shm_attach: |
365 "valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. |
354 "valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. |
366 (Info_flow_shm s pa pb) \<or> |
355 Info_flow_shm s pa pb \<or> |
367 (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or> |
356 (if (pa = p \<and> flag = SHM_RDWR) |
368 (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )" |
357 then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) |
|
358 else if (pb = p) |
|
359 then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') |
|
360 else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> |
|
361 Info_flow_shm s p' pb) \<or> |
|
362 (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb) |
|
363 ) )" |
369 apply (rule ext, rule ext, rule iffI) |
364 apply (rule ext, rule ext, rule iffI) |
370 apply (case_tac "Info_flow_shm s pa pb", simp) |
365 apply (drule_tac pa = pa and pb = pb in Info_flow_shm_attach1, simp) |
371 apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp) |
366 apply (auto split:if_splits)[1] |
372 |
367 apply (drule_tac pa = pa and pb = pb in Info_flow_shm_attach2) |
373 apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp) |
368 apply (auto split:if_splits) |
374 apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp) |
369 done |
375 |
370 |
376 |
|
377 |
|
378 apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp) |
|
379 apply (simp) |
|
380 apply (simp, erule Info_flow_shm_cases', simp, simp) |
|
381 apply (rule_tac x = |
|
382 apply (auto dest:Info_flow_shm.cases) |
|
383 apply (auto simp add:one_flow_shm_simps) |
|
384 |
371 |
385 lemma info_flow_shm_detach: |
372 lemma info_flow_shm_detach: |
386 "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. |
373 "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. |
387 self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or> |
374 self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or> |
388 (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )" |
375 (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )" |