theory Detype_R

lemma createObject_updateMDB_commute:
  "monad_commute
     ((\<lambda>s. src \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) src s) and
      pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and
      pspace_aligned' and pspace_distinct' and valid_arch_state' and
      K (ptr \<noteq> src) and
      K (is_aligned ptr (Types_H.getObjectSize ty us)) and
      K ((Types_H.getObjectSize ty us)< word_bits))
     (updateMDB src f) (RetypeDecls_H.createObject ty ptr us d)" apply (clarsimp simp:updateMDB_def split:if_split_asm) apply (intro conjI impI) apply (simp add: monad_commute_guard_imp[OF return_commute]) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule createObject_setCTE_commute) apply (rule createObject_getCTE_commute) apply wp apply (auto simp:range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute ((\<lambda>s. src \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) src s) and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \<noteq> src) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits)) (updateMDB src f) (global.createObject ty ptr us d) proof (prove)
goal (1 subgoal):
 1. (src = 0 \<longrightarrow> monad_commute (pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> 0) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) (return ()) (global.createObject ty ptr us d)) \<and> (src \<noteq> 0 \<longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) (do cte <- getCTE src;
setCTE src (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od) (global.createObject ty ptr us d)) proof (prove)
goal (2 subgoals):
 1. src = 0 \<Longrightarrow> monad_commute (pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> 0) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) (return ()) (global.createObject ty ptr us d)
 2. src \<noteq> 0 \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) (do cte <- getCTE src;
setCTE src (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od) (global.createObject ty ptr us d) proof (prove)
goal (1 subgoal):
 1. src \<noteq> 0 \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) (do cte <- getCTE src;
setCTE src (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od) (global.createObject ty ptr us d) proof (prove)
goal (2 subgoals):
 1. src \<noteq> 0 \<Longrightarrow> monad_commute ?P8 (do cte <- getCTE src;
setCTE src (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od) (global.createObject ty ptr us d)
 2. \<And>s. \<lbrakk>src \<noteq> 0; (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) s\<rbrakk> \<Longrightarrow> ?P8 s proof (prove)
goal (4 subgoals):
 1. \<And>r. src \<noteq> 0 \<Longrightarrow> monad_commute (?Q12 r) (global.createObject ty ptr us d) (setCTE src (cteMDBNode_update (\<lambda>_. f (cteMDBNode r)) r))
 2. src \<noteq> 0 \<Longrightarrow> monad_commute ?P12 (global.createObject ty ptr us d) (getCTE src)
 3. src \<noteq> 0 \<Longrightarrow> \<lbrace>?P'12\<rbrace> getCTE src \<lbrace>?Q12\<rbrace>
 4. \<And>s. \<lbrakk>src \<noteq> 0; (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) s\<rbrakk> \<Longrightarrow> (?P12 and ?P'12) s proof (prove)
goal (3 subgoals):
 1. src \<noteq> 0 \<Longrightarrow> monad_commute ?P12 (global.createObject ty ptr us d) (getCTE src)
 2. src \<noteq> 0 \<Longrightarrow> \<lbrace>?P'12\<rbrace> getCTE src \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> src) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits)\<rbrace>
 3. \<And>s. \<lbrakk>src \<noteq> 0; (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) s\<rbrakk> \<Longrightarrow> (?P12 and ?P'12) s proof (prove)
goal (2 subgoals):
 1. src \<noteq> 0 \<Longrightarrow> \<lbrace>?P'12\<rbrace> getCTE src \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> src) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits)\<rbrace>
 2. \<And>s. \<lbrakk>src \<noteq> 0; (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> src) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'12) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>src \<noteq> 0; (cte_wp_at' (\<lambda>_. True) src and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and (\<lambda>y. ptr \<noteq> src) and (\<lambda>y. is_aligned ptr (getObjectSize ty us)) and (\<lambda>y. getObjectSize ty us < word_bits)) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> src) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> src) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits))) s proof (prove)
goal:
No subgoals!