theory final_theorems

imports Main rc_theory del_vs_del_s tainted_vs_tainted_s

begin

context tainting_s_complete begin

theorem static_complete: 

  assumes undel: "undeletable obj" and tbl: "taintable obj"

  shows "taintable_s obj"

proof-

  from tbl obtain s where tainted: "obj \<in> tainted s"

    by (auto simp:taintable_def)

  hence vs: "valid s" by (simp add:tainted_is_valid)

  from undel vs have "\<not> deleted obj s" and "exists [] obj" 

    by (auto simp:undeletable_def)

  moreover from tainted have "valid s" by (rule tainted_is_valid)

  ultimately have "source_of_sobj (obj2sobj s obj) = Some obj" 

    using init_obj_keeps_source by auto

  with tainted t2ts 

  show ?thesis unfolding taintable_s_def

    by (rule_tac x = "obj2sobj s obj" in exI, simp)

qed

theorem undeletable_s_complete:

  "undeletable_s obj \<Longrightarrow> undeletable obj"

apply (clarsimp simp:undeletable_s_def undeletable_def)

apply (drule deleted_imp_deletable_s, simp+)

done

theorem final_offer:

  "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; exists [] obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"

apply (erule swap)

by (simp add:static_complete undeletable_s_complete)

end

context tainting_s_sound begin

theorem static_sound:

  assumes tbl_s: "taintable_s obj"

  shows "taintable obj"

proof-

  from tbl_s obtain sobj where ts: "sobj \<in> tainted_s"

    and sreq: "source_of_sobj sobj = Some obj" 

    by (auto simp:taintable_s_def)

  from ts obtain obj' \<tau> where t: "obj' \<in> tainted \<tau>" 

    and vs: "valid \<tau>" and sreq': "sobj_source_eq_obj sobj obj'"

    by (auto dest!:tainted_s2tainted dest:tainted_is_valid)

  from sreq' sreq have "obj = obj'" by (simp add:source_eq)

  with vs t 

  show ?thesis by (auto simp:taintable_def)

qed

end

end