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