aspec+ainvs: remove interrupt/irq from p_monad

- preemption in C is not associated to an irq
- updating aspec to reflect this so that we can have irq-independent
preemptions (needed in MCS)

- proof fix for the above: remove intr

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>

licenses: convert license tags to SPDX

global: isabelle update_cartouches

Removes all trailing whitespaces

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]

paramatrised abstract and haskell specs over L4V_ARCH

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

fewer warnings

Import release snapshot.