aarch64 ainvs: ArchVSpace progress

Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/invariant-abstract/AARCH64/ArchAcc_AI.thy

@@ -165,13 +165,16 @@ lemma is_ko_to_discs:
   apply (all \<open>rule ext, simp add: is_ep_def is_ntfn_def is_tcb_def split: kernel_object.splits\<close>)
   done
 
-lemma cap_to_pt_is_pt_cap:
+locale_abbrev cap_pt_type :: "cap \<Rightarrow> pt_type" where
-  "\<lbrakk> obj_refs cap = {p}; caps_of_state s cptr = Some cap; pts_of s p \<noteq> None;
+  "cap_pt_type cap \<equiv> acap_pt_type (the_arch_cap cap)"
+
+lemma cap_to_pt_is_pt_cap_and_type:
+  "\<lbrakk> obj_refs cap = {p}; caps_of_state s cptr = Some cap; pts_of s p = Some pt;
      valid_caps (caps_of_state s) s \<rbrakk>
-   \<Longrightarrow> is_pt_cap cap"
+   \<Longrightarrow> is_pt_cap cap \<and> cap_pt_type cap = pt_type pt"
   by (drule (1) valid_capsD)
      (auto simp: pts_of_ko_at is_pt_cap_def arch_cap_fun_lift_def arch_cap.disc_eq_case(4)
-                 valid_cap_def obj_at_def is_ko_to_discs is_cap_table_def
+                 valid_cap_def obj_at_def is_ko_to_discs is_cap_table_def the_arch_cap_def
            split: if_splits arch_cap.split cap.splits option.splits)
 
 lemma unique_vs_lookup_table:
@@ -194,7 +197,7 @@ lemma unique_vs_lookup_table:
   apply simp
   apply (subgoal_tac "is_pt_cap cap \<and> is_pt_cap cap'")
    prefer 2
-   apply (simp add: cap_to_pt_is_pt_cap)
+   apply (simp add: cap_to_pt_is_pt_cap_and_type)
   apply (drule (2) unique_table_refsD, simp)
   apply (drule table_cap_ref_vs_cap_ref; simp)
   done
@@ -813,8 +816,8 @@ lemma set_asid_pool_dom[wp]:
      (auto simp: dom_def opt_map_def obj_at_def is_ArchObj_def
            split: option.splits elim!: rsubst[where P=P])
 
-lemma set_asid_pool_None_valid_asid_table[wp]:
+lemma set_asid_pool_valid_asid_table[wp]:
-  "set_asid_pool p (ap (asid_low := None)) \<lbrace>valid_asid_table\<rbrace>"
+  "set_asid_pool p ap \<lbrace>valid_asid_table\<rbrace>"
   unfolding valid_asid_table_def
   using set_asid_pool_asid_pools_of[wp del]
   by (wp_pre, wps, wp, clarsimp)
@@ -2870,7 +2873,9 @@ crunches do_machine_op
   and pspace_in_kernel_window[wp]: pspace_in_kernel_window
   and cap_refs_in_kernel_window[wp]: cap_refs_in_kernel_window
   and vspace_at_asid[wp]: "\<lambda>s. P (vspace_at_asid a pt s)"
-  (simp: valid_kernel_mappings_def)
+  and valid_vs_lookup[wp]: "valid_vs_lookup"
+  and valid_obj[wp]: "valid_obj t obj"
+  (simp: valid_kernel_mappings_def wp: valid_obj_typ)
 
 lemma dmo_invs_lift:
   assumes dev: "\<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>"

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1489,7 +1489,7 @@ lemma decode_fr_inv_map_wf[wp]:
    apply (drule valid_vs_lookupD; clarsimp simp: vmsz_aligned_vref_for_level)
    apply (subgoal_tac "is_pt_cap cap")
     apply (force simp: is_cap_simps)
-   apply (fastforce dest: cap_to_pt_is_pt_cap intro: valid_objs_caps)
+   apply (fastforce dest: cap_to_pt_is_pt_cap_and_type intro: valid_objs_caps)
   apply (rule strengthen_imp_same_first_conj[OF conjI])
    apply (rule_tac x=level in exI)
    apply (rule_tac x="args!0" in exI)
