A lemma set for the strengthen method to pull `invs` out of
implications. Together with simp and conj_cong, this can help avoid
proving `invs` multiple times (which tends to blow up the proof state).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- pull base-level empty_fail lemmas from AInvs into Monads.Empty_Fail
- apply consistent naming
- apply consistent [intro!, wp]
- make all non-conditional lemmas [simp]
- re-add context building to empty_fail rules, because the select_*
rules may need context to solve their side condition
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Factor out the bit0/bit1 setup for the vm_level type into its own file.
It doesn't really have anything to do with BCorres where it was before.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The projection operators should be definitions so that they are stable
under simp and case splits. This enables later projection stacks to
use abbreviations that remain stable.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We initially wanted to move ucast_ucast_ppn to Kernel_Config_Lemmas.
This doesn't work, because ppn is only defined in Arch_Structs_A, but
it turns out that ppn_len is exactly the term `ipa_size - pageBits`
that the lemma needs, so instead of moving the lemma up, we make its
proof generic by providing the symbolic form of `ppn_len` instead.
This still unfolds Kernel_Config.config_ARM_PA_SIZE_BITS_40, but it
does so only trivially and directly where ppn_len is defined.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- make kheap crunch for do_machine_op generic
- make None_Some_strg available generically in LevityCatch
- move word lemmas up into Word_Lib
- move wp lemmas up into lib + minor lib cleanup
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- minor style/whitespace cleanup
- resolve all smaller AARCH64-local FIXMEs
- move AARCH64-local lemmas
- fix up proof fallout from move (gained some automation in the move)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- move proof methods spec and bspec to Eisbach_Methods
- move general lemmas to Lib
- move word lemmas to Word_Lemmas_Internal
- update proof style
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Implementations for machine ops returning a value should have a _val
postfix. This commit brings vcpuHardwareRegVal in line.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit automatically renames bit0.*/bit1.* lemmas (depending on
the value of vm_level) to vm_level.*
The idea is that vm_level.* can now generically refer to the right
instance, so that the same proof text works without change for both an
even and odd number of page table levels.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- define formally where 14 is coming from instead of trying to explain
in a comment,
- also remove unused parts of the lemma where it is used.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
For the proofs in ArchAInvsPre we require knowledge that the default
user-level tables do not map any user-space addresses. In hyp mode, the
default user-level table is completely empty, because the kernel has
its own separate table. We encode that empty table in the
`valid_global_tables` predicate analogously to the RISCV64 formulation.
We explicitly leave `valid_global_arch_objs` as a `typ_at` predicate,
because the proofs expect `valid_global_arch_objs` to be liftable.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Ensure in valid_pti that page table operations, in particular
unmap_page_table, are only called on NormalPTs. This means we can
remove the vspace_for_asid precondition in the associated lemmas.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
wp rules for most operators such as return, get, gets are named
return_wp, get_wp, etc. Then when, whenE, unless, unlessE operators had
an additional hoare_.. prefix that this commit removes for more
consistency.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
set_asid_pool_empty and delete_asid_empty_table_pt aren't used on
RISCV64 (despite being proved and declared [wp]). Hopefully these won't
be needed on AARCH64.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Gerwin Klein
Michael McInerney
Rafal Kolanski