theory Finalise_DR

lemma dcorres_store_invalid_pde_tail_super_section:
  "dcorres dc \<top> (valid_idle and
    (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
    \<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE))
    and K (\<forall>sl\<in> set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits))
  (return a)
  (mapM (swp store_pde ARM_A.pde.InvalidPDE) slots)" proof (induct slots arbitrary:a) case Nil show ?case by (simp add:mapM_Nil) next case (Cons x xs) show ?case apply (rule corres_guard_imp) apply (simp add:mapM_Cons dc_def[symmetric]) apply (rule corres_dummy_return_l) apply (rule corres_split[OF dcorres_store_pde_non_sense]) apply (rule corres_dummy_return_l) apply (rule corres_split[OF Cons.hyps[unfolded swp_def]]) apply (rule corres_free_return[where P=\<top> and P'=\<top>]) apply wp+ apply simp apply (wp store_pde_non_sense_wp) apply simp apply (clarsimp simp:obj_at_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set slots. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) slots) proof (state)
goal (2 subgoals):
 1. \<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set []. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set []. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) [])
 2. \<And>a slots aa. (\<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set slots. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) slots)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (a # slots). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (a # slots). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return aa) (mapM (swp store_pde InvalidPDE) (a # slots)) proof (state)
this:


goal (2 subgoals):
 1. \<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set []. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set []. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) [])
 2. \<And>a slots aa. (\<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set slots. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) slots)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (a # slots). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (a # slots). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return aa) (mapM (swp store_pde InvalidPDE) (a # slots)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set []. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set []. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) []) proof (state)
this:
dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set []. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set []. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) [])

goal (1 subgoal):
 1. \<And>a slots aa. (\<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set slots. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) slots)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (a # slots). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (a # slots). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return aa) (mapM (swp store_pde InvalidPDE) (a # slots)) proof (state)
goal (1 subgoal):
 1. \<And>a slots aa. (\<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set slots. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) slots)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (a # slots). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (a # slots). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return aa) (mapM (swp store_pde InvalidPDE) (a # slots)) proof (state)
this:
dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return ?a) (mapM (swp store_pde InvalidPDE) xs)

goal (1 subgoal):
 1. \<And>a slots aa. (\<And>a. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set slots. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) slots)) \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (a # slots). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (a # slots). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return aa) (mapM (swp store_pde InvalidPDE) (a # slots)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) (x # xs)) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (return a) (mapM (swp store_pde InvalidPDE) (x # xs))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (return a) (do y <- store_pde x InvalidPDE;
ys <- mapM (\<lambda>a. store_pde a InvalidPDE) xs;
return (() # ys)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (return a >>= return) (do y <- store_pde x InvalidPDE;
ys <- mapM (\<lambda>a. store_pde a InvalidPDE) xs;
return (() # ys)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R6 x) (?R'6 rv') (return x) (do ys <- mapM (\<lambda>a. store_pde a InvalidPDE) xs;
return (() # ys)
od)
 2. \<lbrace>?Q6\<rbrace> return a \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> store_pde x InvalidPDE \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>x rv'. dc x rv' \<Longrightarrow> dcorres dc (?R6 x) (?R'6 rv') (return x >>= return) (do ys <- mapM (\<lambda>a. store_pde a InvalidPDE) xs;
return (() # ys)
od)
 2. \<lbrace>?Q6\<rbrace> return a \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> store_pde x InvalidPDE \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>x rv' xa ys. \<lbrakk>dc x rv'; dc xa ys\<rbrakk> \<Longrightarrow> dcorres dc (?R13 x rv' xa) (?R'13 x rv' ys) (return xa) (return (() # ys))
 2. \<And>x rv'. dc x rv' \<Longrightarrow> \<lbrace>?Q15 x\<rbrace> return x \<lbrace>?R13 x rv'\<rbrace>
 3. \<And>x rv'. dc x rv' \<Longrightarrow> \<lbrace>?Q'16 rv'\<rbrace> mapM (\<lambda>a. store_pde a InvalidPDE) xs \<lbrace>?R'13 x rv'\<rbrace>
 4. \<lbrace>?Q6\<rbrace> return a \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q15 x\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> store_pde x InvalidPDE \<lbrace>\<lambda>rv'. valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits) and ?Q'16 rv'\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>x rv'. dc x rv' \<Longrightarrow> \<lbrace>?Q15 x\<rbrace> return x \<lbrace>\<lambda>xa _. True\<rbrace>
 2. \<And>x rv'. dc x rv' \<Longrightarrow> \<lbrace>?Q'16 rv'\<rbrace> mapM (\<lambda>a. store_pde a InvalidPDE) xs \<lbrace>\<lambda>ys _. True\<rbrace>
 3. \<lbrace>?Q6\<rbrace> return a \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q15 x\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> store_pde x InvalidPDE \<lbrace>\<lambda>rv'. valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits) and ?Q'16 rv'\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and ?Q'6) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'34\<rbrace> store_pde x InvalidPDE \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> K (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits) s \<and> True\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 3. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and (\<lambda>s. valid_idle s \<and> ?P'34 s)) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'34\<rbrace> store_pde x InvalidPDE \<lbrace>\<lambda>rv s. (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 3. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and (\<lambda>s. valid_idle s \<and> ?P'34 s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 2. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and (\<lambda>s. valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) s \<Longrightarrow> (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE) and (\<lambda>s. valid_idle s \<and> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) \<and> (\<forall>sl\<in>set xs. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits))) s proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set (x # xs). f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) and K (\<forall>sl\<in>set (x # xs). sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) (return a) (mapM (swp store_pde InvalidPDE) (x # xs))

goal:
No subgoals!