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 shms # \<tau>) 
  \<Longrightarrow> current_sockets (Clone p p' fds shms # \<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 shms. e \<noteq> Clone p p' fds shms;
    \<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 shms # s) \<Longrightarrow> is_tcp_sock (Clone p p' fds shms # 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 shms. e \<noteq> Clone p p' fds shms;
    \<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 shms # s) \<Longrightarrow> is_udp_sock (Clone p p' fds shms # 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 shms. e \<noteq> Clone p p' fds shms;
    \<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