It was a mix of ARM_A and ARM_HYP_A previously. AInvs+Refine+CRefine
needed updates.

Signed-off-by: Rafal Kolanski <[email protected]>

(already in Arch locale)

Signed-off-by: Rafal Kolanski <[email protected]>

Implicitly use L4V_ARCH for global_naming prefix.

Signed-off-by: Rafal Kolanski <[email protected]>

* try get rid of `interpretation Arch .` (slow) in lieu of `(in Arch)`
  (faster) or proper requalifying (nearly instant)
* get rid of requalifications that were already requalified, or were
  global (thanks to new warnings)
* put arch_global_naming on same line as `context Arch begin`

Signed-off-by: Rafal Kolanski <[email protected]>

* get rid of `global_naming Arch`, this is no longer needed since we can
  requalify directly from `arch_global_naming` with `arch_requalify`
  commands
* add missing `arch_global_naming` for `context Arch`, for consistency
* update X64 Refine `Arch.` references (other arches did not need this)

Signed-off-by: Rafal Kolanski <[email protected]>

* prevent duplication between arches by moving requalifications from
  Arch theories to generic ones
  * this strategy is not available for new constants that are introduced
    in the Arch locale that need to be referenced in generic definitions
    or locale instantiations
* fix up the inconsistent qualification of set_cap_valid_arch_caps_simple

Signed-off-by: Rafal Kolanski <[email protected]>

Rename the wellformed_acap version to wf_acap_rights_update_id,
and the valid_arch_cap version to valid_acap_rights_update_id.

Signed-off-by: Rafal Kolanski <[email protected]>

Avoid unnecessary Arch context interpretation (slow).
Remove attempts at requalifying entities that are already generic
(misleading).

Signed-off-by: Rafal Kolanski <[email protected]>

Makes global_naming implicit (based on L4V_ARCH).

Signed-off-by: Rafal Kolanski <[email protected]>

This was generic on these two architectures, not consistent with others.

Signed-off-by: Rafal Kolanski <[email protected]>

MiscMachine_A already contains asid_high_bits, asid_low_bits and
asid_bits. Other architectures don't duplicate them in Arch_Structs_A,
so ARM and ARM_HYP shouldn't either.

For ARM, this also means fixing up DRefine+DPolicy+CamkesCdlRefine to
refer to the MiscMachine_A definitions when needed (CapDL duplicates
them again in Types_D, but as they don't import machine theories, those
can't be removed).

Signed-off-by: Rafal Kolanski <[email protected]>

These proofs have been arch-split for some time now so the FIXMEs appear
resolved. They are also non-specific, so it is impossible to tell at
this point whether they referred to anything.

Signed-off-by: Rafal Kolanski <[email protected]>