diff --git a/spec/abstract/ARM/ArchTcb_A.thy b/spec/abstract/ARM/ArchTcb_A.thy
index 27c9bc67a1..85e70cfdb0 100644
--- a/spec/abstract/ARM/ArchTcb_A.thy
+++ b/spec/abstract/ARM/ArchTcb_A.thy
@@ -34,5 +34,11 @@ definition
 where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
+  "arch_post_set_flags t flags \<equiv> return ()"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end
diff --git a/spec/abstract/ARM/Arch_A.thy b/spec/abstract/ARM/Arch_A.thy
index 4f55fb3795..8ea29c5ed5 100644
--- a/spec/abstract/ARM/Arch_A.thy
+++ b/spec/abstract/ARM/Arch_A.thy
@@ -45,6 +45,9 @@ definition
      set_vm_root thread
    od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"
diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy
index 5c2a766816..dd293e0ea7 100644
--- a/spec/abstract/ARM/Arch_Structs_A.thy
+++ b/spec/abstract/ARM/Arch_Structs_A.thy
@@ -12,7 +12,7 @@ chapter "ARM-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
diff --git a/spec/abstract/ARM/Init_A.thy b/spec/abstract/ARM/Init_A.thy
index 2872ed1276..89836bc135 100644
--- a/spec/abstract/ARM/Init_A.thy
+++ b/spec/abstract/ARM/Init_A.thy
@@ -74,6 +74,7 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_flags = {},
     tcb_arch = init_arch_tcb
   \<rparr>,
   init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), \<comment> \<open>same reason as why we kept the definition of @{term init_globals_frame}\<close>
diff --git a/spec/abstract/ARM_HYP/ArchTcb_A.thy b/spec/abstract/ARM_HYP/ArchTcb_A.thy
index e5da56d323..e6bc391439 100644
--- a/spec/abstract/ARM_HYP/ArchTcb_A.thy
+++ b/spec/abstract/ARM_HYP/ArchTcb_A.thy
@@ -41,5 +41,11 @@ definition
 where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
+  "arch_post_set_flags t flags \<equiv> return ()"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end
diff --git a/spec/abstract/ARM_HYP/Arch_A.thy b/spec/abstract/ARM_HYP/Arch_A.thy
index 15beb775a1..cc87d0bc0e 100644
--- a/spec/abstract/ARM_HYP/Arch_A.thy
+++ b/spec/abstract/ARM_HYP/Arch_A.thy
@@ -46,6 +46,9 @@ definition
      set_vm_root t
    od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"
diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy
index ba98106cc1..ff40be94b6 100644
--- a/spec/abstract/ARM_HYP/Arch_Structs_A.thy
+++ b/spec/abstract/ARM_HYP/Arch_Structs_A.thy
@@ -12,7 +12,7 @@ chapter "ARM-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
diff --git a/spec/abstract/ARM_HYP/Init_A.thy b/spec/abstract/ARM_HYP/Init_A.thy
index e87c2dd6cd..a7746a7e23 100644
--- a/spec/abstract/ARM_HYP/Init_A.thy
+++ b/spec/abstract/ARM_HYP/Init_A.thy
@@ -76,6 +76,7 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_flags = {},
     tcb_arch = init_arch_tcb
   \<rparr>,
   us_global_pd_ptr \<mapsto> us_global_pd)"
diff --git a/spec/abstract/RISCV64/ArchTcb_A.thy b/spec/abstract/RISCV64/ArchTcb_A.thy
index 4e071341a9..e93fcb1b27 100644
--- a/spec/abstract/RISCV64/ArchTcb_A.thy
+++ b/spec/abstract/RISCV64/ArchTcb_A.thy
@@ -24,5 +24,11 @@ definition arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Righta
   where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
+  "arch_post_set_flags t flags \<equiv> return ()"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end
diff --git a/spec/abstract/RISCV64/Arch_A.thy b/spec/abstract/RISCV64/Arch_A.thy
index 818e3a7cf9..29168b7931 100644
--- a/spec/abstract/RISCV64/Arch_A.thy
+++ b/spec/abstract/RISCV64/Arch_A.thy
@@ -36,6 +36,9 @@ definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad"
     set_vm_root thread
   od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
   where
   "arch_activate_idle_thread t \<equiv> return ()"
