ainvs: changed definition of `valid_idle` + `idle_tcb_at` ; defined `valid_arch_idle` invariant

* 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 modify the `valid_idle` invariant so that it includes
the fact that the vcpu of the idle thread is always None.
This is needed for PR291 (see Context above).
`valid_idle` beeing defined with `idle_tcb_at`,
we changed the definition of `idle_tcb_at`
so that it can convey information about the architecture.
And we defined `valid_arch_idle`
that states that the vcpu of an iarch_tcb is None.

* What changed :

Even if these changes are only interesting for the
abstract invariants for arm_hyp architecture
(that are being extended),
it implied changes to several generic and architecture-specific
files of the astract invariants (AInvs) sessions.

Co-authored-by : Corey Lewis <corey.lewis@data61.csiro.au>
Co-authored-by : Santiago Bautista <santiago.bautista@data61.csiro.au>

Isabelle2018: new comment syntax

(result of "isabelle update_comments <dirs>")

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: ioportcontrol: Fixes after adding IOPortControlCaps to x64

Initial proof updates for combinator changes.

ARM ainvs: proof update for user_context refactor

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.

Expand eval_bool; add a method word_eqI_solve.

A number of proofs begin with word_eqI followed by some similar steps,
suggesting a 'word_eqI_solve' proof method, which is implemented here.

Many of these steps are standard, however a tricky part is that constants of
type 'nat' which encode a particular number of bits must often be unfolded.
This was done by expanding the eval_bool machinery to add eval_int_nat, which
tries to evaluate ints and nats.

Testing eval_int_nat revealed the need to improve the code generator setup
somewhat. The Arch locale contains many of the relevant constants, and they are
given global names via requalify_const, but the code generator doesn't know
about them. Some tweaks make them available. I *think* this is safe for
arch_split, as long as the proofs that derive from them are true in each
architecture.

arm/arm_hyp ainvs: rename wellformed_arch_obj to arch_valid_obj

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

Removes all trailing whitespaces

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

arm ainvs: Updated up to ArchFinalise_AI

ainvs x64 arm: remove canonical_address check from do_user_op

For x64, move the check to get_page_info, which is arch-specific.

This means there is no longer any need for canonical_address to be
defined for ARM.

arch_split x64 arm: make endpoint_bits and ntfn_bits arch constants

x64: fix sorry proofs in ArchAInvsPre_AI

The canonical_address constant (but not its definition) is now exported
to generic theories, and used in do_user_op. On ARM, all virtual
addresses are canonical.

x64: progress in Detype_AI

May need some additional work to ensure compatibility with vspace lookup
generalisation.

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>

wp_cleanup: update proofs for new wp behaviour

The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+

- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.

- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.

Isabelle2016-1: update references to renamed constants and facts

invariants: move bexEI to a generic theory

AInvs: remove 32-bit references in Untyped_AI

SELFOUR-553: update rpidrurw in TCBConfigure for simpler Infoflow proofs.

SELFOUR-553: Change Spec according to C code and fix ASpec and AInvs

SELFOUR-421: fix coding style

arch_split: give some vspace concepts more generic names

In particular rename "pd" to "vspace", when the pd represents
an address space.

arch_split: invariants: split Retype_AI [VER-556]

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

word_lib: adjust theory dependencies

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.

arch_split: replaced sublocale with global_naming

arch_split: some quick and dirty arch_splitting by selectively interpreting the ARM locale (with FIXMEs)

arch_split: checkpoint. Checks up to ArchVSpace_AI with two sorries (MattB WIP)

arch_split: reworking predicates about arch objects and types

arch_split: invariants: progress in ArchADT_AI

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

arch_split: change caps_of_state to be explicit projection f caps_of_state

arch_split: change aobj_at to definition instead of abbreviation

arch_split: finished KHeap_AI

arch_split: halfway into KHeap_AI

arch_split: split up Invariants_AI

arch_split: More namespacing progress and invariant splitting. Checks halfway into Invariants_AI

arch_split: progress on namespacing abstract spec