(*<*)

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> 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 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)

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 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)

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, (simp split:option.splits)+)

apply (erule disjE, simp)

apply (rule_tac x = "O_proc p" in exI, simp)

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, 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 # s)\<rbrakk>

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

by (erule co2sobj_some_case, auto simp:alive_clone)

lemma s2ss_clone:

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

     case (cp2sproc (Clone p p' fds # 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)

apply (case_tac "O_proc p' \<in> tainted s", drule tainted_in_current, simp+)

apply (rule disjI1, simp split:if_splits)

apply (simp, 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)

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

lemma s2ss_shm_no_bk_intro4:

  "\<lbrakk>co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p; 

    \<not> info_flow_shm s pfrom p'; p' \<in> current_procs s; co2sobj s (O_proc p') = Some x\<rbrakk>

   \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"

apply (rule notI)

apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)

done  

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 s2ss_shm_no_backup_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 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 split:option.splits)

apply (rule UnI1, simp)

apply (rule_tac x = "O_proc pa" in exI)

apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)

apply (rule notI, clarsimp simp:cp2sproc_other 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 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, (erule exE|erule conjE)+)

apply (rule_tac x = "O_proc p'a" in exI)

apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)

apply (rule_tac x = "O_proc pa" in exI)

apply (clarsimp simp:tainted_ptrace' cp2sproc_other 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 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 s2ss_shm_no_backup_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 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 split:option.splits)

apply (rule UnI1, simp)

apply (rule_tac x = "O_proc pa" in exI)

apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)

apply (rule notI, clarsimp simp:cp2sproc_other 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 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, (erule exE|erule conjE)+)

apply (rule_tac x = "O_proc p'a" in exI)

apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits)

apply (rule_tac x = "O_proc pa" in exI)

apply (clarsimp simp:tainted_ptrace' cp2sproc_other 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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)