iter: add kani proof for next_unchecked (#280)

[0xllx0]

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.

[tautschnig]

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]

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

[tautschnig]

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?

Thank you for your contribution! I'm afraid I don't really see a way to know whether contributions (irrespective of whether they are created by a human or a machine) will eventually conflict with work done by another party? On this occasion, #473 was created well ahead of your PR.

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.

We do not currently have any rules that exclude LLM-generated contributions, and indeed we generally have no way of telling in which way a particular contribution was created. Given the overall number of contributors is still low two-digits, I don't think it will happen all that often that contributions overlap at all.

Would you have any suggestions towards our rules or our processes to improve the contributor experience?

[tautschnig]

Suggested change

	#[kani::proof]
	#[kani::proof_for_contract(UncheckedIterator::next_unchecked)]

so that Kani actually uses the requires clause.

[0xllx0]

This does not work:

error: The function specified in the `proof_for_contract` attribute, `UncheckedIterator::next_unchecked`, is not reachable from the harness `verify_next_unchecked`.
  --> /home/user/src/rust/library/core/src/iter/traits/unchecked_iterator.rs:46:1
   |
46 | fn verify_next_unchecked() {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = help: Make sure that `verify_next_unchecked` calls `UncheckedIterator::next_unchecked`

error: could not compile `core` (lib) due to 1 previous error; 1 warning emitted
warning: build failed, waiting for other jobs to finish...
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

[0xllx0]

Thank you for your contribution! I'm afraid I don't really see a way to know whether contributions (irrespective of whether they are created by a human or a machine) will eventually conflict with work done by another party? On this occasion, #473 was created well ahead of your PR.

Likewise, thank you for your review/feedback. I know conflicts happen, regardless if the changes are automated, or not. #473 may have been opened a while ago, but I was specifically referring to the conflicting commit (525c2f0), which was committed after my changes.

Would you have any suggestions towards our rules or our processes to improve the contributor experience?

I don't know what rules/procedures you have in place, nor the resources the project has available to handle contributions. Given the size of the codebase, I understand it can be hard to keep track of all ongoing work, and where conflicts can arise. I don't know of any tenable solutions to help mitigate these conflicts.

Again, what initially concerned me was the timing of commit conflict. I comment in the tracking issue for the challenge, get the go-ahead to contribute, and submit a PR with some initial work toward one of the challenge goals. Then, within a short time, a contributor piloting an LLM commits changes directly in conflict with my contribution.

It looks like a number of merges occurred in #473, so maybe that is what caused the effective commit date to be after my commit, who knows.