Update ARM and AARCH64 AInvs for explicit FPU changes

proof/access-control/ARM/ArchDomainSepInv.thy

@@ -13,7 +13,8 @@ context Arch begin global_naming ARM_A
 
 named_theorems DomainSepInv_assms
 
-crunch arch_post_cap_deletion, set_pd, set_pt, set_asid_pool, prepare_thread_delete, init_arch_objects
+crunch
+  arch_post_cap_deletion, set_pd, set_pt, set_asid_pool, prepare_thread_delete, init_arch_objects
   for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st"
   (wp: domain_sep_inv_triv crunch_wps set_asid_pool_cte_wp_at set_pd_cte_wp_at set_pt_cte_wp_at)
 
@@ -28,7 +29,8 @@ lemma arch_finalise_cap_rv[DomainSepInv_assms]:
 crunch
   invalidate_tlb_by_asid, handle_reserved_irq, handle_vm_fault,
   handle_hypervisor_fault, handle_arch_fault_reply, arch_mask_irq_signal,
-  arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread
+  arch_switch_to_thread, arch_switch_to_idle_thread, arch_activate_idle_thread,
+  arch_prepare_set_domain, arch_prepare_next_domain, arch_post_set_flags
   for domain_sep_inv[DomainSepInv_assms, wp]: "domain_sep_inv irqs st"
 
 lemma arch_derive_cap_domain_sep_inv[DomainSepInv_assms, wp]:

proof/access-control/ARM/ArchIpc_AC.thy

@@ -12,7 +12,7 @@ context Arch begin global_naming ARM_A
 
 named_theorems Ipc_AC_assms
 
-declare make_fault_message_inv[Ipc_AC_assms]
+declare make_fault_msg_inv[Ipc_AC_assms]
 declare handle_arch_fault_reply_typ_at[Ipc_AC_assms]
 
 crunch cap_insert_ext

proof/access-control/ARM/ArchSyscall_AC.thy

@@ -61,7 +61,7 @@ crunch handle_vm_fault
   for pas_refined[Syscall_AC_assms, wp]: "pas_refined aag"
   and cur_thread[Syscall_AC_assms, wp]: "\<lambda>s. P (cur_thread s)"
   and state_refs_of[Syscall_AC_assms, wp]: "\<lambda>s. P (state_refs_of s)"
-  (wp: as_user_getRestart_invs ignore: as_user)
+  (wp: as_user_getRestart_inv ignore: as_user)
 
 lemma handle_vm_fault_integrity[Syscall_AC_assms]:
   "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace>
@@ -162,7 +162,8 @@ crunch arch_post_cap_deletion
 crunch
   arch_post_modify_registers, arch_invoke_irq_control,
   arch_invoke_irq_handler, arch_perform_invocation, arch_mask_irq_signal,
-  handle_reserved_irq, handle_vm_fault, handle_hypervisor_fault, handle_arch_fault_reply
+  handle_reserved_irq, handle_vm_fault, handle_hypervisor_fault, handle_arch_fault_reply,
+  arch_prepare_set_domain, arch_post_set_flags, arch_prepare_next_domain
   for cur_thread[Syscall_AC_assms, wp]: "\<lambda>s. P (cur_thread s)"
   and idle_thread[Syscall_AC_assms, wp]: "\<lambda>s. P (idle_thread s)"
   and cur_domain[Syscall_AC_assms, wp]:  "\<lambda>s. P (cur_domain s)"
@@ -171,6 +172,15 @@ crunch
 \<comment> \<open>These aren't proved in the previous crunch, and hence need to be declared\<close>
 declare handle_arch_fault_reply_cur_thread[Syscall_AC_assms]
 declare handle_arch_fault_reply_it[Syscall_AC_assms]
