licenses: convert license tags to SPDX

access: proof style cleanup (for GrantReply patch)

As the title says, this commit introduces general formatting and style
cleanup, but only for the parts touched by the recent GrantReply patch.

access: Fix for GrantReply (SELFOUR-6)

Integrity and pasRefined are majorly changed

The main repercussions are:
- 3 new authorities in the policy: Call, Reply, and DeleteDerived
- The cdt and the caps state are linked in pasRefined
- CDT parentship no longer implies control in certain cases (is_transferable)
- CDT parentship now implies DeleteDerived
- Introduction of cdt_change_allowed that specifies which slot your are
allowed to modify
- Integrity for CDT and CDT list use cdt_changes_allowed
- Integrity for objects in now expressed as a transitive closure of
atomic transition rules

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

Removes all trailing whitespaces

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

arch_split: requalify abstract theories

arch_split: Access checking

l4v-sabre: proof fix upto InfoFlowC

msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API

Minor adjustments caused by Strengthen changes.

ioapic: finished up to InfoFlowC

Import release snapshot.