theory Enrich2
imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
 Temp Enrich Proc_fd_of_file_prop
begin

context tainting_s begin

fun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state"
where
  "enrich_msgq [] tq dq = []"
| "enrich_msgq (CreateMsgq p q # s) tq dq = 
    (if (tq = q) 
     then (CreateMsgq p dq # CreateMsgq p q # s)
     else CreateMsgq p q # (enrich_msgq s tq dq))"
| "enrich_msgq (SendMsg p q m # s) tq dq = 
    (if (tq = q) 
     then (SendMsg p dq m # SendMsg p q m # (enrich_msgq s tq dq))
     else SendMsg p q m # (enrich_msgq s tq dq))"
| "enrich_msgq (RecvMsg p q m # s) tq dq = 
    (if (tq = q) 
     then (RecvMsg p dq m # RecvMsg p q m # (enrich_msgq s tq dq))
     else RecvMsg p q m # (enrich_msgq s tq dq))"
| "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)"

lemma enrich_msgq_duq_in:
  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> q' \<in> current_msgqs (enrich_msgq s q q')"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply auto
done

lemma enrich_msgq_duq_sms:
  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') q' = msgs_of_queue s q"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply auto
done

lemma enrich_msgq_cur_inof:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> inum_of_file (enrich_msgq s q q') 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)
done

lemma enrich_msgq_cur_inos:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
apply (rule ext)
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto split:option.splits)
done

lemma enrich_msgq_cur_inos':
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
apply (simp add:enrich_msgq_cur_inos)
done

lemma enrich_msgq_cur_inums:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
apply (auto simp:current_inode_nums_def current_file_inums_def 
  current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
done

lemma enrich_msgq_cur_itag:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
apply (rule ext)
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto split:option.splits t_socket_type.splits)
done

lemma enrich_msgq_cur_tcps:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
apply (rule ext)
apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
  split:option.splits t_inode_tag.splits)
done

lemma enrich_msgq_cur_udps:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
apply (rule ext)
apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
  split:option.splits t_inode_tag.splits)
done

lemma enrich_msgq_cur_msgqs:
  "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto)
done

lemma enrich_msgq_cur_msgs:
  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)" 
apply (rule ext, simp, rule conjI, rule impI)
apply (simp add:enrich_msgq_duq_sms)
apply (rule impI) 
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto)
done

lemma enrich_msgq_cur_procs:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto)
done
  
lemma enrich_msgq_cur_files:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
apply (auto simp:current_files_def)
apply (simp add:enrich_msgq_cur_inof)+
done

lemma enrich_msgq_cur_fds:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply auto
done

lemma enrich_msgq_filefd:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
apply (rule ext, rule ext)
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply auto
done

lemma enrich_msgq_flagfd:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
apply (rule ext, rule ext)
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply auto
done

lemma enrich_msgq_proc_fds:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
done

lemma enrich_msgq_hungs:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> files_hung_by_del (enrich_msgq s q q') = files_hung_by_del s"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
apply (auto simp:files_hung_by_del.simps)
done
  
lemma enrich_msgq_is_file:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
apply (rule ext)
apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
  split:option.splits t_inode_tag.splits)
done

lemma enrich_msgq_is_dir:
  "\<lbrakk>no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
apply (rule ext)
apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
  split:option.splits t_inode_tag.splits)
done

lemma enrich_msgq_alive:
  "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
   \<Longrightarrow> alive (enrich_msgq s q q') obj"
apply (case_tac obj)
apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 
  enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds
  enrich_msgq_cur_tcps enrich_msgq_cur_udps)
apply (rule impI, simp)
done

lemma enrich_msgq_alive':
  "\<lbrakk>alive (enrich_msgq s q q') obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
   \<Longrightarrow> alive s obj \<or> obj = O_msgq q' \<or> (\<exists> m. obj = O_msg q' m \<and> alive s (O_msg q m))"
apply (case_tac obj)
apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 
  enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds
  enrich_msgq_cur_tcps enrich_msgq_cur_udps)
apply (auto split:if_splits)
done

lemma enrich_msgq_not_alive:
  "\<lbrakk>enrich_not_alive s (E_msgq q') obj; q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> enrich_not_alive (enrich_msgq s q q') (E_msgq q') obj"
apply (case_tac obj)
apply (auto simp:enrich_msgq_cur_fds enrich_msgq_cur_files 
  enrich_msgq_cur_procs enrich_msgq_cur_inums enrich_msgq_cur_msgqs enrich_msgq_cur_msgs)
done

lemma enrich_msgq_no_del:
  "\<lbrakk>no_del_event s\<rbrakk> \<Longrightarrow> no_del_event (enrich_msgq s q q')"
apply (induct s, simp)
by (case_tac a, auto)

lemma nodel_died_proc:
  "no_del_event s \<Longrightarrow> \<not> died (O_proc p) s"
apply (induct s, simp)
by (case_tac a, auto)

