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.

x64 aspec: resolve vtd_pt_bits; check IOPageTabelCap functions

Currently unused, but will be relevant for VT-d

aspec/haskell: clean out resolved FIXMEs

x64: spec: changes for IRQ invocations (VER-879)

x64: CR3 and machine op updates for Meltdown

x64: more abstract specs and invariants for ASIDs

x64: Add IOPortControlCaps to control IO port allocation

The previous implementation of IOPortCaps has problems with revocability
and determining parency etc. This commit adds IOPortControlCaps which
behave identically to IRQControlCaps -- invoking the IOPortControlCap
allows one to create IOPortCaps with the supplied range.

There now exist invariants to show that there is only one
IOPortControlCap and that all IOPortCaps in the system do not overlap.
Furthermore there is a global record of which IO ports have been
allocated to prevent reissuing the same ports.

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

x64 spec: remove unused x64_asid_map

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.

x64: rename setCurrentCR3 et al to use underscores for abstract spec

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

x64: abstract: remove spurious VMPML4E from vm_map_type

x64: use generic VMMapType from haskell rather than redefine in abstract

x64: spec: update machine functions, invocations, set_vm_root for new
kernel version

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

x64: fix up ArchIPC_AI

x64: machine: move word_size_bits definition to MachineTypes.

Furthermore, create generic library of word lemmas that require
the Arch context to prove, but can be proven with the same proof in
all architectures. These lemmas can then be used safely in generic
theory files. This library is in spec/machine/WordExports.thy

X64: added dummy VMPML4E to vm_page_entry.

needs to be reviewed

x64: port device-untyped from ARM

x64 invariants: CSpace_AI checking

Includes some changes to the abstract spec:
- replace magic numbers with definitions.
- add missing IOPortCap cases to some definitions.

There is one sorry proof, which I think blast could solve if we
gave it enough time. Will need a more subtle approach.

x64: Invariants_AI now processes, removed some arch-specific types

x64: ArchInvariants_AI passes except 1 sorried lemma - valid_arch_objs_alt

x64: progress in ArchInvariants_AI, up to valid_arch_objs_alt

x64: up to lemmas in ArchInvariants_AI

x64 invs: up to vs_refs_pages

x64: add arch_split'd x64 spec with IOMMU stuff