theory Alive_prop

imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop Proc_fd_of_file_prop

begin

context flask begin

lemma distinct_queue_msgs:

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

apply (induct s)

apply (simp add:init_msgs_distinct)

apply (frule vd_cons, frule vt_grant_os, case_tac a)

apply auto

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

done

lemma received_msg_notin: 

  "\<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"

apply (drule distinct_queue_msgs, simp)

apply (case_tac "msgs_of_queue s q", auto)

done

lemma other_msg_remains:

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

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

apply (drule distinct_queue_msgs, simp)

apply (case_tac "msgs_of_queue s q", auto)

done

lemma is_tcp_in_current:

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

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

lemma is_udp_in_current:

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

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

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

lemma alive_open: 

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

     \<lambda> obj. case obj of 

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

                             else alive s obj

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

                           else if (f = f') then True 

                                else alive s obj)

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

            dest:is_dir_in_current split:if_splits option.splits)

done

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

 * chunhan, 2013-11-20

lemma alive_execve:

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

     \<lambda> obj. case obj of

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

                             else if (p = p') then False

                                  else alive s (O_fd p' fd))

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

                                     else if (p = p') then False

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

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

                                     else if (p = p') then False

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

            | _ \<Rightarrow> alive s obj )"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

            dest:is_dir_in_current split:if_splits option.splits)

done

lemma alive_clone:

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

     \<lambda> obj. case obj of

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

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

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

                                  else alive s obj

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

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

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

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

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

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

            | _ \<Rightarrow> alive s obj )"  

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current split:if_splits option.splits)

done

*)

lemma alive_execve:

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

     \<lambda> obj. case obj of

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

                             else if (p = p') then False

                                  else alive s (O_fd p' fd))

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

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

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

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

            | _ \<Rightarrow> alive s obj )"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

            dest:is_dir_in_current split:if_splits option.splits

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

done

lemma alive_clone:

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

     \<lambda> obj. case obj of

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

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

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

                                  else alive s obj

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

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

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

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

            | _ \<Rightarrow> alive s obj )"  

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current split:if_splits option.splits

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

done

lemma alive_kill:

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

     \<lambda> obj. case obj of 

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

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

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

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

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current split:if_splits option.splits)

done

lemma alive_exit:

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

     \<lambda> obj. case obj of 

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

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

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

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

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current split:if_splits option.splits)

done

lemma alive_closefd:

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

     \<lambda> obj. case obj of 

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

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

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

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

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

                                      then False else alive s obj)

                          | _ \<Rightarrow> alive s obj)

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

           intro:is_tcp_in_current is_udp_in_current

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

done

lemma alive_unlink:

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

     \<lambda> obj. case obj of

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

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict 

           split:if_splits option.splits)

done

lemma alive_rmdir:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict 

           split:if_splits option.splits)

done

lemma alive_mkdir:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

           split:if_splits option.splits)

done

(*

lemma alive_linkhard:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps 

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

           intro:is_tcp_in_current is_udp_in_current

            dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current

           split:if_splits option.splits)

done

*)

lemma alive_createmsgq:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

done

lemma alive_sendmsg:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

done

lemma alive_recvmsg:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def other_msg_remains

            dest:received_msg_notin)

done

lemma alive_removemsgq: 

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

     \<lambda> obj. case obj of

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

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

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

done

(*

lemma alive_createshm:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

done

lemma alive_deleteshm:

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)

done

*)

lemma alive_createsock:

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

     \<lambda> obj. case obj of

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

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

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

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

           intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

done

lemma alive_accept:

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

     \<lambda> obj. case obj of

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

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

            | _ \<Rightarrow> alive s obj)"

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

           intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

done

lemma alive_other:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps

                 is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def

           intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)

done

lemmas alive_simps = alive_open alive_execve alive_clone alive_kill alive_exit alive_closefd alive_unlink

  alive_rmdir alive_mkdir alive_createmsgq alive_removemsgq

  alive_createsock alive_accept alive_other alive_sendmsg alive_recvmsg

end

end