# HG changeset patch
# User chunhan
# Date 1370331469 -28800
# Node ID 570f90f175eec2ef94d5caa1124c42c6976e8ef7
# Parent c8b7c24f1db6dae3dc23fc0b2755fa9b15dc8e45
updated
diff -r c8b7c24f1db6 -r 570f90f175ee Co2sobj_prop.thy
--- a/Co2sobj_prop.thy Mon Jun 03 14:18:14 2013 +0800
+++ b/Co2sobj_prop.thy Tue Jun 04 15:37:49 2013 +0800
@@ -1102,43 +1102,210 @@
(******** cp2sproc simpset *********)
-lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"
-apply (simp add:cp2sproc_def)
-by (simp add:cp2sproc_def index_of_proc.simps)
+lemma not_init_intro_proc: (*???*)
+ "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
+using not_deleted_init_proc by auto
+
+lemma not_init_intro_proc': (*???*)
+ "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
+using not_deleted_init_proc by auto
+
+lemma cp2sproc_clone:
+ "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' :=
+ case (sectxt_of_obj s (O_proc p)) of
+ Some sec \<Rightarrow> Some (Created, sec,
+ {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd},
+ {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag})
+ | _ \<Rightarrow> None)"
+apply (frule cph2spshs_clone, frule cpfd2sfds_clone)
+apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps)
+apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec'
+ dest:current_proc_has_sec split:option.splits if_splits)
+done
+
+lemma cp2sproc_other:
+ "\<lbrakk>valid (e # s);
+ \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p h flag. e \<noteq> Attach p h flag;
+ \<forall> p h. e \<noteq> Detach p h;
+ \<forall> p h. e \<noteq> DeleteShM p h;
+ \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ \<forall> p f fds. e \<noteq> Execve p f fds;
+ \<forall> p p'. e \<noteq> Kill p p';
+ \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cp2sproc (e # s) = cp2sproc s"
+apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+)
+apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec'
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
-lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"
-by (simp add:cp2sproc_nil current_procs.simps)
+lemma cp2sproc_open:
+ "valid (Open p f flags fd opt # s) \<Longrightarrow>
+ cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p :=
+ case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd),
+ cf2sfile (Open p f flags fd opt # s) f) of
+ (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
+ then Init p else Created, sec,
+ (cpfd2sfds s p) \<union> {(fdsec, flags, sf)}, cph2spshs s p)
+ | _ \<Rightarrow> None)"
+apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
+apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p")
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_closefd:
+ "valid (CloseFd p fd # s) \<Longrightarrow>
+ cp2sproc (CloseFd p fd # s) = (cp2sproc s) (p :=
+ if (fd \<in> proc_file_fds s p)
+ then (case (cfd2sfd s p fd) of
+ Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)
+ then cp2sproc s p
+ else (case (sectxt_of_obj s (O_proc p)) of
+ Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
+ then Init p else Created,
+ sec, cpfd2sfds s p - {sfd}, cph2spshs s p)
+ | _ \<Rightarrow> None))
+ | _ \<Rightarrow> cp2sproc s p)
+ else cp2sproc s p)"
+apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p")
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
-lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = (
- if (p'' = p') then SCrea (Suc (length \<tau>))
- else cp2sproc \<tau> p'' )"
-by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
+lemma cp2sproc_attach:
+ "valid (Attach p h flag # s) \<Longrightarrow>
+ cp2sproc (Attach p h flag # s) = (cp2sproc s) (p :=
+ (case (ch2sshm s h) of
+ Some sh \<Rightarrow> (case (sectxt_of_obj s (O_proc p)) of
+ Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
+ then Init p else Created,
+ sec, cpfd2sfds s p, cph2spshs s p \<union> {(sh, flag)})
+ | _ \<Rightarrow> None)
+ | _ \<Rightarrow> cp2sproc s p) )"
+apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p")
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_detach:
+ "valid (Detach p h # s) \<Longrightarrow>
+ cp2sproc (Detach p h # s) = (cp2sproc s) (p :=
+ (case (ch2sshm s h, flag_of_proc_shm s p h) of
+ (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
+ then cp2sproc s p
+ else (case (sectxt_of_obj s (O_proc p)) of
+ Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)
+ then Init p else Created, sec,
+ cpfd2sfds s p, cph2spshs s p - {(sh, flag)})
+ | None \<Rightarrow> None)
+ | _ \<Rightarrow> cp2sproc s p) )"
+apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p")
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
-lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''"
-apply (case_tac e)
-by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
+lemma cp2sproc_deleteshm:
+ "valid (DeleteShM p h # s) \<Longrightarrow>
+ cp2sproc (DeleteShM p h # s) = (\<lambda> p'.
+ (case (ch2sshm s h, flag_of_proc_shm s p' h) of
+ (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
+ then cp2sproc s p'
+ else (case (sectxt_of_obj s (O_proc p')) of
+ Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p') s \<and> p' \<in> init_procs)
+ then Init p' else Created, sec,
+ cpfd2sfds s p', cph2spshs s p' - {(sh, flag)})
+ | None \<Rightarrow> None)
+ | _ \<Rightarrow> cp2sproc s p') )"
+apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow>
+ cp2sproc (Execve p f fds # s) = (cp2sproc s) (p :=
+ (case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of
+ Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
+ {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, {})
+ | _ \<Rightarrow> None) )"
+apply (frule cph2spshs_execve, frule cpfd2sfds_execve)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
-lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other
+lemma cp2sproc_kill:
+ "\<lbrakk>valid (Kill p p' # s); p'' \<noteq> p'\<rbrakk> \<Longrightarrow>
+ cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
+apply (frule cph2spshs_kill, frule cpfd2sfds_kill)
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_kill':
+ "\<lbrakk>valid (Kill p p' # s); p'' \<in> current_procs (Kill p p' # s)\<rbrakk> \<Longrightarrow>
+ cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
+by (drule_tac p'' = p'' in cp2sproc_kill, simp+)
+
+lemma cp2sproc_exit:
+ "\<lbrakk>valid (Exit p # s); p' \<noteq> p\<rbrakk> \<Longrightarrow>
+ cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
+apply (frule cph2spshs_exit, frule cpfd2sfds_exit)
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps
+ dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_exit':
+ "\<lbrakk>valid (Exit p # s); p' \<in> current_procs (Exit p # s)\<rbrakk> \<Longrightarrow>
+ cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
+by (drule_tac p'= p' in cp2sproc_exit, simp+)
+
+lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
+ cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other
(********************* cm2smsg simpset ***********************)
-lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"
-by (simp add:cm2smsg_def index_of_msg.simps)
-
-lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m"
-by (simp add:cm2smsg_nil current_msgs.simps)
-
-lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')"
-by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps)
-
-lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"
+lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
+apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
apply (case_tac e)
-by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits)
lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+(********************* cq2smsgq simpset ***********************)
+
+lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"
+apply (case_tac e)
+by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)
+
+lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+
+
+
+
end
(*<*)