theory Detype_R

lemma placeNewObject_doMachineOp_commute:
  "monad_commute
     (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and>
         objBitsKO (injectKOS ty) + us < word_bits) and
      pspace_aligned' and pspace_distinct' and
      pspace_no_overlap' ptr ((objBitsKO (injectKOS ty)) +  us))
     (placeNewObject ptr ty us) (doMachineOp f)" apply (rule commute_name_pre_state) apply (rule monad_commute_guard_imp) apply (rule commute_rewrite [where Q =
               "pspace_no_overlap' ptr ((objBitsKO (injectKOS ty)) +  us) and pspace_aligned'"]) apply (rule simpler_placeNewObject_def; simp) apply (wp doMachineOp_psp_no_overlap) apply (simp add: modify_specify modify_mapM_x) apply (rule commute_commute) apply (rule mapM_x_commute[where f = id]) apply (rule doMachineOp_upd_heap_commute) apply wp apply clarsimp apply (rule new_cap_addrs_distinct[OF range_cover_rel]) apply (erule(1) range_cover_full) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) (placeNewObject ptr ty us) (doMachineOp f) proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr ty us) (doMachineOp f) proof (prove)
goal (2 subgoals):
 1. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> monad_commute (?P2 s) (placeNewObject ptr ty us) (doMachineOp f)
 2. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ?P2 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') sa\<rbrakk> \<Longrightarrow> placeNewObject ptr ty us sa = ?t5 s sa
 2. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> \<lbrace>?P5 s\<rbrace> doMachineOp f \<lbrace>\<lambda>x. pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned'\<rbrace>
 3. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> monad_commute (?R5 s) (?t5 s) (doMachineOp f)
 4. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> (?P5 s and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and ?R5 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> \<lbrace>?P5 s\<rbrace> doMachineOp f \<lbrace>\<lambda>x. pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned'\<rbrace>
 2. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> monad_commute (?R5 s) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS ty)) (new_cap_addrs (2 ^ us) ptr (injectKOS ty)) (ksPSpace sa))) sa) (doMachineOp f)
 3. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> (?P5 s and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and ?R5 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s \<Longrightarrow> monad_commute (?R5 s) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS ty)) (new_cap_addrs (2 ^ us) ptr (injectKOS ty)) (ksPSpace sa))) sa) (doMachineOp f)
 2. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) \<and> pspace_aligned' s) and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and ?R5 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<Longrightarrow> monad_commute (?R5 s) (mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS ty)))) (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty)))) (doMachineOp f)
 2. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) \<and> pspace_aligned' s) and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and ?R5 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<Longrightarrow> monad_commute (?R5 s) (doMachineOp f) (mapM_x (\<lambda>x. modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS ty)))) (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty))))
 2. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) \<and> pspace_aligned' s) and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and ?R5 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s r. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<Longrightarrow> monad_commute (?P32 s r) (doMachineOp f) (modify (ksPSpace_update (\<lambda>m. m(r \<mapsto> injectKOS ty))))
 2. \<And>s r x. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<Longrightarrow> \<lbrace>?P32 s r and K (id r \<noteq> id x) and ?P32 s x\<rbrace> modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS ty))) \<lbrace>\<lambda>v. ?P32 s r\<rbrace>
 3. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) \<and> pspace_aligned' s) and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and (\<lambda>sa. distinct (map id (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty))). ?P32 s r sa))) sa proof (prove)
goal (2 subgoals):
 1. \<And>s r x. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<Longrightarrow> \<lbrace>(\<lambda>_. True) and K (id r \<noteq> id x) and (\<lambda>_. True)\<rbrace> modify (ksPSpace_update (\<lambda>m. m(x \<mapsto> injectKOS ty))) \<lbrace>\<lambda>v _. True\<rbrace>
 2. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) \<and> pspace_aligned' s) and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and (\<lambda>s. distinct (map id (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty))). True))) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS ty) + us) \<and> objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s) \<and> pspace_aligned' s) and (pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) and pspace_aligned') and (\<lambda>s. distinct (map id (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty)))) \<and> (\<forall>r\<in>set (rev (new_cap_addrs (2 ^ us) ptr (injectKOS ty))). True))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> distinct (new_cap_addrs (2 ^ us) ptr (injectKOS ty)) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> range_cover ptr (?sz47 sa) (?sbit48 sa) (?n48 sa)
 2. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS ty) \<le> ?sbit48 sa
 3. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (?sbit48 sa - objBitsKO (injectKOS ty)) * ?n48 sa proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS ty) \<le> objBitsKO (injectKOS ty) + us
 2. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS ty) + us - objBitsKO (injectKOS ty)) * Suc 0 proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS ty) + us); objBitsKO (injectKOS ty) + us < word_bits; pspace_aligned' sa; pspace_distinct' sa; pspace_no_overlap' ptr (objBitsKO (injectKOS ty) + us) sa\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS ty) + us - objBitsKO (injectKOS ty)) * Suc 0 proof (prove)
goal:
No subgoals!