These sets of references currently differ on all architectures and on both master and rt. Given that cap_relation, and in particular acap_relation, are straightforward and handle the cap references in exactly the same way, there does not seem to be a good reason for these sets to differ. These references feature most prominently in ex_nonz_cap_to/ex_nonz_cap_to', and these in turn are mainly seen as part of if_live_then_nonz_cap/if_live_then_nonz_cap'. Given that so few arch objects are considered to be live, we may not have encountered any problems with this before.
If we were to include further references at the Refine level so that they matched what AInvs currently has, then we should be able to prove the following cross lemma:
"⟦ex_nonz_cap_to ptr s; ∃ko. kheap s ptr = Some (ArchObj ko);
valid_objs s; pspace_relation (kheap s) (ksPSpace s');
pspace_aligned' s'; pspace_distinct' s'⟧
⟹ ex_nonz_cap_to' ptr s'"
These sets of references currently differ on all architectures and on both
masterandrt. Given thatcap_relation, and in particularacap_relation, are straightforward and handle the cap references in exactly the same way, there does not seem to be a good reason for these sets to differ. These references feature most prominently inex_nonz_cap_to/ex_nonz_cap_to', and these in turn are mainly seen as part ofif_live_then_nonz_cap/if_live_then_nonz_cap'. Given that so few arch objects are considered to be live, we may not have encountered any problems with this before.If we were to include further references at the Refine level so that they matched what AInvs currently has, then we should be able to prove the following cross lemma: