theory ArchVSpace_AI

lemma perform_page_table_invocation_invs[wp]:
  notes no_irq[wp] hoare_pre [wp_pre del]
  shows
  "\<lbrace>invs and valid_pti pti\<rbrace>
   perform_page_table_invocation pti
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (cases pti) apply (clarsimp simp: valid_pti_def perform_page_table_invocation_def) apply (wp dmo_invs) apply (rule_tac Q="\<lambda>_. invs" in hoare_post_imp) apply safe apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p =
                                 underlying_memory m p" in use_valid) apply ((clarsimp simp: machine_op_lift_def
                              machine_rest_lift_def split_def | wp)+)[3] apply(erule use_valid, wp no_irq_cleanByVA_PoU no_irq, assumption) apply (wp store_pde_map_invs)[1] apply simp apply (rule hoare_pre, wp arch_update_cap_invs_map arch_update_cap_pspace
             arch_update_cap_valid_mdb set_cap_idle update_cap_ifunsafe
             valid_irq_node_typ valid_pde_lift set_cap_typ_at
             set_cap_irq_handlers set_cap_empty_pde
             hoare_vcg_all_lift hoare_vcg_ex_lift hoare_vcg_imp_lift
             set_cap_arch_obj set_cap_obj_at_impossible set_cap_valid_arch_caps) apply (simp; intro conjI; clarsimp simp: cte_wp_at_caps_of_state) apply (clarsimp simp: is_pt_cap_def is_arch_update_def cap_master_cap_def
                           vs_cap_ref_simps
                    split: cap.splits arch_cap.splits option.splits) apply fastforce apply (rule exI, rule conjI, assumption) apply (clarsimp simp: is_pt_cap_def is_arch_update_def
                         cap_master_cap_def cap_asid_def vs_cap_ref_simps
                         is_arch_cap_def pde_ref_def pde_ref_pages_def
                  split: cap.splits arch_cap.splits option.splits
                         pde.splits) apply (intro allI impI conjI, fastforce) apply (clarsimp simp: caps_of_def cap_of_def) apply (frule invs_pd_caps) apply (drule (1) empty_table_pt_capI) apply (clarsimp simp: obj_at_def empty_table_def pte_ref_pages_def) apply (clarsimp simp: perform_page_table_invocation_def
                 split: cap.split arch_cap.split) apply (rename_tac word option) apply (rule hoare_pre) apply (wp arch_update_cap_invs_unmap_page_table get_cap_wp) apply (simp add: cte_wp_at_caps_of_state) apply (wpc, wp, wpc) apply (rule hoare_lift_Pf2[where f=caps_of_state]) apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift)+ apply (rule hoare_vcg_conj_lift) apply (wp dmo_invs_lift hoare_vcg_all_lift hoare_vcg_const_imp_lift
                   valid_cap_typ[OF do_machine_op_obj_at]
                   mapM_x_swp_store_pte_invs[unfolded cte_wp_at_caps_of_state]
                   mapM_x_swp_store_empty_table
                   valid_cap_typ[OF unmap_page_table_typ_at]
                   unmap_page_table_unmapped3
                   store_pte_no_lookup_pages
              | wp (once) hoare_vcg_conj_lift
              | wp (once) mapM_x_wp'
              | simp)+ apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state
                        is_cap_simps
                        is_arch_update_def cap_rights_update_def
                        acap_rights_update_def cap_master_cap_simps
                        update_map_data_def) apply (rule conjI) apply (clarsimp simp: vs_cap_ref_def) apply (drule invs_pd_caps) apply (simp add: valid_table_caps_def) apply (elim allE, drule(1) mp) apply (simp add: is_cap_simps cap_asid_def) apply (drule mp, rule refl) apply (clarsimp simp: obj_at_def valid_cap_def empty_table_def
                         a_type_def) apply (clarsimp split: Structures_A.kernel_object.split_asm
                          arch_kernel_obj.split_asm) apply (clarsimp simp: valid_cap_def mask_def[where n=asid_bits]
                        vmsz_aligned_def cap_aligned_def vs_cap_ref_def
                        invs_psp_aligned invs_vspace_objs) apply (subgoal_tac "(\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1].
                             x && ~~ mask pt_bits = word)") apply (intro conjI) apply (simp add: cap_master_cap_def) apply fastforce apply (clarsimp simp: image_def) apply (subgoal_tac "word + (ucast x << 2)
                   \<in> set [word, word + 4 .e. word + 2 ^ pt_bits - 1]") apply (rule rev_bexI, assumption) apply (rule ccontr, erule more_pt_inner_beauty) apply simp apply (clarsimp simp: upto_enum_step_def linorder_not_less) apply (subst is_aligned_no_overflow,
           erule is_aligned_weaken,
           (simp_all add: pt_bits_def pageBits_def)[2])+ apply (clarsimp simp: image_def word_shift_by_2) apply (rule exI, rule conjI[OF _ refl]) apply (rule plus_one_helper) apply (rule order_less_le_trans, rule ucast_less, simp+) apply (clarsimp simp: upto_enum_step_def) apply (rule conjunct2, rule is_aligned_add_helper) apply (simp add: pt_bits_def pageBits_def) apply (simp only: word_shift_by_2) apply (rule shiftl_less_t2n) apply (rule word_leq_minus_one_le) apply (simp add: pt_bits_def pageBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_pti pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14. pti = PageTableMap x11 x12 x13 x14 \<Longrightarrow> \<lbrace>invs and valid_pti pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x21 x22. pti = PageTableUnmap x21 x22 \<Longrightarrow> \<lbrace>invs and valid_pti pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> do y <- set_cap x11 (a, b);
y <- store_pde x14 x13;
do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x21 x22. pti = PageTableUnmap x21 x22 \<Longrightarrow> \<lbrace>invs and valid_pti pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 a b x13 x14 y. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>?B4 x11 a b x13 x14 y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>ya s. \<forall>m. \<forall>(r, m')\<in>fst (cleanByVA_PoU x14 (addrFromPPtr x14) m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s\<rbrace>
 2. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>?B4 x11 a b x13 x14\<rbrace>
 3. \<And>x21 x22. pti = PageTableUnmap x21 x22 \<Longrightarrow> \<lbrace>invs and valid_pti pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 a b x13 x14 y rv s. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s\<rbrakk> \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (cleanByVA_PoU x14 (addrFromPPtr x14) m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s
 2. \<And>x11 a b x13 x14 y. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>?B4 x11 a b x13 x14 y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>_. invs\<rbrace>
 3. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>?B4 x11 a b x13 x14\<rbrace>
 4. \<And>x21 x22. pti = PageTableUnmap x21 x22 \<Longrightarrow> \<lbrace>invs and valid_pti pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x11 a b x13 x14 s m ba p. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; ((), ba) \<in> fst (cleanByVA_PoU x14 (addrFromPPtr x14) m); underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>x11 a b x13 x14 s m ba irq. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; ((), ba) \<in> fst (cleanByVA_PoU x14 (addrFromPPtr x14) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq
 3. \<And>x11 a b x13 x14 y. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>?B4 x11 a b x13 x14 y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>_. invs\<rbrace>
 4. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>?B4 x11 a b x13 x14\<rbrace>
 5. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 a b x13 x14 s m ba p. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P29 x11 a b x13 x14 s m ba p\<rbrace> cleanByVA_PoU x14 (addrFromPPtr x14) \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>x11 a b x13 x14 s m ba p. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; underlying_memory ba p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P29 x11 a b x13 x14 s m ba p m
 3. \<And>x11 a b x13 x14 s m ba p. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; underlying_memory ba p \<noteq> underlying_memory m p; underlying_memory ba p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>x11 a b x13 x14 s m ba irq. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; ((), ba) \<in> fst (cleanByVA_PoU x14 (addrFromPPtr x14) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq
 5. \<And>x11 a b x13 x14 y. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>?B4 x11 a b x13 x14 y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>_. invs\<rbrace>
 6. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>?B4 x11 a b x13 x14\<rbrace>
 7. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 a b x13 x14 s m ba irq. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; ((), ba) \<in> fst (cleanByVA_PoU x14 (addrFromPPtr x14) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks ba irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks ba irq
 2. \<And>x11 a b x13 x14 y. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>?B4 x11 a b x13 x14 y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>_. invs\<rbrace>
 3. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>?B4 x11 a b x13 x14\<rbrace>
 4. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 a b x13 x14 y. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>?B4 x11 a b x13 x14 y\<rbrace> store_pde x14 x13 \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>?B4 x11 a b x13 x14\<rbrace>
 3. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. (\<lambda>s. wellformed_pde x13) and invs and empty_pde_at x14 and valid_pde x13 and (\<lambda>s. \<forall>p. pde_ref x13 = Some p \<longrightarrow> (\<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s)) and K (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs) and (\<lambda>s. \<exists>r. (r \<rhd> (x14 && ~~ mask pd_bits)) s \<and> (\<forall>p'. pde_ref_pages x13 = Some p' \<longrightarrow> (\<exists>p'' cap. caps_of_state s p'' = Some cap \<and> p' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # r)) \<and> (\<forall>p''' a b. x13 = PageTablePDE p''' a b \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (ptrFromPAddr p''') s \<longrightarrow> (\<forall>x word. pte_ref_pages (pt x) = Some word \<longrightarrow> (\<exists>p'' cap. caps_of_state s p'' = Some cap \<and> word \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # r)))))))\<rbrace>
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14. pti = PageTableMap x11 (a, b) x13 x14 \<Longrightarrow> \<lbrace>invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))\<rbrace> set_cap x11 (a, b) \<lbrace>\<lambda>y. (\<lambda>s. wellformed_pde x13) and invs and empty_pde_at x14 and valid_pde x13 and (\<lambda>s. \<forall>p. pde_ref x13 = Some p \<longrightarrow> (\<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s)) and (\<lambda>y. VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs) and (\<lambda>s. \<exists>r. (r \<rhd> (x14 && ~~ mask pd_bits)) s \<and> (\<forall>p'. pde_ref_pages x13 = Some p' \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p' \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # r)) \<and> (\<forall>p'''. (\<exists>a b. x13 = PageTablePDE p''' a b) \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (ptrFromPAddr p''') s \<longrightarrow> (\<forall>x word. pte_ref_pages (pt x) = Some word \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> word \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # r)))))))\<rbrace>
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14 s. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; (invs and (pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) (a, b) and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y)))) s\<rbrakk> \<Longrightarrow> wellformed_pde x13 \<and> (cte_wp_at (is_arch_update x11 and (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref x11 = Some r)) (a, b) and invs and valid_cap x11) s \<and> (empty_pde_at x14 and cte_wp_at (\<lambda>_. True) (a, b)) s \<and> valid_pde x13 s \<and> (\<forall>x. pde_ref x13 \<noteq> Some x \<or> (\<exists>xa. (ako_at xa x and cte_wp_at (\<lambda>_. True) (a, b)) s \<and> valid_vspace_obj xa s)) \<and> VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs \<and> (\<exists>x. (x \<rhd> (x14 && ~~ mask pd_bits)) s \<and> (\<forall>xa. pde_ref_pages x13 \<noteq> Some xa \<or> (\<exists>xb xc xd. ((caps_of_state s)((a, b) \<mapsto> x11)) (xb, xc) = Some xd \<and> xa \<in> obj_refs xd \<and> vs_cap_ref xd = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x)) \<and> (\<forall>xa. (\<nexists>a b. x13 = PageTablePDE xa a b) \<or> (\<forall>xb. \<not> ako_at (PageTable xb) (ptrFromPAddr xa) s \<and> (\<forall>ko. ArchObj (PageTable xb) = ko \<longrightarrow> caps_of ko = {}) \<or> (\<forall>xa xc. pte_ref_pages (xb xa) \<noteq> Some xc \<or> (\<exists>xb xd xe. ((caps_of_state s)((a, b) \<mapsto> x11)) (xb, xd) = Some xe \<and> xc \<in> obj_refs xe \<and> vs_cap_ref xe = Some (VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x)))))))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 a b x13 x14 s cap p' ref y ao r. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p'; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; vs_cap_ref cap = Some r\<rbrakk> \<Longrightarrow> VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref = r
 2. \<And>x11 a b x13 x14 s cap p' ref y ao. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; pde_ref x13 = Some p'\<rbrakk> \<Longrightarrow> \<exists>x. ako_at x p' s \<and> valid_vspace_obj x s
 3. \<And>x11 a b x13 x14 s cap p' ref y ao. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p'; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<rhd> (x14 && ~~ mask pd_bits)) s \<and> (\<forall>xa. pde_ref_pages x13 = Some xa \<longrightarrow> (\<exists>xb xc. (xb = a \<and> xc = b \<longrightarrow> xa \<in> obj_refs x11 \<and> ref = x) \<and> ((xb = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (xb, xc) = Some xd \<and> xa \<in> obj_refs xd \<and> vs_cap_ref xd = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x)))) \<and> (\<forall>xa. (\<forall>a b. x13 \<noteq> PageTablePDE xa a b) \<or> (\<forall>xb. \<not> ako_at (PageTable xb) (ptrFromPAddr xa) s \<and> caps_of (ArchObj (PageTable xb)) = {} \<or> (\<forall>xa xc. pte_ref_pages (xb xa) = Some xc \<longrightarrow> (\<exists>xb xd. (xb = a \<longrightarrow> xd \<noteq> b) \<and> ((xb = a \<longrightarrow> xd \<noteq> b) \<longrightarrow> (\<exists>xe. caps_of_state s (xb, xd) = Some xe \<and> xc \<in> obj_refs xe \<and> vs_cap_ref xe = Some (VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x))))))))
 4. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 a b x13 x14 s cap p' ref y ao. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s; pde_ref x13 = Some p'\<rbrakk> \<Longrightarrow> \<exists>x. ako_at x p' s \<and> valid_vspace_obj x s
 2. \<And>x11 a b x13 x14 s cap p' ref y ao. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p'; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<rhd> (x14 && ~~ mask pd_bits)) s \<and> (\<forall>xa. pde_ref_pages x13 = Some xa \<longrightarrow> (\<exists>xb xc. (xb = a \<and> xc = b \<longrightarrow> xa \<in> obj_refs x11 \<and> ref = x) \<and> ((xb = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (xb, xc) = Some xd \<and> xa \<in> obj_refs xd \<and> vs_cap_ref xd = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x)))) \<and> (\<forall>xa. (\<forall>a b. x13 \<noteq> PageTablePDE xa a b) \<or> (\<forall>xb. \<not> ako_at (PageTable xb) (ptrFromPAddr xa) s \<and> caps_of (ArchObj (PageTable xb)) = {} \<or> (\<forall>xa xc. pte_ref_pages (xb xa) = Some xc \<longrightarrow> (\<exists>xb xd. (xb = a \<longrightarrow> xd \<noteq> b) \<and> ((xb = a \<longrightarrow> xd \<noteq> b) \<longrightarrow> (\<exists>xe. caps_of_state s (xb, xd) = Some xe \<and> xc \<in> obj_refs xe \<and> vs_cap_ref xe = Some (VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x))))))))
 3. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14 s cap p' ref y ao. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p'; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<rhd> (x14 && ~~ mask pd_bits)) s \<and> (\<forall>xa. pde_ref_pages x13 = Some xa \<longrightarrow> (\<exists>xb xc. (xb = a \<and> xc = b \<longrightarrow> xa \<in> obj_refs x11 \<and> ref = x) \<and> ((xb = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (xb, xc) = Some xd \<and> xa \<in> obj_refs xd \<and> vs_cap_ref xd = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x)))) \<and> (\<forall>xa. (\<forall>a b. x13 \<noteq> PageTablePDE xa a b) \<or> (\<forall>xb. \<not> ako_at (PageTable xb) (ptrFromPAddr xa) s \<and> caps_of (ArchObj (PageTable xb)) = {} \<or> (\<forall>xa xc. pte_ref_pages (xb xa) = Some xc \<longrightarrow> (\<exists>xb xd. (xb = a \<longrightarrow> xd \<noteq> b) \<and> ((xb = a \<longrightarrow> xd \<noteq> b) \<longrightarrow> (\<exists>xe. caps_of_state s (xb, xd) = Some xe \<and> xc \<in> obj_refs xe \<and> vs_cap_ref xe = Some (VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # x))))))))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b x13 x14 s cap p' ref y ao. \<lbrakk>pti = PageTableMap x11 (a, b) x13 x14; invs s; pde_at x14 s; wellformed_pde x13; valid_pde x13 s; s \<turnstile> x11; empty_pde_at x14 s; caps_of_state s (a, b) = Some cap; is_arch_update x11 cap; cap_asid cap = None; is_pt_cap x11; cap_asid x11 = Some y; vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (x14 && ~~ mask pd_bits)) s; pde_ref x13 = Some p'; p' \<in> obj_refs x11; VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<forall>x. pde_ref_pages x13 = Some x \<longrightarrow> (\<exists>xa xb. (xa = a \<and> xb = b \<longrightarrow> x \<in> obj_refs x11 \<and> ref = ref) \<and> ((xa = a \<longrightarrow> xb \<noteq> b) \<longrightarrow> (\<exists>xc. caps_of_state s (xa, xb) = Some xc \<and> x \<in> obj_refs xc \<and> vs_cap_ref xc = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref)))) \<and> (\<forall>x. (\<forall>a b. x13 \<noteq> PageTablePDE x a b) \<or> (\<forall>xa. \<not> ako_at (PageTable xa) (ptrFromPAddr x) s \<and> caps_of (ArchObj (PageTable xa)) = {} \<or> (\<forall>x xb. pte_ref_pages (xa x) = Some xb \<longrightarrow> (\<exists>xa xc. (xa = a \<longrightarrow> xc \<noteq> b) \<and> ((xa = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (xa, xc) = Some xd \<and> xb \<in> obj_refs xd \<and> vs_cap_ref xd = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref)))))))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x14 s y ao ba x21 x22 x23. \<lbrakk>VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao (ptrFromPAddr x21) s; valid_vspace_obj ao s; pti = PageTableMap (ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba)))) (a, b) (PageTablePDE x21 x22 x23) x14; invs s; pde_at x14 s; typ_at (AArch APageTable) (ptrFromPAddr x21) s; s \<turnstile> ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba))); empty_pde_at x14 s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (ptrFromPAddr x21) None)); ([VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None] \<rhd> (x14 && ~~ mask pd_bits)) s; x22 \<subseteq> {ParityEnabled}; is_aligned x21 pt_bits; ba >> 20 = x14 && mask pd_bits >> 2\<rbrakk> \<Longrightarrow> (\<exists>x xa. (x = a \<longrightarrow> xa \<noteq> b) \<longrightarrow> (\<exists>xb. caps_of_state s (x, xa) = Some xb \<and> ptrFromPAddr x21 \<in> obj_refs xb \<and> vs_cap_ref xb = Some [VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory), VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None])) \<and> (\<forall>x. \<not> ako_at (PageTable x) (ptrFromPAddr x21) s \<and> caps_of (ArchObj (PageTable x)) = {} \<or> (\<forall>xa xb. pte_ref_pages (x xa) = Some xb \<longrightarrow> (\<exists>x xc. (x = a \<longrightarrow> xc \<noteq> b) \<and> ((x = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (x, xc) = Some xd \<and> xb \<in> obj_refs xd \<and> vs_cap_ref xd = Some [VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable), VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory), VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None])))))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x14 s y ao ba x21 x22 x23 x. \<lbrakk>VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao (ptrFromPAddr x21) s; valid_vspace_obj ao s; pti = PageTableMap (ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba)))) (a, b) (PageTablePDE x21 x22 x23) x14; invs s; pde_at x14 s; typ_at (AArch APageTable) (ptrFromPAddr x21) s; s \<turnstile> ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba))); empty_pde_at x14 s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (ptrFromPAddr x21) None)); ([VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None] \<rhd> (x14 && ~~ mask pd_bits)) s; x22 \<subseteq> {ParityEnabled}; is_aligned x21 pt_bits; ba >> 20 = x14 && mask pd_bits >> 2\<rbrakk> \<Longrightarrow> \<not> ako_at (PageTable x) (ptrFromPAddr x21) s \<and> caps_of (ArchObj (PageTable x)) = {} \<or> (\<forall>xa xb. pte_ref_pages (x xa) = Some xb \<longrightarrow> (\<exists>x xc. (x = a \<longrightarrow> xc \<noteq> b) \<and> ((x = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (x, xc) = Some xd \<and> xb \<in> obj_refs xd \<and> vs_cap_ref xd = Some [VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable), VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory), VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None]))))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x14 s y ao ba x21 x22 x23 x xa xb. \<lbrakk>VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao (ptrFromPAddr x21) s; valid_vspace_obj ao s; pti = PageTableMap (ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba)))) (a, b) (PageTablePDE x21 x22 x23) x14; invs s; pde_at x14 s; typ_at (AArch APageTable) (ptrFromPAddr x21) s; s \<turnstile> ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba))); empty_pde_at x14 s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (ptrFromPAddr x21) None)); ([VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None] \<rhd> (x14 && ~~ mask pd_bits)) s; x22 \<subseteq> {ParityEnabled}; is_aligned x21 pt_bits; ba >> 20 = x14 && mask pd_bits >> 2; ako_at (PageTable x) (ptrFromPAddr x21) s; pte_ref_pages (x xa) = Some xb\<rbrakk> \<Longrightarrow> \<exists>x xc. (x = a \<longrightarrow> xc \<noteq> b) \<and> ((x = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (x, xc) = Some xd \<and> xb \<in> obj_refs xd \<and> vs_cap_ref xd = Some [VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable), VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory), VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None]))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x14 s y ao ba x21 x22 x23 x xa xb. \<lbrakk>VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao (ptrFromPAddr x21) s; valid_vspace_obj ao s; pti = PageTableMap (ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba)))) (a, b) (PageTablePDE x21 x22 x23) x14; invs s; pde_at x14 s; typ_at (AArch APageTable) (ptrFromPAddr x21) s; s \<turnstile> ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba))); empty_pde_at x14 s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (ptrFromPAddr x21) None)); ([VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None] \<rhd> (x14 && ~~ mask pd_bits)) s; x22 \<subseteq> {ParityEnabled}; is_aligned x21 pt_bits; ba >> 20 = x14 && mask pd_bits >> 2; ako_at (PageTable x) (ptrFromPAddr x21) s; pte_ref_pages (x xa) = Some xb; valid_table_caps s\<rbrakk> \<Longrightarrow> \<exists>x xc. (x = a \<longrightarrow> xc \<noteq> b) \<and> ((x = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (x, xc) = Some xd \<and> xb \<in> obj_refs xd \<and> vs_cap_ref xd = Some [VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable), VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory), VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None]))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x14 s y ao ba x21 x22 x23 x xa xb. \<lbrakk>VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao (ptrFromPAddr x21) s; valid_vspace_obj ao s; pti = PageTableMap (ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba)))) (a, b) (PageTablePDE x21 x22 x23) x14; invs s; pde_at x14 s; typ_at (AArch APageTable) (ptrFromPAddr x21) s; s \<turnstile> ArchObjectCap (PageTableCap (ptrFromPAddr x21) (Some (y, ba))); empty_pde_at x14 s; ([VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None] \<rhd> (x14 && ~~ mask pd_bits)) s; x22 \<subseteq> {ParityEnabled}; is_aligned x21 pt_bits; ba >> 20 = x14 && mask pd_bits >> 2; ako_at (PageTable x) (ptrFromPAddr x21) s; pte_ref_pages (x xa) = Some xb; valid_table_caps s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (ptrFromPAddr x21) s\<rbrakk> \<Longrightarrow> \<exists>x xc. (x = a \<longrightarrow> xc \<noteq> b) \<and> ((x = a \<longrightarrow> xc \<noteq> b) \<longrightarrow> (\<exists>xd. caps_of_state s (x, xc) = Some xd \<and> xb \<in> obj_refs xd \<and> vs_cap_ref xd = Some [VSRef (UCAST(8 \<rightarrow> 32) xa) (Some APageTable), VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory), VSRef (y && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of y)) None]))
 2. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 a b. pti = PageTableUnmap x21 (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap x21 (a, b))\<rbrace> perform_page_table_invocation (PageTableUnmap x21 (a, b)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b x41 x42. pti = PageTableUnmap (ArchObjectCap (PageTableCap x41 x42)) (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap x41 x42)) (a, b))\<rbrace> do y <- case x42 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr x41;
pte_bits <- return 2;
slots <- return [x41 , x41 + (1 << pte_bits) .e. x41 + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU x41 (x41 + (1 << pt_bits) - 1) (addrFromPPtr x41)
od;
cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (ArchObjectCap (update_map_data cap None)) (a, b)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b word option. pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b) \<Longrightarrow> \<lbrace>invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))\<rbrace> do y <- case option of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od;
cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (ArchObjectCap (update_map_data cap None)) (a, b)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b word option. pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b) \<Longrightarrow> \<lbrace>?Q836 a b word option\<rbrace> do y <- case option of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od;
cap <- liftM the_arch_cap (get_cap (a, b));
set_cap (ArchObjectCap (update_map_data cap None)) (a, b)
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> ?Q836 a b word option s proof (prove)
goal (2 subgoals):
 1. \<And>a b word option. pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b) \<Longrightarrow> \<lbrace>?Q836 a b word option\<rbrace> case option of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>y s. \<forall>cap. cte_wp_at ((=) cap) (a, b) s \<longrightarrow> ((\<lambda>cap s. cte_wp_at (is_arch_update (ArchObjectCap (update_map_data cap None))) (a, b) s \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data cap None) \<and> cte_wp_at (\<lambda>c. is_final_cap' c s) (a, b) s \<and> obj_at (empty_table {}) (obj_ref_of (ArchObjectCap (update_map_data cap None))) s \<and> cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> (r, obj_ref_of (ArchObjectCap (update_map_data cap None))) \<notin> vs_lookup_pages s) (a, b) s \<and> K (is_pt_cap (ArchObjectCap (update_map_data cap None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data cap None)) = None) s) \<circ> the_arch_cap) cap s\<rbrace>
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> ?Q836 a b word option s proof (prove)
goal (2 subgoals):
 1. \<And>a b word option. pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b) \<Longrightarrow> \<lbrace>?Q836 a b word option\<rbrace> case option of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>y s. \<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None\<rbrace>
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> ?Q836 a b word option s proof (prove)
goal (2 subgoals):
 1. \<And>a b word option x2 x1 x2a. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>?R873 a b word option x2 x1 x2a\<rbrace> do unmap_page_table x1 x2a word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>y s. \<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None\<rbrace>
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> (option = None \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None)) \<and> (\<forall>x. option = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R873 a b word option x xa xb s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b word option x2 x1 x2a x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>?Q874 a b word option x2 x1 x2a x\<rbrace> do unmap_page_table x1 x2a word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>_ c. \<forall>cap. x (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs c \<and> c \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap c \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) c \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages c) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None\<rbrace>
 2. \<And>a b word option x2 x1 x2a P. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do unmap_page_table x1 x2a word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 3. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> (option = None \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None)) \<and> (\<forall>x. option = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> ?Q874 a b word option x xa xb (caps_of_state s) s)) proof (prove)
goal (7 subgoals):
 1. \<And>a b word option x2 x1 x2a x cap xa pte_bits slots xb. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B889 a b word option x2 x1 x2a x cap xa pte_bits slots xb\<rbrace> do_machine_op (cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)) \<lbrace>\<lambda>rv s. invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None\<rbrace>
 2. \<And>a b word option x2 x1 x2a x cap xa pte_bits slots. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B888 a b word option x2 x1 x2a x cap xa pte_bits slots\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>?B889 a b word option x2 x1 x2a x cap xa pte_bits slots\<rbrace>
 3. \<And>a b word option x2 x1 x2a x cap xa pte_bits. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B887 a b word option x2 x1 x2a x cap xa pte_bits\<rbrace> return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1] \<lbrace>?B888 a b word option x2 x1 x2a x cap xa pte_bits\<rbrace>
 4. \<And>a b word option x2 x1 x2a x cap xa. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B885 a b word option x2 x1 x2a x cap xa\<rbrace> return 2 \<lbrace>?B887 a b word option x2 x1 x2a x cap xa\<rbrace>
 5. \<And>a b word option x2 x1 x2a x cap. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'882 a b word option x2 x1 x2a x cap\<rbrace> unmap_page_table x1 x2a word \<lbrace>?B885 a b word option x2 x1 x2a x cap\<rbrace>
 6. \<And>a b word option x2 x1 x2a P. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do unmap_page_table x1 x2a word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 7. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> (option = None \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None)) \<and> (\<forall>x. option = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>xc. caps_of_state s (a, b) = Some xc \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap xc) None)) xc \<and> ?P'882 a b word option x xa xb (caps_of_state s) xc s))) proof (prove)
