theory Detype_R

lemma createObject_updateNewFreeIndex_commute:
  "monad_commute
     (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and
      pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and
      valid_arch_state' and
      K (ptr \<noteq> slot) 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 dev) (updateNewFreeIndex slot)" apply (simp add: updateNewFreeIndex_def getSlotCap_def case_eq_if_isUntypedCap
                   updateTrackedFreeIndex_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF _ createObject_getCTE_commute]) apply (rule monad_commute_If_rhs) apply (rule createObject_updateTrackedFreeIndex_commute) apply (rule commute_commute[OF return_commute]) apply (wp getCTE_wp') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) (global.createObject ty ptr us dev) (updateNewFreeIndex slot) proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) (global.createObject ty ptr us dev) (do cte <- getCTE slot;
if isUntypedCap (cteCap cte) then updateTrackedFreeIndex slot (capFreeIndex (cteCap cte)) else return ()
od) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P2 (global.createObject ty ptr us dev) (do cte <- getCTE slot;
if isUntypedCap (cteCap cte) then updateTrackedFreeIndex slot (capFreeIndex (cteCap cte)) else return ()
od)
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> ?P2 s proof (prove)
goal (3 subgoals):
 1. \<And>r. monad_commute (?Q5 r) (global.createObject ty ptr us dev) (if isUntypedCap (cteCap r) then updateTrackedFreeIndex slot (capFreeIndex (cteCap r)) else return ())
 2. \<lbrace>?P'5\<rbrace> getCTE slot \<lbrace>?Q5\<rbrace>
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'5) s proof (prove)
goal (4 subgoals):
 1. \<And>r. monad_commute (?P10 r) (global.createObject ty ptr us dev) (updateTrackedFreeIndex slot (capFreeIndex (cteCap r)))
 2. \<And>r. monad_commute (?Q10 r) (global.createObject ty ptr us dev) (return ())
 3. \<lbrace>?P'5\<rbrace> getCTE slot \<lbrace>\<lambda>r s. (isUntypedCap (cteCap r) \<longrightarrow> ?P10 r s) \<and> (\<not> isUntypedCap (cteCap r) \<longrightarrow> ?Q10 r s)\<rbrace>
 4. \<And>s. (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'5) s proof (prove)
goal (3 subgoals):
 1. \<And>r. monad_commute (?Q10 r) (global.createObject ty ptr us dev) (return ())
 2. \<lbrace>?P'5\<rbrace> getCTE slot \<lbrace>\<lambda>r s. (isUntypedCap (cteCap r) \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s) \<and> (\<not> isUntypedCap (cteCap r) \<longrightarrow> ?Q10 r s)\<rbrace>
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'5) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'5\<rbrace> getCTE slot \<lbrace>\<lambda>r s. (isUntypedCap (cteCap r) \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s) \<and> (\<not> isUntypedCap (cteCap r) \<longrightarrow> True)\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'5) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. ptr \<noteq> slot) and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. is_aligned ptr (getObjectSize ty us))) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> (isUntypedCap (cteCap cte) \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))) s) \<and> (\<not> isUntypedCap (cteCap cte) \<longrightarrow> True))) s proof (prove)
goal:
No subgoals!