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