diff --git a/proof/invariant-abstract/X64/ArchArch_AI.thy b/proof/invariant-abstract/X64/ArchArch_AI.thy
index 94c32186b4..0dfde242dd 100644
--- a/proof/invariant-abstract/X64/ArchArch_AI.thy
+++ b/proof/invariant-abstract/X64/ArchArch_AI.thy
@@ -591,12 +591,22 @@ lemma cap_insert_ioports_ap:
          | wpc | simp split del: if_split)+
   done
 
+lemma cap_insert_ioport_control_ap:
+  "\<lbrace>ioport_control_unique and K (is_ap_cap cap)\<rbrace>
+   cap_insert cap src dest
+   \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  unfolding cap_insert_def set_untyped_cap_as_full_def
+  apply (wpsimp wp: get_cap_wp set_cap_ioport_control_safe hoare_vcg_const_imp_lift)
+  apply (auto simp: cte_wp_at_caps_of_state is_cap_simps)
+  done
+
 lemma cap_insert_valid_arch_state_ap:
   "\<lbrace>valid_arch_state and (\<lambda>s. cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) dest s) and
     K (is_ap_cap cap)\<rbrace>
    cap_insert cap src dest
    \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
-  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_ioports_ap)+
+  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_ioports_ap
+         cap_insert_ioport_control_ap)+
      (simp add: valid_arch_state_def)
 
 lemma cap_insert_ap_invs:
diff --git a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy
index be426f12bb..9048fbba4b 100644
--- a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy
+++ b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy
@@ -444,6 +444,30 @@ lemma cap_swap_ioports[wp]:
                  dest!: weak_derived_cap_ioports)
   by (fastforce elim!: ranE split: if_split_asm)
 
+lemma same_object_as_IOPortControlCap_eq:
+  "same_object_as cap (ArchObjectCap IOPortControlCap) = (cap = ArchObjectCap IOPortControlCap)"
+  unfolding same_object_as_def
+  by (simp split: cap.splits arch_cap.splits)
+
+lemma copy_of_IOPortControlCap_eq:
+  "(copy_of (ArchObjectCap IOPortControlCap) cap) = (cap = ArchObjectCap IOPortControlCap)"
+  unfolding copy_of_def
+  by (auto simp: is_cap_simps same_object_as_IOPortControlCap_eq)
+
+lemma weak_derived_IOPortControlCap_eq[simp]:
+  "weak_derived (ArchObjectCap IOPortControlCap) cap = (cap = ArchObjectCap IOPortControlCap)"
+  unfolding weak_derived_def
+  by (auto simp: copy_of_IOPortControlCap_eq)
+
+lemma cap_swap_ioport_control[wp]:
+  "\<lbrace>ioport_control_unique 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>_. ioport_control_unique\<rbrace>"
+  apply (wpsimp wp: cap_swap_caps_of_state simp: cte_wp_at_caps_of_state)
+  apply (clarsimp simp: ioport_control_unique_def)
+  apply (cases a, cases b)
+  by (rule conjI; clarsimp)+
+
 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
@@ -989,6 +1013,16 @@ lemma cap_move_ioports:
                  dest!: weak_derived_cap_ioports)
   by (fastforce elim!: ranE split: if_split_asm)
 
+lemma cap_move_ioport_control[wp]:
+  "\<lbrace>ioport_control_unique and cte_wp_at (weak_derived cap) ptr\<rbrace>
+   cap_move cap ptr ptr'
+   \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  apply (wpsimp wp: cap_move_caps_of_state simp: cte_wp_at_caps_of_state)
+  apply (clarsimp simp: ioport_control_unique_def)
+  apply (cases ptr)
+  apply (rule conjI; clarsimp)
+  done
+
 lemma cap_move_valid_arch:
   "\<lbrace>valid_arch_state and cte_wp_at ((=) cap.NullCap) ptr'
     and cte_wp_at (weak_derived cap) ptr
diff --git a/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy
index 36defd6de2..539a44f595 100644
--- a/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy
+++ b/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy
@@ -49,13 +49,22 @@ lemma set_cap_ioports_safe:
     apply blast+
   done
 
