theory Detype_R

lemma setCTE_doMachineOp_commute:
  assumes nf: "no_fail Q (doMachineOp x)"
  shows "monad_commute (cte_at' dest and pspace_aligned' and pspace_distinct' and Q)
  (setCTE dest cte)
  (doMachineOp x)" apply (simp add:setCTE_def2 split_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule doMachineOp_upd_heap_commute) apply (rule commute_commute[OF locateCTE_commute]) apply (wp nf locateCTE_cte_no_fail)+ apply clarsimp apply (wp|clarsimp|fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) (setCTE dest cte) (doMachineOp x) proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) (do ptr <- locateCTE dest;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) dest ptr)))
od) (doMachineOp x) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (do ptr <- locateCTE dest;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) dest ptr)))
od) (doMachineOp x)
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>r. monad_commute (?Q4 r) (doMachineOp x) (modify (ksPSpace_update (\<lambda>ps. ps(r \<mapsto> cte_update cte (the (ps r)) dest r))))
 2. monad_commute ?P4 (doMachineOp x) (locateCTE dest)
 3. \<lbrace>?P'4\<rbrace> locateCTE dest \<lbrace>?Q4\<rbrace>
 4. \<And>s. (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (3 subgoals):
 1. monad_commute ?P4 (doMachineOp x) (locateCTE dest)
 2. \<lbrace>?P'4\<rbrace> locateCTE dest \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (8 subgoals):
 1. no_fail ?P0.10 (doMachineOp x)
 2. no_fail ?P1.10 (locateCTE dest)
 3. \<lbrace>?P2.10\<rbrace> doMachineOp x \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
 4. \<lbrace>?P3.10\<rbrace> doMachineOp x \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
 5. \<And>Q dest. \<lbrace>\<lambda>s. (?P0.10 and ?P1.10 and ?P2.10 and ?P3.10) s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s\<rbrace> doMachineOp x \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest\<rbrace>
 6. \<And>dest. \<lbrace>\<lambda>s. (?P0.10 and ?P1.10 and ?P2.10 and ?P3.10) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> doMachineOp x \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 7. \<lbrace>?P'4\<rbrace> locateCTE dest \<lbrace>\<lambda>r _. True\<rbrace>
 8. \<And>s. (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) s \<Longrightarrow> (?P0.10 and ?P1.10 and ?P2.10 and ?P3.10 and ?P4.10 and ?P5.10 and pspace_aligned' and pspace_distinct' and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>Qa desta s. (Q and cte_wp_at' (\<lambda>_. True) dest and pspace_distinct' and pspace_aligned') s \<and> ko_wp_at' (\<lambda>obj. Qa (objBitsKO obj)) desta s \<Longrightarrow> ko_wp_at' (\<lambda>a. Qa (objBitsKO a)) desta s
 2. \<And>desta. \<lbrace>\<lambda>s. (Q and cte_wp_at' (\<lambda>_. True) dest and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) desta s\<rbrace> doMachineOp x \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) desta\<rbrace>
 3. \<lbrace>?P'4\<rbrace> locateCTE dest \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>s. (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) s \<Longrightarrow> (Q and cte_wp_at' (\<lambda>_. True) dest and pspace_distinct' and pspace_aligned' and ?P4.10 and ?P5.10 and pspace_aligned' and pspace_distinct' and ?P'4) s proof (prove)
goal (3 subgoals):
 1. \<And>desta. \<lbrace>\<lambda>s. (Q and cte_wp_at' (\<lambda>_. True) dest and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) desta s\<rbrace> doMachineOp x \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) desta\<rbrace>
 2. \<lbrace>?P'4\<rbrace> locateCTE dest \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) dest and pspace_aligned' and pspace_distinct' and Q) s \<Longrightarrow> (Q and cte_wp_at' (\<lambda>_. True) dest and pspace_distinct' and pspace_aligned' and ?P4.10 and ?P5.10 and pspace_aligned' and pspace_distinct' and ?P'4) s proof (prove)
goal:
No subgoals!