Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

use broadcast for map/set/multiset_properties #1443

Merged
merged 4 commits into from
Feb 12, 2025
Merged

use broadcast for map/set/multiset_properties #1443

merged 4 commits into from
Feb 12, 2025

Conversation

ahuoguo
Copy link
Collaborator

@ahuoguo ahuoguo commented Feb 10, 2025

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

@ahuoguo
Copy link
Collaborator Author

ahuoguo commented Feb 10, 2025

veritas report for verus vstd-broadcast (c57a5a784ca528bc613cabd8c8039b61d2872f67) with features: singular

project revspec outcome total verus time (ms) smt run time (ms)
verus-vstd vstd-broadcast (c57a5a784ca528bc613cabd8c8039b61d2872f67) success (836 verified, 0 errors) 33308 11697
memory-allocator main (bc2ba93dc916aef3afa347b92c5c8d66cb23fee7) success (730 verified, 0 errors) 113826 86719
page-table main (389645228d1da283369473dd80595b8f4ea892c3) success (242 verified, 0 errors) 29632 41572
verified-storage main (7b35ddb12fd505e16a58d9462f15aed559570267) success (272 verified, 0 errors) 15002 13891
node-replication main (b3ca921103220b20c6cc144bd2f7d4f259b7c8be) success (254 verified, 0 errors) 11980 3743

@ahuoguo ahuoguo marked this pull request as ready for review February 10, 2025 23:14
@ahuoguo ahuoguo requested a review from utaal February 11, 2025 15:23
@utaal
Copy link
Collaborator

utaal commented Feb 11, 2025

@ahuoguo checked that the verification times match the prior ones in veritas.

utaal
utaal requested changes Feb 11, 2025
View reviewed changes
Copy link
Collaborator

@utaal utaal left a comment

Choose a reason for hiding this comment

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

Some inline comments / questions.

source/vstd/set_lib.rs Show resolved Hide resolved
source/vstd/set_lib.rs Show resolved Hide resolved
source/vstd/set_lib.rs Outdated Show resolved Hide resolved
utaal
utaal reviewed Feb 12, 2025
View reviewed changes
source/vstd/seq_lib.rs Outdated Show resolved Hide resolved
utaal
utaal reviewed Feb 12, 2025
View reviewed changes
source/vstd/seq_lib.rs Outdated Show resolved Hide resolved
utaal
utaal approved these changes Feb 12, 2025
View reviewed changes
Copy link
Collaborator

@utaal utaal left a comment

Choose a reason for hiding this comment

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

One comment, but looks good to me otherwise.

source/vstd/set_lib.rs Outdated Show resolved Hide resolved
@ahuoguo @utaal
Update source/vstd/set_lib.rs
c8948c5 
Co-authored-by: Andrea Lattuada <andrea@lattuada.me>
@ahuoguo ahuoguo merged commit 10bd10b into verus-lang:main Feb 12, 2025
11 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@utaal utaal utaal approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ahuoguo @utaal