haskell: explicitly import Prelude hiding Word

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

arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242)

Colloquially known as "invert-fastpath".

Update verification efforts on ARM for the following seL4 changes:
- scheduling decisions done in possibleSwitchTo are moved to the
scheduler
- possibleSwitchTo only checks whether the candidate is valid for a
fast switch, not its priority, accepting possible candidates
immmediately as a switch-to scheduler action
- the scheduler checks the candidate against the current thread and
against the bitmaps before making a decision
- attemptSwitchTo and switchIfRequiredTo are gone
- scheduler is now more complicated, and numerous proofs related to it
are rewritten from scratch
- fast path now checks ready queues via the scheduler bitmaps
- L2 scheduler bitmap order reversed for better cache locality

Many iterations between the kernel and verification teams were needed
to get this right.

haskell: integrate all architectures

* Extract wordSizeCase, wordBits et al into a helper file
* remove all references to tpidrurwRegister from non-arch files
* update sanitiseRegister, add getSanitiseRegisterInfo and
setTCBIPCBuffer for x64
* arch-split cnode rightsBits and guardBits

Removes all trailing whitespaces

haskell: add mapMaybe and modifyArchState

Utility functions.

Revert SELFOUR-242: invert bitfield scheduler and optimise fast path

This reverts:
- a67b443ca5a1e4a8f4d4a7fe0757861e2a7898b5
"SELFOUR-242: update goal number based indentation in Fastpath_C"
- f704cf04044209df996ef6c22bc8ea52122a2c1e
"SELFOUR-242: invert bitfield scheduler and optimise fast path"

Verification confirmed functional correctness and refinement of the
system in this case. However, guarantees on thread scheduling and
fairness are not modeled in the current verification. Once this issue is
addressed, SELFOUR-242 will be re-examined.

SELFOUR-242: invert bitfield scheduler and optimise fast path

* Reverse the level 2 of the bitmap scheduler to move the highest priority
threads' level 2 entries into the same cache line as the level 1.
* Use the bitfield scheduler to make the fast path a more common occurrence.
* Change possibleSwitchTo to not invoke scheduler when the fast path would not
invoke it either (using implicit assumptions about the current thread being
the highest priority schedulable thread)

SELFOUR-444: Adjust Haskell, new ghost data.

The new ghost data is saved in the design spec when Untyped caps
are modified and will be used by CRefine.

haskell: move Haskell kernel into spec/