trivial: fix style

cdl-refine: Disable check about inhabited labels

${app_name}_admissible_labelling__all_labels_inhabited is a lemma that
sanity checks whether a label contains mappings. However, becasuse it is
valid for a camkes connector to not create any objects that it owns,
this sanity check isn't valid in all cases. We leave it here as it could
still be used for debugging purposes.

templates: allow adding to integrity policy

This adds a function `add_policy_extra` to the template context,
allowing templates to add extra integrity policy edges in an ad-hoc
fashion. This is used by the `global-endpoint` template.

Implementation note: we extend the capDL `AllocatorState` to store
this extra policy state. However, the new state class is defined in
the capDL library to work around a limitation of the `pickle` module.

templates: cdl-refine: use FastMap for IRQ map

This helps scalability for systems that have more than a few drivers.

templates: cdl-refine: special-case IRQ node size

The capDL library returns `None`, but the proofs require (e.g.) `0`.

templates: eta-contract for Isabelle2019

Isabelle2019 introduced some more eta-expansion regressions in the
simplifier. This adds some post-processing to work around the problem.

templates: cdl-refine: support IRQs and ASIDs

Part of solving VER-986 i.e. proof support for ARM VMs. This adds basic
support for `vm_minimal`, with a single VM and ASID pool.

Many hacks here. For example, the proof currently assumes that there is
at most one ASID pool. This should be generalised when the kernel
supports multiple VMs, as each one will require its own ASID space.

support component groups in cdl-refine proof

The capDL refinement specification assumes that all components have
separate integrity domains. This commit adds two changes to handle
component groups:

1. Components in a CAmkES `group` composition are automatically merged
to the label of the group.

2. For components with unstructured integrity semantics (typically
`hardware` components), we recognise a new `<foo>.integrity_label`
attribute to let the user specify another component label. See the
CAmkES apps repository for examples.

Part of VER-1109.

templates: optimise `policy_wellformed` proof

1. We manually expand policy rules instead of using `fastforce`. This
is more efficient and predictable.
2. The slow `DeleteDerived` transitivity proof is optimised with a
little bit of graph theory: complete graphs are always transitive.

templates: cdl-refine: clean up name references

Refactor the cdl-refine prologue to use fully-qualified names for the
arch-definitions assembly, which simplifies code later.

templates: cdl-refine: tag integrity goals

This depends on a new helper `generic_tag`, added in l4v/lib.

templates, include: explicit Isabelle semantics for connectors

To verify capDL refinement, we need to know the intended semantics for
CAmkES connectors. We use a convention of declaring such semantics in
a new attribute, `isabelle_connector_spec`, which should contain
an Isabelle term of type `connector`. This text is inserted verbatim
when emitting the `Arch_Spec` theory for a CAmkES assembly.

We also add semantics for most of the built-in connectors. These are
merely links to the same built-in connectors of CamkesAdlSpec.
However, other connectors can now declare custom semantics if needed.

templates: fix typo in cdl-refine

templates: support hierarchical identifiers in Isabelle output

This mangles hierarchical identifiers e.g. `foo.bar` into valid
Isabelle identifiers. This relies on capDL-tool performing a similar
mangling (which is currently hardcoded) for the Isabelle capDL spec.

We also prefix Isabelle identifiers for different ADL types e.g.
procedures, components, etc. This is to reduce name conflicts within
the ADL names, as well as conflicts with HOL or l4v builtins.

Implements VER-1012.

trivial: templates: Isabelle cartouches

templates: cdl-refine: minor cleanup

templates: refactor cdl-refine to use object ranges + FP_Eval based proof

cdl-refine: update to work with GrantReply

Also removes an unneccessary W right from RPC receivers' EP caps.

templates: cdl-refine.thy: linter compliance

generate consistent app identifier for Isabelle templates

The generated Isabelle theories and ROOT file need to refer to each
other by filename. This commit modifies the tool and build system to
generate a consistent identifier (based on the app name) and pass that
to all the Isabelle templates. This avoids having to hardcode
assumptions about the build system inside the templates themselves.

Isabelle template for capDL refinement verification

AKA the new label-mapping template. Still needs cleanup and testing.