theory KHeap_AI

lemma set_aobject_caps_of_state [wp]:
  "set_object ptr (ArchObj obj) \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" apply (wpsimp wp: set_object_wp_strong simp: obj_at_def a_type_def) apply (subst cte_wp_caps_of_lift) prefer 2 apply assumption subgoal for _ y by (cases y, auto simp: cte_wp_at_cases a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s ptr = Some ko; AArch (aa_type obj) = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko p Pa. \<lbrakk>P (caps_of_state s); kheap s ptr = Some ko; AArch (aa_type obj) = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>) = cte_wp_at Pa p (?s'9 s ko)
 2. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s ptr = Some ko; AArch (aa_type obj) = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'9 s ko)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (caps_of_state s); kheap s ptr = Some ko; AArch (aa_type obj) = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'9 s ko))
 2. \<And>s ko p Pa. \<lbrakk>P (caps_of_state s); kheap s ptr = Some ko; AArch (aa_type obj) = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>) = cte_wp_at Pa p (?s'9 s ko) proof (prove)
goal (1 subgoal):
 1. \<And>s ko p Pa. \<lbrakk>P (caps_of_state s); kheap s ptr = Some ko; AArch (aa_type obj) = (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj obj)\<rparr>) = cte_wp_at Pa p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (caps_of_state s_); kheap s_ ptr = Some y; AArch (aa_type obj) = (case y of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (aa_type ao))\<rbrakk> \<Longrightarrow> cte_wp_at Pa_ p_ (s_\<lparr>kheap := (kheap s_)(ptr \<mapsto> ArchObj obj)\<rparr>) = cte_wp_at Pa_ p_ s_ proof (prove)
goal:
No subgoals!