seL4 · lsf37 · Jul 28, 2025 · Aug 7, 2025 · Jul 29, 2025 · Jul 31, 2025
diff --git a/proof/asmrefine/SEL4GlobalsSwap.thy b/proof/asmrefine/SEL4GlobalsSwap.thy
@@ -29,7 +29,7 @@ instance ptr :: (c_type)array_outer_packed ..
 instance tcb_queue_C :: array_outer_packed ..
 instance region_C :: array_outer_packed ..
 
-locale graph_refine_locale = kernel_all_substitute
+locale graph_refine_locale = kernel_all_substitute0
     + assumes globals_list_distinct:
         "globals_list_distinct domain symbol_table globals_list"
       assumes globals_list_ok:

diff --git a/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy b/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy
@@ -8,7 +8,7 @@ theory ArchSEL4SimplExport
 imports "AsmRefine.SimplExport" "CSpec.Substitute"
 begin
 
-context kernel_all_substitute begin
+context kernel_all_substitute0 begin
 
 lemma ctzl_body_refines:
   "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x___unsigned_long \<noteq> 0\<rbrace>

diff --git a/proof/asmrefine/export/SEL4SimplExport.thy b/proof/asmrefine/export/SEL4SimplExport.thy
@@ -14,7 +14,7 @@ val csenv = let
   in fn () => the_csenv end
 \<close>
 
-context kernel_all_substitute begin
+context kernel_all_substitute0 begin
 
 declare ctcb_offset_defs[simp]
 

diff --git a/proof/crefine/AARCH64/ADT_C.thy b/proof/crefine/AARCH64/ADT_C.thy
@@ -1692,8 +1692,8 @@ where
 
 end
 
