1 theory Enrich |
1 theory Enrich |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
3 Temp |
3 Temp |
4 begin |
4 begin |
5 |
5 |
|
6 (* enriched objects, closely related to static objects, so are only 3 kinds *) |
|
7 datatype t_enrich_obj = |
|
8 E_proc "t_process" "t_msgq" "t_msgq" |
|
9 | E_file_link "t_file" |
|
10 | E_file "t_file" "nat" |
|
11 (* |
|
12 | E_fd "t_process" "t_fd" |
|
13 | E_inum "nat" *) |
|
14 | E_msgq "t_msgq" |
|
15 (* |
|
16 | E_msg "t_msgq" "t_msg" |
|
17 *) |
|
18 |
|
19 |
6 (* objects that need dynamic indexing, all nature-numbers *) |
20 (* objects that need dynamic indexing, all nature-numbers *) |
7 datatype t_enrich_obj = |
21 datatype t_index_obj = |
8 E_proc "t_process" |
22 I_proc "t_process" |
9 | E_file "t_file" |
23 | I_file "t_file" |
10 | E_fd "t_process" "t_fd" |
24 | I_fd "t_process" "t_fd" |
11 | E_inum "nat" |
25 | I_inum "nat" |
12 | E_msgq "t_msgq" |
26 | I_msgq "t_msgq" |
13 | E_msg "t_msgq" "t_msg" |
27 | I_msg "t_msgq" "t_msg" |
14 |
28 |
15 context tainting_s begin |
29 context tainting_s begin |
16 |
30 |
17 fun no_del_event:: "t_event list \<Rightarrow> bool" |
31 fun no_del_event:: "t_event list \<Rightarrow> bool" |
18 where |
32 where |
71 | "all_files (Open p f flags fd opt # s) = (if opt = None then all_files s else (all_files s \<union> {f}))" |
85 | "all_files (Open p f flags fd opt # s) = (if opt = None then all_files s else (all_files s \<union> {f}))" |
72 | "all_files (Mkdir p f inum # s) = all_files s \<union> {f}" |
86 | "all_files (Mkdir p f inum # s) = all_files s \<union> {f}" |
73 | "all_files (LinkHard p f f' # s) = all_files s \<union> {f'}" |
87 | "all_files (LinkHard p f f' # s) = all_files s \<union> {f'}" |
74 | "all_files (e # s) = all_files s" |
88 | "all_files (e # s) = all_files s" |
75 |
89 |
|
90 (* |
76 fun notin_all:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool" |
91 fun notin_all:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool" |
77 where |
92 where |
78 "notin_all s (E_proc p) = (p \<notin> all_procs s)" |
93 "notin_all s (E_proc p) = (p \<notin> all_procs s)" |
79 | "notin_all s (E_file f) = (f \<notin> all_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))" |
94 | "notin_all s (E_file f) = (f \<notin> all_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))" |
80 | "notin_all s (E_fd p fd) = (fd \<notin> all_fds s p)" |
95 | "notin_all s (E_fd p fd) = (fd \<notin> all_fds s p)" |
81 | "notin_all s (E_inum i) = (i \<notin> all_inums s)" |
96 | "notin_all s (E_inum i) = (i \<notin> all_inums s)" |
82 | "notin_all s (E_msgq q) = (q \<notin> all_msgqs s)" |
97 | "notin_all s (E_msgq q) = (q \<notin> all_msgqs s)" |
83 | "notin_all s (E_msg q m) = (m \<notin> all_msgs s q)" |
98 | "notin_all s (E_msg q m) = (m \<notin> all_msgs s q)" |
|
99 *) |
|
100 |
|
101 fun nums_of_recvmsg:: "t_state \<Rightarrow> t_process \<Rightarrow> nat" |
|
102 where |
|
103 "nums_of_recvmsg [] p' = 0" |
|
104 | "nums_of_recvmsg (RecvMsg p q m # s) p' = |
|
105 (if p' = p then Suc (nums_of_recvmsg s p) else nums_of_recvmsg s p')" |
|
106 | "nums_of_recvmsg (e # s) p' = nums_of_recvmsg s p'" |
|
107 |
|
108 lemma nums_of_recv_0: |
|
109 "\<lbrakk>p \<notin> current_procs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> nums_of_recvmsg s p = 0" |
|
110 apply (induct s, simp) |
|
111 apply (frule vt_grant_os, frule vd_cons, case_tac a) |
|
112 apply (auto) |
|
113 done |
|
114 |
|
115 lemma new_msgq_1: |
|
116 "\<lbrakk>new_msgq s \<le> q; q \<le> new_msgq s - Suc 0\<rbrakk> \<Longrightarrow> False" |
|
117 apply (subgoal_tac "new_msgq s \<noteq> 0") |
|
118 apply (simp, simp add:new_msgq_def next_nat_def) |
|
119 done |
|
120 |
|
121 fun notin_cur:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool" |
|
122 where |
|
123 "notin_cur s (E_proc p qmin qmax) = |
|
124 (p \<notin> current_procs s \<and> qmin = new_msgq s \<and> qmax = new_msgq s + (nums_of_recvmsg s p) - 1)" |
|
125 | "notin_cur s (E_file f inum) = |
|
126 (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf) \<and> inum \<notin> current_inode_nums s)" |
|
127 | "notin_cur s (E_file_link f) = |
|
128 (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))" |
|
129 | "notin_cur s (E_msgq q) = (q \<notin> current_msgqs s)" |
84 |
130 |
85 lemma not_all_procs_cons: |
131 lemma not_all_procs_cons: |
86 "p \<notin> all_procs (e # s) \<Longrightarrow> p \<notin> all_procs s" |
132 "p \<notin> all_procs (e # s) \<Longrightarrow> p \<notin> all_procs s" |
87 by (case_tac e, auto) |
133 by (case_tac e, auto) |
88 |
134 |
116 |
162 |
117 lemma not_all_msgqs_prop3: |
163 lemma not_all_msgqs_prop3: |
118 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s" |
164 "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s" |
119 apply (induct s, simp) |
165 apply (induct s, simp) |
120 by (case_tac a, auto) |
166 by (case_tac a, auto) |
121 |
167 |
122 fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_enrich_obj \<Rightarrow> bool" |
168 fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_index_obj \<Rightarrow> bool" |
123 where |
169 where |
124 "enrich_not_alive s obj (E_file f) = (f \<notin> current_files s \<and> obj \<noteq> E_file f)" |
170 "enrich_not_alive s obj (I_file f) = |
125 | "enrich_not_alive s obj (E_proc p) = (p \<notin> current_procs s \<and> obj \<noteq> E_proc p)" |
171 (f \<notin> current_files s \<and> (\<forall> inum. obj \<noteq> E_file f inum) \<and> obj \<noteq> E_file_link f)" |
126 | "enrich_not_alive s obj (E_fd p fd) = |
172 | "enrich_not_alive s obj (I_proc p) = (p \<notin> current_procs s \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))" |
127 ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> obj \<noteq> E_fd p fd \<and> obj \<noteq> E_proc p)" |
173 | "enrich_not_alive s obj (I_fd p fd) = |
128 | "enrich_not_alive s obj (E_msgq q) = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q)" |
174 ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))" |
129 | "enrich_not_alive s obj (E_inum i) = (i \<notin> current_inode_nums s \<and> obj \<noteq> E_inum i)" |
175 | "enrich_not_alive s obj (I_msgq q) = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q \<and> |
130 | "enrich_not_alive s obj (E_msg q m) = |
176 (case obj of |
131 ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msg q m \<and> obj \<noteq> E_msgq q)" |
177 E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax) |
|
178 | _ \<Rightarrow> True) )" |
|
179 | "enrich_not_alive s obj (I_inum i) = (i \<notin> current_inode_nums s \<and> (\<forall> f. obj \<noteq> E_file f i))" |
|
180 | "enrich_not_alive s obj (I_msg q m) = |
|
181 ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msgq q \<and> |
|
182 (case obj of |
|
183 E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax) |
|
184 | _ \<Rightarrow> True) )" |
132 |
185 |
133 lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf" |
186 lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf" |
134 apply (case_tac f) |
187 apply (case_tac f) |
135 apply (simp, drule root_is_dir', simp+) |
188 apply (simp, drule root_is_dir', simp+) |
136 apply (simp add:parentf_is_dir_prop2) |
189 apply (simp add:parentf_is_dir_prop2) |
308 and fflags_remain: "\<forall> p fd flags. flags_of_proc_fd s p fd = Some flags \<longrightarrow> flags_of_proc_fd s' p fd = Some flags" |
361 and fflags_remain: "\<forall> p fd flags. flags_of_proc_fd s p fd = Some flags \<longrightarrow> flags_of_proc_fd s' p fd = Some flags" |
309 and sms_remain: "\<forall> q. msgs_of_queue s' q = msgs_of_queue s q" |
362 and sms_remain: "\<forall> q. msgs_of_queue s' q = msgs_of_queue s q" |
310 (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *) |
363 (* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *) |
311 and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd" |
364 and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd" |
312 and nodel: "no_del_event (e # s)" |
365 and nodel: "no_del_event (e # s)" |
313 and notin_all: "notin_all (e # s) obj'" |
366 and notin_cur: "notin_cur (e # s) obj'" |
314 shows "valid (e # s')" |
367 shows "valid (e # s')" |
315 proof- |
368 proof- |
316 from vd' have os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
369 from vd' have os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
317 by (auto dest:vt_grant_os vt_grant vd_cons) |
370 by (auto dest:vt_grant_os vt_grant vd_cons) |
318 show ?thesis |
371 show ?thesis |
370 next |
423 next |
371 case (Clone p p' fds) |
424 case (Clone p p' fds) |
372 have p_in: "p \<in> current_procs s'" using os alive |
425 have p_in: "p \<in> current_procs s'" using os alive |
373 apply (erule_tac x = "O_proc p" in allE) |
426 apply (erule_tac x = "O_proc p" in allE) |
374 by (auto simp:Clone) |
427 by (auto simp:Clone) |
375 have p'_not_in: "p' \<notin> current_procs s'" using alive' notin_all os Clone |
428 have p'_not_in: "p' \<notin> current_procs s'" using alive' notin_cur os Clone |
376 apply (erule_tac x = "E_proc p'" in allE) |
429 apply (erule_tac x = "I_proc p'" in allE) |
377 apply (auto dest:not_all_procs_prop3) |
430 apply (auto dest:not_all_procs_prop3 simp del:nums_of_recvmsg.simps) |
378 done |
431 done |
379 have fd_in: "fds \<subseteq> proc_file_fds s' p" using os alive ffd_remain |
432 have fd_in: "fds \<subseteq> proc_file_fds s' p" using os alive ffd_remain |
380 by (auto simp:Clone proc_file_fds_def) |
433 by (auto simp:Clone proc_file_fds_def) |
381 have "os_grant s' e" using p_in p'_not_in fd_in by (simp add:Clone) |
434 have "os_grant s' e" using p_in p'_not_in fd_in by (simp add:Clone) |
382 moreover have "grant s' e" |
435 moreover have "grant s' e" |
480 by (auto simp:Open None) |
533 by (auto simp:Open None) |
481 have f_in: "is_file s' f" using os alive |
534 have f_in: "is_file s' f" using os alive |
482 apply (erule_tac x = "O_file f" in allE) |
535 apply (erule_tac x = "O_file f" in allE) |
483 by (auto simp:Open None) |
536 by (auto simp:Open None) |
484 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
537 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
485 using os alive' p_in notin_all Open None |
538 using os alive' p_in notin_cur Open None |
486 apply (erule_tac x = "E_fd p fd" in allE) |
539 apply (erule_tac x = "I_fd p fd" in allE) |
487 apply (case_tac obj') |
540 apply (case_tac obj') |
488 apply (auto dest:not_all_procs_prop3) |
541 apply (auto dest:not_all_procs_prop3) |
489 done |
542 done |
490 have "os_grant s' e" using p_in f_in fd_not_in os |
543 have "os_grant s' e" using p_in f_in fd_not_in os |
491 by (simp add:Open None) |
544 by (simp add:Open None) |
528 apply (erule_tac x = "O_dir pf" in allE) |
581 apply (erule_tac x = "O_dir pf" in allE) |
529 by simp |
582 by simp |
530 have p_in: "p \<in> current_procs s'" using os alive |
583 have p_in: "p \<in> current_procs s'" using os alive |
531 apply (erule_tac x = "O_proc p" in allE) |
584 apply (erule_tac x = "O_proc p" in allE) |
532 by (auto simp:Open Some) |
585 by (auto simp:Open Some) |
533 have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_all |
586 have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_cur nodel |
534 apply (erule_tac x = "E_file f" in allE) |
587 apply (erule_tac x = "I_file f" in allE) |
535 apply (case_tac obj') |
588 by (case_tac obj', auto simp:current_files_simps) |
536 by auto |
|
537 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
589 have fd_not_in: "fd \<notin> current_proc_fds s' p" |
538 using os alive' p_in Open Some notin_all |
590 using os alive' p_in Open Some notin_cur |
539 apply (erule_tac x = "E_fd p fd" in allE) |
591 apply (erule_tac x = "I_fd p fd" in allE) |
540 apply (case_tac obj', auto dest:not_all_procs_prop3) |
592 apply (case_tac obj', auto dest:not_all_procs_prop3) |
541 done |
593 done |
542 have inum_not_in: "inum \<notin> current_inode_nums s'" |
594 have inum_not_in: "inum \<notin> current_inode_nums s'" |
543 using os alive' Open Some notin_all |
595 using os alive' Open Some notin_cur nodel |
544 apply (erule_tac x = "E_inum inum" in allE) |
596 apply (erule_tac x = "I_inum inum" in allE) |
545 by (case_tac obj', auto) |
597 apply (case_tac obj', auto) |
|
598 apply (auto simp add:current_inode_nums_def current_file_inums_def split:if_splits) |
|
599 done |
546 have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os |
600 have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os |
547 by (simp add:Open Some hungs) |
601 by (simp add:Open Some hungs) |
548 moreover have "grant s' e" |
602 moreover have "grant s' e" |
549 proof- |
603 proof- |
550 from grant parent obtain up rp tp uf rf tf |
604 from grant parent obtain up rp tp uf rf tf |
778 apply (drule parentf_is_dir_prop1, auto) |
832 apply (drule parentf_is_dir_prop1, auto) |
779 done |
833 done |
780 from pf_in_s alive have pf_in: "is_dir s' pf" |
834 from pf_in_s alive have pf_in: "is_dir s' pf" |
781 apply (erule_tac x = "O_dir pf" in allE) |
835 apply (erule_tac x = "O_dir pf" in allE) |
782 by (auto simp:Rmdir) |
836 by (auto simp:Rmdir) |
783 have empty_in: "dir_is_empty s' f" using os Rmdir notin_all |
837 have empty_in: "dir_is_empty s' f" using os Rmdir notin_cur |
784 apply (clarsimp simp add:dir_is_empty_def f_in) |
838 apply (clarsimp simp add:dir_is_empty_def f_in) |
785 using alive' |
839 using alive' |
786 apply (erule_tac x = "E_file f'" in allE) |
840 apply (erule_tac x = "I_file f'" in allE) |
787 apply simp |
841 apply simp |
788 apply (erule disjE) |
842 apply (erule disjE) |
789 apply (erule_tac x = f' in allE, simp) |
843 apply (erule_tac x = f' in allE, simp) |
790 apply (case_tac obj', simp_all) |
844 apply (case_tac obj', simp_all) |
|
845 apply (clarsimp) |
|
846 apply (drule_tac f' = f in parent_ancen) |
|
847 apply (simp, rule notI, simp add:noJ_Anc) |
|
848 apply (case_tac "f = pf") |
|
849 using vd' Rmdir |
|
850 apply (simp_all add:is_dir_rmdir) |
|
851 apply (erule_tac x = pf in allE) |
|
852 apply (drule_tac f = pf in is_dir_in_current) |
|
853 apply (simp add:noJ_Anc) |
|
854 |
791 apply (clarsimp) |
855 apply (clarsimp) |
792 apply (drule_tac f' = f in parent_ancen) |
856 apply (drule_tac f' = f in parent_ancen) |
793 apply (simp, rule notI, simp add:noJ_Anc) |
857 apply (simp, rule notI, simp add:noJ_Anc) |
794 apply (case_tac "f = pf") |
858 apply (case_tac "f = pf") |
795 using vd' Rmdir |
859 using vd' Rmdir |
849 apply (erule_tac x = "O_dir pf" in allE) |
913 apply (erule_tac x = "O_dir pf" in allE) |
850 by simp |
914 by simp |
851 have p_in: "p \<in> current_procs s'" using os alive |
915 have p_in: "p \<in> current_procs s'" using os alive |
852 apply (erule_tac x = "O_proc p" in allE) |
916 apply (erule_tac x = "O_proc p" in allE) |
853 by (auto simp:Mkdir) |
917 by (auto simp:Mkdir) |
854 have f_not_in: "f \<notin> current_files s'" using os alive' Mkdir notin_all |
918 have f_not_in: "f \<notin> current_files s'" |
855 apply (erule_tac x = "E_file f" in allE) |
919 using os alive' Mkdir notin_cur |
856 by (auto) |
920 apply (erule_tac x = "I_file f" in allE) |
|
921 by (auto simp:current_files_simps) |
857 have inum_not_in: "inum \<notin> current_inode_nums s'" |
922 have inum_not_in: "inum \<notin> current_inode_nums s'" |
858 using os alive' Mkdir notin_all |
923 using os alive' Mkdir notin_cur |
859 apply (erule_tac x = "E_inum inum" in allE) |
924 apply (erule_tac x = "I_inum inum" in allE) |
860 by (auto) |
925 apply (auto simp:current_inode_nums_def current_file_inums_def split:if_splits) |
|
926 done |
861 have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in |
927 have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in |
862 by (simp add:Mkdir hungs) |
928 by (simp add:Mkdir hungs) |
863 moreover have "grant s' e" |
929 moreover have "grant s' e" |
864 proof- |
930 proof- |
865 from grant parent obtain up rp tp uf rf tf |
931 from grant parent obtain up rp tp uf rf tf |
901 apply (erule_tac x = "O_dir pf" in allE) |
967 apply (erule_tac x = "O_dir pf" in allE) |
902 by simp |
968 by simp |
903 have p_in: "p \<in> current_procs s'" using os alive |
969 have p_in: "p \<in> current_procs s'" using os alive |
904 apply (erule_tac x = "O_proc p" in allE) |
970 apply (erule_tac x = "O_proc p" in allE) |
905 by (auto simp:LinkHard) |
971 by (auto simp:LinkHard) |
906 have f'_not_in: "f' \<notin> current_files s'" using os alive' LinkHard notin_all |
972 have f'_not_in: "f' \<notin> current_files s'" |
907 apply (erule_tac x = "E_file f'" in allE) |
973 using os alive' LinkHard notin_cur vd' |
908 by (auto simp:LinkHard) |
974 apply (erule_tac x = "I_file f'" in allE) |
|
975 apply (auto simp:LinkHard current_files_simps) |
|
976 done |
909 have f_in: "is_file s' f" using os alive |
977 have f_in: "is_file s' f" using os alive |
910 apply (erule_tac x = "O_file f" in allE) |
978 apply (erule_tac x = "O_file f" in allE) |
911 by (auto simp:LinkHard) |
979 by (auto simp:LinkHard) |
912 have "os_grant s' e" using p_in pf_in parent os f_in f'_not_in |
980 have "os_grant s' e" using p_in pf_in parent os f_in f'_not_in |
913 by (simp add:LinkHard hungs) |
981 by (simp add:LinkHard hungs) |
1002 next |
1070 next |
1003 case (CreateMsgq p q) |
1071 case (CreateMsgq p q) |
1004 have p_in: "p \<in> current_procs s'" using os alive |
1072 have p_in: "p \<in> current_procs s'" using os alive |
1005 apply (erule_tac x = "O_proc p" in allE) |
1073 apply (erule_tac x = "O_proc p" in allE) |
1006 by (auto simp:CreateMsgq) |
1074 by (auto simp:CreateMsgq) |
1007 have q_not_in: "q \<notin> current_msgqs s'" using os alive' CreateMsgq notin_all |
1075 have q_not_in: "q \<notin> current_msgqs s'" |
1008 apply (erule_tac x = "E_msgq q" in allE) |
1076 using os alive' CreateMsgq notin_cur nodel vd |
1009 by auto |
1077 apply (erule_tac x = "I_msgq q" in allE) |
|
1078 apply (auto split:t_enrich_obj.splits) |
|
1079 apply (drule nums_of_recv_0, simp+) |
|
1080 apply (drule new_msgq_1, simp+) |
|
1081 done |
1010 have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq) |
1082 have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq) |
1011 moreover have "grant s' e" |
1083 moreover have "grant s' e" |
1012 proof- |
1084 proof- |
1013 from grant obtain up rp tp |
1085 from grant obtain up rp tp |
1014 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
1086 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
1060 apply (erule_tac x = "O_proc p" in allE) |
1132 apply (erule_tac x = "O_proc p" in allE) |
1061 by (auto simp:SendMsg) |
1133 by (auto simp:SendMsg) |
1062 have q_in: "q \<in> current_msgqs s'" using os alive |
1134 have q_in: "q \<in> current_msgqs s'" using os alive |
1063 apply (erule_tac x = "O_msgq q" in allE) |
1135 apply (erule_tac x = "O_msgq q" in allE) |
1064 by (simp add:SendMsg) |
1136 by (simp add:SendMsg) |
1065 have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in |
1137 have m_not_in: "m \<notin> set (msgs_of_queue s' q)" |
1066 apply (erule_tac x = "E_msg q m" in allE) |
1138 using os alive' notin_cur SendMsg q_in nodel vd |
|
1139 apply (erule_tac x = "I_msg q m" in allE) |
1067 apply (case_tac obj', auto dest:not_all_msgqs_prop3) |
1140 apply (case_tac obj', auto dest:not_all_msgqs_prop3) |
|
1141 apply (drule nums_of_recv_0, simp+) |
|
1142 apply (drule new_msgq_1, simp+) |
1068 done |
1143 done |
1069 have "os_grant s' e" using p_in q_in m_not_in sms_remain os |
1144 have "os_grant s' e" using p_in q_in m_not_in sms_remain os |
1070 by (simp add:SendMsg) |
1145 by (simp add:SendMsg) |
1071 moreover have "grant s' e" |
1146 moreover have "grant s' e" |
1072 proof- |
1147 proof- |