theory Detype_R

lemma modify_pde_pde_at':
  "\<lbrace>pde_at' ptr\<rbrace>
   modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))))
   \<lbrace>\<lambda>a. pde_at' ptr\<rbrace>" apply wp apply (clarsimp simp del: fun_upd_apply
                  simp: typ_at'_def ko_wp_at'_def objBits_simps archObjSize_def) apply (clarsimp simp:ps_clear_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (clarsimp simp:archObjSize_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pde_at' ptr\<rbrace> modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde)))) \<lbrace>\<lambda>a. pde_at' ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pde_at' ptr s \<Longrightarrow> pde_at' ptr (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits); koTypeOf ko = ArchT PDET; ps_clear ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s\<rbrakk> \<Longrightarrow> \<exists>ko. ((ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde))) ptr = Some ko \<and> is_aligned ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) \<and> koTypeOf ko = ArchT PDET \<and> ps_clear ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits); koTypeOf ko = ArchT PDET; ({ptr..ptr + 2 ^ (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) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> is_aligned ptr (archObjSize (KOPDE new_pde)) \<and> ({ptr..ptr + 2 ^ archObjSize (KOPDE new_pde) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>ksPSpace s ptr = Some (KOArch x8); is_aligned ptr (archObjSize x8); archTypeOf x8 = PDET; ({ptr..ptr + 2 ^ archObjSize x8 - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; ko = KOArch x8\<rbrakk> \<Longrightarrow> is_aligned ptr (archObjSize (KOPDE new_pde)) \<and> ({ptr..ptr + 2 ^ archObjSize (KOPDE new_pde) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (archObjSize arch_kernel_object); archTypeOf arch_kernel_object = PDET; ({ptr..ptr + 2 ^ archObjSize arch_kernel_object - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> is_aligned ptr (archObjSize (KOPDE new_pde)) \<and> ({ptr..ptr + 2 ^ archObjSize (KOPDE new_pde) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (archObjSize (KOPDE x3)); ({ptr..ptr + 2 ^ archObjSize (KOPDE x3) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> is_aligned ptr (archObjSize (KOPDE new_pde)) \<and> ({ptr..ptr + 2 ^ archObjSize (KOPDE new_pde) - 1} - {ptr}) \<inter> dom (ksPSpace s) = {} proof (prove)
goal:
No subgoals!