goal (8 subgoals):
 1. \<And>a b word option x2 x1 x2a x cap xa pte_bits slots xb. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?P893 a b word option x2 x1 x2a x cap xa pte_bits slots xb\<rbrace> do_machine_op (cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>a b word option x2 x1 x2a x cap xa pte_bits slots xb. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'893 a b word option x2 x1 x2a x cap xa pte_bits slots xb\<rbrace> do_machine_op (cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)) \<lbrace>\<lambda>rv s. s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None\<rbrace>
 3. \<And>a b word option x2 x1 x2a x cap xa pte_bits slots. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B888 a b word option x2 x1 x2a x cap xa pte_bits slots\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>xb s. ?P893 a b word option x2 x1 x2a x cap xa pte_bits slots xb s \<and> ?P'893 a b word option x2 x1 x2a x cap xa pte_bits slots xb s\<rbrace>
 4. \<And>a b word option x2 x1 x2a x cap xa pte_bits. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B887 a b word option x2 x1 x2a x cap xa pte_bits\<rbrace> return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1] \<lbrace>?B888 a b word option x2 x1 x2a x cap xa pte_bits\<rbrace>
 5. \<And>a b word option x2 x1 x2a x cap xa. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?B885 a b word option x2 x1 x2a x cap xa\<rbrace> return 2 \<lbrace>?B887 a b word option x2 x1 x2a x cap xa\<rbrace>
 6. \<And>a b word option x2 x1 x2a x cap. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a); x (a, b) = Some cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'882 a b word option x2 x1 x2a x cap\<rbrace> unmap_page_table x1 x2a word \<lbrace>?B885 a b word option x2 x1 x2a x cap\<rbrace>
 7. \<And>a b word option x2 x1 x2a P. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); option = Some x2; x2 = (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do unmap_page_table x1 x2a word;
pte_bits <- return 2;
slots <- return [word , word + (1 << pte_bits) .e. word + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU word (word + (1 << pt_bits) - 1) (addrFromPPtr word)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 8. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); (invs and valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b))) s\<rbrakk> \<Longrightarrow> (option = None \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> invs s \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None)) \<and> (\<forall>x. option = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<forall>xc. caps_of_state s (a, b) = Some xc \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap xc) None)) xc \<and> ?P'882 a b word option x xa xb (caps_of_state s) xc s))) proof (prove)
goal (1 subgoal):
 1. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s \<and> valid_pti (PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b)) s\<rbrakk> \<Longrightarrow> (option = None \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap cap) None)) cap \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap cap) None) \<and> is_final_cap' cap s \<and> obj_at (empty_table {}) (the (aobj_ref (update_map_data (the_arch_cap cap) None))) s \<and> (\<forall>r. vs_cap_ref cap = Some r \<longrightarrow> (r, the (aobj_ref (update_map_data (the_arch_cap cap) None))) \<notin> vs_lookup_pages s) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap cap) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap cap) None)) = None)) \<and> (\<forall>aa ba. option = Some (aa, ba) \<longrightarrow> (\<forall>x. caps_of_state s (a, b) = Some x \<longrightarrow> is_arch_update (ArchObjectCap (update_map_data (the_arch_cap x) None)) x \<and> aa \<le> mask local.asid_bits \<and> ba < kernel_base \<and> vmsz_aligned ba ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> is_pt_cap cap) \<and> s \<turnstile> ArchObjectCap (update_map_data (the_arch_cap x) None) \<and> is_final_cap' x s \<and> typ_at (AArch APageTable) (the (aobj_ref (update_map_data (the_arch_cap x) None))) s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>xa\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. xa && ~~ mask pt_bits = the (aobj_ref (update_map_data (the_arch_cap x) None))) \<and> (\<forall>xa. vs_cap_ref x = Some xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> xa = [VSRef (ba >> 20) (Some APageDirectory), VSRef (aa && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of aa)) None] \<and> the (aobj_ref (update_map_data (the_arch_cap x) None)) = word) \<and> is_pt_cap (ArchObjectCap (update_map_data (the_arch_cap x) None)) \<and> vs_cap_ref (ArchObjectCap (update_map_data (the_arch_cap x) None)) = None)) proof (prove)
