aspec: msg_align_bits and related are arch independent

While the numerical value is arch dependent, the definition and symbolic value
are not. This commit factors out the symbolic computation and only unfolds the
numeric value in the architecture dependent spec.

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: mark vt-d FIXME

aspec/haskell: clean out resolved FIXMEs

x64: spec: fix up definition of decodeX64FrameInvocation to match C

x64: aspec+haskell: reorder attribsFromWord to match C

x64: spec+ainvs+refine: add machine ops for nativeThreadUsingFPU and switchFpuOwner

x64: ainvs+refine: remove invalidateASIDEntry, simplify with just hwASIDInvalidate

x64: CR3 and machine op updates for Meltdown

x64: more abstract specs and invariants for ASIDs

x64: clear some sorry proofs from CSpace_C

Also update some Haskell and abstract specs relating to IO ports.

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.

x64: VER-917: correct VSpace invocations to update map_type, and add invariants to check that maptype and mapped addresses correspond for PageCaps

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.

x64 spec: remove unused x64_asid_map

x64 abstract: make invalidate_asid_entry take a bare vspace pointer

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

x64: AInvs: move invalidate_asid_entry into case for delete_asid

x64: abstract: reorder arguments in hwASIDInvalidate

x64: abstract: updated msg_align_bits to use word_size_bits

x64: aspec/ainvs: miscellaneous updates

* make update_cap_data do nothing for IOPorts
* return same_aobject_as to previous definition for IOPorts
* change cap_master_cap for IOPorts to be the identity

x64: abstract: tweak spec to match C code

x64: abstract: remove spurious VMPML4E from vm_map_type

x64: ASpec builds after merge for ARM, X64

x64: fix CR3 check in set_vm_root spec

x64: spec: add loop to delete_asid_pool; re-add asid_map updates

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: added more machine definitions

X64: added dummy VMPML4E to vm_page_entry.

needs to be reviewed

x64: port device-untyped from ARM

x64: more progress in ArchVSpace_AI

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 abstract spec: add some missing cases in ArchVSpace_A unmap operations

These had been undefined, causing some crunch commands to fail.

x64: progress in ArchInvariants_AI, up to valid_arch_objs_alt

x64: add arch_split'd x64 spec with IOMMU stuff