theory Detype_R

lemma createObject_getCTE_commute:
  "monad_commute
     (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and
      pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and
      K (ptr \<noteq> dests) and K (Types_H.getObjectSize ty us < word_bits) and
      K (is_aligned ptr (Types_H.getObjectSize ty us)))
     (RetypeDecls_H.createObject ty ptr us d) (getCTE dests)" apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule getCTE_commute) apply (rule hoare_pre) apply (wp createObject_cte_wp_at') apply (clarsimp simp:cte_wp_at_ctes_of) apply assumption apply (clarsimp simp:cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) (global.createObject ty ptr us d) (getCTE dests) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (getCTE dests) (global.createObject ty ptr us d)
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> ?P s proof (prove)
goal (2 subgoals):
 1. \<And>Q. \<lbrace>\<lambda>s. ?P4 s \<and> cte_wp_at' Q dests s\<rbrace> global.createObject ty ptr us d \<lbrace>\<lambda>a. cte_wp_at' Q dests\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (?P4 and cte_wp_at' (\<lambda>_. True) dests) s proof (prove)
goal (3 subgoals):
 1. \<And>Q. \<lbrace>?Q6 Q\<rbrace> global.createObject ty ptr us d \<lbrace>\<lambda>a. cte_wp_at' Q dests\<rbrace>
 2. \<And>Q s. ?P4 s \<and> cte_wp_at' Q dests s \<Longrightarrow> ?Q6 Q s
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (?P4 and cte_wp_at' (\<lambda>_. True) dests) s proof (prove)
goal (2 subgoals):
 1. \<And>Q s. ?P4 s \<and> cte_wp_at' Q dests s \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned ptr (getObjectSize ty us) \<and> pspace_no_overlap' ptr (getObjectSize ty us) s \<and> cte_wp_at' Q dests s \<and> pspace_aligned' s \<and> pspace_distinct' s
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (?P4 and cte_wp_at' (\<lambda>_. True) dests) s proof (prove)
goal (2 subgoals):
 1. \<And>Q s cte. \<lbrakk>?P4 s; ctes_of s dests = Some cte; Q cte\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits \<and> is_aligned ptr (getObjectSize ty us) \<and> pspace_no_overlap' ptr (getObjectSize ty us) s \<and> pspace_aligned' s \<and> pspace_distinct' s
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (?P4 and cte_wp_at' (\<lambda>_. True) dests) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> dests) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> ((\<lambda>s. getObjectSize ty us < word_bits \<and> is_aligned ptr (getObjectSize ty us) \<and> pspace_no_overlap' ptr (getObjectSize ty us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) and cte_wp_at' (\<lambda>_. True) dests) s proof (prove)
goal:
No subgoals!