theory Detype_R

lemma placeNewObject_locateCTE_commute:
  "monad_commute
     (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_at' src)
     (placeNewObject ptr val us) (locateCTE src)" apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF locateCTE_commute]) apply (wp no_fail_placeNewObject locateCTE_cte_no_fail
        placeNewObject_pspace_aligned'
        placeNewObject_pspace_distinct'
        placeNewObject_ko_wp_at' | simp)+ apply (clarsimp simp:ko_wp_at'_def) apply (drule(3) not_in_new_cap_addrs) apply fastforce+ apply (wp placeNewObject_cte_wp_at'') apply clarsimp apply fastforce 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> 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) (placeNewObject ptr val us) (locateCTE src) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (placeNewObject ptr val us) (locateCTE src)
 2. \<And>s. (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) s \<Longrightarrow> ?P s proof (prove)
goal (7 subgoals):
 1. no_fail ?P0.4 (placeNewObject ptr val us)
 2. no_fail ?P1.4 (locateCTE src)
 3. \<lbrace>?P2.4\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
 4. \<lbrace>?P3.4\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
 5. \<And>Q dest. \<lbrace>\<lambda>s. (?P0.4 and ?P1.4 and ?P2.4 and ?P3.4) s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest\<rbrace>
 6. \<And>dest. \<lbrace>\<lambda>s. (?P0.4 and ?P1.4 and ?P2.4 and ?P3.4) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 7. \<And>s. (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) s \<Longrightarrow> (?P0.4 and ?P1.4 and ?P2.4 and ?P3.4 and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal (3 subgoals):
 1. \<And>Q dest s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>_. True) src s \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s \<Longrightarrow> dest \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) \<longrightarrow> Q (objBitsKO (injectKOS val))
 2. \<And>dest. \<lbrace>\<lambda>s. ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us))) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s. (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) s \<Longrightarrow> ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal (3 subgoals):
 1. \<And>Q dest s ko. \<lbrakk>cte_wp_at' (\<lambda>_. True) src s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ksPSpace s dest = Some ko; is_aligned dest (objBitsKO ko); Q (objBitsKO ko); ps_clear dest (objBitsKO ko) s; dest \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> Q (objBitsKO (injectKOS val))
 2. \<And>dest. \<lbrace>\<lambda>s. ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us))) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<And>s. (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) s \<Longrightarrow> ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>Q dest s ko. \<lbrakk>cte_wp_at' (\<lambda>_. True) src s; objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ksPSpace s dest = Some ko; is_aligned dest (objBitsKO ko); Q (objBitsKO ko); ps_clear dest (objBitsKO ko) s; dest \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>Q dest s ko. \<lbrakk>cte_wp_at' (\<lambda>_. True) src s; objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; ksPSpace s dest = Some ko; is_aligned dest (objBitsKO ko); Q (objBitsKO ko); ps_clear dest (objBitsKO ko) s; dest \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)); dest \<notin> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))\<rbrakk> \<Longrightarrow> Q (objBitsKO (injectKOS val))
 3. \<And>dest. \<lbrace>\<lambda>s. ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us))) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 4. \<And>s. (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) s \<Longrightarrow> ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal (2 subgoals):
 1. \<And>dest. \<lbrace>\<lambda>s. ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us))) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 2. \<And>s. (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) s \<Longrightarrow> ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal (2 subgoals):
 1. \<And>dest s. ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us))) s \<and> cte_wp_at' (\<lambda>_. True) dest s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest s \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s
 2. \<And>s. (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) s \<Longrightarrow> ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (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) s \<Longrightarrow> ((\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) and cte_wp_at' (\<lambda>_. True) src and (\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) and ?P4.4 and ?P5.4 and pspace_aligned' and pspace_distinct') s proof (prove)
goal:
No subgoals!