(*<*)
theory S2ss_prop
imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop
begin
(*>*)

context tainting_s begin

(* simpset for s2ss*)

lemma co2sobj_some_case:
  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);
    \<And> f. obj = O_file f \<Longrightarrow> P (O_file f); \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h);
    \<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>
   \<Longrightarrow> P obj"
by (case_tac obj, auto)

lemma co2sobj_execve_alive:
  "\<lbrakk>alive s obj; co2sobj s obj = Some x; valid (Execve p f fds # s)\<rbrakk>
   \<Longrightarrow> alive (Execve p f fds # s) obj"
apply (erule co2sobj_some_case)
by (auto simp:alive_simps simp del:alive.simps)

lemma s2ss_execve:
  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (
     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
     then (case (cp2sproc (Execve p f fds # s) p) of
             Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
           | _ \<Rightarrow> {} )
     else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of
             (Some sp, Some sp') \<Rightarrow> s2ss s - {S_proc sp' (O_proc p \<in> Tainted s)}
                                    \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}
           | _ \<Rightarrow> {} ) )"
apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)

apply (rule conjI, rule impI, (erule exE|erule conjE)+)
apply (frule_tac p = p in current_proc_has_sp, simp, erule exE)
apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE, simp)
apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)")
apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)
apply (erule exE, simp)
apply (simp add:s2ss_def, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (case_tac "obj = O_proc p")
apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits)
apply (simp add:co2sobj_execve, rule disjI2)
apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1]
apply (simp, erule disjE)
apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)
apply (erule exE| erule conjE)+
apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")
apply (rule_tac x = "O_proc p'" in exI)
apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve)
apply (case_tac "obj = O_proc p", simp)
apply (frule co2sobj_execve_alive, simp, simp)
apply (frule_tac obj = obj in co2sobj_execve, simp)
apply (rule_tac x = obj in exI, simp, simp)

apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp)
apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") 
apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)
apply (erule exE, erule conjE, simp)
apply (simp add:s2ss_def, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (case_tac "obj = O_proc p", simp add:tainted_eq_Tainted)
apply (rule disjI1, simp split:if_splits)
apply (simp add:co2sobj_execve, rule disjI2)
apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
apply (rule notI, simp, case_tac obj)
apply (erule_tac x = nat in allE, simp add:tainted_eq_Tainted, (simp split:option.splits)+)
apply (erule disjE, simp)
apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)
apply (erule exE|erule conjE)+
apply (rule_tac x = obj in exI)
apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)
apply (frule_tac obj = obj in co2sobj_execve, simp, simp)
apply (rule impI, simp add:tainted_eq_Tainted, simp)
done

lemma s2ss_clone_alive:
  "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds shms # s)\<rbrakk>
   \<Longrightarrow> alive (Clone p p' fds shms # s) obj"
by (erule co2sobj_some_case, auto simp:alive_clone)

lemma s2ss_clone:
  "valid (Clone p p' fds shms # s) \<Longrightarrow> s2ss (Clone p p' fds shms # s) = (
     case (cp2sproc (Clone p p' fds shms # s) p') of
       Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s)}
     | _       \<Rightarrow> {})"
apply (frule vd_cons, frule vt_grant_os, split option.splits)
apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
apply (rule allI, rule impI, simp add:s2ss_def)
apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)
apply (case_tac "obj = O_proc p'", simp add:tainted_eq_Tainted)
apply (case_tac "O_proc p' \<in> Tainted s", drule Tainted_in_current, simp+)
apply (rule disjI1, simp split:if_splits)
apply (simp add:tainted_eq_Tainted, rule disjI2)
apply (frule co2sobj_clone, simp)
apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)

apply (simp, erule disjE, simp)
apply (rule_tac x = "O_proc p'" in exI, simp add:tainted_eq_Tainted)
apply (rule impI, rule notI, drule Tainted_in_current, simp+)
apply (erule exE| erule conjE)+
apply (case_tac "obj = O_proc p'", simp)
apply (rule_tac x = obj in exI)
apply (frule s2ss_clone_alive, simp+)
apply (auto simp:co2sobj_clone alive_simps)
done

definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" 
where
  "update_s2ss_shm s pfrom \<equiv> s2ss s 
     \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}
     - {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and> 
           (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> 
                cp2sproc s p' = Some sp \<and> O_proc p' \<notin> Tainted s))}"

lemma Tainted_ptrace':
  "valid s \<Longrightarrow> Tainted (Ptrace p p' # s) = 
     (if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s)
      then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
      else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
           then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
                else Tainted s)"
