Skip to content

feat: add btree spec in vstd_extra - #704

Open
Marsman1996 wants to merge 2 commits into
asterinas:mainfrom
Marsman1996:btree
Open

feat: add btree spec in vstd_extra#704
Marsman1996 wants to merge 2 commits into
asterinas:mainfrom
Marsman1996:btree

Conversation

@Marsman1996

Copy link
Copy Markdown
Collaborator

No description provided.

@Marsman1996 Marsman1996 mentioned this pull request Aug 12, 2026
2 tasks
@Marsman1996 Marsman1996 added the AI-assist AI-aided proof or generation label Aug 12, 2026
@rikosellic

Copy link
Copy Markdown
Collaborator

The get_mut part looks good to me, but the Cursor is not very informative. I've been thinking about the model of the Cursor, and what I thought was something like

{
   /// The ordered sequence of keys
   pub keys: Seq<Key>
   /// The position of the cursor. According to the documentation, the cursor is located in the gap between two keys, we can use this field to refer to the index of the element after the cursor.
   pub position: int
  /// The submap of the BtreeMap view that can be accessed by the cursor. Its keys should match the keys field.
  pub map: Map<Key, Value>
}

@rikosellic

Copy link
Copy Markdown
Collaborator

borrowed_key_ordering_matches looks like a good design to me. And it seems this is missing from the spec of BTreeMap::get in vstd. You may create a PR about this.

Comment thread verified_libs/vstd_extra/src/external/btree.rs Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

AI-assist AI-aided proof or generation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants