theory Retype_R

lemma copyGlobalMappings_corres:
  "corres dc (valid_arch_state and valid_etcbs and pspace_aligned and page_directory_at pd)
             (valid_arch_state' and page_directory_at' pd)
          (copy_global_mappings pd)
          (copyGlobalMappings pd)" apply (simp add: copy_global_mappings_def
                   copyGlobalMappings_def
                   objBits_simps archObjSize_def
                   pd_bits_def pdBits_def mapM_x_mapM) apply (rule corres_guard_imp) apply (rule corres_split_eqr) apply (rule corres_trivial, clarsimp simp: state_relation_def arch_state_relation_def) apply (rule_tac F ="is_aligned pd 6 \<and> is_aligned global_pd 6" in corres_gen_asm) apply (simp add: liftM_def[symmetric]) apply (rule_tac S="(=)" and r'=dc
                  and Q="\<lambda>xs s. \<forall>x \<in> set xs. pde_at (global_pd + (x << 2)) s
                                             \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and>
                                             valid_etcbs s"
                  and Q'="\<lambda>xs s. \<forall>x \<in> set xs. pde_at' (global_pd + (x << 2)) s
                                             \<and> pde_at' (pd + (x << 2)) s"
                         in corres_mapM_list_all2, (simp add: pdeBits_def)+) apply (rule corres_guard_imp, rule corres_split) apply (rule_tac getObject_PDE_corres[OF refl]) apply (rule storePDE_corres[OF _ refl]) apply clarsimp apply (drule(1) pde_relation_aligned_eq) apply fastforce apply (wp hoare_vcg_const_Ball_lift | simp)+ apply (simp add: kernel_base_def ARM.pptrBase_def pptrBase_def list_all2_refl pageBits_def) apply wp+ apply (clarsimp simp: valid_arch_state_def) apply (auto elim: page_directory_pde_atI is_aligned_weaken[OF pd_aligned])[1] apply (clarsimp simp: valid_arch_state'_def) apply (auto simp: le_less_trans elim!: page_directory_pde_atI'[simplified pageBits_def, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) (valid_arch_state' and page_directory_at' pd) (copy_global_mappings pd) (copyGlobalMappings pd) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) (valid_arch_state' and page_directory_at' pd) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