+lemma set_cap_ioport_control_safe:
+ "\<lbrace>\<lambda>s. ioport_control_unique s \<and>
+       (cap = ArchObjectCap IOPortControlCap \<longrightarrow> cte_wp_at ((=) (ArchObjectCap IOPortControlCap)) ptr s) \<rbrace>
+    set_cap cap ptr
+  \<lbrace>\<lambda>rv. ioport_control_unique \<rbrace>"
+  apply wp
+  apply (auto simp: ioport_control_unique_def cte_wp_at_caps_of_state)
+  done
+
 lemma set_cap_non_arch_valid_arch_state:
  "\<lbrace>\<lambda>s. valid_arch_state s \<and> cte_wp_at (\<lambda>_. \<not>is_arch_cap cap) ptr s\<rbrace>
   set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_arch_state \<rbrace>"
   unfolding valid_arch_state_def
   by (wp set_cap.aobj_at valid_asid_table_lift valid_global_pts_lift valid_global_pds_lift
-         valid_global_pdpts_lift typ_at_lift set_cap_ioports_safe)+
+         valid_global_pdpts_lift typ_at_lift set_cap_ioports_safe set_cap_ioport_control_safe)+
      (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_pspace_def safe_ioport_insert_triv)
 
 lemma set_cap_ioports_no_new_ioports:
@@ -80,12 +89,15 @@ lemma set_cap_ioports_no_new_ioports:
 
 lemma set_cap_no_new_ioports_arch_valid_arch_state:
  "\<lbrace>\<lambda>s. valid_arch_state s
-       \<and> cte_wp_at (\<lambda>cap'. cap_ioports cap = {} \<or> cap_ioports cap = cap_ioports cap') ptr s\<rbrace>
+       \<and> cte_wp_at (\<lambda>cap'. cap_ioports cap = {} \<or> cap_ioports cap = cap_ioports cap') ptr s
+       \<and> (cap = ArchObjectCap IOPortControlCap \<longrightarrow>
+          cte_wp_at ((=) (ArchObjectCap IOPortControlCap)) ptr s) \<rbrace>
   set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_arch_state \<rbrace>"
   unfolding valid_arch_state_def
   by (wp set_cap.aobj_at valid_asid_table_lift valid_global_pts_lift valid_global_pds_lift
-         valid_global_pdpts_lift typ_at_lift set_cap_ioports_no_new_ioports)+
+         valid_global_pdpts_lift typ_at_lift set_cap_ioports_no_new_ioports
+         set_cap_ioport_control_safe)+
      (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_pspace_def)
 
 lemma valid_ioportsD:
@@ -111,6 +123,10 @@ lemma unique_table_refs_no_cap_asidE:
 lemmas unique_table_refs_no_cap_asidD
      = unique_table_refs_no_cap_asidE[where S="{}"]
 
+lemma is_ioport_control_cap_simp[simp]:
+  "is_ioport_control_cap (ArchObjectCap IOPortControlCap)"
+  by (simp add: is_ioport_control_cap_def)
+
 lemma replace_cap_invs:
   "\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s p cap) p s
         \<and> cap \<noteq> cap.NullCap
@@ -214,6 +230,7 @@ lemma replace_cap_invs:
                     valid_arch_caps_def unique_table_refs_no_cap_asidE)
   apply clarsimp
   apply (rule conjI, solves clarsimp)
+  apply (rule conjI, solves clarsimp)
   apply (rule Ball_emptyI, simp add: gen_obj_refs_subset)
   done
 
diff --git a/proof/invariant-abstract/X64/ArchCSpace_AI.thy b/proof/invariant-abstract/X64/ArchCSpace_AI.thy
index 5ab4847157..6f586a32af 100644
--- a/proof/invariant-abstract/X64/ArchCSpace_AI.thy
+++ b/proof/invariant-abstract/X64/ArchCSpace_AI.thy
@@ -419,17 +419,32 @@ lemma cap_insert_derived_ioports:
   apply (drule_tac cap=cap in valid_ioports_issuedD, simp+)
   done
 
