theory Retype_R

lemma copyGlobalMappings_ko_wp_at:
  "\<lbrace>(\<lambda>s. P (ko_wp_at' P' p s)) and K (\<forall>pde_x :: pde. P' (injectKO pde_x) = v)\<rbrace>
     copyGlobalMappings pd
   \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: copyGlobalMappings_def storePDE_def) apply (wp mapM_x_wp' setObject_ko_wp_at) apply simp apply (simp add: objBits_simps archObjSize_def) apply (simp add: pdeBits_def) apply (simp cong: if_cong split del: if_split) apply (wp getObject_inv loadObject_default_inv | simp split del: if_split)+ apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (ko_wp_at' P' p s)) and K (\<forall>pde_x. P' (injectKOS pde_x) = v)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>pde_x. P' (injectKOS pde_x) = v \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= setObject (pd + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>globalPD x xa ko s xb y n. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> updateObject xa ko (pd + (x << pdeBits)) y n s = updateObject_default xa ko (pd + (x << pdeBits)) y n s
 2. \<And>globalPD x xa v'. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> objBits v' = ?n6 globalPD x xa
 3. \<And>globalPD x xa. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> 1 < 2 ^ ?n6 globalPD x xa
 4. \<And>globalPD x. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> getObject (globalPD + (x << pdeBits)) \<lbrace>\<lambda>xa s. obj_at' (\<lambda>x. True) (pd + (x << pdeBits)) s \<longrightarrow> P (ko_wp_at' (if pd + (x << pdeBits) = p then K (P' (injectKOS xa)) else P') p s)\<rbrace>
 5. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 6. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>globalPD x xa v'. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> objBits v' = ?n6 globalPD x xa
 2. \<And>globalPD x xa. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> 1 < 2 ^ ?n6 globalPD x xa
 3. \<And>globalPD x. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> getObject (globalPD + (x << pdeBits)) \<lbrace>\<lambda>xa s. obj_at' (\<lambda>x. True) (pd + (x << pdeBits)) s \<longrightarrow> P (ko_wp_at' (if pd + (x << pdeBits) = p then K (P' (injectKOS xa)) else P') p s)\<rbrace>
 4. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 5. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>globalPD x xa. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> 1 < 2 ^ pdeBits
 2. \<And>globalPD x. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> getObject (globalPD + (x << pdeBits)) \<lbrace>\<lambda>xa s. obj_at' (\<lambda>x. True) (pd + (x << pdeBits)) s \<longrightarrow> P (ko_wp_at' (if pd + (x << pdeBits) = p then K (P' (injectKOS xa)) else P') p s)\<rbrace>
 3. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 4. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>globalPD x. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; x \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> getObject (globalPD + (x << pdeBits)) \<lbrace>\<lambda>xa s. obj_at' (\<lambda>x. True) (pd + (x << pdeBits)) s \<longrightarrow> P (ko_wp_at' (if pd + (x << pdeBits) = p then K (P' (injectKOS xa)) else P') p s)\<rbrace>
 2. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>globalPD x. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; pptrBase >> 20 \<le> x \<and> x \<le> 2 ^ (pdBits - pdeBits) - 1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ko_wp_at' P' p s)\<rbrace> getObject (globalPD + (x << pdeBits)) \<lbrace>\<lambda>xa s. obj_at' (\<lambda>x. True) (pd + (x << pdeBits)) s \<longrightarrow> P (ko_wp_at' (if pd + (x << pdeBits) = p then \<lambda>y. v else P') p s)\<rbrace>
 2. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; pptrBase >> 20 \<le> x \<and> x \<le> 2 ^ (pdBits - pdeBits) - 1; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) (pd + (x << pdeBits)) s \<longrightarrow> P (ko_wp_at' (if pd + (x << pdeBits) = p then \<lambda>y. v else P') p s)
 2. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 3. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s. P (ko_wp_at' P' p s)\<rbrace>
 2. \<And>s. \<lbrakk>\<forall>pde_x. P' (KOArch (KOPDE pde_x)) = v; P (ko_wp_at' P' p s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!