using info_flow_shm_Tainted by auto

lemma co2sobj_some_caseD:
  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);
    \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); 
    \<And> h. \<lbrakk>co2sobj s obj = Some sobj; obj = O_shm h\<rbrakk> \<Longrightarrow> P (O_shm h);
    \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_dir f\<rbrakk> \<Longrightarrow> P (O_dir f); 
    \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk>
   \<Longrightarrow> P obj"
by (case_tac obj, auto)

lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp

lemma s2ss_ptrace1:
  "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> Tainted s; O_proc p' \<notin> Tainted s\<rbrakk>
   \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'"
unfolding update_s2ss_shm_def s2ss_def
apply (frule vd_cons, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (erule co2sobj_some_caseD)
apply (rule DiffI)
apply (case_tac "O_proc pa \<in> Tainted s")
apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (case_tac "info_flow_shm s p' pa")
apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule_tac x = a in exI, rule_tac x = pa in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule UnI1, simp)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (erule_tac x = pa in allE, simp)

apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp split:option.splits)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp split:option.splits)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp split:option.splits)

apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "O_proc pa \<in> Tainted s")
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
apply (rule_tac x = "O_proc p'a" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
done

lemma s2ss_ptrace2:
  "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk>
   \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p"
unfolding update_s2ss_shm_def s2ss_def
apply (frule vd_cons, rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (erule co2sobj_some_caseD)
apply (rule DiffI)
apply (case_tac "O_proc pa \<in> Tainted s")
apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (case_tac "info_flow_shm s p pa")
apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule_tac x = a in exI, rule_tac x = pa in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule UnI1, simp)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (erule_tac x = pa in allE, simp)

apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp split:option.splits)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp split:option.splits)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (simp split:option.splits)

apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "O_proc pa \<in> Tainted s")
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
apply (rule_tac x = "O_proc p'a" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)

apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]

apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
done

lemma s2ss_ptrace3:
  "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> Tainted s) = (O_proc p \<in> Tainted s)\<rbrakk>
   \<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s"
unfolding s2ss_def
apply (frule vd_cons, rule set_eqI, rule iffI)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (frule alive_other, simp+)
apply (frule_tac obj = obj in co2sobj_ptrace, simp)
apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits
  intro:info_flow_shm_Tainted)[1]

apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (frule alive_other, simp+)
apply (frule_tac obj = obj in co2sobj_ptrace, simp)
apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits 
  intro:info_flow_shm_Tainted)
done

lemma s2ss_ptrace:
  "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (
     if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s) 
     then update_s2ss_shm s p'
     else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
          then update_s2ss_shm s p
          else s2ss s                                   )"
apply (frule vt_grant_os, frule vd_cons)
apply (simp add:s2ss_ptrace2 s2ss_ptrace1 split:if_splits)
by (auto dest:s2ss_ptrace3)

lemma s2ss_kill:
  "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = (
     if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p'))
     then s2ss s 
     else (case (co2sobj s (O_proc p')) of
             Some sp \<Rightarrow> s2ss s - {sp}
           | _       \<Rightarrow> {}))"
apply (frule vt_grant_os, frule vd_cons)
unfolding s2ss_def
apply (simp split:if_splits, rule conjI)
apply (rule impI, (erule exE|erule conjE)+)
apply (split option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (simp split: option.splits, (erule conjE)+)
apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p'")
apply (rule_tac x = "O_proc p''" in exI)
apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+

apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp)
apply (rule set_eqI, rule iffI)
apply (erule CollectE, erule exE, erule conjE, rule DiffI)
apply (rule CollectI, rule_tac x = obj in exI)
apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
apply (rule notI, simp, case_tac obj)
apply (erule_tac x = nat in allE)
apply (simp add:co2sobj_kill cp2sproc_kill tainted_eq_Tainted split:option.splits)
apply (simp split:option.splits)+
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p'")
apply (rule_tac x = "O_proc p''" in exI)
apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
done

lemma s2ss_exit:
  "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = (
     if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
     then s2ss s 
     else (case (co2sobj s (O_proc p)) of
             Some sp \<Rightarrow> s2ss s - {sp}
           | _       \<Rightarrow> {}))"
