Conversation
…odel-checking#292) `git subtree merge --squash` will always reset the subtree to the state of the tree that is being merged from, which effectively eradicates all our local changes. This was just masked by merge conflicts arising as we were always attempted to merge from some long-ago version as we hadn't consistently kept "git-subtree-split" markers. This PR now amends the pull request descriptions to make sure we retain the necessary information and uses `git merge` instead of the subtree command. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…#309) This is an automated PR to merge library subtree updates from 2025-03-17 (rust-lang/rust@227690a) to 2025-03-18 (rust-lang/rust@43a2e9d), inclusive. This is a clean merge, no conflicts were detected. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 8902bd3 --------- Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: fuyangpengqi <995764973@qq.com> Signed-off-by: Ookiineko <chiisaineko@protonmail.com> Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Signed-off-by: Sean Cross <sean@xobs.io> Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com> Co-authored-by: Folkert de Vries <folkert@folkertdev.nl> Co-authored-by: Will Woods <w@wizard.zone> Co-authored-by: Matthias Krüger <matthias.krueger@famsik.de> Co-authored-by: Slanterns <slanterns.w@gmail.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: Peter Jaszkowiak <p.jaszkow@gmail.com> Co-authored-by: Karol Zwolak <karolzwolak7@gmail.com> Co-authored-by: binarycat <binarycat@envs.net> Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: Speedy_Lex <alex.ciocildau@gmail.com> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: fuyangpengqi <995764973@qq.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Henry Jiang <henry.jiang1@ibm.com> Co-authored-by: pcorwin <phoebe.corwin23@gmail.com> Co-authored-by: Michael Goulet <michael@errs.io> Co-authored-by: Jubilee <workingjubilee@gmail.com> Co-authored-by: 许杰友 Jieyou Xu (Joe) <39484203+jieyouxu@users.noreply.github.com> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: Oli Scherer <github333195615777966@oli-obk.de> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: Redddy <78539407+reddevilmidzy@users.noreply.github.com> Co-authored-by: Eric Huss <eric@huss.org> Co-authored-by: Santiago Pastorino <spastorino@gmail.com> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: Kevin Reid <kpreid@switchb.org> Co-authored-by: ltdk <usr@ltdk.xyz> Co-authored-by: Tobias Decking <Tobias.Decking@gmail.com> Co-authored-by: Steven Malis <smmalis37@gmail.com> Co-authored-by: Martin Habovstiak <martin.habovstiak@gmail.com> Co-authored-by: bdbai <bdbaiapp@163.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Jethro Beekman <jethro@fortanix.com> Co-authored-by: LemonJ <1632798336@qq.com> Co-authored-by: Bastian Kersting <bkersting@google.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: 王宇逸 <Strawberry_Str@hotmail.com> Co-authored-by: Ookiineko <chiisaineko@protonmail.com> Co-authored-by: Nicole LeGare <legare@google.com> Co-authored-by: Nicole LeGare <legaren@immunant.com> Co-authored-by: Nicole L <dlegare.1001@gmail.com> Co-authored-by: Arjun Ramesh <arjunr2@andrew.cmu.edu> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru> Co-authored-by: Oli Scherer <git-spam-no-reply9815368754983@oli-obk.de> Co-authored-by: Jakub Beránek <berykubik@gmail.com> Co-authored-by: Sean Cross <sean@xobs.io> Co-authored-by: Aurelia Molzer <5550310+HeroicKatora@users.noreply.github.com> Co-authored-by: beetrees <b@beetr.ee> Co-authored-by: Josh Stone <jistone@redhat.com> Co-authored-by: Manish Goregaokar <manishsmail@gmail.com> Co-authored-by: ClearLove <98693523+DiuDiu777@users.noreply.github.com> Co-authored-by: Thom Chiovoloni <thom@shift.click> Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com> Co-authored-by: León Orell Valerian Liehr <me@fmease.dev> Co-authored-by: Yotam Ofek <yotam.ofek@gmail.com> Co-authored-by: Noratrieb <48135649+Noratrieb@users.noreply.github.com> Co-authored-by: gitbot <git@bot>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This PR adds: 1. Challenge 17 : for slice functions 2. Chalenge 18: for slice-iter's functions generated by macros By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech <cmzech@amazon.com> Co-authored-by: Michael Tautschnig <mt@debian.org>
In this PR, I add a challenge for Iterator functions in (library/core/src/iter/adapters) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech <cmzech@amazon.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
…#312) This is an automated PR to merge library subtree updates from 2025-03-18 (rust-lang/rust@43a2e9d) to 2025-04-01 (rust-lang/rust@0b45675) (inclusive) into main. `git merge` resulted in conflicts, which require manual resolution. Files were commited with merge conflict markers. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: c60865a --------- Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Signed-off-by: Sean Cross <sean@xobs.io> Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Nicole LeGare <legare@google.com> Co-authored-by: Nicole LeGare <legaren@immunant.com> Co-authored-by: Nicole L <dlegare.1001@gmail.com> Co-authored-by: Kevin Reid <kpreid@switchb.org> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: Arjun Ramesh <arjunr2@andrew.cmu.edu> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru> Co-authored-by: Oli Scherer <git-spam-no-reply9815368754983@oli-obk.de> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: Jakub Beránek <berykubik@gmail.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Sean Cross <sean@xobs.io> Co-authored-by: Aurelia Molzer <5550310+HeroicKatora@users.noreply.github.com> Co-authored-by: Eric Huss <eric@huss.org> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: beetrees <b@beetr.ee> Co-authored-by: Josh Stone <jistone@redhat.com> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: Berrysoft <Strawberry_Str@hotmail.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: Manish Goregaokar <manishsmail@gmail.com> Co-authored-by: ClearLove <98693523+DiuDiu777@users.noreply.github.com> Co-authored-by: Thom Chiovoloni <thom@shift.click> Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com> Co-authored-by: Michael Goulet <michael@errs.io> Co-authored-by: The Miri Cronjob Bot <miri@cron.bot> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: Tobias Bucher <tobiasbucher5991@gmail.com> Co-authored-by: León Orell Valerian Liehr <me@fmease.dev> Co-authored-by: Yotam Ofek <yotam.ofek@gmail.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: 许杰友 Jieyou Xu (Joe) <39484203+jieyouxu@users.noreply.github.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Noratrieb <48135649+Noratrieb@users.noreply.github.com> Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com> Co-authored-by: Ibraheem Ahmed <ibraheem@ibraheem.ca> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: Taiki Endo <te316e89@gmail.com> Co-authored-by: bendn <bend.n@outlook.com> Co-authored-by: Caleb Zulawski <caleb.zulawski@gmail.com> Co-authored-by: Jana Dönszelmann <jana@donsz.nl> Co-authored-by: syvb <me@iter.ca> Co-authored-by: Sebastian Urban <surban@surban.net> Co-authored-by: Bardi Harborow <bardi@bardiharborow.com> Co-authored-by: moxian <moxian@users.noreply.github.com> Co-authored-by: Frank King <frankking1729@gmail.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com> Co-authored-by: Mads Marquart <mads@marquart.dk> Co-authored-by: Christopher Durham <cad97@cad97.com> Co-authored-by: Rafael Bachmann <rafael.bachmann.93@gmail.com> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: Daniel Henry-Mantilla <daniel.henry.mantilla@gmail.com> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
…#313) 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.
…#318) This is an automated PR to merge library subtree updates from 2025-04-01 (rust-lang/rust@0b45675) to 2025-04-04 (rust-lang/rust@00095b3), inclusive. This is a clean merge, no conflicts were detected. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 0cce469 --------- Signed-off-by: Sean Cross <sean@xobs.io> Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Oli Scherer <git-spam-no-reply9815368754983@oli-obk.de> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: Jakub Beránek <berykubik@gmail.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Sean Cross <sean@xobs.io> Co-authored-by: Aurelia Molzer <5550310+HeroicKatora@users.noreply.github.com> Co-authored-by: Eric Huss <eric@huss.org> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: Nicole L <dlegare.1001@gmail.com> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: beetrees <b@beetr.ee> Co-authored-by: Josh Stone <jistone@redhat.com> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: Berrysoft <Strawberry_Str@hotmail.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: Manish Goregaokar <manishsmail@gmail.com> Co-authored-by: ClearLove <98693523+DiuDiu777@users.noreply.github.com> Co-authored-by: Thom Chiovoloni <thom@shift.click> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com> Co-authored-by: Michael Goulet <michael@errs.io> Co-authored-by: The Miri Cronjob Bot <miri@cron.bot> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: Tobias Bucher <tobiasbucher5991@gmail.com> Co-authored-by: León Orell Valerian Liehr <me@fmease.dev> Co-authored-by: Yotam Ofek <yotam.ofek@gmail.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: 许杰友 Jieyou Xu (Joe) <39484203+jieyouxu@users.noreply.github.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Noratrieb <48135649+Noratrieb@users.noreply.github.com> Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com> Co-authored-by: Ibraheem Ahmed <ibraheem@ibraheem.ca> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: Taiki Endo <te316e89@gmail.com> Co-authored-by: bendn <bend.n@outlook.com> Co-authored-by: Caleb Zulawski <caleb.zulawski@gmail.com> Co-authored-by: Jana Dönszelmann <jana@donsz.nl> Co-authored-by: syvb <me@iter.ca> Co-authored-by: Sebastian Urban <surban@surban.net> Co-authored-by: Bardi Harborow <bardi@bardiharborow.com> Co-authored-by: lcnr <rust@lcnr.de> Co-authored-by: moxian <moxian@users.noreply.github.com> Co-authored-by: Frank King <frankking1729@gmail.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com> Co-authored-by: Mads Marquart <mads@marquart.dk> Co-authored-by: Christopher Durham <cad97@cad97.com> Co-authored-by: Rafael Bachmann <rafael.bachmann.93@gmail.com> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: Daniel Henry-Mantilla <daniel.henry.mantilla@gmail.com> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: clubby789 <jamie@hill-daniel.co.uk> Co-authored-by: Daniel Bloom <daniel@wormholelabs.xyz> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
…#320) This is an automated PR to merge library subtree updates from 2025-04-04 (rust-lang/rust@00095b3) to 2025-04-06 (rust-lang/rust@5e17a2a) (inclusive) into main. `git merge` resulted in conflicts, which require manual resolution. Files were commited with merge conflict markers. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: a5c6692 --------- Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: Berrysoft <Strawberry_Str@hotmail.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: Manish Goregaokar <manishsmail@gmail.com> Co-authored-by: Josh Stone <jistone@redhat.com> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: ClearLove <98693523+DiuDiu777@users.noreply.github.com> Co-authored-by: Thom Chiovoloni <thom@shift.click> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Michael Goulet <michael@errs.io> Co-authored-by: The Miri Cronjob Bot <miri@cron.bot> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: Tobias Bucher <tobiasbucher5991@gmail.com> Co-authored-by: León Orell Valerian Liehr <me@fmease.dev> Co-authored-by: Yotam Ofek <yotam.ofek@gmail.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: 许杰友 Jieyou Xu (Joe) <39484203+jieyouxu@users.noreply.github.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Noratrieb <48135649+Noratrieb@users.noreply.github.com> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com> Co-authored-by: Ibraheem Ahmed <ibraheem@ibraheem.ca> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: Taiki Endo <te316e89@gmail.com> Co-authored-by: Andrei Damian <andreidaamian@gmail.com> Co-authored-by: bendn <bend.n@outlook.com> Co-authored-by: Caleb Zulawski <caleb.zulawski@gmail.com> Co-authored-by: Jana Dönszelmann <jana@donsz.nl> Co-authored-by: syvb <me@iter.ca> Co-authored-by: Sebastian Urban <surban@surban.net> Co-authored-by: Bardi Harborow <bardi@bardiharborow.com> Co-authored-by: lcnr <rust@lcnr.de> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: moxian <moxian@users.noreply.github.com> Co-authored-by: Frank King <frankking1729@gmail.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com> Co-authored-by: Mads Marquart <mads@marquart.dk> Co-authored-by: Christopher Durham <cad97@cad97.com> Co-authored-by: Rafael Bachmann <rafael.bachmann.93@gmail.com> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: Daniel Henry-Mantilla <daniel.henry.mantilla@gmail.com> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: clubby789 <jamie@hill-daniel.co.uk> Co-authored-by: Daniel Bloom <daniel@wormholelabs.xyz> Co-authored-by: Jake Wharton <jw@squareup.com> Co-authored-by: Calder Coalson <caldercoalson@gmail.com> Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
We now do all updates via github actions, which neither use the scripts removed in this commit nor do we do it the same way as those scripts. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…is up-to-date (model-checking#326) When the PR updating the `subtree/library` branch has been merged already we may still need to bring updates into `main` that haven't previously been added to a pull request. This situation arises when an older merge-into-main PR was still open at the time where the subtree automation creating the `subtree/library` update PR ran. The changes in this PR avoid this problem by making sure the merge-into-main part of the automation is run even when `subtree/library` is already up-to-date. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is a helper script to collect all existing contracts for subsequent review or analysis. This facilitates metrics we want to report. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…#329) This is an automated PR to merge library subtree updates from 2025-04-06 (rust-lang/rust@5e17a2a) to 2025-04-07 (rust-lang/rust@2fa8b11), inclusive. This is a clean merge, no conflicts were detected. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 0b8a1cd --------- Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Michael Goulet <michael@errs.io> Co-authored-by: The Miri Cronjob Bot <miri@cron.bot> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: Tobias Bucher <tobiasbucher5991@gmail.com> Co-authored-by: León Orell Valerian Liehr <me@fmease.dev> Co-authored-by: Yotam Ofek <yotam.ofek@gmail.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: 许杰友 Jieyou Xu (Joe) <39484203+jieyouxu@users.noreply.github.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Noratrieb <48135649+Noratrieb@users.noreply.github.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com> Co-authored-by: Ibraheem Ahmed <ibraheem@ibraheem.ca> Co-authored-by: Berrysoft <Strawberry_Str@hotmail.com> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: Taiki Endo <te316e89@gmail.com> Co-authored-by: Andrei Damian <andreidaamian@gmail.com> Co-authored-by: bendn <bend.n@outlook.com> Co-authored-by: Caleb Zulawski <caleb.zulawski@gmail.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: Jana Dönszelmann <jana@donsz.nl> Co-authored-by: syvb <me@iter.ca> Co-authored-by: Sebastian Urban <surban@surban.net> Co-authored-by: Bardi Harborow <bardi@bardiharborow.com> Co-authored-by: lcnr <rust@lcnr.de> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: moxian <moxian@users.noreply.github.com> Co-authored-by: Frank King <frankking1729@gmail.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com> Co-authored-by: Mads Marquart <mads@marquart.dk> Co-authored-by: Christopher Durham <cad97@cad97.com> Co-authored-by: Rafael Bachmann <rafael.bachmann.93@gmail.com> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: Nikolai Kuklin <nickkuklin@gmail.com> Co-authored-by: Daniel Henry-Mantilla <daniel.henry.mantilla@gmail.com> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: clubby789 <jamie@hill-daniel.co.uk> Co-authored-by: Daniel Bloom <daniel@wormholelabs.xyz> Co-authored-by: Jake Wharton <jw@squareup.com> Co-authored-by: Kornel <kornel@geekhood.net> Co-authored-by: Calder Coalson <caldercoalson@gmail.com> Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
…#336) This is an automated PR to merge library subtree updates from 2025-04-07 (rust-lang/rust@2fa8b11) to 2025-04-21 (rust-lang/rust@b8c54d6) (inclusive) into main. `git merge` resulted in conflicts, which require manual resolution. Files were commited with merge conflict markers. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 2ab28f3 --------- Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Signed-off-by: Petros Angelatos <petrosagg@gmail.com> Signed-off-by: Huang Qi <huangqi3@xiaomi.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: beetrees <b@beetr.ee> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: Mads Marquart <mads@marquart.dk> Co-authored-by: Christopher Durham <cad97@cad97.com> Co-authored-by: James Wainwright <james.wainwright@lowrisc.org> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: Rafael Bachmann <rafael.bachmann.93@gmail.com> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: Nikolai Kuklin <nickkuklin@gmail.com> Co-authored-by: Frank King <frankking1729@gmail.com> Co-authored-by: Daniel Henry-Mantilla <daniel.henry.mantilla@gmail.com> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: clubby789 <jamie@hill-daniel.co.uk> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: Daniel Bloom <daniel@wormholelabs.xyz> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: Jake Wharton <jw@squareup.com> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Kornel <kornel@geekhood.net> Co-authored-by: Calder Coalson <caldercoalson@gmail.com> Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: izarma <phuckuhh@gmail.com> Co-authored-by: Bennet Bleßmann <bb-github@t-online.de> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Jonathan Gruner <jogru0@gmail.com> Co-authored-by: Stan Manilov <stanislav.manilov@gmail.com> Co-authored-by: Gabriel Bjørnager Jensen <gabriel@achernar.io> Co-authored-by: lincot <lincot@disroot.org> Co-authored-by: timesince <seekseat@icloud.com> Co-authored-by: Boxy <rust@boxyuwu.dev> Co-authored-by: oyvindln <oyvindln@users.noreply.github.com> Co-authored-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: Folkert de Vries <folkert@folkertdev.nl> Co-authored-by: Bastian Kersting <bkersting@google.com> Co-authored-by: Petros Angelatos <petrosagg@gmail.com> Co-authored-by: Jesus Checa Hidalgo <jchecahi@redhat.com> Co-authored-by: Michael Howell <michael@notriddle.com> Co-authored-by: Ricardo Fernández Serrata <76864299+Rudxain@users.noreply.github.com> Co-authored-by: GenYuLi <witherslin@synology.com> Co-authored-by: Chris Denton <christophersdenton@gmail.com> Co-authored-by: Amanieu d'Antras <amanieu@gmail.com> Co-authored-by: Sky <sky@sky9.dev> Co-authored-by: Huang Qi <huangqi3@xiaomi.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: 0x79de <0x79de@gmail.com> Co-authored-by: binarycat <binarycat@envs.net> Co-authored-by: Glyn Normington <glyn.normington@gmail.com> Co-authored-by: Tamir Duberstein <tamird@gmail.com> Co-authored-by: Josh Triplett <josh@joshtriplett.org> Co-authored-by: Bastian Kersting <bastian@cmbt.de> Co-authored-by: Lyndon Brown <jnqnfe@gmail.com> Co-authored-by: Patrick Mooney <pmooney@pfmooney.com> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
…#340) This is an automated PR to merge library subtree updates from 2025-04-21 (rust-lang/rust@b8c54d6) to 2025-04-23 (rust-lang/rust@6bc57c6), inclusive. This is a clean merge, no conflicts were detected. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 54a7b4f --------- Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Signed-off-by: Petros Angelatos <petrosagg@gmail.com> Signed-off-by: Huang Qi <huangqi3@xiaomi.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: Frank King <frankking1729@gmail.com> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: Daniel Henry-Mantilla <daniel.henry.mantilla@gmail.com> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: clubby789 <jamie@hill-daniel.co.uk> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: Daniel Bloom <daniel@wormholelabs.xyz> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: Jake Wharton <jw@squareup.com> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Kornel <kornel@geekhood.net> Co-authored-by: Calder Coalson <caldercoalson@gmail.com> Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: izarma <phuckuhh@gmail.com> Co-authored-by: Bennet Bleßmann <bb-github@t-online.de> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Jonathan Gruner <jogru0@gmail.com> Co-authored-by: Stan Manilov <stanislav.manilov@gmail.com> Co-authored-by: Gabriel Bjørnager Jensen <gabriel@achernar.io> Co-authored-by: lincot <lincot@disroot.org> Co-authored-by: timesince <seekseat@icloud.com> Co-authored-by: Boxy <rust@boxyuwu.dev> Co-authored-by: oyvindln <oyvindln@users.noreply.github.com> Co-authored-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: Folkert de Vries <folkert@folkertdev.nl> Co-authored-by: Bastian Kersting <bkersting@google.com> Co-authored-by: Petros Angelatos <petrosagg@gmail.com> Co-authored-by: Jesus Checa Hidalgo <jchecahi@redhat.com> Co-authored-by: Michael Howell <michael@notriddle.com> Co-authored-by: Ricardo Fernández Serrata <76864299+Rudxain@users.noreply.github.com> Co-authored-by: GenYuLi <witherslin@synology.com> Co-authored-by: Chris Denton <christophersdenton@gmail.com> Co-authored-by: Amanieu d'Antras <amanieu@gmail.com> Co-authored-by: Sky <sky@sky9.dev> Co-authored-by: Huang Qi <huangqi3@xiaomi.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Jethro Beekman <jethro@fortanix.com> Co-authored-by: 0x79de <0x79de@gmail.com> Co-authored-by: binarycat <binarycat@envs.net> Co-authored-by: Glyn Normington <glyn.normington@gmail.com> Co-authored-by: Tamir Duberstein <tamird@gmail.com> Co-authored-by: Josh Triplett <josh@joshtriplett.org> Co-authored-by: Bastian Kersting <bastian@cmbt.de> Co-authored-by: Lyndon Brown <jnqnfe@gmail.com> Co-authored-by: Kent Ross <k@mad.cash> Co-authored-by: Noa <coolreader18@gmail.com> Co-authored-by: Lieselotte <52315535+she3py@users.noreply.github.com> Co-authored-by: Patrick Mooney <pmooney@pfmooney.com> Co-authored-by: Onè <43485962+c-git@users.noreply.github.com> Co-authored-by: 王宇逸 <Strawberry_Str@hotmail.com> Co-authored-by: gitbot <git@bot>
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…#342) This is an automated PR to merge library subtree updates from 2025-04-23 (rust-lang/rust@6bc57c6) to 2025-04-24 (rust-lang/rust@df35ff6) (inclusive) into main. `git merge` resulted in conflicts, which require manual resolution. Files were commited with merge conflict markers. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 563e49d --------- Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn> Signed-off-by: Petros Angelatos <petrosagg@gmail.com> Signed-off-by: Huang Qi <huangqi3@xiaomi.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Signed-off-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: Mara Bos <m-ou.se@m-ou.se> Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com> Co-authored-by: okaneco <47607823+okaneco@users.noreply.github.com> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn> Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr> Co-authored-by: clubby789 <jamie@hill-daniel.co.uk> Co-authored-by: Takayuki Maeda <takoyaki0316@gmail.com> Co-authored-by: Daniel Bloom <daniel@wormholelabs.xyz> Co-authored-by: Trevor Gross <tmgross@umich.edu> Co-authored-by: Jake Wharton <jw@squareup.com> Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Kornel <kornel@geekhood.net> Co-authored-by: Chris Denton <chris@chrisdenton.dev> Co-authored-by: Calder Coalson <caldercoalson@gmail.com> Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com> Co-authored-by: izarma <phuckuhh@gmail.com> Co-authored-by: Bennet Bleßmann <bb-github@t-online.de> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Jonathan Gruner <jogru0@gmail.com> Co-authored-by: Stan Manilov <stanislav.manilov@gmail.com> Co-authored-by: Gabriel Bjørnager Jensen <gabriel@achernar.io> Co-authored-by: lincot <lincot@disroot.org> Co-authored-by: timesince <seekseat@icloud.com> Co-authored-by: Boxy <rust@boxyuwu.dev> Co-authored-by: oyvindln <oyvindln@users.noreply.github.com> Co-authored-by: Berrysoft <Strawberry_Str@hotmail.com> Co-authored-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: Folkert de Vries <folkert@folkertdev.nl> Co-authored-by: Bastian Kersting <bkersting@google.com> Co-authored-by: Petros Angelatos <petrosagg@gmail.com> Co-authored-by: Jesus Checa Hidalgo <jchecahi@redhat.com> Co-authored-by: Michael Howell <michael@notriddle.com> Co-authored-by: Ricardo Fernández Serrata <76864299+Rudxain@users.noreply.github.com> Co-authored-by: GenYuLi <witherslin@synology.com> Co-authored-by: Chris Denton <christophersdenton@gmail.com> Co-authored-by: Amanieu d'Antras <amanieu@gmail.com> Co-authored-by: Sky <sky@sky9.dev> Co-authored-by: Huang Qi <huangqi3@xiaomi.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Jethro Beekman <jethro@fortanix.com> Co-authored-by: 0x79de <0x79de@gmail.com> Co-authored-by: binarycat <binarycat@envs.net> Co-authored-by: Glyn Normington <glyn.normington@gmail.com> Co-authored-by: Tamir Duberstein <tamird@gmail.com> Co-authored-by: Josh Triplett <josh@joshtriplett.org> Co-authored-by: Bastian Kersting <bastian@cmbt.de> Co-authored-by: Lyndon Brown <jnqnfe@gmail.com> Co-authored-by: Kent Ross <k@mad.cash> Co-authored-by: Noa <coolreader18@gmail.com> Co-authored-by: Lieselotte <52315535+she3py@users.noreply.github.com> Co-authored-by: Patrick Mooney <pmooney@pfmooney.com> Co-authored-by: Onè <43485962+c-git@users.noreply.github.com> Co-authored-by: gitbot <git@bot> Co-authored-by: Carolyn Zech <cmzech@amazon.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
Is PR add loop_invariants for `checked_pow`, `wrapping_pow`, `overflowing_pow` functions in `library/core/src/num/uint_macros.rs` and `library/core/src/num/int_macros.rs`. Side notes: - We need the feature that separate panic and other UBs to verify the function `strict_pow`, because this function calls `strict_mul`, which will panic when overflow happens. - The function `pow` can overflow and may require contracts, such as ``` #[kani::requires(self.checked_pow(exp).is_some())] #[kani::ensures(|x| *x == self.checked_pow(exp).unwrap())] ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
…odel-checking#328) Implement `kani::Arbitrary` for the `Wrapping`, `Saturating`, and `Simd` types. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <mt@debian.org>
Run https://github.com/carolynzech/autoharness_analyzer and push its results to the job summary. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Run a selected set of automatic harnesses where their previous, manual harnesses are being removed in this PR. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
…fast-proofs/` (model-checking#351) We are making a lot of changes to our `scripts/` and `.github/workflows/` folders to improve automation. These changes are low-risk; we have no plans to upstream them and they're not part of the public-facing challenge effort. Update our workflow to require two committee approvals iff `doc/`, `library/` or `verifast-proofs/` are modified, and otherwise just require one. See carolynzech#35 and carolynzech#36 for test runs on my fork. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
I was grepping for contract and this one didn't match because of the typo. Minor comment-only change. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
…checking#346) The result of a rotate operation is always non-zero, which could still be less than zero in case of signed types. Proofs were failing with the prior contract, but this still passed CI as we haven't yet picked up the Kani version where autoharness exits with a non-zero exit code in case of proof failure. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR adds loop_invariant and harness for array reverse. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
…king one (model-checking#502) Proposes a reward of 10k USD for several challenges and 20k for the larger ones among them. This PR restores what model-checking#459 originally proposed and had gotten approved, but was then lost during merge-conflict resolution. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
…del-checking#510) Clarify that `can_dereference` asserts a pointer has both read and write permissions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
Also: - Bumps VeriFast to 25.08 - Polishes the RawVec proof - Links to the VeriFast proofs from verifast-proofs/README.md Hopefully this can be merged before RustConf. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
…#504) This is an automated PR to merge library subtree updates from 2025-09-09 (rust-lang/rust@9c27f27) to 2025-10-09 (rust-lang/rust@b6f0945) (inclusive) into main. `git merge` resulted in conflicts, which require manual resolution. Files were commited with merge conflict markers. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 7e44c2b --------- Signed-off-by: Petros Angelatos <petrosagg@gmail.com> Signed-off-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: Christian Poveda <christian.poveda@ferrous-systems.com> Co-authored-by: bors <bors@rust-lang.org> Co-authored-by: Jana Dönszelmann <jonathan@donsz.nl> Co-authored-by: The Miri Cronjob Bot <miri@cron.bot> Co-authored-by: Jacob Pratt <jacob@jhpratt.dev> Co-authored-by: Ralf Jung <post@ralfj.de> Co-authored-by: Maybe Waffle <waffle.lapkin@gmail.com> Co-authored-by: Folkert de Vries <folkert@folkertdev.nl> Co-authored-by: Jo Bates <29763794+jbatez@users.noreply.github.com> Co-authored-by: Zalathar <Zalathar@users.noreply.github.com> Co-authored-by: Tsukasa OI <floss_rust@irq.a4lg.com> Co-authored-by: Laine Taffin Altman <alexanderaltman@me.com> Co-authored-by: Sidney Cammeresi <sac@cheesecake.org> Co-authored-by: Alan Somers <asomers@gmail.com> Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com> Co-authored-by: Folkert de Vries <flokkievids@gmail.com> Co-authored-by: tiif <pekyuan@gmail.com> Co-authored-by: Nathaniel McCallum <nathaniel@mccallum.life> Co-authored-by: Aapo Alasuutari <aapo.alasuutari@gmail.com> Co-authored-by: Sayantan Chakraborty <142906350+sayantn@users.noreply.github.com> Co-authored-by: Marijn Schouten <mhkbst@gmail.com> Co-authored-by: Joe Birr-Pixton <jpixton@gmail.com> Co-authored-by: Camille Gillot <gillot.camille@gmail.com> Co-authored-by: Alan Wu <XrXr@users.noreply.github.com> Co-authored-by: Alex Crichton <alex@alexcrichton.com> Co-authored-by: Yotam Ofek <yotam.ofek@gmail.com> Co-authored-by: joboet <jonasboettiger@icloud.com> Co-authored-by: Mads Marquart <mads@marquart.dk> Co-authored-by: Thalia Archibald <thalia@archibald.dev> Co-authored-by: tk <49250442+tkr-sh@users.noreply.github.com> Co-authored-by: Ben Kimock <kimockb@gmail.com> Co-authored-by: Jules Bertholet <julesbertholet@quoi.xyz> Co-authored-by: ltdk <usr@ltdk.xyz> Co-authored-by: Petros Angelatos <petrosagg@gmail.com> Co-authored-by: Taiki Endo <te316e89@gmail.com> Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com> Co-authored-by: Peter Lyons Kehl <peter.kehl@gmail.com> Co-authored-by: Ayush Singh <ayush@beagleboard.org> Co-authored-by: sysrex <769991+sysrex@users.noreply.github.com> Co-authored-by: BenjaminBrienen <Benjamin.Brienen@outlook.com> Co-authored-by: Iris Shi <0.0@owo.li> Co-authored-by: Tropical <42101043+Tropix126@users.noreply.github.com> Co-authored-by: Lewis McClelland <lewis@lewismcclelland.me> Co-authored-by: Stepan Koltsov <stepan.koltsov@gmail.com> Co-authored-by: Jeremy Smart <jeremy3141592@gmail.com> Co-authored-by: Adam Harvey <adam@adamharvey.name> Co-authored-by: DimitriiTrater <dima1603040@gmail.com> Co-authored-by: Tim 'Piepmatz' Hesse <git+github@cptpiepmatz.de> Co-authored-by: Vadim Petrochenkov <vadim.petrochenkov@gmail.com> Co-authored-by: Noratrieb <48135649+Noratrieb@users.noreply.github.com> Co-authored-by: Joshua Rayton <joshua.rayton@gmail.com> Co-authored-by: David Carlier <devnexen@gmail.com> Co-authored-by: Mark Rousskov <mark.simulacrum@gmail.com> Co-authored-by: Daniel Verkamp <daniel@drv.nu> Co-authored-by: Jeremy Soller <jackpot51@gmail.com> Co-authored-by: León Orell Valerian Liehr <me@fmease.dev> Co-authored-by: David Tolnay <dtolnay@gmail.com> Co-authored-by: Sebastian Speitel <sebastian.speitel@fem.tu-ilmenau.de> Co-authored-by: cyrgani <ansgar.w.zielke@gmail.com> Co-authored-by: Josh Simmons <josh@nega.tv> Co-authored-by: ivmarkov <ivan.markov@gmail.com> Co-authored-by: Cameron Steffen <cam.steffen94@gmail.com> Co-authored-by: edwloef <edwin.frank.loeffler@gmail.com> Co-authored-by: Fletcher Porter <me@fletcherporter.com> Co-authored-by: EFanZh <efanzh@gmail.com> Co-authored-by: Ada Alakbarova <ada.alakbarova@proton.me> Co-authored-by: Alice Ryhl <aliceryhl@google.com> Co-authored-by: gitbot <git@bot> Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Bart Jacobs <bart.jacobs@cs.kuleuven.be> Co-authored-by: Nico Lehmann <nico.lehmannm@gmail.com> Co-authored-by: Ranjit Jhala <rjhala@ucsd.edu>
- Fixes a bug in the Subtree Update action where a failed patch of the VeriFast proofs would cause an obscurely named, unhelpful commit to be added to the PR. - patch-verifast-proofs.sh now uses `git merge-file` instead of `patch` and can be called from anywhere - patch-verifast-proofs.sh now checks the updated proofs and rolls back the changes if the proof fails - Move the VeriFast invocation for checking a particular proof into a `verify.sh` script in that proof's directory. Makes the proof easier to audit. - Each VeriFast proof can now use a different version of VeriFast By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This PR proposes a new challenge (to verify the flt2dec module). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
This PR proposes a new challenge (verifying the boxed module). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
…model-checking#552) > Please add a description of your PR. > If this is a solution to an open challenge, please explain your solution. > > Don't forget to check our book to ensure your solution satisfy the overall > requirements as well as the challenge success criteria. > This PR uses minimal GitHub Token permissions for writing to a branch and creating a PR instead of relying on overly permissive defaults. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
Synchronise the challenge rewards mentioned in README.md with the ones in the book. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
Add `.github/copilot-instructions.md` to guide GitHub Copilot's automated code reviews for this repository. This will help us triage the coming wave of challenge solutions. The instructions cover review guidelines for the four types of PRs we receive: - **Challenge solutions** — formal verification rigor (no vacuous proofs, justified assumptions, contracts matching safety docs), Rust std library code quality standards, and success criteria compliance. - **New challenge proposals** — template and tracking issue requirements. - **New tool applications** — CI workflow and book entry requirements. - **Maintenance** — ensuring existing proofs are not weakened. Also includes a list of common red flags to watch for (e.g., over-constrained assumptions, missing cfg gates, unapproved tools). Reference: [Copilot code review custom instructions](https://docs.github.com/en/copilot/how-tos/configure-custom-instructions/add-repository-instructions). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <118344674+github-merge-queue@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
14 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Rebasing with upstream main