AArch64: support SMC calls in verified kernel

[lsf37]

This adds support for SMC (Secure Monitor Calls), see also RFC-9.

Currently, this forces KernelAllowSMCCalls to be ON for AArch64 builds. The plan is to remove all SMC ifdefs in the C code apart from the one that provides the initial SMC master cap at boot. (Or, if people are happy with that, just have SMC always on, because the initialiser will not pass on the SMC master cap if it is not explicitly requested).

The main proof change on the generic interface side is the introduction of arch_cap_badge/arch_capBadge, which was necessary because the proofs previously assumed that arch caps never have a badge that is managed with the standard badge mechanisms.

Since we know nothing about the actual content of SMC operations, the best we can do is assume that the doSMC_mop will only modify machine state the kernel does not manage, and leave kernel-visible memory unchanged. This appears to be a true assumption in how SMC is used so far in seL4 (power management and device access). Other uses will have to make their own assessment.

There is a companion seL4 PR (https://github.com/seL4/seL4/pull/1572) with a minor code refactor that aligns the C more to the usual decode/invoke split and argument passing. Not behaviour change is intended.

During the proofs it came up that the capclass definition was placed in a generic ASpec file, but has architecture-specific content (e.g. IOPorts). It turns out that we only make use of 3 actual cap classes: physical, reply, and the rest. Since this still works in the generic setting, instead of arch splitting the type, I have adjusted it into these 3 classes in a separate commit at the end. The initial ASpec commit for SMC caps introduces an SMCClass which is later removed in that consolidation.

Test with: https://github.com/seL4/seL4/pull/1572

[lsf37]

@michaelmcinerney this one should not break MCS proofs -- even though it introduces new interface constants, the C code changes are all constrained to AArch64.

[lsf37]

I should mention that I had to move around some lemmas and definitions in CRefine: the auxiliary definition of setMR (we only have setMRs in Haskell, but C has setMR) needed a common ancestor between Arch_R and Ipc_R, which was a bit tricky to find -- the monad definitions could go into TcbAcc_C, where I think it makes sense, but the setMR_ccorres lemma only works further down in SyscallArgs_C because it needs the helper lemmas defined there (I tried moving those up, but that pulls out a whole tree of dependencies). setMR does make some sense in SyscallArgs because it is for the system call protocol, so I don't think it's too terrible.

[Xaphiosis]

commit nitpicks/suggestions while I warm up:

• declare constants for SMC caps doesn't declare the consts, only flags them for import?
• Haskell is using -> Haskell uses
• It appears that "||" has been correctly -> should that be \|? Confused
• Similarly to AInvs in the previous commit, this commit introduces -> ..., introduce ?
• This introduces -> Introduces
• This commit introduces -> Introduce
• orphanage -> Orphanage
• arm+arm-hyp+riscv_x64 should have a + there, and arch_cap_bade should be badge

Also, is the plan to squash any of these at the end, or leave as is? The other thing is that the order is a bit strange. I was expecting a story, like aspec, then haskell / design infrastructure, then aarch64 proofs, and then mop-up operations for other arches. The later parts seem in order, but at the start it's a bit confusing to follow since I'm reviewing commit-by-commit.