+declare arch_prepare_set_domain_idle_thread[Syscall_AC_assms]
+
+crunch arch_prepare_next_domain
+  for pas_refined[Syscall_AC_assms, wp]: "pas_refined aag"
+  and integrity[Syscall_AC_assms, wp]: "integrity aag X st"
+  and ct_not_in_q[Syscall_AC_assms, wp]: ct_not_in_q
+  and valid_sched_action[Syscall_AC_assms, wp]: valid_sched_action
+  and ct_in_cur_domain[Syscall_AC_assms, wp]: ct_in_cur_domain
+  and valid_idle_etcb[Syscall_AC_assms, wp]: valid_idle_etcb
 
 end
 

proof/access-control/ARM/ArchTcb_AC.thy

@@ -14,7 +14,7 @@ named_theorems Tcb_AC_assms
 
 declare arch_get_sanitise_register_info_inv[Tcb_AC_assms]
 
-crunch arch_post_modify_registers
+crunch arch_post_modify_registers, arch_post_set_flags
   for pas_refined[Tcb_AC_assms, wp]: "pas_refined aag"
 
 lemma arch_post_modify_registers_respects[Tcb_AC_assms]:
@@ -23,6 +23,12 @@ lemma arch_post_modify_registers_respects[Tcb_AC_assms]:
    \<lbrace>\<lambda>_ s. integrity aag X st s\<rbrace>"
   by wpsimp
 
+lemma arch_post_set_flags_respects[Tcb_AC_assms]:
+  "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
+   arch_post_set_flags t flags
+   \<lbrace>\<lambda>_ s. integrity aag X st s\<rbrace>"
+  by (wpsimp simp: arch_post_set_flags_def)
+
 lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
   "\<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action
                        and tcb_inv_wf (ThreadControl t sl ep mcp priority croot vroot buf)

proof/access-control/ARM/ExampleSystem.thy

@@ -315,6 +315,7 @@ where
      tcb_priority           = undefined,
      tcb_time_slice         = undefined,
      tcb_domain             = 0,
+     tcb_flags              = undefined,
      tcb_arch               = \<lparr>tcb_context = undefined\<rparr> \<rparr>"
 
 
@@ -339,6 +340,7 @@ where
      tcb_priority           = undefined,
      tcb_time_slice         = undefined,
      tcb_domain             = 0,
+     tcb_flags              = undefined,
      tcb_arch               = \<lparr>tcb_context = undefined\<rparr>\<rparr>"
 
 definition
@@ -869,6 +871,7 @@ where
      tcb_priority           = undefined,
      tcb_time_slice         = undefined,
      tcb_domain             = 0,
+     tcb_flags              = undefined,
      tcb_arch          = \<lparr>tcb_context = undefined\<rparr>\<rparr>"
 
 
@@ -893,6 +896,7 @@ where
      tcb_priority           = undefined,
      tcb_time_slice         = undefined,
      tcb_domain             = 0,
