theory Detype_R

lemma setCTE_placeNewObject_commute:
  "monad_commute
     (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
         objBitsKO (injectKOS val) + us < word_bits) and
      K(ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and
      pspace_aligned' and pspace_distinct' and
      pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us))
     (setCTE src cte) (placeNewObject ptr val us)" apply (clarsimp simp: setCTE_def2 split_def) apply (rule commute_commute) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF placeNewObject_modify_commute]) apply (rule placeNewObject_locateCTE_commute) apply (wp locateCTE_inv locateCTE_ko_wp_at' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and K (ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) (setCTE src cte) (placeNewObject ptr val us) proof (prove)
goal (1 subgoal):
 1. monad_commute ((\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od) (placeNewObject ptr val us) proof (prove)
goal (1 subgoal):
 1. monad_commute ((\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) (placeNewObject ptr val us) (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P2 (placeNewObject ptr val us) (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od)
 2. \<And>s. ((\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> ?P2 s proof (prove)
goal (3 subgoals):
 1. monad_commute ?P5 (placeNewObject ptr val us) (locateCTE src)
 2. \<lbrace>?P'5\<rbrace> locateCTE src \<lbrace>\<lambda>ptra. K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and ko_wp_at' (\<lambda>a. objBitsKO (cte_update cte (the (Some a)) src ptra) = objBitsKO a) ptra\<rbrace>
 3. \<And>s. ((\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> (?P5 and ?P'5) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'5\<rbrace> locateCTE src \<lbrace>\<lambda>ptra. K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and ko_wp_at' (\<lambda>a. objBitsKO (cte_update cte (the (Some a)) src ptra) = objBitsKO a) ptra\<rbrace>
 2. \<And>s. ((\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> ptr \<noteq> src) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) src and ?P'5) s proof (prove)
goal:
No subgoals!