Prove admit() in ostd/src with spec modification#392
Prove admit() in ostd/src with spec modification#392Marsman1996 wants to merge 7 commits intoasterinas:mainfrom
admit() in ostd/src with spec modification#392Conversation
|
The |
Marsman1996
force-pushed
the
prove-admit-new
branch
from
4fedcc4 to
4aa9a46
Compare
|
KVerus cannot prove the rest 9 |
This comment was marked as off-topic.
This comment was marked as off-topic.
|
Reviewing this requires a deep understanding of the current MetaSlot model, which, unfortunately, I do not have yet. Need some time. |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| let cur_idx = frame_to_index_spec(cur_mapped_pa); | ||
| let tracked slot_perm = EntryOwner::<KernelPtConfig>::placeholder_slot_perm( | ||
| cur_mapped_pa, | ||
| &*regions, | ||
| ); | ||
| regions.slots.tracked_insert(cur_idx, slot_perm); | ||
| regions_before_map.frame_slot_perm_insert_preserves_inv(cur_idx, slot_perm, *regions); |
There was a problem hiding this comment.
This proof mints a slot_perm via EntryOwner::placeholder_slot_perm(...) and inserts it into regions.slots to satisfy item_slot_in_regions. placeholder_slot_perm is an axiomatically-created permission intended as a temporary placeholder, so using it here effectively bypasses the linear “slot permission” discipline and can make the verification unsound. Instead, thread the real slot permission for cur_mapped_pa into this function (e.g., via preconditions/arguments that provide the existing regions.slots[idx] permission) or restructure so the CursorMut::map precondition is met without fabricating permissions.
|
I need to dig into this a little more, but my current thoughts are that the spec modifications look reasonable but some of the proofs are questionable. In particular the ones that use
|
|
I looked into |
You can directly modify this PR if you want. |
This time I add a spec modfication evaluation module and the agent drops the specs whose rating is lower than 7