l4v icon indicating copy to clipboard operation
l4v copied to clipboard
verified publisher icon seL4

factor out more VCPU lemmas

Open lsf37 opened this issue 2 years ago • 0 comments

Currently a lot of VCPU lemmas are mixed into ArchVSpace. It would probably make sense to collect these in a separate file (and also see which other VCPU lemmas are mixed into other theories).

This would apply to both ARM_HYP and AARCH64.

There is already a separate file ArchVCPU_AI, but this comes after theory AInvs and is for the additional VCPU invariant that the current VCPU always is the VCPU of the current thread.

lsf37 avatar Feb 05 '23 23:02 lsf37