goal (1 subgoal):
 1. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> (option = None \<longrightarrow> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word None)) s \<and> obj_at (empty_table {}) word s \<and> (\<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap word None)) = Some r \<longrightarrow> (r, word) \<notin> vs_lookup_pages s) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None) \<and> (\<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None) proof (prove)
goal (2 subgoals):
 1. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> option = None \<longrightarrow> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word None)) s \<and> obj_at (empty_table {}) word s \<and> (\<forall>r. vs_cap_ref (ArchObjectCap (PageTableCap word None)) = Some r \<longrightarrow> (r, word) \<notin> vs_lookup_pages s) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); s \<turnstile> ArchObjectCap (PageTableCap word None); is_final_cap' (ArchObjectCap (PageTableCap word None)) s\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) word s
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); s \<turnstile> ArchObjectCap (PageTableCap word None); is_final_cap' (ArchObjectCap (PageTableCap word None)) s; valid_table_caps s\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) word s
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); s \<turnstile> ArchObjectCap (PageTableCap word None); is_final_cap' (ArchObjectCap (PageTableCap word None)) s; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) word s
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); s \<turnstile> ArchObjectCap (PageTableCap word None); is_final_cap' (ArchObjectCap (PageTableCap word None)) s; (is_pd_cap (ArchObjectCap (PageTableCap word None)) \<longrightarrow> cap_asid (ArchObjectCap (PageTableCap word None)) = None \<longrightarrow> ?r1089 a b word s \<in> obj_refs (ArchObjectCap (PageTableCap word None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (?r1089 a b word s) s) \<and> (is_pt_cap (ArchObjectCap (PageTableCap word None)) \<longrightarrow> cap_asid (ArchObjectCap (PageTableCap word None)) = None \<longrightarrow> ?r1089 a b word s \<in> obj_refs (ArchObjectCap (PageTableCap word None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (?r1089 a b word s) s)\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) word s
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); s \<turnstile> ArchObjectCap (PageTableCap word None); is_final_cap' (ArchObjectCap (PageTableCap word None)) s; ?r1089 a b word s = word \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (?r1089 a b word s) s\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) word s
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); s \<turnstile> ArchObjectCap (PageTableCap word None); is_final_cap' (ArchObjectCap (PageTableCap word None)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) word s\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) word s
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b word s ko. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word None)) (a, b); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word None)); is_final_cap' (ArchObjectCap (PageTableCap word None)) s; cap_aligned (ArchObjectCap (PageTableCap word None)); case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False; kheap s word = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable\<rbrakk> \<Longrightarrow> case ko of ArchObj (PageTable pt) \<Rightarrow> \<forall>x. pt x = InvalidPTE | ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> {}) \<and> valid_pde_mappings (pd x) \<and> (x \<notin> kernel_mapping_slots \<longrightarrow> pd x = InvalidPDE) | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False
 2. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b word option s. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word option)) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word option)); s \<turnstile> ArchObjectCap (PageTableCap word option); is_final_cap' (ArchObjectCap (PageTableCap word option)) s\<rbrakk> \<Longrightarrow> \<forall>a b. option = Some (a, b) \<longrightarrow> a \<le> mask local.asid_bits \<and> b < kernel_base \<and> vmsz_aligned b ARMSection \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> s \<turnstile> ArchObjectCap (PageTableCap word None) \<and> is_final_cap' (ArchObjectCap (PageTableCap word (Some (a, b)))) s \<and> typ_at (AArch APageTable) word s \<and> pspace_aligned s \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) \<and> (\<forall>x. vs_cap_ref (ArchObjectCap (PageTableCap word (Some (a, b)))) = Some x \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageTable) word s \<and> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> vs_cap_ref (ArchObjectCap (PageTableCap word None)) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word) proof (prove)
