diff --git a/spec/haskell/src/SEL4/API/Invocation/ARM_HYP.lhs b/spec/haskell/src/SEL4/API/Invocation/ARM_HYP.lhs
index 36cb78be8..8f23140fa 100644
--- a/spec/haskell/src/SEL4/API/Invocation/ARM_HYP.lhs
+++ b/spec/haskell/src/SEL4/API/Invocation/ARM_HYP.lhs
@@ -123,13 +123,13 @@ IO pages are invoked using InvokePage (cap contains a bit indicating it is an IO
 
 FIXME ARMHYP move HyperReg definition (to Hardware?)
 
-> type HyperReg = Word32 -- FIXME ARMHYP can abstract
+> type HyperReg = Int -- FIXME ARMHYP can abstract
 > type HyperRegVal = Word32 -- FIXME ARMHYP can abstract
 
 > data VCPUInvocation
 >     = VCPUSetTCB (PPtr VCPU) (PPtr TCB)
->     -- XXX ARMHYP vcpu index group priority virq
->     | VCPUInjectIRQ (PPtr VCPU) Word8 Word8 Word8 Word16
+>     -- XXX ARMHYP vcpu index virq
+>     | VCPUInjectIRQ (PPtr VCPU) Int VIRQ
 >     | VCPUReadRegister (PPtr VCPU) HyperReg
 >     | VCPUWriteRegister (PPtr VCPU) HyperReg HyperRegVal
 >     deriving (Show, Eq)
diff --git a/spec/haskell/src/SEL4/Object/Structures/ARM_HYP.lhs b/spec/haskell/src/SEL4/Object/Structures/ARM_HYP.lhs
index 32acb3269..bde2c003b 100644
--- a/spec/haskell/src/SEL4/Object/Structures/ARM_HYP.lhs
+++ b/spec/haskell/src/SEL4/Object/Structures/ARM_HYP.lhs
@@ -165,13 +165,15 @@ but this structure is never manipulated as a whole.
 
 FIXME ARMHYP move to platform
 
+> type VIRQ = Word32
+
 > gicVCPUMaxNumLR = (64 :: Int)
 
 > data GICVCPUInterface = VGICInterface {
 >                        vgicHCR :: Word32,
 >                        vgicVMCR :: Word32,
 >                        vgicAPR :: Word32,
->                        vgicLR :: Array Int Word32
+>                        vgicLR :: Array Int VIRQ
 >                        }
 >     deriving Show
 
diff --git a/spec/haskell/src/SEL4/Object/VCPU/ARM_HYP.lhs b/spec/haskell/src/SEL4/Object/VCPU/ARM_HYP.lhs
index 83951118c..4ecc6ae8f 100644
--- a/spec/haskell/src/SEL4/Object/VCPU/ARM_HYP.lhs
+++ b/spec/haskell/src/SEL4/Object/VCPU/ARM_HYP.lhs
@@ -141,15 +141,27 @@ Currently, there is only one VCPU register available for reading/writing by the
 
 \subsection{VCPU: inject IRQ}
 
+FIXME ARMHYP: this does not at this instance correspond to exactly what the C
+    does, but it is the value that is stored inside of lr in the vgic
+
+> makeVIRQ :: Word32 -> Word32 -> Word32 -> VIRQ
+> makeVIRQ group prio irq =
+>     (group `shiftL` groupShift) .|. (prio `shiftL` prioShift) .|. irq .|.
+>         irqPending .|. eoiirqen
+>     where groupShift = 30
+>           prioShift = 23
+>           irqPending = bit 28
+>           eoiirqen = bit 19
+
 > decodeVCPUInjectIRQ :: [Word] -> ArchCapability ->
 >         KernelF SyscallError ArchInv.Invocation
 > decodeVCPUInjectIRQ (mr0:mr1:_) cap@(VCPUCap {}) =
 >   do
 >     let vcpuPtr = capVCPUPtr cap
->     let vid = (fromIntegral (mr0 .&. 0xffff) :: Word16)
->     let priority = fromIntegral $ (mr0 `shiftR` 16) .&. 0xff
->     let group = fromIntegral $ (mr0 `shiftR` 24) .&. 0xff
->     let index = ((fromIntegral $ mr1 .&. 0xff) :: Word8)
+>     let vid = mr0 .&. 0xffff
+>     let priority = (mr0 `shiftR` 16) .&. 0xff
+>     let group = (mr0 `shiftR` 24) .&. 0xff
+>     let index = mr1 .&. 0xff
 >
 >     rangeCheck vid (0::Int) ((1 `shiftL` 10) - 1)
 >     rangeCheck priority (0::Int) 31
@@ -157,11 +169,11 @@ Currently, there is only one VCPU register available for reading/writing by the
 >     gic_vcpu_num_list_regs <- withoutFailure $
 >         gets (armKSGICVCPUNumListRegs . ksArchState)
 >     rangeCheck index 0 gic_vcpu_num_list_regs
->     vcpu <- withoutFailure $ getObject vcpuPtr
->     let x = addressTranslateS1CPR
->     let vcpuLR = vgicLR $ vcpuVGIC vcpu
->     when (vcpuLR ! (fromIntegral index) .&. vgicIRQMask == vgicIRQActive) $ throw DeleteFirst
->     return $ InvokeVCPU $ VCPUInjectIRQ vcpuPtr (fromIntegral index) group priority vid
+>     vcpuLR <- withoutFailure $ liftM (vgicLR . vcpuVGIC) $ getObject vcpuPtr
+>     when (vcpuLR ! (fromIntegral index) .&. vgicIRQMask == vgicIRQActive) $
+>         throw DeleteFirst
+>     let virq = makeVIRQ (fromIntegral group) (fromIntegral priority) (fromIntegral vid)
+>     return $ InvokeVCPU $ VCPUInjectIRQ vcpuPtr (fromIntegral index) virq
 > decodeVCPUInjectIRQ _ _ = throw TruncatedMessage
 
 \subsection{VCPU: perform and decode main functions}
@@ -173,7 +185,7 @@ Currently, there is only one VCPU register available for reading/writing by the
 >     invokeVCPUReadReg vcpuPtr reg
 > performARMVCPUInvocation (VCPUWriteRegister vcpuPtr reg val) =
 >     invokeVCPUWriteReg vcpuPtr reg val
-> performARMVCPUInvocation (VCPUInjectIRQ vcpuPtr _ _ _ _)  = error "FIXME ARMHYP TODO"
+> performARMVCPUInvocation (VCPUInjectIRQ vcpuPtr _ _)  = error "FIXME ARMHYP TODO"
 
 > decodeARMVCPUInvocation :: Word -> [Word] -> CPtr -> PPtr CTE ->
 >         ArchCapability -> [(Capability, PPtr CTE)] ->