-locale kernel_global = state_rel + kernel_all_global_addresses
-(* repeating ADT definitions in the c-parser's locale now (not the substitute) *)
+locale kernel_global = state_rel + kernel_all_multi
+(* repeating ADT definitions in the (multikernel-adjusted) C parser's locale now, not the substitute *)
 begin
 
 definition

diff --git a/proof/crefine/AARCH64/Ipc_C.thy b/proof/crefine/AARCH64/Ipc_C.thy
@@ -295,9 +295,9 @@ lemma ccap_relation_reply_helpers:
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
 (*FIXME: fupdate simplification issues for 2D arrays *)
 abbreviation "syscallMessageC \<equiv>  kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
-lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
-abbreviation "exceptionMessageC \<equiv> kernel_all_substitute.fault_messages.[unat MessageID_Exception]"
-lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def
+lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def
+abbreviation "exceptionMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]"
+lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def
 
 lemma syscallMessage_ccorres:
   "n < unat n_syscallMessage
@@ -6072,6 +6072,7 @@ lemma receiveIPC_ccorres [corres]:
   apply (auto simp: isCap_simps valid_cap'_def)
   done
 
+
 lemma sendSignal_dequeue_ccorres_helper:
   "ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_'
            (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest

diff --git a/proof/crefine/AARCH64/Machine_C.thy b/proof/crefine/AARCH64/Machine_C.thy
@@ -21,8 +21,11 @@ instance virq_C :: array_inner_packed
 
 locale kernel_m = kernel +
 
-(* timer and IRQ common machine ops (function names exist on other platforms *)
+(* The current verification is for unicore only *)
+assumes cpu_0:
+  "cpuNum = 0"
 
+(* timer and IRQ common machine ops (function names exist on other platforms *)
 assumes resetTimer_ccorres:
   "ccorres dc xfdc \<top> UNIV []
            (doMachineOp resetTimer)

diff --git a/proof/crefine/AARCH64/Refine_C.thy b/proof/crefine/AARCH64/Refine_C.thy
@@ -1229,8 +1229,8 @@ lemma ccorres_underlying_Fault:
 lemma monadic_rewrite_\<Gamma>:
   "monadic_rewrite True False \<top>
     (exec_C \<Gamma> c)
-    (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c)"
-  using spec_refine [of symbol_table domain]
+    (exec_C (kernel_all_multi.\<Gamma> symbol_table cpuNum) c)"
+  using spec_refine [of symbol_table cpuNum domain]
   using spec_simulates_to_exec_simulates
   apply (clarsimp simp: spec_statefn_simulates_via_statefn
                         o_def map_option_case monadic_rewrite_def exec_C_def
@@ -1247,8 +1247,8 @@ lemma no_fail_getActiveIRQ_C:
   done
 
 lemma kernel_all_subset_kernel:
-  "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop)
-       (kernel_global.kernel_call_C symbol_table fp)
+  "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop)
+       (kernel_global.kernel_call_C symbol_table cpuNum fp)
        \<subseteq> global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)"
   apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def
                         relcomp_unfold in_lift_state_relation_eq)
@@ -1298,7 +1298,7 @@ lemma kernel_all_subset_kernel:
   done
 
 theorem true_refinement:
-  "kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop
+  "kernel_global.ADT_C symbol_table armKSKernelVSpace_C cpuNum uop
    \<sqsubseteq> ADT_H uop"
   apply (rule refinement_trans[OF _ refinement2])
   apply (simp add: kernel_global.ADT_C_def ADT_C_def)
@@ -1310,7 +1310,7 @@ theorem true_refinement:
   done
 
 theorem true_fp_refinement:
-  "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop
+  "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop
    \<sqsubseteq> ADT_H uop"
   apply (rule refinement_trans[OF _ fp_refinement])
   apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def)

diff --git a/proof/crefine/AARCH64/SR_lemmas_C.thy b/proof/crefine/AARCH64/SR_lemmas_C.thy
@@ -2567,9 +2567,9 @@ lemma unat_scast_numDomains:
 
 (* link up Kernel_Config loaded from the seL4 build system with physBase in C code *)
 lemma physBase_spec:
-  "\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }"
+  "\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. cpuNum = 0 \<longrightarrow> ret__unsigned_long_' t = Kernel_Config.physBase }"
   apply (rule allI, rule conseqPre, vcg)
-  apply (simp add: Kernel_Config.physBase_def)
+  apply (simp add: Kernel_Config.physBase_def ph_base_def)
   done
 
 lemma rf_sr_obj_update_helper:

diff --git a/proof/crefine/AARCH64/SyscallArgs_C.thy b/proof/crefine/AARCH64/SyscallArgs_C.thy
@@ -15,8 +15,8 @@ begin
 
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
 context kernel_m begin
-abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
-lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
+abbreviation "msgRegistersC \<equiv> kernel_all_global_addresses.msgRegisters"
+lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def
 end
 
 context begin interpretation Arch . (*FIXME: arch-split*)

diff --git a/proof/crefine/AARCH64/Tcb_C.thy b/proof/crefine/AARCH64/Tcb_C.thy
@@ -1106,10 +1106,10 @@ lemma Arch_performTransfer_ccorres:
   done
 
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
-abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters"
-lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def
-abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters"
-lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def
+abbreviation "frameRegistersC \<equiv> kernel_all_global_addresses.frameRegisters"
+lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def
+abbreviation "gpRegistersC \<equiv> kernel_all_global_addresses.gpRegisters"
+lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def
 
 lemma frame_gp_registers_convs:
   "length AARCH64_H.frameRegisters = unat n_frameRegisters"

diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy
@@ -327,7 +327,7 @@ lemma addrFromKPPtr_spec:
    \<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
   apply vcg
   apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
-                   kernelELFBase_def pptrBase_def mask_def)
+                   kernelELFBase_def pptrBase_def mask_def cpu_0)
   done
 
 (* FIXME: move *)
@@ -1576,8 +1576,8 @@ lemma setRegister_ccorres:
 
 lemma msgRegisters_ccorres:
   "n < unat n_msgRegisters \<Longrightarrow>
-  register_from_H (AARCH64_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)"
-  apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def)
+  register_from_H (AARCH64_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)"
+  apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def)
   apply (simp add: Arrays.update_def n_msgRegisters_def nth_Cons' split: if_split)
   done
 

diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy
@@ -12,7 +12,7 @@ theory Wellformed_C
 imports
   "CLib.CTranslationNICTA"
   CLevityCatch
-  "CSpec.Substitute"
+  "CSpec.Multikernel_C"
 begin
 
 context begin interpretation Arch . (*FIXME: arch-split*)

diff --git a/proof/crefine/ARM/ADT_C.thy b/proof/crefine/ARM/ADT_C.thy
@@ -1552,7 +1552,7 @@ where
 
 end
 
-locale kernel_global = state_rel + kernel_all_global_addresses
+locale kernel_global = state_rel + kernel_all_multi
 (* note we're in the c-parser's locale now, not the substitute *)
 begin
 

diff --git a/proof/crefine/ARM/Ipc_C.thy b/proof/crefine/ARM/Ipc_C.thy
@@ -278,9 +278,9 @@ lemma ccap_relation_reply_helpers:
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
 (*FIXME: fupdate simplification issues for 2D arrays *)
 abbreviation "syscallMessageC \<equiv>  kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
-lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
-abbreviation "exceptionMessageC \<equiv> kernel_all_substitute.fault_messages.[unat MessageID_Exception]"
-lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def
+lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def
+abbreviation "exceptionMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]"
+lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def
 
 lemma syscallMessage_ccorres:
   "n < unat n_syscallMessage
@@ -5551,6 +5551,7 @@ lemma receiveIPC_ccorres [corres]:
   apply (auto simp:  isCap_simps valid_cap'_def)
   done
 
+
 lemma sendSignal_dequeue_ccorres_helper:
   "ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest_'
            (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest

diff --git a/proof/crefine/ARM/Machine_C.thy b/proof/crefine/ARM/Machine_C.thy
@@ -15,6 +15,11 @@ imports Ctac_lemmas_C
 begin
 
 locale kernel_m = kernel +
+
+(* The current verification is for unicore only *)
+assumes cpu_0:
+  "cpuNum = 0"
+
 assumes resetTimer_ccorres:
   "ccorres dc xfdc \<top> UNIV []
            (doMachineOp resetTimer)

diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy
@@ -1079,8 +1079,8 @@ lemma ccorres_underlying_Fault:
 lemma monadic_rewrite_\<Gamma>:
   "monadic_rewrite True False \<top>
     (exec_C \<Gamma> c)
-    (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c)"
-  using spec_refine [of symbol_table domain]
+    (exec_C (kernel_all_multi.\<Gamma> symbol_table cpuNum) c)"
+  using spec_refine [of symbol_table cpuNum domain]
   using spec_simulates_to_exec_simulates
   apply (clarsimp simp: spec_statefn_simulates_via_statefn
                         o_def map_option_case monadic_rewrite_def exec_C_def
@@ -1097,8 +1097,8 @@ lemma no_fail_getActiveIRQ_C:
   done
 
 lemma kernel_all_subset_kernel:
-  "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop)
-       (kernel_global.kernel_call_C symbol_table fp)
+  "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop)
+       (kernel_global.kernel_call_C symbol_table cpuNum fp)
        \<subseteq> global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)"
   apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def
                         relcomp_unfold in_lift_state_relation_eq)
@@ -1148,7 +1148,7 @@ lemma kernel_all_subset_kernel:
   done
 
 theorem true_refinement:
-  "kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop
+  "kernel_global.ADT_C symbol_table armKSKernelVSpace_C cpuNum uop
    \<sqsubseteq> ADT_H uop"
   apply (rule refinement_trans[OF _ refinement2])
   apply (simp add: kernel_global.ADT_C_def ADT_C_def)
@@ -1160,7 +1160,7 @@ theorem true_refinement:
   done
 
 theorem true_fp_refinement:
-  "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop
+  "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop
    \<sqsubseteq> ADT_H uop"
   apply (rule refinement_trans[OF _ fp_refinement])
   apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def)

diff --git a/proof/crefine/ARM/SR_lemmas_C.thy b/proof/crefine/ARM/SR_lemmas_C.thy
@@ -2201,9 +2201,9 @@ lemma msgRegisters_size_sanity:
 
 (* link up Kernel_Config loaded from the seL4 build system with physBase in C code *)
 lemma physBase_spec:
-  "\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }"
+  "\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. cpuNum = 0 \<longrightarrow> ret__unsigned_long_' t = Kernel_Config.physBase }"
   apply (rule allI, rule conseqPre, vcg)
-  apply (simp add: Kernel_Config.physBase_def)
+  apply (simp add: Kernel_Config.physBase_def ph_base_def)
   done
 
 lemma rf_sr_obj_update_helper:

diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy
@@ -14,8 +14,8 @@ begin
 
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
 context kernel_m begin
-abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
-lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
+abbreviation "msgRegistersC \<equiv> kernel_all_global_addresses.msgRegisters"
+lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def
 end
 
 context begin interpretation Arch . (*FIXME: arch-split*)

diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy
@@ -1036,10 +1036,10 @@ lemma Arch_performTransfer_ccorres:
   done
 
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
-abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters"
-lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def
-abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters"
-lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def
+abbreviation "frameRegistersC \<equiv> kernel_all_global_addresses.frameRegisters"
+lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def
+abbreviation "gpRegistersC \<equiv> kernel_all_global_addresses.gpRegisters"
+lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def
 
 lemma frame_gp_registers_convs:
   "length ARM_H.frameRegisters = unat n_frameRegisters"

diff --git a/proof/crefine/ARM/VSpace_C.thy b/proof/crefine/ARM/VSpace_C.thy
@@ -710,15 +710,15 @@ lemma ptrFromPAddr_spec:
    Call ptrFromPAddr_'proc
    \<lbrace>\<acute>ret__ptr_to_void =  Ptr (ptrFromPAddr (paddr_' s))\<rbrace>"
   apply vcg
-  apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def)
+  apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def cpu_0)
   done
 
 lemma addrFromPPtr_spec:
   "\<forall>s. \<Gamma> \<turnstile> {s}
    Call addrFromPPtr_'proc
    \<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\<rbrace>"
   apply vcg
-  apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def)
+  apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def cpu_0)
   done
 
 lemma addrFromKPPtr_spec:
