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