goal (2 subgoals):
 1. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))) \<and> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<and> (\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word)
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (4 subgoals):
 1. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 4. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (4 subgoals):
 1. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<lambda>x. word) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs cap \<and> (\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid))
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 4. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x = UCAST(32 \<rightarrow> 8) (xa && mask pt_bits >> 2)
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (4 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word; word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<exists>xa\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x = UCAST(32 \<rightarrow> 8) (xa && mask pt_bits >> 2)
 2. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 4. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (4 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word; word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> x = UCAST(32 \<rightarrow> 8) (word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits >> 2)
 2. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 4. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (4 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word; word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> (word + (UCAST(8 \<rightarrow> 32) x << 2) && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) x << 2) = word + (UCAST(8 \<rightarrow> 32) x << 2)
 2. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 4. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set (if word + 2 ^ pt_bits - 1 < word then [] else map (\<lambda>x. word + x * (word + 4 - word)) [0 .e. (word + 2 ^ pt_bits - 1 - word) div (word + 4 - word)]). x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> word \<le> word + 2 ^ pt_bits - 1 \<and> (word \<le> word + 2 ^ pt_bits - 1 \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> (2 ^ pt_bits - 1) div 4})
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set (if 0x3FF + word < word then [] else map (\<lambda>x. word + x * (word + 4 - word)) [0 .e. (word + 2 ^ pt_bits - 1 - word) div (word + 4 - word)]). x && ~~ mask 10 = word\<rbrakk> \<Longrightarrow> word \<le> 0x3FF + word \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> 0xFF}
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set (if 0x3FF + word < word then [] else map (\<lambda>x. word + x * (word + 4 - word)) [0 .e. (word + 2 ^ pt_bits - 1 - word) div (word + 4 - word)]). x && ~~ mask 10 = word; word \<le> 0x3FF + word\<rbrakk> \<Longrightarrow> \<exists>xa\<le>0xFF. UCAST(8 \<rightarrow> 32) x << 2 = xa << 2
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set (if 0x3FF + word < word then [] else map (\<lambda>x. word + x * (word + 4 - word)) [0 .e. (word + 2 ^ pt_bits - 1 - word) div (word + 4 - word)]). x && ~~ mask 10 = word; word \<le> 0x3FF + word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<le> 0xFF
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set (if 0x3FF + word < word then [] else map (\<lambda>x. word + x * (word + 4 - word)) [0 .e. (word + 2 ^ pt_bits - 1 - word) div (word + 4 - word)]). x && ~~ mask 10 = word; word \<le> 0x3FF + word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < 0xFF + 1
 2. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word
 3. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (1 subgoal):
 1. \<And>a b word s aa ba. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. x && ~~ mask pt_bits = word proof (prove)
goal (1 subgoal):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> word + x * 4 && ~~ mask pt_bits = word proof (prove)
goal (2 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 2. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x * 4 < 2 ^ pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x * 4 < 2 ^ pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x < 2 ^ (pt_bits - 2)
 2. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> 2 ^ (pt_bits - 2) \<noteq> 0
 2. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> x \<le> 2 ^ (pt_bits - 2) - 1
 3. \<And>a b word s aa ba x. \<lbrakk>pti = PageTableUnmap (ArchObjectCap (PageTableCap word (Some (aa, ba)))) (a, b); invs s; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap word (Some (aa, ba)))); is_final_cap' (ArchObjectCap (PageTableCap word (Some (aa, ba)))) s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; 0 < aa; aa < 2 ^ local.asid_bits; ba < kernel_base; is_aligned ba 20; \<not> word + 2 ^ pt_bits - 1 < word; x \<le> (2 ^ pt_bits - 1) div 4\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32) proof (prove)
goal:
No subgoals!