(*<*)
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_createshm:
  "\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
      case obj of 
        O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
                                        Some sh \<Rightarrow> Some (S_shm sh)
                                      | _       \<Rightarrow> None)
                    else co2sobj s obj
      | _        \<Rightarrow> co2sobj s obj)"
apply (frule vt_grant_os, frule vd_cons, case_tac obj)
apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
             simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
                  same_inode_files_prop6 ch2sshm_simps
             dest!:current_shm_has_sh'
             dest:is_file_in_current is_dir_in_current)
done

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