+lemma is_derived_not_ioport_control:
+  "is_derived (cdt s) src cap cap' \<Longrightarrow> cap \<noteq> ArchObjectCap IOPortControlCap"
+  by (clarsimp simp add: is_derived_def is_derived_arch_def split: if_splits)
+
+lemma cap_insert_derived_ioport_control:
+  "\<lbrace>ioport_control_unique and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace>
+     cap_insert cap src dest
+   \<lbrace>\<lambda>rv. ioport_control_unique\<rbrace>"
+  unfolding cap_insert_def set_untyped_cap_as_full_def
+  apply (wpsimp wp: get_cap_wp)
+  apply (auto dest!: is_derived_not_ioport_control
+              simp: cte_wp_at_caps_of_state ioport_control_unique_def is_cap_simps)
+  done
+
 lemma cap_insert_derived_valid_arch_state[CSpace_AI_assms]:
   "\<lbrace>valid_arch_state and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace>
    cap_insert cap src dest
    \<lbrace>\<lambda>rv. valid_arch_state \<rbrace>"
-  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_derived_ioports)+
+  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_derived_ioports
+         cap_insert_derived_ioport_control)+
      (simp add: cap_insert_aobj_at valid_arch_state_def)
 
 lemma cap_insert_simple_ioports:
   "\<lbrace>valid_ioports and (\<lambda>s. cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) dest s) and
         K (is_simple_cap cap \<and> \<not>is_ap_cap cap)\<rbrace>
-     cap_insert cap src dest
+   cap_insert cap src dest
    \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
   apply (simp add: cap_insert_def)
   apply (wp get_cap_wp set_cap_ioports_safe set_untyped_cap_as_full_ioports
@@ -437,12 +452,21 @@ lemma cap_insert_simple_ioports:
          | wpc | simp split del: if_splits)+
   done
 
+lemma cap_insert_simple_ioport_control:
+  "\<lbrace>ioport_control_unique and K (is_simple_cap cap)\<rbrace>
+   cap_insert cap src dest
+   \<lbrace>\<lambda>rv. ioport_control_unique\<rbrace>"
+  unfolding cap_insert_def set_untyped_cap_as_full_def
+  by (wpsimp wp: get_cap_wp)
+     (auto simp: cte_wp_at_caps_of_state is_simple_cap_def ioport_control_unique_def)
+
 lemma cap_insert_simple_valid_arch_state:
   "\<lbrace>valid_arch_state and (\<lambda>s. cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) dest s) and
     K (is_simple_cap cap \<and> \<not>is_ap_cap cap)\<rbrace>
    cap_insert cap src dest
    \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
-  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_simple_ioports)+
+  by (wp valid_arch_state_lift_ioports_aobj_at cap_insert_aobj_at cap_insert_simple_ioports
+         cap_insert_simple_ioport_control)+
      (simp add: valid_arch_state_def)
 
 end
@@ -629,6 +653,11 @@ lemma setup_reply_master_ioports[wp]:
   apply (wpsimp simp: setup_reply_master_def wp: set_cap_ioports_no_new_ioports get_cap_wp)
   by (clarsimp simp: cte_wp_at_caps_of_state)
 
+lemma setup_reply_master_arch_ioport_control[wp]:
+  "setup_reply_master t \<lbrace>ioport_control_unique\<rbrace>"
+  unfolding setup_reply_master_def
+  by (wpsimp wp: get_cap_wp simp: ioport_control_unique_def)
+
 lemma setup_reply_master_arch[CSpace_AI_assms]:
   "setup_reply_master t \<lbrace> valid_arch_state \<rbrace>"
   by (wp valid_arch_state_lift_ioports_typ_at setup_reply_master_ioports)+
diff --git a/proof/invariant-abstract/X64/ArchDetype_AI.thy b/proof/invariant-abstract/X64/ArchDetype_AI.thy
index 2cd93f1bb6..54b138c07f 100644
--- a/proof/invariant-abstract/X64/ArchDetype_AI.thy
+++ b/proof/invariant-abstract/X64/ArchDetype_AI.thy
@@ -181,11 +181,15 @@ lemma tcb_arch_detype[detype_invs_proofs]:
 
 lemma valid_ioports_detype:
   "valid_ioports s \<Longrightarrow> valid_ioports (detype (untyped_range cap) s)"