+     tcb_flags              = undefined,
      tcb_arch               = \<lparr>tcb_context = undefined\<rparr>\<rparr>"
 
 (* the boolean in BlockedOnReceive is True if the object can receive but not send.

proof/access-control/DomainSepInv.thy

@@ -325,6 +325,12 @@ locale DomainSepInv_1 =
     "\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv s :: det_ext state. domain_sep_inv_cap irqs rv\<rbrace>,-"
   and arch_post_modify_registers_domain_sep_inv[wp]:
     "arch_post_modify_registers cur t \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
+  and arch_prepare_set_domain_domain_sep_inv[wp]:
+    "arch_prepare_set_domain t new_dom \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
+  and arch_prepare_next_domain_domain_sep_inv[wp]:
+    "arch_prepare_next_domain \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
+  and arch_post_set_flags_domain_sep_inv[wp]:
+    "arch_post_set_flags t flags \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
   and handle_arch_fault_reply_domain_sep_inv[wp]:
     "handle_arch_fault_reply vmf thread d ds \<lbrace>\<lambda>s :: det_ext state. domain_sep_inv irqs st s\<rbrace>"
   and handle_vm_fault_domain_sep_inv[wp]:
@@ -429,6 +435,8 @@ lemmas thread_set_tcb_domain_update_domain_sep_inv[wp]
   = thread_set_domain_sep_inv_triv[where f="tcb_domain_update f" for f, simplified ran_tcb_cap_cases, simplified]
 lemmas thread_set_tcb_registers_caps_merge_default_tcb_domain_sep_inv[wp]
   = thread_set_domain_sep_inv_triv[where f="tcb_registers_caps_merge tcb" for tcb, simplified ran_tcb_cap_cases tcb_registers_caps_merge_def, simplified]
+lemmas thread_set_tcb_flags_update_domain_sep_inv[wp]
+  = thread_set_domain_sep_inv_triv[where f="tcb_flags_update f" for f, simplified ran_tcb_cap_cases, simplified]
 
 crunch as_user
   for domain_sep_inv[wp]: "domain_sep_inv irqs st"
@@ -877,13 +885,17 @@ lemma checked_cap_insert_domain_sep_inv:
   apply (erule (1) same_object_as_domain_sep_inv_cap)
   done
 
-crunch bind_notification, set_mcpriority, set_priority, invoke_domain
+crunch bind_notification, set_mcpriority, set_priority
   for domain_sep_inv[wp]: "domain_sep_inv irqs st"
   (ignore: thread_set)
 
 
 context DomainSepInv_1 begin
 
+crunch invoke_domain, set_flags
+  for domain_sep_inv[wp]: "domain_sep_inv irqs (st :: 'state_ext state) :: det_ext state \<Rightarrow> _"
+  (ignore: thread_set)
+
 lemma invoke_tcb_domain_sep_inv:
   "\<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace>
    invoke_tcb tinv

proof/access-control/Syscall_AC.thy

@@ -521,6 +521,30 @@ locale Syscall_AC_1 =
               set_thread_state thread Structures_A.thread_state.Running
      od
      \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
+  and arch_prepare_next_domain_respects[wp]:
+    "arch_prepare_next_domain \<lbrace>integrity aag X st\<rbrace>"
+  assumes arch_prepare_next_domain_pas_refined[wp]:
+    "arch_prepare_next_domain \<lbrace>pas_refined aag\<rbrace>"
+  assumes arch_prepare_next_domain_ct_not_in_q[wp]:
+    "arch_prepare_next_domain \<lbrace>ct_not_in_q :: det_state \<Rightarrow> _\<rbrace>"
+  assumes arch_prepare_next_domain_valid_sched_action[wp]:
+    "arch_prepare_next_domain \<lbrace>valid_sched_action :: det_state \<Rightarrow> _\<rbrace>"
+  assumes arch_prepare_next_domain_ct_in_cur_domain[wp]:
+    "arch_prepare_next_domain \<lbrace>ct_in_cur_domain :: det_state \<Rightarrow> _\<rbrace>"
+  assumes arch_prepare_next_domain_valid_idle_etcb[wp]:
+    "arch_prepare_next_domain \<lbrace>valid_idle_etcb :: det_state \<Rightarrow> _\<rbrace>"
+  assumes arch_prepare_set_domain_cur_thread[wp]:
+    "\<And>P. arch_prepare_set_domain t new_dom \<lbrace>\<lambda>s :: det_state. P (cur_thread s)\<rbrace>"
+  assumes arch_post_set_flags_cur_thread[wp]:
+    "\<And>P. arch_post_set_flags t flags \<lbrace>\<lambda>s :: det_state. P (cur_thread s)\<rbrace>"
+  assumes arch_prepare_set_domain_idle_thread[wp]:
+    "\<And>P. arch_prepare_set_domain t new_dom \<lbrace>\<lambda>s :: det_state. P (idle_thread s)\<rbrace>"
+  assumes arch_post_set_flags_idle_thread[wp]:
+    "\<And>P. arch_post_set_flags t flags \<lbrace>\<lambda>s :: det_state. P (idle_thread s)\<rbrace>"
+  assumes arch_prepare_set_domain_cur_domain[wp]:
+    "\<And>P. arch_prepare_set_domain t new_dom \<lbrace>\<lambda>s :: det_state. P (cur_domain s)\<rbrace>"
+  assumes arch_post_set_flags_cur_domain[wp]:
+    "\<And>P. arch_post_set_flags t flags \<lbrace>\<lambda>s :: det_state. P (cur_domain s)\<rbrace>"
 
 
 sublocale Syscall_AC_1 \<subseteq> prepare_thread_delete: gpd_wps' "prepare_thread_delete p"

proof/access-control/Tcb_AC.thy

@@ -25,7 +25,8 @@ definition authorised_tcb_inv :: "'a PAS \<Rightarrow> tcb_invocation \<Rightarr
   | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src
   | WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest
   | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest
-  | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb"
+  | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb
+  | SetFlags tcb clearFlags setFlags \<Rightarrow> is_subject aag tcb"
 
 subsection\<open>invoke\<close>
 
@@ -288,6 +289,12 @@ locale Tcb_AC_1 =
     "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
      arch_post_modify_registers cur t
      \<lbrace>\<lambda>_ s. integrity aag X st s\<rbrace>"
+  and arch_post_set_flags_respects[wp]:
+    "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace>
+     arch_post_set_flags t flags
+     \<lbrace>\<lambda>_ s. integrity aag X st s\<rbrace>"
+  assumes arch_post_set_flags_pas_refined[wp]:
+    "arch_post_set_flags t flags \<lbrace>pas_refined aag\<rbrace>"
   and arch_get_sanitise_register_info_inv[wp]:
     "arch_get_sanitise_register_info t \<lbrace>\<lambda>s :: det_ext state. P s\<rbrace>"
   and invoke_tcb_tc_respects_aag:
@@ -298,6 +305,17 @@ locale Tcb_AC_1 =
      \<lbrace>\<lambda>rv. integrity aag X st and pas_refined aag\<rbrace>"
 begin
 
+crunch set_flags
+  for integrity_autarch[wp]: "integrity aag X st"
+
+lemma invoke_tcb_set_flags_respects[wp]:
+  "\<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action
+                       and tcb_inv_wf (SetFlags tcb clearFlags setFlags)
+                       and K (authorised_tcb_inv aag (SetFlags tcb clearFlags setFlags))\<rbrace>
+   invoke_tcb (SetFlags tcb clearFlags setFlags)
+   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
+  by (wpsimp simp: authorised_tcb_inv_def)
+
 lemma invoke_tcb_respects:
   "\<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action
                        and tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\<rbrace>
@@ -346,6 +364,16 @@ lemma invoke_tcb_ntfn_control_pas_refined[wp]:
 
 context Tcb_AC_1 begin
 
+crunch set_flags
+  for pas_refined[wp]: "pas_refined aag"
+
+lemma invoke_tcb_set_flags_pas_refined[wp]:
+  "\<lbrace>pas_refined aag and tcb_inv_wf (SetFlags tcb clearFlags setFlags) and einvs and simple_sched_action
+                    and K (authorised_tcb_inv aag (SetFlags tcb clearFlags setFlags))\<rbrace>
+   invoke_tcb (SetFlags tcb clearFlags setFlags)
+   \<lbrace>\<lambda>_. pas_refined aag \<rbrace>"
+  by wpsimp
+
 lemma invoke_tcb_pas_refined:
   "\<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action
                     and K (authorised_tcb_inv aag ti)\<rbrace>
@@ -512,6 +540,14 @@ lemma decode_set_tls_base_authorised:
   apply (wpsimp wp: gbn_wp)
   done
 
+lemma decode_set_flags_authorised:
+  "\<lbrace>K (is_subject aag t)\<rbrace>
+   decode_set_flags args (ThreadCap t)
+   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -"
+  unfolding decode_set_flags_def authorised_tcb_inv_def
+  apply wpsimp
+  done
+
 lemma decode_tcb_invocation_authorised:
   "\<lbrace>invs and pas_refined aag
          and K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x)))
