|
1 theory Current_sockets_prop |
|
2 imports Main Flask Flask_type Current_files_prop |
|
3 begin |
|
4 |
|
5 context flask begin |
|
6 |
|
7 lemma cn_in_curp: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> p \<in> current_procs \<tau>" |
|
8 apply (induct \<tau>) defer |
|
9 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
10 apply (auto simp:current_sockets_def inum_of_socket.simps current_procs.simps os_grant.simps split:if_splits option.splits |
|
11 dest:inos_has_sock_tag init_socket_has_inode) |
|
12 done |
|
13 |
|
14 lemma cn_in_curfd_aux: "\<forall> p. (p, fd) \<in> current_sockets \<tau> \<and> valid \<tau> \<longrightarrow> fd \<in> current_proc_fds \<tau> p" |
|
15 apply (induct \<tau>) defer |
|
16 apply (rule allI, rule impI, erule conjE, frule vd_cons, frule vt_grant_os, case_tac a) |
|
17 apply (auto simp:current_sockets_def current_proc_fds.simps os_grant.simps inum_of_socket.simps |
|
18 split:if_splits option.splits t_socket_af.splits dest:inos_has_sock_tag init_socket_has_inode) |
|
19 done |
|
20 |
|
21 lemma cn_in_curfd: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p" |
|
22 by (simp add:cn_in_curfd_aux) |
|
23 |
|
24 lemma cn_in_curfd': "\<lbrakk>inum_of_socket \<tau> (p, fd) = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p" |
|
25 by (rule cn_in_curfd, simp_all add:current_sockets_def) |
|
26 |
|
27 lemma cn_in_curp': "\<lbrakk>inum_of_socket \<tau> (p, fd) = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> p \<in> current_procs \<tau>" |
|
28 apply (rule cn_in_curp) |
|
29 by (auto simp:current_sockets_def) |
|
30 |
|
31 (***************** current_sockets simpset *****************) |
|
32 |
|
33 lemma current_sockets_nil: "current_sockets [] = init_sockets" |
|
34 apply (simp add:current_sockets_def inum_of_socket.simps) |
|
35 using init_socket_has_inode inos_has_sock_tag |
|
36 by auto |
|
37 |
|
38 lemma current_sockets_closefd: "current_sockets (CloseFd p fd # \<tau>) = current_sockets \<tau> - {(p, fd)}" |
|
39 by (auto simp add:current_sockets_def inum_of_socket.simps) |
|
40 |
|
41 lemma current_sockets_createsock: "current_sockets (CreateSock p aft st fd ino # \<tau>) = insert (p, fd) (current_sockets \<tau>)" |
|
42 by (auto simp add:current_sockets_def inum_of_socket.simps) |
|
43 |
|
44 lemma current_sockets_accept: "current_sockets (Accept p fd addr lport' fd' ino # \<tau>) = insert (p, fd') (current_sockets \<tau>)" |
|
45 by (auto simp add:current_sockets_def inum_of_socket.simps) |
|
46 |
|
47 lemma current_sockets_clone: "valid (Clone p p' fds # \<tau>) |
|
48 \<Longrightarrow> current_sockets (Clone p p' fds # \<tau>) = |
|
49 current_sockets \<tau> \<union> {(p', fd)| fd. (p, fd) \<in> current_sockets \<tau> \<and> fd \<in> fds}" |
|
50 apply (frule vd_cons, drule vt_grant_os) |
|
51 apply (auto simp add:os_grant.simps current_sockets_def inum_of_socket.simps split:if_splits |
|
52 dest:cn_in_curp') |
|
53 done |
|
54 |
|
55 lemma current_sockets_execve: "valid (Execve p f fds # \<tau>) |
|
56 \<Longrightarrow> current_sockets (Execve p f fds # \<tau>) = |
|
57 current_sockets \<tau> - {(p, fd)| fd. (p, fd) \<in> current_sockets \<tau> \<and> fd \<notin> fds}" |
|
58 apply (frule vd_cons, drule vt_grant_os) |
|
59 apply (auto simp add:os_grant.simps current_sockets_def inum_of_socket.simps split:if_splits |
|
60 dest:cn_in_curp') |
|
61 done |
|
62 |
|
63 lemma current_sockets_kill: "current_sockets (Kill p p' # \<tau>) = current_sockets \<tau> - {(p', fd)| fd. (p', fd) \<in> current_sockets \<tau>}" |
|
64 by (auto simp add:current_sockets_def inum_of_socket.simps split:if_splits) |
|
65 |
|
66 lemma current_sockets_exit: "current_sockets (Exit p # \<tau>) = current_sockets \<tau> - {(p, fd)| fd. (p, fd) \<in> current_sockets \<tau>}" |
|
67 by (auto simp add:current_sockets_def inum_of_socket.simps split:if_splits) |
|
68 |
|
69 lemma current_sockets_other: |
|
70 "\<lbrakk>\<forall> p fd. e \<noteq> CloseFd p fd; |
|
71 \<forall> p aft st fd ino. e \<noteq> CreateSock p aft st fd ino; |
|
72 \<forall> p fd addr lport' fd' ino. e \<noteq> Accept p fd addr lport' fd' ino; |
|
73 \<forall> p p' fds. e \<noteq> Clone p p' fds; |
|
74 \<forall> p f fds. e \<noteq> Execve p f fds; |
|
75 \<forall> p p'. e \<noteq> Kill p p'; |
|
76 \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> current_sockets (e # \<tau>) = current_sockets \<tau>" |
|
77 apply (case_tac e) |
|
78 by (auto simp add:current_sockets_def inum_of_socket.simps split:if_splits) |
|
79 |
|
80 lemmas current_sockets_simps = current_sockets_nil current_sockets_closefd current_sockets_createsock |
|
81 current_sockets_accept current_sockets_execve current_sockets_clone |
|
82 current_sockets_kill current_sockets_exit current_sockets_other |
|
83 |
|
84 (********** is_tcp_sock simpset ***************) |
|
85 |
|
86 lemma is_tcp_sock_nil: |
|
87 "is_tcp_sock [] = is_init_tcp_sock" |
|
88 apply (rule ext) |
|
89 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
|
90 dest:init_socket_has_inode split:option.splits) |
|
91 done |
|
92 |
|
93 lemma is_tcp_sock_closefd: |
|
94 "is_tcp_sock (CloseFd p fd # s) = (is_tcp_sock s) ((p, fd) := False)" |
|
95 apply (rule ext) |
|
96 by (auto simp add:is_tcp_sock_def inum_of_socket.simps split:option.splits t_inode_tag.splits) |
|
97 |
|
98 lemma is_tcp_sock_createsock: |
|
99 "valid (CreateSock p af st fd ino # s) \<Longrightarrow> is_tcp_sock (CreateSock p af st fd ino # s) = ( |
|
100 case st of |
|
101 STREAM \<Rightarrow> (is_tcp_sock s) ((p, fd) := True) |
|
102 | _ \<Rightarrow> is_tcp_sock s )" |
|
103 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
104 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
105 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
106 |
|
107 lemma is_tcp_sock_accept: |
|
108 "valid (Accept p fd addr lport fd' ino # s) |
|
109 \<Longrightarrow> is_tcp_sock (Accept p fd addr lport fd' ino # s) = (is_tcp_sock s) ((p,fd') := True)" |
|
110 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
111 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
112 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
113 |
|
114 lemma is_tcp_sock_execve: |
|
115 "valid (Execve p f fds # s) \<Longrightarrow> is_tcp_sock (Execve p f fds # s) = ( |
|
116 \<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then is_tcp_sock s (p, fd) |
|
117 else if (p' = p) then False |
|
118 else is_tcp_sock s (p', fd))" |
|
119 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
120 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
121 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
122 |
|
123 lemma is_tcp_sock_clone: |
|
124 "valid (Clone p p' fds # s) \<Longrightarrow> is_tcp_sock (Clone p p' fds # s) = ( |
|
125 \<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then is_tcp_sock s (p, fd) |
|
126 else if (p'' = p') then False |
|
127 else is_tcp_sock s (p'', fd))" |
|
128 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
129 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
130 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
131 |
|
132 lemma is_tcp_sock_kill: |
|
133 "valid (Kill p p' # s) \<Longrightarrow> is_tcp_sock (Kill p p' # s) = ( |
|
134 \<lambda> (p'', fd). if (p'' = p') then False |
|
135 else is_tcp_sock s (p'', fd))" |
|
136 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
137 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
138 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
139 |
|
140 lemma is_tcp_sock_exit: |
|
141 "valid (Exit p # s) \<Longrightarrow> is_tcp_sock (Exit p # s) = ( |
|
142 \<lambda> (p', fd). if (p' = p) then False |
|
143 else is_tcp_sock s (p', fd))" |
|
144 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
145 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
146 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
147 |
|
148 lemma is_tcp_sock_other: |
|
149 "\<lbrakk>valid (e # \<tau>); |
|
150 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
151 \<forall> p aft st fd ino. e \<noteq> CreateSock p aft st fd ino; |
|
152 \<forall> p fd addr lport' fd' ino. e \<noteq> Accept p fd addr lport' fd' ino; |
|
153 \<forall> p p' fds. e \<noteq> Clone p p' fds; |
|
154 \<forall> p f fds. e \<noteq> Execve p f fds; |
|
155 \<forall> p p'. e \<noteq> Kill p p'; |
|
156 \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> is_tcp_sock (e # \<tau>) = is_tcp_sock \<tau>" |
|
157 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x, case_tac e) |
|
158 prefer 6 apply (case_tac option) |
|
159 by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
160 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
161 |
|
162 lemmas is_tcp_sock_simps = is_tcp_sock_nil is_tcp_sock_closefd is_tcp_sock_createsock is_tcp_sock_accept |
|
163 is_tcp_sock_clone is_tcp_sock_execve is_tcp_sock_kill is_tcp_sock_exit is_tcp_sock_other |
|
164 |
|
165 |
|
166 (************ is_udp_sock simpset *************) |
|
167 |
|
168 lemma is_udp_sock_nil: |
|
169 "is_udp_sock [] = is_init_udp_sock" |
|
170 apply (rule ext) |
|
171 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
|
172 dest:init_socket_has_inode split:option.splits) |
|
173 done |
|
174 |
|
175 lemma is_udp_sock_closefd: |
|
176 "is_udp_sock (CloseFd p fd # s) = (is_udp_sock s) ((p, fd) := False)" |
|
177 apply (rule ext) |
|
178 by (auto simp add:is_udp_sock_def inum_of_socket.simps split:option.splits t_inode_tag.splits) |
|
179 |
|
180 lemma is_udp_sock_createsock: |
|
181 "valid (CreateSock p af st fd ino # s) \<Longrightarrow> is_udp_sock (CreateSock p af st fd ino # s) = ( |
|
182 case st of |
|
183 DGRAM \<Rightarrow> (is_udp_sock s) ((p, fd) := True) |
|
184 | _ \<Rightarrow> is_udp_sock s )" |
|
185 apply (frule vd_cons, frule vt_grant_os, rule ext) |
|
186 by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
187 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
188 |
|
189 lemma is_udp_sock_execve: |
|
190 "valid (Execve p f fds # s) \<Longrightarrow> is_udp_sock (Execve p f fds # s) = ( |
|
191 \<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then is_udp_sock s (p, fd) |
|
192 else if (p' = p) then False |
|
193 else is_udp_sock s (p', fd))" |
|
194 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
195 by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
196 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
197 |
|
198 lemma is_udp_sock_clone: |
|
199 "valid (Clone p p' fds # s) \<Longrightarrow> is_udp_sock (Clone p p' fds # s) = ( |
|
200 \<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then is_udp_sock s (p, fd) |
|
201 else if (p'' = p') then False |
|
202 else is_udp_sock s (p'', fd))" |
|
203 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
204 by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
205 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
206 |
|
207 lemma is_udp_sock_kill: |
|
208 "valid (Kill p p' # s) \<Longrightarrow> is_udp_sock (Kill p p' # s) = ( |
|
209 \<lambda> (p'', fd). if (p'' = p') then False |
|
210 else is_udp_sock s (p'', fd))" |
|
211 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
212 by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
213 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
214 |
|
215 lemma is_udp_sock_exit: |
|
216 "valid (Exit p # s) \<Longrightarrow> is_udp_sock (Exit p # s) = ( |
|
217 \<lambda> (p', fd). if (p' = p) then False |
|
218 else is_udp_sock s (p', fd))" |
|
219 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x) |
|
220 by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
221 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
222 |
|
223 lemma is_udp_sock_other: |
|
224 "\<lbrakk>valid (e # \<tau>); |
|
225 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
226 \<forall> p aft st fd ino. e \<noteq> CreateSock p aft st fd ino; |
|
227 \<forall> p p' fds. e \<noteq> Clone p p' fds; |
|
228 \<forall> p f fds. e \<noteq> Execve p f fds; |
|
229 \<forall> p p'. e \<noteq> Kill p p'; |
|
230 \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> is_udp_sock (e # \<tau>) = is_udp_sock \<tau>" |
|
231 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x, case_tac e) |
|
232 prefer 6 apply (case_tac option) |
|
233 by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd' |
|
234 split:option.splits t_inode_tag.splits t_socket_type.splits) |
|
235 |
|
236 lemmas is_udp_sock_simps = is_udp_sock_nil is_udp_sock_closefd is_udp_sock_createsock |
|
237 is_udp_sock_clone is_udp_sock_execve is_udp_sock_kill is_udp_sock_exit is_udp_sock_other |
|
238 |
|
239 lemma update_with_shuthow_someI: "socket_in_trans \<tau> s \<Longrightarrow> \<exists> st'. update_with_shuthow (socket_state \<tau> s) how = Some st'" |
|
240 apply (case_tac "socket_state \<tau> s", simp add:socket_in_trans_def, case_tac a) |
|
241 apply (auto simp:update_with_shuthow.simps socket_in_trans_def split:option.splits) |
|
242 apply (case_tac t_sock_trans_state, case_tac [!] how) |
|
243 by auto |
|
244 |
|
245 lemma is_tcp_sock_imp_curernt_proc: |
|
246 "\<lbrakk>is_tcp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
247 apply (induct s) |
|
248 apply (simp add:is_tcp_sock_nil is_init_tcp_sock_prop3) |
|
249 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
250 by (auto simp:is_tcp_sock_simps split:if_splits option.splits t_socket_type.splits) |
|
251 |
|
252 lemma is_udp_sock_imp_curernt_proc: |
|
253 "\<lbrakk>is_udp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
254 apply (induct s) |
|
255 apply (simp add:is_udp_sock_nil is_init_udp_sock_prop3) |
|
256 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
257 by (auto simp:is_udp_sock_simps split:if_splits option.splits t_socket_type.splits) |
|
258 |
|
259 |
|
260 (***** below should be adjusted after starting static analysis of sockets ! ??? ****) |
|
261 |
|
262 (* |
|
263 lemma cn_has_sockstate: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> socket_state \<tau> (p, fd) \<noteq> None" |
|
264 apply (induct \<tau> arbitrary: p) using init_socket_has_state |
|
265 apply (simp add:current_sockets_simps socket_state.simps bidirect_in_init_def) |
|
266 |
|
267 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
268 apply (auto simp:current_sockets_simps os_grant.simps socket_state.simps intro:update_with_shuthow_someI dest:cn_no_newproc' split:option.splits) |
|
269 done |
|
270 |
|
271 lemma after_bind_update: "\<lbrakk>after_bind (update_with_shuthow (socket_state \<tau> s) t_shutdown_how); valid \<tau>\<rbrakk> \<Longrightarrow> after_bind (socket_state \<tau> s)" |
|
272 apply (case_tac "socket_state \<tau> s", simp, case_tac a) |
|
273 apply (auto simp:update_with_shuthow.simps split:option.splits) |
|
274 done |
|
275 |
|
276 lemma after_bind_has_laddr_aux: "\<forall> p fd. after_bind (socket_state \<tau> (p, fd)) \<and> valid \<tau> \<longrightarrow> (\<exists> ip port. local_addr \<tau> (p, fd) = Some (INET_ADDR ip port))" |
|
277 apply (induct \<tau>) |
|
278 apply (clarsimp simp add:socket_state.simps local_addr.simps) |
|
279 apply (drule init_socket_has_laddr, simp, erule exE) |
|
280 apply (case_tac y, simp) |
|
281 |
|
282 apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a) |
|
283 apply (auto simp:socket_state.simps local_addr.simps os_grant.simps dest:after_bind_update split:if_splits option.splits t_sock_addr.splits) |
|
284 apply (erule_tac x = nat1 in allE, erule_tac x = nat2 in allE, erule impE, simp+) |
|
285 done |
|
286 |
|
287 lemma after_bind_has_laddr: "\<lbrakk>after_bind (socket_state \<tau> (p, fd)); valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> ip port. local_addr \<tau> (p, fd) = Some (INET_ADDR ip port)" |
|
288 by (rule after_bind_has_laddr_aux[rule_format], simp+) |
|
289 |
|
290 lemma after_bind_has_laddr': "\<lbrakk>after_bind (socket_state \<tau> s); valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> ip port. local_addr \<tau> s = Some (INET_ADDR ip port)" |
|
291 by (case_tac s, auto dest:after_bind_has_laddr) |
|
292 |
|
293 lemma after_bind_has_laddr_D: "\<lbrakk>local_addr \<tau> s = None; valid \<tau>\<rbrakk> \<Longrightarrow> \<not> after_bind (socket_state \<tau> s)" |
|
294 by (auto dest:after_bind_has_laddr') |
|
295 |
|
296 lemma local_addr_valid: "\<lbrakk>local_addr \<tau> (p, fd) = Some (INET_ADDR ip port); (p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> ip \<in> local_ipaddrs" |
|
297 apply (induct \<tau> arbitrary:p fd port) |
|
298 apply (simp add:local_addr.simps current_sockets_simps local_ip_valid) |
|
299 |
|
300 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
301 apply (auto simp:current_sockets_simps local_addr.simps os_grant.simps split:if_splits option.splits t_sock_addr.splits dest:cn_no_newproc' after_bind_has_laddr_D) |
|
302 done |
|
303 |
|
304 lemma local_addr_valid': "\<lbrakk>local_addr \<tau> s = Some (INET_ADDR ip port); s \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> ip \<in> local_ipaddrs" |
|
305 by (case_tac s, simp add:local_addr_valid) |
|
306 |
|
307 lemma local_ip_has_dev_D: "\<lbrakk>local_ip2dev ip = None; local_addr \<tau> s = Some (INET_ADDR ip port); s \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
|
308 using local_ip2dev_valid |
|
309 by (drule_tac local_addr_valid', simp+) |
|
310 |
|
311 lemma after_bind_has_netdev: "\<lbrakk>after_bind (socket_state \<tau> s); s \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> dev. netdev_of_socket \<tau> s = Some dev" |
|
312 apply (drule after_bind_has_laddr', simp, clarsimp) |
|
313 apply (frule local_addr_valid', simp+) |
|
314 apply (drule local_ip2dev_valid, simp add:netdev_of_socket_def) |
|
315 done |
|
316 |
|
317 lemma after_bind_has_netdev_D: "\<lbrakk>netdev_of_socket \<tau> s = None; s \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<not> after_bind (socket_state \<tau> s)" |
|
318 by (auto dest:after_bind_has_netdev) |
|
319 |
|
320 lemma after_conacc_update: "\<lbrakk>after_conacc (update_with_shuthow (socket_state \<tau> s) t_shutdown_how); valid \<tau>\<rbrakk> \<Longrightarrow> after_conacc (socket_state \<tau> s)" |
|
321 apply (case_tac "socket_state \<tau> s", simp, case_tac a) |
|
322 apply (auto simp:update_with_shuthow.simps split:option.splits) |
|
323 done |
|
324 |
|
325 lemma after_conacc_has_raddr: "\<lbrakk>after_conacc (socket_state \<tau> (p, fd)); valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> addr. remote_addr \<tau> (p, fd) = Some addr" |
|
326 apply (induct \<tau> arbitrary:p fd) |
|
327 apply (simp add:socket_state.simps local_addr.simps) using init_socket_has_raddr apply blast |
|
328 |
|
329 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
330 apply (auto simp:socket_state.simps local_addr.simps os_grant.simps dest:after_conacc_update split:if_splits option.splits t_sock_addr.splits) |
|
331 done |
|
332 |
|
333 lemma after_conacc_has_raddr': "\<lbrakk>after_conacc (socket_state \<tau> s); valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> addr. remote_addr \<tau> s = Some addr" |
|
334 by (case_tac s, auto dest:after_conacc_has_raddr) |
|
335 |
|
336 lemma after_conacc_has_raddr_D: "\<lbrakk>remote_addr \<tau> s = None; valid \<tau>\<rbrakk> \<Longrightarrow> \<not> after_conacc (socket_state \<tau> s)" |
|
337 by (auto dest:after_conacc_has_raddr') |
|
338 |
|
339 |
|
340 lemma cn_has_socktype: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> st. socket_type \<tau> (p, fd) = Some st" |
|
341 apply (induct \<tau> arbitrary:p fd) |
|
342 using init_socket_has_socktype |
|
343 apply (simp add:socket_type.simps current_sockets_nil bidirect_in_init_def) |
|
344 |
|
345 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
346 apply (auto simp:socket_type.simps current_sockets_simps os_grant.simps dest:cn_no_newproc' split:if_splits option.splits t_sock_addr.splits) |
|
347 done |
|
348 |
|
349 lemma accept_has_temps: "Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # valid \<tau> \<Longrightarrow> \<exists> temp. nettemp_of_socket (Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # \<tau>) (p, fd\<^isub>2) is_remote = Some temp" |
|
350 apply (frule vd_cons, frule vt_grant_os) |
|
351 apply (auto dest:cn_has_socktype simp:os_grant.simps nettemp_of_socket_def netdev_of_socket_def |
|
352 dest!:after_conacc_has_raddr_D after_bind_has_laddr_D local_ip_has_dev_D |
|
353 simp:socket_state.simps split:if_splits option.splits t_sock_addr.splits) |
|
354 done |
|
355 |
|
356 lemma accept_has_temps': |
|
357 "Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # valid \<tau> |
|
358 \<Longrightarrow> (\<exists> ltemp. nettemp_of_socket (Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # \<tau>) (p, fd\<^isub>2) False = Some ltemp) \<and> |
|
359 (\<exists> rtemp. nettemp_of_socket (Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # \<tau>) (p, fd\<^isub>2) True = Some rtemp)" |
|
360 apply (frule accept_has_temps[where is_remote = True]) |
|
361 apply (frule accept_has_temps[where is_remote = False]) |
|
362 by auto |
|
363 |
|
364 lemma bind_has_ltemp: "Bind p fd addr # valid \<tau> \<Longrightarrow> \<exists> temp. nettemp_of_socket (Bind p fd addr # \<tau>) (p, fd) False = Some temp" |
|
365 apply (frule vd_cons, frule vt_grant_os) |
|
366 apply (auto dest:cn_has_socktype simp:os_grant.simps current_sockets_simps nettemp_of_socket_def dest!:after_bind_has_netdev_D after_bind_has_laddr_D |
|
367 simp:socket_state.simps split:if_splits option.splits t_sock_addr.splits) |
|
368 done |
|
369 |
|
370 lemma connect_has_rtemp: "Connect p fd addr # valid \<tau> \<Longrightarrow> \<exists> temp. nettemp_of_socket (Connect p fd addr # \<tau>) (p, fd) True = Some temp" |
|
371 apply (frule vd_cons, frule vt_grant_os) |
|
372 apply (auto dest:cn_has_socktype simp:os_grant.simps current_sockets_simps nettemp_of_socket_def dest!:after_bind_has_netdev_D after_bind_has_laddr_D |
|
373 simp:socket_state.simps split:if_splits option.splits t_sock_addr.splits) |
|
374 done |
|
375 *) |
|
376 |
|
377 |
|
378 end |
|
379 |
|
380 end |