@@ -1516,7 +1516,7 @@ lemma decode_fr_inv_map_wf[wp]:
   apply (drule valid_vs_lookupD; clarsimp simp: vmsz_aligned_vref_for_level)
   apply (subgoal_tac "is_pt_cap cap")
    apply (force simp: is_cap_simps)
-  apply (fastforce dest: cap_to_pt_is_pt_cap intro: valid_objs_caps)
+  apply (fastforce dest: cap_to_pt_is_pt_cap_and_type intro: valid_objs_caps)
   done *)
 
 lemma decode_frame_invocation_wf[wp]:

proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy

@@ -60,9 +60,6 @@ definition
   "reachable_frame_cap cap \<equiv> \<lambda>s.
      is_frame_cap cap \<and> (\<exists>ref. vs_cap_ref cap = Some ref \<and> reachable_target ref (obj_ref_of cap) s)"
 
-abbreviation
-  "cap_pt_type cap \<equiv> acap_pt_type (the_arch_cap cap)"
-
 (* The conditions under which it is legal to immediately replace an arch_cap
    cap with newcap at slot sl, assuming cap is final. *)
 definition

proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

@@ -319,8 +319,11 @@ definition wellformed_pte :: "pte \<Rightarrow> bool" where
 definition valid_vcpu :: "vcpu \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
   "valid_vcpu vcpu \<equiv> case_option \<top> (typ_at ATCB) (vcpu_tcb vcpu) "
 
+(* Since the page tables may translate more bits than the IPA address space has, not all mapping
+   slots in the top level table can be used. Slots with any of the top "pt_bits_left asid_pool_level
+   - ipa_size" bits set correspond to mappings outside of the address space. *)
 definition valid_vs_slot_bits :: nat where
-  "valid_vs_slot_bits = pt_bits_left asid_pool_level - ipa_size"
+  "valid_vs_slot_bits = ptTranslationBits VSRootPT_T - (pt_bits_left asid_pool_level - ipa_size)"
 
 definition invalid_mapping_slots :: "vs_index set" where
   "invalid_mapping_slots \<equiv>

proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy

@@ -105,8 +105,6 @@ lemma pt_at_asid_unique2:
   "\<lbrakk> vspace_at_asid asid pt s; vspace_at_asid asid pt' s \<rbrakk> \<Longrightarrow> pt = pt'"
   by (clarsimp simp: vspace_at_asid_def)
 
-crunch valid_vs_lookup[wp]: do_machine_op "valid_vs_lookup" (* FIXME AARCH64: move to ArchAcc crunches *)
-
 lemmas ackInterrupt_irq_masks = no_irq[OF no_irq_ackInterrupt]
 
 lemma ucast_ucast_low_bits:
@@ -244,10 +242,6 @@ lemma set_vcpu_valid_objs[wp]:
   apply (wp set_object_valid_objs)
   done
 
-(* FIXME AARCH64: move to ArchAcc crunches *)
-lemma do_machine_op_valid_obj[wp]: "\<lbrace>valid_obj t obj\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_obj t obj\<rbrace>"
-  by (rule valid_obj_typ) wp
-
 lemma get_vcpu_valid[wp]: "\<lbrace>valid_objs\<rbrace> get_vcpu t \<lbrace>\<lambda>r. valid_obj t (ArchObj (VCPU r))\<rbrace>"
   apply (wpsimp simp: get_vcpu_def)
   apply (erule valid_objsE; simp add: in_omonad)
@@ -273,11 +267,10 @@ lemma valid_vcpu_typ_at:
    \<Longrightarrow> \<lbrace>valid_vcpu vcpu\<rbrace> F \<lbrace>\<lambda>r. valid_vcpu (P r vcpu )\<rbrace>"
   by (wpsimp simp: valid_vcpu_def split: option.splits)
 
-(* FIXME AARCH64 VCPU
 crunches vgic_update_lr, vcpu_write_reg, vcpu_save_reg, vcpu_disable, vcpu_restore,
           save_virt_timer, restore_virt_timer, vcpu_save, vcpu_switch, vcpu_save_reg_range
   for valid_objs[wp]: valid_objs
-  (ignore: vcpu_update simp: vcpu_update_def valid_vcpu_def wp: crunch_wps) *)
+  (ignore: vcpu_update simp: vcpu_update_def valid_vcpu_def wp: crunch_wps)
 
 (* FIXME AARCH64: set up [simp] centrally properly for a_type *)
 lemma a_type_VCPU [simp]:
@@ -646,13 +639,6 @@ lemma store_vmid_valid_vspace_objs[wp]:
   unfolding store_vmid_def
   by wpsimp
 
-(* FIXME AARCH64: move, replace set_asid_pool_None_valid_asid_table *)
-lemma set_asid_pool_valid_asid_table[wp]:
-  "set_asid_pool p ap \<lbrace>valid_asid_table\<rbrace>"
-  unfolding valid_asid_table_def
-  using set_asid_pool_asid_pools_of[wp del]
-  by (wp_pre, wps, wp, clarsimp)
-
 lemma valid_global_arch_objs_upd_eq_lift:
   "(\<And>s. arm_us_global_vspace (f s) = arm_us_global_vspace s) \<Longrightarrow>
    valid_global_arch_objs (s\<lparr>arch_state := f (arch_state s)\<rparr>) = valid_global_arch_objs s"
@@ -793,7 +779,7 @@ lemma update_asid_pool_entry_vs_lookup_pages_vmid[wp]:
    \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace>"
   by (wpsimp wp: vs_lookup_pages_target_lift[OF update_asid_pool_entry_valid_vs_lookup_target])
 
-crunches update_asid_pool_entry, find_free_vmid
+crunches update_asid_pool_entry, find_free_vmid, store_vmid
   for if_live[wp]: if_live_then_nonz_cap
   and zombies_final[wp]: zombies_final
   and state_refs[wp]: "\<lambda>s. P (state_refs_of s)"
@@ -813,7 +799,7 @@ crunches update_asid_pool_entry, find_free_vmid
   and cap_refs_in_kernel_window[wp]: cap_refs_in_kernel_window
   (simp: valid_global_objs_def)
 
-crunches invalidate_asid, find_free_vmid
+crunches invalidate_asid, find_free_vmid, store_vmid
   for valid_machine_state[wp]: valid_machine_state
   and pspace_respects_device_region[wp]: pspace_respects_device_region
   and cap_refs_respects_device_region[wp]: cap_refs_respects_device_region
@@ -822,7 +808,7 @@ crunches invalidate_asid, find_free_vmid
    wp: pspace_respects_device_region_dmo cap_refs_respects_device_region_dmo
        dmo_valid_irq_states)
 
