8000 iter: add `kani` proof for `next_unchecked` (#280) by 0xllx0 · Pull Request #501 · model-checking/verify-rust-std · GitHub
[go: up one dir, main page]
Skip to content

iter: add kani proof for next_unchecked (#280) #501

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
Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

iter: add kani proof for next_unchecked (#280) #501

wants to merge 1 commit into from

Conversation

0xllx0
Copy link
@0xllx0 0xllx0 commented Oct 7, 2025

Adds kani proof and function contract for UncheckedIterator::next_unchecked.

Ensures that the safety invariants are held using the model checker.

Related #280

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@0xllx0 0xllx0 requested a review from a team as a code owner October 7, 2025 15:56
@tautschnig
Copy link
Member

Thank you for this contribution! Could you please resolve conflicts as there have been updates to main (which include merging some additional contracts). Thank you!

@0xllx0
iter: add kani proof for next_unchecked (rust-lang#280)
9e55863 
Adds `kani` proof and function contract for
`UncheckedIterator::next_unchecked`.

Ensures that the safety invariants are held using the model checker.
@0xllx0 0xllx0 force-pushed the model-checking/iter-next-unchecked branch from 10299a4 to 9e55863 Compare October 10, 2025 16:09
@0xllx0
Copy link
Author
0xllx0 commented Oct 10, 2025 •
edited
Loading

Thank you for this contribution! Could you please resolve conflicts as there have been updates to main (which include merging some additional contracts). Thank you!

Hi, it looks like the conflict was generated by an LLM commit from the user @vonaka. Is this common to have other contributors submit LLM contributions conflicting with work being done by human contributors?

I'm not sure I want to continue contributing if my work will just be poorly regurgitated by some LLM, and then I have to be tasked with cleaning up the mess.

You were also listed as co-author in the conflicting commit: 525c2f0

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

Reviewers

No reviews

Assignees

@0xllx0 0xllx0

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@0xllx0 @tautschnig
0