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.

SELFOUR-748: rename tlb invalidation functions

haskell: move Haskell kernel into spec/