--- a/Alive_prop.thy Wed Nov 20 15:19:58 2013 +0800
+++ b/Alive_prop.thy Wed Nov 20 16:24:16 2013 +0800
@@ -109,9 +109,8 @@
apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
is_tcp_sock_simps is_udp_sock_simps
- dest:is_dir_in_current split:if_splits option.splits)
-apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto)
-
+ dest:is_dir_in_current split:if_splits option.splits
+ dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
done
lemma alive_clone:
@@ -121,21 +120,19 @@
| O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
else if (p'' = p') then False
else alive s obj
- | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
- else if (p'' = p') then False
- else alive s (O_tcp_sock (p'', fd)))
- | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
- else if (p'' = p') then False
- else alive s (O_udp_sock (p'', fd)))
+ | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False
+ else alive s (O_tcp_sock (p'', fd)))
+ | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False
+ else alive s (O_udp_sock (p'', fd)))
| _ \<Rightarrow> alive s obj )"
apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
is_tcp_sock_simps is_udp_sock_simps
intro:is_tcp_in_current is_udp_in_current
- dest:is_dir_in_current split:if_splits option.splits)
+ dest:is_dir_in_current split:if_splits option.splits
+ dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
done
-
lemma alive_kill:
"valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (
\<lambda> obj. case obj of
--- a/Init_prop.thy Wed Nov 20 15:19:58 2013 +0800
+++ b/Init_prop.thy Wed Nov 20 16:24:16 2013 +0800
@@ -66,6 +66,9 @@
apply (case_tac s, auto)
done
+lemma init_socket_prop6: "(p, fd) \<in> init_sockets \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest: init_socket_has_inode)
+
lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5
lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files"
@@ -114,8 +117,12 @@
by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
dest:init_socket_has_inode inos_has_sock_tag)
+lemma is_init_udp_sock_prop5:
+ "is_init_udp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_udp_sock_prop1 intro:init_socket_prop6)
+
lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3
- is_init_udp_sock_prop4
+ is_init_udp_sock_prop4 is_init_udp_sock_prop5
lemma is_tcp_sock_nil:
"is_tcp_sock [] k = is_init_tcp_sock k"
@@ -141,8 +148,12 @@
by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
dest:init_socket_has_inode inos_has_sock_tag)
+lemma is_init_tcp_sock_prop5:
+ "is_init_tcp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_tcp_sock_prop1 intro:init_socket_prop6)
+
lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3
- is_init_tcp_sock_prop4
+ is_init_tcp_sock_prop4 is_init_tcp_sock_prop5
lemma init_parent_file_prop1:
"\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"
@@ -221,7 +232,16 @@
lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"
by (auto dest:init_filefd_valid simp:is_init_file_def)
-lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5
+lemma init_filefd_prop6: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_tcp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_tcp_sock_prop1)
+
+lemma init_filefd_prop7: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_udp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_udp_sock_prop1)
+
+lemma init_filefd_prop8: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> (p, fd) \<notin> init_sockets"
+by (auto dest!:init_filefd_valid)
+
+lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5 init_filefd_prop6 init_filefd_prop7 init_filefd_prop8
lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"
by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)
--- a/Proc_fd_of_file_prop.thy Wed Nov 20 15:19:58 2013 +0800
+++ b/Proc_fd_of_file_prop.thy Wed Nov 20 16:24:16 2013 +0800
@@ -49,20 +49,42 @@
"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 tcp_filefd_conflict:
- "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False"
-apply (induct s, simp)
-apply (auto simp:is_tcp_sock_simps)
+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> fd \<notin> proc_file_fds s p"
-apply (auto simp:proc_file_fds_def)
+ "\<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> fd \<notin> proc_file_fds s p"
+ "\<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
+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 ***********************)
(*