Fix up proofs after word lemma moves

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

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

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

infoflow: Clean up infoflow, comment, wrap lines, ...

Proof update for crunch changes

Many proof repairs.

Initial proof updates for combinator changes.

Genericise deletion actions that occur after empty_slot

This patch adds a generic "post_cap_deletion" step that is called by
finalise_slot. Previous to this, the only caps which had actions
required at this stage were IRQHandlerCaps -- it was required that the
IRQ bitmap be updated after the cap itself was removed (as the
invariants state that for any existing IRQHandlerCap, the corresponding
bit in the IRQ bitmap must be set).

By genericising this, we add the capacity for new, arch-specific post
cap deletion actions to occur in the future.

arm: update for simple_ko getter/setter

Removes all trailing whitespaces

wp: update the proofs for the new wp/wpc/wpsimp

Bisim / Access / InfoFlow: updates for Hypervisor stub

Access and InfoFlow fix for prepare_thread_delete

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.

Isabelle2016-1: update references to renamed constants and facts

trivial: remove some uses of find_theorems

Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes

* tcb_context rephrasing to (tcb_context o tcb_arch) and respectively
for set operations

* unfolding of reserved_irq for trivially solving most lemmas

* Changes to the inductive definition of integrity_obj to account for
tcb_arch and tcb_context new location

* Changes to the tcb examples in ExampleSystem to include tcb_arch

* Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case

* Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch)

* Trivial unfolding of handle_reserved_irq for hoare rules

* Examples in Example_Valid_State.thy were updated

* Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ
handling

* Fun fact, some proofs are now shorter

tags: [VER-623][SELFOUR-413]

SELFOUR-553: rebase and fix styles and comments

SELFOUR-553: update rpidrurw in TCBConfigure for simpler Infoflow proofs.

SELFOUR-64: Remove general Recycle operation

This removes the RecycleCap CNodeInvocation, whilst
retaining recycle behaviour for Endpoints -- now renamed
CNodeCancelBadgedSends.

SELFOUR-444: Repair InfoFlow.

SELFOUR-444: Avoid unnecessary cache clears.

Adjust both specs and propagate the changes.

SELFOUR-444: Finished InfoFlow and DRefine.

SELFOUR-276: Finish proofs for maximum controlled priority (MCP)

To finish the proof of refinement to C, the specification for checkPrio
needed strengthening: the checkPrio spec now takes a machine word
argument. In the spec, priorities are still stored as 8-bit quantities,
however. Once the spec was strenthened, it was possible to remove some
redundant checks and mask operations from the C code.

A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).

SELFOUR-421: infoflow and infoflow_c builds

arch-split: Tcb_AI.thy done

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

arch_split: requalify abstract theories

arch_split: InfoFlow checking

SELFOUR-420: Verification of maxIRQ check in handle_interrupt.

SELFOUR-56: Remove diminish rights from IPC

arch_split: Access and InfoFlow now build

Wait -> Recv: update proofs

add arch_tcb object to C, rename aep -> ntfn

Minor adjustments caused by Strengthen changes.

poll: added non blocking sync wait

poll: Added new syscall for polling async endpoints (non-blocking wait)

history squashed patch for aep-binding

SELFOUR-220: When calling handleWait, only delete the
TCB's ReplyCap when actually waiting on a synchronous
endpoint.

infoflow: minor cleanup

fewer warnings

infoflow: 2015 update (apart from C refinement)

Fix Access, InfoFlow and DRefine.

Updates for getpaddr system call (by Joel Beeren)

Import release snapshot.