@@ -527,7 +563,7 @@ lemma decode_tcb_invocation_authorised:
             decode_set_ipc_buffer_authorised decode_set_space_authorised
             decode_bind_notification_authorised
             decode_unbind_notification_authorised
-            decode_set_tls_base_authorised)+
+            decode_set_tls_base_authorised decode_set_flags_authorised)+
   by (auto iff: authorised_tcb_inv_def)
 
 text\<open>

proof/invariant-abstract/AARCH64/ArchAcc_AI.thy

@@ -1583,6 +1583,11 @@ lemma set_asid_pool_iflive [wp]:
   by (wp set_object_iflive)
      (clarsimp simp: obj_at_def live_def hyp_live_def arch_live_def in_omonad)
 
+lemma set_asid_pool_nonz_cap_to[wp]:
+  "set_asid_pool p ap \<lbrace>ex_nonz_cap_to t\<rbrace>"
+  unfolding set_asid_pool_def
+  by (wpsimp simp: in_omonad obj_at_def)
+
 lemma set_asid_pool_zombies [wp]:
   "set_asid_pool p ap \<lbrace>zombies_final\<rbrace>"
   unfolding set_asid_pool_def
@@ -1997,6 +2002,10 @@ lemma set_asid_pool_None_valid_asid_map[wp]:
   apply (fastforce simp: entry_for_pool_def obind_None_eq in_omonad split: if_split_asm)
   done
 
