54 proof (induct s) |
54 proof (induct s) |
55 case Nil |
55 case Nil |
56 thus ?case by (auto simp:is_created_proc_def) |
56 thus ?case by (auto simp:is_created_proc_def) |
57 next |
57 next |
58 case (Cons e s) |
58 case (Cons e s) |
59 hence vd_cons: "valid (e # s)" and created_cons: "is_created_proc (e # s) p" |
59 hence vd_cons': "valid (e # s)" and created_cons: "is_created_proc (e # s) p" |
60 and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" |
60 and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" |
61 and os: "os_grant s e" and grant: "grant s e" |
61 and os: "os_grant s e" and grant: "grant s e" |
62 by (auto dest:vd_cons vt_grant_os vt_grant) |
62 by (auto dest:vd_cons' vt_grant_os vt_grant) |
63 from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto) |
63 from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto) |
64 from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and> |
64 from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and> |
65 (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
65 (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
66 (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
66 (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and> |
67 files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and> |
67 files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and> |
480 using a1 |
480 using a1 |
481 by (erule_tac valid.intros(2), simp+) |
481 by (erule_tac valid.intros(2), simp+) |
482 qed |
482 qed |
483 qed |
483 qed |
484 ultimately show ?thesis |
484 ultimately show ?thesis |
485 using created_cons vd_cons all_procs_cons |
485 using created_cons vd_cons' all_procs_cons |
486 apply (case_tac e) |
486 apply (case_tac e) |
487 apply (auto simp:is_created_proc_simps split:if_splits) |
487 apply (auto simp:is_created_proc_simps split:if_splits) |
488 done |
488 done |
489 qed |
489 qed |
490 moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj" |
490 moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj" |
491 sorry |
491 proof clarify |
|
492 fix obj |
|
493 assume a0: "alive (e # s) obj" |
|
494 have a1: "is_created_proc s p \<Longrightarrow> \<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" |
|
495 using pre by auto |
|
496 show "alive (enrich_proc (e # s) p p') obj" (* |
|
497 proof (cases e) |
|
498 case (Execve tp f fds) |
|
499 with created_cons a1 |
|
500 have b1: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" |
|
501 by (auto simp:is_created_proc_simps) |
|
502 show ?thesis |
|
503 using created_cons all_procs_cons vd_enrich_cons Execve b1 os a0 |
|
504 apply (simp add:alive_execve split:if_splits) |
|
505 apply (frule_tac vd_cons) defer |
|
506 apply (frule_tac vd_cons) |
|
507 using vd_cons' Execve vd os |
|
508 apply (auto simp:is_file_simps is_dir_simps is_created_proc_simps alive.simps |
|
509 split:t_object.splits if_splits |
|
510 dest:set_mp file_fds_subset_pfds) |
|
511 apply (erule_tac x = "O_proc nat" in allE, simp) |
|
512 apply (erule_tac x = "O_file list" in allE, simp) |
|
513 apply (drule set_mp, simp) |
|
514 apply (drule_tac s = s and p = tp in file_fds_subset_pfds) |
|
515 apply (erule_tac x = "O_fd tp nat2" in allE, simp) |
|
516 apply (auto)[1] |
|
517 apply (erule_tac x = "O_fd nat1 nat2" in allE, auto dest:set_mp file_fds_subset_pfds)[1] |
|
518 apply (erule_tac x = "O_dir list" in allE, simp) |
|
519 sorry |
|
520 show ?thesis *) sorry |
492 moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj" |
521 moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj" |
|
522 thm enrich_not_alive.simps |
493 sorry |
523 sorry |
494 moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)" |
524 moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)" |
|
525 proof- |
|
526 have "is_created_proc s p \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s" |
|
527 and ffd_remain: "is_created_proc s p \<Longrightarrow> |
|
528 \<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> |
|
529 file_of_proc_fd (enrich_proc s p p') tp fd = Some f" |
|
530 using pre by auto |
|
531 with created_cons all_procs_cons os vd_cons' vd |
|
532 show ?thesis |
|
533 apply (frule_tac not_all_procs_prop3) |
|
534 apply (case_tac e) |
|
535 apply (auto simp:files_hung_by_del.simps is_created_proc_simps) |
|
536 apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def procfd_of_file_eq_fpfd'' |
|
537 dest:procfd_of_file_imp_fpfd procfd_of_file_imp_fpfd' procfd_of_file_non_empty |
|
538 ) |
|
539 apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def split:if_splits)[1] |
|
540 |
|
541 apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def files_hung_by_del.simps |
|
542 split:option.splits)[1] |
|
543 apply (auto split:option.splits)[1] |
|
544 thm is_created_proc_simps |
495 sorry |
545 sorry |
496 moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp" |
546 moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp" |
497 sorry |
547 sorry |
498 moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" |
548 moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" |
499 sorry |
549 sorry |
522 and a2: "valid (Execve tp f fds # s)" and a3: "is_created_proc (Execve tp f fds # s) p" |
572 and a2: "valid (Execve tp f fds # s)" and a3: "is_created_proc (Execve tp f fds # s) p" |
523 and a4: "p' \<notin> all_procs (Execve tp f fds # s)" |
573 and a4: "p' \<notin> all_procs (Execve tp f fds # s)" |
524 show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p" |
574 show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p" |
525 proof (cases "tp = p") |
575 proof (cases "tp = p") |
526 case True |
576 case True |
527 show ?thesis using True a1 a2 a3 a4 |
577 show ?thesis using True a1 a2 a3 a4 b0 |
528 thm not_all_procs_prop3 |
578 thm not_all_procs_prop3 |
|
579 apply (frule_tac not_all_procs_prop2) |
|
580 apply (frule not_all_procs_prop3) |
529 apply (auto simp add:cp2sproc_execve is_created_proc_def split:option.splits dest!:current_has_sec' |
581 apply (auto simp add:cp2sproc_execve is_created_proc_def split:option.splits dest!:current_has_sec' |
530 dest:vt_grant_os not_all_procs_prop2 not_all_procs_prop3) |
582 dest:vt_grant_os) |
|
583 apply (auto simp:sectxt_of_obj_simps split:option.splits dest:valid.cases) |
531 |
584 |
532 sorry |
585 sorry |
533 next |
586 next |
534 case False |
587 case False |
535 show ?thesis sorry |
588 show ?thesis sorry |
550 have b7: "\<And> tp fd. cp2sproc (enrich_proc (CloseFd tp fd # s) p p') p' = cp2sproc (CloseFd tp fd # s) p" |
603 have b7: "\<And> tp fd. cp2sproc (enrich_proc (CloseFd tp fd # s) p p') p' = cp2sproc (CloseFd tp fd # s) p" |
551 sorry |
604 sorry |
552 show ?thesis using vd_enrich_cons |
605 show ?thesis using vd_enrich_cons |
553 apply (case_tac e) |
606 apply (case_tac e) |
554 apply (simp_all only:b1 b2 b3 b4 b5 b6 b7) |
607 apply (simp_all only:b1 b2 b3 b4 b5 b6 b7) |
555 using created_cons vd_enrich_cons vd_cons b0 |
608 using created_cons vd_enrich_cons vd_cons' b0 |
556 apply (auto simp:cp2sproc_other is_created_proc_def) |
609 apply (auto simp:cp2sproc_other is_created_proc_def) |
557 done |
610 done |
558 qed |
611 qed |
559 moreover have "\<forall> fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> |
612 moreover have "\<forall> fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> |
560 cfd2sfd (enrich_proc (e # s) p p') p' fd = cfd2sfd (e # s) p fd" |
613 cfd2sfd (enrich_proc (e # s) p p') p' fd = cfd2sfd (e # s) p fd" |