This is a small file and the one arch-specific lemma has a proof
identical on all architectures. Therefore use only one version of this
file.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Notable changes:
* isCap_simps is only available in Arch; generic gets gen_isCap_simps
* projectKOs is now [simp] on all architectures
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Leave corresK as is, consolidate ex_abs as an abbreviation on
ex_abs_underlying, and provide convenience _def lemma instead of using a
definition. Clean up Refine.thy for affected architectures.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The value of gicNumTargets_bits was wrong for GICv3 platforms, breaking
CRefine for those platforms.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add separation logic specification lemmas for the new SGISignalCap API
for later use in sys-init.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
SGISignal caps require arch specific conditions in the valid_badges and
mdb_chunked predicates. Add an arch interface for these.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This contains a slight tweak to generic CSpace_AI and proof adjustments
for the architectures that do not implement the SGISignalCap API.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- add SGISignalCap API for ARM, ARM_HYP, AARCH64
- add generic interface for should_be_arch_parent_of and
is_irq_control_descendant in the cdt implementation
- add default interface implementations new interfaces for RISCV64, X64
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This affects all architectures, because generic interfaces are changing,
but the SGISignalCap API is only added to ARM, ARM_HYP, and AARCH64.
For X64 and RISCV64, we trivially implement the new interfaces, and in
generic code we call those interfaces.
These new interfaces are isArchMDBParentOf and
isIRQControlCapDescendant, for checking in generic code if there are
architecture specific cases in isMDBParentOf and isCapRevocable
respectively.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Define the new constants numSGIs and gicNumTargets, plus a new
machine operation ipiSendTarget.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This protects against both tests being run simultaneously and trying to
write to the same file.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Newer arches and global interfaces favour left shifts over k*2^n, which
results in breakage in proofs of older arches.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
setObject_other_corres was temporarily patched to handle both arch and generic
objects, while setObject_other_arch_corres is a derived version for arch
objects only. This will be revised later as arch-split continues.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Similarly to invariants, the state relation contains a large number of
definitions. To reduce load on locales and number of theory files, the
architecture-specific definitions go first (ArchStateRelation), then the
generic definitions and lemmas (StateRelation), and finally the
arch-specific lemmas (ArchStateRelationLemmas).
Notable changes:
- due to ghost_relation being arch-specific on AARCH64, ghost_relation
becomes arch-specific, with a generic `ghost_relation_wrapper`
exported into generic context
- ghost_relation is required to not depend on machine state
- the [a]obj_relation_cuts infrastructure conflated arch and generic
object cases in other_obj_relation and those had to be split up
- obj_relation_cutsE unfortunately still spills all the cases, but
defining that properly can only happen when dealing with KHeap_R
- after discussion, we opted for introducing StateRelationPre to contain
generic setup needed by ArchStateRelation
- it turned out APIType_map is not used anywhere (in lieu of APIType_map2
introduced in Retype_R), so was removed
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The demo does not work with `smt (verit)` (diverges). Comment out the
Z3 call, since it is not essential for anything.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- pos_mod_sign is now in the default simp set
- pred_*_def lemmas have become lemma sets -- use only the
parts that are needed in metis to avoid warnings.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use `smt (verity)` instead of just `smt` to avoid the Z3 default. There
is no soundness problem with Z3, but various versions of Z3 do not work
on Linux/AArch64 which means that proof reconstruction fails.
To make sure these proofs work with vanilla Isabelle distributions, we
fix the invocations instead of providing specific Z3 versions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Rafal Kolanski