+crunch set_asid_pool
+  for valid_cur_fpu[wp]: valid_cur_fpu
+  (wp: valid_cur_fpu_lift)
+
 lemma set_asid_pool_invs_unmap:
   "\<lbrace>invs and
     (\<lambda>s. asid_pools_of s p = Some ap) and
@@ -2745,6 +2754,10 @@ lemma store_pte_valid_global_tables[wp]:
   unfolding store_pte_def valid_global_tables_2_def
   by (wpsimp wp: set_pt_pts_of simp: global_refs_def | wps)+
 
+crunch store_pte
+  for valid_cur_fpu[wp]: valid_cur_fpu
+  (wp: valid_cur_fpu_lift)
+
 lemma store_pte_invs:
   "\<lbrace> invs
      and (\<lambda>s. table_base pt_t p \<notin> global_refs s)
@@ -2830,6 +2843,7 @@ crunch do_machine_op
   and vspace_at_asid[wp]: "\<lambda>s. P (vspace_at_asid a pt s)"
   and valid_vs_lookup[wp]: "\<lambda>s. P (valid_vs_lookup s)"
   and valid_obj[wp]: "valid_obj t obj"
+  and valid_cur_fpu[wp]: valid_cur_fpu
   (simp: valid_kernel_mappings_def wp: valid_obj_typ)
 
 lemma dmo_invs_lift:

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1136,6 +1136,12 @@ lemma associate_vcpu_tcb_valid_objs[wp]:
                wp: arch_thread_get_wp
       | simp add: obj_at_def)+
 
+crunch associate_vcpu_tcb
+  for arm_current_fpu_owner[wp]: "\<lambda>s. P (arm_current_fpu_owner (arch_state s))"
+  and arch_tcb_cur_fpu[wp]: "\<lambda>s. P (arch_tcb_at itcb_cur_fpu p s)"
+  and valid_cur_fpu[wp]: valid_cur_fpu
+  (wp: valid_cur_fpu_lift_arch arch_thread_set_no_change_arch_tcb_at crunch_wps)
+
 lemma associate_vcpu_tcb_invs[wp]:
   "\<lbrace>invs and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb and vcpu_at vcpu and (\<lambda>s. tcb \<noteq> idle_thread s)\<rbrace>
    associate_vcpu_tcb vcpu tcb

proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy

@@ -29,7 +29,7 @@ crunch invoke_untyped
   for (bcorres) bcorres[wp]: truncate_state
   (ignore: sequence_x)
 
-crunch set_mcpriority, set_priority
+crunch set_mcpriority, set_priority, set_flags, arch_post_set_flags
   for (bcorres) bcorres[wp]: truncate_state
 
 crunch arch_get_sanitise_register_info, arch_post_modify_registers
@@ -71,7 +71,7 @@ lemma make_arch_fault_msg_bcorres[wp,BCorres2_AI_assms]:
   "bcorres (make_arch_fault_msg a b) (make_arch_fault_msg a b)"
   by (cases a; simp ; wp)
 
-lemma  handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
+lemma handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
   "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)"
   by (cases a; simp add: handle_arch_fault_reply_def; wp)
 
@@ -104,7 +104,7 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d
 crunch
   decode_set_ipc_buffer, decode_set_space, decode_set_priority,
   decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
-  decode_unbind_notification, decode_set_tls_base
+  decode_unbind_notification, decode_set_tls_base, decode_set_flags
   for (bcorres) bcorres[wp]: truncate_state
 
 lemma decode_tcb_configure_bcorres[wp]:

proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy

@@ -38,6 +38,11 @@ lemma pt_lookup_from_level_bcorres[wp]:
   "bcorres (pt_lookup_from_level l r b c) (pt_lookup_from_level l r b c)"
   by (induct l arbitrary: r b c rule: vm_level.minus_induct; wpsimp simp: pt_lookup_from_level_simps)
 
+\<comment> \<open>FIXME: move to BCorres_UL\<close>
+lemma maybeM_bcorres_underlying[wp]:
+  "\<lbrakk>\<And>x. y = Some x \<Longrightarrow> bcorres_underlying t (f x) (f' x)\<rbrakk> \<Longrightarrow> bcorres_underlying t (maybeM f y) (maybeM f' y)"
+  by (wpsimp simp: maybeM_def)
+
 crunch arch_finalise_cap
   for (bcorres) bcorres[wp]: truncate_state
 crunch prepare_thread_delete

proof/invariant-abstract/AARCH64/ArchBits_AI.thy

@@ -33,6 +33,10 @@ sublocale p_asid_table_current_vcpu_update:
   Arch_p_asid_table_update_eq "\<lambda>s. s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>"
   by (unfold_locales) auto
 
+sublocale p_asid_table_current_vcpu_update:
+  Arch_p_asid_table_update_eq "\<lambda>s. s\<lparr>arch_state := arm_current_fpu_owner_update f (arch_state s)\<rparr>"
+  by (unfold_locales) auto
+
 
 lemma invs_unique_table_caps[elim!]:
   "invs s \<Longrightarrow> unique_table_caps s"

proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy

@@ -522,7 +522,7 @@ lemma cap_swap_valid_arch_state[wp, CNodeInv_AI_assms]:
   "\<lbrace>valid_arch_state and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace>
    cap_swap c a c' b
    \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
-  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps cap_swap_aobj_at)
+  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps cap_swap_typ_ats cap_swap_aobj_at)
 
 end
 

proof/invariant-abstract/AARCH64/ArchCSpaceInv_AI.thy

@@ -16,7 +16,7 @@ context Arch begin arch_global_naming
 
 lemma set_cap_valid_arch_state[wp]:
   "set_cap cap ptr \<lbrace> valid_arch_state \<rbrace>"
-  by (wp valid_arch_state_lift_aobj_at_no_caps set_cap.aobj_at)
+  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps set_cap_tcb set_cap.aobj_at)
 
 lemma replace_cap_invs:
   "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s p cap) p s