diff --git a/spec/abstract/RISCV64/Arch_Structs_A.thy b/spec/abstract/RISCV64/Arch_Structs_A.thy
index 8844ee0576..e6b12df36f 100644
--- a/spec/abstract/RISCV64/Arch_Structs_A.thy
+++ b/spec/abstract/RISCV64/Arch_Structs_A.thy
@@ -8,7 +8,7 @@ chapter "RISCV64-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
diff --git a/spec/abstract/RISCV64/Init_A.thy b/spec/abstract/RISCV64/Init_A.thy
index 42bb63a180..03eb6d0196 100644
--- a/spec/abstract/RISCV64/Init_A.thy
+++ b/spec/abstract/RISCV64/Init_A.thy
@@ -111,6 +111,7 @@ definition init_kheap :: kheap
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_flags = {},
          tcb_arch = init_arch_tcb
          \<rparr>,
       riscv_global_pt_ptr \<mapsto> init_global_pt
diff --git a/spec/design/skel/ARM/ArchStructures_H.thy b/spec/design/skel/ARM/ArchStructures_H.thy
index 306ff88e7f..9f9868f514 100644
--- a/spec/design/skel/ARM/ArchStructures_H.thy
+++ b/spec/design/skel/ARM/ArchStructures_H.thy
@@ -15,9 +15,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PDET
diff --git a/spec/design/skel/ARM/Arch_Structs_B.thy b/spec/design/skel/ARM/Arch_Structs_B.thy
index 0817aa7d62..17bfcf1cd3 100644
--- a/spec/design/skel/ARM/Arch_Structs_B.thy
+++ b/spec/design/skel/ARM/Arch_Structs_B.thy
@@ -4,16 +4,22 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(* Architecture-specific data types shared by spec and abstract. *)
+(* Architecture-specific data types shared by design and abstract specs. *)
 
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
+
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_H ONLY ArmVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 end
diff --git a/spec/design/skel/ARM_HYP/ArchStructures_H.thy b/spec/design/skel/ARM_HYP/ArchStructures_H.thy
index a10a1163a5..07665aaf2a 100644
--- a/spec/design/skel/ARM_HYP/ArchStructures_H.thy
+++ b/spec/design/skel/ARM_HYP/ArchStructures_H.thy
@@ -15,9 +15,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H decls_only NOT VPPIEventIRQ VirtTimer
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H decls_only NOT VPPIEventIRQ VirtTimer \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H instanceproofs NOT VPPIEventIRQ VirtTimer
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H bodies_only NOT makeVCPUObject
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H bodies_only NOT makeVCPUObject \
+  NOT archTcbFlagToWord
 
 (* we define makeVCPUObject_def manually because we want a total function vgicLR *)
 defs makeVCPUObject_def:
diff --git a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy
index 75b5f0b951..9e524bdd1d 100644
--- a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy
+++ b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy
@@ -4,16 +4,21 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(* Architecture-specific data types shared by spec and abstract. *)
+(* Architecture-specific data types shared by design and abstract specs. *)
 
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_HYP_H ONLY ArmVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 end
diff --git a/spec/design/skel/RISCV64/ArchStructures_H.thy b/spec/design/skel/RISCV64/ArchStructures_H.thy
index b3ba3b4cde..d25a2cf274 100644
--- a/spec/design/skel/RISCV64/ArchStructures_H.thy
+++ b/spec/design/skel/RISCV64/ArchStructures_H.thy
@@ -16,9 +16,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PTET
diff --git a/spec/design/skel/RISCV64/Arch_Structs_B.thy b/spec/design/skel/RISCV64/Arch_Structs_B.thy
index 5ced589393..3257881b5b 100644
--- a/spec/design/skel/RISCV64/Arch_Structs_B.thy
+++ b/spec/design/skel/RISCV64/Arch_Structs_B.thy
@@ -4,18 +4,23 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(* Architecture-specific data types shared by spec and abstract. *)
+(* Architecture-specific data types shared by design and abstract specs. *)
 
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
 
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/RISCV64.hs CONTEXT RISCV64_H ONLY RISCVVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 
 end
