theory final_theoremsimports Main rc_theory del_vs_del_s tainted_vs_tainted_sbegincontext tainting_s_complete begintheorem 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)qedtheorem undeletable_s_complete: "undeletable_s obj \<Longrightarrow> undeletable obj"apply (clarsimp simp:undeletable_s_def undeletable_def)apply (drule deleted_imp_deletable_s, simp+)donetheorem 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)endcontext tainting_s_sound begintheorem 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)qedendend