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 f f'. e \<noteq> LinkHard p f f';
    \<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" (* 
    \<forall> p h. e \<noteq> CreateShM p h; 
    \<forall> p h. e \<noteq> DeleteShM p h;*)
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_linkhard alive_createmsgq alive_removemsgq (* alive_createshm alive_deleteshm *)
  alive_createsock alive_accept alive_other alive_sendmsg alive_recvmsg

  
end

end