theory ArchVSpaceEntries_AI

lemma mapM_x_copy_pde_updates:
  "\<lbrakk> \<forall>x \<in> set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits;
               is_aligned p' pd_bits \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<not> page_directory_at p s \<longrightarrow> Q s) \<and> (\<not> page_directory_at p' s \<longrightarrow> Q s) \<and>
        (\<forall>pd pd'. ko_at (ArchObj (PageDirectory pd)) p s
                \<and> ko_at (ArchObj (PageDirectory pd')) p' s
           \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p' := Some (ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x.
         ucast (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))) \<rparr>))\<rbrace>
     mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs
   \<lbrace>\<lambda>_. Q\<rbrace>" apply (induct xs) apply (simp add: mapM_x_Nil) apply wp apply (clarsimp simp: obj_at_def fun_upd_idem dest!: a_type_pdD) apply (simp add: mapM_x_Cons) apply wp apply (thin_tac "valid P f Q" for P f Q) apply (simp add: store_pde_def set_pd_def set_object_def
              cong: bind_cong split del: if_split) apply (wp get_object_wp get_pde_wp) apply (clarsimp simp: obj_at_def a_type_simps mask_out_add_aligned[symmetric]
             split del: if_split) apply (simp add: a_type_simps, safe) apply (erule rsubst[where P=Q]) apply (rule abstract_state.fold_congs[OF refl refl]) apply (rule ext, clarsimp) apply (rule ext, simp) apply (erule rsubst[where P=Q]) apply (rule abstract_state.fold_congs[OF refl refl]) apply (rule ext, clarsimp) apply (rule ext, simp add: mask_add_aligned) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set [] then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) [] \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory pd'))\<rparr>))\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned p pd_bits; is_aligned p' pd_bits; (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory pd'))\<rparr>))\<rbrakk> \<Longrightarrow> Q s
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> do y <- get_pde (p + f a) >>= store_pde (p' + f a);
mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q39 a xs\<rbrace> get_pde (p + f a) >>= store_pde (p' + f a) \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits; (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrakk> \<Longrightarrow> ?Q39 a xs s proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q39 a xs\<rbrace> get_pde (p + f a) >>= store_pde (p' + f a) \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits; (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrakk> \<Longrightarrow> ?Q39 a xs s proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q39 a xs\<rbrace> do v <- get_pde (p + f a);
va <- get_pd (p' + f a && ~~ mask pd_bits);
vb <- get_object (p' + f a && ~~ mask pd_bits);
b <- assert (a_type vb = a_type (ArchObj (PageDirectory (va(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := v)))));
vb <- get;
put (vb\<lparr>kheap := (kheap vb)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (va(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := v))))\<rparr>)
od \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits; (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrakk> \<Longrightarrow> ?Q39 a xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = 0 \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0); is_aligned p pd_bits; is_aligned p' pd_bits; (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<not> typ_at (AArch APageDirectory) p' s \<longrightarrow> Q s) \<and> (\<forall>pd pd'. ako_at (PageDirectory pd) p s \<and> ako_at (PageDirectory pd') p' s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrakk> \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p + f a && ~~ mask pd_bits) s \<longrightarrow> (\<forall>pda. ako_at (PageDirectory pda) (p' + f a && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p' + f a && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)))))) \<longrightarrow> (\<not> typ_at (AArch APageDirectory) p (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>)) \<and> (\<not> typ_at (AArch APageDirectory) p' (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>)) \<and> (\<forall>pdb pd'. ako_at (PageDirectory pdb) p (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>) \<and> ako_at (PageDirectory pd') p' (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)))))), kheap := (kheap (s\<lparr>kheap := (kheap s)(p' + f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) := pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2))))))\<rparr>))(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pdb y else pd' y)))\<rparr>)))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> ((\<forall>ko. (if p = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda b))) else Some (ArchObj (PageDirectory pd))) = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q (s\<lparr>kheap := \<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b\<rparr>)) \<and> (\<forall>pdb. (if p = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda b))) else Some (ArchObj (PageDirectory pd))) = Some (ArchObj (PageDirectory pdb)) \<longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pdb y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p' = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p' + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p' pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p' = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p = p'\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda y)))\<rparr>)
 2. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p' = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p' + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p' pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; kheap s p' = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p = p'\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr> = s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda y)))\<rparr>
 2. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a xs s pd pda v. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p' = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p' + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p' pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; kheap s p' = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p = p'; kheap s = v\<rbrakk> \<Longrightarrow> (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y))) = (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda y)))
 2. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>a xs s pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p' = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p' + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; kheap s p' = Some (ArchObj (PageDirectory pda)); p = p'\<rbrakk> \<Longrightarrow> pda = (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pda (UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2)) else pda y)
 2. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr>); kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y)))\<rparr> = s\<lparr>kheap := (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y)))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd pda v. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'; kheap s = v\<rbrakk> \<Longrightarrow> (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y))) = (\<lambda>b. if b = p' then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda b))) else kheap s b)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd pda. \<lbrakk>\<lbrace>\<lambda>s. ((\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> ((\<forall>ko. kheap s p' = Some ko \<longrightarrow> a_type ko \<noteq> AArch APageDirectory) \<longrightarrow> Q s) \<and> (\<forall>pd pd'. kheap s p = Some (ArchObj (PageDirectory pd)) \<and> kheap s p' = Some (ArchObj (PageDirectory pd')) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p' \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \<lbrace>\<lambda>_. Q\<rbrace>; is_aligned p pd_bits; is_aligned p' pd_bits; f a && ~~ mask pd_bits = 0; \<forall>x\<in>set xs. f x && ~~ mask pd_bits = 0; kheap s p = Some (ArchObj (PageDirectory pd)); kheap s p' = Some (ArchObj (PageDirectory pda)); p \<noteq> p'\<rbrakk> \<Longrightarrow> (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else pda y) = (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pd y else if y = UCAST(32 \<rightarrow> 12) (p' + f a && mask pd_bits >> 2) then pd (UCAST(32 \<rightarrow> 12) (p + f a && mask pd_bits >> 2)) else pda y) proof (prove)
goal:
No subgoals!