diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy
index 7699df732..b933f6225 100644
--- a/proof/invariant-abstract/ADT_AI.thy
+++ b/proof/invariant-abstract/ADT_AI.thy
@@ -183,7 +183,7 @@ definition
   check_active_irq :: "(bool,'z :: state_ext) s_monad"
   where
   "check_active_irq \<equiv> do
-      irq \<leftarrow> do_machine_op getActiveIRQ;
+      irq \<leftarrow> do_machine_op $ getActiveIRQ False;
       return (irq \<noteq> None)
   od"
 
diff --git a/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy
index 20047ec5c..97a56fa5c 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy
@@ -23,7 +23,7 @@ named_theorems CSpace_AI_assms
 (* FIXME: move? *)
 lemma getActiveIRQ_wp [CSpace_AI_assms]:
   "irq_state_independent_A P \<Longrightarrow>
-   valid P (do_machine_op getActiveIRQ) (\<lambda>_. P)"
+   valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)"
   apply (simp add: getActiveIRQ_def do_machine_op_def split_def exec_gets
                    select_f_select[simplified liftM_def]
                    select_modify_comm gets_machine_state_modify)
diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
index b543dbc57..5562eb5f0 100644
--- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
@@ -328,7 +328,7 @@ lemma no_fail_freeMemory[simp, wp]:
 
 
 lemma no_fail_getActiveIRQ[wp]:
-  "no_fail \<top> getActiveIRQ"
+  "no_fail \<top> (getActiveIRQ in_kernel)"
   apply (simp add: getActiveIRQ_def)
   apply (rule no_fail_pre)
    apply (wp non_fail_select)
@@ -338,7 +338,7 @@ lemma no_fail_getActiveIRQ[wp]:
 definition "irq_state_independent P \<equiv> \<forall>f s. P s \<longrightarrow> P (irq_state_update f s)"
 
 lemma getActiveIRQ_inv [wp]:
-  "\<lbrakk>irq_state_independent P\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv. P\<rbrace>"
+  "\<lbrakk>irq_state_independent P\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv. P\<rbrace>"
   apply (simp add: getActiveIRQ_def)
   apply (wp alternative_wp select_wp)
   apply (simp add: irq_state_independent_def)
@@ -529,7 +529,7 @@ lemma no_irq_loadWord: "no_irq (loadWord x)"
   done
 
 
-lemma no_irq_getActiveIRQ: "no_irq getActiveIRQ"
+lemma no_irq_getActiveIRQ: "no_irq (getActiveIRQ in_kernel)"
   apply (clarsimp simp: no_irq_def)
   apply (rule getActiveIRQ_inv)
   apply (simp add: irq_state_independent_def)
@@ -671,7 +671,7 @@ lemma no_irq_clearMemory: "no_irq (clearMemory a b)"
   done
 
 lemma getActiveIRQ_le_maxIRQ':
-  "\<lbrace>\<lambda>s. \<forall>irq > maxIRQ. irq_masks s irq\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
+  "\<lbrace>\<lambda>s. \<forall>irq > maxIRQ. irq_masks s irq\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
   apply (simp add: getActiveIRQ_def)
   apply (wp alternative_wp select_wp)
   apply clarsimp
@@ -681,12 +681,28 @@ lemma getActiveIRQ_le_maxIRQ':
 
 (* FIXME: follows already from getActiveIRQ_le_maxIRQ *)
 lemma getActiveIRQ_neq_Some0xFF':
-  "\<lbrace>\<top>\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
+  "\<lbrace>\<top>\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
   apply (simp add: getActiveIRQ_def)
   apply (wp alternative_wp select_wp)
   apply simp
   done
 
+lemma getActiveIRQ_neq_non_kernel:
+  "\<lbrace>\<top>\<rbrace> getActiveIRQ True \<lbrace>\<lambda>rv s. rv \<notin> Some ` non_kernel_IRQs \<rbrace>"
+  apply (simp add: getActiveIRQ_def)
+  apply (wp alternative_wp select_wp)
+  apply auto
+  done
+
+lemma dmo_getActiveIRQ_non_kernel[wp]:
+  "\<lbrace>\<top>\<rbrace> do_machine_op (getActiveIRQ True)
+   \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> irq \<in> non_kernel_IRQs \<longrightarrow> P irq s\<rbrace>"
+  unfolding do_machine_op_def
+  apply wpsimp
+  apply (drule use_valid, rule getActiveIRQ_neq_non_kernel, rule TrueI)
+  apply clarsimp
+  done
+
 lemma empty_fail_isb: "empty_fail  isb"
   by (simp add: isb_def)
 
diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy
index a8e90ab83..ff34a1eaf 100644
--- a/proof/invariant-abstract/CSpace_AI.thy
+++ b/proof/invariant-abstract/CSpace_AI.thy
@@ -114,7 +114,7 @@ locale CSpace_AI_getActiveIRQ_wp =
   fixes state_ext_t :: "'state_ext::state_ext itself"
   assumes getActiveIRQ_wp[wp]:
     "\<And>P :: 'state_ext state \<Rightarrow> bool.
-      irq_state_independent_A P \<Longrightarrow> valid P (do_machine_op getActiveIRQ) (\<lambda>_. P)"
+      irq_state_independent_A P \<Longrightarrow> valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)"
 
 
 lemma OR_choiceE_weak_wp:
diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy
index ac607366d..5fd16ec10 100644
--- a/proof/invariant-abstract/EmptyFail_AI.thy
+++ b/proof/invariant-abstract/EmptyFail_AI.thy
@@ -450,7 +450,7 @@ locale EmptyFail_AI_call_kernel = EmptyFail_AI_schedule state_ext_t
   assumes activate_thread_empty_fail[wp]:
     "empty_fail (activate_thread :: (unit, 'state_ext) s_monad)"
   assumes getActiveIRQ_empty_fail[wp]:
-    "empty_fail getActiveIRQ"
+    "empty_fail (getActiveIRQ in_kernel)"
   assumes handle_event_empty_fail[wp]:
     "\<And>event. empty_fail (handle_event event :: (unit, 'state_ext) p_monad)"
   assumes handle_interrupt_empty_fail[wp]:
diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy
index 6df38f193..6e4cb258c 100644
--- a/proof/invariant-abstract/KHeap_AI.thy
+++ b/proof/invariant-abstract/KHeap_AI.thy
@@ -57,6 +57,9 @@ requalify_facts
   wellformed_arch_obj_same_type
   default_arch_object_not_live
   default_tcb_not_live
+
+  getActiveIRQ_neq_non_kernel
+  dmo_getActiveIRQ_non_kernel
 end
 
 lemmas cap_is_device_obj_is_device[simp] = cap_is_device_obj_is_device