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 (*

   218 lemma alive_linkhard:

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

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

   221 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

   222                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   223            intro:is_tcp_in_current is_udp_in_current

   224             dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

   225            split:if_splits option.splits)

   226 done

   227 *)

   228 

   229 lemma alive_createmsgq:

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

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

   232 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   233                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   234 done

   235 

   236 lemma alive_sendmsg:

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

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

   239 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   240                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   241 done

   242 

   243 lemma alive_recvmsg:

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

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

   246 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   247                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def other_msg_remains

   248             dest:received_msg_notin)

   249 done

   250 

   251 lemma alive_removemsgq: 

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

   253      \<lambda> obj. case obj of

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

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

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

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

   258 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   259                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   260 done

   261 

   262 (*

   263 lemma alive_createshm:

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

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

   266 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   267                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   268 done

   269 

   270 lemma alive_deleteshm:

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

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

   273 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   274                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

   275 done

   276 *)

   277 

   278 lemma alive_createsock:

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

   280      \<lambda> obj. case obj of

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

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

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

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

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

   286 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   287                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   288            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   289 done

   290 

   291 lemma alive_accept:

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

   293      \<lambda> obj. case obj of

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

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

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

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

   298 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

   299                  is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

   300            intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

   301 done

   302 

   303 lemma alive_other:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   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_createmsgq alive_removemsgq

   330   alive_createsock alive_accept alive_other alive_sendmsg alive_recvmsg

   331 

   332   

   333 end

   334 

   335 end