47 |
47 |
48 lemma file_fds_subset_pfds: |
48 lemma file_fds_subset_pfds: |
49 "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p" |
49 "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p" |
50 by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds) |
50 by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds) |
51 |
51 |
52 lemma tcp_filefd_conflict: |
52 lemma filefd_socket_conflict: |
53 "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False" |
53 "\<lbrakk>file_of_proc_fd s p fd = Some f; (p, fd) \<in> current_sockets s; valid s\<rbrakk> \<Longrightarrow> False" |
54 apply (induct s, simp) |
54 apply (induct s arbitrary:p) |
55 apply (auto simp:is_tcp_sock_simps) |
55 apply (simp add:current_sockets_simps init_filefd_prop8) |
|
56 apply (frule vt_grant_os, frule vd_cons, frule file_fds_subset_pfds, case_tac a) |
|
57 apply (auto simp:current_sockets_simps split:if_splits option.splits |
|
58 dest:cn_in_curp cn_in_curfd proc_fd_in_fds) |
|
59 done |
56 |
60 |
|
61 lemma is_tcp_in_current: "is_tcp_sock s sock \<Longrightarrow> sock \<in> current_sockets s" |
|
62 by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits) |
|
63 |
|
64 lemma is_udp_in_current: "is_udp_sock s sock \<Longrightarrow> sock \<in> current_sockets s" |
|
65 by (auto simp:is_udp_sock_def current_sockets_def split:option.splits) |
57 |
66 |
58 lemma tcp_not_file_fd: |
67 lemma tcp_not_file_fd: |
59 "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p" |
68 "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None" |
60 apply (auto simp:proc_file_fds_def) |
69 apply (case_tac "file_of_proc_fd s p fd", simp) |
|
70 apply (drule is_tcp_in_current) |
|
71 apply (drule filefd_socket_conflict, simp+) |
|
72 done |
61 |
73 |
62 lemma udp_not_file_fd: |
74 lemma udp_not_file_fd: |
|
75 "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None" |
|
76 apply (case_tac "file_of_proc_fd s p fd", simp) |
|
77 apply (drule is_udp_in_current) |
|
78 apply (drule filefd_socket_conflict, simp+) |
|
79 done |
|
80 |
|
81 lemma tcp_notin_file_fds: |
|
82 "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p" |
|
83 by (auto simp:proc_file_fds_def intro:tcp_not_file_fd) |
|
84 |
|
85 lemma udp_notin_file_fds: |
63 "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p" |
86 "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p" |
64 |
87 by (auto simp:proc_file_fds_def intro:udp_not_file_fd) |
65 lemma |
|
66 |
88 |
67 (******************* rebuild proc_fd_of_file simpset ***********************) |
89 (******************* rebuild proc_fd_of_file simpset ***********************) |
68 (* |
90 (* |
69 lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> |
91 lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> |
70 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')" |
92 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')" |