apply (frule vt_grant_os, frule vd_cons)
unfolding s2ss_def
apply (simp split:if_splits, rule conjI)
apply (rule impI, (erule exE|erule conjE)+)
apply (split option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (simp split: option.splits, (erule conjE)+)
apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p")
apply (rule_tac x = "O_proc p'" in exI)
apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+

apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp)
apply (rule set_eqI, rule iffI)
apply (erule CollectE, erule exE, erule conjE, rule DiffI)
apply (rule CollectI, rule_tac x = obj in exI)
apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
apply (rule notI, simp, case_tac obj)
apply (erule_tac x = nat in allE)
apply (simp add:co2sobj_exit cp2sproc_exit tainted_eq_Tainted split:option.splits)
apply (simp split:option.splits)+
apply (erule co2sobj_some_caseD)
apply (case_tac "pa = p")
apply (rule_tac x = "O_proc p'" in exI)
apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
  split:t_object.splits if_splits option.splits)
apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
done

lemma alive_has_sobj':
  "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"
apply (case_tac obj)
apply (auto split:option.splits)
oops

declare co2sobj.simps [simp del]

lemma co2sobj_open_none:
  "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (
      if (obj = O_proc p) 
      then (case (cp2sproc (Open p f flag fd None # s) p) of
              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
           | _       \<Rightarrow> None)
      else co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons)
apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
done

lemma co2sobj_open_some:
  "\<lbrakk>valid (Open p f flag fd (Some i) # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (
      if (obj = O_proc p) 
      then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of
              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
           | _       \<Rightarrow> None)
      else if (obj = O_file f) 
           then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of
                   Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
                 | _       \<Rightarrow> None)
           else co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons)
apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
done

lemma alive_co2sobj_some_open_none:
  "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk>
   \<Longrightarrow> alive (Open p f flag fd None # s) obj"
by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

lemma alive_co2sobj_some_open_none':
  "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; 
    valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj"
by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

lemma co2sobj_proc_obj:
  "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk>
   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

lemma s2ss_open_none:
  "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = (
      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of
        (Some sp, Some sp') \<Rightarrow> 
           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
           then s2ss s \<union> {sp'}
           else s2ss s - {sp} \<union> {sp'} 
      | _                   \<Rightarrow> {} )"
unfolding s2ss_def
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)")
apply (simp add:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp)
apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp)
apply (rule conjI, rule impI, erule exE, (erule conjE)+)
apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp)
apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
apply (rule impI)
apply (case_tac "obj = O_proc p", simp)
apply (rule Meson.disj_comm, rule disjCI, rule conjI)
apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
apply (simp add:co2sobj_open_none split:option.splits)
apply (rule notI)
apply (frule co2sobj_proc_obj, simp, erule exE)
apply (erule_tac x = p' in allE, simp)

apply (simp split:if_splits)
apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
apply (erule exE, erule conjE, case_tac "obj = O_proc p")
apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p")
apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
done

lemma alive_co2sobj_some_open_some:
  "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk>
   \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj"
by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps)

lemma alive_co2sobj_some_open_some':
  "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; 
    valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj"
by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)

lemma s2ss_open_some:
  "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = (
      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p),
            co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of
        (Some sp, Some sp', Some sf) \<Rightarrow> 
           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
           then s2ss s \<union> {sp', sf} 
           else s2ss s - {sp} \<union> {sp', sf} 
      | _                   \<Rightarrow> {} )"
unfolding s2ss_def
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)")
apply (simp add:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)")
apply (simp add:co2sobj.simps split:option.splits)
apply (clarsimp split del:if_splits)

apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE)
apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
apply (rule UnI1, rule CollectI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
apply (simp add:co2sobj_open split:t_object.splits)
apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
apply (simp add:co2sobj_open split:t_object.splits)
apply (frule_tac obj = obj in co2sobj_open_some, simp+)
apply (simp add:alive_co2sobj_some_open_some', simp)
apply (rule notI)
apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE)
apply (erule_tac x = p' in allE, simp)

apply (simp split:if_splits, erule disjE)
apply (rule_tac x = "O_proc p" in exI, simp)
apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p", simp)
apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some)
apply (case_tac "obj = O_file f", simp add:is_file_in_current)
apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
apply (erule conjE, erule exE, erule conjE)
apply (case_tac "obj = O_proc p", simp)
apply (case_tac "obj = O_file f", simp add:is_file_in_current)
apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
done

lemma s2ss_open:
  "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = (
     if opt = None
     then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of
        (Some sp, Some sp') \<Rightarrow> 
           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
           then s2ss s \<union> {sp'}
           else s2ss s - {sp} \<union> {sp'} 
      | _                   \<Rightarrow> {} )
     else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p),
            co2sobj (Open p f flag fd opt # s) (O_file f)) of
        (Some sp, Some sp', Some sf) \<Rightarrow> 
           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
           then s2ss s \<union> {sp', sf} 
           else s2ss s - {sp} \<union> {sp', sf} 
      | _                   \<Rightarrow> {} ) )"
apply (case_tac opt)
apply (simp add:s2ss_open_some s2ss_open_none)+
done

lemma s2ss_readfile:
  "valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = (
     case (file_of_proc_fd s p fd) of 
       Some f \<Rightarrow> if (O_file f \<in> Tainted s)
                 then update_s2ss_shm s p
                 else s2ss s
     | _      \<Rightarrow> {})"
apply (frule vt_grant_os, frule vd_cons, clarsimp split:option.splits)
apply (rule conjI, rule impI, rule impI, simp)
unfolding update_s2ss_shm_def s2ss_def
apply (rule set_eqI, rule iffI)
apply (drule CollectD, (erule exE|erule conjE)+)
apply (erule co2sobj_some_caseD)
apply (rule DiffI)
apply (case_tac "O_proc pa \<in> Tainted s")
apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
apply (case_tac "info_flow_shm s p pa")
apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule_tac x = ab in exI, rule_tac x = pa in exI)
apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
apply (rule UnI1, simp)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
apply (erule_tac x = pa in allE, simp)

apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)
apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)

apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (erule co2sobj_some_caseD)
apply (case_tac "O_proc pa \<in> Tainted s")
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits)
apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE)
apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
apply (rule_tac x = "O_proc p'" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)

apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
apply (rule_tac x = obj in exI,
       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]

apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
apply (rule_tac x = "O_proc pa" in exI)
apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps)


apply (rule impI, rule impI)
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)
apply (rule_tac x = obj in exI, simp add:alive_simps co2sobj_readfile split:t_object.splits)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (rule_tac x = obj in exI, simp add:alive_simps)
apply (drule_tac obj = obj in co2sobj_readfile, simp)
apply (simp split:t_object.splits)
apply (simp add:co2sobj.simps)+
done

lemma same_inode_files_prop9:
  "is_file s f \<Longrightarrow> f \<in> same_inode_files s f"
by (simp add:same_inode_files_def)

lemma cf2sfiles_prop:
  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> cf2sfiles s f = cf2sfiles s f'"
apply (auto simp:cf2sfiles_def)
apply (rule_tac x = f'a in bexI, simp)
apply (erule same_inode_files_prop4, simp)
apply (rule_tac x = f'a in bexI, simp)
apply (drule same_inode_files_prop5)
apply (erule same_inode_files_prop4, simp)
done

lemma co2sobj_writefile_unchange:
  "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;
    O_proc p \<in> Tainted s \<longrightarrow> O_file f \<in> Tainted s\<rbrakk> 
   \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"
apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)
apply (simp add:co2sobj.simps)
apply (case_tac "O_proc p \<in> Tainted s")
apply (simp add:tainted_eq_Tainted same_inodes_Tainted)+
done

lemma s2ss_writefile:
  "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (
     case (file_of_proc_fd s p fd) of
       Some f \<Rightarrow> if (O_proc p \<in> Tainted s \<and> O_file f \<notin> Tainted s)
                 then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>
                                 co2sobj s (O_file f') = co2sobj s (O_file f))
                       then s2ss s \<union> {S_file (cf2sfiles s f) True}
                       else s2ss s - {S_file (cf2sfiles s f) False} 
                                   \<union> {S_file (cf2sfiles s f) True})
                 else s2ss s
     | _      \<Rightarrow> {})"
apply (frule vd_cons, frule vt_grant_os)
apply (clarsimp split:option.splits)
unfolding s2ss_def
apply (rule conjI|rule impI|erule exE|erule conjE)+
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)
apply (simp split:t_object.splits if_splits)
apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)
apply (rule disjI1, simp add:cf2sfiles_prop)
apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)
apply (simp add:co2sobj.simps)
apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)
apply (simp add:co2sobj.simps)
apply (simp add:co2sobj.simps)
apply (simp add:co2sobj.simps)
apply (rule disjI2, rule_tac x = obj in exI, simp)
apply (rule disjI2, rule_tac x = obj in exI, simp)
apply (simp add:co2sobj.simps)

