Temp Enrich Proc_fd_of_file_prop New_obj_prop

fun assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option"

where

  "assoc [] a = None"

| "assoc (e # l) a = (if (fst e = a) then Some (snd e) else assoc l a)"

context flask begin

lemma sock_inum_eq_prop:

  "\<lbrakk>inum_of_socket s (p, fd) = Some im; inum_of_socket s (p', fd') = Some im; valid s\<rbrakk>

   \<Longrightarrow> (p' = p \<and> fd' = fd)"

apply (induct s arbitrary:p p')

apply (simp) defer

apply (frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto split:if_splits option.splits simp:proc_file_fds_def)

sorry

lemma inums_execve:

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

     current_inode_nums (Execve p f fds # s) = current_inode_nums s - 

     {inum. \<exists> fd. inum_of_socket s (p, fd) = Some inum}"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' dest:fim_noninter_sim'' sock_inum_eq_prop)

apply (drule set_mp, simp, simp, erule exE, drule filefd_socket_conflict, 

  simp add:current_sockets_def, simp, simp)+

apply (case_tac "a = p", simp)

apply (auto)

done

lemma inums_clone:

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

     current_inode_nums (Clone p p' fds # s) = current_inode_nums s"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' dest:fim_noninter_sim'' sock_inum_eq_prop)

apply (case_tac "a = p'")

apply (subgoal_tac "(p', b) \<in> current_sockets s")

apply (drule cn_in_curp, simp, simp, simp add:current_sockets_def)

apply auto

done

lemma inums_kill:

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

     {inum. \<exists> fd. inum_of_socket s (p', fd) = Some inum}"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop)

done

lemma inums_exit:

  "valid (Exit p # s) \<Longrightarrow> current_inode_nums (Exit p # s) = current_inode_nums s -

     {inum. \<exists> fd. inum_of_socket s (p, fd) = Some inum}"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop)

done

lemma inums_ptrace:

  "current_inode_nums (Ptrace p p' # s) = current_inode_nums s"

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop)

done

lemma inums_open:

  "valid (Open p f flags fd opt # s) \<Longrightarrow> 

    current_inode_nums (Open p f flags fd opt # s) = (

     case opt of

       None \<Rightarrow> current_inode_nums s

     | Some i \<Rightarrow> current_inode_nums s \<union> {i})"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits)

apply (case_tac "fa = f", simp add:current_files_def)

apply (rule_tac x = fa in exI, auto)

done

lemma inums_readfile:

  "current_inode_nums (ReadFile p fd # s) = current_inode_nums s"

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def)  

done

lemma inums_writefile:

  "current_inode_nums (WriteFile p fd # s) = current_inode_nums s"

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def)  

done

lemma inums_mkdir:

  "valid (Mkdir p f inum # s) \<Longrightarrow> current_inode_nums (Mkdir p f inum # s) = current_inode_nums s \<union> {inum}"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits)

apply (case_tac "fa = f", simp add:current_files_def)

apply (rule_tac x = fa in exI, auto)

done

lemma inums_linkhard:

  "valid (LinkHard p f f' # s) \<Longrightarrow> current_inode_nums (LinkHard p f f' # s) = current_inode_nums s"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def

  dest:filefd_socket_conflict fim_noninter_sim' fim_noninter_sim'' sock_inum_eq_prop split:option.splits)

apply (case_tac "fa = f'", simp add:current_files_def)

apply (rule_tac x = fa in exI, auto)

done 

lemma inums_truncate:

  "current_inode_nums (Truncate p f len # s) = current_inode_nums s"

apply (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def proc_file_fds_def)  

done

lemma inums_createmsgq:

  "current_inode_nums (CreateMsgq p q # s) = current_inode_nums s"

by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  

lemma inums_sendmsg:

  "current_inode_nums (SendMsg p q m # s) = current_inode_nums s"

by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  

lemma inums_recvmsg:

  "current_inode_nums (RecvMsg p q m # s) = current_inode_nums s"

by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  

lemma inums_removemsgq:

  "current_inode_nums (RemoveMsgq p q # s) = current_inode_nums s"

by (auto simp:current_inode_nums_def current_sock_inums_def current_file_inums_def)  

