theory ArchRetype_AC

lemma copy_global_mappings_pas_refined:
  "is_aligned pd pd_bits
   \<Longrightarrow> \<lbrace>pas_refined aag and valid_kernel_mappings and valid_arch_state
                        and valid_global_objs and valid_global_refs and pspace_aligned\<rbrace>
       copy_global_mappings pd
       \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: copy_global_mappings_def) apply wp 
    (* Use \<circ> to avoid wp filtering out the global_pd condition here
       TODO: see if we can clean this up *)
     apply (rule_tac Q="\<lambda>rv s. is_aligned global_pd pd_bits \<and>
                              (global_pd = (arm_global_pd \<circ> arch_state) s \<and>
                               valid_kernel_mappings s \<and> valid_arch_state s \<and>
                               valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s)"
                 in hoare_strengthen_post) apply (rule mapM_x_wp[OF _ subset_refl]) apply (rule hoare_seq_ext) apply (unfold o_def) 
    (* Use [1] so wp doesn't filter out the global_pd condition *)
       apply (wp store_pde_pas_refined store_pde_valid_kernel_mappings_map_global)[1] apply (frule subsetD[OF copy_global_mappings_index_subset]) apply (rule hoare_gen_asm[simplified K_def pred_conj_def conj_commute]) apply (simp add: get_pde_def) apply (subst kernel_vsrefs_kernel_mapping_slots[symmetric]) apply wp apply (clarsimp simp: get_pde_def pd_shifting' pd_shifting_dual' triple_shift_fun) apply (subst (asm) obj_at_def, erule exE, erule conjE) apply (rotate_tac -1, drule sym, simp) apply (frule (1) valid_kernel_mappingsD[folded obj_at_def]) apply (clarsimp simp: kernel_mapping_slots_def shiftr_20_less pde_ref_def
                           global_refs_def empty_table_update_from_arm_global_pts) apply fastforce apply (rule gets_wp) apply (simp, blast intro: invs_aligned_pdD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?B1 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B1\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?B1 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B1\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?B1 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>rv s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B1\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>rv s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?B8 global_pd x xa\<rbrace> store_pde (pd + (x << 2)) xa \<lbrace>\<lambda>rv s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 2. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>?B8 global_pd x\<rbrace>
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?B8 global_pd x xa\<rbrace> store_pde (pd + (x << 2)) xa \<lbrace>\<lambda>rv s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 2. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>?B8 global_pd x\<rbrace>
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?B8 global_pd x xa\<rbrace> store_pde (pd + (x << 2)) xa \<lbrace>\<lambda>rv s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 2. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>?B8 global_pd x\<rbrace>
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> (valid_kernel_mappings and valid_arch_state and valid_global_objs and K (VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref xa = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))) s \<and> valid_arch_state s \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (pd + (x << 2) && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := xa))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> valid_global_refs s \<and> (pas_refined aag and K (UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>xb. pde_ref2 xa = Some xb \<longrightarrow> (\<forall>a\<in>snd (snd xb). \<forall>p'\<in>ptr_range (fst xb) (fst (snd xb)). auth_graph_map (pasObjectAbs aag) {(pd + (x << 2) && ~~ mask pd_bits, a, p')} \<subseteq> pasPolicy aag)))) s\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; x \<in> {x. \<exists>y. x = y >> 20}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> (valid_kernel_mappings and valid_arch_state and valid_global_objs and K (VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref xa = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))) s \<and> valid_arch_state s \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (pd + (x << 2) && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := xa))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> valid_global_refs s \<and> (pas_refined aag and K (UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>xb. pde_ref2 xa = Some xb \<longrightarrow> (\<forall>a\<in>snd (snd xb). \<forall>p'\<in>ptr_range (fst xb) (fst (snd xb)). auth_graph_map (pasObjectAbs aag) {(pd + (x << 2) && ~~ mask pd_bits, a, p')} \<subseteq> pasPolicy aag)))) s\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; x \<in> {x. \<exists>y. x = y >> 20}; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. global_pd = arm_global_pd (arch_state x) \<and> valid_kernel_mappings x \<and> valid_arch_state x \<and> valid_global_objs x \<and> valid_global_refs x \<and> pas_refined aag x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> (valid_kernel_mappings and valid_arch_state and valid_global_objs and K (VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<forall>p. pde_ref xa = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))) s \<and> valid_arch_state s \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (pd + (x << 2) && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := xa))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> valid_global_refs s \<and> (pas_refined aag and K (UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>xb. pde_ref2 xa = Some xb \<longrightarrow> (\<forall>a\<in>snd (snd xb). \<forall>p'\<in>ptr_range (fst xb) (fst (snd xb)). auth_graph_map (pasObjectAbs aag) {(pd + (x << 2) && ~~ mask pd_bits, a, p')} \<subseteq> pasPolicy aag)))) s\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1; \<exists>y. x = y >> 20; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. global_pd = arm_global_pd (arch_state x) \<and> valid_kernel_mappings x \<and> valid_arch_state x \<and> valid_global_objs x \<and> valid_global_refs x \<and> pas_refined aag x\<rbrace> do pd <- get_pd (global_pd + (x << 2) && ~~ mask pd_bits);
return (pd (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2)))
od \<lbrace>\<lambda>xa s. global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref xa = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> valid_arch_state s \<and> ((\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (pd + (x << 2) && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := xa))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s)) \<and> valid_global_refs s \<and> pas_refined aag s \<and> (UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xa = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd + (x << 2) && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1; \<exists>y. x = y >> 20; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. global_pd = arm_global_pd (arch_state x) \<and> valid_kernel_mappings x \<and> valid_arch_state x \<and> valid_global_objs x \<and> valid_global_refs x \<and> pas_refined aag x\<rbrace> do pd <- get_pd (global_pd + (x << 2) && ~~ mask pd_bits);
return (pd (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2)))
od \<lbrace>\<lambda>xa s. global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> (\<forall>p. pde_ref xa = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> valid_arch_state s \<and> ((\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (pd + (x << 2) && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := xa))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s)) \<and> valid_global_refs s \<and> pas_refined aag s \<and> (UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 xa = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd + (x << 2) && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x s. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1; \<exists>y. x = y >> 20; is_aligned global_pd pd_bits; global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (global_pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> valid_arch_state s \<and> ((\<forall>pdb. obj_at (empty_table (set (second_level_tables (arch_state s)))) (pd + (x << 2) && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pdb) (pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) := pda (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s)) \<and> valid_global_refs s \<and> pas_refined aag s \<and> (UCAST(32 \<rightarrow> 12) (pd + (x << 2) && mask pd_bits >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 (pda (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2))) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd + (x << 2) && ~~ mask pd_bits, ab, p')} \<subseteq> pasPolicy aag)))
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s y pda. \<lbrakk>is_aligned pd pd_bits; is_aligned (arm_global_pd (arch_state s)) pd_bits; kernel_base >> 20 \<le> y >> 20; y >> 20 \<le> 2 ^ (pd_bits - 2) - 1; valid_kernel_mappings s; valid_arch_state s; valid_global_objs s; valid_global_refs s; pas_refined aag s; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y >> 20) \<in> kernel_mapping_slots \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> ((\<forall>pdb. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s \<and> ako_at (PageDirectory pdb) pd s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (y >> 20) := pda (UCAST(32 \<rightarrow> 12) (y >> 20))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> (UCAST(32 \<rightarrow> 12) (y >> 20) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd, ab, p')} \<subseteq> pasPolicy aag)))
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s y pda ko. \<lbrakk>is_aligned pd pd_bits; is_aligned (arm_global_pd (arch_state s)) pd_bits; kernel_base >> 20 \<le> y >> 20; y >> 20 \<le> 2 ^ (pd_bits - 2) - 1; valid_kernel_mappings s; valid_arch_state s; valid_global_objs s; valid_global_refs s; pas_refined aag s; kheap s (arm_global_pd (arch_state s)) = Some ko; ArchObj (PageDirectory pda) = ko\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y >> 20) \<in> kernel_mapping_slots \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> ((\<forall>pdb. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s \<and> ako_at (PageDirectory pdb) pd s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (y >> 20) := pda (UCAST(32 \<rightarrow> 12) (y >> 20))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> (UCAST(32 \<rightarrow> 12) (y >> 20) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd, ab, p')} \<subseteq> pasPolicy aag)))
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s y pda ko. \<lbrakk>is_aligned pd pd_bits; is_aligned (arm_global_pd (arch_state s)) pd_bits; kernel_base >> 20 \<le> y >> 20; y >> 20 \<le> 2 ^ (pd_bits - 2) - 1; valid_kernel_mappings s; valid_arch_state s; valid_global_objs s; valid_global_refs s; pas_refined aag s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pda)); ko = ArchObj (PageDirectory pda)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y >> 20) \<in> kernel_mapping_slots \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> ((\<forall>pdb. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s \<and> ako_at (PageDirectory pdb) pd s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (y >> 20) := pda (UCAST(32 \<rightarrow> 12) (y >> 20))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> (UCAST(32 \<rightarrow> 12) (y >> 20) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd, ab, p')} \<subseteq> pasPolicy aag)))
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s y pda ko. \<lbrakk>is_aligned pd pd_bits; is_aligned (arm_global_pd (arch_state s)) pd_bits; kernel_base >> 20 \<le> y >> 20; y >> 20 \<le> 2 ^ (pd_bits - 2) - 1; valid_kernel_mappings s; valid_arch_state s; valid_global_objs s; valid_global_refs s; pas_refined aag s; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pda)); ko = ArchObj (PageDirectory pda); \<forall>x r. pde_ref (pda x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y >> 20) \<in> kernel_mapping_slots \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> ((\<forall>pdb. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s \<and> ako_at (PageDirectory pdb) pd s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pdb(UCAST(32 \<rightarrow> 12) (y >> 20) := pda (UCAST(32 \<rightarrow> 12) (y >> 20))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> (UCAST(32 \<rightarrow> 12) (y >> 20) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (\<forall>a aa b. pde_ref2 (pda (UCAST(32 \<rightarrow> 12) (y >> 20))) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p'\<in>ptr_range a aa. auth_graph_map (pasObjectAbs aag) {(pd, ab, p')} \<subseteq> pasPolicy aag)))
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (\<lambda>x. arm_global_pd (arch_state x)) \<lbrace>\<lambda>global_pd s. is_aligned global_pd pd_bits \<and> global_pd = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned pd pd_bits; (pas_refined aag and valid_kernel_mappings and valid_arch_state and valid_global_objs and valid_global_refs and pspace_aligned) s\<rbrakk> \<Longrightarrow> is_aligned (arm_global_pd (arch_state s)) pd_bits \<and> arm_global_pd (arch_state s) = arm_global_pd (arch_state s) \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s proof (prove)
goal:
No subgoals!