Sync the VeriFast proofs and provide guidance on same

[btj]

Updates the VeriFast proofs after linked_list.rs was modified by rust-lang@c39f33b .

Also:

• Added a bash script that attempts to automatically patch the proofs after the original file was changed.
• The VeriFast CI actions now produce an error alert suggesting to run this script, if a source file that is the subject of a VeriFast proof is changed.

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

[btj]

By the way: I noticed only a few hours ago that the VeriFast actions have been failing for a month :-( I wish there was a way for me to get notified when a VeriFast action fails on main.

[tautschnig]

By the way: I noticed only a few hours ago that the VeriFast actions have been failing for a month :-( I wish there was a way for me to get notified when a VeriFast action fails on main.

Given https://github.com/orgs/community/discussions/43415 I see a couple of options:

1. If there is a failure in your fork of this repository, you will be notified.
2. We can @mention you when anyone notices such a failure (and the script that you kindly provided doesn't do the trick).
3. We can create an issue and mention you.

[btj]

Yes, please don't hesitate to mention me and/or create an issue when this happens again! And indeed, I should probably set up some kind of a cron job that syncs my fork with this repo and/or monitors the status of the VeriFast actions.

[tautschnig]

Yes, please don't hesitate to mention me and/or create an issue when this happens again! And indeed, I should probably set up some kind of a cron job that syncs my fork with this repo and/or monitors the status of the VeriFast actions.

Cool, we'll be sure to mention you, but please just let us know if/when to stop :)

[btj]

@tautschnig I updated the VeriFast action so that it sends me an e-mail on failure. (You may want to re-review the PR.) Also, I created a cron job that reminds me once a day if the VeriFast action is failing.

[tautschnig]

Re-approving to affirm the additional changes.

[remi-delmas-3000]

Hi @btj ! Thanks for the udpate. I approved the PR.

Could we also consider defining an action that would attempt to patch the proofs with upstream changes (without doing anything else) and submit a PR if it succeeds ?

We recently automated merging upstream std-lib changes into this verify-rust-std repo, so this could extend the action to automatically patching the verifast proofs whenever it is possible.

We already have something similar going on in the Kani workflow where we continuously attempt to build kani and run regression tests with the current head of all our dependencies (rust toolchain, cbmc , etc.), issue a PR if it succeeds. This really helps keeping up to date with changes.

[btj]

Could we also consider defining an action that would attempt to patch the proofs with upstream changes (without doing anything else) and submit a PR if it succeeds ?

We recently automated merging upstream std-lib changes into this verify-rust-std repo, so this could extend the action to automatically patching the verifast proofs whenever it is possible.

We already have something similar going on in the Kani workflow where we continuously attempt to build kani and run regression tests with the current head of all our dependencies (rust toolchain, cbmc , etc.), issue a PR if it succeeds. This really helps keeping up to date with changes.

I think adding logic to the update-subtree workflow to install the VeriFast toolchain and try and run verifast-proofs/check-verifast-proofs.mysh and, if it fails, try and run verifast-proofs/patch-verifast-proofs.sh, and if that succeeds, including those proof changes into the update-subtree PR would make a lot of sense. But I propose that that is not an urgent thing to do. The present PR ensures I am notified immediately and reminded daily whenever the VeriFast proofs fail; whenever they fail again I will (manually, for now) create a PR to fix them in short order.

[tautschnig]

We already have something similar going on in the Kani workflow where we continuously attempt to build kani and run regression tests with the current head of all our dependencies (rust toolchain, cbmc , etc.), issue a PR if it succeeds. This really helps keeping up to date with changes.

I think adding logic to the update-subtree workflow to install the VeriFast toolchain and try and run verifast-proofs/check-verifast-proofs.mysh and, if it fails, try and run verifast-proofs/patch-verifast-proofs.sh, and if that succeeds, including those proof changes into the update-subtree PR would make a lot of sense. But I propose that that is not an urgent thing to do. The present PR ensures I am notified immediately and reminded daily whenever the VeriFast proofs fail; whenever they fail again I will (manually, for now) create a PR to fix them in short order.

Thanks both! I'd suggest we apply a work-stealing algorithm here and just race for whoever gets to this first.