-crunches invalidate_asid, find_free_vmid
+crunches invalidate_asid, find_free_vmid, store_vmid
   for vs_lookup_pages[wp]: "\<lambda>s. P (vs_lookup_pages s)"
   (ignore: update_asid_pool_entry)
 
@@ -866,12 +852,25 @@ lemma find_free_vmid_invs[wp]:
              simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def
                    valid_global_vspace_mappings_def)
 
-lemma store_hw_asid_valid_arch:
+lemma store_hw_asid_valid_arch[wp]:
   "\<lbrace>valid_arch_state and (\<lambda>s. asid_map s asid = None \<and> arm_vmid_table (arch_state s) vmid = None)\<rbrace>
    store_vmid asid vmid
    \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
-  unfolding store_vmid_def
+  unfolding store_vmid_def valid_arch_state_def vmid_inv_def
-  sorry (* FIXME AARCH64 *)
+  supply fun_upd_apply[simp del]
+  apply (wpsimp simp: valid_global_arch_objs_upd_eq_lift | wps)+
+  apply (fastforce simp: vmid_for_asid_upd_eq elim: is_inv_Some_upd)
+  done
+
+lemma store_vmid_invs[wp]:
+  "\<lbrace>invs and (\<lambda>s. asid_map s asid = None \<and> arm_vmid_table (arch_state s) vmid = None)\<rbrace>
+   store_vmid asid vmid
+   \<lbrace>\<lambda>_. invs\<rbrace>"
+  unfolding invs_def valid_state_def valid_pspace_def
+  by (wpsimp wp: valid_irq_node_typ valid_irq_handlers_lift valid_arch_caps_lift
+                 pspace_in_kernel_window_atyp_lift_strong
+             simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def
+                   valid_global_vspace_mappings_def)
 
 lemma invalidate_vmid_entry_None[wp]:
   "\<lbrace>\<top>\<rbrace> invalidate_vmid_entry vmid \<lbrace>\<lambda>_ s. arm_vmid_table (arch_state s) vmid = None\<rbrace>"
