Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.

riscv haskell-translator: caseconvs update

arm-hyp: ioportcontrol: fixes after adding IOPortControlCaps to x64

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.

Genericise deletion actions that occur after empty_slot

This patch adds a generic "post_cap_deletion" step that is called by
finalise_slot. Previous to this, the only caps which had actions
required at this stage were IRQHandlerCaps -- it was required that the
IRQ bitmap be updated after the cap itself was removed (as the
invariants state that for any existing IRQHandlerCap, the corresponding
bit in the IRQ bitmap must be set).

By genericising this, we add the capacity for new, arch-specific post
cap deletion actions to occur in the future.

manually adjust non-obvious cases of tab to space replacement

remove most tab characters

Removes all trailing whitespaces

haskell translator: update caseconvs

after making ARM look like preprocessed ARM_HYP

changes after rebasing (for isabelle2016-1 and the new wp)

arm-hyp execspec: pdates for VER-623

with correct copy_global_mappings for ARM_HYP

arm-hyp execspec: add irqVGICMaintenane and initInterruptController

with caseconvs, generated files

arm-hyp execspec: caseconvs for VGIC interface etc.

arm-hyp execspec: add caseconvs, fixes in haskell + VCPU_H

x64: more caseconvs

x64: more caseconvs

x64: misc: added more caseconvs

x64: haskell: fix broken caseconvs; use generic ptTranslationBits

x64: haskell-translator: fixed broken caseconvs

x64: got haskell translator running on existing haskell kernel

execspec: add hypervisor, HypFaultType in skeletons (ARM), generated files

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

SELFOUR-444: Adjust Haskell, new ghost data.

The new ghost data is saved in the design spec when Untyped caps
are modified and will be used by CRefine.

SELFOUR-421: crefine builds

SELFOUR-421: refine done

SELFOUR-421: AInvs done, no added invariants yet

x64: add arch_split'd x64 spec with IOMMU stuff

paramatrised abstract and haskell specs over L4V_ARCH

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

Fix Orphanage from array changes, refactor.

Some generalisation is done in finaliseSlot_invs'' to avoid
duplicating it in Orphanage and PageTableDuplicates.

Finally cleanup in haskell translation.

add arch_tcb object to C, rename aep -> ntfn

Import release snapshot.