theory Detype_R

lemma storePDE_setCTE_commute:
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  shows "monad_commute
     (pde_at' ptr and pspace_distinct' and pspace_aligned' and
      cte_wp_at' (\<lambda>_. True) src)
     (setCTE src cte) (storePDE ptr (new_pde::ARM_H.pde))" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF storePDE_det]) apply assumption apply (wp setCTE_pde_at') apply (simp add:setCTE_def2) apply (rule monad_commute_split) apply (subst modify_specify) apply (rule modify_obj_commute') apply (rule commute_commute[OF locateCTE_commute]) apply (wp locateCTE_cte_no_fail no_fail_modify
                   modify_pde_pspace_distinct'
                   modify_pde_pspace_aligned'| subst modify_specify)+ apply (clarsimp simp:simpler_modify_def valid_def typ_at'_def) apply (clarsimp simp:ko_wp_at'_def dest!: koTypeOf_pde) apply (intro conjI impI) apply (clarsimp simp:objBits_simps archObjSize_def)+ apply (simp add:ps_clear_def in_dom_eq) apply (simp add:ps_clear_def in_dom_eq) apply (clarsimp simp:simpler_modify_def valid_def) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all add:koTypeOf_def )[1] apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all add:archTypeOf_def)[1] apply (erule(2) cte_wp_at_modify_pde) apply wp apply (thin_tac "cte_wp_at' P src s" for P s)+ apply (clarsimp simp: typ_at'_def cte_wp_at_obj_cases_mask obj_at'_real_def) apply (wp locateCTE_ret_neq locateCTE_ko_wp_at') apply (clarsimp simp:ko_wp_at'_def objBits_simps archObjSize_def typ_at'_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (pde_at' ptr and pspace_distinct' and pspace_aligned' and cte_wp_at' (\<lambda>_. True) src) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pde_at' ptr and pspace_distinct' and pspace_aligned' and cte_wp_at' (\<lambda>_. True) src) s \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some ko; pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch x8); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch x8)); archTypeOf x8 = PDET; ps_clear ptr (objBitsKO (KOArch x8)) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch arch_kernel_object); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = PDET; ps_clear ptr (objBitsKO (KOArch arch_kernel_object)) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (storePDE ptr new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P14 s pde) (setCTE src cte) (storePDE ptr new_pde)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> ?P14 s pde sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P14 s pde) (storePDE ptr new_pde) (setCTE src cte)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> ?P14 s pde sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; ?Q19 s pde sa\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE (?pde20 s pde sa)))) ptr sa
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s pde\<rbrace> setCTE src cte \<lbrace>\<lambda>x. ?Q19 s pde\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?R19 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (setCTE src cte)
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (?P19 s pde and ?Q19 s pde and ?R19 s pde) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s pde\<rbrace> setCTE src cte \<lbrace>\<lambda>x sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde20 s pde sa)))) ptr sa\<rbrace>
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?R19 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (setCTE src cte)
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (?P19 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde20 s pde sa)))) ptr sa) and ?R19 s pde) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?R19 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (setCTE src cte)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ?R19 s pde) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?R19 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ?R19 s pde) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde r. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?Q28 s pde r) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (modify (ksPSpace_update (\<lambda>ps. ps(r \<mapsto> cte_update cte (the (ps r)) src r))))
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P28 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (locateCTE src)
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>?Q28 s pde\<rbrace>
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and (?P28 s pde and ?P'28 s pde)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde r. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?Q33 s pde r (?s33 s pde r) (?pdea33 s pde r) r) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))))) (modify (ksPSpace_update (\<lambda>ps. ps(r \<mapsto> cte_update cte (the (ps r)) src r))))
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P28 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (locateCTE src)
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. ?Q33 s pde r (?s33 s pde r) (?pdea33 s pde r) r\<rbrace>
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and (?P28 s pde and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P28 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s) (locateCTE src)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and (?P28 s pde and ?P'28 s pde)) sa proof (prove)
goal (8 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> no_fail (?P0.37 s pde) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> no_fail (?P1.37 s pde) (locateCTE src)
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P2.37 s pde\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
 4. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P3.37 s pde\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
 5. \<And>s pde Q dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (?P0.37 s pde and ?P1.37 s pde and ?P2.37 s pde and ?P3.37 s pde) sa \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest sa\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest\<rbrace>
 6. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. (?P0.37 s pde and ?P1.37 s pde and ?P2.37 s pde and ?P3.37 s pde) sa \<and> cte_wp_at' (\<lambda>_. True) dest sa\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 7. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 8. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and (?P0.37 s pde and ?P1.37 s pde and ?P2.37 s pde and ?P3.37 s pde and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde Q dest sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) sa \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest sa\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> KOArch (KOPDE new_pde))) sa)
 2. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde Q dest sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) ptr sa; pspace_aligned' sa; ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest sa\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)
 2. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa\<rbrakk> \<Longrightarrow> (dest = ptr \<longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE new_pde))) \<and> Q (objBitsKO (KOArch (KOPDE new_pde))) \<and> ps_clear ptr (objBitsKO (KOArch (KOPDE new_pde))) (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)) \<and> (dest \<noteq> ptr \<longrightarrow> ps_clear dest (objBitsKO koa) (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa))
 2. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (7 subgoals):
 1. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa; dest = ptr\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE new_pde)))
 2. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa; dest = ptr\<rbrakk> \<Longrightarrow> Q (objBitsKO (KOArch (KOPDE new_pde)))
 3. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa; dest = ptr\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO (KOArch (KOPDE new_pde))) (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)
 4. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa; dest \<noteq> ptr\<rbrakk> \<Longrightarrow> ps_clear dest (objBitsKO koa) (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)
 5. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 6. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 7. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (5 subgoals):
 1. \<And>s pde Q sa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr pdeBits; ps_clear ptr pdeBits s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ps_clear ptr pdeBits sa; Q pdeBits\<rbrakk> \<Longrightarrow> ps_clear ptr pdeBits (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)
 2. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa; dest \<noteq> ptr\<rbrakk> \<Longrightarrow> ps_clear dest (objBitsKO koa) (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)
 3. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 4. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 5. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde Q dest sa koa pdea. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pdea)); ksPSpace sa dest = Some koa; is_aligned ptr (objBitsKO (KOArch (KOPDE pdea))); is_aligned dest (objBitsKO koa); ps_clear ptr (objBitsKO (KOArch (KOPDE pdea))) sa; Q (objBitsKO koa); ps_clear dest (objBitsKO koa) sa; dest \<noteq> ptr\<rbrakk> \<Longrightarrow> ps_clear dest (objBitsKO koa) (ksPSpace_update (\<lambda>ps a. if a = ptr then Some (KOArch (KOPDE new_pde)) else ps a) sa)
 2. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde dest. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned')) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> \<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(ptr \<mapsto> KOArch (KOPDE new_pde)))) s \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde dest sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pde_at' ptr sa; pspace_aligned' sa; cte_wp_at' (\<lambda>_. True) dest sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest (sa\<lparr>ksPSpace := (ksPSpace sa)(ptr \<mapsto> KOArch (KOPDE new_pde))\<rparr>)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde dest sa ko. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; cte_wp_at' (\<lambda>_. True) dest sa; ksPSpace sa ptr = Some ko; is_aligned ptr (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear ptr (objBitsKO ko) sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest (sa\<lparr>ksPSpace := (ksPSpace sa)(ptr \<mapsto> KOArch (KOPDE new_pde))\<rparr>)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde dest sa ko x8. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; cte_wp_at' (\<lambda>_. True) dest sa; ksPSpace sa ptr = Some (KOArch x8); is_aligned ptr (objBitsKO (KOArch x8)); archTypeOf x8 = PDET; ps_clear ptr (objBitsKO (KOArch x8)) sa; ko = KOArch x8\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest (sa\<lparr>ksPSpace := (ksPSpace sa)(ptr \<mapsto> KOArch (KOPDE new_pde))\<rparr>)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde dest sa ko arch_kernel_object. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; cte_wp_at' (\<lambda>_. True) dest sa; ksPSpace sa ptr = Some (KOArch arch_kernel_object); is_aligned ptr (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = PDET; ps_clear ptr (objBitsKO (KOArch arch_kernel_object)) sa; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest (sa\<lparr>ksPSpace := (ksPSpace sa)(ptr \<mapsto> KOArch (KOPDE new_pde))\<rparr>)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde dest sa ko arch_kernel_object x3. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; cte_wp_at' (\<lambda>_. True) src sa; pspace_distinct' sa; pspace_aligned' sa; cte_wp_at' (\<lambda>_. True) dest sa; ksPSpace sa ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) sa; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest (sa\<lparr>ksPSpace := (ksPSpace sa)(ptr \<mapsto> KOArch (KOPDE new_pde))\<rparr>)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r. K (ptr \<noteq> r) and ko_wp_at' (\<lambda>_. True) r\<rbrace>
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r s. K (ptr \<noteq> r) s \<and> ko_wp_at' (\<lambda>_. True) r s\<rbrace>
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r s. K (ptr \<noteq> r) s \<and> ko_wp_at' (\<lambda>_. True) r s\<rbrace>
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 s pde\<rbrace> locateCTE src \<lbrace>\<lambda>r s. ptr \<noteq> r \<and> ko_wp_at' (\<lambda>_. True) r s\<rbrace>
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and ?P'28 s pde)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde26 s pde)))) ptr and ((\<lambda>a. True) and cte_wp_at' (\<lambda>_. True) src and (pde_at' ptr and pspace_distinct') and (pde_at' ptr and pspace_aligned') and ?P4.37 s pde and ?P5.37 s pde and pspace_aligned' and pspace_distinct' and (\<lambda>s. ko_wp_at' (\<lambda>x. koTypeOf x \<noteq> TCBT \<and> koTypeOf x \<noteq> CTET) ptr s \<and> (cte_wp_at' (\<lambda>_. True) src and pspace_distinct') s))) sa proof (prove)
goal (1 subgoal):
 1. \<And>pde sa. \<lbrakk>pspace_distinct' sa; ksPSpace sa ptr = Some (KOArch (KOPDE pde)); pspace_aligned' sa; cte_wp_at' (\<lambda>_. True) src sa; is_aligned ptr pdeBits; ps_clear ptr pdeBits sa\<rbrakk> \<Longrightarrow> ?pde26 sa pde = pde \<and> pde = ?pde26 sa pde \<and> ?P4.37 sa pde sa \<and> ?P5.37 sa pde sa proof (prove)
goal:
No subgoals!