@@ -883,19 +882,29 @@ lemma find_free_vmid_None[wp]:
   unfolding find_free_vmid_def
   by wpsimp (clarsimp dest!: findSomeD)
 
+lemma invalidate_vmid_entry_vmid_for_asid_None[wp]:
+  "invalidate_vmid_entry vmid \<lbrace>\<lambda>s. vmid_for_asid s asid = None\<rbrace>"
+  unfolding invalidate_vmid_entry_def
+  by wpsimp
+
+lemma invalidate_asid_vmid_for_asid_None[wp]:
+  "invalidate_asid asid' \<lbrace>\<lambda>s. vmid_for_asid s asid = None\<rbrace>"
+  unfolding invalidate_asid_def update_asid_pool_entry_def
+  supply fun_upd_apply[simp del]
+  apply (wpsimp|wps)+
+  apply (auto simp: vmid_for_asid_def entry_for_pool_def fun_upd_apply obind_def in_opt_map_None_eq
+              split: option.split)
+  done
+
 lemma find_free_vmid_None_asid_map[wp]:
   "find_free_vmid \<lbrace>\<lambda>s. asid_map s asid = None\<rbrace>"
-  sorry (* FIXME AARCH64 *)
+  unfolding find_free_vmid_def
+  by wpsimp
 
 lemma get_hw_asid_valid_arch[wp]:
   "get_vmid asid \<lbrace>valid_arch_state\<rbrace>"
-  sorry (* FIXME AARCH64 *)
+  unfolding get_vmid_def
-
+  by wpsimp
-lemma store_vmid_invs:
-  "\<lbrace>invs and (\<lambda>s. asid_map s asid = None \<and> arm_vmid_table (arch_state s) vmid = None)\<rbrace>
-   store_vmid asid vmid
-   \<lbrace>\<lambda>x. invs\<rbrace>"
-  sorry (* FIXME AARCH64 *)
 
 lemma get_hw_asid_invs[wp]:
   "get_vmid asid \<lbrace>invs\<rbrace>"
@@ -922,11 +931,15 @@ crunches set_vm_root
   for typ_at[wp]: "\<lambda>s. P (typ_at T p s)"
   (simp: crunch_simps)
 
+lemma set_global_user_vspace_invs[wp]:
+  "set_global_user_vspace \<lbrace>invs\<rbrace>"
+  unfolding set_global_user_vspace_def
+  by wpsimp
+
 lemma set_vm_root_invs[wp]:
   "set_vm_root t \<lbrace>invs\<rbrace>"
   unfolding set_vm_root_def
-  sorry (* FIXME AARCH64
+  by (wpsimp simp: if_distribR wp: get_cap_wp)
-  by (wpsimp simp: if_distribR wp: get_cap_wp) *)
 
 crunch pred_tcb_at[wp]: set_vm_root "pred_tcb_at proj P t"
   (simp: crunch_simps)
@@ -1043,9 +1056,8 @@ lemma arch_update_cap_invs_map:
   apply (thin_tac "cap_range a = cap_range b" for a b)
   apply (rule conjI)
    apply (clarsimp simp: is_valid_vtable_root_def vs_cap_ref_def vs_cap_ref_arch_def split: cap.splits)
-   apply (simp split: arch_cap.splits option.splits;
+   apply (simp split: arch_cap.splits option.splits pt_type.splits;
           clarsimp simp: cap_master_cap_simps vs_cap_ref_arch_def)
-  sorry (* FIXME AARCH64
   apply (rule conjI)
    apply (rule ext)
    apply (simp add: cap_master_cap_def split: cap.splits arch_cap.splits)
@@ -1100,7 +1112,7 @@ lemma arch_update_cap_invs_map:
                  elim!: ranE cong: master_cap_eq_is_device_cap_eq
              | rule conjI)+
   apply (clarsimp dest!: master_cap_eq_is_device_cap_eq)
-  done *)
+  done
 
 lemma pool_for_asid_ap_at:
   "\<lbrakk> pool_for_asid asid s = Some p; valid_arch_state s \<rbrakk> \<Longrightarrow> asid_pool_at p s"
@@ -1239,10 +1251,6 @@ lemma not_in_global_refs_vs_lookup:
   apply (simp add: cap_range_def)
   done
 
