theory CNode_DR

lemma dcorres_clear_object_caps_pt:
  "dcorres dc \<top> (invs and  cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageTableCap w option))) (a, b))
    (clear_object_caps w)
    (mapM_x (swp store_pte ARM_A.pte.InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])" apply (clarsimp simp: clear_object_caps_def gets_def) apply (rule dcorres_absorb_get_l) apply (subgoal_tac "\<exists>ptx. (ko_at (ArchObj (arch_kernel_obj.PageTable ptx)) w) s'") apply clarsimp apply (subst upto_enum_step_subtract[where x = w]) apply (clarsimp simp:invs_def valid_state_def valid_pspace_def) apply (drule cte_wp_valid_cap,simp) apply (clarsimp simp:valid_cap_def cap_aligned_def) apply (rule is_aligned_no_overflow) apply (simp add:pt_bits_def pageBits_def word_bits_def)+ apply (rule corres_guard_imp) apply (rule_tac x = "(map (\<lambda>x. (w,unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])" in select_pick_corres) apply (rule_tac S = "{(x,y). x = (y && ~~ mask pt_bits,unat (y && mask pt_bits >> 2))}"  in corres_mapM_x) apply clarsimp apply (rule dcorres_empty_pte_slot,simp) apply (rule hoare_pre) apply (wp valid_idle_store_pte store_pte_ct |clarsimp simp:cur_tcb_def | wps store_pte_ct )+ apply (simp add:swp_def) apply (simp add:pt_bits_def pageBits_def word_bits_def)+ apply clarsimp apply (subst (asm) zip_map_eqv) apply (clarsimp) apply (drule cte_wp_valid_cap) apply (simp add:invs_def valid_state_def valid_pspace_def) apply (intro conjI) apply (simp add:valid_cap_def cap_aligned_def) apply (rule conjunct2[OF is_aligned_add_helper,symmetric]) apply (clarsimp simp:valid_cap_def cap_aligned_def) apply (clarsimp simp:upto_enum_step_def image_def) apply (rule div_lt_mult,simp) apply (unat_arith,simp) apply (rule_tac f="\<lambda>x. x >>2" in arg_cong) apply (rule conjunct1[OF is_aligned_add_helper,symmetric]) apply (clarsimp simp:valid_cap_def cap_aligned_def) apply (clarsimp simp:upto_enum_step_def image_def) apply (rule div_lt_mult,simp) apply (unat_arith,simp) apply (simp | rule conjI)+ apply (rule set_eqI) apply (clarsimp simp:image_def) apply (clarsimp simp: transform_def opt_cap_def slots_of_def valid_state_def
                           valid_pspace_def transform_objects_def restrict_map_def map_add_def
                           obj_at_def invs_def) apply (drule(1) arch_obj_not_idle) apply (case_tac "aa = idle_thread s'", simp add: not_idle_thread_def, simp) apply (rule iffI) apply (clarsimp simp: upto_enum_step_def not_idle_thread_def object_slots_def
                            transform_page_table_contents_def unat_map_def) apply (rule unat_less_helper) apply (subst mult.commute) apply (simp add:shiftl_t2n[where n= 2,simplified,symmetric]) apply (simp add:shiftl_shiftr1 word_size) apply (subst iffD2[OF mask_eq_iff_w2p]) apply (simp add:word_size pt_bits_def pageBits_def)+ apply unat_arith apply (simp add:word_size pt_bits_def pageBits_def)+ apply unat_arith apply (clarsimp simp: not_idle_thread_def object_slots_def transform_page_table_contents_def unat_map_def
                    split: if_splits) apply (rule_tac x = "(of_nat ba) << 2" in bexI) apply (simp add: shiftl_shiftr1 word_size) apply (subst iffD2[OF mask_eq_iff_w2p],simp add:word_size) apply (rule of_nat_power) apply (simp add:word_size unat_of_nat)+ apply (clarsimp simp:upto_enum_step_def image_def) apply (rule_tac x= "of_nat ba" in exI) apply (simp add:shiftl_t2n) apply (clarsimp simp: pt_bits_def pageBits_def word_of_nat_le) apply (clarsimp simp: distinct_map distinct_enum_upto upto_enum_step_def inj_on_def
                          pt_bits_def pageBits_def) apply (subst (asm) mult.commute[where b = 4])+ apply (simp add:shiftl_t2n[where n=2,simplified,symmetric] shiftl_shiftr1 word_size) apply (subst (asm) iffD2[OF mask_eq_iff_w2p],simp add:word_size) apply (erule le_less_trans,simp) apply (subst (asm) iffD2[OF mask_eq_iff_w2p],simp add:word_size) apply (erule le_less_trans,simp+) apply (simp add:invs_def valid_state_def valid_pspace_def valid_mdb_def) by (clarsimp simp: invs_def valid_state_def valid_cap_def obj_at_def valid_pspace_def
              dest!: cte_wp_valid_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) (clear_object_caps w) (mapM_x (swp store_pte InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1]) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) (do s <- get;
select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr s = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot
od) (mapM_x (swp store_pte InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1]) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1]) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'; \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> w \<le> w + 2 ^ pt_bits - 1
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , w + 4 - w .e. w + 2 ^ pt_bits - 1 - w]))
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'\<rbrakk> \<Longrightarrow> w \<le> w + 2 ^ pt_bits - 1
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , w + 4 - w .e. w + 2 ^ pt_bits - 1 - w]))
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> w \<le> w + 2 ^ pt_bits - 1
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , w + 4 - w .e. w + 2 ^ pt_bits - 1 - w]))
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; is_aligned w 10; 10 < word_bits; typ_at (AArch APageTable) w s'; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> w \<le> w + 2 ^ pt_bits - 1
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , w + 4 - w .e. w + 2 ^ pt_bits - 1 - w]))
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; is_aligned w 10; 10 < word_bits; typ_at (AArch APageTable) w s'; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> is_aligned w pt_bits
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , w + 4 - w .e. w + 2 ^ pt_bits - 1 - w]))
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , 4 .e. 0x3FF]))
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q53 s' ptx) (?Q'53 s' ptx) (select {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs} >>= mapM_x PageTableUnmap_D.empty_slot) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , 4 .e. 0x3FF]))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q53 s' ptx s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'53 s' ptx s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P57 s' ptx) (?Q'53 s' ptx) (mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])) (mapM_x (swp store_pte InvalidPTE) (map ((+) w) [0 , 4 .e. 0x3FF]))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> (?P57 s' ptx and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'53 s' ptx s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (8 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> dcorres dc (?P57 s' ptx) (?Q'53 s' ptx) (PageTableUnmap_D.empty_slot x) (swp store_pte InvalidPTE y)
 2. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> \<lbrace>?P57 s' ptx\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv. ?P57 s' ptx\<rbrace>
 3. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 s' ptx\<rbrace> swp store_pte InvalidPTE y \<lbrace>\<lambda>rv. ?Q'53 s' ptx\<rbrace>
 4. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> length (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) = length (map ((+) w) [0 , 4 .e. 0x3FF])
 5. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}
 6. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> (?P57 s' ptx and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 7. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'53 s' ptx s
 8. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (8 subgoals):
 1. \<And>s' ptx y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P57 s' ptx) (?Q'53 s' ptx) (PageTableUnmap_D.empty_slot (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))) (store_pte y InvalidPTE)
 2. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> \<lbrace>?P57 s' ptx\<rbrace> PageTableUnmap_D.empty_slot x \<lbrace>\<lambda>rv. ?P57 s' ptx\<rbrace>
 3. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 s' ptx\<rbrace> swp store_pte InvalidPTE y \<lbrace>\<lambda>rv. ?Q'53 s' ptx\<rbrace>
 4. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> length (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) = length (map ((+) w) [0 , 4 .e. 0x3FF])
 5. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}
 6. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> (?P57 s' ptx and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 7. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'53 s' ptx s
 8. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (6 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> \<lbrace>valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace> swp store_pte InvalidPTE y \<lbrace>\<lambda>rv. valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> length (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) = length (map ((+) w) [0 , 4 .e. 0x3FF])
 3. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 6. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (7 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}\<rbrakk> \<Longrightarrow> \<lbrace>?Q126 s' ptx x y\<rbrace> swp store_pte InvalidPTE y \<lbrace>\<lambda>rv. valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))\<rbrace>
 2. \<And>s' ptx x y s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; (x, y) \<in> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}; (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s\<rbrakk> \<Longrightarrow> ?Q126 s' ptx x y s
 3. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> length (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) = length (map ((+) w) [0 , 4 .e. 0x3FF])
 4. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 6. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 7. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (6 subgoals):
 1. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; valid_idle s; tcb_at (cur_thread s) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s)
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> length (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) = length (map ((+) w) [0 , 4 .e. 0x3FF])
 3. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 6. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> length (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) = length (map ((+) w) [0 , 4 .e. 0x3FF])
 2. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))}
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 0x3FF]) (map ((+) w) [0 , 4 .e. 0x3FF])) \<subseteq> {(x, y). x = (y && ~~ mask 10, unat (y && mask 10 >> 2))}
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba baa. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; ((aa, ba), baa) \<in> set (zip (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 0x3FF]) (map ((+) w) [0 , 4 .e. 0x3FF]))\<rbrakk> \<Longrightarrow> aa = baa && ~~ mask 10 \<and> ba = unat (baa && mask 10 >> 2)
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba baa. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; \<exists>t. (aa, ba) = (w, unat (t >> 2)) \<and> baa = w + t \<and> t \<in> set [0 , 4 .e. 0x3FF]\<rbrakk> \<Longrightarrow> aa = baa && ~~ mask 10 \<and> ba = unat (baa && mask 10 >> 2)
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; t \<in> set [0 , 4 .e. 0x3FF]\<rbrakk> \<Longrightarrow> w = w + t && ~~ mask 10 \<and> t >> 2 = w + t && mask 10 >> 2
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> w = w + t && ~~ mask 10 \<and> t >> 2 = w + t && mask 10 >> 2
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> w = w + t && ~~ mask 10 \<and> t >> 2 = w + t && mask 10 >> 2
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> w = w + t && ~~ mask 10
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; is_aligned w 10 \<and> 10 < word_bits \<and> typ_at (AArch APageTable) w s' \<and> (case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))\<rbrakk> \<Longrightarrow> w = w + t && ~~ mask 10
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (6 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; is_aligned w 10 \<and> 10 < word_bits \<and> typ_at (AArch APageTable) w s' \<and> (case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))\<rbrakk> \<Longrightarrow> is_aligned w 10
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; is_aligned w 10 \<and> 10 < word_bits \<and> typ_at (AArch APageTable) w s' \<and> (case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))\<rbrakk> \<Longrightarrow> t < 2 ^ 10
 3. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 6. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; is_aligned w 10 \<and> 10 < word_bits \<and> typ_at (AArch APageTable) w s' \<and> (case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection))\<rbrakk> \<Longrightarrow> t < 2 ^ 10
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; is_aligned w 10; x \<le> 0xFF; 10 < word_bits; typ_at (AArch APageTable) w s'; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> x * 4 < 0x400
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (6 subgoals):
 1. \<And>s' ptx x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; is_aligned w 10; x \<le> 0xFF; 10 < word_bits; typ_at (AArch APageTable) w s'; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> x < 0x100
 2. \<And>s' ptx x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; is_aligned w 10; x \<le> 0xFF; 10 < word_bits; typ_at (AArch APageTable) w s'; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> 0 < 4
 3. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 6. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t >> 2 = w + t && mask 10 >> 2
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t = w + t && mask 10
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> is_aligned w 10
 2. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t < 2 ^ 10
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx t. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; t \<in> set [0 , 4 .e. 0x3FF]; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option)\<rbrakk> \<Longrightarrow> t < 2 ^ 10
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option); x \<le> 0xFF\<rbrakk> \<Longrightarrow> x * 4 < 0x400
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option); x \<le> 0xFF\<rbrakk> \<Longrightarrow> x < 0x100
 2. \<And>s' ptx x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; s' \<turnstile> ArchObjectCap (arch_cap.PageTableCap w option); x \<le> 0xFF\<rbrakk> \<Longrightarrow> 0 < 4
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1] \<in> {xs. set xs = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr (transform s') = Some y)} \<and> distinct xs})) s
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> (\<lambda>x. (w, unat (x >> 2))) ` set [0 , 4 .e. 2 ^ pt_bits - 1] = {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr s = Some y)}
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx s x. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> (x \<in> (\<lambda>x. (w, unat (x >> 2))) ` set [0 , 4 .e. 2 ^ pt_bits - 1]) = (x \<in> {cptr. fst cptr = w \<and> (\<exists>y. opt_cap cptr s = Some y)})
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'\<rbrakk> \<Longrightarrow> (aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))) = (aa = w \<and> (\<exists>y. opt_cap (aa, ba) (transform s') = Some y))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'\<rbrakk> \<Longrightarrow> (aa \<noteq> idle_thread s' \<longrightarrow> (aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))) = (aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y))) \<and> (aa = idle_thread s' \<longrightarrow> idle_thread s' = w \<longrightarrow> (\<forall>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba \<noteq> unat (x >> 2)))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'\<rbrakk> \<Longrightarrow> (aa \<noteq> idle_thread s' \<longrightarrow> (aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))) = (aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y))) \<and> (aa = idle_thread s' \<longrightarrow> idle_thread s' = w \<longrightarrow> (\<forall>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba \<noteq> unat (x >> 2)))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> (aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))) = (aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> unat (x * 4 >> 2) < 256
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x * 4 >> 2 < word_of_nat 256
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> 4 * x >> 2 < word_of_nat 256
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x << 2 >> 2 < 0x100
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x && mask 30 < 0x100
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (7 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> 30 < size x
 2. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x < 2 ^ 30
 3. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x < 0x100
 4. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 6. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 7. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (6 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> 0xFF\<rbrakk> \<Longrightarrow> x < 0x40000000
 2. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x < 0x100
 3. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 6. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x < 0x100
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx x. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; x \<le> 0xFF\<rbrakk> \<Longrightarrow> x < 0x100
 2. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx aa ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; not_idle_thread w s'; aa \<noteq> idle_thread s'; aa = w \<and> (\<exists>y. (case case kheap s' aa of None \<Rightarrow> Some cdl_object.Untyped | Some x \<Rightarrow> (Some \<circ> transform_object (machine_state s') aa (ekheap s' aa)) x of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) ba = Some y)\<rbrakk> \<Longrightarrow> aa = w \<and> (\<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2))
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> \<exists>x\<in>set [0 , 4 .e. 2 ^ pt_bits - 1]. ba = unat (x >> 2)
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> ba = unat (word_of_nat ba << 2 >> 2)
 2. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba << 2 \<in> set [0 , 4 .e. 2 ^ pt_bits - 1]
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (5 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> ba = unat (word_of_nat ba && mask 30)
 2. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba << 2 \<in> set [0 , 4 .e. 2 ^ pt_bits - 1]
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 5. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (6 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba < 2 ^ 30
 2. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> ba = unat (word_of_nat ba)
 3. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba << 2 \<in> set [0 , 4 .e. 2 ^ pt_bits - 1]
 4. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 6. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (7 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> ba < 2 ^ 30
 2. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> 30 < LENGTH(32)
 3. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> ba = unat (word_of_nat ba)
 4. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba << 2 \<in> set [0 , 4 .e. 2 ^ pt_bits - 1]
 5. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 6. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 7. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba << 2 \<in> set [0 , 4 .e. 2 ^ pt_bits - 1]
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> \<exists>x\<le>(2 ^ pt_bits - 1) div 4. word_of_nat ba << 2 = x * 4
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba \<le> (2 ^ pt_bits - 1) div 4 \<and> word_of_nat ba << 2 = word_of_nat ba * 4
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx ba. \<lbrakk>kheap s' w = Some (ArchObj (arch_kernel_obj.PageTable ptx)); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; 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_ioc 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_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_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'; w \<noteq> idle_thread s'; ba < 256\<rbrakk> \<Longrightarrow> word_of_nat ba \<le> (2 ^ pt_bits - 1) div 4
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; transform s' = s\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. (w, unat (x >> 2))) [0 , 4 .e. 2 ^ pt_bits - 1])
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF; x * 4 >> 2 = y * 4 >> 2\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF; 4 * x >> 2 = 4 * y >> 2\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF; x && mask 30 = y && mask 30\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF\<rbrakk> \<Longrightarrow> x < 2 ^ 30
 2. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF; x = y && mask 30\<rbrakk> \<Longrightarrow> x = y
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (3 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF; x = y && mask 30\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 3. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (4 subgoals):
 1. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF\<rbrakk> \<Longrightarrow> y < 2 ^ 30
 2. \<And>s' ptx x y. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; x \<le> 0xFF; y \<le> 0xFF; x = y\<rbrakk> \<Longrightarrow> x = y
 3. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s'; invs s'; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s
 4. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (2 subgoals):
 1. \<And>s' ptx s. \<lbrakk>ako_at (arch_kernel_obj.PageTable ptx) w s; invs s; cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b) s; s' = s\<rbrakk> \<Longrightarrow> valid_idle s \<and> cur_tcb s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)
 2. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (invs and cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) s'\<rbrakk> \<Longrightarrow> \<exists>ptx. ako_at (arch_kernel_obj.PageTable ptx) w s'