diff -r f27ba31b7e96 -r 6f7b9039715f no_shm_selinux/Proc_fd_of_file_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/no_shm_selinux/Proc_fd_of_file_prop.thy	Tue Dec 17 13:30:21 2013 +0800
@@ -0,0 +1,155 @@
+theory Proc_fd_of_file_prop
+imports Main Flask Flask_type Valid_prop Current_files_prop Current_sockets_prop
+begin
+
+context flask begin
+
+lemma proc_fd_in_procs: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk>  \<Longrightarrow> p \<in> current_procs \<tau>"
+apply (induct \<tau> arbitrary: f) defer
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:file_of_proc_fd.simps current_procs.simps os_grant.simps split:if_splits option.splits)
+by (drule init_filefd_valid, simp)
+
+lemma proc_fd_in_fds_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> fd \<in> current_proc_fds \<tau> p"
+apply (induct \<tau>)
+apply (simp add:file_of_proc_fd.simps current_proc_fds.simps)
+apply (clarify, drule init_filefd_valid, simp)
+apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:file_of_proc_fd.simps current_proc_fds.simps split:if_splits option.splits t_sock_addr.splits)
+done
+
+lemma proc_fd_in_fds: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p"
+by (rule proc_fd_in_fds_aux[rule_format], simp+)
+
+lemma proc_fd_file_in_cur: "\<lbrakk>(p, fd) \<in> proc_fd_of_file \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (auto simp:proc_fd_of_file_def intro:file_of_pfd_in_current)
+
+lemma proc_fd_file_in_cur': "\<lbrakk>proc_fd_of_file \<tau> f \<noteq> {}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (auto simp:proc_fd_file_in_cur)
+
+lemma proc_fd_file_in_cur'': "\<lbrakk>proc_fd_of_file \<tau> f = {(p,fd)}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (auto simp:proc_fd_file_in_cur')
+
+lemma procfd_of_file_imp_fpfd: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"
+by (auto simp:proc_fd_of_file_def)
+
+lemma procfd_of_file_imp_fpfd': "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd \<noteq> None"
+by (auto simp:proc_fd_of_file_def)
+
+lemma procfd_of_file_eq_fpfd'': "(p, fd) \<in> proc_fd_of_file \<tau> f = (file_of_proc_fd \<tau> p fd = Some f)"
+by (auto simp:proc_fd_of_file_def)
+
+lemma procfd_of_file_non_empty: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> proc_fd_of_file \<tau> f \<noteq> {}"
+by (auto simp:proc_fd_of_file_def)
+
+lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')
+
+lemma file_fds_subset_pfds:
+  "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p"
+by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)
+
+lemma filefd_socket_conflict:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; (p, fd) \<in> current_sockets s; valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s arbitrary:p)
+apply (simp add:current_sockets_simps init_filefd_prop8)
+apply (frule vt_grant_os, frule vd_cons, frule file_fds_subset_pfds, case_tac a)
+apply (auto simp:current_sockets_simps split:if_splits option.splits 
+            dest:cn_in_curp cn_in_curfd proc_fd_in_fds)
+done
+
+lemma is_tcp_in_current: "is_tcp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"
+by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)
+
+lemma is_udp_in_current: "is_udp_sock s sock \<Longrightarrow> sock \<in> current_sockets s"
+by (auto simp:is_udp_sock_def current_sockets_def split:option.splits)
+
+lemma tcp_not_file_fd:
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (drule is_tcp_in_current)
+apply (drule filefd_socket_conflict, simp+)
+done
+
+lemma udp_not_file_fd:
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd", simp)
+apply (drule is_udp_in_current)
+apply (drule filefd_socket_conflict, simp+)
+done
+
+lemma tcp_notin_file_fds:
+  "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+by (auto simp:proc_file_fds_def intro:tcp_not_file_fd)
+
+lemma udp_notin_file_fds:
+  "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+by (auto simp:proc_file_fds_def intro:udp_not_file_fd)
+
+(******************* rebuild proc_fd_of_file simpset ***********************)
+(*
+lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> 
+  proc_fd_of_file (Open p f flags fd iopt # \<tau>) f' = (if (f' = f) then insert (p, fd) (proc_fd_of_file \<tau> f') else proc_fd_of_file \<tau> f')"
+apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)
+apply (frule vd_cons, drule vt_grant_os, case_tac iopt)
+apply (drule proc_fd_in_fds, simp, simp add:os_grant.simps nfd_notin_curfd)+
+done
+
+lemma proc_fd_of_file_closefd: "proc_fd_of_file (CloseFd p fd # \<tau>) f = (if (file_of_proc_fd \<tau> p fd = Some f) then (proc_fd_of_file \<tau> f - {(p,fd)}) else proc_fd_of_file \<tau> f) "
+by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)
+
+lemma proc_fd_of_file_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow> 
+  proc_fd_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (if (f\<^isub>3 \<preceq> f) then proc_fd_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) else proc_fd_of_file \<tau> f)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "f\<^isub>3 \<preceq> f")
+apply (subgoal_tac "f \<notin> current_files \<tau>") prefer 2 apply (rule notI)
+apply (clarsimp simp:os_grant.simps, drule_tac f = f\<^isub>3 and f' = f in ancenf_in_current, simp, simp, simp)
+apply (auto simp add:proc_fd_of_file_def)[1]
+
+apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
+apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = aa and f\<^isub>2 = f\<^isub>2 in file_renaming_prop5, simp)
+apply (drule file_of_pfd_in_current, simp+)
+apply (simp add:file_of_proc_fd.simps)
+apply (rule conjI, rule impI, simp add:file_renaming_prop5')
+apply (rule impI, simp add:file_before_rename_def)
+
+apply (simp add:proc_fd_of_file_def split:if_splits)
+apply auto
+apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
+apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>2 = f\<^isub>2 and f = aa in file_renaming_prop1, simp)
+apply (simp add:current_files_simps)
+apply (erule exE| erule conjE)+
+apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
+apply (drule_tac f = f\<^isub>1 in rename_renaming_decom', simp+)
+apply (simp add:file_after_rename_def)
+done
+
+
+lemma proc_fd_of_file_kill: "proc_fd_of_file (Kill p\<^isub>1 p\<^isub>2 # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p\<^isub>2}"
+by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+
+lemma proc_fd_of_file_exit: "proc_fd_of_file (Exit p' # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p'}"
+by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+
+lemma proc_fd_of_file_clone: "Clone p\<^isub>1 p\<^isub>2 # valid \<tau> \<Longrightarrow> proc_fd_of_file (Clone p\<^isub>1 p\<^isub>2 # \<tau>) f = proc_fd_of_file \<tau> f \<union> {(p\<^isub>2, fd)| fd. (p\<^isub>1, fd) \<in> proc_fd_of_file \<tau> f}" 
+apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+apply (frule vd_cons, drule vt_grant_os)
+apply (drule proc_fd_in_procs, (simp add:os_grant.simps np_notin_curp)+)
+done
+
+lemma proc_fd_of_file_other: "\<lbrakk>e # valid \<tau>;
+                               \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+                               \<forall> p fd. e \<noteq> CloseFd p fd;
+                               \<forall> p f f'. e \<noteq> Rename p f f';
+                               \<forall> p p'. e \<noteq> Kill p p';
+                               \<forall> p. e \<noteq> Exit p;
+                               \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> proc_fd_of_file (e # \<tau>) f = proc_fd_of_file \<tau> f"
+apply (case_tac e, auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+done
+
+lemmas proc_fd_of_file_simps = proc_fd_of_file_open proc_fd_of_file_closefd proc_fd_of_file_rename proc_fd_of_file_kill proc_fd_of_file_exit proc_fd_of_file_clone proc_fd_of_file_other
+*)
+end
+
+
+end
\ No newline at end of file