@@ -727,7 +727,7 @@ lemma addrFromKPPtr_spec:
    \<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
   apply vcg
   apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
-                   kernelELFBase_def pptrBase_def mask_def)
+                   kernelELFBase_def pptrBase_def mask_def cpu_0)
   done
 
 abbreviation
@@ -1715,8 +1715,8 @@ lemma setRegister_ccorres:
 
 lemma msgRegisters_ccorres:
   "n < unat n_msgRegisters \<Longrightarrow>
-  register_from_H (ARM_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)"
-  apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def)
+  register_from_H (ARM_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)"
+  apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def)
   apply (simp add: Arrays.update_def n_msgRegisters_def nth_Cons' split: if_split)
   done
 

diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy
@@ -11,7 +11,7 @@ theory Wellformed_C
 imports
   "CLib.CTranslationNICTA"
   CLevityCatch
-  "CSpec.Substitute"
+  "CSpec.Multikernel_C"
 begin
 
 context begin interpretation Arch . (*FIXME: arch-split*)

diff --git a/proof/crefine/ARM_HYP/ADT_C.thy b/proof/crefine/ARM_HYP/ADT_C.thy
@@ -1718,7 +1718,7 @@ where
 
 end
 
-locale kernel_global = state_rel + kernel_all_global_addresses
+locale kernel_global = state_rel + kernel_all_multi
 (* note we're in the c-parser's locale now, not the substitute *)
 begin
 

diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy
@@ -2776,7 +2776,7 @@ lemma decodeARMFrameInvocation_ccorres:
                 apply (clarsimp dest!: ccap_relation_PageCap_generics)
                 apply (clarsimp simp: hd_drop_conv_nth hd_conv_nth)
                 (* sync up preprocessor-defined number sources coming from C *)
-                apply (clarsimp simp: fromPAddr_def paddrTop_def pptrBase_def pptrTop_def
+                apply (clarsimp simp: fromPAddr_def paddrTop_def pptrBase_def pptrTop_def cpu_0
                                       pptrBaseOffset_def add.commute from_bool_eq_if')
                apply ceqv
 

diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy
@@ -349,9 +349,9 @@ lemma ccap_relation_reply_helpers:
 (*FIXME: arch-split: C kernel names hidden by Haskell names *)
 (*FIXME: fupdate simplification issues for 2D arrays *)
 abbreviation "syscallMessageC \<equiv>  kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
-lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
-abbreviation "exceptionMessageC \<equiv> kernel_all_substitute.fault_messages.[unat MessageID_Exception]"
-lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def
+lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def
+abbreviation "exceptionMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]"
+lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def
 
 lemma syscallMessage_ccorres:
   "n < unat n_syscallMessage
@@ -6076,6 +6076,7 @@ lemma receiveIPC_ccorres [corres]:
   apply (auto simp:  isCap_simps valid_cap'_def)
   done
 
+
 lemma sendSignal_dequeue_ccorres_helper:
   "ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest_'
            (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest

diff --git a/proof/crefine/ARM_HYP/Machine_C.thy b/proof/crefine/ARM_HYP/Machine_C.thy
@@ -25,6 +25,11 @@ where
   "setCurrentPDPL2 = undefined"
 
 locale kernel_m = kernel +
+
+(* The current verification is for unicore only *)
+assumes cpu_0:
+  "cpuNum = 0"
+
 assumes resetTimer_ccorres:
   "ccorres dc xfdc \<top> UNIV []
            (doMachineOp resetTimer)
-Original file line number
+Diff line change
@@ Expand Up / @@ -1552,7 +1552,7 @@ where @@
     end
-    locale kernel_global = state_rel + kernel_all_global_addresses
+    locale kernel_global = state_rel + kernel_all_multi
     (* note we're in the c-parser's locale now, not the substitute *)
     begin
@@ Expand Down @@