-(* FIXME AARCH64: different machine ops here
-lemma no_irq_sfence[wp,intro!]: "no_irq sfence"
-  by (wpsimp simp: sfence_def no_irq_def machine_op_lift_def machine_rest_lift_def) *)
-
 lemma pt_lookup_from_level_wp:
   "\<lbrace>\<lambda>s. (\<forall>level pt' pte.
             pt_walk top_level level top_level_pt vref (ptes_of s) = Some (level, pt') \<longrightarrow>
@@ -1311,21 +1319,25 @@ lemma reachable_page_table_not_global:
   apply assumption
   done
 
+lemma user_region_invalid_mapping_slots:
+  "vref \<in> user_region \<Longrightarrow> ucast (pt_index max_pt_level vref) \<notin> invalid_mapping_slots"
+  unfolding user_region_def pt_index_def invalid_mapping_slots_def canonical_user_def
+  apply (clarsimp split: if_split_asm)
+  apply (rule ucast_le_maskI)
+  apply (clarsimp simp: valid_vs_slot_bits_def bit_simps word_and_le1 split: if_split_asm)
+  apply (simp add: pt_bits_left_def bit_simps size_max_pt_level)
+  apply (rule order_trans, rule word_and_le2)
+  apply (rule leq_mask_shift)
+  apply simp
+  done
+
 lemma unmap_page_table_invs[wp]:
   "\<lbrace>invs and K (vaddr \<in> user_region)\<rbrace>
      unmap_page_table asid vaddr pt
    \<lbrace>\<lambda>rv. invs\<rbrace>"
-  apply (simp add: unmap_page_table_def)
+  unfolding unmap_page_table_def
-  apply (rule hoare_pre)
+  apply (wpsimp wp: invalidate_tlb_by_asid_invs dmo_invs_lift store_pte_invs_unmap
-   apply (wp dmo_invs | wpc | simp)+
+                    pt_lookup_from_level_wp)
-     apply (rule_tac Q="\<lambda>_. invs" in hoare_post_imp)
-      apply safe
-  sorry (* FIXME AARCH64
-       apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p =
-                                  underlying_memory m p" in use_valid)
-         apply ((wp | simp)+)[3]
-      apply(erule use_valid, wp no_irq, assumption)
-     apply (wpsimp wp: store_pte_invs_unmap pt_lookup_from_level_wp)+
   apply (frule pt_walk_max_level)
   apply (drule (2) pt_lookup_vs_lookupI)
   apply (frule (2) valid_vspace_objs_strongD[rotated]; clarsimp)
@@ -1334,15 +1346,16 @@ lemma unmap_page_table_invs[wp]:
    apply (drule (1) vs_lookup_table_target)
    apply (drule valid_vs_lookupD, erule vref_for_level_user_region, clarsimp)
    apply clarsimp
-   apply (frule (1) cap_to_pt_is_pt_cap; clarsimp?)
+   apply (frule (1) cap_to_pt_is_pt_cap_and_type; clarsimp?)
+     apply fastforce
     apply (fastforce intro: valid_objs_caps)
    apply (fastforce simp: is_cap_simps)
   apply (rule conjI; clarsimp?)
    apply (drule (3) vs_lookup_table_vspace)
-   apply (simp add: table_index_max_level_slots)
+   apply (simp add: user_region_invalid_mapping_slots)
   apply (drule (1) vs_lookup_table_target)
   apply (drule vs_lookup_target_not_global, erule vref_for_level_user_region; simp)
-  done *)
+  done
 
 lemma final_cap_lift:
   assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
@@ -1718,7 +1731,7 @@ lemma perform_pt_inv_unmap_invs[wp]:
     apply (simp add: cap_range_def)
    apply (frule vspace_for_asid_target)
    apply (drule valid_vs_lookupD; clarsimp)
-   apply (frule (1) cap_to_pt_is_pt_cap, clarsimp simp: in_omonad obj_at_def)
+   apply (frule (1) cap_to_pt_is_pt_cap_and_type, clarsimp simp: in_omonad obj_at_def)
     apply (fastforce intro: valid_objs_caps)
    apply (drule (1) unique_table_refsD[rotated]; clarsimp)
    apply (clarsimp simp: is_cap_simps)
@@ -1773,14 +1786,14 @@ lemma perform_pt_inv_map_invs[wp]:
    apply clarsimp
    apply (drule (1) vs_lookup_table_target)
    apply (drule valid_vs_lookupD, erule vref_for_level_user_region; clarsimp)
-   apply (frule (1) cap_to_pt_is_pt_cap, simp, fastforce intro: valid_objs_caps)
+   apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp, fastforce intro: valid_objs_caps)
    apply (clarsimp simp: is_cap_simps)
    apply (drule (1) unique_table_refsD[rotated]; clarsimp)
   apply (rule conjI, clarsimp)
    apply (frule (2) valid_vspace_objs_strongD[rotated]; clarsimp)
    apply (drule (1) vs_lookup_table_target)
    apply (drule valid_vs_lookupD, erule vref_for_level_user_region; clarsimp)
-   apply (frule (1) cap_to_pt_is_pt_cap, simp, fastforce intro: valid_objs_caps)
+   apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp, fastforce intro: valid_objs_caps)
    apply (clarsimp simp: is_cap_simps)
    apply (thin_tac "caps_of_state s ct_slot = Some cap" for cap)
    apply (drule (1) unique_table_refsD[rotated]; clarsimp)
@@ -1799,7 +1812,7 @@ lemma perform_pt_inv_map_invs[wp]:
   apply (rule conjI, clarsimp) (* p \<noteq> pt_ptr *)
    apply (drule (1) vs_lookup_table_target)
    apply (drule valid_vs_lookupD, erule vref_for_level_user_region; clarsimp)
-   apply (frule (1) cap_to_pt_is_pt_cap, simp, fastforce intro: valid_objs_caps)
+   apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp, fastforce intro: valid_objs_caps)
    apply (clarsimp simp: is_cap_simps)
    apply (drule (1) unique_table_refsD[rotated]; clarsimp)
   apply (frule pt_slot_offset_vref_for_level; simp)
@@ -1834,7 +1847,7 @@ lemma pt_lookup_slot_cap_to:
   apply (frule_tac level=level in valid_vspace_objs_strongD[rotated]; clarsimp)
   apply (drule vs_lookup_table_target[where level=level], simp)
   apply (drule valid_vs_lookupD, erule vref_for_level_user_region; clarsimp)
-  apply (frule (1) cap_to_pt_is_pt_cap, simp)
+  apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp)
    apply (fastforce intro: valid_objs_caps)
   apply (frule pts_of_Some_alignedD, fastforce)
   apply (frule caps_of_state_valid, fastforce)
@@ -1853,9 +1866,9 @@ lemma find_vspace_for_asid_cap_to:
   apply simp
   apply (drule vs_lookup_table_target, simp)
   apply (drule valid_vs_lookupD; clarsimp simp: vref_for_level_def)
-  apply (frule (1) cap_to_pt_is_pt_cap, simp)
+  apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp)
    apply (fastforce intro: valid_objs_caps)
-  apply (fastforce intro: caps_of_state_valid cap_to_pt_is_pt_cap)
+  apply (fastforce intro: caps_of_state_valid cap_to_pt_is_pt_cap_and_type)
   done
 
 lemma ex_pt_cap_eq:
@@ -1886,7 +1899,7 @@ lemma unmap_page_invs:
   apply (frule (2) vs_lookup_target_not_global)
   apply simp
   apply (frule (1) valid_vs_lookupD; clarsimp)
-  apply (frule (1) cap_to_pt_is_pt_cap; (clarsimp intro!: valid_objs_caps)?)
+  apply (frule (1) cap_to_pt_is_pt_cap_and_type; (clarsimp intro!: valid_objs_caps)?)
   apply (rule conjI, fastforce simp: is_cap_simps)
   apply clarsimp
   apply (drule (3) vs_lookup_table_vspace)
@@ -2470,7 +2483,7 @@ lemma perform_asid_pool_invs [wp]:
   apply (clarsimp simp: cap_range_def)
   apply (rule conjI, clarsimp)
    apply (drule (1) vs_lookup_table_valid_cap; clarsimp)
-   apply (frule (1) cap_to_pt_is_pt_cap, simp, fastforce intro: valid_objs_caps)
+   apply (frule (1) cap_to_pt_is_pt_cap_and_type, simp, fastforce intro: valid_objs_caps)
    apply (drule (1) unique_table_refsD[rotated]; clarsimp)
    apply (clarsimp simp: is_cap_simps)
   apply (rule conjI, clarsimp)