theory KHeap_R

lemma setNotification_corres [corres]:
  "ntfn_relation ae ae' \<Longrightarrow>
  corres dc (ntfn_at ptr) (ntfn_at' ptr)
            (set_notification ptr ae) (setNotification ptr ae')" apply (simp add: set_simple_ko_def setNotification_def is_ntfn_def[symmetric]) apply (corresK_search search: setObject_other_corres[where P="\<lambda>_. True"]) apply (corresKsimp wp: get_object_ret get_object_wp)+ by (fastforce simp: is_ntfn obj_at_simps objBits_defs partial_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_relation ae ae' \<Longrightarrow> corres dc (ntfn_at ptr) (ntfn_at' ptr) (set_notification ptr ae) (setNotification ptr ae') proof (prove)
goal (1 subgoal):
 1. ntfn_relation ae ae' \<Longrightarrow> corres dc (ntfn_at ptr) (ntfn_at' ptr) (do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Notification y = obj);
set_object ptr (Notification ae)
od) (setObject ptr ae') proof (prove)
goal (13 subgoals):
 1. \<And>rv rva. ntfn_relation ae ae' \<Longrightarrow> corres_rv (?Fa8 rv rva) dc (?RR8 rv rva) (\<lambda>_. True) (assert (\<exists>y. Notification y = rv)) corres_noop (\<lambda>rv _. updateObject ae' = updateObject_default ae' \<and> (\<forall>s. ntfn_at' ptr s \<longrightarrow> map_to_ctes ((ksPSpace s)(ptr \<mapsto> injectKO ae')) = ctes_of s) \<and> is_other_obj_relation_type (a_type (Notification ae)) \<and> (\<forall>ko. True \<longrightarrow> objBits ko = objBits ae') \<and> (\<forall>ko. True \<longrightarrow> exst_same' (injectKO ko) (injectKO ae')) \<and> (\<forall>v. 1 < 2 ^ objBits v) \<and> other_obj_relation (Notification ae) (injectKO ae'))
 2. \<And>rv rva. ntfn_relation ae ae' \<Longrightarrow> empty_fail (assert (\<exists>y. Notification y = rv))
 3. \<And>rv rva. ntfn_relation ae ae' \<Longrightarrow> no_fail (?P8 rv rva) (assert (\<exists>y. Notification y = rv))
 4. \<And>rv rva. ntfn_relation ae ae' \<Longrightarrow> \<lbrace>?R8 rv rva\<rbrace> assert (\<exists>y. Notification y = rv) \<lbrace>\<lambda>rvb. typ_at (a_type (Notification ae)) ptr and obj_at (same_caps (Notification ae)) ptr\<rbrace>
 5. \<And>rv. ntfn_relation ae ae' \<Longrightarrow> corres_rv (?Fb8 rv) dc (?RRa8 rv) (\<lambda>_. True) (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN)) corres_noop (\<lambda>rva _. ?Fa8 rv rva)
 6. \<And>rv. ntfn_relation ae ae' \<Longrightarrow> empty_fail (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN))
 7. \<And>rv. ntfn_relation ae ae' \<Longrightarrow> no_fail (?Pa8 rv) (assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN))
 8. \<And>rv. ntfn_relation ae ae' \<Longrightarrow> \<lbrace>?Ra8 rv\<rbrace> assert (a_type rv = AEndpoint \<or> a_type rv = ANTFN) \<lbrace>\<lambda>rva. ?RR8 rv rva and ?P8 rv rva and ?R8 rv rva and (\<lambda>s. \<forall>s'. s = s' \<longrightarrow> (\<exists>y. Notification y = rv) \<longrightarrow> s' = s)\<rbrace>
 9. ntfn_relation ae ae' \<Longrightarrow> corres_rv ?Fc8 dc ?RRb8 (\<lambda>_. True) (get_object ptr) corres_noop (\<lambda>rv _. ?Fb8 rv)
 10. ntfn_relation ae ae' \<Longrightarrow> empty_fail (get_object ptr)
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ntfn_relation ae ae'; ntfn_at ptr s; ntfn_at' ptr s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>s. ntfn_at' ptr s \<longrightarrow> map_to_ctes ((ksPSpace s)(ptr \<mapsto> KONotification ae')) = ctes_of s) \<and> is_other_obj_relation_type ANTFN \<and> (\<forall>ko. objBits ko = objBits ae') \<and> (\<forall>v. 1 < 2 ^ objBits v) \<and> other_obj_relation (Notification ae) (KONotification ae') \<and> obj_at (\<lambda>_. True) ptr s \<and> (\<forall>ko. ko_at ko ptr s \<longrightarrow> (a_type ko = AEndpoint \<or> a_type ko = ANTFN) \<and> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. Notification y = ko) \<and> ((\<exists>y. Notification y = ko) \<longrightarrow> typ_at ANTFN ptr s)) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. Notification y = ko) \<and> ((\<exists>y. Notification y = ko) \<longrightarrow> typ_at ANTFN ptr s)))