haskell: explicitly import Prelude hiding Word

everywhere where it can clash with Word type defined by SEL4.

reject all invalid IRQ inputs to IRQ control syscall

This updates the proofs for a change in the C code. The IRQ control
syscall now returns an error whenever the IRQ parameter is not a valid
IRQ value. Previously, the syscall threw away some higher-order bits
before checking for IRQ validity.

Incidentally, the C now only uses the name `irq` for variables of type
`irq_t`, and `irq_w` for variables of type `word_t`. This avoids trouble
with c-parser name mangling.

Removes all trailing whitespaces

x64: haskell: fix up interrupt invocation functions

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Haskell: arch-specific faults + split VMFault -> ArchFault + ReservedIRQ

Hypervisor extensions add extra fault types which are entirely
arch-specific. While the concept of a VM fault exists on all platforms,
these faults are also arch-specific.

This change adds an ArchFault datatype and constructor to the generic
Faults and Failures, and moves VMFault into ArchFault for the ARM
platform.

NOTE: fault indices have changed (generic goes before arch) as per
the changes needed for SELFOUR-413, which is the seL4 C equivalent of
this commit.

* add arch faults and failures to SEL4.cabal

* introduce and handle IRQReserved

On ARM this does nothing, but on other platforms reserved IRQs are
actually used.

* split TCB into ArchTCB (userContext)

* changing ArchFault to make haskell-translator to work

tags: [VER-623][SELFOUR-413]

x64: reinstate maxIRQ check

This was accidentally removed from the Haskell and executable specifications.

x64: add x64 haskell code from seL4 repository

haskell: move Haskell kernel into spec/