Base ASpec + machine on OptionMonad_ND; fix proof fallout

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

lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad

arm: address setCurrentPD mismatch between abstract/haskell/C

ARM setCurrentPD was recently refactored as part of multi-VM support for
ARM_HYP. The Haskell was updated correctly, and the C was not.
Unfortunately, setCurrentPD was manually redefined in MachineOps.thy for
ARM hiding the change, making the C look correct when it wasn't.

We scrap the second definition of setCurrentPD, load it from the Haskell,
and have an abstract set_current_pd that's a bit simpler to refine down
from.

The proofs are updated for the above change and the update to the C
setCurrentPD that was breaking on KZM.

Removes all trailing whitespaces

SELFOUR-748: rename tlb invalidation functions

arm ainvs: Updated up to ArchFinalise_AI

wp_cleanup: update proofs for new wp behaviour

The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+

- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.

- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.

Refactor of crunch.

Substantial adjustments to crunch. Main user changes are:
- 'lift' and 'unfold' mechanisms replaced by more general 'rule'.
- some more 'ignores' standardised.
- crunch has a more principled overall design:
+ discover crunch rule
* provided or by definition extraction
+ recurse according to rule
+ prove goal based on rule, recursive discoveries, standard tactic
* wp/simp adjustments tweak tactic

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.

arch_split: halfway into KHeap_AI