feat: add btree spec in vstd_extra

[Marsman1996]

No description provided.

[rikosellic]

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]

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.

[rikosellic]

Why can we compare these two types？

[Marsman1996]

We do not directly compare Key with Q. The BTreeMap API requires Key: Borrow<Q> and Q: Ord, so the stored key is first borrowed as &Q, then compared with the lookup key using Q::cmp. borrowed_key_cmp abstracts stored_key.borrow().cmp(key) because vstd does not provide a general specification for Borrow::borrow.