lemma inums_bind:

  "valid (Bind p fd addr # s) \<Longrightarrow> current_inode_nums (Bind p fd addr # s) = current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_connect:

  "valid (Connect p fd addr # s) \<Longrightarrow> current_inode_nums (Connect p fd addr # s) = current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_listen:

  "valid (Listen p fd # s) \<Longrightarrow> current_inode_nums (Listen p fd # s) = current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_sendsock:

  "valid (SendSock p fd # s) \<Longrightarrow> current_inode_nums (SendSock p fd # s) = current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_recvsock:

  "valid (RecvSock p fd # s) \<Longrightarrow> current_inode_nums (RecvSock p fd # s) = current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_shutdown:

  "valid (Shutdown p fd how # s) \<Longrightarrow> current_inode_nums (Shutdown p fd how # s) = current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_createsock:

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

     current_inode_nums s"

by (auto dest:vt_grant)

lemma inums_accept:

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

     current_inode_nums s"

by (auto dest:vt_grant)

lemmas current_inode_nums_simps = inums_execve inums_open inums_mkdir 

  inums_linkhard inums_createmsgq inums_sendmsg

  inums_createsock inums_accept inums_clone inums_kill inums_ptrace inums_exit inums_readfile

  inums_writefile inums_truncate inums_recvmsg inums_removemsgq

  inums_bind inums_connect inums_listen inums_sendsock

  inums_recvsock inums_shutdown

end

fun new_cf :: "t_file set \<Rightarrow> t_file \<Rightarrow> t_file"

  "new_cf fs []     = []"

| "new_cf fs (f#pf) = new_childf_general pf fs"

lemma new_cf_notin_fs:

  "\<lbrakk>finite fs; f \<noteq> []\<rbrakk> \<Longrightarrow> new_cf fs f \<notin> fs"

apply (case_tac f, simp)

apply (auto simp:ncf_notin_curf_general)

done

fun enrich_dufs:: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file set \<Rightarrow> (t_file \<times> t_file) list"

  "enrich_dufs [] sames curfs = []"

| "enrich_dufs (Open p f flags fd opt # s) sames curfs = 

    (if (f \<in> sames \<and> opt \<noteq> None) 

     then (f, new_cf (curfs \<union> set (map snd (enrich_dufs s sames curfs))) f) # enrich_dufs s sames curfs

     else enrich_dufs s sames curfs)"

