diff -r ded3f83f6cb9 -r 003cac7b8bf5 no_shm_selinux/Enrich2.thy --- a/no_shm_selinux/Enrich2.thy Mon Jan 06 23:07:51 2014 +0800 +++ b/no_shm_selinux/Enrich2.thy Tue Jan 07 22:04:06 2014 +0800 @@ -203,6 +203,579 @@ apply (auto split:if_splits) done +lemma enrich_msgq_not_alive: + "\enrich_not_alive s (E_msgq q') obj; q' \ current_msgqs s; q \ current_msgqs s; no_del_event s; valid s\ + \ enrich_not_alive (enrich_msgq s q q') (E_msgq q') obj" +apply (case_tac obj) +apply (auto simp:enrich_msgq_cur_fds enrich_msgq_cur_files + enrich_msgq_cur_procs enrich_msgq_cur_inums enrich_msgq_cur_msgqs enrich_msgq_cur_msgs) +done + +lemma enrich_msgq_no_del: + "\no_del_event s\ \ no_del_event (enrich_msgq s q q')" +apply (induct s, simp) +by (case_tac a, auto) + +lemma nodel_died_proc: + "no_del_event s \ \ died (O_proc p) s" +apply (induct s, simp) +by (case_tac a, auto) + +lemma cf2sfile_execve: + "\ff \ current_files (Execve p f fds # s); valid (Execve p f fds # s)\ + \ cf2sfile (Execve p f fds # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_clone: + "\ff \ current_files (Clone p p' fds # s); valid (Clone p p' fds # s)\ + \ cf2sfile (Clone p p' fds # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_ptrace: + "\ff \ current_files (Ptrace p p' # s); valid (Ptrace p p' # s)\ + \ cf2sfile (Ptrace p p' # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_readfile: + "\ff \ current_files (ReadFile p fd # s); valid (ReadFile p fd # s)\ + \ cf2sfile (ReadFile p fd # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_writefile: + "\ff \ current_files (WriteFile p fd # s); valid (WriteFile p fd # s)\ + \ cf2sfile (WriteFile p fd # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_truncate: + "\ff \ current_files (Truncate p f len # s); valid (Truncate p f len # s)\ + \ cf2sfile (Truncate p f len # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_createmsgq: + "\ff \ current_files (CreateMsgq p q # s); valid (CreateMsgq p q # s)\ + \ cf2sfile (CreateMsgq p q # s) ff= cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_sendmsg: + "\ff \ current_files (SendMsg p q m # s); valid (SendMsg p q m # s)\ + \ cf2sfile (SendMsg p q m # s) ff = cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemma cf2sfile_recvmsg: + "\ff \ current_files (RecvMsg p q m # s); valid (RecvMsg p q m # s)\ + \ cf2sfile (RecvMsg p q m # s) ff = cf2sfile s ff" +by (auto dest:cf2sfile_other' simp:current_files_simps) +lemmas cf2sfile_other'' = cf2sfile_recvmsg cf2sfile_sendmsg cf2sfile_createmsgq cf2sfile_truncate + cf2sfile_writefile cf2sfile_readfile cf2sfile_ptrace cf2sfile_clone cf2sfile_execve + +lemma enrich_msgq_prop: + "\valid s; q \ current_msgqs s; q' \ current_msgqs s; no_del_event s\ + \ valid (enrich_msgq s q q') \ + (\ tp. tp \ current_procs s \ cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \ + (\ f. f \ current_files s \ cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \ + (\ tq. tq \ current_msgqs s \ cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \ + (\ tp fd. fd \ proc_file_fds s tp \ cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \ + (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)" +proof (induct s) + case Nil + thus ?case by (auto) +next + case (Cons e s) + hence vd_cons': "valid (e # s)" and curq_cons: "q \ current_msgqs (e # s)" + and curq'_cons: "q' \ current_msgqs (e # s)" and nodel_cons: "no_del_event (e # s)" + and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" + by (auto dest:vd_cons vt_grant_os vt_grant) + from curq'_cons nodel_cons have curq': "q' \ current_msgqs s" by (case_tac e, auto) + from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto) + from nodel curq' vd Cons + have pre: "q \ current_msgqs s \ valid (enrich_msgq s q q') \ + (\tp. tp \ current_procs s \ cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \ + (\f. f \ current_files s \ cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \ + (\tq. tq \ current_msgqs s \ cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \ + (\tp fd. fd \ proc_file_fds s tp \ cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \ + (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)" + by auto + + from pre have pre_vd: "q \ current_msgqs s \ valid (enrich_msgq s q q')" by simp + from pre have pre_sp: "\ tp. \tp \ current_procs s; q \ current_msgqs s\ + \ cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp" by auto + from pre have pre_sf: "\ f. \f \ current_files s; q \ current_msgqs s\ + \ cf2sfile (enrich_msgq s q q') f = cf2sfile s f" by auto + from pre have pre_sq: "\ tq. \tq \ current_msgqs s; q \ current_msgqs s\ + \ cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq" by auto + from pre have pre_sfd: "\ tp fd. \fd \ proc_file_fds s tp; q \ current_msgqs s\ + \ cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by auto + hence pre_sfd': "\ tp fd f. \file_of_proc_fd s tp fd = Some f; q \ current_msgqs s\ + \ cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def) + from pre have pre_duq: "q \ current_msgqs s \ cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q" + by auto + have vd_enrich:"q \ current_msgqs s \ valid (e # enrich_msgq s q q')" + apply (frule pre_vd) + apply (erule_tac s = s and obj' = "E_msgq q'" in enrich_valid_intro_cons) + apply (simp_all add:pre nodel nodel_cons curq_cons vd_cons' vd enrich_msgq_hungs) + apply (clarsimp simp:nodel vd curq' enrich_msgq_alive) + apply (rule allI, rule impI, erule enrich_msgq_not_alive) + apply (simp_all add:curq' curq'_cons nodel vd enrich_msgq_cur_msgs enrich_msgq_filefd enrich_msgq_flagfd) + done + + have q_neq_q': "q' \ q" using curq'_cons curq_cons by auto + + have vd_enrich_cons: "valid (enrich_msgq (e # s) q q')" + proof- + have "\ p q''. e = CreateMsgq p q'' \ valid (enrich_msgq (e # s) q q')" + proof- + fix p q'' assume ev: "e = CreateMsgq p q''" + show "valid (enrich_msgq (e # s) q q')" + proof (cases "q'' = q") + case False with ev vd_enrich curq_cons + show ?thesis by simp + next + case True + have "os_grant (CreateMsgq p q # s) (CreateMsgq p q')" + using os ev + by (simp add:q_neq_q' curq') + moreover have "grant (CreateMsgq p q # s) (CreateMsgq p q')" + using grant ev + by (auto simp add:sectxt_of_obj_def split:option.splits) + ultimately + show ?thesis using ev vd_cons' True + by (auto intro: valid.intros(2)) + qed + qed + moreover have "\ p q'' m. \e = SendMsg p q'' m; q \ current_msgqs s\ + \ valid (enrich_msgq (e # s) q q')" + proof- + fix p q'' m assume ev: "e = SendMsg p q'' m" and q_in: "q \ current_msgqs s" + show "valid (enrich_msgq (e # s) q q')" + proof (cases "q'' = q") + case False with ev vd_enrich q_in + show ?thesis by simp + next + case True + from grant os ev True obtain psec qsec + where psec: "sectxt_of_obj s (O_proc p) = Some psec" + and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec" + by (auto split:option.splits) + from psec q_in os ev + have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec" + by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits) + from qsec q_in pre_duq vd + have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec" + by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') + show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd + curq' psec psec' qsec qsec' grant os q_neq_q' + apply (simp, erule_tac valid.intros(2)) + apply (auto simp:q_neq_q' enrich_msgq_cur_msgqs enrich_msgq_cur_procs + enrich_msgq_cur_msgs sectxt_of_obj_simps) + done + qed + qed + moreover have "\ p q'' m. \e = RecvMsg p q'' m; q \ current_msgqs s\ + \ valid (enrich_msgq (e # s) q q')" + proof- + fix p q'' m assume ev: "e = RecvMsg p q'' m" and q_in: "q \ current_msgqs s" + show "valid (enrich_msgq (e # s) q q')" + proof (cases "q'' = q") + case False with ev vd_enrich q_in + show ?thesis by simp + next + case True + from grant os ev True obtain psec qsec msec + where psec: "sectxt_of_obj s (O_proc p) = Some psec" + and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec" + and msec: "sectxt_of_obj s (O_msg q (hd (msgs_of_queue s q))) = Some msec" + by (auto split:option.splits) + from psec q_in os ev + have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec" + by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits) + from qsec q_in pre_duq vd + have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec" + by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') + from qsec q_in vd + have qsec'': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q) = Some qsec" + apply (frule_tac pre_sq, simp_all) + by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms') + from msec q_in pre_duq vd qsec qsec' qsec'' curq' nodel + have msec': "sectxt_of_obj (enrich_msgq s q q') (O_msg q' (hd (msgs_of_queue s q))) = Some msec" + apply (auto simp:cq2smsgq_def enrich_msgq_cur_msgs + split:option.splits dest!:current_has_sms') + apply (case_tac "msgs_of_queue s q") + using os ev True apply simp + apply (simp add:cqm2sms.simps split:option.splits) + apply (auto simp:cm2smsg_def split:option.splits) + done + show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd + curq' grant os q_neq_q' psec psec' msec msec' qsec qsec' + apply (simp, erule_tac valid.intros(2)) + apply (auto simp:enrich_msgq_cur_msgqs enrich_msgq_cur_procs + enrich_msgq_cur_msgs sectxt_of_obj_simps) + done + qed + qed + ultimately + show ?thesis using vd_enrich curq_cons vd_cons' + apply (case_tac e) + apply (auto simp del:enrich_msgq.simps) + apply (auto split:if_splits ) + done + qed + + have curpsec: "\ tp. \tp \ current_procs s; q \ current_msgqs s\ \ + sectxt_of_obj (enrich_msgq s q q') (O_proc tp) = sectxt_of_obj s (O_proc tp)" + using pre_vd vd + apply (frule_tac pre_sp, simp) + by (auto simp:cp2sproc_def split:option.splits if_splits dest!:current_has_sec') + have curfsec: "\ f. \is_file s f; q \ current_msgqs s\ \ + sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)" + proof- + fix f + assume a1: "is_file s f" and a2: "q \ current_msgqs s" + from a2 pre_sf pre_vd + have pre': "\f. f \ current_files s \ cf2sfile (enrich_msgq s q q') f = cf2sfile s f" + and vd_enrich: "valid (enrich_msgq s q q')" + by auto + hence csf: "cf2sfile (enrich_msgq s q q') f = cf2sfile s f" + using a1 by (auto simp:is_file_in_current) + from a1 obtain sf where csf_some: "cf2sfile s f = Some sf" + apply (case_tac "cf2sfile s f") + apply (drule current_file_has_sfile') + apply (simp add:vd, simp add:is_file_in_current, simp) + done + from a1 have a1': "is_file (enrich_msgq s q q') f" + using vd nodel by (simp add:enrich_msgq_is_file) + show "sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)" + using csf csf_some vd_enrich vd a1 a1' + apply (auto simp:cf2sfile_def split:option.splits if_splits) + apply (case_tac f, simp_all) + apply (drule root_is_dir', simp+) + done + qed + have curdsec: "\ tf. \is_dir s tf; q \ current_msgqs s\ + \ sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)" + proof- + fix tf + assume a1: "is_dir s tf" and a2: "q \ current_msgqs s" + from a2 pre_sf pre_vd + have pre': "\f. f \ current_files s \ cf2sfile (enrich_msgq s q q') f = cf2sfile s f" + and vd_enrich: "valid (enrich_msgq s q q')" + by auto + hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf" + using a1 by (auto simp:is_dir_in_current) + from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf" + apply (case_tac "cf2sfile s tf") + apply (drule current_file_has_sfile') + apply (simp add:vd, simp add:is_dir_in_current, simp) + done + from a1 have a1': "is_dir (enrich_msgq s q q') tf" + using enrich_msgq_is_dir vd nodel by simp + from a1 have a3: "\ is_file s tf" using vd by (simp add:is_dir_not_file) + from a1' vd have a3': "\ is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) + show "sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)" + using csf csf_some a3 a3' vd_enrich vd + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac tf) + apply (simp add:root_sec_remains, simp) + done + qed + have curpsecs: "\ tf ctxts'. \is_dir s tf; q \ current_msgqs s; get_parentfs_ctxts s tf = Some ctxts'\ + \ \ ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \ set ctxts = set ctxts'" + proof- + fix tf ctxts' + assume a1: "is_dir s tf" and a2: "q \ current_msgqs s" + and a4: "get_parentfs_ctxts s tf = Some ctxts'" + from a2 pre + have pre': "\f. f \ current_files s \ cf2sfile (enrich_msgq s q q') f = cf2sfile s f" + and vd_enrich': "valid (enrich_msgq s q q')" + by auto + hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf" + using a1 by (auto simp:is_dir_in_current) + from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf" + apply (case_tac "cf2sfile s tf") + apply (drule current_file_has_sfile') + apply (simp add:vd, simp add:is_dir_in_current, simp) + done + from a1 have a1': "is_dir (enrich_msgq s q q') tf" + using enrich_msgq_is_dir vd nodel by simp + from a1 have a5: "\ is_file s tf" using vd by (simp add:is_dir_not_file) + from a1' vd have a5': "\ is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) + + from a1' pre_vd a2 obtain ctxts + where a3: "get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts" + apply (case_tac "get_parentfs_ctxts (enrich_msgq s q q') tf") + apply (drule get_pfs_secs_prop', simp+) + done + moreover have "set ctxts = set ctxts'" + proof (cases tf) + case Nil + with a3 a4 vd vd_enrich' + show ?thesis + by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits) + next + case (Cons a ff) + with csf csf_some a5 a5' vd_enrich' vd a3 a4 + show ?thesis + apply (auto simp:cf2sfile_def split:option.splits if_splits) + done + qed + ultimately + show "\ ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \ set ctxts = set ctxts'" + by auto + qed + + have psec_cons: "\ tp. tp \ current_procs (e # s) \ + sectxt_of_obj (enrich_msgq (e # s) q q') (O_proc tp) = sectxt_of_obj (e # s) (O_proc tp)" + using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd + apply (case_tac e) + apply (auto intro:curpsec simp:sectxt_of_obj_simps) + apply (frule curpsec, simp, frule curfsec, simp) + apply (auto split:option.splits)[1] + apply (frule vd_cons) defer apply (frule vd_cons) + apply (auto intro:curpsec simp:sectxt_of_obj_simps) + done + + + have sf_cons: "\ f. f \ current_files (e # s) \ cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof- + fix f + assume a1: "f \ current_files (e # s)" + hence a1': "f \ current_files (enrich_msgq (e # s) q q')" + using nodel_cons os vd vd_cons' vd_enrich_cons + apply (case_tac e) + apply (auto simp:current_files_simps enrich_msgq_cur_files dest:is_file_in_current split:option.splits) + done + have b1: "\ p f' flags fd opt. e = Open p f' flags fd opt \ + cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof- + fix p f' flags fd opt + assume ev: "e = Open p f' flags fd opt" + show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof (cases opt) + case None + with a1 a1' ev vd_cons' vd_enrich_cons curq_cons + show ?thesis + apply (simp add:cf2sfile_open_none) + apply (simp add:pre_sf current_files_simps) + done + next + case (Some inum) + show ?thesis + proof (cases "f = f'") + case False + with a1 a1' ev vd_cons' vd_enrich_cons curq_cons Some + show ?thesis + apply (simp add:cf2sfile_open) + apply (simp add:pre_sf current_files_simps) + done + next + case True + with vd_cons' ev os Some + obtain pf where pf: "parent f = Some pf" by auto + then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" + using os vd ev Some True + apply (case_tac "get_parentfs_ctxts s pf") + apply (drule get_pfs_secs_prop', simp, simp) + apply auto + done + + have "sectxt_of_obj (Open p f' flags fd (Some inum) # enrich_msgq s q q') (O_file f') = + sectxt_of_obj (Open p f' flags fd (Some inum) # s) (O_file f')" + using Some vd_enrich_cons vd_cons' ev pf True os curq_cons + by (simp add:sectxt_of_obj_simps curpsec curdsec) + moreover + have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" + using curq_cons ev pf Some True os + by (simp add:curdsec) + moreover + have "\ ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \ set ctxts' = set ctxts" + using curq_cons ev pf Some True os vd psecs + apply (case_tac "get_parentfs_ctxts s pf") + apply (drule get_pfs_secs_prop', simp+) + apply (rule curpsecs, simp+) + done + then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" + and psecs_eq: "set ctxts' = set ctxts" by auto + ultimately show ?thesis + using a1 a1' ev vd_cons' vd_enrich_cons Some True pf psecs + by (simp add:cf2sfile_open split:option.splits) + qed + qed + qed + have b2: "\ p f' inum. e = Mkdir p f' inum \ + cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof- + fix p f' inum + assume ev: "e = Mkdir p f' inum" + show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof (cases "f' = f") + case False + with a1 a1' ev vd_cons' vd_enrich_cons curq_cons + show ?thesis + apply (simp add:cf2sfile_mkdir) + apply (simp add:pre_sf current_files_simps) + done + next + case True + with vd_cons' ev os + obtain pf where pf: "parent f = Some pf" by auto + then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" + using os vd ev True + apply (case_tac "get_parentfs_ctxts s pf") + apply (drule get_pfs_secs_prop', simp, simp) + apply auto + done + + have "sectxt_of_obj (Mkdir p f' inum # enrich_msgq s q q') (O_dir f') = + sectxt_of_obj (Mkdir p f' inum # s) (O_dir f')" + using vd_enrich_cons vd_cons' ev pf True os curq_cons + by (simp add:sectxt_of_obj_simps curpsec curdsec) + moreover + have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" + using curq_cons ev pf True os + by (simp add:curdsec) + moreover + have "\ ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \ set ctxts' = set ctxts" + using curq_cons ev pf True os vd psecs + apply (case_tac "get_parentfs_ctxts s pf") + apply (drule get_pfs_secs_prop', simp+) + apply (rule curpsecs, simp+) + done + then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" + and psecs_eq: "set ctxts' = set ctxts" by auto + ultimately show ?thesis + using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs + apply (simp add:cf2sfile_mkdir split:option.splits) + done + qed + qed + have b3: "\ p f' f''. e = LinkHard p f' f'' \ + cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof- + fix p f' f'' + assume ev: "e = LinkHard p f' f''" + show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + proof (cases "f'' = f") + case False + with a1 a1' ev vd_cons' vd_enrich_cons curq_cons + show ?thesis + apply (simp add:cf2sfile_linkhard) + apply (simp add:pre_sf current_files_simps) + done + next + case True + with vd_cons' ev os + obtain pf where pf: "parent f = Some pf" by auto + then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts" + using os vd ev True + apply (case_tac "get_parentfs_ctxts s pf") + apply (drule get_pfs_secs_prop', simp, simp) + apply auto + done + + have "sectxt_of_obj (LinkHard p f' f'' # enrich_msgq s q q') (O_file f) = + sectxt_of_obj (LinkHard p f' f'' # s) (O_file f)" + using vd_enrich_cons vd_cons' ev pf True os curq_cons + by (simp add:sectxt_of_obj_simps curpsec curdsec) + moreover + have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)" + using curq_cons ev pf True os + by (simp add:curdsec) + moreover + have "\ ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \ set ctxts' = set ctxts" + using curq_cons ev pf True os vd psecs + apply (case_tac "get_parentfs_ctxts s pf") + apply (drule get_pfs_secs_prop', simp+) + apply (rule curpsecs, simp+) + done + then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'" + and psecs_eq: "set ctxts' = set ctxts" by auto + ultimately show ?thesis + using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs + apply (simp add:cf2sfile_linkhard split:option.splits) + done + qed + qed + show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f" + apply (case_tac e) + prefer 6 apply (erule b1) + prefer 11 apply (erule b2) + prefer 11 apply (erule b3) + apply (simp_all only:b1 b2 b3) + using a1' a1 vd_enrich_cons vd_cons' curq_cons nodel_cons + apply (simp_all add:cf2sfile_other'' cf2sfile_simps enrich_msgq.simps no_del_event.simps split:if_splits) + apply (simp_all add:pre_sf cf2sfile_other' current_files_simps split:if_splits) + apply (drule vd_cons, simp add:cf2sfile_other', drule pre_sf, simp+)+ + done + qed + + have sfd_cons:"\ tp fd f. file_of_proc_fd (e # s) tp fd = Some f \ + cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" + proof- + fix tp fd f + assume a1: "file_of_proc_fd (e # s) tp fd = Some f" + hence a1': "file_of_proc_fd (enrich_msgq (e # s) q q') tp fd = Some f" + using nodel_cons vd_enrich os vd_cons' + apply (case_tac e, auto simp:enrich_msgq_filefd simp del:enrich_msgq.simps) + done + have b1: "\ p f' flags fd' opt. e = Open p f' flags fd' opt \ + cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" + proof- + fix p f' flags fd' opt + assume ev: "e = Open p f' flags fd' opt" + have c1': "file_of_proc_fd (Open p f' flags fd' opt # s) tp fd = Some f" + using a1' ev a1 by (simp split:if_splits) + show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" thm cfd2sfd_open + proof (cases "tp = p \ fd = fd'") + case False + show ?thesis using ev vd_enrich_cons vd_cons' a1' a1 False curq_cons + apply (simp add:cfd2sfd_open split:if_splits del:file_of_proc_fd.simps) + apply (rule conjI, rule impI, simp) + apply (rule conjI, rule impI, simp) + apply (auto simp: False intro!:pre_sfd' split:if_splits) + done + next + case True + have "f' \ current_files (Open p f' flags fd' opt # s)" using ev vd_cons' os + by (auto simp:current_files_simps is_file_in_current split:option.splits) + hence "cf2sfile (Open p f' flags fd' opt # enrich_msgq s q q') f' + = cf2sfile (Open p f' flags fd' opt # s) f'" + using sf_cons ev by auto + moreover have "sectxt_of_obj (enrich_msgq s q q') (O_proc p) = sectxt_of_obj s (O_proc p)" + apply (rule curpsec) + using os ev curq_cons + by (auto split:option.splits) + ultimately show ?thesis + using ev True a1 a1' vd_enrich_cons vd_cons' + apply (simp add:cfd2sfd_open sectxt_of_obj_simps del:file_of_proc_fd.simps) + done + qed + qed + show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" + apply (case_tac e) + prefer 6 apply (erule b1) + using a1' a1 vd_enrich_cons vd_cons' curq_cons + apply (simp_all only:cfd2sfd_simps enrich_msgq.simps) + apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits) + done + qed + + thm psec_cons + thm cp2sproc_def + have pfds_cons: "\ tp. tp \ current_procs (e # s) \ + cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp" + apply (auto simp add:cpfd2sfds_def) + sorry + + have "\tp fd. fd \ proc_file_fds (e # s) tp \ cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd" + by (auto simp:proc_file_fds_def elim!:sfd_cons) + moreover + have "\tp. tp \ current_procs (e # s) \ cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp" + apply (auto simp:cp2sproc_def pfds_cons psec_cons split:option.splits) + sorry + moreover + have "\tq. tq \ current_msgqs (e # s) \ cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq" + sorry + moreover + have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q" + sorry + ultimately show ?case using vd_enrich_cons sf_cons + by auto +qed + + +thm cp2sproc_def + (* enrich s target_proc duplicated_pro *) fun enrich_proc :: "t_state \ t_process \ t_process \ nat \ t_state" where