arm-hyp ainvs: prove that the vcpu of the idle thread is always None

* Context :

We would like to prove that, for ARM_HYP architecture,
the current vcpu is always the vcpu associated to the current thread.
See issue https://jira.csiro.au/browse/VER-770
and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291

* Intermediate step : the vcpu of the idle thread is always None

In this commit we update the proofs of abstract invariants for
the arm_hyp architecture, so that the new version of `valid_idle`,
stating that the vcpu of the idle thread is always None, holds.

Fix up proofs after word lemma moves

Isabelle2018 arm: AInvs

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

x64: more abstract specs and invariants for ASIDs

ainvs: Add itcb_arch to the itcb projection

This allows us to more easily show that arch specific tcb fields are
preserved by many functions of the spec. For ARM_HYP we add a
projection for the tcb_vcpu field.

arm-hyp: update proofs for SELFOUR-584: running multiple VMs on ARM

As requested by verification, hypervisor registers are now an
enumeration-indexed array rather than individual fields. This cleans up
some of the proof. Additionally, we sweep some non-complexity under the
machine op rug: vcpu_hw_write/read_reg_ccorres is as deep as we go,
rather than specifying every operation and proving that
vcpu_hw_write seL4_VCPUReg_REG calls set_REG for every REG

I took this opportunity to clean up some arm-hyp definitions and proofs,
so some whitespace cleanup got tangled in.

Proof update for crunch changes

Many proof repairs.

Initial proof updates for combinator changes.

Remove valid_arch_objs

now that we have valid_vspace_objs to express validiy of
vspace objects, we do not need valid_arch_objs: we have
valid_objs to state the validity of non-vspace arch objects.

ainvs: integrate all architectures

ainvs: reintroduce second_level_tables all over the place, update generic Arch_AI and various ArchArch_AI's to match

arm-hyp AInvs: reintroduce valid_global_objs and valid_global_vspace_mappings

arm-hyp invariants: fix fallouts from invoke_vcpu_inject_irq changey

arm-hyp ainvs: update for asid_high_bits change

arm-hyp ainvs: add valid_arch_tcb invariant (vcpu_at for tcb_vcpu)

arm-hyp ainvs: proof updates for abstract spec changes

In particular for:
- new global PD
- disable vcpu on switch to idle
- banked registers

arm-hyp: AInvs sorry-free

ArchFinalise_AI and ArchArch_AI sorry-free

arm-hyp: AInvs checkpoint

- AInvs builds with new definitions of dissociate et al
- fixed most of the fallout of the change, left some as additional sorries
- should now be ready for additional cur_vcp live invariant

arm-hyp invariants: ArchArch_AI progress

* Most sorries in ArchArch_AI are done
* valid_arch_objs_lift moved to ArchKHeap_AI

tags: [VER-679]

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

arm-hyp invariants: fixing crunches and invs proofs

arch_splitting, fixing sorries, some more invariants

arm-hyp invariants: fix arch_splitting/locales

* tcb_arch_ref: definition and invariants (to access obj_refs in tcb_arch in generic contexts)
* fixes related hyp_refs

arm-hyp invariants: incremental progress (sorrying, fixing crunches/alignments, etc.)

* sorry perform_vcpu_invocation invariant statements
* fix pg_entry_align and related statements
* some crunches in ArchFinalise_AI

arm-hyp invariants: changes from rebase for ARM_HYP invariants

arm-hyp invariants: updates for vcpu, alignments, valid_vspace_obj, wellformed_arch_obj, etc.

arm-hyp invariants: copy arch-splitted invariant files from ARM

earlier updates in ArchInvariants are kept

arm-hyp invariants: add ARM_HYP directory, updating ArchInvariants_AI and Invariants_AI