diff --git a/proof/access-control/ARM/ArchIpc_AC.thy b/proof/access-control/ARM/ArchIpc_AC.thy
index 4f2b49cd9d..b7d2687f13 100644
--- a/proof/access-control/ARM/ArchIpc_AC.thy
+++ b/proof/access-control/ARM/ArchIpc_AC.thy
@@ -63,6 +63,10 @@ lemma tcb_context_no_change[Ipc_AC_assms]:
   apply (auto simp: arch_tcb_context_set_def)
   done
 
+lemma transfer_caps_loop_valid_arch[Ipc_AC_assms]:
+  "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps transfer_caps_loop_aobj_at)
+
 end
 
 
diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy
index 383935f0bf..b79309883c 100644
--- a/proof/access-control/CNode_AC.thy
+++ b/proof/access-control/CNode_AC.thy
@@ -8,6 +8,19 @@ theory CNode_AC
 imports ArchAccess_AC
 begin
 
+(* Note: exporting the following diverges from AInvs interfaces where valid_arch_state is
+   permitted to depend on caps (due to supporting x64). If x64 access control is to go ahead,
+   these will need more careful management. *)
+arch_requalify_facts
+  set_cap_valid_arch_state
+  cap_insert_simple_valid_arch_state
+
+lemmas [wp] = set_cap_valid_arch_state cap_insert_simple_valid_arch_state
+
+crunch set_untyped_cap_as_full
+  for valid_arch_state[wp]: valid_arch_state
+
+
 section\<open>CNode-specific AC.\<close>
 
 
@@ -33,7 +46,6 @@ crunch cap_swap_ext,cap_move_ext,empty_slot_ext
 crunch set_untyped_cap_as_full
   for integrity_autarch: "integrity aag X st"
 
-
 locale CNode_AC_1 =
   fixes aag :: "'a PAS"
   and val_t :: "'b"
@@ -1010,8 +1022,6 @@ locale CNode_AC_3 = CNode_AC_2 +
     "arch_post_cap_deletion irqopt \<lbrace>pas_refined aag\<rbrace>"
   and aobj_ref'_same_aobject:
     "same_aobject_as ao' ao \<Longrightarrow> aobj_ref' ao = aobj_ref' ao'"
-  and set_untyped_cap_as_full_valid_arch_state[wp]:
-    "set_untyped_cap_as_full src_cap new_cap src_slot \<lbrace>\<lambda>s :: det_ext state. valid_arch_state s\<rbrace>"
 begin
 
 lemma cap_insert_pas_refined:
diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy
index 465471bb1f..36f064cfa3 100644
--- a/proof/access-control/Finalise_AC.thy
+++ b/proof/access-control/Finalise_AC.thy
@@ -372,7 +372,7 @@ crunch suspend
   for pspace_aligned[wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
   and valid_vspace_objs[wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
   and valid_arch_state[wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
-  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)
+  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps simp: tcb_cap_cases_def)
 
 crunch suspend
   for pas_refined[wp]: "pas_refined aag"
diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy
index aec0b47790..eb7a8cc056 100644
--- a/proof/access-control/Ipc_AC.thy
+++ b/proof/access-control/Ipc_AC.thy
@@ -172,6 +172,9 @@ locale Ipc_AC_1 =
     "\<And>P. make_fault_msg ft t \<lbrace>\<lambda>s :: det_ext state. P s\<rbrace>"
   and tcb_context_no_change:
     "\<exists>ctxt. (tcb :: tcb) = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr>"
+  (* This assumption excludes x64 (its valid_arch_state includes caps) *)
+  and transfer_caps_loop_valid_arch[wp]:
+    "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
 begin
 
 lemma send_upd_ctxintegrity:
@@ -914,7 +917,7 @@ crunch do_fault_transfer
   for pas_refined[wp]: "\<lambda>s :: det_ext state. pas_refined aag s"
 
 crunch transfer_caps, copy_mrs
-  for valid_arch_state[wp]: valid_arch_state
+  for valid_arch_state[wp]: "valid_arch_state :: det_ext state \<Rightarrow> _"
   (wp: crunch_wps)
 
 lemma do_normal_transfer_pas_refined:
@@ -1067,6 +1070,7 @@ lemma send_ipc_pas_refined:
                     in hoare_strengthen_post[rotated])
         apply simp
        apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined hoare_weak_lift_imp gts_wp
