--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/no_shm_selinux/Current_sockets_prop.thy Tue Dec 17 13:30:21 2013 +0800
@@ -0,0 +1,380 @@
+theory Current_sockets_prop
+imports Main Flask Flask_type Current_files_prop
+begin
+
+context flask begin
+
+lemma cn_in_curp: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> p \<in> current_procs \<tau>"
+apply (induct \<tau>) defer
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:current_sockets_def inum_of_socket.simps current_procs.simps os_grant.simps split:if_splits option.splits
+ dest:inos_has_sock_tag init_socket_has_inode)
+done
+
+lemma cn_in_curfd_aux: "\<forall> p. (p, fd) \<in> current_sockets \<tau> \<and> valid \<tau> \<longrightarrow> fd \<in> current_proc_fds \<tau> p"
+apply (induct \<tau>) defer
+apply (rule allI, rule impI, erule conjE, frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:current_sockets_def current_proc_fds.simps os_grant.simps inum_of_socket.simps
+ split:if_splits option.splits t_socket_af.splits dest:inos_has_sock_tag init_socket_has_inode)
+done
+
+lemma cn_in_curfd: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p"
+by (simp add:cn_in_curfd_aux)
+
+lemma cn_in_curfd': "\<lbrakk>inum_of_socket \<tau> (p, fd) = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p"
+by (rule cn_in_curfd, simp_all add:current_sockets_def)
+
+lemma cn_in_curp': "\<lbrakk>inum_of_socket \<tau> (p, fd) = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> p \<in> current_procs \<tau>"
+apply (rule cn_in_curp)
+by (auto simp:current_sockets_def)
+
+(***************** current_sockets simpset *****************)
+
+lemma current_sockets_nil: "current_sockets [] = init_sockets"
+apply (simp add:current_sockets_def inum_of_socket.simps)
+using init_socket_has_inode inos_has_sock_tag
+by auto
+
+lemma current_sockets_closefd: "current_sockets (CloseFd p fd # \<tau>) = current_sockets \<tau> - {(p, fd)}"
+by (auto simp add:current_sockets_def inum_of_socket.simps)
+
+lemma current_sockets_createsock: "current_sockets (CreateSock p aft st fd ino # \<tau>) = insert (p, fd) (current_sockets \<tau>)"
+by (auto simp add:current_sockets_def inum_of_socket.simps)
+
+lemma current_sockets_accept: "current_sockets (Accept p fd addr lport' fd' ino # \<tau>) = insert (p, fd') (current_sockets \<tau>)"
+by (auto simp add:current_sockets_def inum_of_socket.simps)
+
+lemma current_sockets_clone: "valid (Clone p p' fds # \<tau>)
+ \<Longrightarrow> current_sockets (Clone p p' fds # \<tau>) =
+ current_sockets \<tau> \<union> {(p', fd)| fd. (p, fd) \<in> current_sockets \<tau> \<and> fd \<in> fds}"
+apply (frule vd_cons, drule vt_grant_os)
+apply (auto simp add:os_grant.simps current_sockets_def inum_of_socket.simps split:if_splits
+ dest:cn_in_curp')
+done
+
+lemma current_sockets_execve: "valid (Execve p f fds # \<tau>)
+ \<Longrightarrow> current_sockets (Execve p f fds # \<tau>) =
+ current_sockets \<tau> - {(p, fd)| fd. (p, fd) \<in> current_sockets \<tau> \<and> fd \<notin> fds}"
+apply (frule vd_cons, drule vt_grant_os)
+apply (auto simp add:os_grant.simps current_sockets_def inum_of_socket.simps split:if_splits
+ dest:cn_in_curp')
+done
+
+lemma current_sockets_kill: "current_sockets (Kill p p' # \<tau>) = current_sockets \<tau> - {(p', fd)| fd. (p', fd) \<in> current_sockets \<tau>}"
+by (auto simp add:current_sockets_def inum_of_socket.simps split:if_splits)
+
+lemma current_sockets_exit: "current_sockets (Exit p # \<tau>) = current_sockets \<tau> - {(p, fd)| fd. (p, fd) \<in> current_sockets \<tau>}"
+by (auto simp add:current_sockets_def inum_of_socket.simps split:if_splits)
+
+lemma current_sockets_other:
+ "\<lbrakk>\<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p aft st fd ino. e \<noteq> CreateSock p aft st fd ino;
+ \<forall> p fd addr lport' fd' ino. e \<noteq> Accept p fd addr lport' fd' ino;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
+ \<forall> p f fds. e \<noteq> Execve p f fds;
+ \<forall> p p'. e \<noteq> Kill p p';
+ \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> current_sockets (e # \<tau>) = current_sockets \<tau>"
+apply (case_tac e)
+by (auto simp add:current_sockets_def inum_of_socket.simps split:if_splits)
+
+lemmas current_sockets_simps = current_sockets_nil current_sockets_closefd current_sockets_createsock
+ current_sockets_accept current_sockets_execve current_sockets_clone
+ current_sockets_kill current_sockets_exit current_sockets_other
+
+(********** is_tcp_sock simpset ***************)
+
+lemma is_tcp_sock_nil:
+ "is_tcp_sock [] = is_init_tcp_sock"
+apply (rule ext)
+apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props
+ dest:init_socket_has_inode split:option.splits)
+done
+
+lemma is_tcp_sock_closefd:
+ "is_tcp_sock (CloseFd p fd # s) = (is_tcp_sock s) ((p, fd) := False)"
+apply (rule ext)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps split:option.splits t_inode_tag.splits)
+
+lemma is_tcp_sock_createsock:
+ "valid (CreateSock p af st fd ino # s) \<Longrightarrow> is_tcp_sock (CreateSock p af st fd ino # s) = (
+ case st of
+ STREAM \<Rightarrow> (is_tcp_sock s) ((p, fd) := True)
+ | _ \<Rightarrow> is_tcp_sock s )"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_tcp_sock_accept:
+ "valid (Accept p fd addr lport fd' ino # s)
+ \<Longrightarrow> is_tcp_sock (Accept p fd addr lport fd' ino # s) = (is_tcp_sock s) ((p,fd') := True)"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_tcp_sock_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> is_tcp_sock (Execve p f fds # s) = (
+ \<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then is_tcp_sock s (p, fd)
+ else if (p' = p) then False
+ else is_tcp_sock s (p', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_tcp_sock_clone:
+ "valid (Clone p p' fds # s) \<Longrightarrow> is_tcp_sock (Clone p p' fds # s) = (
+ \<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then is_tcp_sock s (p, fd)
+ else if (p'' = p') then False
+ else is_tcp_sock s (p'', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_tcp_sock_kill:
+ "valid (Kill p p' # s) \<Longrightarrow> is_tcp_sock (Kill p p' # s) = (
+ \<lambda> (p'', fd). if (p'' = p') then False
+ else is_tcp_sock s (p'', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_tcp_sock_exit:
+ "valid (Exit p # s) \<Longrightarrow> is_tcp_sock (Exit p # s) = (
+ \<lambda> (p', fd). if (p' = p) then False
+ else is_tcp_sock s (p', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_tcp_sock_other:
+ "\<lbrakk>valid (e # \<tau>);
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p aft st fd ino. e \<noteq> CreateSock p aft st fd ino;
+ \<forall> p fd addr lport' fd' ino. e \<noteq> Accept p fd addr lport' fd' ino;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
+ \<forall> p f fds. e \<noteq> Execve p f fds;
+ \<forall> p p'. e \<noteq> Kill p p';
+ \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> is_tcp_sock (e # \<tau>) = is_tcp_sock \<tau>"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x, case_tac e)
+prefer 6 apply (case_tac option)
+by (auto simp add:is_tcp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemmas is_tcp_sock_simps = is_tcp_sock_nil is_tcp_sock_closefd is_tcp_sock_createsock is_tcp_sock_accept
+ is_tcp_sock_clone is_tcp_sock_execve is_tcp_sock_kill is_tcp_sock_exit is_tcp_sock_other
+
+
+(************ is_udp_sock simpset *************)
+
+lemma is_udp_sock_nil:
+ "is_udp_sock [] = is_init_udp_sock"
+apply (rule ext)
+apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props
+ dest:init_socket_has_inode split:option.splits)
+done
+
+lemma is_udp_sock_closefd:
+ "is_udp_sock (CloseFd p fd # s) = (is_udp_sock s) ((p, fd) := False)"
+apply (rule ext)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps split:option.splits t_inode_tag.splits)
+
+lemma is_udp_sock_createsock:
+ "valid (CreateSock p af st fd ino # s) \<Longrightarrow> is_udp_sock (CreateSock p af st fd ino # s) = (
+ case st of
+ DGRAM \<Rightarrow> (is_udp_sock s) ((p, fd) := True)
+ | _ \<Rightarrow> is_udp_sock s )"
+apply (frule vd_cons, frule vt_grant_os, rule ext)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_udp_sock_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> is_udp_sock (Execve p f fds # s) = (
+ \<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then is_udp_sock s (p, fd)
+ else if (p' = p) then False
+ else is_udp_sock s (p', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_udp_sock_clone:
+ "valid (Clone p p' fds # s) \<Longrightarrow> is_udp_sock (Clone p p' fds # s) = (
+ \<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then is_udp_sock s (p, fd)
+ else if (p'' = p') then False
+ else is_udp_sock s (p'', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_udp_sock_kill:
+ "valid (Kill p p' # s) \<Longrightarrow> is_udp_sock (Kill p p' # s) = (
+ \<lambda> (p'', fd). if (p'' = p') then False
+ else is_udp_sock s (p'', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_udp_sock_exit:
+ "valid (Exit p # s) \<Longrightarrow> is_udp_sock (Exit p # s) = (
+ \<lambda> (p', fd). if (p' = p) then False
+ else is_udp_sock s (p', fd))"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemma is_udp_sock_other:
+ "\<lbrakk>valid (e # \<tau>);
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p aft st fd ino. e \<noteq> CreateSock p aft st fd ino;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
+ \<forall> p f fds. e \<noteq> Execve p f fds;
+ \<forall> p p'. e \<noteq> Kill p p';
+ \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> is_udp_sock (e # \<tau>) = is_udp_sock \<tau>"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x, case_tac e)
+prefer 6 apply (case_tac option)
+by (auto simp add:is_udp_sock_def inum_of_socket.simps dest:ios's_im_in_cim cn_in_curfd'
+ split:option.splits t_inode_tag.splits t_socket_type.splits)
+
+lemmas is_udp_sock_simps = is_udp_sock_nil is_udp_sock_closefd is_udp_sock_createsock
+ is_udp_sock_clone is_udp_sock_execve is_udp_sock_kill is_udp_sock_exit is_udp_sock_other
+
+lemma update_with_shuthow_someI: "socket_in_trans \<tau> s \<Longrightarrow> \<exists> st'. update_with_shuthow (socket_state \<tau> s) how = Some st'"
+apply (case_tac "socket_state \<tau> s", simp add:socket_in_trans_def, case_tac a)
+apply (auto simp:update_with_shuthow.simps socket_in_trans_def split:option.splits)
+apply (case_tac t_sock_trans_state, case_tac [!] how)
+by auto
+
+lemma is_tcp_sock_imp_curernt_proc:
+ "\<lbrakk>is_tcp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:is_tcp_sock_nil is_init_tcp_sock_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by (auto simp:is_tcp_sock_simps split:if_splits option.splits t_socket_type.splits)
+
+lemma is_udp_sock_imp_curernt_proc:
+ "\<lbrakk>is_udp_sock s (p,fd); valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:is_udp_sock_nil is_init_udp_sock_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by (auto simp:is_udp_sock_simps split:if_splits option.splits t_socket_type.splits)
+
+
+(***** below should be adjusted after starting static analysis of sockets ! ??? ****)
+
+(*
+lemma cn_has_sockstate: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> socket_state \<tau> (p, fd) \<noteq> None"
+apply (induct \<tau> arbitrary: p) using init_socket_has_state
+apply (simp add:current_sockets_simps socket_state.simps bidirect_in_init_def)
+
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:current_sockets_simps os_grant.simps socket_state.simps intro:update_with_shuthow_someI dest:cn_no_newproc' split:option.splits)
+done
+
+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)"
+apply (case_tac "socket_state \<tau> s", simp, case_tac a)
+apply (auto simp:update_with_shuthow.simps split:option.splits)
+done
+
+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))"
+apply (induct \<tau>)
+apply (clarsimp simp add:socket_state.simps local_addr.simps)
+apply (drule init_socket_has_laddr, simp, erule exE)
+apply (case_tac y, simp)
+
+apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
+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)
+apply (erule_tac x = nat1 in allE, erule_tac x = nat2 in allE, erule impE, simp+)
+done
+
+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)"
+by (rule after_bind_has_laddr_aux[rule_format], simp+)
+
+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)"
+by (case_tac s, auto dest:after_bind_has_laddr)
+
+lemma after_bind_has_laddr_D: "\<lbrakk>local_addr \<tau> s = None; valid \<tau>\<rbrakk> \<Longrightarrow> \<not> after_bind (socket_state \<tau> s)"
+by (auto dest:after_bind_has_laddr')
+
+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"
+apply (induct \<tau> arbitrary:p fd port)
+apply (simp add:local_addr.simps current_sockets_simps local_ip_valid)
+
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+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)
+done
+
+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"
+by (case_tac s, simp add:local_addr_valid)
+
+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"
+using local_ip2dev_valid
+by (drule_tac local_addr_valid', simp+)
+
+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"
+apply (drule after_bind_has_laddr', simp, clarsimp)
+apply (frule local_addr_valid', simp+)
+apply (drule local_ip2dev_valid, simp add:netdev_of_socket_def)
+done
+
+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)"
+by (auto dest:after_bind_has_netdev)
+
+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)"
+apply (case_tac "socket_state \<tau> s", simp, case_tac a)
+apply (auto simp:update_with_shuthow.simps split:option.splits)
+done
+
+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"
+apply (induct \<tau> arbitrary:p fd)
+apply (simp add:socket_state.simps local_addr.simps) using init_socket_has_raddr apply blast
+
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+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)
+done
+
+lemma after_conacc_has_raddr': "\<lbrakk>after_conacc (socket_state \<tau> s); valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> addr. remote_addr \<tau> s = Some addr"
+by (case_tac s, auto dest:after_conacc_has_raddr)
+
+lemma after_conacc_has_raddr_D: "\<lbrakk>remote_addr \<tau> s = None; valid \<tau>\<rbrakk> \<Longrightarrow> \<not> after_conacc (socket_state \<tau> s)"
+by (auto dest:after_conacc_has_raddr')
+
+
+lemma cn_has_socktype: "\<lbrakk>(p, fd) \<in> current_sockets \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> st. socket_type \<tau> (p, fd) = Some st"
+apply (induct \<tau> arbitrary:p fd)
+using init_socket_has_socktype
+apply (simp add:socket_type.simps current_sockets_nil bidirect_in_init_def)
+
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+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)
+done
+
+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"
+apply (frule vd_cons, frule vt_grant_os)
+apply (auto dest:cn_has_socktype simp:os_grant.simps nettemp_of_socket_def netdev_of_socket_def
+ dest!:after_conacc_has_raddr_D after_bind_has_laddr_D local_ip_has_dev_D
+ simp:socket_state.simps split:if_splits option.splits t_sock_addr.splits)
+done
+
+lemma accept_has_temps':
+ "Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # valid \<tau>
+ \<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>
+ (\<exists> rtemp. nettemp_of_socket (Accept p fd\<^isub>1 addr port fd\<^isub>2 inum # \<tau>) (p, fd\<^isub>2) True = Some rtemp)"
+apply (frule accept_has_temps[where is_remote = True])
+apply (frule accept_has_temps[where is_remote = False])
+by auto
+
+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"
+apply (frule vd_cons, frule vt_grant_os)
+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
+ simp:socket_state.simps split:if_splits option.splits t_sock_addr.splits)
+done
+
+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"
+apply (frule vd_cons, frule vt_grant_os)
+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
+ simp:socket_state.simps split:if_splits option.splits t_sock_addr.splits)
+done
+*)
+
+
+end
+
+end
\ No newline at end of file