Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.

haskell: explicitly import Prelude hiding Word

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

arm-hyp: update proofs for SELFOUR-584: running multiple VMs on ARM

As requested by verification, hypervisor registers are now an
enumeration-indexed array rather than individual fields. This cleans up
some of the proof. Additionally, we sweep some non-complexity under the
machine op rug: vcpu_hw_write/read_reg_ccorres is as deep as we go,
rather than specifying every operation and proving that
vcpu_hw_write seL4_VCPUReg_REG calls set_REG for every REG

I took this opportunity to clean up some arm-hyp definitions and proofs,
so some whitespace cleanup got tangled in.

haskell: unify arm and arm-hyp haskell files

- both ARM and ARM_HYP haskell specs are now generated from the same set of files using cpp
- callbacks and platform files are merged into one directory (ARM)
- remove check-arm-hyp.py now that there are no ARM_HYP.lhs files

SELFOUR-748: rename tlb invalidation functions

haskell: make ARM_HYP match ARM when preprocessed for non-hyp platforms

haskell: adopt new getActiveIRQ parameter

haskell: make ARM resemble the output of ARM_HYP preprocessing

The first step of merging the ARM hypervisor extensions into existing
ARM is to make the current ARM look like the preprocessed output of
ARM_HYP, which currently supports both platforms.

NOTE: this requires updates to ARM Refine and CRefine due to shuffling
around some constants (pteBits et al.). That is on its way.

haskell: fix misguided import for ARM platform

arm-hyp haskell: VSpace compiles with enabled SMMU (stubbed IO for the moment)

haskell: add Hypervisor module, add concept of Hypervisor exceptions

The kernel gains an entry point for hypervisor exception events, as well
as a way to add arch-specific handlers for these events.

We do this since the hypervisor has its own entry point into the kernel,
and that must be reflected in the top-level kernel entry interface.

For ARM target, which does not have hypervisor support, we add an no-op stub.

haskell: move Haskell kernel into spec/