+                 do_ipc_transfer_valid_arch
               | wpc
               | simp add: hoare_if_r_and)+
    apply (wp hoare_vcg_all_lift hoare_imp_lift_something | simp add: st_tcb_at_tcb_states_of_state_eq)+
@@ -1214,6 +1218,7 @@ lemma receive_ipc_base_pas_refined:
         apply (wp hoare_weak_lift_imp do_ipc_transfer_pas_refined set_simple_ko_pas_refined
                   set_thread_state_pas_refined get_simple_ko_wp hoare_vcg_all_lift
                   hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
+                  do_ipc_transfer_valid_arch
                | wpc
                | simp add: thread_get_def  get_thread_state_def do_nbrecv_failed_transfer_def)+
   apply (clarsimp simp: tcb_at_def [symmetric] tcb_at_st_tcb_at)
@@ -2541,9 +2546,9 @@ lemma do_reply_transfer_pas_refined:
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   apply (simp add: do_reply_transfer_def)
   apply (rule hoare_pre)
-  apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined
-            thread_set_pas_refined K_valid
-         | wpc | simp add: thread_get_def split del: if_split)+
+  apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined do_ipc_transfer_valid_arch
+            thread_set_pas_refined K_valid thread_set_valid_arch_state
+         | wpc | simp add: thread_get_def tcb_cap_cases_def split del: if_split)+
   (* otherwise simp does too much *)
   apply (rule hoare_strengthen_post, rule gts_inv)
    apply (rule impI)
diff --git a/proof/access-control/RISCV64/ArchIpc_AC.thy b/proof/access-control/RISCV64/ArchIpc_AC.thy
index 7be518e246..211262fde4 100644
--- a/proof/access-control/RISCV64/ArchIpc_AC.thy
+++ b/proof/access-control/RISCV64/ArchIpc_AC.thy
@@ -66,6 +66,10 @@ lemma tcb_context_no_change[Ipc_AC_assms]:
   apply (auto simp: arch_tcb_context_set_def)
   done
 
+lemma transfer_caps_loop_valid_arch[Ipc_AC_assms]:
+  "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps transfer_caps_loop_aobj_at)
+
 end
 
 
diff --git a/proof/infoflow/ARM/ArchRetype_IF.thy b/proof/infoflow/ARM/ArchRetype_IF.thy
index 8a8060dc9d..d30122f709 100644
--- a/proof/infoflow/ARM/ArchRetype_IF.thy
+++ b/proof/infoflow/ARM/ArchRetype_IF.thy
@@ -12,6 +12,15 @@ context Arch begin global_naming ARM
 
 named_theorems Retype_IF_assms
 
+lemma do_ipc_transfer_valid_arch_no_caps[wp]:
+  "do_ipc_transfer s ep bg grt r \<lbrace>valid_arch_state\<rbrace>"
+  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps do_ipc_transfer_aobj_at)
+
+lemma create_cap_valid_arch_state_no_caps[wp]:
+  "\<lbrace>valid_arch_state \<rbrace> create_cap tp sz p dev ref
+   \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps create_cap_aobj_at)
+
 lemma cacheRangeOp_ev[wp]:
   "(\<And>a b. equiv_valid_inv I A \<top> (oper a b))
    \<Longrightarrow> equiv_valid_inv I A \<top> (cacheRangeOp oper x y z)"
diff --git a/proof/infoflow/ARM/ArchTcb_IF.thy b/proof/infoflow/ARM/ArchTcb_IF.thy
index 44dd1df9c1..c84b03c1fd 100644
--- a/proof/infoflow/ARM/ArchTcb_IF.thy
+++ b/proof/infoflow/ARM/ArchTcb_IF.thy
@@ -185,6 +185,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
                            cap_delete_pas_refined' itr_wps(12) itr_wps(14) cap_insert_cte_at
                            checked_insert_no_cap_to hoare_vcg_const_imp_liftE_R hoare_vcg_conj_lift
                            as_user_reads_respects_f thread_set_mdb cap_delete_invs
