model-checking / verify-rust-std

Verifying the Rust standard library
https://model-checking.github.io/verify-rust-std/
Other
9 stars 7 forks source link

Tracking issue: Verifying raw pointer arithmetic #21

Open celinval opened 1 month ago

celinval commented 1 month ago

This is a tracking issue for the challenge proposal of verifying the raw pointer arithmetic.

jaisnan commented 4 weeks ago

Tracking issues should have links to the challenges they're tracking.

  1. In case, they're already added to the book, I am linking them to the issues.
  2. If not, can we add the links to the challenges to the issue description once the PR for that challenge has been merged?
celinval commented 4 weeks ago

This is a chicken and egg problem. We want to have the issue linking to the book and the book linking to the issue.

This requires a three step process, which we initially proposed to be the following:

  1. Create a tracking issue (not labeled with "Challenge" yet).
  2. Create the PR including the link to the issue.
  3. Once PR is merged, update the issue with the book link and the "Challenge" label.

I think updating the issue twice is more reasonable than updating the book twice since the latter needs a CR.

That said, this is tedious and manual, so anything that can reduce the manual work is welcome! :)