Fix up proofs after word lemma moves

Remove pure word lemmas from proof/*

Removes redundant lemmas after moving them up to Word_Lib.

lib: change runErrorT to runExceptT to match Haskell code

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

crefine: update for C-parser change to avoid complex call lvals (JIRA VER-881)

VER-910: add msgLabelBits to haskell

message_info structs have 20 bit labels. On 32-bit systems, the label
does not need to be masked as there are no extra padding bits in the
struct, but this is not true for 64-bit systems. As a result, the
haskell needs to mask msgLabelBits (=20) when extracting the label in
messageInfoFromWord.

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.

autocorres-crefine: update CRefine proofs for AutoCorres

update object and field widths for x64, and remove some magic numbers

In X64 update the following to match the C kernel:
- TCB size-bits (11).
- Endpoint size-bits (4).
- Guard bits (58).
- Message registers.

For all architectures, replace magic numbers with defined constants in
specifications, and as far as possible in proofs:
- tcb_bits in abstract spec.
- tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell
spec, Haskell and C refinement proofs.

Removes all trailing whitespaces

crefine: move crefine/* into crefine/ARM/*