+                           thread_set_valid_arch_state
                       | wpc
                       | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
                                   tcb_at_st_tcb_at when_def
@@ -231,6 +232,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
              thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
              thread_set_cte_at thread_set_no_cap_to_trivial
              thread_set_tcb_fault_handler_update_only_timer_irq_inv
+             thread_set_valid_arch_state
           | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imp)+
   apply (clarsimp simp: authorised_tcb_inv_def  authorised_tcb_inv_extra_def emptyable_def)
   by (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def is_valid_vtable_root_def det_setRegister
diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy
index 98d64ca9d7..ea1c2388a8 100644
--- a/proof/infoflow/Arch_IF.thy
+++ b/proof/infoflow/Arch_IF.thy
@@ -8,6 +8,14 @@ theory Arch_IF
 imports ArchRetype_IF
 begin
 
+(* Note: exporting the following diverges from AInvs interfaces where valid_arch_state is
+   permitted to depend on caps (due to supporting x64). If x64 confidentiality is to go ahead,
+   this will need more careful management. *)
+arch_requalify_facts
+  do_ipc_transfer_valid_arch_no_caps
+
+lemmas [wp] = do_ipc_transfer_valid_arch_no_caps
+
 abbreviation irq_state_of_state :: "det_state \<Rightarrow> nat" where
   "irq_state_of_state s \<equiv> irq_state (machine_state s)"
 
diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy
index 476a7a8062..259a182e72 100644
--- a/proof/infoflow/Finalise_IF.thy
+++ b/proof/infoflow/Finalise_IF.thy
@@ -1489,7 +1489,8 @@ crunch deleting_irq_handler
 
 crunch cancel_ipc
   for globals_equiv[wp]: "globals_equiv st"
-  (wp: mapM_x_wp select_inv hoare_drop_imps hoare_vcg_if_lift2 simp: unless_def)
+  (wp: mapM_x_wp select_inv hoare_drop_imps hoare_vcg_if_lift2 thread_set_valid_arch_state
+   simp: unless_def tcb_cap_cases_def)
 
 lemma suspend_globals_equiv[ wp]:
   "\<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state\<rbrace>
diff --git a/proof/infoflow/Ipc_IF.thy b/proof/infoflow/Ipc_IF.thy
index 11865a8ea3..049644dedb 100644
--- a/proof/infoflow/Ipc_IF.thy
+++ b/proof/infoflow/Ipc_IF.thy
@@ -1600,9 +1600,9 @@ lemma do_reply_transfer_reads_respects_f:
             cap_delete_one_silc_inv do_ipc_transfer_silc_inv
             set_thread_state_pas_refined thread_set_fault_pas_refined'
             possible_switch_to_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
-            when_ev
+            when_ev thread_set_valid_arch_state
          | wpc
-         | simp split del: if_split
+         | simp split del: if_split add: tcb_cap_cases_def
          | wp (once) reads_respects_f[where aag=aag and st=st]
          | elim conjE
          | wp (once) hoare_drop_imps)+
@@ -1987,8 +1987,10 @@ lemma send_fault_ipc_globals_equiv:
   apply (wp)
      apply (simp add: Let_def)
      apply (wp send_ipc_globals_equiv thread_set_globals_equiv thread_set_valid_objs''
-               thread_set_fault_valid_global_refs thread_set_valid_idle_trivial thread_set_refs_trivial
-            | wpc | simp)+
+               thread_set_fault_valid_global_refs thread_set_valid_idle_trivial
+               thread_set_refs_trivial thread_set_valid_arch_state
+               thread_set_tcb_fault_update_valid_mdb
+            | wpc | simp add: tcb_cap_cases_def)+
     apply (rule_tac Q'="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and
                             valid_global_refs and pspace_distinct and pspace_aligned and
                             valid_global_objs and K (valid_fault fault) and valid_idle and
@@ -2000,8 +2002,9 @@ lemma send_fault_ipc_globals_equiv:
   done
 
 crunch send_fault_ipc
-  for valid_arch_state[wp]: valid_arch_state
-  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)
+  for valid_arch_statex[wp]: valid_arch_state
+  (wp: dxo_wp_weak hoare_drop_imps thread_set_valid_arch_state crunch_wps
+   simp: crunch_simps tcb_cap_cases_def)
 
 lemma handle_fault_globals_equiv:
   "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