| "enrich_dufs (LinkHard p f f' # s) sames curfs = 

    (if (f' \<in> sames) 

     then (f', new_cf (curfs \<union> set (map snd (enrich_dufs s sames curfs))) f') # enrich_dufs s sames curfs

     else enrich_dufs s sames curfs)"

| "enrich_dufs (_ # s) sames curfs = enrich_dufs s sames curfs"

lemma enrich_dufs_sameinodes1:

  "set (map fst (enrich_dufs s sames curfs)) \<subseteq> sames"

apply (induct s, simp)

by (case_tac a, auto)

  "\<lbrakk>valid s; \<forall> f \<in> sames. f \<notin> init_files; no_del_event s\<rbrakk> 

   \<Longrightarrow> set (map fst (enrich_dufs s sames curfs)) = sames \<inter> {f. is_file s f} "

apply (induct s)

apply (auto simp:is_file_nil is_init_file_props current_files_simps)[1]

apply (frule vt_grant_os, frule vd_cons, case_tac a)

apply (auto simp:is_file_simps is_file_in_current current_files_simps 

  same_inode_files_simps split:option.splits if_splits)

done

lemma finite_enrich_nfs:

  "finite (snd ` set (enrich_dufs s sames curfs))"

by (auto)

lemma new_cf_enrich:

  "\<lbrakk>finite curfs; f \<noteq> []\<rbrakk> \<Longrightarrow> new_cf (curfs \<union> snd ` set (enrich_dufs s sames curfs)) f \<notin> curfs \<union> snd ` set (enrich_dufs s sames curfs)"

using finite_enrich_nfs[where s = s and sames =sames and curfs = curfs]

apply (drule_tac F = curfs and G = "snd ` set (enrich_dufs s sames curfs)" in finite_UnI, simp)

apply (rule new_cf_notin_fs, simp+)

done

lemma enrich_dufs_nfs:

  "\<lbrakk>finite curfs; [] \<notin> sames\<rbrakk>

   \<Longrightarrow> set (map snd (enrich_dufs s sames curfs)) \<inter> curfs = {}"

apply (induct s)

apply (simp)

apply ( case_tac a)

apply (auto simp:is_file_in_current)

apply (drule_tac f = list and sames = sames and curfs = curfs and s = s in new_cf_enrich)

apply (rule notI, simp+)

apply (drule_tac f = list2 and sames = sames and curfs = curfs and s = s in new_cf_enrich)

apply (rule notI, simp+)

done

lemma pair_list_set: "(a, b) \<in> set l \<Longrightarrow> b \<in> snd ` set l"

by (induct l, auto)

lemma enrich_dufs_nfs_distinct:

  "\<lbrakk>finite curfs; [] \<notin> sames\<rbrakk> \<Longrightarrow> distinct (map snd (enrich_dufs s sames curfs))"

apply (induct s, simp)

apply (case_tac a, auto)

apply (drule pair_list_set)

apply (drule_tac f = list and s = s and sames = sames and curfs = curfs in new_cf_enrich)

apply (rule notI, simp, simp)

apply (drule pair_list_set)

apply (drule_tac f = list2 and s = s and sames = sames and curfs = curfs in new_cf_enrich)

apply (rule notI, simp, simp)

done

fun all_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"

  "all_fds [] = init_fds_of_proc"

| "all_fds (Open p f flags fd ipt # s) = (all_fds s) (p := all_fds s p \<union> {fd})" (*

| "all_fds (CreateSock p sf st fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})"

| "all_fds (Accept p fd' raddr port fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})" *)

| "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)"

| "all_fds (_ # s) = all_fds s"

fun enrich_dufds :: "t_state \<Rightarrow> t_file set \<Rightarrow> (t_process \<Rightarrow> t_fd set) \<Rightarrow> (t_state \<times> t_fd) list"

where 

  "enrich_dufds [] sames allpfds = []"

| "enrich_dufds (Open p f flags fd opt # s) sames allpfds = 

    (if (f \<in> sames) 

     then (Open p f flags fd opt # s, next_nat (allpfds p \<union> set (map snd (enrich_dufds s sames allpfds)))) #

          (enrich_dufds s sames allpfds)

     else enrich_dufds s sames allpfds)"

| "enrich_dufds (e # s) sames allpfds = enrich_dufds s sames allpfds"

fun index_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_state"

where

  "index_fd [] p fd = []"

| "index_fd (Open p f flags fd opt # s) p' fd' = 

    (if (p' = p \<and> fd' = fd) then Open p f flags fd opt # s

     else index_fd s p' fd')"

| "index_fd (e # s) p fd = index_fd s p fd"

definition enrich_fdset :: "t_state \<Rightarrow> (t_state \<times> t_fd) list \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> t_fd set"

where

  "enrich_fdset s dufds p fds \<equiv> 

    fds \<union> {fd'. \<exists> fd \<in> fds. assoc dufds (index_fd s p fd) = Some fd'}"

fun enrich_file :: "t_state \<Rightarrow> t_inode_num \<Rightarrow> (t_file \<times> t_file) list 

  \<Rightarrow> ((t_file \<times> t_process \<times> t_fd) \<times> t_fd) list \<Rightarrow> t_state"

where

  "enrich_file [] inum dufs dufds = []"

| "enrich_file (Open p f flags fd None # s) inum dufs dufds = 

    (case (assoc dufds (Open p f flags fd None # s), assoc dufs f) of

       (Some fd', Some f') \<Rightarrow> Open p f' flags fd' None # Open p f flags fd None # enrich_file s inum dufs dufds

     | _                   \<Rightarrow> Open p f flags fd None # (enrich_file s inum dufs dufds))"

| "enrich_file (Open p f flags fd (Some inum) # s) inum' dufs dufds = 

    (case (assoc dufs f, assoc dufds (f, p, fd)) of

        (Some f', Some fd') \<Rightarrow> Open p f' flags fd' (Some inum') # Open p f flags fd (Some inum) #

                               enrich_file s inum dufs dufds

    | _ \<Rightarrow> Open p f flags fd (Some inum) # enrich_file s inum dufs dufds)"

| "enrich_file (LinkHard p f f' # s) inum dufs dufds = 

    (case (assoc dufs f, assoc dufs f') of

       (Some df, Some df') \<Rightarrow> LinkHard p df df' # LinkHard p f f' # enrich_file s inum dufs dufds

     | _ \<Rightarrow> LinkHard p f f' # enrich_file s inum dufs dufds)"

| "enrich_file (Clone p p' fds # s) inum dufs dufds = 

    Clone p p' (enrich_fdset s dufds p fds) # (enrich_file s inum dufs dufds)" 

| "enrich_file (Execve p f fds # s) inum dufs dufds = 

    Execve p f (enrich_fdset s dufds p fds) # (enrich_file s inum dufs dufds)"    

| "enrich_file (WriteFile p fd # s) inum dufs dufds = 

    (case (file_of_proc_fd s p fd) of 

       Some f \<Rightarrow> (case (assoc dufds (f, p, fd)) of

                    Some fd' \<Rightarrow> WriteFile p fd' # WriteFile p fd # enrich_file s inum dufs dufds

                  | _        \<Rightarrow> WriteFile p fd # enrich_file s inum dufs dufds)

    | _       \<Rightarrow> [])"

| "enrich_file (e # s) inum dufs dufds = e # enrich_file s inum dufs dufds"

definition same_inodes_list :: "t_state \<Rightarrow> t_file list \<Rightarrow> bool"

where

  "same_inodes_list s flist \<equiv> flist \<noteq> [] \<and> set flist = same_inode_files s (hd flist)"

lemma assoc_dufs_prop1:

  "\<lbrakk>\<forall> f \<in> set (map snd dufs). f \<notin> current_files s; assoc dufs f = Some f'\<rbrakk> \<Longrightarrow> f' \<notin> current_files s"

apply (erule_tac x = "f'" in ballE)

apply auto

apply (induct dufs, auto split:if_splits)

done

lemma enrich_file_dufs_inode_aux1:

  "\<lbrakk>no_del_event s; valid s; f \<in> current_files s; \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> f' \<notin> current_files s\<rbrakk> 

   \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f = inum_of_file s f"

apply (induct s arbitrary:f, simp)

apply (frule vt_grant_os, frule vd_cons, case_tac a)

apply (auto split:option.splits simp:current_files_simps dest:is_file_in_current is_dir_in_current)

done

lemma enrich_file_dufs_inode1:

  "\<lbrakk>no_del_event s; valid s; f \<in> current_files s; \<forall> f \<in> set (map snd dufs). f \<notin> current_files s\<rbrakk> 

   \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f = inum_of_file s f"

apply (erule enrich_file_dufs_inode_aux1)

apply (simp, simp)

apply (erule assoc_dufs_prop1, simp+)

done

lemma enrich_file_dufs_inode2:

  "\<lbrakk>no_del_event s; valid s; is_file s f; f \<notin> init_files; assoc dufs f = Some f';

    \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> f' \<notin> current_files s;    

    \<And> f f'. assoc dufs f = Some f' \<Longrightarrow> inum_of_file s f' = None\<rbrakk> 

   \<Longrightarrow> inum_of_file (enrich_file s inum dufs) f' = Some inum"

apply (induct s arbitrary:f f', simp) defer

apply(frule vt_grant_os, frule vd_cons, case_tac a)

apply (auto split:option.splits if_splits

 simp:current_files_simps  current_inode_nums_simps is_file_simps

dest:is_file_in_current is_dir_in_current)

lemma enrich_file_dufs_sameinodes:

  "\<lbrakk>same_inodes_list s (map fst dufs); \<forall> f \<in> set (map fst dufs). f \<notin> init_files; inum \<notin> current_inode_nums s; 

    distinct (map snd dufs); \<forall> f \<in> set (map snd dufs). f \<notin> current_files s; valid s\<rbrakk> 

   \<Longrightarrow> same_inodes_list (enrich_file s inum dufs) (map snd dufs)"

apply (induct s) apply (simp add:same_inodes_list_def same_inode_files_simps)

defer

apply (frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto simp:same_inodes_list_def same_inode_files_simps)

lemma enrich_dufs_fst:

  "\<lbrakk>valid s; "