lemma cf2sfile_execve:
  "\<lbrakk>ff \<in> current_files (Execve p f fds # s); valid (Execve p f fds # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (Execve p f fds # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_clone:
  "\<lbrakk>ff \<in> current_files (Clone p p' fds # s); valid (Clone p p' fds # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (Clone p p' fds # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_ptrace:
  "\<lbrakk>ff \<in> current_files (Ptrace p p' # s); valid (Ptrace p p' # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (Ptrace p p' # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_readfile:
  "\<lbrakk>ff \<in> current_files (ReadFile p fd # s); valid (ReadFile p fd # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (ReadFile p fd # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_writefile:
  "\<lbrakk>ff \<in> current_files (WriteFile p fd # s); valid (WriteFile p fd # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (WriteFile p fd # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_truncate:
  "\<lbrakk>ff \<in> current_files (Truncate p f len # s); valid (Truncate p f len # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (Truncate p f len # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_createmsgq:
  "\<lbrakk>ff \<in> current_files (CreateMsgq p q # s); valid (CreateMsgq p q # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (CreateMsgq p q # s) ff= cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_sendmsg:
  "\<lbrakk>ff \<in> current_files (SendMsg p q m # s); valid (SendMsg p q m # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (SendMsg p q m # s) ff = cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemma cf2sfile_recvmsg:
  "\<lbrakk>ff \<in> current_files (RecvMsg p q m # s); valid (RecvMsg p q m # s)\<rbrakk>
   \<Longrightarrow> cf2sfile (RecvMsg p q m # s) ff = cf2sfile s ff"
by (auto dest:cf2sfile_other' simp:current_files_simps)
lemmas cf2sfile_other'' = cf2sfile_recvmsg cf2sfile_sendmsg cf2sfile_createmsgq cf2sfile_truncate
  cf2sfile_writefile cf2sfile_readfile cf2sfile_ptrace cf2sfile_clone cf2sfile_execve

lemma enrich_msgq_prop:
  "\<lbrakk>valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
   \<Longrightarrow> valid (enrich_msgq s q q') \<and>
       (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and>
       (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and> 
       (\<forall> tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and> 
       (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and>
       (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)"
proof (induct s)
  case Nil
  thus ?case by (auto)
next
  case (Cons e s)
  hence vd_cons': "valid (e # s)" and curq_cons: "q \<in> current_msgqs (e # s)"
    and curq'_cons: "q' \<notin> current_msgqs (e # s)" and nodel_cons: "no_del_event (e # s)"
    and os: "os_grant s e" and grant: "grant s e"  and vd: "valid s"
    by (auto dest:vd_cons vt_grant_os vt_grant)
  from curq'_cons nodel_cons have curq': "q' \<notin> current_msgqs s" by (case_tac e, auto)
  from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto)
  from nodel curq' vd Cons
  have pre: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q') \<and>
     (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and>
     (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and>
     (\<forall>tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and>
     (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and>
     (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)"
    by auto
  
  from pre have pre_vd: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q')" by simp
  from pre have pre_sp: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk>
    \<Longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp" by auto
  from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; q \<in> current_msgqs s\<rbrakk>
    \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" by auto
  from pre have pre_sq: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk>
    \<Longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq" by auto
  from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; q \<in> current_msgqs s\<rbrakk>
    \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by auto
  hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; q \<in> current_msgqs s\<rbrakk>
    \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
  from pre have pre_duq: "q \<in> current_msgqs s \<Longrightarrow> cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q"
    by auto
  have vd_enrich:"q \<in> current_msgqs s \<Longrightarrow> valid (e # enrich_msgq s q q')" 
    apply (frule pre_vd)
    apply (erule_tac s = s and obj' = "E_msgq q'" in enrich_valid_intro_cons)
    apply (simp_all add:pre nodel nodel_cons curq_cons vd_cons' vd enrich_msgq_hungs)
    apply (clarsimp simp:nodel vd curq' enrich_msgq_alive)
    apply (rule allI, rule impI, erule enrich_msgq_not_alive)
    apply (simp_all add:curq' curq'_cons nodel vd enrich_msgq_cur_msgs enrich_msgq_filefd enrich_msgq_flagfd)
    done
  
  have q_neq_q': "q' \<noteq> q" using curq'_cons curq_cons by auto

  have vd_enrich_cons: "valid (enrich_msgq (e # s) q q')"
  proof-
    have "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> valid (enrich_msgq (e # s) q q')"
    proof-
      fix p q'' assume ev: "e = CreateMsgq p q''" 
      show "valid (enrich_msgq (e # s) q q')"
      proof (cases "q'' = q")
        case False with ev vd_enrich curq_cons
        show ?thesis by simp
      next
        case True 
        have "os_grant (CreateMsgq p q # s) (CreateMsgq p q')"
          using os ev
          by (simp add:q_neq_q' curq')
        moreover have "grant (CreateMsgq p q # s) (CreateMsgq p q')"
          using grant ev
          by (auto simp add:sectxt_of_obj_def split:option.splits)
        ultimately 
        show ?thesis using  ev vd_cons' True 
          by (auto intro: valid.intros(2))
      qed
    qed
    moreover have "\<And> p q'' m. \<lbrakk>e = SendMsg p q'' m; q \<in> current_msgqs s\<rbrakk>
      \<Longrightarrow> valid (enrich_msgq (e # s) q q')" 
    proof-
      fix p q'' m assume ev: "e = SendMsg p q'' m" and q_in: "q \<in> current_msgqs s"
      show "valid (enrich_msgq (e # s) q q')"
      proof (cases "q'' = q")
        case False with ev vd_enrich q_in
        show ?thesis by simp
      next
        case True
        from grant os ev True obtain psec qsec 
          where psec: "sectxt_of_obj s (O_proc p) = Some psec"
          and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec"
          by (auto split:option.splits)
        from psec q_in os ev 
        have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec"  
          by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits)
        from qsec q_in pre_duq vd
        have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec"
          by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms')
        show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd 
          curq' psec psec' qsec qsec' grant os q_neq_q'
          apply (simp, erule_tac valid.intros(2))    
          apply (auto simp:q_neq_q' enrich_msgq_cur_msgqs enrich_msgq_cur_procs
            enrich_msgq_cur_msgs sectxt_of_obj_simps)
          done        
      qed
    qed
    moreover have "\<And> p q'' m. \<lbrakk>e = RecvMsg p q'' m; q \<in> current_msgqs s\<rbrakk>
           \<Longrightarrow> valid (enrich_msgq (e # s) q q')"
    proof-
      fix p q'' m assume ev: "e = RecvMsg p q'' m" and q_in: "q \<in> current_msgqs s"
      show "valid (enrich_msgq (e # s) q q')"
      proof (cases "q'' = q")
        case False with ev vd_enrich q_in
        show ?thesis by simp
      next
        case True
        from grant os ev True obtain psec qsec msec
          where psec: "sectxt_of_obj s (O_proc p) = Some psec"
          and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec"
          and msec: "sectxt_of_obj s (O_msg q (hd (msgs_of_queue s q))) = Some msec"
          by (auto split:option.splits)
        from psec q_in os ev 
        have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec"  
          by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits)
        from qsec q_in pre_duq vd
        have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec"
          by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms')
        from qsec q_in vd
        have qsec'': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q) = Some qsec"
          apply (frule_tac pre_sq, simp_all)          
          by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms')
        from msec q_in pre_duq vd qsec qsec' qsec'' curq' nodel
        have msec': "sectxt_of_obj (enrich_msgq s q q') (O_msg q' (hd (msgs_of_queue s q))) = Some msec"
          apply (auto simp:cq2smsgq_def  enrich_msgq_cur_msgs
            split:option.splits dest!:current_has_sms')
          apply (case_tac "msgs_of_queue s q")
          using os ev True apply simp
          apply (simp add:cqm2sms.simps split:option.splits)
          apply (auto simp:cm2smsg_def split:option.splits)
          done          
        show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd 
          curq'  grant os q_neq_q' psec psec' msec msec' qsec qsec'
          apply (simp, erule_tac valid.intros(2))
          apply (auto simp:enrich_msgq_cur_msgqs enrich_msgq_cur_procs
            enrich_msgq_cur_msgs sectxt_of_obj_simps)
          done
      qed
    qed
    ultimately
    show ?thesis using vd_enrich curq_cons vd_cons'
      apply (case_tac e)
      apply (auto simp del:enrich_msgq.simps)
      apply (auto split:if_splits )
      done
  qed

  have curpsec: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> 
    sectxt_of_obj (enrich_msgq s q q') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
    using pre_vd vd
    apply (frule_tac pre_sp, simp)
    by (auto simp:cp2sproc_def split:option.splits if_splits dest!:current_has_sec')    
  have curfsec: "\<And> f. \<lbrakk>is_file s f; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> 
    sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)"
  proof-
    fix f 
    assume a1: "is_file s f" and a2: "q \<in> current_msgqs s"
    from a2 pre_sf pre_vd
    have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"
      and vd_enrich: "valid (enrich_msgq s q q')"
      by auto
    hence csf: "cf2sfile (enrich_msgq s q q') f = cf2sfile s f"
      using a1 by (auto simp:is_file_in_current)
    from a1 obtain sf where csf_some: "cf2sfile s f = Some sf"
      apply (case_tac "cf2sfile s f")
      apply (drule current_file_has_sfile')
      apply (simp add:vd, simp add:is_file_in_current, simp)
      done
    from a1 have a1': "is_file (enrich_msgq s q q') f"
      using vd nodel by (simp add:enrich_msgq_is_file)
    show "sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)"
      using csf csf_some vd_enrich vd a1 a1'
      apply (auto simp:cf2sfile_def split:option.splits if_splits)
      apply (case_tac f, simp_all)
      apply (drule root_is_dir', simp+)
      done
  qed
  have curdsec: "\<And> tf. \<lbrakk>is_dir s tf; q \<in> current_msgqs s\<rbrakk>
    \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
  proof-  
    fix tf 
    assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s"
    from a2 pre_sf pre_vd
    have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"
      and vd_enrich: "valid (enrich_msgq s q q')"
      by auto
    hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf"
      using a1 by (auto simp:is_dir_in_current)
    from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
      apply (case_tac "cf2sfile s tf")
      apply (drule current_file_has_sfile')
      apply (simp add:vd, simp add:is_dir_in_current, simp)
      done      
    from a1 have a1': "is_dir (enrich_msgq s q q') tf"
      using enrich_msgq_is_dir vd nodel by simp
    from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
    from a1' vd have a3': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file)  
    show "sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
      using csf csf_some a3 a3' vd_enrich vd
      apply (auto simp:cf2sfile_def split:option.splits)
      apply (case_tac tf)
      apply (simp add:root_sec_remains, simp)
      done
  qed
  have curpsecs: "\<And> tf ctxts'. \<lbrakk>is_dir s tf; q \<in> current_msgqs s; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk>
    \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'"
  proof-
    fix tf ctxts'
    assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s" 
      and a4: "get_parentfs_ctxts s tf = Some ctxts'"
    from a2 pre
    have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"
      and vd_enrich': "valid (enrich_msgq s q q')"
      by auto
    hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf"
      using a1 by (auto simp:is_dir_in_current)
    from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
      apply (case_tac "cf2sfile s tf")
      apply (drule current_file_has_sfile')
      apply (simp add:vd, simp add:is_dir_in_current, simp)
      done      
    from a1 have a1': "is_dir (enrich_msgq s q q') tf"
      using enrich_msgq_is_dir vd nodel by simp
    from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
    from a1' vd have a5': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) 
    
    from a1' pre_vd a2 obtain ctxts 
      where a3: "get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts"
      apply (case_tac "get_parentfs_ctxts (enrich_msgq s q q') tf")
      apply (drule get_pfs_secs_prop', simp+)
      done
    moreover have "set ctxts = set ctxts'"
    proof (cases tf)
      case Nil          
      with a3 a4 vd vd_enrich'
      show ?thesis
        by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits)
    next
      case (Cons a ff)
      with csf csf_some a5 a5' vd_enrich' vd a3 a4
      show ?thesis
        apply (auto simp:cf2sfile_def split:option.splits if_splits)
        done
    qed
    ultimately 
    show "\<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'"
      by auto        
  qed
    
  have psec_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> 
    sectxt_of_obj (enrich_msgq (e # s) q q') (O_proc tp) = sectxt_of_obj (e # s) (O_proc tp)"
    using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd
    apply (case_tac e)
    apply (auto intro:curpsec simp:sectxt_of_obj_simps)
    apply (frule curpsec, simp, frule curfsec, simp)    
    apply (auto split:option.splits)[1]
    apply (frule vd_cons) defer apply (frule vd_cons)
    apply (auto intro:curpsec simp:sectxt_of_obj_simps)
    done
  

  have sf_cons: "\<And> f. f \<in> current_files (e # s) \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
  proof-
    fix f
    assume a1: "f \<in> current_files (e # s)"
    hence a1': "f \<in> current_files (enrich_msgq (e # s) q q')"
      using nodel_cons os vd vd_cons' vd_enrich_cons
      apply (case_tac e)
      apply (auto simp:current_files_simps enrich_msgq_cur_files dest:is_file_in_current split:option.splits)
      done
    have b1: "\<And> p f' flags fd opt. e = Open p f' flags fd opt \<Longrightarrow> 
      cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
    proof-
      fix p f' flags fd opt 
      assume ev: "e = Open p f' flags fd opt"
      show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
      proof (cases opt)
        case None
        with a1 a1' ev vd_cons' vd_enrich_cons curq_cons
        show ?thesis
          apply (simp add:cf2sfile_open_none)
          apply (simp add:pre_sf current_files_simps)
          done
      next
        case (Some inum)
        show ?thesis
        proof (cases "f = f'")
          case False
          with a1 a1' ev vd_cons' vd_enrich_cons curq_cons Some
          show ?thesis
            apply (simp add:cf2sfile_open)
            apply (simp add:pre_sf current_files_simps)
            done
        next
          case True
          with vd_cons' ev os Some
          obtain pf where pf: "parent f = Some pf" by auto
          then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts"
            using os vd ev Some True
            apply (case_tac "get_parentfs_ctxts s pf")
            apply (drule get_pfs_secs_prop', simp, simp)
            apply auto
            done
            
          have "sectxt_of_obj (Open p f' flags fd (Some inum) # enrich_msgq s q q') (O_file f') = 
                sectxt_of_obj (Open p f' flags fd (Some inum) # s) (O_file f')"
            using Some vd_enrich_cons vd_cons' ev pf True os curq_cons
            by (simp add:sectxt_of_obj_simps curpsec curdsec)
          moreover 
          have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)"
            using curq_cons ev pf Some True os 
            by (simp add:curdsec)
          moreover
          have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts"
            using curq_cons ev pf Some True os vd psecs
            apply (case_tac "get_parentfs_ctxts s pf")
            apply (drule get_pfs_secs_prop', simp+)
            apply (rule curpsecs, simp+)
            done
          then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'"
            and psecs_eq: "set ctxts' = set ctxts" by auto
          ultimately show ?thesis
            using a1 a1' ev vd_cons' vd_enrich_cons Some True pf psecs
            by (simp add:cf2sfile_open split:option.splits)
        qed
      qed
    qed
    have b2: "\<And> p f' inum. e = Mkdir p f' inum \<Longrightarrow> 
      cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
    proof-
      fix p f' inum
      assume ev: "e = Mkdir p f' inum"
      show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
      proof (cases "f' = f")
        case False
        with a1 a1' ev vd_cons' vd_enrich_cons curq_cons
        show ?thesis
          apply (simp add:cf2sfile_mkdir)
          apply (simp add:pre_sf current_files_simps)
          done
      next
        case True
        with vd_cons' ev os
        obtain pf where pf: "parent f = Some pf" by auto
        then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts"
          using os vd ev True
          apply (case_tac "get_parentfs_ctxts s pf")
          apply (drule get_pfs_secs_prop', simp, simp)
          apply auto
          done

        have "sectxt_of_obj (Mkdir p f' inum # enrich_msgq s q q') (O_dir f') = 
          sectxt_of_obj (Mkdir p f' inum # s) (O_dir f')"
          using vd_enrich_cons vd_cons' ev pf True os curq_cons
          by (simp add:sectxt_of_obj_simps curpsec curdsec)
        moreover 
        have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)"
          using curq_cons ev pf True os 
          by (simp add:curdsec)
        moreover
        have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts"
          using curq_cons ev pf True os vd psecs
          apply (case_tac "get_parentfs_ctxts s pf")
          apply (drule get_pfs_secs_prop', simp+)
          apply (rule curpsecs, simp+)
          done
        then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'"
          and psecs_eq: "set ctxts' = set ctxts" by auto
        ultimately show ?thesis
          using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs
          apply (simp add:cf2sfile_mkdir split:option.splits)
          done
      qed
    qed
    have b3: "\<And> p f' f''. e = LinkHard p f' f'' \<Longrightarrow> 
      cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
    proof-
      fix p f' f''
      assume ev: "e = LinkHard p f' f''"
      show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
      proof (cases "f'' = f")
        case False
        with a1 a1' ev vd_cons' vd_enrich_cons curq_cons
        show ?thesis
          apply (simp add:cf2sfile_linkhard)
          apply (simp add:pre_sf current_files_simps)
          done
      next
        case True
        with vd_cons' ev os
        obtain pf where pf: "parent f = Some pf" by auto
        then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts"
          using os vd ev True
          apply (case_tac "get_parentfs_ctxts s pf")
          apply (drule get_pfs_secs_prop', simp, simp)
          apply auto
          done

        have "sectxt_of_obj (LinkHard p f' f'' # enrich_msgq s q q') (O_file f) = 
          sectxt_of_obj (LinkHard p f' f'' # s) (O_file f)"
          using vd_enrich_cons vd_cons' ev pf True os curq_cons
          by (simp add:sectxt_of_obj_simps curpsec curdsec)
        moreover 
        have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)"
          using curq_cons ev pf True os 
          by (simp add:curdsec)
        moreover
        have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts"
          using curq_cons ev pf True os vd psecs
          apply (case_tac "get_parentfs_ctxts s pf")
          apply (drule get_pfs_secs_prop', simp+)
          apply (rule curpsecs, simp+)
          done
        then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'"
          and psecs_eq: "set ctxts' = set ctxts" by auto
        ultimately show ?thesis
          using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs
          apply (simp add:cf2sfile_linkhard split:option.splits)
          done
      qed
    qed
    show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"
      apply (case_tac e)
      prefer 6 apply (erule b1)
      prefer 11 apply (erule b2)
      prefer 11 apply (erule b3)
      apply (simp_all only:b1 b2 b3)
      using a1' a1 vd_enrich_cons vd_cons' curq_cons nodel_cons 
      apply (simp_all add:cf2sfile_other'' cf2sfile_simps enrich_msgq.simps no_del_event.simps split:if_splits)
      apply (simp_all add:pre_sf cf2sfile_other' current_files_simps split:if_splits)
      apply (drule vd_cons, simp add:cf2sfile_other', drule pre_sf, simp+)+
      done
  qed
  
  have sfd_cons:"\<And> tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<Longrightarrow> 
    cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"
  proof-
    fix tp fd f
    assume a1: "file_of_proc_fd (e # s) tp fd = Some f"
    hence a1': "file_of_proc_fd (enrich_msgq (e # s) q q') tp fd = Some f"
      using nodel_cons vd_enrich os vd_cons'
      apply (case_tac e, auto simp:enrich_msgq_filefd simp del:enrich_msgq.simps)
      done
    have b1: "\<And> p f' flags fd' opt. e = Open p f' flags fd' opt \<Longrightarrow> 
      cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"
    proof-
      fix p f' flags fd' opt
      assume ev: "e = Open p f' flags fd' opt"
      have c1': "file_of_proc_fd (Open p f' flags fd' opt # s) tp fd = Some f"
        using a1' ev a1 by (simp split:if_splits)
      show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"        thm cfd2sfd_open
      proof (cases "tp = p \<and> fd = fd'")
        case False
        show ?thesis using ev vd_enrich_cons vd_cons' a1' a1 False curq_cons
          apply (simp add:cfd2sfd_open split:if_splits del:file_of_proc_fd.simps)
          apply (rule conjI, rule impI, simp)
          apply (rule conjI, rule impI, simp)
          apply (auto simp: False  intro!:pre_sfd' split:if_splits)
          done
      next
        case True
        have "f' \<in> current_files (Open p f' flags fd' opt # s)" using ev vd_cons' os
          by (auto simp:current_files_simps is_file_in_current split:option.splits) 
        hence "cf2sfile (Open p f' flags fd' opt # enrich_msgq s q q') f' 
          = cf2sfile (Open p f' flags fd' opt # s) f'"
          using sf_cons ev by auto
        moreover have "sectxt_of_obj (enrich_msgq s q q') (O_proc p) = sectxt_of_obj s (O_proc p)"
          apply (rule curpsec)
          using os ev curq_cons   
          by (auto split:option.splits)
        ultimately show ?thesis
          using ev True a1 a1' vd_enrich_cons vd_cons'
          apply (simp add:cfd2sfd_open sectxt_of_obj_simps del:file_of_proc_fd.simps)
          done
      qed
    qed
    show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"
      apply (case_tac e)
      prefer 6 apply (erule b1)
      using a1' a1 vd_enrich_cons vd_cons' curq_cons
      apply (simp_all only:cfd2sfd_simps enrich_msgq.simps)
      apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits)
      done
  qed

  thm psec_cons
  thm cp2sproc_def
  have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> 
    cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp"
    apply (auto simp add:cpfd2sfds_def)
    sorry
  
  have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"
    by (auto simp:proc_file_fds_def elim!:sfd_cons)
  moreover 
  have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp"
    apply (auto simp:cp2sproc_def pfds_cons psec_cons split:option.splits)
    sorry
  moreover 
  have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq"
    sorry
  moreover 
  have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q"
    sorry
  ultimately show ?case using vd_enrich_cons sf_cons
    by auto
qed


thm cp2sproc_def

(* enrich s target_proc duplicated_pro *)
fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> nat \<Rightarrow> t_state"
where 
  "enrich_proc [] tp dp n = []"
| "enrich_proc (Execve p f fds # s) tp dp n = (
     if (tp = p) 
     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp n)
     else Execve p f fds # (enrich_proc s tp dp n))"
| "enrich_proc (Clone p p' fds # s) tp dp n = (
     if (tp = p') 
     then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
     else Clone p p' fds # (enrich_proc s tp dp n))"
| "enrich_proc (Open p f flags fd opt # s) tp dp n= (
     if (tp = p)
     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp n)
     else Open p f flags fd opt # (enrich_proc s tp dp n))"
| "enrich_proc (ReadFile p fd # s) tp dp n = (
     if (tp = p) 
     then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp n)
     else ReadFile p fd # (enrich_proc s tp dp n))"
| "enrich_proc (RecvMsg p q m # s) tp dp n = (
     if (tp = p) 
     then RecvMsg dp n m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp (n+1)) q n)
     else RecvMsg p q m # (enrich_proc s tp dp n))"
(*
| "enrich_proc (CloseFd p fd # s) tp dp = (
     if (tp = p \<and> fd \<in> proc_file_fds s p)
     then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
     else CloseFd p fd # (enrich_proc s tp dp))"
*)
(*
| "enrich_proc (Attach p h flag # s) tp dp = (
     if (tp = p)
     then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp)
     else Attach p h flag # (enrich_proc s tp dp))"
| "enrich_proc (Detach p h # s) tp dp = (
     if (tp = p) 
     then Detach dp h # Detach p h # (enrich_proc s tp dp)
     else Detach p h # (enrich_proc s tp dp))"
*)
(*
| "enrich_proc (Kill p p' # s) tp dp = (
     if (tp = p') then Kill p p' # s
     else Kill p p' # (enrich_proc s tp dp))"
| "enrich_proc (Exit p # s) tp dp = (
     if (tp = p) then Exit p # s
     else Exit p # (enrich_proc s tp dp))"
*)
| "enrich_proc (e # s) tp dp n = e # (enrich_proc s tp dp n)"

definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
where
  "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"

definition is_created_proc':: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
where
  "is_created_proc' s p \<equiv> p \<in> current_procs s \<and> p \<notin> init_procs"

lemma created_proc_clone:
  "valid (Clone p p' fds # s) \<Longrightarrow> 
   is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)"
apply (drule vt_grant_os)
apply (auto simp:is_created_proc_def dest:not_all_procs_prop2)
using not_died_init_proc
by auto

lemma created_proc_exit: 
  "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)"
by (simp add:is_created_proc_def)

lemma created_proc_kill:
  "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)"
by (simp add:is_created_proc_def)

lemma created_proc_other:
  "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds;
    \<And> p. e \<noteq> Exit p;
    \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp"
by (case_tac e, auto simp:is_created_proc_def)

lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other

lemma no_del_died:
  "\<lbrakk>no_del_event s; died obj s\<rbrakk> \<Longrightarrow> (\<exists> p fd. obj = O_fd p fd \<or> obj = O_tcp_sock (p, fd) \<or> obj = O_udp_sock (p, fd))
  \<or> (\<exists> q m. obj = O_msg q m) "
apply (induct s)
apply simp
apply (case_tac a)
apply (auto split:option.splits)
done

lemma no_del_created_eq:
  "no_del_event s \<Longrightarrow> is_created_proc s p = is_created_proc' s p"
apply (induct s)
apply (simp add:is_created_proc_def is_created_proc'_def)
apply (case_tac a)
apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
done

lemma enrich_proc_dup_in:
  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p' i)"
apply (induct s, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a)
apply ( auto simp:is_created_proc_def Let_def enrich_msgq_cur_procs
  dest:not_all_procs_prop3)
sorry

lemma enrich_proc_dup_ffd:
  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f"
apply (induct s, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
  dest:not_all_procs_prop3 split:if_splits option.splits)
sorry

lemma enrich_proc_dup_ffd':
  "\<lbrakk>file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
    no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> file_of_proc_fd s p fd = Some f"
apply (induct s, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
  dest:not_all_procs_prop3 split:if_splits option.splits)
sorry

lemma enrich_proc_dup_ffd_eq:
  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = file_of_proc_fd s p fd"
apply (case_tac "file_of_proc_fd s p fd")
apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p' i) p' fd")
apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
apply (drule_tac i = i in enrich_proc_dup_ffd, simp+)
done

lemma enrich_proc_cur_msgqs:
  "\<lbrakk>valid s\<rbrakk> \<Longrightarrow> current_msgqs (enrich_proc s p p' i) = current_msgqs s \<union> {q'. q' \<ge> new_msgq s \<and> q' \<le> new_msgq s + (nums_of_recvmsg s p) - 1}"
apply (induct s, simp)
apply (auto)[1]
apply (drule new_msgq_1, simp, simp)
apply (frule vt_grant_os, frule vd_cons)
sorry

lemma enrich_proc_not_alive:
  "\<lbrakk>enrich_not_alive s (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj; 
    is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
  \<Longrightarrow> enrich_not_alive (enrich_proc s p p' (new_msgq s)) (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj"
apply (case_tac obj, simp_all)
prefer 5
apply (simp add:enrich_proc_cur_msgqs)
apply (rule impI, rule notI)
apply simp
apply (auto)[1]
defer
apply simp
apply (rule impI, rule notI)
defer
apply (subgoal_tac "new_msgq s \<noteq> 0")
apply simp
apply arith
apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
  enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
defer
apply (rule impI, rule notI)
sorry


lemma enrich_proc_dup_fflags:
  "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
   \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
       flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
apply (induct s arbitrary:p, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def Let_def
  dest:not_all_procs_prop3 split:if_splits option.splits)
sorry

lemma enrich_proc_dup_ffds:
  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
apply (auto simp:proc_file_fds_def)
apply (rule_tac x = f in exI) 
apply (erule enrich_proc_dup_ffd', simp+)
apply (rule_tac x = f in exI)
apply (erule enrich_proc_dup_ffd, simp+)
done

lemma enrich_proc_dup_ffds_eq_fds:
  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_proc_fds (enrich_proc s p p') p' = proc_file_fds s p"
apply (induct s arbitrary:p)
apply (simp add: is_created_proc_def)
apply (frule not_all_procs_prop3)
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
  simp:proc_file_fds_def is_created_proc_def Let_def)
sorry

lemma enrich_proc_dup_ffds':
  "\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
apply (auto simp:enrich_proc_dup_ffds_eq_fds)
apply (simp add:proc_file_fds_def)
done

lemma enrich_proc_cur_inof:
  "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
apply (induct s arbitrary:f)
apply simp
apply (frule vd_cons, frule vt_grant_os, frule vt_grant)
apply (case_tac a, auto)
apply (auto split:option.splits simp del:grant.simps simp add:Let_def)
sorry

lemma not_all_procs_sock:
  "\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
apply (frule not_all_procs_prop3)
apply (case_tac "inum_of_socket s (p', fd)", simp_all)
apply (drule cn_in_curp', simp+)
done

lemma enrich_proc_cur_inos:
  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   \<Longrightarrow> inum_of_socket (enrich_proc s p p') (tp, fd) = inum_of_socket s (tp, fd)"
apply (induct s arbitrary:tp)
apply simp
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:option.splits simp:not_all_procs_sock Let_def)
apply (simp add:proc_file_fds_def, erule exE)
apply (case_tac "inum_of_socket s (nat1, fd)", simp_all)
apply (drule filefd_socket_conflict, simp_all add:current_sockets_def)
sorry

lemma enrich_proc_cur_inums:
  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
   \<Longrightarrow> current_inode_nums (enrich_proc s p p') = current_inode_nums s"
apply (auto simp:current_inode_nums_def current_file_inums_def 
  current_sock_inums_def enrich_proc_cur_inof enrich_proc_cur_inos)
done

lemma enrich_proc_cur_itag:
  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   \<Longrightarrow> itag_of_inum (enrich_proc s p p') i = itag_of_inum s i"
apply (induct s)
apply simp
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:option.splits t_socket_type.splits simp:Let_def)
sorry

lemma enrich_proc_cur_tcps:
  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   \<Longrightarrow> is_tcp_sock (enrich_proc s p p') = is_tcp_sock s"
apply (rule ext, case_tac x)
apply (auto simp add:is_tcp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
  split:option.splits t_inode_tag.splits)
done

lemma enrich_proc_cur_udps:
  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   \<Longrightarrow> is_udp_sock (enrich_proc s p p') = is_udp_sock s"
apply (rule ext, case_tac x)
apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos 
  split:option.splits t_inode_tag.splits)
done

lemma enrich_proc_cur_msgqs:
  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (enrich_proc s p p')"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:Let_def)
sorry

lemma enrich_proc_cur_msgs:
  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q"
apply (induct s, simp)
apply (frule_tac p = p and p' = p' in enrich_proc_cur_msgqs, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:Let_def)
sorry

lemma enrich_proc_cur_procs:
  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk> 
   \<Longrightarrow> current_procs (enrich_proc s p p') = current_procs s \<union> {p'}"
apply (induct s, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:is_created_proc_simps Let_def)
sorry

lemma enrich_proc_cur_files:
  "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
apply (auto simp:current_files_def)
apply (simp add: enrich_proc_cur_inof)+
done

lemma enrich_proc_cur_fds1:
  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<in> current_procs s\<rbrakk>
   \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
apply (induct s, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (frule not_all_procs_prop3)
apply (case_tac a)
sorry
(*
apply (auto simp:is_created_proc_simps)
done
*)

lemma enrich_proc_cur_fds1':
  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<noteq> p'\<rbrakk>
   \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
apply (induct s, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (frule not_all_procs_prop3) sorry  (*
apply (case_tac a)
apply (auto simp:is_created_proc_simps)
done
*)

lemma enrich_proc_cur_fds:
  "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
   \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = (if (tp = p') then proc_file_fds s p else current_proc_fds s tp)"
apply (simp add:enrich_proc_cur_fds1' enrich_proc_dup_ffds_eq_fds split:if_splits)
done

lemma enrich_proc_not_alive:
  "\<lbrakk>enrich_not_alive s (E_proc p') obj; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
  \<Longrightarrow> enrich_not_alive (enrich_proc s p p') (E_proc p') obj"
apply (case_tac obj)
apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
  enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
defer
apply (rule impI, rule notI)
sorry

lemma enrich_proc_filefd:
  "\<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
apply (induct s arbitrary:tp, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (frule not_all_procs_prop3)
apply (case_tac a)
apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs split:if_splits)
sorry

lemma enrich_proc_flagfd:
  "\<lbrakk>flags_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
  \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some f"
apply (induct s arbitrary:tp, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (frule not_all_procs_prop3)
apply (case_tac a)
apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs current_fflag_has_ffd split:if_splits option.splits)
sorry

lemma enrich_proc_hungs:
  "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto simp:files_hung_by_del.simps)
sorry

lemma enrich_proc_is_file:
  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   \<Longrightarrow> is_file (enrich_proc s p p') = is_file s"
apply (rule ext, case_tac x)
apply (auto simp add:is_file_def enrich_proc_cur_itag enrich_proc_cur_inof
  split:option.splits t_inode_tag.splits)
done

lemma enrich_proc_is_dir:
  "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
   \<Longrightarrow> is_dir (enrich_proc s p p') = is_dir s"
apply (rule ext, case_tac x)
apply (auto simp add:is_dir_def enrich_proc_cur_itag enrich_proc_cur_inof
  split:option.splits t_inode_tag.splits)
done

lemma enrich_proc_alive:
  "\<lbrakk>alive s obj; valid s; is_created_proc s p; p' \<notin> all_procs s; no_del_event s\<rbrakk>
   \<Longrightarrow> alive (enrich_proc s p p') obj"
apply (case_tac obj)
apply (simp_all add:enrich_proc_is_file enrich_proc_is_dir enrich_proc_cur_msgqs 
  enrich_proc_cur_msgs enrich_proc_cur_procs enrich_proc_cur_fds
  enrich_proc_cur_tcps enrich_proc_cur_udps)
apply (rule impI, simp)
apply (drule current_proc_fds_in_curp, simp, simp add:not_all_procs_prop3)
done

lemma enrich_proc_prop:
  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s; no_del_event s\<rbrakk>
   \<Longrightarrow> valid (enrich_proc s p p') \<and> 
       (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
       (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> 
       (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> 
       (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>
       (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
       (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
proof (induct s)
  case Nil
  thus ?case by (auto simp:is_created_proc_def)
next
  case (Cons e s)
  hence vd_cons': "valid (e # s)" and created_cons: "is_created_proc (e # s) p"
    and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" 
    and os: "os_grant s e" and grant: "grant s e" 
    and nodel_cons: "no_del_event (e # s)"
    by (auto dest:vd_cons' vt_grant_os vt_grant)
  from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto)
  from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto)
  from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and>
     (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
     (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
     (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and>
     (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>     
     (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
     (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
    using vd all_procs nodel by auto
  
  from pre have pre_vd: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
  have vd_enrich:"is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" 
    apply (frule pre_vd)
    apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)
    apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
    apply (clarsimp simp:enrich_proc_alive nodel all_procs vd)
    apply (rule allI, rule impI, erule enrich_proc_not_alive)
    apply (simp_all add:nodel all_procs vd enrich_proc_hungs enrich_proc_cur_msgs)
    apply ((rule allI| rule impI)+, erule enrich_proc_filefd)
    apply (simp_all add:nodel all_procs vd)
    apply ((rule allI| rule impI)+, erule enrich_proc_flagfd)
    apply (simp_all add:nodel all_procs vd)
    done  
  have vd_enrich_cons: "valid (enrich_proc (e # s) p p')"
  proof-
    have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p; 
      valid (Execve p f fds # s); p' \<notin> all_procs s\<rbrakk>
      \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
    proof-
      fix f fds
      assume a1: "valid (Execve p f fds # enrich_proc s p p')" and a2: "is_created_proc s p"
        and a3: "valid (Execve p f fds # s)" and a0: "p' \<notin> all_procs s"
      have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
        and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
        and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
        and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
        and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
        using pre a2
        by auto
      show "valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
      proof-
        from a0 a3 have a0': "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3)
        from a3 have grant: "grant s (Execve p f fds)" and os: "os_grant s (Execve p f fds)"
          by (auto dest:vt_grant_os vt_grant simp del:os_grant.simps)
        have f_in: "is_file (enrich_proc s p p') f"
          using vd nodel os all_procs
          by (auto dest:vt_grant_os simp:enrich_proc_is_file)
        moreover have a5: "proc_file_fds s p \<subseteq> proc_file_fds (Execve p f fds # enrich_proc s p p') p'" 
          using a3 a0'
          apply (frule_tac vt_grant_os)
          apply (auto simp:proc_file_fds_def)
          apply (rule_tac x = fa in exI)
          apply (erule enrich_proc_dup_ffd)
          apply (simp_all add:vd all_procs a2)
          done
        ultimately have "os_grant (Execve p f fds # enrich_proc s p p') (Execve p' f (fds \<inter> proc_file_fds s p))"
          apply (auto simp:is_file_simps enrich_proc_dup_in a2 vd all_procs a1 enrich_proc_dup_ffds)
          done
        moreover have "grant (Execve p f fds # enrich_proc s p p') (Execve p' f (fds \<inter> proc_file_fds s p))"
        proof-
          from grant obtain up rp tp uf rf tf 
            where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"
            and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 
            by (simp split:option.splits, blast)
          with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)"
            by (simp split:option.splits del:npctxt_execve.simps, blast)
          have p1': "sectxt_of_obj (Execve p f fds # enrich_proc s p p') (O_proc p') = Some (up, rp, tp)"
            using p1 dup_sp a1 a0'
            apply (simp add:sectxt_of_obj_simps)
            by (simp add:cp2sproc_def split:option.splits)
          from os have f_in': "is_file s f"  by simp 
          from vd os have "\<exists> sf. cf2sfile s f = Some sf"
            by (auto dest!:is_file_in_current current_file_has_sfile)
          hence p2': "sectxt_of_obj (Execve p f fds # enrich_proc s p p') (O_file f) = Some (uf, rf, tf)" 
            using f_in p2 cf2sf os a1
            apply (erule_tac x = f in allE)
            apply (auto dest:is_file_in_current simp:cf2sfile_def sectxt_of_obj_simps split:option.splits)
            apply (case_tac f, simp)
            apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)
            done 
          from dup_sfd a5 have "\<forall>fd. fd \<in> proc_file_fds s p \<longrightarrow> 
            cfd2sfd (Execve p f fds # enrich_proc s p p') p' fd = cfd2sfd s p fd"
            apply (rule_tac allI)
            apply (erule_tac x = fd in allE, clarsimp)
            apply (drule set_mp, simp)
            apply (auto simp:cfd2sfd_execve proc_file_fds_def a1)
            done
          hence "inherit_fds_check (Execve p f fds # enrich_proc s p p') (up, nr, nt) p' (fds \<inter> proc_file_fds s p)"
            using grant os p1 p2 p3 vd
            apply (clarsimp)
            apply (rule_tac s = s and p = p and fds = fds in enrich_inherit_fds_check_dup)
            apply simp_all
            done
          moreover have "search_check (Execve p f fds # enrich_proc s p p') (up, rp, tp) f"
            using p1 p2 p2' vd cf2sf f_in f_in' grant p3 f_in a1
            apply (rule_tac s = s in enrich_search_check)
            apply (simp_all add:is_file_simps)
            apply (rule allI, rule impI, erule_tac x = fa in allE, simp)
            apply (drule_tac ff = fa in cf2sfile_other')
            apply (auto simp:a2 enrich_proc_cur_files nodel)
            done
          ultimately show ?thesis 
            using p1' p2' p3
            apply (simp split:option.splits)
            using grant p1 p2
            apply simp
            done
        qed
        ultimately show ?thesis using a1
          by (erule_tac valid.intros(2), auto)
      qed
    qed
    moreover have "\<And>tp fds. \<lbrakk>valid (Clone tp p fds # s); p' \<noteq> p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> 
      valid (Clone tp p' (fds \<inter> proc_file_fds s tp) # Clone tp p fds # s)"
      apply (frule vt_grant_os, frule vt_grant, drule not_all_procs_prop3)
      apply (rule valid.intros(2))
      apply (simp_all split:option.splits add:sectxt_of_obj_simps)
      apply (auto simp add:proc_file_fds_def)[1]
      apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def)
      done
    moreover have "\<And>f flags fd opt. \<lbrakk>valid (Open p f flags fd opt # enrich_proc s p p'); 
      is_created_proc s p; valid (Open p f flags fd opt # s); p' \<notin> all_procs s\<rbrakk>
       \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')"
    proof-
      fix f flags fd opt
      assume a1: "valid (Open p f flags fd opt # enrich_proc s p p')" and a2: "is_created_proc s p"
        and a3: "valid (Open p f flags fd opt # s)" and a4: "p' \<notin> all_procs s"
      have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
        and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
        and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
        and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
        and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
        using pre a2 by auto
      from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3 split:option.splits)
      have a5: "p' \<in> current_procs (enrich_proc s p p')" 
        using a2 a3 vd
        apply (erule_tac enrich_proc_dup_in)
        by (simp_all add:vd a4)
      have a6: "is_file (Open p f flags fd opt # enrich_proc s p p') f"
        using a1 a3
        by (auto simp:is_file_open dest:vt_grant_os)
      have a7: "fd \<notin> current_proc_fds (enrich_proc s p p') p'"
        using a2 a4 vd nodel
        apply (simp add:enrich_proc_dup_ffds_eq_fds)
        apply (rule notI)
        apply (drule_tac p = p in file_fds_subset_pfds)
        apply (drule set_mp, simp)
        using a3
        apply (drule_tac vt_grant_os)
        apply (auto split:option.splits)
        done
      from a1 have a8: "valid (enrich_proc s p p')" by (erule_tac valid.cases, auto)
      from a3 have grant: "grant s (Open p f flags fd opt)" and os: "os_grant s (Open p f flags fd opt)"
        by (auto dest:vt_grant_os vt_grant)
      show "valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')"
      proof (cases opt)
        case None
        have f_in: "is_file (enrich_proc s p p') f"
          using vd nodel os all_procs None
          by (auto dest:vt_grant_os simp:enrich_proc_is_file) 
        from grant None obtain up rp tp uf rf tf 
          where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"
          and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" 
          apply (simp split:option.splits)
          by (case_tac a, case_tac aa, blast)
        have p1': "sectxt_of_obj (Open p f flags fd opt # enrich_proc s p p') (O_proc p') = Some (up, rp, tp)"
          using p1 dup_sp a1
          apply (simp add:sectxt_of_obj_simps)
          by (simp add:cp2sproc_def split:option.splits)
        from os None have f_in': "is_file s f" by simp 
        from vd os None have "\<exists> sf. cf2sfile s f = Some sf"
          by (auto dest!:is_file_in_current current_file_has_sfile)
        hence p2': "sectxt_of_obj (Open p f flags fd opt # enrich_proc s p p') (O_file f) = Some (uf, rf, tf)" 
          using p2 cf2sf os a1 None f_in' vd f_in
          apply (erule_tac x = f in allE)
          apply (auto dest:is_file_in_current simp:cf2sfile_def sectxt_of_obj_simps split:option.splits)
          apply (case_tac f, simp)
          apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)
          done 
        have "search_check (Open p f flags fd opt # enrich_proc s p p') (up, rp, tp) f"
          using p1 p2 p2' vd cf2sf f_in f_in' grant f_in a1 None
          apply (rule_tac s = s in enrich_search_check)
          apply (simp_all add:is_file_simps)
          apply (rule allI, rule impI, erule_tac x = fa in allE, simp)
          apply (simp add:cf2sfile_open_none)
          done
        thus ?thesis using a0 a5 a6 a7 None a1
          apply (rule_tac valid.intros(2))
          apply (simp_all add:a1)
          apply (case_tac flags, simp add:is_creat_excl_flag_def)
          using p1' p2'
          apply simp
          using grant p1 p2
          apply (simp add:oflags_check_remove_create)
          done
      next
        case (Some inum)
        with os obtain pf where parent: "parent f = Some pf" by auto
        with grant Some obtain pu rp pt pfu pfr pft where
          p1: "sectxt_of_obj s (O_proc p) = Some (pu, rp, pt)" 
          and p2: "sectxt_of_obj s (O_dir pf) = Some (pfu, pfr, pft)"
          apply (simp split:option.splits)
          apply (case_tac a, case_tac aa, blast)
          done
        from p1 have p1': "sectxt_of_obj (enrich_proc s p p') (O_proc p) = Some (pu, rp, pt)"
          using cp2sp os
          apply (erule_tac x = p in allE)
          apply (auto split:option.splits simp:cp2sproc_def)
          done
        from os parent Some
        have pf_in: "is_dir s pf" by auto
        hence "\<exists> sf. cf2sfile s pf = Some sf" using vd
          by (auto dest!:is_dir_in_current current_file_has_sfile)
        from a1 parent Some have pf_in': "is_dir (enrich_proc s p p') pf" 
          apply (frule_tac vt_grant_os)
          by (clarsimp)
        have p2': "sectxt_of_obj (enrich_proc s p p') (O_dir pf) = Some (pfu, pfr, pft)"
        proof-
          have "cf2sfile (enrich_proc s p p') pf = cf2sfile s pf"
            using cf2sf pf_in
            apply (drule_tac is_dir_in_current)
            apply (erule_tac x = pf in allE)
            by simp
          with pf_in pf_in' p2 vd Some a8
          show ?thesis            
            apply (frule_tac is_dir_not_file)
            apply (frule_tac s = "enrich_proc s p p'" in is_dir_not_file)
            apply (simp add:cf2sfile_def)
            apply (case_tac pf, simp) 
            apply (simp add:sroot_def root_sec_remains)            
            by (auto split:option.splits dest!:current_has_sec' get_pfs_secs_prop' dest:parentf_is_dir_prop1)        
        qed
        from p1 have dup: "sectxt_of_obj (Open p f flags fd (Some inum) # enrich_proc s p p') (O_proc p') 
          = Some (pu, rp, pt)"
          using a1 Some
          apply (simp add:sec_open)
          using dup_sp
          apply (auto split:option.splits if_splits simp:cp2sproc_def)
          done        
        have nsf: "sectxt_of_obj (Open p f flags fd (Some inum) # enrich_proc s p p') (O_file f) 
          = Some (pu, R_object, type_transition pt pft C_file True)"
          using a1 Some p1 p2 parent p2' p1'
          by (simp add:sec_open)
        have "search_check (Open p f flags fd (Some inum) # enrich_proc s p p') (pu, rp, pt) f"
        proof-
          have "search_check (Open p f flags fd (Some inum) # enrich_proc s p p') (pu, rp, pt) pf"
            using grant Some parent p1 p2 vd a1 pf_in pf_in' p2'
            apply simp 
            apply (rule_tac s = s in enrich_search_check') 
            apply (simp_all add:is_dir_simps sectxt_of_obj_simps)
            apply (rule allI, rule impI)
            apply (case_tac "fa = f")
            using os Some
            apply simp
            apply (drule_tac f' = fa in cf2sfile_open)
            apply (simp add:current_files_simps)
            using enrich_proc_cur_files a2 nodel
            apply simp
            apply simp
            using cf2sf
            apply simp
            done
          moreover have "is_file (Open p f flags fd (Some inum) # enrich_proc s p p') f"
            using a1 Some
            by (simp add:is_file_open)
          ultimately 
          show ?thesis
            using parent a1 Some nsf
            apply (erule_tac search_check_leveling_f)
            apply (simp_all)
            apply (simp add:search_check_file_def)
            (* create new file, grant only check pf's SEARCH permission, not newfile itself, so we make assumptions of this case in the locale *)
            apply (simp add:permission_check.simps)
            sorry
        qed
        thus ?thesis using a0 a5 a6 a7 a1 Some
          apply (rule_tac valid.intros(2))
          apply (simp add:a1)
          apply simp
          apply (case_tac flags, simp add:is_creat_excl_flag_def)
          using grant p1 p2 parent dup nsf
          apply (simp add:oflags_check_remove_create)
          done
      qed
    qed
    moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p; 
      valid (CloseFd p fd # s); p' \<notin> all_procs s; fd \<in> proc_file_fds s p\<rbrakk>
      \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
    proof-
      fix fd
      assume a1: "valid (CloseFd p fd # enrich_proc s p p')" and a2: "is_created_proc s p" 
        and a3: "p' \<notin> all_procs s" and a4: "valid (CloseFd p fd # s)"
        and a5: "fd \<in> proc_file_fds s p"
      from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3)
      have "p' \<in> current_procs (enrich_proc s p p')" 
        using a2 a3 vd
        by (auto intro:enrich_proc_dup_in)
      moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'"      
        using a5 a2 a3 vd pre_vd nodel
        apply (simp)
        apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds)
        apply (erule set_mp)
        apply (simp add:enrich_proc_dup_ffds)
        done
      ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
        apply (rule_tac valid.intros(2))
        apply (simp_all add:a1 a0 a2 pre_vd)
        done
    qed
    moreover have "\<And> fd. \<lbrakk>valid (ReadFile p fd # enrich_proc s p p');
            is_created_proc s p; valid (ReadFile p fd # s); p' \<notin> all_procs s\<rbrakk>
           \<Longrightarrow> valid (ReadFile p' fd # ReadFile p fd # enrich_proc s p p')"
    proof-
      fix fd
      assume a1: "valid (ReadFile p fd # enrich_proc s p p')" and a2: "is_created_proc s p"
        and a3: "valid (ReadFile p fd # s)" and a4: "p' \<notin> all_procs s"
      from a3 have os: "os_grant s (ReadFile p fd)" and grant: "grant s (ReadFile p fd)"
        by (auto dest:vt_grant_os vt_grant)
      have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
        and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
        and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
        and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
        and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
        using pre a2 by auto
      have vd_enrich: "valid (enrich_proc s p p')" using a1 by (auto dest:valid.cases)
      show "valid (ReadFile p' fd # ReadFile p fd # enrich_proc s p p')"
      proof-
        have "os_grant (ReadFile p fd # enrich_proc s p p') (ReadFile p' fd)"
          using a1 a2 a4 vd os nodel
          apply (clarsimp simp:current_files_simps enrich_proc_dup_in enrich_proc_dup_ffds_eq_fds)
          apply (simp add:proc_file_fds_def)
          apply (rule conjI)
          apply (rule_tac x = f in exI, simp add:enrich_proc_dup_ffd)
          using enrich_proc_cur_files
          apply (simp)
          apply (drule enrich_proc_dup_fflags)
          apply simp_all
          apply (erule disjE)
          apply auto
          apply (simp add:is_read_flag_def)
          done
        moreover have "grant (ReadFile p fd # enrich_proc s p p') (ReadFile p' fd)"
        proof-
          from grant obtain f sp sfd sf where p1: "file_of_proc_fd s p fd = Some f"
            and p2: "sectxt_of_obj s (O_proc p) = Some sp" 
            and p3: "sectxt_of_obj s (O_fd p fd) = Some sfd"
            and p4: "sectxt_of_obj s (O_file f) = Some sf"
            by (auto split:option.splits) 
          from os obtain flag where p0: "flags_of_proc_fd s p fd = Some flag"
            by auto
          from os have f_in_s: "f \<in> current_files s" using p1 by simp
          from p1 vd have isfile_s: "is_file s f" by (erule_tac file_of_pfd_is_file, simp)
          hence isfile_s': "is_file (enrich_proc s p p') f"
            using vd nodel all_procs a2
            by (auto simp:enrich_proc_is_file) 
          from p0 obtain flag' where p0': "flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag'"
            and p0'': "(flag' = flag) \<or> (flag' = remove_create_flag flag)"
            using a2 a4 vd
            apply (drule_tac enrich_proc_dup_fflags)
            apply auto
            apply (case_tac flag, auto)
            apply (case_tac flag, auto)
            done            
          from p1 have p1': "file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
            using a2 a4 vd
            by (simp add:enrich_proc_dup_ffd)
          from p2 have p2': "sectxt_of_obj (enrich_proc s p p') (O_proc p') = Some sp"
            using dup_sp
            by (auto simp:cp2sproc_def split:option.splits)
          from p3 p1 p1' p0 p0' os have p3': "sectxt_of_obj (enrich_proc s p p') (O_fd p' fd) = Some sfd"
            using dup_sfd
            apply (erule_tac x = fd in allE)
            apply (auto simp:proc_file_fds_def cfd2sfd_def split:option.splits)
            apply (drule current_file_has_sfile')
            apply (simp add:vd, simp)
            apply (drule current_file_has_sfile')
            apply (simp add:vd, simp)
            done
          from p4 have p4': "sectxt_of_obj (enrich_proc s p p') (O_file f) = Some sf" 
            using f_in_s cf2sf isfile_s isfile_s' a1 vd_enrich vd
            apply (erule_tac x = f in allE)
            apply (simp)
            apply (auto simp:cf2sfile_def split:option.splits 
              dest!:current_has_sec' get_pfs_secs_prop' dest:parentf_is_dir is_file_in_current)
            apply (case_tac f, simp, drule root_is_dir', simp, simp, simp)
            done
          show ?thesis using p1' p2' p3' p4' a1
            apply (simp add:sectxt_of_obj_simps)
            using grant p1 p2 p3 p4 
            apply simp
            done
        qed
        ultimately show ?thesis
          using a1
          by (erule_tac valid.intros(2), simp+)
      qed
    qed
    ultimately show ?thesis 
      using vd_enrich created_cons vd_cons' all_procs_cons
      apply (case_tac e)
      apply (auto simp:is_created_proc_simps split:if_splits)
      done
  qed
  have sec_proc:
    "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> 
    \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
    using pre 
    apply (clarsimp)
    apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)
    done
  have sf_cons:
    "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
  proof clarify
    fix f 
    assume a1: "f \<in> current_files (e # s)"
    from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; is_created_proc s p\<rbrakk>
      \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
      by auto
    from a1 have a1': "f \<in> current_files (enrich_proc (e # s) p p')"
      using vd_cons' nodel_cons
      by (simp add:enrich_proc_cur_files)
    from a1 have a1'': "f \<in> current_files (e # enrich_proc s p p')"
      using vd_cons' nodel_cons os vd vd_enrich created_cons
      apply (case_tac e)
      apply (auto simp:enrich_proc_cur_files current_files_simps is_created_proc_simps
        dest:is_file_in_current is_dir_in_current split:option.splits)
      done
    
    have sec_dir:
      "\<And> tf. \<lbrakk>is_dir s tf; is_created_proc s p\<rbrakk>
      \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
    proof-
      fix tf 
      assume a1: "is_dir s tf" and a2: "is_created_proc s p"
      from a2 pre
      have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
        and vd_enrich: "valid (enrich_proc s p p')"
        by auto
      hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
        using a1 by (auto simp:is_dir_in_current)
      from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
        apply (case_tac "cf2sfile s tf")
        apply (drule current_file_has_sfile')
        apply (simp add:vd, simp add:is_dir_in_current, simp)
        done      
      from a1 have a1': "is_dir (enrich_proc s p p') tf"
        using enrich_proc_is_dir vd nodel all_procs by simp
      from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
      from a1' vd have a3': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file)  
      show "sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
        using csf csf_some a3 a3' vd_enrich vd
        apply (auto simp:cf2sfile_def split:option.splits)
        apply (case_tac tf)
        apply (simp add:root_sec_remains, simp)
        done
    qed
    have sec_file:
      "\<And> tf. \<lbrakk>is_file s tf; is_created_proc s p\<rbrakk>
      \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"
    proof-
      fix tf 
      assume a1: "is_file s tf" and a2: "is_created_proc s p"
      from a2 pre
      have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
        and vd_enrich: "valid (enrich_proc s p p')"
        by auto
      hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
        using a1 by (auto simp:is_file_in_current)
      from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
        apply (case_tac "cf2sfile s tf")
        apply (drule current_file_has_sfile')
        apply (simp add:vd, simp add:is_file_in_current, simp)
        done
      from a1 have a1': "is_file (enrich_proc s p p') tf"
        using vd nodel all_procs by (simp add:enrich_proc_is_file)
      show "sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"
        using csf csf_some vd_enrich vd a1 a1'
        apply (auto simp:cf2sfile_def split:option.splits if_splits)
        apply (case_tac tf, simp_all)
        apply (drule root_is_dir', simp+)
        done
    qed
    have secs_dir:
      "\<And> tf ctxts'. \<lbrakk>is_dir s tf; is_created_proc s p; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk>
       \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"
    proof-
      fix tf ctxts'
      assume a1: "is_dir s tf" and a2: "is_created_proc s p" 
        and a4: "get_parentfs_ctxts s tf = Some ctxts'"
      from a2 pre
      have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
        and vd_enrich': "valid (enrich_proc s p p')"
        by auto
      hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
        using a1 by (auto simp:is_dir_in_current)
      from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
        apply (case_tac "cf2sfile s tf")
        apply (drule current_file_has_sfile')
        apply (simp add:vd, simp add:is_dir_in_current, simp)
        done      
      from a1 have a1': "is_dir (enrich_proc s p p') tf"
        using enrich_proc_is_dir vd nodel all_procs by simp
      from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
      from a1' vd have a5': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file) 
      
      from a1' pre_vd a2 obtain ctxts 
        where a3: "get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts"
        apply (case_tac "get_parentfs_ctxts (enrich_proc s p p') tf")
        apply (drule get_pfs_secs_prop', simp+)
        done
      moreover have "set ctxts = set ctxts'"
      proof (cases tf)
        case Nil          
        with a3 a4 vd vd_enrich'
        show ?thesis
          by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits)
      next
        case (Cons a ff)
        with csf csf_some a5 a5' vd_enrich' vd a3 a4
        show ?thesis
          apply (auto simp:cf2sfile_def split:option.splits if_splits)
          done
      qed
      ultimately 
      show "\<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"
        by auto        
    qed
    have b1: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 
      \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
    proof-
      fix proc f' flags fd' opt
      assume ev: "e = Open proc f' flags fd' opt"
      have b1': "cf2sfile (e # enrich_proc s p p') f = cf2sfile (e # s) f"
      proof (cases opt)
        case None
        thus ?thesis
          using vd_cons' vd_enrich a1 created_cons 
          by (simp add:cf2sfile_open_none ev pre_sf 
            is_created_proc_simps current_files_simps)
      next
        case (Some inum)
        show ?thesis
        proof (cases "f' = f")
          case True
          from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
            apply (case_tac "cf2sfile (e # s) f")
            apply (drule current_file_has_sfile')
            apply (simp add:vd_cons', simp, simp)
            done
          from a1 ev os Some True obtain pf where parent: "parent f = Some pf"
            and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
          have f_in: "f \<in> current_files (e # enrich_proc s p p')"
            using ev True Some
            by (simp add:current_files_open)
          thus ?thesis using ev Some csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
            apply (simp add:is_created_proc_simps cf2sfile_open)
            apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
            apply (drule_tac tf = pf in secs_dir, simp+) 
            apply (erule exE, erule conjE, simp)
            apply (case_tac aa, simp)
            done
        next
          case False
          have f_in: "f \<in> current_files (e # enrich_proc s p p')"
            using ev False Some vd_enrich a1 created_cons nodel vd
            by (simp add:current_files_open is_created_proc_simps enrich_proc_cur_files)
          with ev Some a1 vd_enrich vd_cons' created_cons False
          show ?thesis
            apply (simp add:is_created_proc_simps cf2sfile_open)
            apply (simp add:current_files_simps pre_sf)
            done
        qed
      qed
      show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" 
        using ev vd_enrich_cons
        apply simp
        apply (rule conjI, rule impI)
        apply (simp add:cf2sfile_open_none)
        using b1' apply (auto dest:vd_cons)
        done
    qed
    have b2: "\<And> proc f' inum. e = Mkdir proc f' inum
      \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
    proof-
      fix proc f' inum
      assume ev: "e = Mkdir proc f' inum"
      
      show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
      proof (cases "f' = f")
        case True
        from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
          apply (case_tac "cf2sfile (e # s) f")
          apply (drule current_file_has_sfile')
          apply (simp add:vd_cons', simp, simp)
          done
        from a1 ev os True obtain pf where parent: "parent f = Some pf"
          and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
          using ev True
          by (simp add:current_files_mkdir)
        thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
          apply (simp add:is_created_proc_simps cf2sfile_mkdir)
          apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
          apply (drule_tac tf = pf in secs_dir, simp+) 
          apply (erule exE, erule conjE, simp)
          apply (case_tac aa, simp)
          done
      next
        case False
        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
          using ev False vd_enrich a1 created_cons nodel vd
          by (simp add:current_files_mkdir is_created_proc_simps enrich_proc_cur_files)
        with ev a1 vd_enrich vd_cons' created_cons False
        show ?thesis
          apply (simp add:is_created_proc_simps cf2sfile_mkdir)
          apply (simp add:current_files_simps pre_sf)
          done
      qed
    qed
    have b3: "\<And> proc f' f''. e = LinkHard proc f' f''
      \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
    proof-
      fix proc f' f'' 
      assume ev: "e = LinkHard proc f' f''"      
      show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
      proof (cases "f'' = f")
        case True
        from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
          apply (case_tac "cf2sfile (e # s) f")
          apply (drule current_file_has_sfile')
          apply (simp add:vd_cons', simp, simp)
          done
        from a1 ev os True obtain pf where parent: "parent f'' = Some pf"
          and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
          using ev True vd_enrich created_cons
          by (simp add:current_files_simps is_created_proc_simps)
        thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
          apply (simp add:is_created_proc_simps cf2sfile_linkhard)
          apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
          apply (drule_tac tf = pf in secs_dir, simp+) 
          apply (erule exE, erule conjE, simp)
          apply (case_tac aa, simp)
          done
      next
        case False
        have f_in: "f \<in> current_files (e # enrich_proc s p p')"
          using ev False vd_enrich a1 created_cons nodel vd vd_cons'
          by (simp add:current_files_linkhard is_created_proc_simps enrich_proc_cur_files)
        with ev a1 vd_enrich vd_cons' created_cons False
        show ?thesis
          apply (simp add:is_created_proc_simps cf2sfile_linkhard)
          apply (simp add:current_files_simps pre_sf)
          done
      qed      
    qed
    show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
      apply (case_tac e) 
      prefer 6 apply (erule b1)
      prefer 11 apply (erule b2)
      prefer 11 apply (erule b3)
      using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
      apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps current_files_simps
        split:if_splits dest:vd_cons cf2sfile_other')
      done
  qed
  moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> 
    cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
  proof clarify
    fix tp fd 
    assume a1: "fd \<in> proc_file_fds (e # s) tp"
    from a1 obtain f where a1': "file_of_proc_fd (e # s) tp fd = Some f" 
      by (auto simp:proc_file_fds_def)
    from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; is_created_proc s p\<rbrakk> \<Longrightarrow>
      cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by auto
    hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p\<rbrakk> \<Longrightarrow>
      cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
    hence pre_sfd'': "\<And> tp fd f proc. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p = proc\<rbrakk> \<Longrightarrow>
      cfd2sfd (enrich_proc s proc p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
    from a1' all_procs_cons vd_cons' have a2: "tp \<noteq> p'"
      apply (drule_tac not_all_procs_prop3)
      apply (drule proc_fd_in_procs, simp)
      by (rule notI, simp)
    have a3: "p' \<noteq> p" using all_procs_cons created_cons
      apply (drule_tac not_all_procs_prop3)
      apply (rule notI, simp add:is_created_proc_def)
      done      
    have a4: "file_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some f" 
      using a1' nodel_cons all_procs_cons a1' created_cons vd_cons'
      apply (frule_tac enrich_proc_filefd, simp_all)
      done
    have sec_proc:
      "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> 
       \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
      using pre 
      apply (clarsimp)
      apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)
      done
    have sec_proc':
      "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p; p = tp\<rbrakk> 
       \<Longrightarrow> sectxt_of_obj (enrich_proc s tp p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
      apply (drule_tac sec_proc, simp+)
      done
    show "cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
    proof-
      have b1: "\<And> proc f' fds. e = Execve proc f' fds
        \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
        using a4 vd_enrich_cons a1' vd_cons' created_cons
        apply (simp split:if_splits del:file_of_proc_fd.simps add:a2) 
        apply (simp only:cfd2sfd_execve)
        apply (drule_tac s = "Execve proc f' fds # enrich_proc s proc p'" in vd_cons)
        apply (simp split:if_splits add:a2)
        apply (drule_tac p' = proc and fd' = fd and s = "enrich_proc s proc p'" in cfd2sfd_execve, simp+)
        apply (erule_tac pre_sfd'', simp add:is_created_proc_simps, simp)
        apply (drule_tac p' = tp and fd' = fd in cfd2sfd_execve, simp+)
        apply (erule_tac pre_sfd'', simp add:is_created_proc_simps, simp)
        apply (simp only:cfd2sfd_execve)
        apply (rule_tac pre_sfd')
        apply (auto split:if_splits simp:is_created_proc_simps)
        done 
      have b2: "\<And> proc proc' fds. e = Clone proc proc' fds
       \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
        using a4 vd_enrich_cons a1' vd_cons' created_cons
        apply (simp split:if_splits del:file_of_proc_fd.simps) 
        apply (simp add:cfd2sfd_clone add:a2)
        apply (simp add:cfd2sfd_clone split:if_splits)
        apply (erule pre_sfd'', simp add:is_created_proc_simps, simp)
        apply (erule pre_sfd', simp add:is_created_proc_simps)
        done 
      have b3: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 
         \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
        using a4 a1' vd_enrich_cons vd_cons' created_cons 
        apply (simp split:if_splits del:file_of_proc_fd.simps) 
        
        apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps)
        apply (tactic {*my_clarify_tac 1*})
        apply (drule vd_cons)
        apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits)
        apply (case_tac "proc \<in> current_procs s")
        apply (simp add:sec_proc')
        apply (case_tac "sectxt_of_obj s (O_proc proc)", simp+)        
        apply (case_tac "f \<in> current_files (e # s)")
        apply (drule sf_cons[rule_format], simp)
        using vd_enrich_cons
        apply (simp add:cf2sfile_open_none)
        using os
        apply (simp add:current_files_simps is_file_in_current split:option.splits)
        using os
        apply (simp split:option.splits)
        apply (rule impI)
        apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits)
        apply (drule vd_cons)
        apply (drule_tac p' = tp and fd' = fd and f' = f and s = "enrich_proc s proc p'" in cfd2sfd_open)
        apply (simp, rule impI, simp)
        apply (simp split:if_splits, rule conjI, rule impI, simp)
        apply (drule pre_sfd', simp, simp)

        apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps)
        apply (case_tac "proc \<in> current_procs s")
        apply (simp add:sec_proc)
        apply (case_tac "f' \<in> current_files (e # s)")
        apply (drule sf_cons[rule_format], simp)
        apply (simp split:option.splits)
        apply (rule impI|rule conjI)+
        apply (drule current_has_sec', simp add:vd, simp add:os)
        apply (rule impI, rule impI)
        apply (simp split:if_splits)
        apply (simp add:pre_sfd')
        using os
        apply (simp add:current_files_simps is_file_in_current split:option.splits)
        using os
        apply (simp split:option.splits)
        done
      have b4: "\<And> proc fd'. e = ReadFile proc fd' 
         \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
        using a4 vd_enrich_cons a1' vd_cons' created_cons
        apply (simp split:if_splits del:file_of_proc_fd.simps) 
        apply (frule_tac s = "ReadFile proc fd' # enrich_proc s proc p'" in vd_cons)
        apply (simp add:cfd2sfd_other)
        apply (erule pre_sfd'', simp add:is_created_proc_simps, simp)
        apply (simp add:cfd2sfd_other)
        apply (erule pre_sfd', simp add:is_created_proc_simps)
        done 
      show ?thesis
        apply (case_tac e)
        apply (erule b1, erule b2) 
        prefer 4 apply (erule b3) prefer 4 apply (erule b4)
        using vd created_cons nodel_cons a1' a4 vd_enrich_cons vd_cons'
        apply (auto intro!:pre_sfd' simp:cfd2sfd_simps is_created_proc_simps 
          simp del:file_of_proc_fd.simps split:if_splits dest:vd_cons enrich_proc_filefd)
        apply (simp_all)
        done
    qed
  qed
  moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
  proof clarify
    fix q
    assume a1: "q \<in> current_msgqs (e # s)"
    from pre have pre_smsgq: "\<And> q. \<lbrakk>q \<in> current_msgqs s; is_created_proc s p\<rbrakk>
      \<Longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q"
      by auto 
    show "cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
      using vd_enrich_cons a1 created_cons nodel_cons vd_cons' os
      apply (case_tac e) 
      apply (auto simp:cq2smsgq_simps cq2smsg_createmsgq is_created_proc_simps sec_proc 
        dest:cq2smsgq_other intro!:pre_smsgq split:if_splits dest:vd_cons)
      
      apply (simp add:sectxt_of_obj_simps split:option.splits)
      
      thm sec_proc
      thm cq2smsgq_simps
      thm cq2smsg_createmsgq
    sorry
  moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
    sorry
  moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"
  proof-
    from pre have b0: "is_created_proc s p \<Longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p" by simp
    have b1: "\<And> tp f fds. \<lbrakk>valid (enrich_proc (Execve tp f fds # s) p p'); valid (Execve tp f fds # s);
      is_created_proc (Execve tp f fds # s) p; p' \<notin> all_procs (Execve tp f fds # s)\<rbrakk>
      \<Longrightarrow> cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p"
    proof-
      fix tp f fds
      assume a1: "valid (enrich_proc (Execve tp f fds # s) p p')"
      and a2: "valid (Execve tp f fds # s)" and a3: "is_created_proc (Execve tp f fds # s) p"
      and a4: "p' \<notin> all_procs (Execve tp f fds # s)"
      show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p"
      proof (cases "tp = p")
        case True
        show ?thesis using True a1 a2 a3 a4 b0 vd
          thm not_all_procs_prop3
          apply (frule_tac not_all_procs_prop2)
          apply (frule not_all_procs_prop3)
          apply (simp add:is_created_proc_simps)
          apply (frule vd_cons) (*
          apply (frule_tac vt_grant_os) 
          apply (frule_tac \<tau> = "enrich_proc s p p'" in vt_grant_os) *)
          apply (frule_tac s = "enrich_proc s p p'" in vd_cons)
          apply (frule_tac \<tau> = s in vt_grant_os)
          apply (case_tac "p' = p", simp) (*
          apply (auto simp add:cp2sproc_execve sectxt_of_obj_simps enrich_proc_dup_in
            split:option.splits dest!:current_has_sec' dest:vt_grant is_file)
          apply (simp_all add:is_created_proc_def)
          apply (auto simp:cp2sproc_def)
          apply (simp_all add:enrich_proc_dup_in)

          
          apply (auto simp:sectxt_of_obj_simps split:option.splits dest:valid.cases)
  *)        
          sorry
      next
        case False
        show ?thesis sorry
      qed
    qed
    have b2: "\<And> tp fd. cp2sproc (enrich_proc (ReadFile tp fd # s) p p') p' = cp2sproc (ReadFile tp fd # s) p"
      sorry
    have b3: "\<And> tp. cp2sproc (enrich_proc (Exit tp # s) p p') p' = cp2sproc (Exit tp # s) p"
      sorry
    have b4: "\<And> tp tp'. cp2sproc (enrich_proc (Kill tp tp' # s) p p') p' = cp2sproc (Kill tp tp' # s) p"
      sorry
    have b5: "\<And> tp tp' fds. cp2sproc (enrich_proc (Clone tp tp' fds # s) p p') p' = 
      cp2sproc (Clone tp tp' fds # s) p"
      sorry
    have b6: "\<And> tp f flags fd opt. cp2sproc (enrich_proc (Open tp f flags fd opt # s) p p') p' =
      cp2sproc (Open tp f flags fd opt # s) p"
      sorry
    have b7: "\<And> tp fd. cp2sproc (enrich_proc (CloseFd tp fd # s) p p') p' = cp2sproc (CloseFd tp fd # s) p"
      sorry
    show ?thesis using vd_enrich_cons
      apply (case_tac e)
      using vd_cons' created_cons all_procs_cons
      apply (auto intro!:b1 b2 b3 b4 b5 b6 b7 simp del:enrich_proc.simps)
      using created_cons vd_enrich_cons vd_cons' b0
      apply (auto simp:cp2sproc_other is_created_proc_def)
      done
  qed
  moreover have "\<forall> fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> 
    cfd2sfd (enrich_proc (e # s) p p') p' fd = cfd2sfd (e # s) p fd"
    sorry
  ultimately show ?case using vd_enrich_cons
    by simp
qed
  
lemma enrich_proc_s2ss:
  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> s2ss (enrich_proc s p p') = s2ss s"

lemma enrich_proc_valid:
  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"
by (auto dest:enrich_proc_prop)

lemma enrich_proc_valid:
  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> " 

lemma enrich_proc_tainted: 
  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
   \<Longrightarrow> tainted (enrich_proc s p p') = (if (O_proc p \<in> tainted s) 
         then tainted s \<union> {O_proc p'} else tainted s)"
apply (induct s)
apply (simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons, simp)
apply (frule enrich_proc_dup_in, simp+)
apply (frule not_all_procs_prop3)
apply (case_tac a)
prefer 3
apply (simp split:if_splits)
apply (rule impI|rule conjI)+
apply (simp add:is_created_proc_def)
apply (auto simp:is_created_proc_def split:if_splits dest:tainted_in_current)[1]
apply (simp add:is_created_proc_def)

prefer 4
apply (simp split:if_splits)
apply (rule impI|rule conjI)+
apply (simp add:is_created_proc_def)
apply (auto simp:is_created_proc_def split:if_splits dest:tainted_in_current)[1]
apply (simp add:is_created_proc_def)

prefer 4
apply (auto simp:is_created_proc_def split:if_splits option.splits dest:tainted_in_current)[1]

prefer 4
apply (auto simp:is_created_proc_def split:if_splits option.splits dest:tainted_in_current enrich_proc_dup_ffd enrich_proc_dup_ffd')[1]



lemma enrich_proc_dup_tainted:
  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
   \<Longrightarrow> (O_proc p' \<in> tainted (enrich_proc s p p')) = (O_proc p \<in> tainted s)"
apply (induct s)
apply (simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a)
apply (auto simp:is_created_proc_def)[1]


lemma enrich_proc_tainted:



end

end