theory ArchRetype_AI

lemma copy_global_invs_mappings_restricted:
  "\<lbrace>(\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (insert pd S) s)
          and (\<lambda>s. insert pd S \<inter> global_refs s = {})
          and K (is_aligned pd pd_bits)\<rbrace>
     copy_global_mappings pd
   \<lbrace>\<lambda>rv. all_invs_but_equal_kernel_mappings_restricted S\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: valid_pspace_def pred_conj_def) apply (rule hoare_conjI, wp copy_global_equal_kernel_mappings_restricted) apply (clarsimp simp: global_refs_def) apply (rule hoare_post_add, rule hoare_vcg_conj_lift, rule hoare_TrueI) apply (simp add: copy_global_mappings_def valid_pspace_def) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_strengthen_post) apply (rule mapM_x_wp[where S="{x. kernel_base >> 20 \<le> x
                                       \<and> x < 2 ^ (pd_bits - 2)}"]) apply simp_all apply (rule hoare_pre) apply (wp valid_irq_node_typ valid_irq_handlers_lift
              store_pde_map_global_valid_arch_caps
              store_pde_map_global_valid_vspace_objs
              store_pde_valid_kernel_mappings_map_global
              get_pde_wp) apply (clarsimp simp: valid_global_objs_def) apply (frule(1) invs_aligned_pdD) apply (frule shiftl_less_t2n) apply (simp add: pd_bits_def pageBits_def) apply (clarsimp simp: is_aligned_add_helper) apply (cut_tac x=x and n=2 in shiftl_shiftr_id) apply (simp add: word_bits_def) apply (erule order_less_le_trans) apply (simp add: word_bits_def pd_bits_def pageBits_def) apply (rule conjI) apply (simp add: valid_objs_def dom_def obj_at_def valid_obj_def) apply (drule spec, erule impE, fastforce, clarsimp) apply (clarsimp simp: obj_at_def empty_table_def kernel_vsrefs_def second_level_tables_def) apply clarsimp apply (erule word_leq_minus_one_le[rotated]) apply (simp add: pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports and (\<lambda>s. insert pd S \<inter> global_refs s = {}) and K (is_aligned pd pd_bits)\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports and (\<lambda>s. insert pd S \<inter> global_refs s = {})\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>x. equal_kernel_mappings (x\<lparr>kheap := kheap x |` (- insert pd S)\<rparr>) \<and> valid_objs x \<and> pspace_aligned x \<and> pspace_distinct x \<and> if_live_then_nonz_cap x \<and> zombies_final x \<and> sym_refs (state_refs_of x) \<and> sym_refs (state_hyp_refs_of x) \<and> valid_mdb x \<and> valid_idle x \<and> only_idle x \<and> if_unsafe_then_cap x \<and> valid_reply_caps x \<and> valid_reply_masters x \<and> valid_global_refs x \<and> valid_arch_state x \<and> valid_irq_node x \<and> valid_irq_handlers x \<and> valid_vspace_objs x \<and> valid_irq_states x \<and> valid_global_objs x \<and> valid_arch_caps x \<and> valid_kernel_mappings x \<and> valid_asid_map x \<and> valid_global_vspace_mappings x \<and> pspace_in_kernel_window x \<and> cap_refs_in_kernel_window x \<and> pspace_respects_device_region x \<and> cap_refs_respects_device_region x \<and> cur_tcb x \<and> valid_ioc x \<and> valid_machine_state x \<and> pd \<notin> global_refs x \<and> S \<inter> global_refs x = {}\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv x. equal_kernel_mappings (x\<lparr>kheap := kheap x |` (- S)\<rparr>) \<and> valid_objs x \<and> pspace_aligned x \<and> pspace_distinct x \<and> if_live_then_nonz_cap x \<and> zombies_final x \<and> sym_refs (state_refs_of x) \<and> sym_refs (state_hyp_refs_of x) \<and> valid_mdb x \<and> valid_idle x \<and> only_idle x \<and> if_unsafe_then_cap x \<and> valid_reply_caps x \<and> valid_reply_masters x \<and> valid_global_refs x \<and> valid_arch_state x \<and> valid_irq_node x \<and> valid_irq_handlers x \<and> valid_vspace_objs x \<and> valid_irq_states x \<and> valid_global_objs x \<and> valid_arch_caps x \<and> valid_kernel_mappings x \<and> valid_asid_map x \<and> valid_global_vspace_mappings x \<and> pspace_in_kernel_window x \<and> cap_refs_in_kernel_window x \<and> pspace_respects_device_region x \<and> cap_refs_respects_device_region x \<and> cur_tcb x \<and> valid_ioc x \<and> valid_machine_state x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned pd pd_bits; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<notin> insert pd S \<and> pspace_aligned s \<and> valid_arch_state s
 2. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>x. equal_kernel_mappings (x\<lparr>kheap := kheap x |` (- insert pd S)\<rparr>) \<and> valid_objs x \<and> pspace_aligned x \<and> pspace_distinct x \<and> if_live_then_nonz_cap x \<and> zombies_final x \<and> sym_refs (state_refs_of x) \<and> sym_refs (state_hyp_refs_of x) \<and> valid_mdb x \<and> valid_idle x \<and> only_idle x \<and> if_unsafe_then_cap x \<and> valid_reply_caps x \<and> valid_reply_masters x \<and> valid_global_refs x \<and> valid_arch_state x \<and> valid_irq_node x \<and> valid_irq_handlers x \<and> valid_vspace_objs x \<and> valid_irq_states x \<and> valid_global_objs x \<and> valid_arch_caps x \<and> valid_kernel_mappings x \<and> valid_asid_map x \<and> valid_global_vspace_mappings x \<and> pspace_in_kernel_window x \<and> cap_refs_in_kernel_window x \<and> pspace_respects_device_region x \<and> cap_refs_respects_device_region x \<and> cur_tcb x \<and> valid_ioc x \<and> valid_machine_state x \<and> pd \<notin> global_refs x \<and> S \<inter> global_refs x = {}\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>r s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>x. equal_kernel_mappings (x\<lparr>kheap := kheap x |` (- insert pd S)\<rparr>) \<and> valid_objs x \<and> pspace_aligned x \<and> pspace_distinct x \<and> if_live_then_nonz_cap x \<and> zombies_final x \<and> sym_refs (state_refs_of x) \<and> sym_refs (state_hyp_refs_of x) \<and> valid_mdb x \<and> valid_idle x \<and> only_idle x \<and> if_unsafe_then_cap x \<and> valid_reply_caps x \<and> valid_reply_masters x \<and> valid_global_refs x \<and> valid_arch_state x \<and> valid_irq_node x \<and> valid_irq_handlers x \<and> valid_vspace_objs x \<and> valid_irq_states x \<and> valid_global_objs x \<and> valid_arch_caps x \<and> valid_kernel_mappings x \<and> valid_asid_map x \<and> valid_global_vspace_mappings x \<and> pspace_in_kernel_window x \<and> cap_refs_in_kernel_window x \<and> pspace_respects_device_region x \<and> cap_refs_respects_device_region x \<and> cur_tcb x \<and> valid_ioc x \<and> valid_machine_state x \<and> pd \<notin> global_refs x \<and> S \<inter> global_refs x = {}\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>r s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}\<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>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = 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. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = 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>?Q95 global_pd\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ?Q95 global_pd rv s\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s proof (prove)
