Add compile time checks for conditions on physBase that are necessary
for verification of multikernel builds to succeed -- if these fail, the
proofs will fail.
If these succeed, and nothing else has changed compared to a verified
kernel other than physBase, then the proofs will succeed. This does not
mean that all platform requirements are validated, it just means that
all requirements for the proofs to be consistent are met.
The conditions correspond to those in
spec/machine/*/Arch_Kernel_Config_Lemmas.thy
in the verification repository.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
ca1d5f9226