-  apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def issued_ioports_def more_update.caps_of_state_update)
-  apply (clarsimp simp: detype_def cap_ioports_def ran_def elim!: ranE split: if_splits cap.splits arch_cap.splits)
-  apply (rule conjI)
-   apply (force simp: ran_def)
-  by (metis (full_types) ranI)
+  apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def
+                        issued_ioports_def)
+  apply (clarsimp simp: detype_def cap_ioports_def ran_def)
+  by blast
+
+lemma ioport_control_detype:
+  "ioport_control_unique_2 caps \<Longrightarrow>
+   ioport_control_unique_2 (\<lambda>p. if fst p \<in> S then None else caps p)"
+  by (auto simp: ioport_control_unique_2_def)
 
 lemma valid_arch_state_detype[detype_invs_proofs]:
   "valid_arch_state (detype (untyped_range cap) s)"
@@ -194,7 +198,7 @@ lemma valid_arch_state_detype[detype_invs_proofs]:
   apply (strengthen valid_ioports_detype,
          simp add: valid_arch_state_def valid_asid_table_def
                    valid_global_pdpts_def valid_global_pds_def valid_global_pts_def
-                   global_refs_def cap_range_def)
+                   global_refs_def cap_range_def ioport_control_detype)
   apply (clarsimp simp: ran_def arch_state_det)
   apply (drule vs_lookup_atI)
   apply (drule (1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])
diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy
index 61ab34ef58..c96a2482c2 100644
--- a/proof/invariant-abstract/X64/ArchInvariants_AI.thy
+++ b/proof/invariant-abstract/X64/ArchInvariants_AI.thy
@@ -1051,6 +1051,21 @@ definition
 where
   "valid_x64_irq_state irqState \<equiv> \<forall>irq > maxIRQ. irqState irq = IRQFree"
 
+
+(* Mainly used to discharge the Haskell assertion archMDBAssertions, which is
+   used in CRefine. The invariant says that there is only one IOPortControlCap
+   in the system. *)
+definition ioport_control_unique_2 :: "(cslot_ptr \<Rightarrow> cap option) \<Rightarrow> bool" where
+  "ioport_control_unique_2 caps \<equiv>
+     \<forall>p p'. caps p = Some (ArchObjectCap IOPortControlCap) \<longrightarrow>
+            caps p' = Some (ArchObjectCap IOPortControlCap) \<longrightarrow>
+            p' = p"
+
+locale_abbrev ioport_control_unique where
+  "ioport_control_unique s \<equiv> ioport_control_unique_2 (caps_of_state s)"
+
+lemmas ioport_control_unique_def = ioport_control_unique_2_def
+
 definition
   valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
 where
@@ -1062,6 +1077,7 @@ where
       \<and> valid_global_pdpts s
       \<and> valid_cr3 (x64_current_cr3 (arch_state s))
       \<and> valid_x64_irq_state (x64_irq_state (arch_state s))
+      \<and> ioport_control_unique s
       \<and> valid_ioports s"
 
 definition
@@ -1778,23 +1794,23 @@ lemma valid_arch_state_lift:
    apply (wp arch typs caps hoare_vcg_conj_lift hoare_vcg_const_Ball_lift)+
   done
 
-(* we usually have a rule for valid_ioports, but it often comes with side-conditions *)
+(* we usually have a rule for valid_ioports and ioport_control_unique, but they often come with
+   side-conditions *)
 lemma valid_arch_state_lift_ioports_typ_at:
-  fixes Q
   assumes typs: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace>"
   assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
   assumes ports: "\<lbrace> Q \<rbrace> f \<lbrace>\<lambda>_. valid_ioports \<rbrace>"
-  shows "\<lbrace>valid_arch_state and Q\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
-  apply (simp add: valid_arch_state_def pred_conj_def)
+  assumes control: "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. ioport_control_unique\<rbrace>"
+  shows "\<lbrace>valid_arch_state and Q and P\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
   apply (simp add: valid_arch_state_def valid_asid_table_def
                    valid_global_pts_def valid_global_pds_def valid_global_pdpts_def)
