diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy
index 7a51fe3a9..99f84bf22 100644
--- a/proof/crefine/ARM/Wellformed_C.thy
+++ b/proof/crefine/ARM/Wellformed_C.thy
@@ -116,18 +116,6 @@ definition
   where
   "cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
 
-definition
-  ctcb_size_bits :: nat
-  where
-  "ctcb_size_bits \<equiv> 8"
-
-definition
-  ctcb_offset :: word32
-  where
-  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
-
-lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
-
 definition
   ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word32"
   where
diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy
index 2e609e9ef..d48c8a32c 100644
--- a/proof/crefine/ARM_HYP/Wellformed_C.thy
+++ b/proof/crefine/ARM_HYP/Wellformed_C.thy
@@ -131,18 +131,6 @@ definition
   where
   "cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
 
-definition
-  ctcb_size_bits :: nat
-  where
-  "ctcb_size_bits \<equiv> 8"
-
-definition
-  ctcb_offset :: word32
-  where
-  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
-
-lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
-
 definition
   ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word32"
   where
diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy
index 53a9db66a..c8b949b9b 100644
--- a/proof/crefine/X64/Wellformed_C.thy
+++ b/proof/crefine/X64/Wellformed_C.thy
@@ -122,18 +122,6 @@ definition
   where
   "cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)"
 
-definition
-  ctcb_size_bits :: nat
-  where
-  "ctcb_size_bits \<equiv> 10"
-
-definition
-  ctcb_offset :: machine_word
-  where
-  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
-
-lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
-
 definition
   ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word64"
   where
diff --git a/spec/cspec/ARM/Kernel_C.thy b/spec/cspec/ARM/Kernel_C.thy
index e4951c3d5..a9df1c1a4 100644
--- a/spec/cspec/ARM/Kernel_C.thy
+++ b/spec/cspec/ARM/Kernel_C.thy
@@ -77,6 +77,18 @@ requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
 
 end
 
+definition
+  ctcb_size_bits :: nat
+where
+  "ctcb_size_bits \<equiv> 8"
+
+definition
+  ctcb_offset :: "32 word"
+where
+  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
+
+lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
+
 install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
   [machinety=machine_state, ghostty=cghost_state]
 
diff --git a/spec/cspec/ARM_HYP/Kernel_C.thy b/spec/cspec/ARM_HYP/Kernel_C.thy
index e4951c3d5..a9df1c1a4 100644
--- a/spec/cspec/ARM_HYP/Kernel_C.thy
+++ b/spec/cspec/ARM_HYP/Kernel_C.thy
@@ -77,6 +77,18 @@ requalify_consts ARMSmallPage ARMLargePage ARMSection ARMSuperSection
 
 end
 
+definition
+  ctcb_size_bits :: nat
+where
+  "ctcb_size_bits \<equiv> 8"
+
+definition
+  ctcb_offset :: "32 word"
+where
+  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
+
+lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
+
 install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
   [machinety=machine_state, ghostty=cghost_state]
 
diff --git a/spec/cspec/X64/Kernel_C.thy b/spec/cspec/X64/Kernel_C.thy
index 7d9004211..37f6ed5e0 100644
--- a/spec/cspec/X64/Kernel_C.thy
+++ b/spec/cspec/X64/Kernel_C.thy
@@ -75,6 +75,18 @@ context begin interpretation Arch . global_naming vmpage_size
 requalify_consts X64SmallPage X64LargePage X64HugePage
 end
 
+definition
+  ctcb_size_bits :: nat
+where
+  "ctcb_size_bits \<equiv> 10"
+
+definition
+  ctcb_offset :: "64 word"
+where
+  "ctcb_offset \<equiv> 2 ^ ctcb_size_bits"
+
+lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def
+
 install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp"
   [machinety=machine_state, ghostty=cghost_state]