all: remove theory import path references

In Isabelle2020, when isabelle jedit is started without a session
context, e.g. `isabelle jedit -l ASpec`, theory imports with path
references cause the isabelle process to hang.

Since sessions now declare directories, Isabelle can find those files
without path reference and we therefore remove all such path references
from import statements. With this, `jedit` and `build` should work with
and without explicit session context as before.

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

licenses: convert license tags to SPDX

proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule

Prior to this commit the kernel would always trigger a full reschedule
on setPriority. This change allows the kernel to attempt a direct
switch, avoiding invoking the scheduler.

abstract: updates for moving IPC buffer register to thread-local storage for SELFOUR-1524

global: isabelle update_cartouches

aspec: Update ASpec for GrantReply (SELFOUR-6)

spec: add SetTLSBase invocation and update the registers (VER-807)

aspec/haskell/machine: refactor user_context interface

- remove separate abstract set_/get_register implementation, directly use machine op
- make interface aware that user_context does not always need to equal
(register => machine_word)
- introduce FPU state on x64

SELFOUR-1016: fix confused deputy problem when setting priorities

VER-849: abstractly declare a threads registers have changed

This removes an ifdef present in invokeTCB_(Copy|Write)Registers, and
adds the function Arch_postModifyRegisters which does nothing on any
arch except x86-64.

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.

misc: clean up before merging x64

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.

arm: refactor sanitise_register to take a bool instead of a kernel_object

This simplified the sanitise_register logic in CRefine for arm-hyp.

provide TCB argument for sanitiseRegister

Other platforms such as arm-hyp will need to look into additional TCB state
such as VCPU in sanitiseRegister. This commit provides the scaffolding for
that.

abstract: remove two obsolete functions

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>

fix ARM build after merge

Also:
- move some ARM-specific things out of Tcb_AI
- port changes from ARM to X64, up to beginning of ArchVSpace_AI

ASpec: arch-specific faults + VMFault -> ArchFault + ReservedIRQ

* fixing name space for arch_tcb and tcb_context

* arch_fault added

* changing name space for arch_tcb

- as_user, set_mrs, get_mrs, copyRegsToArea, and copyRegsToArea are
moved to the ARM_HYP directory. This breaks the proofs in
refinement, etc., mostly in tcb related files.

* removed a duplicate range check definition

* fixes ARM for arch_tcb

* adding arch_thread_get/set

* add ReserveIRQ

- initInterruptController is not added yet.

* add arch_fault

- arch_fault and related functions are added.

* arch-parametrising arch-specific extra registers

- ArchDefaultExtraRegisters is the common interface that refers to the
arch-specific data (ARMNoExtraRegisters for ARM/ARM_HYP)

* Adding accesors for tcb_context

- Despite the fact that tcb_context has an arch-specific definition,
it is reasonable to assume that some form of tcb_context will be
available in any architecture, thus the need for accesors to handle
updates.

* as_user updated to use tcb_context accesors

* set_mrs and get_mrs updated to use tcb_context accesors

- Several function on ArchTcb_A and ArchTcbAcc_A (both theories where
removed) can be defined in a general context by using the
tcb_context accesors

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

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

SELFOUR-276: Add MCP to specs and invariants

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

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

arch_split: split up Invariants_AI

arch_split: More namespacing progress and invariant splitting. Checks halfway into Invariants_AI

arch_split: progress on namespacing abstract spec

paramatrised abstract and haskell specs over L4V_ARCH

Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.

add arch_tcb object to C, rename aep -> ntfn

removed unused (and outdated) constants

history squashed patch for aep-binding

fewer warnings

ported ASpec to Isabelle2014-RC0

Updates for getpaddr system call (by Joel Beeren)

Import release snapshot.