(*<*)
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 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> s2ss s)
     else (case (cp2sproc (Execve p f fds # s) p) of
             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> s2ss s) )"
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, simp_all add:co2sobj_execve alive_simps)
thm alive_execve
thm co2sobj_execve
apply (simp add:co2sobj_execve, rule disjI2)
apply (rule_tac x = obj in exI, simp split:t_object.splits)
thm co2sobj_execve
apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1]
apply (simp add:co2sobj_execve)
apply clarsimp
thm current_proc_has_sp

apply (auto simp:s2ss_def co2sobj_execve split:option.splits)



apply (rule conjI, clarify)
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)
apply (simp, (erule conjE)+)
apply (split option.splits, rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
apply (rule allI, rule impI)
apply (rule set_eqI, rule iffI)

apply (simp split:option.splits)
apply (frule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp)
thm current_proc_has_sp


apply (simp split:option.splits)
apply (drule current_proc_has_sp', simp, simp)
apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
apply (simp add:s2ss_def)
apply (rule allI|rule impI)+
apply (rule set_eqI, rule iffI)
apply (auto simp:alive_simps)
apply (case_tac obj, auto split:option.splits simp:cp2sproc_execve)
apply (auto split:if_splits)