diff --git a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs
index c844d80aa5..060b185072 100644
--- a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs
+++ b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs
@@ -65,3 +65,7 @@ There is nothing special about idle thread activation on ARM.
 > activateIdleThread :: PPtr TCB -> Kernel ()
 > activateIdleThread _ = return ()
 
+There is nothing special that needs to be done before calling nextDomain on ARM.
+
+> prepareNextDomain :: Kernel ()
+> prepareNextDomain = return ()
diff --git a/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs b/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs
index ea92b524c7..34ed57c7e5 100644
--- a/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs
+++ b/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs
@@ -30,3 +30,6 @@ switchToIdleThread = do
 
 activateIdleThread :: PPtr TCB -> Kernel ()
 activateIdleThread _ = return ()
+
+prepareNextDomain :: Kernel ()
+prepareNextDomain = return ()
diff --git a/spec/haskell/src/SEL4/Object/Structures/ARM.lhs b/spec/haskell/src/SEL4/Object/Structures/ARM.lhs
index c660aaeb12..692f8f2c19 100644
--- a/spec/haskell/src/SEL4/Object/Structures/ARM.lhs
+++ b/spec/haskell/src/SEL4/Object/Structures/ARM.lhs
@@ -136,6 +136,11 @@ present on all platforms is stored here.
 > atcbContextGet :: ArchTCB -> UserContext
 > atcbContextGet = atcbContext
 
+> type ArchTcbFlag = ()
+
+> archTcbFlagToWord :: ArchTcbFlag -> Word
+> archTcbFlagToWord _ = error "ARM does not have any arch specific flags"
+
 \subsection{ASID Pools}
 
 An ASID pool is an array of pointers to page directories. This is used to implement virtual ASIDs on ARM; it is not accessed by the hardware.
diff --git a/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs b/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs
index 49974204fd..bdcd44ae7c 100644
--- a/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs
+++ b/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs
@@ -73,6 +73,10 @@ atcbContextSet uc atcb = atcb { atcbContext = uc }
 atcbContextGet :: ArchTCB -> UserContext
 atcbContextGet = atcbContext
 
+type ArchTcbFlag = ()
+
+archTcbFlagToWord :: ArchTcbFlag -> Word
+archTcbFlagToWord _ = error "ARM does not have any arch specific flags"
 
 {- ASID Pools -}
 
diff --git a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs
index b40d822d62..337e760f99 100644
--- a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs
+++ b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs
@@ -23,6 +23,7 @@ There are presently no ARM-specific register subsets defined, but in future this
 > import SEL4.Model
 > import SEL4.Object.Structures
 > import SEL4.Object.Instances()
+> import SEL4.API.Types
 > import SEL4.API.Failures
 > import SEL4.API.Invocation.ARM
 > import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..))
@@ -66,3 +67,8 @@ There are presently no ARM-specific register subsets defined, but in future this
 > postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad ()
 > postModifyRegisters cur ptr = return ()
 
+> postSetFlags :: PPtr TCB -> TcbFlags -> Kernel ()
+> postSetFlags t flags = return ()
+
+> prepareSetDomain :: PPtr TCB -> Domain -> Kernel ()
+> prepareSetDomain t newDom = return ()
diff --git a/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs b/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs
index 32fc54cf90..a0bbb595b8 100644
--- a/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs
+++ b/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs
@@ -18,6 +18,7 @@ import Prelude hiding (Word)
 import SEL4.Machine(PPtr)
 import SEL4.Model
 import SEL4.Object.Structures
+import SEL4.API.Types
 import SEL4.API.Failures
 import SEL4.API.Invocation.RISCV64
 import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..))
@@ -41,3 +42,9 @@ getSanitiseRegisterInfo _ = return False
 
 postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad ()
 postModifyRegisters _ _ = return ()
+
+postSetFlags :: PPtr TCB -> TcbFlags -> Kernel ()
+postSetFlags t flags = return ()
+
+prepareSetDomain :: PPtr TCB -> Domain -> Kernel ()
+prepareSetDomain t newDom = return ()