1 theory Alive_prop

     2 imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop

     3 begin

     4 

     5 context flask begin

     6 

     7 lemma distinct_queue_msgs:

     8   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> distinct (msgs_of_queue s q)"

     9 apply (induct s)

    10 apply (simp add:init_msgs_distinct)

    11 apply (frule vd_cons, frule vt_grant_os, case_tac a)

    12 apply auto

    13 apply (case_tac "msgs_of_queue s q", simp+)

    14 done

    15 

    16 lemma received_msg_notin: 

    17   "\<lbrakk>hd (msgs_of_queue s q) \<in> set (tl (msgs_of_queue s q)); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> False"

    18 apply (drule distinct_queue_msgs, simp)

    19 apply (case_tac "msgs_of_queue s q", auto)

    20 done

    21 

    22 lemma other_msg_remains:

    23   "\<lbrakk>m \<noteq> hd (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>

    24    \<Longrightarrow> (m \<in> set (tl (msgs_of_queue s q))) = (m \<in> set (msgs_of_queue s q))"

    25 apply (drule distinct_queue_msgs, simp)

    26 apply (case_tac "msgs_of_queue s q", auto)

    27 done

    28 

    29 lemma is_file_in_current:

    30   "is_file s f \<Longrightarrow> f \<in> current_files s"

    31 by (auto simp:is_file_def current_files_def split:option.splits)

    32 

    33 lemma is_dir_in_current:

    34   "is_dir s f \<Longrightarrow> f \<in> current_files s"

    35 by (auto simp:is_dir_def current_files_def split:option.splits)

    36 

    37 lemma is_tcp_in_current:

    38   "is_tcp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>"

    39 by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)

    40 

    41 lemma is_udp_in_current:

    42   "is_udp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>"

    43 by (auto simp:is_udp_sock_def current_sockets_def split:option.splits)

    44 

    45 (************ alive simpset **************)

    46 

    47 lemma alive_open: 

    48   "valid (Open p f flag fd opt # s) \<Longrightarrow> alive (Open p f flag fd opt # s) = (

    49      \<lambda> obj. case obj of 

    50               O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then True

    51                              else alive s obj

    52             | O_file f' \<Rightarrow> (if (opt = None) then alive s obj

    53                            else if (f = f') then True 

    54                                 else alive s obj)

    55             | _ \<Rightarrow> alive s obj)"

    56 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

    57 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

    58                  is_tcp_sock_simps is_udp_sock_simps

    59             dest:is_dir_in_current split:if_splits option.splits)

    60 done

    61 

    62 lemma alive_execve:

    63   "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (

    64      \<lambda> obj. case obj of

    65               O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd)

    66                              else if (p = p') then False

    67                                   else alive s (O_fd p' fd))

    68             | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))

    69                                      else if (p = p') then False

    70                                           else alive s (O_tcp_sock (p', fd)))

    71             | O_udp_sock (p', fd) \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))

    72                                      else if (p = p') then False

    73                                           else alive s (O_udp_sock (p', fd)))

    74             | _ \<Rightarrow> alive s obj )"

    75 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

    76 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

    77                  is_tcp_sock_simps is_udp_sock_simps

    78             dest:is_dir_in_current split:if_splits option.splits)

    79 done

    80 

    81 lemma alive_clone:

    82   "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = (

    83      \<lambda> obj. case obj of

    84               O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj

    85             | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True

    86                              else if (p'' = p') then False

    87                                   else alive s obj

    88             | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))

    89                                       else if (p'' = p') then False

    90                                            else alive s (O_tcp_sock (p'', fd)))

    91             | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))

    92                                       else if (p'' = p') then False

    93                                            else alive s (O_udp_sock (p'', fd)))

    94             | _ \<Rightarrow> alive s obj )"  

    95 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

    96 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

    97                  is_tcp_sock_simps is_udp_sock_simps

    98            intro:is_tcp_in_current is_udp_in_current

    99             dest:is_dir_in_current split:if_splits option.splits)

   100 done

   101 

   102 lemma alive_kill:

   103   "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (

   104      \<lambda> obj. case obj of 

   105               O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj

   106             | O_fd p'' fd \<Rightarrow> if (p'' = p') then False else alive s obj

   107             | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj

   108             | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj

   109             | _ \<Rightarrow> alive s obj)"

   110 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   111 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   112                  is_tcp_sock_simps is_udp_sock_simps

   113            intro:is_tcp_in_current is_udp_in_current

   114             dest:is_dir_in_current split:if_splits option.splits)

   115 done

   116 

   117 lemma alive_exit:

   118   "valid (Exit p' # s) \<Longrightarrow> alive (Exit p' # s) = (

   119      \<lambda> obj. case obj of 

   120               O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj

   121             | O_fd p'' fd \<Rightarrow> if (p'' = p') then False else alive s obj

   122             | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj

   123             | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj

   124             | _ \<Rightarrow> alive s obj)"

   125 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   126 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   127                  is_tcp_sock_simps is_udp_sock_simps

   128            intro:is_tcp_in_current is_udp_in_current

   129             dest:is_dir_in_current split:if_splits option.splits)

   130 done

   131 

   132 lemma alive_closefd:

   133   "valid (CloseFd p fd # s) \<Longrightarrow> alive (CloseFd p fd # s) = (

   134      \<lambda> obj. case obj of 

   135               O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then False else alive s obj

   136             | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd) then False else alive s obj

   137             | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd) then False else alive s obj

   138             | O_file f \<Rightarrow> (case (file_of_proc_fd s p fd) of

   139                             Some f' \<Rightarrow> (if (f = f' \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s) 

   140                                       then False else alive s obj)

   141                           | _ \<Rightarrow> alive s obj)

   142             | _ \<Rightarrow> alive s obj)"

   143 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   144 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   145                  is_tcp_sock_simps is_udp_sock_simps

   146            intro:is_tcp_in_current is_udp_in_current

   147             dest:is_dir_in_current file_of_pfd_is_file' split:if_splits option.splits)

   148 done

   149 

   150 lemma alive_unlink:

   151   "valid (UnLink p f # s) \<Longrightarrow> alive (UnLink p f # s) = (

   152      \<lambda> obj. case obj of

   153               O_file f' \<Rightarrow> if (f' = f \<and> proc_fd_of_file s f = {}) then False else alive s obj

   154             | _ \<Rightarrow> alive s obj)"

   155 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   156 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   157                  is_tcp_sock_simps is_udp_sock_simps

   158            intro:is_tcp_in_current is_udp_in_current

   159             dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict 

   160            split:if_splits option.splits)

   161 done

   162 

   163 lemma alive_rmdir:

   164   "valid (Rmdir p d # s) \<Longrightarrow> alive (Rmdir p d # s) = (alive s) (O_dir d := False)"

   165 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   166 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   167                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   168            intro:is_tcp_in_current is_udp_in_current

   169             dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict 

   170            split:if_splits option.splits)

   171 done

   172 

   173 lemma alive_mkdir:

   174   "valid (Mkdir p d inum # s) \<Longrightarrow> alive (Mkdir p d inum # s) = (alive s) (O_dir d := True)"

   175 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   176 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   177                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   178            intro:is_tcp_in_current is_udp_in_current

   179             dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

   180            split:if_splits option.splits)

   181 done

   182 

   183 lemma alive_linkhard:

   184   "valid (LinkHard p f f' # s) \<Longrightarrow> alive (LinkHard p f f' # s) = (alive s) (O_file f' := True)"

   185 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   186 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   187                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   188            intro:is_tcp_in_current is_udp_in_current

   189             dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

   190            split:if_splits option.splits)

   191 done

   192 

   193 lemma alive_createmsgq:

   194   "valid (CreateMsgq p q # s) \<Longrightarrow> alive (CreateMsgq p q # s) = (alive s) (O_msgq q := True)"

   195 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   196 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   197                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   198 done

   199 

   200 lemma alive_sendmsg:

   201   "valid (SendMsg p q m # s) \<Longrightarrow> alive (SendMsg p q m # s) = (alive s) (O_msg q m := True)"

   202 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   203 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   204                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   205 done

   206 

   207 lemma alive_recvmsg:

   208   "valid (RecvMsg p q m # s) \<Longrightarrow> alive (RecvMsg p q m # s) = (alive s) (O_msg q m := False)"

   209 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   210 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   211                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def other_msg_remains

   212             dest:received_msg_notin)

   213 done

   214 

   215 lemma alive_removemsgq: 

   216   "valid (RemoveMsgq p q # s) \<Longrightarrow> alive (RemoveMsgq p q # s) = (

   217      \<lambda> obj. case obj of

   218               O_msgq q' \<Rightarrow> if (q' = q) then False else alive s obj

   219             | O_msg q' m \<Rightarrow> if (q' = q) then False else alive s obj

   220             | _ \<Rightarrow> alive s obj)"

   221 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   222 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   223                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   224 done

   225 

   226 lemma alive_createshm:

   227   "valid (CreateShM p h # s) \<Longrightarrow> alive (CreateShM p h # s) = (alive s) (O_shm h := True)"

   228 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   229 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   230                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   231 done

   232 

   233 lemma alive_deleteshm:

   234   "valid (DeleteShM p h # s) \<Longrightarrow> alive (DeleteShM p h # s) = (alive s) (O_shm h := False)"

   235 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)

   236 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   237                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   238 done

   239 

   240 lemma alive_createsock:

   241   "valid (CreateSock p af st fd inum # s) \<Longrightarrow> alive (CreateSock p af st fd inum # s) = (

   242      \<lambda> obj. case obj of

   243               O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then True else alive s obj

   244             | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then True else alive s obj

   245             | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then True else alive s obj

   246             | _ \<Rightarrow> alive s obj)"

   247 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   248 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   249                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   250            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   251 done

   252 

   253 lemma alive_accept:

   254   "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> alive (Accept p fd addr port fd' inum # s) = (

   255      \<lambda> obj. case obj of

   256               O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then True else alive s obj

   257             | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then True else alive s obj

   258             | _ \<Rightarrow> alive s obj)"

   259 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)

   260 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   261                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   262            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   263 done

   264 

   265 lemma alive_other:

   266   "\<lbrakk>valid (e # s); 

   267     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   268     \<forall> p f fds. e \<noteq> Execve p f fds;

   269     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;

   270     \<forall> p p'. e \<noteq> Kill p p';

   271     \<forall> p. e \<noteq> Exit p; 

   272     \<forall> p fd. e \<noteq> CloseFd p fd;

   273     \<forall> p f. e \<noteq> UnLink p f;

   274     \<forall> p d. e \<noteq> Rmdir p d;

   275     \<forall> p d inum. e \<noteq> Mkdir p d inum;

   276     \<forall> p f f'. e \<noteq> LinkHard p f f';

   277     \<forall> p q. e \<noteq> CreateMsgq p q;

   278     \<forall> p q m. e \<noteq> SendMsg p q m;

   279     \<forall> p q m. e \<noteq> RecvMsg p q m;

   280     \<forall> p q. e \<noteq> RemoveMsgq p q;

   281     \<forall> p h. e \<noteq> CreateShM p h; 

   282     \<forall> p h. e \<noteq> DeleteShM p h;

   283     \<forall> p af st fd inum. e \<noteq> CreateSock p af st fd inum;

   284     \<forall> p fd addr port fd' inum. e \<noteq> Accept p fd addr port fd' inum\<rbrakk>

   285    \<Longrightarrow> alive (e # s) = alive s"

   286 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x, case_tac [!] e)

   287 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   288                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   289            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   290 done

   291 

   292 lemmas alive_simps = alive_open alive_execve alive_clone alive_kill alive_exit alive_closefd alive_unlink

   293   alive_rmdir alive_mkdir alive_linkhard alive_createmsgq alive_removemsgq alive_createshm alive_deleteshm

   294   alive_createsock alive_accept alive_other alive_sendmsg alive_recvmsg

   295 

   296   

   297 end

   298 

   299 end