-  (* we need to do this piece-wise so we can grab
-     `valid_ioports_2 (caps_of_state x) (arch_state x) \<and> Q x` at the end *)
-  apply (rule hoare_vcg_conj_lift[rotated])+
-  apply (solves \<open>wpsimp wp: ports\<close>)
-  (* the rest are trivial once arch_state is lifted out *)
-  apply (rule hoare_lift_Pf2[where f="\<lambda>s. arch_state s", OF _ arch],
-         solves \<open>wp typs hoare_vcg_conj_lift hoare_vcg_const_Ball_lift\<close>)+
+  apply wp_pre
+   (* isolate the `valid_ioports_2 (caps_of_state s) (arch_state s)` at the end,
+      because we don't want wps to act on (arch_state s) there. *)
+   apply (rule hoare_vcg_conj_lift[rotated])+
+            apply (rule ports)
+           apply (wps arch | wp control typs hoare_vcg_op_lift)+
+  apply simp
   done
 
 lemma aobj_at_default_arch_cap_valid:
diff --git a/proof/invariant-abstract/X64/ArchIpc_AI.thy b/proof/invariant-abstract/X64/ArchIpc_AI.thy
index d99816f59d..226b0b83bb 100644
--- a/proof/invariant-abstract/X64/ArchIpc_AI.thy
+++ b/proof/invariant-abstract/X64/ArchIpc_AI.thy
@@ -442,6 +442,25 @@ lemma transfer_caps_loop_ioports:
   apply clarsimp
   done
 
+lemma transfer_caps_loop_ioport_control:
+  "\<lbrace>ioport_control_unique and valid_objs and valid_mdb and K (distinct slots)
+         and (\<lambda>s. \<forall>x \<in> set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s)
+         and transfer_caps_srcs caps\<rbrace>
+   transfer_caps_loop ep buffer n caps slots mi
+   \<lbrace>\<lambda>rv. ioport_control_unique\<rbrace>"
+  apply (rule hoare_pre)
+   apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False])
+     apply (wp cap_insert_derived_ioport_control)
+     apply (clarsimp simp: cte_wp_at_caps_of_state)
+    apply (wp valid_ioports_lift)
+   apply (clarsimp simp:cte_wp_at_caps_of_state|intro conjI ballI)+
+   apply (drule(1) bspec,clarsimp)
+   apply (frule(1) caps_of_state_valid)
+   apply (fastforce simp:valid_cap_def)
+  apply (drule(1) bspec)
+  apply clarsimp
+  done
+
 lemma transfer_caps_loop_valid_arch[Ipc_AI_2_assms]:
   "\<And>slots caps ep buffer n mi.
     \<lbrace>valid_arch_state and valid_objs and valid_mdb and K (distinct slots)
@@ -450,7 +469,7 @@ lemma transfer_caps_loop_valid_arch[Ipc_AI_2_assms]:
       transfer_caps_loop ep buffer n caps slots mi
     \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
   by (wpsimp wp: valid_arch_state_lift_ioports_aobj_at transfer_caps_loop_ioports
-                 transfer_caps_loop_aobj_at)
+                 transfer_caps_loop_ioport_control transfer_caps_loop_aobj_at)
      (simp add: valid_arch_state_def)
 
 lemma setup_caller_cap_aobj_at:
@@ -459,14 +478,22 @@ lemma setup_caller_cap_aobj_at:
   unfolding setup_caller_cap_def
   by (wpsimp wp: cap_insert_aobj_at sts.aobj_at)
 
+lemma setup_caller_cap_ioport_control[wp]:
+  "setup_caller_cap st rt grant \<lbrace>ioport_control_unique\<rbrace>"
+  unfolding setup_caller_cap_def cap_insert_def set_untyped_cap_as_full_def
+  apply (wpsimp wp: get_cap_wp split_del: if_split simp: cte_wp_at_caps_of_state)
+  apply (auto simp: ioport_control_unique_def)
+  done
+
 lemma setup_caller_cap_valid_arch[Ipc_AI_2_assms, wp]:
   "setup_caller_cap st rt grant \<lbrace>valid_arch_state\<rbrace>"
   by (wp valid_arch_state_lift_ioports_aobj_at[rotated -1] setup_caller_cap_ioports
-         setup_caller_cap_aobj_at)
+         setup_caller_cap_aobj_at)+
      (simp add: valid_arch_state_def)
 
 crunch do_ipc_transfer
   for ioports[wp]: "valid_ioports"
