theory ArchAcc_R

lemma setObject_ASIDPool_corres [corres]:
  "p = p' \<Longrightarrow> a = inv ASIDPool a' o ucast \<Longrightarrow>
  corres dc (asid_pool_at p and valid_etcbs) (asid_pool_at' p')
            (set_asid_pool p a) (setObject p' a')" apply (simp add: set_asid_pool_def) apply (corresKsimp search: setObject_other_corres[where P="\<lambda>_. True"]
                        wp: get_object_ret get_object_wp) apply (simp add: other_obj_relation_def asid_pool_relation_def) apply (clarsimp simp: obj_at_simps ) by (auto simp: obj_at_simps typ_at_to_obj_at_arches
          split: Structures_A.kernel_object.splits if_splits arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = p'; a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres dc (typ_at (AArch AASIDPool) p and valid_etcbs) (asid_pool_at' p') (set_asid_pool p a) (setObject p' a') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = p'; a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32)\<rbrakk> \<Longrightarrow> corres dc (typ_at (AArch AASIDPool) p' and valid_etcbs) (asid_pool_at' p') (set_object p' (ArchObj (arch_kernel_obj.ASIDPool (inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32))))) (setObject p' a') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>p = p'; a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32); asid_pool_at' p' s'; (s, s') \<in> state_relation; typ_at (AArch AASIDPool) p' s; valid_etcbs s\<rbrakk> \<Longrightarrow> (\<forall>s. obj_at' (\<lambda>_. True) p' s \<longrightarrow> map_to_ctes ((ksPSpace s)(p' \<mapsto> KOArch (KOASIDPool a'))) = ctes_of s) \<and> is_other_obj_relation_type (a_type (ArchObj (arch_kernel_obj.ASIDPool (inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32))))) \<and> (\<forall>ko. objBits ko = objBits a') \<and> (\<forall>v. 1 < 2 ^ objBits v) \<and> other_obj_relation (ArchObj (arch_kernel_obj.ASIDPool (inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32)))) (KOArch (KOASIDPool a')) \<and> typ_at (a_type (ArchObj (arch_kernel_obj.ASIDPool (inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32))))) p' s \<and> obj_at (\<lambda>val. \<exists>ao'. val = ArchObj ao') p' s \<and> obj_at' (\<lambda>_. True) p' s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>p = p'; a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32); asid_pool_at' p' s'; (s, s') \<in> state_relation; typ_at (AArch AASIDPool) p' s; valid_etcbs s\<rbrakk> \<Longrightarrow> (\<forall>s. obj_at' (\<lambda>_. True) p' s \<longrightarrow> map_to_ctes ((ksPSpace s)(p' \<mapsto> KOArch (KOASIDPool a'))) = ctes_of s) \<and> is_other_obj_relation_type (a_type (ArchObj (arch_kernel_obj.ASIDPool (inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32))))) \<and> (\<forall>ko. objBits ko = objBits a') \<and> (\<forall>v. 1 < 2 ^ objBits v) \<and> typ_at (a_type (ArchObj (arch_kernel_obj.ASIDPool (inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32))))) p' s \<and> obj_at (\<lambda>val. \<exists>ao'. val = ArchObj ao') p' s \<and> obj_at' (\<lambda>_. True) p' s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko. \<lbrakk>p = p'; a = inv asidpool.ASIDPool a' \<circ> UCAST(10 \<rightarrow> 32); asid_pool_at' p' s'; (s, s') \<in> state_relation; valid_etcbs s; kheap s p' = Some ko; (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 (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch AASIDPool\<rbrakk> \<Longrightarrow> (\<forall>s. (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOArch (KOASIDPool obj)) \<and> ps_clear p' (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<longrightarrow> map_to_ctes ((ksPSpace s)(p' \<mapsto> KOArch (KOASIDPool a'))) = ctes_of s) \<and> (\<exists>ao'. ko = ArchObj ao') \<and> (\<exists>ko. ksPSpace s' p' = Some ko \<and> is_aligned p' (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOArch (KOASIDPool obj)) \<and> ps_clear p' (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s')