1 theory Alive_prop

     2 imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop Proc_fd_of_file_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_tcp_in_current:

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

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

    32 

    33 lemma is_udp_in_current:

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

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

    36 

    37 (************ alive simpset **************)

    38 

    39 lemma alive_open: 

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

    41      \<lambda> obj. case obj of 

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

    43                              else alive s obj

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

    45                            else if (f = f') then True 

    46                                 else alive s obj)

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

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

    49 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

    50                  is_tcp_sock_simps is_udp_sock_simps

    51             dest:is_dir_in_current split:if_splits option.splits)

    52 done

    53 

    54 (* sock is not inherited on Execve, Clone cases, cause I simplified it with os_grant. 

    55  * chunhan, 2013-11-20

    56 lemma alive_execve:

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

    58      \<lambda> obj. case obj of

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

    60                              else if (p = p') then False

    61                                   else alive s (O_fd p' fd))

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

    63                                      else if (p = p') then False

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

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

    66                                      else if (p = p') then False

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

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

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

    70 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

    71                  is_tcp_sock_simps is_udp_sock_simps

    72             dest:is_dir_in_current split:if_splits option.splits)

    73 

    74 done

    75 

    76 lemma alive_clone:

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

    78      \<lambda> obj. case obj of

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

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

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

    82                                   else alive s obj

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

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

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

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

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

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

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

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

    91 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

    92                  is_tcp_sock_simps is_udp_sock_simps

    93            intro:is_tcp_in_current is_udp_in_current

    94             dest:is_dir_in_current split:if_splits option.splits)

    95 done

    96 *)

    97 

    98 lemma alive_execve:

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

   100      \<lambda> obj. case obj of

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

   102                              else if (p = p') then False

   103                                   else alive s (O_fd p' fd))

   104             | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p') then False

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

   106             | O_udp_sock (p', fd) \<Rightarrow> (if (p = p') then False

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

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

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

   110 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   111                  is_tcp_sock_simps is_udp_sock_simps

   112             dest:is_dir_in_current split:if_splits option.splits

   113   dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)

   114 done

   115 

   116 lemma alive_clone:

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

   118      \<lambda> obj. case obj of

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

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

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

   122                                   else alive s obj

   123             | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False

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

   125             | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False

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

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

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

   129 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   130                  is_tcp_sock_simps is_udp_sock_simps

   131            intro:is_tcp_in_current is_udp_in_current

   132             dest:is_dir_in_current split:if_splits option.splits

   133   dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)

   134 done

   135 

   136 lemma alive_kill:

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

   138      \<lambda> obj. case obj of 

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

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

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

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

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

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

   145 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   146                  is_tcp_sock_simps is_udp_sock_simps

   147            intro:is_tcp_in_current is_udp_in_current

   148             dest:is_dir_in_current split:if_splits option.splits)

   149 done

   150 

   151 lemma alive_exit:

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

   153      \<lambda> obj. case obj of 

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

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

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

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

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

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

   160 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   161                  is_tcp_sock_simps is_udp_sock_simps

   162            intro:is_tcp_in_current is_udp_in_current

   163             dest:is_dir_in_current split:if_splits option.splits)

   164 done

   165 

   166 lemma alive_closefd:

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

   168      \<lambda> obj. case obj of 

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

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

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

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

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

   174                                       then False else alive s obj)

   175                           | _ \<Rightarrow> alive s obj)

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

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

   178 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   179                  is_tcp_sock_simps is_udp_sock_simps

   180            intro:is_tcp_in_current is_udp_in_current

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

   182 done

   183 

   184 lemma alive_unlink:

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

   186      \<lambda> obj. case obj of

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

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

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

   190 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   191                  is_tcp_sock_simps is_udp_sock_simps

   192            intro:is_tcp_in_current is_udp_in_current

   193             dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict 

   194            split:if_splits option.splits)

   195 done

   196 

   197 lemma alive_rmdir:

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

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

   200 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   201                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   202            intro:is_tcp_in_current is_udp_in_current

   203             dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict 

   204            split:if_splits option.splits)

   205 done

   206 

   207 lemma alive_mkdir:

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

   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

   212            intro:is_tcp_in_current is_udp_in_current

   213             dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

   214            split:if_splits option.splits)

   215 done

   216 

   217 lemma alive_linkhard:

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

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

   220 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   221                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   222            intro:is_tcp_in_current is_udp_in_current

   223             dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

   224            split:if_splits option.splits)

   225 done

   226 

   227 lemma alive_createmsgq:

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

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

   230 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   231                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   232 done

   233 

   234 lemma alive_sendmsg:

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

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

   237 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   238                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   239 done

   240 

   241 lemma alive_recvmsg:

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

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

   244 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   245                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def other_msg_remains

   246             dest:received_msg_notin)

   247 done

   248 

   249 lemma alive_removemsgq: 

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

   251      \<lambda> obj. case obj of

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

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

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

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

   256 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   257                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   258 done

   259 

   260 (*

   261 lemma alive_createshm:

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

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

   264 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   265                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   266 done

   267 

   268 lemma alive_deleteshm:

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

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

   271 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   272                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   273 done

   274 *)

   275 

   276 lemma alive_createsock:

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

   278      \<lambda> obj. case obj of

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

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

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

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

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

   284 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   285                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   286            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   287 done

   288 

   289 lemma alive_accept:

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

   291      \<lambda> obj. case obj of

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

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

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

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

   296 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   297                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   298            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   299 done

   300 

   301 lemma alive_other:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   321     \<forall> p h. e \<noteq> DeleteShM p h;*)

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

   323 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   324                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   325            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   326 done

   327 

   328 lemmas alive_simps = alive_open alive_execve alive_clone alive_kill alive_exit alive_closefd alive_unlink

   329   alive_rmdir alive_mkdir alive_linkhard alive_createmsgq alive_removemsgq (* alive_createshm alive_deleteshm *)

   330   alive_createsock alive_accept alive_other alive_sendmsg alive_recvmsg

   331 

   332   

   333 end

   334 

   335 end