apply (simp, erule disjE)
apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)
apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)
apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)
apply (erule exE, erule conjE)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
apply (case_tac "fa \<in> same_inode_files s aa")
apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)
apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)
apply (rule conjI, rule impI, simp add:same_inode_files_prop5)
apply (rule impI, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)
apply (rule impI, simp add:same_inode_files_prop5)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)
apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)
apply (simp add:co2sobj_writefile split:t_object.splits if_splits)
apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
apply (case_tac "O_proc p \<in> Tainted s", simp, simp)
apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_writefile_unchange alive_simps)

apply (rule impI| rule conjI|erule conjE)+
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
  rule notI, simp add:co2sobj.simps split:option.splits)
apply (simp split:if_splits)
apply (rule disjI1, simp add:cf2sfiles_prop)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)
apply (rule notI, simp add:co2sobj.simps split:option.splits)
apply (erule_tac x = list in allE, simp add:tainted_eq_Tainted same_inode_files_prop5)
apply (simp add:co2sobj.simps)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
  rule notI, simp add:co2sobj.simps split:option.splits)
apply (simp add:co2sobj.simps)
apply (simp add:co2sobj.simps)
apply (simp add:co2sobj.simps)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
  rule notI, simp add:co2sobj.simps split:option.splits)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
  rule notI, simp add:co2sobj.simps split:option.splits)
apply (simp add:co2sobj.simps)
apply (simp)
apply (erule disjE)
apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)
apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)
apply (erule exE|erule conjE)+
apply (erule co2sobj_some_caseD)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
apply (case_tac "fa \<in> same_inode_files s aa")
apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)
apply (rule impI, simp add:same_inode_files_prop5)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
apply (rule impI, rule impI)

apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)
apply (rule_tac x = obj in exI)
apply (simp add:co2sobj_writefile_unchange alive_simps)
apply (erule CollectE, erule exE, erule conjE)
apply (rule CollectI, rule_tac x = obj in exI)
apply (simp add:co2sobj_writefile_unchange alive_simps)
done


definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
where
  "update_s2ss_obj s ss obj sobj sobj' = 
     (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
      then ss \<union> {sobj'}
      else ss - {sobj} \<union> {sobj'})"

definition update_s2ss_sfile :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
where 
  "update_s2ss_sfile s ss f sf \<equiv> 
     if (same_inode_files s f = {f})
     then ss
     else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"

definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
where
  "del_s2ss_file s ss f sf = 
     (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
      then ss
      else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
           then update_s2ss_sfile s ss f sf
           else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf"

lemma alive_co2sobj_closefd1:
  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
    file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
   \<Longrightarrow> alive (CloseFd p fd # s) obj"
apply (erule co2sobj_some_caseD)
by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

lemma alive_co2sobj_closefd3:
  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;
    file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>
   \<Longrightarrow> alive (CloseFd p fd # s) obj"
apply (erule co2sobj_some_caseD)
by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

lemma alive_co2sobj_closefd2:
  "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>
   \<Longrightarrow> alive (CloseFd p fd # s) obj"
apply (erule co2sobj_some_caseD)
by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)

lemma alive_co2sobj_closefd':
  "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; 
    valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"
apply (erule co2sobj_some_caseD)
by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)

ML {*asm_full_simp_tac*}

ML {*
fun my_setiff_tac i = 
     (etac @{thm CollectE} i 
      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i
              THEN etac @{thm disjE} i)
      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i
              THEN etac @{thm conjE} i 
              THEN (REPEAT (etac @{thm CollectE} i))))
THEN (REPEAT ((        etac @{thm exE} 
               ORELSE' etac @{thm conjE}
               ORELSE' etac @{thm bexE}) i))
THEN (rtac @{thm CollectI} i
      ORELSE (     asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i))

*}

ML {*
fun my_seteq_tac i = 
     (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1)
THEN (rtac @{thm set_eqI} i)
THEN (rtac @{thm iffI} i)
THEN my_setiff_tac i
*}

lemma co2sobj_sproc_imp:
  "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"
by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

lemma co2sobj_sfile_imp:
  "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"
by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

lemma co2sobj_sdir_imp:
  "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"
by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

lemma co2sobj_sshm_imp:
  "co2sobj s obj = Some (S_shm sh) \<Longrightarrow> \<exists> h. obj = O_shm h"
by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

lemma co2sobj_smsgq_imp:
  "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
by (case_tac obj, auto simp:co2sobj.simps split:option.splits)

lemma s2ss_closefd:
  "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
     case (file_of_proc_fd s p fd) of
       Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})
                 then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
                         (Some sf, Some sp, Some sp') \<Rightarrow> 
                            (del_s2ss_file s (
                               update_s2ss_obj s (s2ss s) (O_proc p) 
                                 (S_proc sp (O_proc p \<in> Tainted s))
                                 (S_proc sp' (O_proc p \<in> Tainted s))) f sf)
                      | _ \<Rightarrow> {})
                 else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of 
                         (Some sp, Some sp') \<Rightarrow> 
                            (update_s2ss_obj s (s2ss s) (O_proc p)
                               (S_proc sp (O_proc p \<in> Tainted s))
                               (S_proc sp' (O_proc p \<in> Tainted s)))
                      | _ \<Rightarrow> {})
      | _     \<Rightarrow> s2ss s)"
apply (frule vd_cons, frule vt_grant_os)
apply (clarsimp simp only:os_grant.simps)
apply (frule current_proc_has_sp, simp, erule exE)
apply (case_tac "file_of_proc_fd s p fd")

apply (simp add:s2ss_def)
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)
apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
apply (frule co2sobj_closefd, simp)
apply (frule cp2sproc_closefd, simp)
apply (simp add:proc_file_fds_def split:t_object.splits)
apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted)
apply (erule CollectE, erule exE, erule conjE, rule CollectI)
apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)
apply (frule cp2sproc_closefd, simp)
apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted 
            split:t_object.splits option.splits if_splits)[1]

apply (case_tac "cp2sproc (CloseFd p fd # s) p")
apply (drule current_proc_has_sp', simp, simp)
apply (case_tac "cf2sfile s a")
apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current)
apply (simp)

apply (rule conjI, rule impI, erule conjE)
apply (simp add:del_s2ss_file_def)
apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+

apply (simp add:update_s2ss_obj_def)
apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
apply (tactic {*my_seteq_tac 1*})
apply simp
apply (case_tac "obj = O_proc p")
apply (simp add:co2sobj.simps tainted_eq_Tainted)
apply (rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)
apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = "O_proc p" in exI)
apply (simp add:co2sobj.simps tainted_eq_Tainted)
apply (tactic {*my_setiff_tac 1*})
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI)
apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
apply (simp add:co2sobj.simps tainted_eq_Tainted)
apply (case_tac "obj = O_file a")
apply (rule_tac x = "O_file f'" in exI)
apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

apply (rule impI)+
apply (tactic {*my_seteq_tac 1*})
apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)
apply (rule disjI2)
apply (case_tac "obj = O_file a", simp add:alive_simps)
apply (rule DiffI, simp)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
apply (erule_tac x = "O_proc pa" in allE, simp)
apply (tactic {*my_setiff_tac 1*})
apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
apply (tactic {*my_setiff_tac 1*})
apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)
apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]

apply (rule impI, tactic {*my_seteq_tac 1*})
apply (simp add:update_s2ss_obj_def)
apply (rule conjI, rule impI, (erule exE|erule conjE)+)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
apply (erule bexE, erule conjE)
apply (erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule impI)
apply (erule_tac obj = obj in co2sobj_some_caseD)
apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp)
apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
apply (rule notI, simp add:co2sobj_closefd)
apply (erule_tac x = obj in allE, simp)
apply (case_tac "f = a", simp add:alive_simps)
apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
apply (erule bexE, erule conjE)
apply (erule_tac x = f'' in ballE, simp, simp)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
apply (tactic {*my_setiff_tac 1*})




defer
apply (rule impI)
apply (simp add:update_s2ss_obj_def)
apply (rule conjI, rule impI, erule exE, erule conjE)
apply (simp add:s2ss_def)
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (simp)
apply (case_tac "obj = O_proc p")
apply (simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
apply (rule disjI2, rule_tac x = obj in exI, erule conjE)
apply (simp add:alive_co2sobj_closefd')
apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits)
apply (simp, erule disjE)
apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
apply (erule exE, erule conjE)
apply (case_tac "obj = O_proc p")
apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1)
apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
apply (rule impI)
apply (simp add:s2ss_def)
apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
apply (simp)
apply (case_tac "obj = O_proc p")
apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd')
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits)
apply (simp)
apply (erule disjE)
apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
apply (erule exE|erule conjE)+
apply (rule_tac x = obj in exI)
apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
apply (clarsimp split:t_object.splits if_splits option.splits 
                simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1)
done





lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
  s2ss_readfile s2ss_writefile s2ss_closefd