access: Isabelle2020 update

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

proofs: adjustments for word_lib changes

global: isabelle update_cartouches

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

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

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

lib+spec: move definition of machine_word to Word_Lib

JIRA VER-963

Proof update for crunch changes

add constant definitions for bounds on untyped object sizes

Removes all trailing whitespaces

arm access: ARM Access now builds on arm-hyp

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

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

update references to word32_plus_mono_right_split

This is now called machine_word_plus_mono_right_split, since it now
works at the current architecture's machine word size.

SELFOUR-444: Logic generalised; Access finished.

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

SELFOUR-421: fix coding style

SELFOUR-421: infoflow and infoflow_c builds

SELFOUR-421: crefine builds

arch_split: access: fixup locale introduction rule

arch_split: requalify abstract theories

arch_split: Access checking

port Access proofs to Isabelle2016-RC2

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.

Refine working.

Proof updates, working as far as AInvs.

Import release snapshot.