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>

aspec: factor out arch_mask_irq_signal

On RISC-V we do not call mask_irq.

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

aspec: arch split on invokeIRQHandler

The RISCV implementation of invokeIRQHandler calls plic_complete_claim
instead of maskInterrupt. plicCompleteClaim is added as a machine op
and invokeIRQHandler has been arch split for the ACKIrq case.

Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>

licenses: convert license tags to SPDX

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

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

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]