New approach to specifying iterators via a prophetic sequence encoding#2163
Draft
New approach to specifying iterators via a prophetic sequence encoding#2163
Conversation
generic proofs about iterator properties.
for the Skip/Take proofs to go through.
all_next(), which is an improvement on the old design.
reasonable invariant that says we only perform Next operations. This suffices to restore two Skip3 tests.
…n how to use it. (#2104) * cfg_features: add verus_in_verification feature In relation to #2063, this commit adds a new verus_in_verification feature flag that is intended for client usage (but only on use statements). Usage outside use statements can serve as an escape hatch for verification, possibly introducing unsoundness. This commit also adds documentation in the guide about the feature flag, how to use it and its pitfalls. * cfg_features: add allow unexpected_cfgs to default Cargo.toml generated by cargo-verus
This should save some CI time
a basic test passes.
Restores `peek`, but that causes a panic.
parno
commented
Feb 10, 2026
| } | ||
| } => Ok(()) | ||
| } | ||
| //test_verify_one_file_with_options! { |
Collaborator
Author
There was a problem hiding this comment.
I wasn't sure if we still wanted a test along these lines, but I can cook one up if we do.
parno
commented
Feb 10, 2026
Collaborator
Author
There was a problem hiding this comment.
I initially couldn't remember why this file changed, but it was due to 612d209 to make the encoding of the decreases clause more flexible.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
So far, this only updates the iterator definitions for
VecandRange. If we decide we like this style, we'll need to update the other containers, as well asSlicefor&Vec.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.