We previously made use of the fact that the table to be unmapped will
be a NormalPT_T. This is still true, but to avoid an unnecessary proof
obligation here, we take the pt_type provided by the cap instead, which
coincides with the pt_type the proof uses.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Generalise concept of proving word equality by splitting two words at
bit n and comparing the parts.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Clean up and consolidate further do_machine_op lemmas on AARCH64.
Includes enabling some crunches and lemmas that were blocked on
do_machine_op.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Clean up KHeap_AI. It turns out that almost all do_machine_op lemmas
proved here are crunchable, so move them all into on place.
This only proves lemmas originally already in KHeap_AI. It would likely
make sense to collect general do_machine_op lemmas from other places
in AInvs here as well.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
It was likely a mistake from the beginning to single out this machine
op for crunch ignore here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Includes some progress inside ArchVSpace_AI as well.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Introduce a locale similar to Arch_pspace_update_eq, but where also
`asid_table s` is preserved. This preserves most vspace predicates and
is much more widely applicable than the existing locale in the
hierarchy that demands all of `arch_state s` to be preserved.
Since this only makes sense for Arch functions, there is no generic
version of this locale and instantiation happens only in ArchBits_AI,
not in Invariants_AI.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- reduce assumptions of some of the no-loop helper lemmas
- factor out common reasoning for vs_lookup_table/pt_walk stitching
- close last sorry
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- includes cur_vcpu lemmas for set_asid_pool and store_pte that were
masked by the missing vmid_inv results.
- vmid_inv lemmas for the case where an entire asid pool entry is being
removed. In this case, the vmid entry will already have been reset.
- set_asid_pool unmap lemmas reformulated from map/set restriction to
single entry unmap, because the vmid lemmas don't make sense for sets.
The set version was only ever used for single entries anyway, so had
unnecessary generality.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The rule applies to anything that has `aobjs_of` in the abbreviation
stack, e.g. including asid_pools_of and vcpus_of, and is therefore too
eager for `[wp]`.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The pattern `(ucast high << asid_low_bits) || ucast low` occurs in
a few places in the proofs and `asid_of high low` is easier to read.
For example, it makes obvious that
`asid_low_bits_of (asid_of hi_bits lo_bits) = lo_bits`
should be a simp rule.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- project out the parts of the state that are needed
(asid_pools_of and asid_table) to remove need for lifting rules
- fix argument order (state first)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- equality proof by focussing on the left side of an |>
- relationship between obind and opt_map
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Two key lemmas are vs_lookup_slot_unique_level and store_pte_valid_objs.
The latter needs the new concept of of valid_mapping_insert to preserve
valid_pt_range (which is part of valid_obj).
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a bit more involved than on RISCV64, but with treating
max_pt_level separately from the rest, most of the argument can be
recovered.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This includes a few hopefully useful lemmas about page table type
uniqueness.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The remaining interesting lemma (which is not proved) is
vs_lookup_non_PageTablePTE which needed two statement adjustments, one
to adjust the ptes_of update (certain that this is correct), and one to
add a new precondition valid_vspace_objs (speculative, but hopefully
enough to solve the lemma).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Check that the type of the page table that is present is the type we
are requested to update. The same assert is already present for ptes_of.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- use vspace_objs_of instead of aobjs_of where possible to reduce
scope and make lifting rules stronger
- prove remaining lifting rules in ArchKHeap_AI
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- provides case split rules for vspace_objs_of lifting
- proves the provable vspace_objs_of/vspace_obj_pred lifting rules. The
other lifting rules will need rephrasing for AARCH64 since
vspace_objs_of does not cover all arch objects.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Domain equality is nice to state and sometimes nice to prove, but it is
hard to use in automation (fastforce/auto). The new phrasing here is not
as nice to read, but useful in automation.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Carefully not disturbing the simpset, because too many things break
otherwise.
Similarly, if_option_Some2 is not included with if_option_Some, because
the latter is being declared globally [simp] at some stage and then
breaks things in too many random places.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We so far have unfolded opt_map in these ... = None situations. Using
the new rule directly eliminates one of the cases (the Some case), so
is slightly more efficient when we stack them and get many of these.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Gerwin Klein
Rafal Kolanski
Corey Lewis