181 apply (rule ext) |
181 apply (rule ext) |
182 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof |
182 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof |
183 split:option.splits t_inode_tag.splits) |
183 split:option.splits t_inode_tag.splits) |
184 done |
184 done |
185 |
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 |
186 lemma enrich_msgq_alive: |
221 lemma enrich_msgq_alive: |
187 "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> |
222 "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk> |
188 \<Longrightarrow> alive (enrich_msgq s q q') obj" |
223 \<Longrightarrow> alive (enrich_msgq s q q') obj" |
189 apply (case_tac obj) |
224 apply (case_tac obj) |
190 apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs |
225 apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs |
748 apply (simp_all only:cfd2sfd_simps enrich_msgq.simps) |
785 apply (simp_all only:cfd2sfd_simps enrich_msgq.simps) |
749 apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits) |
786 apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits) |
750 done |
787 done |
751 qed |
788 qed |
752 |
789 |
753 thm psec_cons |
|
754 thm cp2sproc_def |
|
755 have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> |
790 have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> |
756 cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp" |
791 cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp" |
757 apply (auto simp add:cpfd2sfds_def) |
792 apply (auto simp add:cpfd2sfds_def proc_file_fds_def) |
758 sorry |
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 |
759 |
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 |
760 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" |
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" |
761 by (auto simp:proc_file_fds_def elim!:sfd_cons) |
811 by (auto simp:proc_file_fds_def elim!:sfd_cons) |
762 moreover |
812 moreover |
763 have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp" |
813 have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp" |
764 apply (auto simp:cp2sproc_def pfds_cons psec_cons split:option.splits) |
814 by (auto simp:cp2sproc_def pfds_cons psec_cons enrich_msgq_died_proc split:option.splits) |
765 sorry |
|
766 moreover |
815 moreover |
767 have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" |
816 have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" |
768 sorry |
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 |
769 moreover |
886 moreover |
770 have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q" |
887 have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q" |
771 sorry |
888 proof- |
772 ultimately show ?case using vd_enrich_cons sf_cons |
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 |
773 by auto |
956 by auto |
774 qed |
957 qed |
|
958 |
|
959 |
|
960 |
|
961 lemma enrich_msgq_s2ss: |
|
962 "" |
775 |
963 |
776 |
964 |
777 thm cp2sproc_def |
965 thm cp2sproc_def |
778 |
966 |
779 (* enrich s target_proc duplicated_pro *) |
967 (* enrich s target_proc duplicated_pro *) |