x <- mapM (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ pageBits - 1];
return ()
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
x <- mapM (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 0xFFF];
return ()
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q1 ?Q'1 (do global_pd <- gets (arm_global_pd \<circ> arch_state);
x <- mapM (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ pageBits - 1];
return ()
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
x <- mapM (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 0xFFF];
return ()
od)
 2. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ?Q1 s
 3. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P5 ?P'5 (gets (arm_global_pd \<circ> arch_state)) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<And>global_pd. corres dc (?R5 global_pd) (?R'5 global_pd) (do x <- mapM (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ pageBits - 1];
return ()
od) (do x <- mapM (\<lambda>index. getObject (global_pd + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 0xFFF];
return ()
od)
 3. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?R5\<rbrace>
 4. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'5\<rbrace>
 5. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd. corres dc (?R5 global_pd) (?R'5 global_pd) (do x <- mapM (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ pageBits - 1];
return ()
od) (do x <- mapM (\<lambda>index. getObject (global_pd + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 0xFFF];
return ()
od)
 2. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?R5\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'5\<rbrace>
 4. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> corres dc (?P12 global_pd) (?R'5 global_pd) (do x <- mapM (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ pageBits - 1];
return ()
od) (do x <- mapM (\<lambda>index. getObject (global_pd + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 0xFFF];
return ()
od)
 2. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. ?P12 global_pd and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'5\<rbrace>
 4. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> corres dc (?P12 global_pd) (?R'5 global_pd) (mapM (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ pageBits - 1]) (mapM (\<lambda>index. getObject (global_pd + (index << pdeBits)) >>= storePDE (pd + (index << pdeBits))) [pptrBase >> 20 .e. 0xFFF])
 2. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. ?P12 global_pd and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'5\<rbrace>
 4. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)) (\<lambda>s. pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)) (get_pde (global_pd + (y << 2)) >>= store_pde (pd + (y << 2))) (getObject (global_pd + (y << 2)) >>= storePDE (pd + (y << 2)))
 2. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 3. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 4. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 5. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 7. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (13 subgoals):
 1. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> corres (?r'19 global_pd x xs y ys) (?P19 global_pd x xs y ys) (?P'19 global_pd x xs y ys) (get_pde (global_pd + (y << 2))) (getObject (global_pd + (y << 2)))
 2. \<And>global_pd x xs y ys rv rv'. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; ?r'19 global_pd x xs y ys rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R19 global_pd x xs y ys rv) (?R'19 global_pd x xs y ys rv') (store_pde (pd + (y << 2)) rv) (storePDE (pd + (y << 2)) rv')
 3. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 global_pd x xs y ys\<rbrace> get_pde (global_pd + (y << 2)) \<lbrace>?R19 global_pd x xs y ys\<rbrace>
 4. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 global_pd x xs y ys\<rbrace> getObject (global_pd + (y << 2)) \<lbrace>?R'19 global_pd x xs y ys\<rbrace>
 5. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (?P19 global_pd x xs y ys and ?Q19 global_pd x xs y ys) s
 6. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)\<rbrakk> \<Longrightarrow> (?P'19 global_pd x xs y ys and ?Q'19 global_pd x xs y ys) s
 7. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 8. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 9. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 10. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>global_pd x xs y ys rv rv'. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_relation_aligned (global_pd + (y << 2) >> 2) rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R19 global_pd x xs y ys rv) (?R'19 global_pd x xs y ys rv') (store_pde (pd + (y << 2)) rv) (storePDE (pd + (y << 2)) rv')
 2. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 global_pd x xs y ys\<rbrace> get_pde (global_pd + (y << 2)) \<lbrace>?R19 global_pd x xs y ys\<rbrace>
 3. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 global_pd x xs y ys\<rbrace> getObject (global_pd + (y << 2)) \<lbrace>?R'19 global_pd x xs y ys\<rbrace>
 4. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (pde_at (global_pd + (y << 2)) and ?Q19 global_pd x xs y ys) s
 5. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)\<rbrakk> \<Longrightarrow> (pde_at' (global_pd + (y << 2)) and ?Q'19 global_pd x xs y ys) s
 6. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 7. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 8. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 9. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 10. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>global_pd x xs y ys rv rv'. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_relation_aligned (global_pd + (y << 2) >> 2) rv rv'\<rbrakk> \<Longrightarrow> pde_relation_aligned (pd + (y << 2) >> 2) rv rv'
 2. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 global_pd x xs y ys\<rbrace> get_pde (global_pd + (y << 2)) \<lbrace>\<lambda>rv. pde_at (pd + (y << 2)) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 global_pd x xs y ys\<rbrace> getObject (global_pd + (y << 2)) \<lbrace>\<lambda>rv'. pde_at' (pd + (y << 2))\<rbrace>
 4. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (pde_at (global_pd + (y << 2)) and ?Q19 global_pd x xs y ys) s
 5. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)\<rbrakk> \<Longrightarrow> (pde_at' (global_pd + (y << 2)) and ?Q'19 global_pd x xs y ys) s
 6. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 7. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 8. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 9. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 10. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>global_pd xs y ys rv rv'. \<lbrakk>list_all2 (=) xs ys; pde_relation_aligned (global_pd + (y << 2) >> 2) rv rv'; is_aligned pd 6; is_aligned global_pd 6\<rbrakk> \<Longrightarrow> pde_relation_aligned (pd + (y << 2) >> 2) rv rv'
 2. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 global_pd x xs y ys\<rbrace> get_pde (global_pd + (y << 2)) \<lbrace>\<lambda>rv. pde_at (pd + (y << 2)) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 global_pd x xs y ys\<rbrace> getObject (global_pd + (y << 2)) \<lbrace>\<lambda>rv'. pde_at' (pd + (y << 2))\<rbrace>
 4. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (pde_at (global_pd + (y << 2)) and ?Q19 global_pd x xs y ys) s
 5. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)\<rbrakk> \<Longrightarrow> (pde_at' (global_pd + (y << 2)) and ?Q'19 global_pd x xs y ys) s
 6. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 7. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 8. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 9. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 10. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>global_pd xs y ys rv rv'. \<lbrakk>list_all2 (=) xs ys; pde_relation_aligned (global_pd + (y << 2) >> 2) rv rv'; is_aligned global_pd 6; pde_relation_aligned (pd + ?x36 global_pd xs y ys rv rv' >> 2) (?xa36 global_pd xs y ys rv rv') (?ya36 global_pd xs y ys rv rv') = pde_relation_aligned (global_pd + ?x36 global_pd xs y ys rv rv' >> 2) (?xa36 global_pd xs y ys rv rv') (?ya36 global_pd xs y ys rv rv')\<rbrakk> \<Longrightarrow> pde_relation_aligned (pd + (y << 2) >> 2) rv rv'
 2. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 global_pd x xs y ys\<rbrace> get_pde (global_pd + (y << 2)) \<lbrace>\<lambda>rv. pde_at (pd + (y << 2)) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 global_pd x xs y ys\<rbrace> getObject (global_pd + (y << 2)) \<lbrace>\<lambda>rv'. pde_at' (pd + (y << 2))\<rbrace>
 4. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (pde_at (global_pd + (y << 2)) and ?Q19 global_pd x xs y ys) s
 5. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)\<rbrakk> \<Longrightarrow> (pde_at' (global_pd + (y << 2)) and ?Q'19 global_pd x xs y ys) s
 6. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 7. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 8. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 9. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 10. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 global_pd x xs y ys\<rbrace> get_pde (global_pd + (y << 2)) \<lbrace>\<lambda>rv. pde_at (pd + (y << 2)) and pspace_aligned and valid_etcbs\<rbrace>
 2. \<And>global_pd x xs y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 global_pd x xs y ys\<rbrace> getObject (global_pd + (y << 2)) \<lbrace>\<lambda>rv'. pde_at' (pd + (y << 2))\<rbrace>
 3. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at (global_pd + (y << 2)) s \<and> pde_at (pd + (y << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (pde_at (global_pd + (y << 2)) and ?Q19 global_pd x xs y ys) s
 4. \<And>global_pd x xs y ys s. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; list_all2 (=) xs ys; pde_at' (global_pd + (y << 2)) s \<and> pde_at' (pd + (y << 2)) s \<and> (\<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)\<rbrakk> \<Longrightarrow> (pde_at' (global_pd + (y << 2)) and ?Q'19 global_pd x xs y ys) s
 5. \<And>global_pd x xs y. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (x # xs) [kernel_base >> 20 .e. 2 ^ pageBits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (x # xs). pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 6. \<And>global_pd x y ys. \<lbrakk>is_aligned pd 6 \<and> is_aligned global_pd 6; x = y; suffix (y # ys) [pptrBase >> 20 .e. 0xFFF]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set (y # ys). pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace> getObject (global_pd + (y << pdeBits)) >>= storePDE (pd + (y << pdeBits)) \<lbrace>\<lambda>r s. \<forall>x\<in>set ys. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 7. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 8. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 9. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 10. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>global_pd. is_aligned pd 6 \<and> is_aligned global_pd 6 \<Longrightarrow> list_all2 (=) [kernel_base >> 20 .e. 2 ^ pageBits - 1] [pptrBase >> 20 .e. 0xFFF]
 2. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 4. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q5\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. (\<lambda>s. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at (global_pd + (x << 2)) s \<and> pde_at (pd + (x << 2)) s \<and> pspace_aligned s \<and> valid_etcbs s) and (\<lambda>s. is_aligned pd 6 \<and> is_aligned global_pd 6)\<rbrace>
 2. \<lbrace>?Q'5\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' (global_pd + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s\<rbrace>
 3. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 4. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_arch_state and valid_etcbs and pspace_aligned and typ_at (AArch APageDirectory) pd) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>sa. \<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ pageBits - 1]. pde_at ((arm_global_pd \<circ> arch_state) s + (x << 2)) sa \<and> pde_at (pd + (x << 2)) sa \<and> pspace_aligned sa \<and> valid_etcbs sa) and (\<lambda>sa. is_aligned pd 6 \<and> is_aligned ((arm_global_pd \<circ> arch_state) s) 6)) s)) s
 2. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' ((armKSGlobalPD \<circ> ksArchState) s + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); valid_etcbs s; pspace_aligned s; typ_at (AArch APageDirectory) pd s\<rbrakk> \<Longrightarrow> (\<forall>x. kernel_base >> 20 \<le> x \<and> x < 2 ^ pageBits \<longrightarrow> pde_at (arm_global_pd (arch_state s) + (x << 2)) s \<and> pde_at (pd + (x << 2)) s) \<and> is_aligned pd 6 \<and> is_aligned (arm_global_pd (arch_state s)) 6
 2. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' ((armKSGlobalPD \<circ> ksArchState) s + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_state' and page_directory_at' pd) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<forall>x\<in>set [pptrBase >> 20 .e. 0xFFF]. pde_at' ((armKSGlobalPD \<circ> ksArchState) s + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); page_directory_at' pd s; pptrBase >> 20 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> pde_at' (armKSGlobalPD (ksArchState s) + (x << 2)) s \<and> pde_at' (pd + (x << 2)) s proof (prove)
goal:
No subgoals!