+  and ioport_control[wp]: "ioport_control_unique"
   (wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_ioports
    simp: zipWithM_x_mapM crunch_simps ball_conj_distrib )
 
diff --git a/proof/invariant-abstract/X64/ArchKHeap_AI.thy b/proof/invariant-abstract/X64/ArchKHeap_AI.thy
index b2551e9b08..0be4430dae 100644
--- a/proof/invariant-abstract/X64/ArchKHeap_AI.thy
+++ b/proof/invariant-abstract/X64/ArchKHeap_AI.thy
@@ -541,17 +541,17 @@ lemma typ_at_lift:
      (wpsimp wp: aobj_at)
 
 lemma valid_arch_state_lift_ioports_aobj_at:
-  fixes P
   assumes ioports: "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. valid_ioports \<rbrace>"
-  shows "\<lbrace>valid_arch_state and P\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
+  assumes control: "\<lbrace> Q \<rbrace> f \<lbrace>\<lambda>_. ioport_control_unique \<rbrace>"
+  shows "\<lbrace>valid_arch_state and P and Q\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
   apply (simp add: valid_arch_state_def)
   apply (rule hoare_vcg_conj_lift
          | wp valid_asid_table_lift typ_at_lift valid_global_pts_lift valid_global_pds_lift
             valid_global_pdpts_lift)+
-  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
-  apply (rule hoare_vcg_conj_lift)
-  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
-  apply (wp ioports)
+    apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
+   apply (rule hoare_vcg_conj_lift)
+    apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch], wp)
+   apply (wp control ioports)
   apply simp
   done
 
diff --git a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy
index a60898c122..1917227bab 100644
--- a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy
+++ b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy
@@ -305,6 +305,8 @@ lemma invs_A:
     apply (clarsimp simp: valid_arch_state_def)
     apply (rule conjI)
      apply (clarsimp simp: valid_asid_table_def state_defs)
+    apply (prop_tac "ioport_control_unique init_A_st")
+     apply (simp add: caps_of_state_init_A_st_Null ioport_control_unique_def)
     apply (subgoal_tac "valid_ioports init_A_st")
      apply (simp add: valid_global_pts_def valid_global_pds_def valid_global_pdpts_def
                       valid_arch_state_def state_defs obj_at_def a_type_def
diff --git a/proof/invariant-abstract/X64/ArchRetype_AI.thy b/proof/invariant-abstract/X64/ArchRetype_AI.thy
index 4fda34a834..36e0e30b11 100644
--- a/proof/invariant-abstract/X64/ArchRetype_AI.thy
+++ b/proof/invariant-abstract/X64/ArchRetype_AI.thy
@@ -885,6 +885,15 @@ lemma ioports_no_overlap_null:
    apply (case_tac cap'; clarsimp)
   by (case_tac cap; clarsimp simp: ran_null_filter)
 
+lemma null_filter_IOPortControlCap_eq[simp]:
+  "(null_filter caps p = Some (ArchObjectCap IOPortControlCap)) =
+   (caps p = Some (ArchObjectCap IOPortControlCap))"
+  by (auto simp add: null_filter_def)
+
+lemma ioport_control_null:
+  "ioport_control_unique_2 (null_filter caps) = ioport_control_unique_2 caps"
+  by (clarsimp simp: ioport_control_unique_def)
+
 lemma pspace_respects_device_regionI:
   assumes uat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz))
                 \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - device_region s"
@@ -1010,12 +1019,16 @@ lemma valid_ioports:
   "valid_ioports s \<Longrightarrow> valid_ioports s'"
   by (clarsimp simp: valid_ioports_def ioports_no_overlap_eq all_ioports_issued_eq)
 
