theory KHeap_R

lemma setEndpoint_corres [corres]:
  "ep_relation e e' \<Longrightarrow>
  corres dc (ep_at ptr) (ep_at' ptr)
            (set_endpoint ptr e) (setEndpoint ptr e')" apply (simp add: set_simple_ko_def setEndpoint_def is_ep_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_ep obj_at_simps objBits_defs partial_inv_def)

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