access+infoflow+drefine: update for new definition of `idle_tcb_at`

* Context :

We would like to prove that, for ARM_HYP architecture,
the current vcpu is always the vcpu associated to the current thread.
See issue https://jira.csiro.au/browse/VER-770
and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291

In this process, we changed the definition of `idle_tcb_at`

* In this commit :

Update some proofs in access, infoflow and drefine to take
the new definition of `idle_tcb_at` into account.

Isabelle2018: Access

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

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

access, infoflow: cleanup from previous commit; some style cleanup

access-control, infoflow: use generic relation for pasDomainAbs

This patch generalises the mapping between authority labels and
scheduler domains, so that the access-control integrity property still
holds when labels are not partitioned into domains. This lets us use
the integrity result on systems that don't use the domain scheduler.

The information flow proofs still rely on the domain partitioning,
hence we add constraints on the label-domain mapping for the info-flow
results to hold.

Jira VER-945

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

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.

Removes all trailing whitespaces

SELFOUR-748: rename tlb invalidation functions

arm access: ARM Access now builds on arm-hyp

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: rename free variables to avoid capture

Isabelle2016-1: update references to renamed constants and facts

SELFOUR-64: Remove general Recycle operation

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

SELFOUR-444: Logic generalised; Access finished.

Tweak AInvs proof for Untyped to be more reusable, finish integrity
proofs.

SELFOUR-421: infoflow and infoflow_c builds

word_lib: adjust theory dependencies

arch_split: requalify abstract theories

arch_split: Access checking

arch_split: Access and InfoFlow now build

add arch_tcb object to C, rename aep -> ntfn

history squashed patch for aep-binding

fewer warnings

2015 update for access

Fix Access, InfoFlow and DRefine.

Proof updates, working as far as AInvs.

Updates for getpaddr system call (by Joel Beeren)

Import release snapshot.