theory CNode_DR

lemma dcorres_dummy_empty_slot_pd_mapM_x:
  "\<forall>x\<in> set ls. 0xE00 \<le> unat x \<and> unat x < 4096
       \<Longrightarrow> dcorres dc \<top> (page_directory_at w and valid_idle)
           (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (ls::word32 list)))
           (return x)" proof (induct ls arbitrary: x) case Nil show ?case apply (clarsimp simp:mapM_x_def sequence_x_def) done next case (Cons x ls) show ?case apply (clarsimp simp:mapM_x_Cons dc_def[symmetric]) apply (rule corres_dummy_return_r) apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule dcorres_dummy_empty_slot_pd) apply (clarsimp simp:Cons)+ apply (rule Cons.hyps) apply (clarsimp simp:Cons) apply wp apply (fastforce simp: obj_at_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x) proof (state)
goal (2 subgoals):
 1. \<And>x. \<forall>x\<in>set []. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) [])) (return x)
 2. \<And>a ls x. \<lbrakk>\<And>x. \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x); \<forall>x\<in>set (a # ls). 3584 \<le> unat x \<and> unat x < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (a # ls))) (return x) proof (state)
this:
\<forall>x\<in>set []. 3584 \<le> unat x \<and> unat x < 4096

goal (2 subgoals):
 1. \<And>x. \<forall>x\<in>set []. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) [])) (return x)
 2. \<And>a ls x. \<lbrakk>\<And>x. \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x); \<forall>x\<in>set (a # ls). 3584 \<le> unat x \<and> unat x < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (a # ls))) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) [])) (return x) proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) [])) (return x)

goal (1 subgoal):
 1. \<And>a ls x. \<lbrakk>\<And>x. \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x); \<forall>x\<in>set (a # ls). 3584 \<le> unat x \<and> unat x < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (a # ls))) (return x) proof (state)
goal (1 subgoal):
 1. \<And>a ls x. \<lbrakk>\<And>x. \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x); \<forall>x\<in>set (a # ls). 3584 \<le> unat x \<and> unat x < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (a # ls))) (return x) proof (state)
this:
\<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return ?x)
\<forall>x\<in>set (xa__ # ls). 3584 \<le> unat x \<and> unat x < 4096

goal (1 subgoal):
 1. \<And>a ls x. \<lbrakk>\<And>x. \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096 \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x); \<forall>x\<in>set (a # ls). 3584 \<le> unat x \<and> unat x < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (a # ls))) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (xa__ # ls))) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) w a \<and> valid_idle a) (do y <- PageTableUnmap_D.empty_slot (w, unat xa__);
mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)
od) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>a. typ_at (AArch APageDirectory) w a \<and> valid_idle a) (do y <- PageTableUnmap_D.empty_slot (w, unat xa__);
mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)
od) (return x >>= return) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do y <- PageTableUnmap_D.empty_slot (w, unat xa__);
mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)
od) (return x >>= return) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q4 s s') (?Q'4 s s') (do y <- PageTableUnmap_D.empty_slot (w, unat xa__);
mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)
od) (return x >>= return)
 2. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> ?Q4 s s' sa
 3. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'4 s s' sa proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> dcorres (?r'8 s s') (?P8 s s') (?P'8 s s') (PageTableUnmap_D.empty_slot (w, unat xa__)) (return x)
 2. \<And>s s' rv x. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; ?r'8 s s' rv x\<rbrakk> \<Longrightarrow> dcorres dc (?R8 s s' rv) (?R'8 s s' x) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x)
 3. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s s'\<rbrace> PageTableUnmap_D.empty_slot (w, unat xa__) \<lbrace>?R8 s s'\<rbrace>
 4. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8 s s'\<rbrace> return x \<lbrace>?R'8 s s'\<rbrace>
 5. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> (?P8 s s' and ?Q8 s s') sa
 6. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> (?P'8 s s' and ?Q'8 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> 3584 \<le> unat xa__
 2. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> unat xa__ < 4096
 3. \<And>s s' rv x. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; dc rv x\<rbrakk> \<Longrightarrow> dcorres dc (?R8 s s' rv) (?R'8 s s' x) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x)
 4. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s s'\<rbrace> PageTableUnmap_D.empty_slot (w, unat xa__) \<lbrace>?R8 s s'\<rbrace>
 5. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8 s s'\<rbrace> return x \<lbrace>?R'8 s s'\<rbrace>
 6. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 s s') sa
 7. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch APageDirectory) w and ?Q'8 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s' x. \<lbrakk>typ_at (AArch APageDirectory) w s'; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc (?R8 (transform s') s' ()) (?R'8 (transform s') s' x) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) ls)) (return x)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s s'\<rbrace> PageTableUnmap_D.empty_slot (w, unat xa__) \<lbrace>?R8 s s'\<rbrace>
 3. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8 s s'\<rbrace> return x \<lbrace>?R'8 s s'\<rbrace>
 4. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 s s') sa
 5. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch APageDirectory) w and ?Q'8 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s' x. \<lbrakk>typ_at (AArch APageDirectory) w s'; valid_idle s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ls. 3584 \<le> unat x \<and> unat x < 4096
 2. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s s'\<rbrace> PageTableUnmap_D.empty_slot (w, unat xa__) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8 s s'\<rbrace> return x \<lbrace>\<lambda>a. typ_at (AArch APageDirectory) w and valid_idle\<rbrace>
 4. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 s s') sa
 5. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch APageDirectory) w and ?Q'8 s s') sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s s'\<rbrace> PageTableUnmap_D.empty_slot (w, unat xa__) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8 s s'\<rbrace> return x \<lbrace>\<lambda>a. typ_at (AArch APageDirectory) w and valid_idle\<rbrace>
 3. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 s s') sa
 4. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch APageDirectory) w and ?Q'8 s s') sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8 s s'\<rbrace> return x \<lbrace>\<lambda>a. typ_at (AArch APageDirectory) w and valid_idle\<rbrace>
 2. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) sa
 3. \<And>s s' sa. \<lbrakk>s = transform s'; True; typ_at (AArch APageDirectory) w s' \<and> valid_idle s'; s' = sa\<rbrakk> \<Longrightarrow> (valid_idle and typ_at (AArch APageDirectory) w and ?Q'8 s s') sa proof (prove)
goal:
No subgoals! proof (state)
this:
dcorres dc (\<lambda>_. True) (typ_at (AArch APageDirectory) w and valid_idle) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (xa__ # ls))) (return x)

goal:
No subgoals!