archirq: Remove redundant invocation, renamed

arch_decode_interrupt_control.
2016-01-14 15:01:46 +11:00 · 2016-01-14 15:01:46 +11:00 · efb4c61816
parent dcce50ce79
commit efb4c61816
25 changed files with 77 additions and 90 deletions
--- a/proof/crefine/Interrupt_C.thy
+++ b/proof/crefine/Interrupt_C.thy
@ -367,13 +367,13 @@ lemma Platform_maxIRQ:
  "Platform.maxIRQ = scast Kernel_C.maxIRQ"
  by (simp add: Platform.maxIRQ_def Kernel_C.maxIRQ_def)

-lemma Arch_decodeInterruptControl_ccorres:
+lemma Arch_decodeIRQControlInvocation_ccorres:
  "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
      \<top> UNIV []
-     (decodeInterruptControl args extraCaps
-        >>= invocationCatch thread isBlocking isCall (InvokeIRQControl o InterruptControl))
-     (Call Arch_decodeInterruptControl_'proc)"
-  apply (cinit' simp: decodeInterruptControl_def)
+     (ArchInterrupt_H.decodeIRQControlInvocation label args srcSlot extraCaps
+        >>= invocationCatch thread isBlocking isCall (InvokeIRQControl o ArchIRQControl))
+     (Call Arch_decodeIRQControlInvocation_'proc)"
+  apply (cinit' simp: ArchInterrupt_H.decodeIRQControlInvocation_def)
   apply (simp add: throwError_bind invocationCatch_def
              cong: StateSpace.state.fold_congs globals.fold_congs)
   apply (rule syscall_error_throwError_ccorres_n)
@ -395,6 +395,10 @@ lemma maxIRQ_ucast_scast [simp]:
  "ucast (scast Kernel_C.maxIRQ :: word8) = scast Kernel_C.maxIRQ"
  by (clarsimp simp: Kernel_C.maxIRQ_def)

+lemma decodeIRQ_arch_helper: "x \<noteq> invocation_label.IRQIssueIRQHandler \<Longrightarrow> 
+         (case x of invocation_label.IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g"
+  by (clarsimp split: invocation_label.splits)
+  
 lemma decodeIRQControlInvocation_ccorres:
  notes if_cong[cong] tl_drop_1[simp]
  shows
@ -524,19 +528,15 @@ lemma decodeIRQControlInvocation_ccorres:
     apply wp
    apply (simp add: Collect_const_mem all_ex_eq_helper)
    apply (vcg exspec=getSyscallArg_modifies)
-   apply (rule ccorres_Cond_rhs)
-    apply (simp add: liftME_invocationCatch)
-    apply (rule ccorres_add_returnOk)
-    apply (ctac add: Arch_decodeInterruptControl_ccorres)
-       apply (rule ccorres_return_CE, simp+)[1]
-      apply (rule ccorres_return_C_errorE, simp+)[1]
-     apply wp
-    apply vcg
-   apply (rule ccorres_equals_throwError)
-    apply (fastforce simp: throwError_bind invocationCatch_def
-                   split: invocation_label.split)
-   apply (rule syscall_error_throwError_ccorres_n)
-   apply (simp add: syscall_error_to_H_cases)
+   apply (clarsimp simp: decodeIRQ_arch_helper)
+   apply (simp add: liftME_invocationCatch)
+   apply (rule ccorres_add_returnOk)
+   apply (ctac add: Arch_decodeIRQControlInvocation_ccorres)
+      apply (rule ccorres_return_CE, simp+)[1]
+     apply (rule ccorres_return_C_errorE, simp+)[1]
+    apply wp
+   apply vcg
+  apply (simp add: syscall_error_to_H_cases)
  apply (clarsimp simp: if_1_0_0 interpret_excaps_test_null excaps_map_def
                        Collect_const_mem word_sless_def word_sle_def
                        ThreadState_Restart_def unat_of_nat mask_def
--- a/proof/drefine/Interrupt_DR.thy
+++ b/proof/drefine/Interrupt_DR.thy
@ -18,9 +18,8 @@ lemma decode_irq_control_error_corres:
      (throwError e)
      (Decode_A.decode_irq_control_invocation label args slot (map fst excaps))"
  apply (unfold decode_irq_control_invocation_def)
-  apply (cases "invocation_type label", simp_all)
+  apply (cases "invocation_type label"; simp add: arch_decode_irq_control_invocation_def)
   apply (simp add: transform_intent_def transform_intent_issue_irq_handler_def split: list.splits)
-  apply (simp add: transform_intent_def)
  done

 (* Interrupt Control Invocations *)
@ -91,9 +90,7 @@ lemma decode_irq_control_corres:
   apply wp
   apply (cases excaps', auto)[1]
   apply wp[1]
-  apply (cases "invocation_type label' = IRQInterruptControl")
-   apply (clarsimp simp: arch_decode_interrupt_control_def transform_intent_def)
-  apply clarsimp
+  apply (clarsimp simp: arch_decode_irq_control_invocation_def transform_intent_def)
  apply (rule corres_guard_imp)
    apply (cases ui)
     apply (auto simp: dcorres_alternative_throw)
--- a/proof/drefine/StateTranslation_D.thy
+++ b/proof/drefine/StateTranslation_D.thy
@ -327,8 +327,6 @@ definition
    | IRQIssueIRQHandler \<Rightarrow>
          map_option IrqControlIntent
                   (transform_intent_issue_irq_handler args)
-    | IRQInterruptControl \<Rightarrow>
-          Some (IrqControlIntent IrqControlInterruptControlIntent)
    | IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent)
    | IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent)
    | IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent)
@ -396,7 +394,6 @@ lemma transform_tcb_intent_invocation:
    label \<noteq> CNodeRotate \<and>
    label \<noteq> CNodeSaveCaller \<and>
    label \<noteq> IRQIssueIRQHandler \<and>
-    label \<noteq> IRQInterruptControl \<and>
    label \<noteq> IRQAckIRQ \<and>
    label \<noteq> IRQSetIRQHandler \<and>
    label \<noteq> IRQClearIRQHandler \<and>
--- a/proof/drefine/Syscall_DR.thy
+++ b/proof/drefine/Syscall_DR.thy
@ -428,12 +428,12 @@ lemma transform_intent_irq_control_None:
      \<Longrightarrow> \<lbrace>op = s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. op = s\<rbrace>"
  apply (clarsimp simp:Decode_A.decode_invocation_def)
    apply wp
-  apply (clarsimp simp:decode_irq_control_invocation_def split del:if_splits)
+  apply (clarsimp simp:decode_irq_control_invocation_def arch_decode_irq_control_invocation_def split del:if_splits)
  apply (case_tac "invocation_type label")
    apply (clarsimp,wp)+
    apply (clarsimp simp:transform_intent_issue_irq_handler_def transform_intent_def split:list.split_asm split del:if_splits,wp)
-    apply (clarsimp simp:arch_decode_interrupt_control_def,wp)+
-done
+    apply (clarsimp simp:arch_decode_irq_control_invocation_def,wp)+
+  done

 lemma transform_intent_irq_handler_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQHandlerCap w\<rbrakk>
--- a/proof/infoflow/Decode_IF.thy
+++ b/proof/infoflow/Decode_IF.thy
@ -277,7 +277,7 @@ lemma decode_irq_control_invocation_rev:
  apply (wp ensure_empty_rev lookup_slot_for_cnode_op_rev 
            is_irq_active_rev whenE_inv
        | wp_once hoare_drop_imps 
-        | simp add: Let_def arch_decode_interrupt_control_def)+
+        | simp add: Let_def arch_decode_irq_control_invocation_def)+
  apply safe
       apply simp+
    apply(blast intro: aag_Control_into_owns_irq)
--- a/proof/invariant-abstract/EmptyFail_AI.thy
+++ b/proof/invariant-abstract/EmptyFail_AI.thy
@ -334,8 +334,8 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail:
 lemma arch_decode_invocation_empty_fail[wp]:
  "empty_fail (arch_decode_invocation label b c d e f)"
  apply (case_tac "invocation_type label")
-  prefer 44  
-  prefer 45
+  prefer 43  
+  prefer 44
  apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2]  
  by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+)

--- a/proof/invariant-abstract/Interrupt_AI.thy
+++ b/proof/invariant-abstract/Interrupt_AI.thy
@ -37,7 +37,7 @@ where
 primrec
  irq_control_inv_valid :: "irq_control_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
 where
-  "irq_control_inv_valid (Invocations_A.InterruptControl ivk) = \<bottom>"
+  "irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = \<bottom>"
 | "irq_control_inv_valid (Invocations_A.IRQControl irq ptr ptr') =
       (cte_wp_at (op = cap.NullCap) ptr and
        cte_wp_at (op = cap.IRQControlCap) ptr'
@ -72,7 +72,7 @@ crunch inv[wp]: is_irq_active "P"
 lemma decode_irq_control_invocation_inv[wp]:
  "\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>"
  apply (simp add: decode_irq_control_invocation_def Let_def
-                   arch_decode_interrupt_control_def whenE_def, safe)
+                   arch_decode_irq_control_invocation_def whenE_def, safe)
  apply (wp | simp)+
  done

@ -85,7 +85,7 @@ lemma decode_irq_control_valid[wp]:
   \<lbrace>irq_control_inv_valid\<rbrace>,-"
  apply (simp add: decode_irq_control_invocation_def Let_def split_def
                   lookup_target_slot_def whenE_def
-                   arch_decode_interrupt_control_def
+                   arch_decode_irq_control_invocation_def
                 split del: split_if cong: if_cong)
  apply (rule hoare_pre)
   apply (wp ensure_empty_stronger | simp add: cte_wp_at_eq_simp
--- a/proof/refine/Interrupt_R.thy
+++ b/proof/refine/Interrupt_R.thy
@ -26,15 +26,15 @@ where
 | "irq_handler_inv_relation (Invocations_A.SetMode irq trig pol) x = (x = SetMode irq trig pol)"

 consts
-  interrupt_control_relation :: "arch_interrupt_control \<Rightarrow> interrupt_control \<Rightarrow> bool"
+  interrupt_control_relation :: "arch_irq_control_invocation \<Rightarrow> ArchRetypeDecls_H.irqcontrol_invocation \<Rightarrow> bool"

 primrec
  irq_control_inv_relation :: "irq_control_invocation \<Rightarrow> irqcontrol_invocation \<Rightarrow> bool"
 where
  "irq_control_inv_relation (Invocations_A.IRQControl irq slot slot') x
       = (x = IssueIRQHandler irq (cte_map slot) (cte_map slot'))"
-| "irq_control_inv_relation (Invocations_A.InterruptControl ivk) x
-       = (\<exists>ivk'. x = InterruptControl ivk' \<and> interrupt_control_relation ivk ivk')"
+| "irq_control_inv_relation (Invocations_A.ArchIRQControl ivk) x
+       = (\<exists>ivk'. x = ArchIRQControl ivk' \<and> interrupt_control_relation ivk ivk')"

 primrec
  irq_handler_inv_valid' :: "irqhandler_invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -52,7 +52,7 @@ where
 primrec
  irq_control_inv_valid' :: "irqcontrol_invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
-  "irq_control_inv_valid' (InterruptControl ivk) = \<bottom>"
+  "irq_control_inv_valid' (ArchIRQControl ivk) = \<bottom>"
 | "irq_control_inv_valid' (IssueIRQHandler irq ptr ptr') =
       (cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) ptr and
        cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) ptr' and
@ -136,7 +136,7 @@ lemma decode_irq_control_corres:
     (decode_irq_control_invocation label args slot caps)
     (decodeIRQControlInvocation label args (cte_map slot) caps')"
  apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def
-                        decodeInterruptControl_def arch_decode_interrupt_control_def
+                        ArchInterrupt_H.decodeIRQControlInvocation_def arch_decode_irq_control_invocation_def
             split del: split_if cong: if_cong
                 split: invocation_label.split)
  apply (cases caps, simp split: list.split)
@ -165,7 +165,7 @@ lemma decode_irq_control_corres:
  done

 crunch inv[wp]: decodeIRQControlInvocation "P"
-  (simp: crunch_simps decodeInterruptControl_def)
+  (simp: crunch_simps ArchInterrupt_H.decodeIRQControlInvocation_def)

 (* Levity: added (20090201 10:50:27) *)
 declare ensureEmptySlot_stronger [wp]
@ -197,7 +197,7 @@ lemma decode_irq_control_valid'[wp]:
  apply (rule hoare_pre)
   apply (wp ensureEmptySlot_stronger isIRQActive_wp
             whenE_throwError_wp
-                | simp add: decodeInterruptControl_def | wpc
+                | simp add: ArchInterrupt_H.decodeIRQControlInvocation_def | wpc
                | wp_once hoare_drop_imps)+
  apply (clarsimp simp: minIRQ_def maxIRQ_def
                        toEnum_of_nat word_le_nat_alt unat_of_nat)
@ -348,7 +348,7 @@ lemma invoke_irq_control_corres:
   apply (case_tac ctea)
   apply (clarsimp simp: isCap_simps sameRegionAs_def3)
   apply (auto dest: valid_irq_handlers_ctes_ofD)[1]
-  apply (clarsimp simp: arch_invoke_irq_control_def invokeInterruptControl_def)
+  apply (clarsimp simp: arch_invoke_irq_control_def ArchInterrupt_H.invokeIRQControl_def)
  done

 crunch valid_cap'[wp]: setIRQState "valid_cap' cap"
--- a/proof/refine/Orphanage.thy
+++ b/proof/refine/Orphanage.thy
@ -1968,7 +1968,7 @@ lemma invokeIRQControl_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   invokeIRQControl i
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
-  apply (cases i, simp_all add: invokeIRQControl_def invokeInterruptControl_def)
+  apply (cases i, simp_all add: invokeIRQControl_def ArchInterrupt_H.invokeIRQControl_def)
  apply (wp | clarsimp)+
  done

--- a/proof/refine/PageTableDuplicates.thy
+++ b/proof/refine/PageTableDuplicates.thy
@ -2041,9 +2041,9 @@ crunch valid_duplicates'[wp]:
 lemma invokeIRQControl_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<rbrace> invokeIRQControl a
  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
-  apply (simp add:invokeIRQControl_def invokeInterruptControl_def)
+  apply (simp add:invokeIRQControl_def ArchInterrupt_H.invokeIRQControl_def)
  apply (rule hoare_pre)
-  apply (wp|wpc | simp add:invokeInterruptControl_def)+
+  apply (wp|wpc | simp add:ArchInterrupt_H.invokeIRQControl_def)+
  apply fastforce
 done

@ -2052,7 +2052,7 @@ lemma invokeIRQHandler_valid_duplicates'[wp]:
  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
  apply (simp add:invokeIRQHandler_def)
  apply (rule hoare_pre)
-  apply (wp|wpc | simp add:invokeInterruptControl_def)+
+  apply (wp|wpc | simp add: ArchInterrupt_H.invokeIRQControl_def)+
  done

 lemma invokeCNode_valid_duplicates'[wp]:
--- a/proof/refine/Syscall_R.thy
+++ b/proof/refine/Syscall_R.thy
@ -2397,7 +2397,7 @@ lemma inv_irq_IRQInactive:
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>"
  apply (simp add: invokeIRQControl_def)
  apply (rule hoare_pre)
-   apply (wpc|wp|simp add: invokeInterruptControl_def)+
+   apply (wpc|wp|simp add: ArchInterrupt_H.invokeIRQControl_def)+
  done

 lemma inv_arch_IRQInactive:
--- a/spec/abstract/ArchInvocation_A.thy
+++ b/spec/abstract/ArchInvocation_A.thy
@ -70,6 +70,6 @@ datatype arch_invocation
     | InvokeASIDPool asid_pool_invocation

 -- "There are no additional interrupt control operations on ARM."
-typedecl arch_interrupt_control
+typedecl arch_irq_control_invocation

 end
--- a/spec/abstract/Arch_A.thy
+++ b/spec/abstract/Arch_A.thy
@ -23,7 +23,7 @@ definition "page_bits \<equiv> pageBits"
 text {* The ARM architecture does not provide any additional operations on its
 interrupt controller. *}
 definition
-  arch_invoke_irq_control :: "arch_interrupt_control \<Rightarrow> (unit,'z::state_ext) p_monad" where
+  arch_invoke_irq_control :: "arch_irq_control_invocation \<Rightarrow> (unit,'z::state_ext) p_monad" where
  "arch_invoke_irq_control aic \<equiv> fail"

 text {* Switch to a thread's virtual address space context and write its IPC
--- a/spec/abstract/Decode_A.thy
+++ b/spec/abstract/Decode_A.thy
@ -279,9 +279,9 @@ where

 text "ARM does not support additional interrupt control operations"
 definition
-  arch_decode_interrupt_control ::
-  "data list \<Rightarrow> cap list \<Rightarrow> (arch_interrupt_control,'z::state_ext) se_monad" where
-  "arch_decode_interrupt_control d cs \<equiv> throwError IllegalOperation"
+  arch_decode_irq_control_invocation ::
+  "data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap list \<Rightarrow> (arch_irq_control_invocation,'z::state_ext) se_monad" where
+  "arch_decode_irq_control_invocation label args slot excaps \<equiv> throwError IllegalOperation"

 section "CNode"

@ -645,10 +645,7 @@ definition
        returnOk $ IRQControl irqv dest_slot src_slot
      odE
    else throwError TruncatedMessage
-  else if invocation_type label = IRQInterruptControl
-    then liftME InterruptControl
-         $ arch_decode_interrupt_control args cps
-  else throwError IllegalOperation)"
+  else liftME ArchIRQControl $ arch_decode_irq_control_invocation label args src_slot cps)"

 definition
  data_to_bool :: "data \<Rightarrow> bool"
--- a/spec/abstract/Interrupt_A.thy
+++ b/spec/abstract/Interrupt_A.thy
@ -32,7 +32,7 @@ where
  "invoke_irq_control (IRQControl irq handler_slot control_slot) = 
     liftE (do set_irq_state IRQSignal irq;
               cap_insert (IRQHandlerCap irq) control_slot handler_slot od)"
-| "invoke_irq_control (InterruptControl invok) =
+| "invoke_irq_control (ArchIRQControl invok) =
     arch_invoke_irq_control invok"

 text {* The IRQHandler capability may be used to configure how interrupts on an
--- a/spec/abstract/Invocations_A.thy
+++ b/spec/abstract/Invocations_A.thy
@ -49,7 +49,7 @@ datatype tcb_invocation =

 datatype irq_control_invocation =
    IRQControl irq cslot_ptr cslot_ptr
-  | InterruptControl arch_interrupt_control
+  | ArchIRQControl arch_irq_control_invocation

 datatype irq_handler_invocation =
    ACKIrq irq
--- a/spec/capDL/Intents_D.thy
+++ b/spec/capDL/Intents_D.thy
@ -134,7 +134,7 @@ datatype cdl_irq_control_intent =
    (* IssueIrqHandler: (target), irq, (root), index, depth *)
    IrqControlIssueIrqHandlerIntent word8 word32 word32
    (* InterruptControl *)
- |  IrqControlInterruptControlIntent
+ |  IrqControlArchIrqControlIntent

 datatype cdl_page_table_intent =
    (* Map: (target), (pd), vaddr, attr *)
--- a/spec/capDL/Interrupt_D.thy
+++ b/spec/capDL/Interrupt_D.thy
@ -47,7 +47,7 @@ where
          dest_slot_cap_ref \<leftarrow> lookup_slot_for_cnode_op cnode_cap index (unat depth);
          returnOk $ IssueIrqHandler irq target_ref dest_slot_cap_ref
        odE \<sqinter> throw
-    | IrqControlInterruptControlIntent \<Rightarrow> throw
+    | IrqControlArchIrqControlIntent \<Rightarrow> throw
  "

 definition
--- a/spec/design/ArchInterrupt_H.thy
+++ b/spec/design/ArchInterrupt_H.thy
@ -13,14 +13,14 @@ imports RetypeDecls_H
 begin

 definition
-decodeInterruptControl :: "machine_word list \<Rightarrow> capability list \<Rightarrow> ( syscall_error , interrupt_control ) kernel_f"
+decodeIRQControlInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> capability list \<Rightarrow> ( syscall_error , ArchRetypeDecls_H.irqcontrol_invocation ) kernel_f"
 where
-"decodeInterruptControl arg1 arg2 \<equiv> throw IllegalOperation"
+"decodeIRQControlInvocation arg1 arg2 arg3 arg4 \<equiv> throw IllegalOperation"

 definition
-invokeInterruptControl :: "interrupt_control \<Rightarrow> unit kernel_p"
+invokeIRQControl :: "ArchRetypeDecls_H.irqcontrol_invocation \<Rightarrow> unit kernel_p"
 where
-"invokeInterruptControl arg1 \<equiv> haskell_fail []"
+"invokeIRQControl arg1 \<equiv> haskell_fail []"


 end
--- a/spec/design/ArchRetypeDecls_H.thy
+++ b/spec/design/ArchRetypeDecls_H.thy
@ -606,7 +606,7 @@ datatype invocation =
  | InvokeASIDControl asidcontrol_invocation
  | InvokeASIDPool asidpool_invocation

-typedecl interrupt_control
+typedecl irqcontrol_invocation

 datatype copy_register_sets =
    ARMNoExtraRegisters
--- a/spec/design/Interrupt_H.thy
+++ b/spec/design/Interrupt_H.thy
@ -68,9 +68,7 @@ defs decodeIRQControlInvocation_def:
            returnOk $ IssueIRQHandler irq destSlot srcSlot
          odE)
        | (IRQIssueIRQHandler,_,_) \<Rightarrow>   throw TruncatedMessage
-        | (IRQInterruptControl,_,_) \<Rightarrow>   liftME InterruptControl $
-            ArchInterrupt_H.decodeInterruptControl args extraCaps
-        | _ \<Rightarrow>   throw IllegalOperation
+        | _ \<Rightarrow>   liftME ArchIRQControl $ ArchInterrupt_H.decodeIRQControlInvocation label args srcSlot extraCaps
        )"

 defs invokeIRQControl_def:
@ -80,8 +78,8 @@ defs invokeIRQControl_def:
    setIRQState (IRQSignal) irq;
    cteInsert (IRQHandlerCap irq) controlSlot handlerSlot
  od)
-  | (InterruptControl invok) \<Rightarrow>   
-    ArchInterrupt_H.invokeInterruptControl invok
+  | (ArchIRQControl invok) \<Rightarrow>   
+    ArchInterrupt_H.invokeIRQControl invok
  )"

 defs decodeIRQHandlerInvocation_def:
--- a/spec/design/InvocationLabels_H.thy
+++ b/spec/design/InvocationLabels_H.thy
@ -42,7 +42,6 @@ datatype invocation_label =
  | CNodeRotate
  | CNodeSaveCaller
  | IRQIssueIRQHandler
-  | IRQInterruptControl
  | IRQAckIRQ
  | IRQSetIRQHandler
  | IRQClearIRQHandler
@ -116,7 +115,6 @@ definition
      CNodeRotate,
      CNodeSaveCaller,
      IRQIssueIRQHandler,
-      IRQInterruptControl,
      IRQAckIRQ,
      IRQSetIRQHandler,
      IRQClearIRQHandler,
--- a/spec/design/Invocations_H.thy
+++ b/spec/design/Invocations_H.thy
@ -760,14 +760,9 @@ lemma retypeNewSizeBits_retypeNewSizeBits_update [simp]:
  by (cases v) simp

 datatype irqcontrol_invocation =
-    InterruptControl ArchRetypeDecls_H.interrupt_control
+    ArchIRQControl ArchRetypeDecls_H.irqcontrol_invocation
  | IssueIRQHandler irq machine_word machine_word

-primrec
-  interruptControlArch :: "irqcontrol_invocation \<Rightarrow> ArchRetypeDecls_H.interrupt_control"
-where
-  "interruptControlArch (InterruptControl v0) = v0"
-
 primrec
  issueHandlerSlot :: "irqcontrol_invocation \<Rightarrow> machine_word"
 where
@ -784,9 +779,9 @@ where
  "issueHandlerControllerSlot (IssueIRQHandler v0 v1 v2) = v2"

 primrec
-  interruptControlArch_update :: "(ArchRetypeDecls_H.interrupt_control \<Rightarrow> ArchRetypeDecls_H.interrupt_control) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
+  archIRQControl :: "irqcontrol_invocation \<Rightarrow> ArchRetypeDecls_H.irqcontrol_invocation"
 where
-  "interruptControlArch_update f (InterruptControl v0) = InterruptControl (f v0)"
+  "archIRQControl (ArchIRQControl v0) = v0"

 primrec
  issueHandlerSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
@ -803,10 +798,15 @@ primrec
 where
  "issueHandlerControllerSlot_update f (IssueIRQHandler v0 v1 v2) = IssueIRQHandler v0 v1 (f v2)"

-abbreviation (input)
-  InterruptControl_trans :: "(ArchRetypeDecls_H.interrupt_control) \<Rightarrow> irqcontrol_invocation" ("InterruptControl'_ \<lparr> interruptControlArch= _ \<rparr>")
+primrec
+  archIRQControl_update :: "(ArchRetypeDecls_H.irqcontrol_invocation \<Rightarrow> ArchRetypeDecls_H.irqcontrol_invocation) \<Rightarrow> irqcontrol_invocation \<Rightarrow> irqcontrol_invocation"
 where
-  "InterruptControl_ \<lparr> interruptControlArch= v0 \<rparr> == InterruptControl v0"
+  "archIRQControl_update f (ArchIRQControl v0) = ArchIRQControl (f v0)"
+
+abbreviation (input)
+  ArchIRQControl_trans :: "(ArchRetypeDecls_H.irqcontrol_invocation) \<Rightarrow> irqcontrol_invocation" ("ArchIRQControl'_ \<lparr> archIRQControl= _ \<rparr>")
+where
+  "ArchIRQControl_ \<lparr> archIRQControl= v0 \<rparr> == ArchIRQControl v0"

 abbreviation (input)
  IssueIRQHandler_trans :: "(irq) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> irqcontrol_invocation" ("IssueIRQHandler'_ \<lparr> issueHandlerIRQ= _, issueHandlerSlot= _, issueHandlerControllerSlot= _ \<rparr>")
@ -814,10 +814,10 @@ where
  "IssueIRQHandler_ \<lparr> issueHandlerIRQ= v0, issueHandlerSlot= v1, issueHandlerControllerSlot= v2 \<rparr> == IssueIRQHandler v0 v1 v2"

 definition
-  isInterruptControl :: "irqcontrol_invocation \<Rightarrow> bool"
+  isArchIRQControl :: "irqcontrol_invocation \<Rightarrow> bool"
 where
- "isInterruptControl v \<equiv> case v of
-    InterruptControl v0 \<Rightarrow> True
+ "isArchIRQControl v \<equiv> case v of
+    ArchIRQControl v0 \<Rightarrow> True
  | _ \<Rightarrow> False"

 definition
--- a/spec/design/skel/ArchInterrupt_H.thy
+++ b/spec/design/skel/ArchInterrupt_H.thy
@ -12,6 +12,6 @@ theory ArchInterrupt_H
 imports RetypeDecls_H
 begin

-#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs
+#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs ArchInv=ArchRetypeDecls_H

 end
--- a/spec/design/version
+++ b/spec/design/version
@ -1,5 +1,5 @@
-Built from git repo at /home/tsewell/dev/verification/seL4/haskell by tsewell
+Built from git repo at /net/nfshome/export/home/insecure/jbeeren/work/test/seL4/haskell by jbeeren

 Generated from changeset:
-f7b60e9 Final patch to lookupSlot variants.
+d59b73d Remove redundant IRQInterruptControl invocation, and replace with a mechanism to actually decode arch specific IRQ invocations