77
+ − 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