@@ -2033,7 +2036,8 @@ lemma do_reply_transfer_globals_equiv:
   unfolding do_reply_transfer_def
   apply (wp set_thread_state_globals_equiv cap_delete_one_globals_equiv do_ipc_transfer_globals_equiv
             thread_set_globals_equiv handle_fault_reply_globals_equiv dxo_wp_weak
-         | wpc | simp split del: if_split)+
+            thread_set_valid_arch_state
+         | wpc | simp split del: if_split add: tcb_cap_cases_def)+
      apply (rule_tac Q'="\<lambda>_. globals_equiv st and valid_arch_state and valid_objs and valid_arch_state
                                              and valid_global_refs and pspace_distinct
                                              and pspace_aligned and valid_global_objs
diff --git a/proof/infoflow/RISCV64/ArchRetype_IF.thy b/proof/infoflow/RISCV64/ArchRetype_IF.thy
index 194bdbbf0d..3f23f73912 100644
--- a/proof/infoflow/RISCV64/ArchRetype_IF.thy
+++ b/proof/infoflow/RISCV64/ArchRetype_IF.thy
@@ -12,6 +12,15 @@ context Arch begin global_naming RISCV64
 
 named_theorems Retype_IF_assms
 
+lemma do_ipc_transfer_valid_arch_no_caps[wp]:
+  "do_ipc_transfer s ep bg grt r \<lbrace>valid_arch_state\<rbrace>"
+  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps do_ipc_transfer_aobj_at)
+
+lemma create_cap_valid_arch_state_no_caps[wp]:
+  "\<lbrace>valid_arch_state \<rbrace> create_cap tp sz p dev ref
+   \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps create_cap_aobj_at)
+
 lemma modify_underlying_memory_update_0_ev:
   "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) \<top>
                    (modify (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 7,
diff --git a/proof/infoflow/RISCV64/ArchTcb_IF.thy b/proof/infoflow/RISCV64/ArchTcb_IF.thy
index 56830a0004..999bc04b2c 100644
--- a/proof/infoflow/RISCV64/ArchTcb_IF.thy
+++ b/proof/infoflow/RISCV64/ArchTcb_IF.thy
@@ -181,6 +181,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
                            cap_delete_pas_refined' itr_wps(12) itr_wps(14) cap_insert_cte_at
                            checked_insert_no_cap_to hoare_vcg_const_imp_liftE_R hoare_vcg_conj_lift
                            as_user_reads_respects_f thread_set_mdb cap_delete_invs
+                           thread_set_valid_arch_state
                       | wpc
                       | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
                                   tcb_at_st_tcb_at when_def
@@ -220,6 +221,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
     apply (simp add: option_update_thread_def tcb_cap_cases_def
            | wp hoare_weak_lift_imp hoare_weak_lift_imp_conj thread_set_pas_refined
                 reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
+                thread_set_valid_arch_state
            | wpc)+
    apply (wp hoare_vcg_all_lift thread_set_tcb_fault_handler_update_invs
              thread_set_tcb_fault_handler_update_silc_inv
@@ -227,6 +229,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
              thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
              thread_set_cte_at thread_set_no_cap_to_trivial
              thread_set_tcb_fault_handler_update_only_timer_irq_inv
+             thread_set_valid_arch_state
           | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imp)+
   apply (clarsimp simp: authorised_tcb_inv_def authorised_tcb_inv_extra_def emptyable_def)
   apply (clarsimp simp: invs_psp_aligned invs_vspace_objs invs_arch_state)
diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy
index 16cfd1f855..fcdcb12975 100644
--- a/proof/infoflow/Tcb_IF.thy
+++ b/proof/infoflow/Tcb_IF.thy
@@ -196,7 +196,7 @@ begin
 
 crunch cap_swap_for_delete
   for valid_arch_state[wp]: valid_arch_state
-  (wp: dxo_wp_weak)
+  (wp: dxo_wp_weak simp: crunch_simps)
 
 lemma rec_del_globals_equiv:
   "\<lbrace>\<lambda>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>