goal (3 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; x \<in> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>rv. (\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace>
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)}
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s proof (prove)
goal (2 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. arm_global_pd (arch_state s) = global_pd)\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>rv. (\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. arm_global_pd (arch_state s) = global_pd)\<rbrace>
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (3 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (pd + (x << 2)) \<lbrace>\<lambda>rv. (\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. arm_global_pd (arch_state s) = global_pd)\<rbrace>
 2. \<And>global_pd x s. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2); ((\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. arm_global_pd (arch_state s) = global_pd)) s\<rbrakk> \<Longrightarrow> ?Q101 global_pd x s
 3. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>global_pd x s. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2); ((\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_irq_states s \<and> valid_global_objs s \<and> valid_arch_caps s \<and> valid_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) and (\<lambda>s. arm_global_pd (arch_state s) = global_pd)) s\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (global_pd + (x << 2) && ~~ mask pd_bits) s \<longrightarrow> ((\<lambda>s. wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2)))) and valid_objs) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> (valid_vspace_objs and valid_arch_state and valid_global_objs and K (VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)) s \<and> valid_irq_states s \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<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>slot. cte_wp_at (\<lambda>cap. pd + (x << 2) && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> (valid_arch_caps and valid_objs and valid_vspace_objs and valid_arch_state and valid_global_objs and K (valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (global_pd + (x << 2) && mask pd_bits >> 2)))) and K (VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs) and (\<lambda>s. \<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)))) 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 (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)))) s \<and> valid_asid_map s \<and> (valid_global_objs and valid_global_vspace_mappings and (\<lambda>s. pd + (x << 2) && ~~ mask pd_bits \<notin> global_refs s)) s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> valid_ioc s \<and> valid_machine_state s \<and> (pd \<notin> global_refs s \<and> S \<inter> global_refs s = {}) \<and> arm_global_pd (arch_state s) = global_pd
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (arm_global_pd (arch_state s) + (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_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> pd + (x << 2) && ~~ mask pd_bits \<notin> global_refs s
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s; is_aligned (arm_global_pd (arch_state s)) pd_bits\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (arm_global_pd (arch_state s) + (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_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> pd + (x << 2) && ~~ mask pd_bits \<notin> global_refs s
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s; is_aligned (arm_global_pd (arch_state s)) pd_bits\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (arm_global_pd (arch_state s) + (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_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> pd + (x << 2) && ~~ mask pd_bits \<notin> global_refs s
 3. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s) + (x << 2) && ~~ mask pd_bits) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (arm_global_pd (arch_state s) + (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_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (pd + (x << 2) && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (arm_global_pd (arch_state s) + (x << 2) && mask pd_bits >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> pd + (x << 2) && ~~ mask pd_bits \<notin> global_refs s
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (4 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 2)
 3. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 4. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 2)
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 3. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits\<rbrakk> \<Longrightarrow> 2 ^ (pd_bits - 2) \<le> 2 ^ (LENGTH(32) - 2)
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 3. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2)))
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 3. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (3 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)); pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pda)); \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pda)); is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> wellformed_pde (pda (UCAST(32 \<rightarrow> 12) x))
 2. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 3. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x s pda. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x < 2 ^ (pd_bits - 2); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_irq_states s; valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); valid_arch_caps s; valid_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_ioc s; valid_machine_state s; pd \<notin> global_refs s; S \<inter> global_refs s = {}; ako_at (PageDirectory pda) (arm_global_pd (arch_state s)) s; is_aligned (arm_global_pd (arch_state s)) pd_bits; x << 2 < 2 ^ pd_bits; x << 2 >> 2 = x\<rbrakk> \<Longrightarrow> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<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) (x << 2 >> 2) := pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. pd \<in> obj_refs cap) (a, b) s)) \<and> valid_pde_mappings (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s))) \<and> VSRef (x << 2 >> 2) (Some APageDirectory) \<in> kernel_vsrefs \<and> (\<forall>p. pde_ref (pda (UCAST(32 \<rightarrow> 12) (x << 2 >> 2))) = Some p \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))
 2. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> {x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1} \<subseteq> {x. kernel_base >> 20 \<le> x \<and> x < 2 ^ (pd_bits - 2)} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (pd_bits - 2) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned pd pd_bits; kernel_base >> 20 \<le> x\<rbrakk> \<Longrightarrow> 2 ^ (pd_bits - 2) \<noteq> 0 proof (prove)
goal:
No subgoals!