prove: cursor_mut_at at mm::frame::linked_list

[Marsman1996]

Strength assessment: stronger.
Intent preservation assessment: preserved.
Redundancy assessment: minor.
Score: 9/10.

  Rationale: The changes strengthen the target contract in ostd/src/mm/frame/linked_list.rs:428 by requiring list/region well-formedness and by
  guaranteeing that a successful cursor_mut_at returns a valid cursor owner pointing at frame. That matches the nearby documented intent that
  the cursor should be well-formed and point to the matching element.

  The owner invariant edits in ostd/specs/mm/frame/linked_list/linked_list_owners.rs:230 also strengthen consistency: nonempty lists must have
  a nonzero list_id, and each link’s tracked in_list permission value must agree with the logical list_id.

  The only deduction is minor redundancy/proof-shaping: the added cursor_mut_at preconditions around non-list safe slots and in_list == 0
  appear to restate properties that should mostly follow from region ownership invariants, so they add some maintenance burden. I do not see a
  spec weakening or a changed contract purpose.

[rikosellic]

This PR will be reviewed after #452 to avoid potential conflicts.

[rikosellic]

@Marsman1996 Please merge the latest main to check whether everything is consistent.

[rikosellic]

I think this pre-condition is suspicious because it is completely irrelevant with the LinkedListOwner. Maybe we need a better way to do this. I will think more about it when reviewing mm code. @SNoAnd What do you think?

[SNoAnd]

This is tricky. Because the frames owned by the LinkedList always come from UniqueFrame, we transfer ownership to the list itself, and the perms are carried by owner.list_own.perms and not found in regions. But the proof code in this function is old, and doesn't really work with the approach; it assumes that the perm can be found in regions.

The idiomatic approach would be to find paddr in owner.list_own.perms and extract it. in_list should match iff the perm is actually present.

[SNoAnd]

This is good progress. It is illustrating an issue with the permission division, though. It works great when the chosen paddr is part of the linked list, because we can access the permission directly. But if not, we still need to access the permission in order to read the slot before checking the list id. Hence the preconditions here asserting that the permission must otherwise be in regions.

I think that removing those preconditions will actually require us to retire the "uniquely-owned perms live with their owners" pattern and just keep all slot permissions in regions at all times. I have some sketches of what that looks like, I can see how tractable it would be to make the migration.

Currently this proof is vacuous if paddr is in a different linked list, or if it corresponds to a UniqueFrame or a page table node, the other instances where the permission is allowed to leave perms.