Skip to content

vstd: add specs for BinaryHeap, BTreeMap, and BTreeSet#2059

Open
briangmilnes wants to merge 1 commit intoverus-lang:mainfrom
briangmilnes:milnes-more-rust-wrapping
Open

vstd: add specs for BinaryHeap, BTreeMap, and BTreeSet#2059
briangmilnes wants to merge 1 commit intoverus-lang:mainfrom
briangmilnes:milnes-more-rust-wrapping

Conversation

@briangmilnes
Copy link

Add formal specifications for three Rust stdlib collection types (easy additions suggested by veracity-analyze_rust_wrapping_needs).

  • BinaryHeap: push, pop, peek, len, is_empty, clear, with DeepView support and is_heap_max maximality predicate
  • BTreeMap: new, insert, get, contains_key, remove, clear, clone, len, is_empty, with iterators (Keys, Values, Iter, IntoIter) and DeepView
  • BTreeSet: new, insert, remove, contains, len, is_empty, clear, clone, with iterators (Iter, IntoIter) and DeepView

Includes comprehensive tests covering:

  • All methods with value verification
  • Iterator tests with for-loop, while-loop, and loop-match patterns
  • DeepView tests for nested types

Also adds CONTRIBUTING.md section on controlling test parallelism (RUST_TEST_THREADS) since vargo does not forward -j flag.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Add formal specifications for three Rust stdlib collection types:

- BinaryHeap: push, pop, peek, len, is_empty, clear, with DeepView support
  and is_heap_max maximality predicate
- BTreeMap: new, insert, get, contains_key, remove, clear, clone, len,
  is_empty, with iterators (Keys, Values, Iter, IntoIter) and DeepView
- BTreeSet: new, insert, remove, contains, len, is_empty, clear, clone,
  with iterators (Iter, IntoIter) and DeepView

Includes comprehensive tests covering:
- All methods with value verification
- Iterator tests with for-loop, while-loop, and loop-match patterns
- DeepView tests for nested types

Also adds CONTRIBUTING.md section on controlling test parallelism
(RUST_TEST_THREADS) since vargo does not forward -j flag.
Copy link
Collaborator

@tjhance tjhance left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I haven't looked at this in detail, but at the very least, these containers need to use some sort of obeys_key_model assumption (similar to our specs for HashMap), i.e., an assumption that comparisons are deterministic and that equality is compatible with Ord.

@briangmilnes
Copy link
Author

10q! Got it, but this is going to take some work and I might as well then put in my additions for Ordering in cmp. Which I trust more now. What's the process? Do I just close out this PR as it's getting dated? Get up to date and start a new one?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants