access: Isabelle2020 update

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

licenses: convert license tags to SPDX

proof: update for wp changes

Updated 'wp_once' to 'wp (once)' and removed several stray uses of 'wp_trace'.

global: isabelle update_cartouches

SELFOUR-1198: update proofs for correct restart PC

Fixes a case where a thread can go from Running->Inactive->Restart and
use a restart PC that is out of date. An out of date restart PC occurs
when a thread was transitioned to running after being in a blocked
state, but was never scheduled and so did not execute the traps code
that updates the restart PC.

This also renames relevant register names for consistency across
architectures (FaultIP and NextIP).

access-control: update for new definition of set_object

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.

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

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

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

Proof update for crunch changes

ARM access: proof update for user_context refactor

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

update proofs for SELFOUR-30/291 "Reschedule on self-modification"

- SELFOUR-30 Reschedule when changing own IPC buffer
Previously if you invoked the TCB of the current thread and
changed the IPC buffer frame this would not immediately take
affect, as the kernels view of the current IPC buffer is
updated in Arch_switchToThread. This change forces Arch_switchToThread
to get called, even if we would switch back to the original
thread.

- SELFOUR-291 Reschedule when changing own registers
Previously if you wrote to TCB of the current thread and
changed the TLS_BASE this would not immediately take
affect, as the kernel only updates this register in
Arch_switchToThread. This change forces Arch_switchToThread
to get called, even if we would switch back to the original
thread.

Bisim / Access / InfoFlow: updates for Hypervisor stub

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

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-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-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

word_lib: adjust theory dependencies

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: Access checking

SELFOUR-56: Remove diminish rights from IPC

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.

fewer warnings

2015 update for access

Updates for getpaddr system call (by Joel Beeren)

release cleanup

Import release snapshot.