Add 10 more challenges #260
Conversation
|
|
||
| The verification must be unbounded---it must hold for slices of arbitrary length. | ||
|
|
||
| It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. |
There was a problem hiding this comment.
We should be explicit about which concrete types we want proofs for.
| @@ -0,0 +1,79 @@ | |||
| # Challenge 20: Verify the memory safety of `slice` functions | |||
There was a problem hiding this comment.
This file name has a typo (silce instead of slice).
| - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) | ||
| - **Start date:** *2025/03/07* | ||
| - **End date:** *2025/10/17* | ||
| - **Reward:** *?* |
There was a problem hiding this comment.
Note for the future: we'll need to ping @rahulku for reward numbers before merging this, but let's get the content reviews done before doing that.
|
|
||
| | Function | | ||
| |---------| | ||
| |next_back_unchecked| |
There was a problem hiding this comment.
@celinval already started work on this in #148 . So we either need to update this challenge to acknowledge that fact and be explicit about what remains to be done, or, if we don't think enough remains to justify a challenge, remove it altogether. You should audit the work that Celina did and see what remains to be done, and we can make a decision from there.
There was a problem hiding this comment.
Thanks. I have taken a look at it. The different is that this challenge requires unbounded proofs.
|
|
||
| The verification must be unbounded---it must hold for slices of arbitrary length. | ||
|
|
||
| It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. |
There was a problem hiding this comment.
Same comment about being explicit about which of these primitive types we care about.
In this PR, I add 10 new challenge:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.