+lemmas ioport_control_eq
+    = arg_cong[where f=ioport_control_unique_2, OF null_filter,
+               simplified ioport_control_null]
+
 lemma valid_arch_state:
   "valid_arch_state s \<Longrightarrow> valid_arch_state s'"
   unfolding valid_arch_state_def
   by (strengthen valid_ioports,
       clarsimp simp: valid_arch_state_def obj_at_pres valid_asid_table_def valid_global_pts_def
-                     valid_global_pds_def valid_global_pdpts_def)
+                     valid_global_pds_def valid_global_pdpts_def ioport_control_eq)
 
 lemma valid_global_objs:
   "valid_global_objs s \<Longrightarrow> valid_global_objs s'"
diff --git a/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy b/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy
index a635a890db..b3ebd49a0b 100644
--- a/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy
+++ b/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy
@@ -188,6 +188,7 @@ lemma thread_set_valid_arch_state[TcbAcc_AI_assms]:
   "(\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb)
    \<Longrightarrow> thread_set f t \<lbrace> valid_arch_state \<rbrace>"
   by (wp valid_arch_state_lift_ioports_aobj_at thread_set_ioports thread_set.aobj_at
+         thread_set_caps_of_state_trivial
       | simp add: valid_arch_state_def)+
 
 end
diff --git a/proof/invariant-abstract/X64/ArchUntyped_AI.thy b/proof/invariant-abstract/X64/ArchUntyped_AI.thy
index 65a303877f..93790d5832 100644
--- a/proof/invariant-abstract/X64/ArchUntyped_AI.thy
+++ b/proof/invariant-abstract/X64/ArchUntyped_AI.thy
@@ -386,6 +386,16 @@ lemma create_cap_ioports[wp]:
   by (wpsimp wp: set_cap_ioports_safe set_cdt_cte_wp_at
               simp: safe_ioport_insert_not_ioport[OF default_cap_not_ioport] create_cap_def)
 
+lemma default_cap_neq_IOPortControlCap[simp]:
+  "default_cap tp oref sz dev \<noteq> ArchObjectCap IOPortControlCap"
+  by (cases tp; simp)
+     (simp add: arch_default_cap_def split: aobject_type.split)
+
+lemma create_cap_ioport_control[wp]:
+  "create_cap tp sz p dev (cref,oref) \<lbrace>ioport_control_unique\<rbrace>"
+  unfolding create_cap_def
+  by (wpsimp simp: ioport_control_unique_def)
+
 lemma create_cap_valid_arch_state[wp, Untyped_AI_assms]:
   "\<lbrace>valid_arch_state and cte_wp_at (\<lambda>_. True) cref\<rbrace>
    create_cap tp sz p dev (cref,oref)
diff --git a/proof/invariant-abstract/X64/ArchVSpace_AI.thy b/proof/invariant-abstract/X64/ArchVSpace_AI.thy
index d8cae2e16f..787b97a428 100644
--- a/proof/invariant-abstract/X64/ArchVSpace_AI.thy
+++ b/proof/invariant-abstract/X64/ArchVSpace_AI.thy
@@ -1334,6 +1334,10 @@ lemma master_cap_eq_is_device_cap_eq:
 lemmas vs_cap_ref_eq_imp_table_cap_ref_eq' =
        vs_cap_ref_eq_imp_table_cap_ref_eq[OF master_cap_eq_is_pg_cap_eq]
 
+lemma IOPortControlCap_cap_master_cap_eq[simp]:
+  "(ArchObjectCap IOPortControlCap = cap_master_cap cap) = (cap = ArchObjectCap IOPortControlCap)"
+  by (simp add: cap_master_cap_def split: cap.splits arch_cap.splits)
+
 lemma arch_update_cap_invs_map:
   "\<lbrace>cte_wp_at (is_arch_update cap and
                (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p
@@ -1372,6 +1376,7 @@ lemma arch_update_cap_invs_map:
   apply (rule conjI)
    apply (frule master_cap_obj_refs)
    apply (clarsimp simp: cap_ioports_def cap_master_cap_def split: arch_cap.splits cap.splits)
+  apply (rule conjI, solves \<open>clarsimp simp: cap_master_cap_simps\<close>)
   apply (rule conjI, frule master_cap_obj_refs, simp)
   apply (rule conjI)
    apply (frule master_cap_obj_refs)