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.

aspec: move up mask_vm_rights, make arch independent

Strictly speaking vmrights might at some point become architecture dependent,
but all present architectures have precisely the same implementation, and there
are no plans to do anything different in the foreseeable future.

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

add constant definitions for bounds on untyped object sizes

update object and field widths for x64, and remove some magic numbers

In X64 update the following to match the C kernel:
- TCB size-bits (11).
- Endpoint size-bits (4).
- Guard bits (58).
- Message registers.

For all architectures, replace magic numbers with defined constants in
specifications, and as far as possible in proofs:
- tcb_bits in abstract spec.
- tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell
spec, Haskell and C refinement proofs.

aspec: integrate all architectures

Removes all trailing whitespaces

arch_split: make cte_level_bits_def work with existing proofs

Many generic proofs make use of cte_level_bits_def. Although the
definition is architecture specific, the proofs work for any reasonable
value of cte_level_bits, so it's fine to expose the definition to
generic proofs.

arch_split x64 arm: make endpoint_bits and ntfn_bits arch constants

arch_split x64 arm: make cte_level_bits an arch constant

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>

x64: fix ARM build after merge

AInvs: remove references to arch specific stuff in Ipc_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: Change Spec according to C code and fix ASpec and AInvs

SELFOUR-421: crefine builds

SELFOUR-421: AInvs done, no added invariants yet

SELFOUR-421: first attempt at abstract spec

arch_split: replaced sublocale with global_naming

arch_split: added ARM_A and ARM_H locales

arch_split: reworking predicates about arch objects and types

arch_split: initial attempt at redefining invariants to avoid changing too many proofs

arch_split: split up 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.