Add Challenge 19: Safety of RawVec#314
Merged
tautschnig merged 5 commits intomodel-checking:mainfrom May 21, 2025
Merged
Conversation
tautschnig
approved these changes
Apr 4, 2025
qinheping
approved these changes
Apr 17, 2025
rahulku
approved these changes
May 20, 2025
tautschnig
approved these changes
May 21, 2025
dkcumming
added a commit
to runtimeverification/verify-rust-std
that referenced
this pull request
Apr 10, 2026
* Subtree update automation: do not use `git subtree merge --squash` (#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.
* Merge subtree update for toolchain nightly-2025-03-18 (#309)
This is an automated PR to merge library subtree updates from 2025-03-17
(rust-lang/rust@227690a258492c84ae9927d18289208d0180e62f) to 2025-03-18
(rust-lang/rust@43a2e9d2c72db101f5fedac8b3acb78981b06bf2), 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: 8902bd397a755de86dff7de58c37a5366e402b00
---------
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>
* Update Kani Metrics (#305)
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 Challenges 17 18 for slices (#265)
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>
* Add Challenge 16: Iterator (#260)
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>
* Merge subtree update for toolchain nightly-2025-04-01 (#312)
This is an automated PR to merge library subtree updates from 2025-03-18
(rust-lang/rust@43a2e9d2c72db101f5fedac8b3acb78981b06bf2) to 2025-04-01
(rust-lang/rust@0b45675cfcec57f30a3794e1a1e18423aa9cf200) (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: c60865a9e2c90a1850f8343960fb23d1aac894a0
---------
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>
* Update Kani Metrics (#316)
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>
* Sync the VeriFast proofs and provide guidance on same (#313)
Updates the VeriFast proofs after `linked_list.rs` was modified by
https://github.com/rust-lang/rust/commit/c39f33baae94665d69a45d45a00d0dc028c80cc9
.
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.
* Merge subtree update for toolchain nightly-2025-04-04 (#318)
This is an automated PR to merge library subtree updates from 2025-04-01
(rust-lang/rust@0b45675cfcec57f30a3794e1a1e18423aa9cf200) to 2025-04-04
(rust-lang/rust@00095b3da4f23d9b3e7a809ac6a4e2b2530df84c), 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: 0cce469840a731f39efceef764628640e13152b2
---------
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>
* Merge subtree update for toolchain nightly-2025-04-06 (#320)
This is an automated PR to merge library subtree updates from 2025-04-04
(rust-lang/rust@00095b3da4f23d9b3e7a809ac6a4e2b2530df84c) to 2025-04-06
(rust-lang/rust@5e17a2a91dd7dbefd8b4a1087c2e42257457deeb) (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: a5c66929ceae8c225c1913e67509394276d3ee9e
---------
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>
* Update Kani Metrics (#322)
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>
* Remove unused subtree update helper scripts (#325)
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.
* Subtree update automation: create merge PR even when subtree/library is up-to-date (#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.
* Add script to text-extract all contracts (#323)
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.
* Merge subtree update for toolchain nightly-2025-04-07 (#329)
This is an automated PR to merge library subtree updates from 2025-04-06
(rust-lang/rust@5e17a2a91dd7dbefd8b4a1087c2e42257457deeb) to 2025-04-07
(rust-lang/rust@2fa8b11f0933dae9b4e5d287cc10c989218e8b36), 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: 0b8a1cde759561d2d1ef225d9dcbecfe41f1688d
---------
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>
* Update Kani Metrics (#333)
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>
* Merge subtree update for toolchain nightly-2025-04-21 (#336)
This is an automated PR to merge library subtree updates from 2025-04-07
(rust-lang/rust@2fa8b11f0933dae9b4e5d287cc10c989218e8b36) to 2025-04-21
(rust-lang/rust@b8c54d6358926028ac2fab1ec2b8665c70edb1c0) (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: 2ab28f38e1a6040c3e12ab4bf72cb5b5fb3b03c1
---------
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>
* Merge subtree update for toolchain nightly-2025-04-23 (#340)
This is an automated PR to merge library subtree updates from 2025-04-21
(rust-lang/rust@b8c54d6358926028ac2fab1ec2b8665c70edb1c0) to 2025-04-23
(rust-lang/rust@6bc57c6bf7d0024ad9ea5a2c112f3fc9c383c8a4), 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: 54a7b4f89b6e3b11734cde061e239c35ec6cf2e3
---------
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>
* Fix Challenge 18 rendering in book (#337)
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
* Merge subtree update for toolchain nightly-2025-04-24 (#342)
This is an automated PR to merge library subtree updates from 2025-04-23
(rust-lang/rust@6bc57c6bf7d0024ad9ea5a2c112f3fc9c383c8a4) to 2025-04-24
(rust-lang/rust@df35ff6c354f1f1fbf430b84e7dea37dfe997f34) (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: 563e49d1793208e58831ccc0eb1b3d684b296943
---------
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>
* Update Kani Metrics (#343)
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 loop_invariants for some Int power functions (#327)
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>
* Implement kani::Arbitrary for Wrapping, Saturating, and Simd types (#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>
* Add autoharness-analyzer CI job (#344)
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.
* Add autoharness to run-kani script and use in CI (#334)
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.
* Update Kani Metrics (#349)
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>
* Only require two approvals for changes to `doc/`, `library/` or `verifast-proofs/` (#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 https://github.com/carolynzech/rust/pull/35 and
https://github.com/carolynzech/rust/pull/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.
* Fix typo in comment ('contact' -> 'contract') (#352)
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.
* Update Kani Metrics (#355)
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>
* Fix num::nonzero::NonZero::<*>::rotate_{left,right} contracts (#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.
* Update Kani Metrics (#359)
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>
* Merge subtree update for toolchain nightly-2025-05-06 (#354)
This is an automated PR to merge library subtree updates from 2025-04-24
(rust-lang/rust@df35ff6c354f1f1fbf430b84e7dea37dfe997f34) to 2025-05-06
(rust-lang/rust@2e6882ac5be27a73293d6f7ae56397fdf32848de) (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: 794e27443f2bd557da13a2f7b1289b42bffaec6f
---------
Signed-off-by: Huang Qi <huangqi3@xiaomi.com>
Signed-off-by: Ayush Singh <ayush@beagleboard.org>
Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn>
Signed-off-by: Alice Ryhl <aliceryhl@google.com>
Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com>
Signed-off-by: Sean Cross <sean@xobs.io>
Co-authored-by: Chris Denton <christophersdenton@gmail.com>
Co-authored-by: Huang Qi <huangqi3@xiaomi.com>
Co-authored-by: bors <bors@rust-lang.org>
Co-authored-by: Ayush Singh <ayush@beagleboard.org>
Co-authored-by: Thalia Archibald <thalia@archibald.dev>
Co-authored-by: Jacob Pratt <jacob@jhpratt.dev>
Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn>
Co-authored-by: Diego Ongaro <ongardie@gmail.com>
Co-authored-by: Jethro Beekman <jethro@fortanix.com>
Co-authored-by: Ralf Jung <post@ralfj.de>
Co-authored-by: Janggun Lee <leesisi123@naver.com>
Co-authored-by: 0x79de <0x79de@gmail.com>
Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com>
Co-authored-by: binarycat <binarycat@envs.net>
Co-authored-by: Glyn Normington <glyn.normington@gmail.com>
Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com>
Co-authored-by: Tamir Duberstein <tamird@gmail.com>
Co-authored-by: Alice Ryhl <aliceryhl@google.com>
Co-authored-by: Mara Bos <m-ou.se@m-ou.se>
Co-authored-by: Josh Triplett <josh@joshtriplett.org>
Co-authored-by: Bastian Kersting <bastian@cmbt.de>
Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com>
Co-authored-by: Lyndon Brown <jnqnfe@gmail.com>
Co-authored-by: Kent Ross <k@mad.cash>
Co-authored-by: Amanieu d'Antras <amanieu@gmail.com>
Co-authored-by: Noa <coolreader18@gmail.com>
Co-authored-by: Ed Page <eopage@gmail.com>
Co-authored-by: Trevor Gross <tmgross@umich.edu>
Co-authored-by: The Miri Cronjob Bot <miri@cron.bot>
Co-authored-by: Lieselotte <52315535+she3py@users.noreply.github.com>
Co-authored-by: Patrick Mooney <pmooney@pfmooney.com>
Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com>
Co-authored-by: Jonathan Gruner <jogru0@gmail.com>
Co-authored-by: Chris Denton <chris@chrisdenton.dev>
Co-authored-by: Onè <43485962+c-git@users.noreply.github.com>
Co-authored-by: Folkert de Vries <folkert@folkertdev.nl>
Co-authored-by: Urgau <urgau@numericable.fr>
Co-authored-by: 王宇逸 <Strawberry_Str@hotmail.com>
Co-authored-by: Jonas Böttiger <jonasboettiger@icloud.com>
Co-authored-by: Hegui Dai <natural_selection_@outlook.com>
Co-authored-by: Gabriel Bjørnager Jensen <gabriel@achernar.io>
Co-authored-by: Artur Roos <artur.roos@ktnlvr.dev>
Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com>
Co-authored-by: Nicholas Nethercote <n.nethercote@gmail.com>
Co-authored-by: bendn <bend.n@outlook.com>
Co-authored-by: ismailarilik <arilik.ismail@gmail.com>
Co-authored-by: Tobias <206408826+t5kd@users.noreply.github.com>
Co-authored-by: Ethan Wu <ethanwu10@gmail.com>
Co-authored-by: Jake Goulding <jake.goulding@gmail.com>
Co-authored-by: Michael Howell <michael@notriddle.com>
Co-authored-by: Christopher Durham <cad97@cad97.com>
Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>
Co-authored-by: LemonJ <1632798336@qq.com>
Co-authored-by: SabrinaJewson <sejewson@gmail.com>
Co-authored-by: Andrew Zhogin <andrew.zhogin@gmail.com>
Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com>
Co-authored-by: Sean Cross <sean@xobs.io>
Co-authored-by: Trevor Gross <t.gross35@gmail.com>
Co-authored-by: Zachary S <zasample18+github@gmail.com>
Co-authored-by: sayantn <sayantn05@gmail.com>
Co-authored-by: Eyal Kalderon <ebkalderon@gmail.com>
Co-authored-by: Lynnesbian <lynne@bune.city>
Co-authored-by: Christopher Berner <me@cberner.com>
Co-authored-by: gitbot <git@bot>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
* Parse log file of multi-threaded Kani run (terse output) into JSON (#324)
Given a run of Kani on the standard library with `--jobs=<N>
--output-format=terse` (and, typically, `autoharness`) enabled this
produces a machine-processable JSON result via
```
python3 log_parser.py \
--kani-list-file kani-list.json \
--analysis-results-dir std_lib_analysis/results/ \
verification.log -o results.json
```
where each entry in the resulting JSON array is of the form
```
{
"thread_id": int,
"result": {
"harness": string,
"is_autoharness": bool,
"autoharness_result": string,
"with_contract": bool,
"crate": string,
"function": string,
"function_safeness": string,
"file_name": string,
"n_failed_properties": int,
"n_total_properties": int,
"result": string,
"time": string,
"output": array
}
}
```
With the help of `jq` one can then conveniently compute various metrics,
e.g.,
```
jq 'map(select(.result.result == "SUCCESSFUL" and
.result.is_autoharness == true and
.result.crate == "core" and
.result.function_safeness == "unsafe" and
.result.with_contract == true)) | length' results.json
```
to find the number of successfully-verified contracts of unsafe
functions in crate `core` that were verified using automatically
generated harnesses.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
* Add Challenges 20 21 22 for str Pattern and iter (#266)
This PR adds:
- Challenge 20 21: for functions in str::pattern.rs
- Challenge 22: for functions in str::iter.rs
Resolves #ISSUE-NUMBER
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>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
* Add Challenge 25: VecDeque (#269)
This PR adds Challenge 25 for VecDeque
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>
* Add Challenge 19: Safety of RawVec (#314)
This PR adds Challenge 19: Safety of RawVec
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: Michael Tautschnig <mt@debian.org>
* Add safety preconditions to std/src/alloc.rs (#330)
These contracts formalize the safety requirements that were previously
only documented in comments.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
* Challenge 7: make panicking part optional; remove mention of verifying intrinsics (#357)
Update the atomic intrinsics challenge to make verifying the intrinsics
out of scope, since that would require verifying compiler
implementations that are out of scope for this effort. Also make the
part about verifying the absence of panics optional to restrict the
requirements to safety only.
I also added a `mdbook-linkcheck` dependency because I discovered I
needed that to build the book locally.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
* Merge subtree update for toolchain nightly-2025-05-20 (#361)
This is an automated PR to merge library subtree updates from 2025-05-06
(rust-lang/rust@2e6882ac5be27a73293d6f7ae56397fdf32848de) to 2025-05-20
(rust-lang/rust@60dabef95a3de3ec974dcb50926e4bfe743f078f) (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: cc38593415f4067ec72919ba180614e5f3209663
---------
Signed-off-by: Jiahao XU <Jiahao_XU@outlook.com>
Signed-off-by: Ayush Singh <ayush@beagleboard.org>
Signed-off-by: Sean Cross <sean@xobs.io>
Signed-off-by: Vladimir Krivopalov <vladimir.krivopalov@gmail.com>
Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn>
Co-authored-by: Thalia Archibald <thalia@archibald.dev>
Co-authored-by: Chris Denton <chris@chrisdenton.dev>
Co-authored-by: The Miri Cronjob Bot <miri@cron.bot>
Co-authored-by: Gabriel Bjørnager Jensen <gabriel@achernar.io>
Co-authored-by: Artur Roos <artur.roos@ktnlvr.dev>
Co-authored-by: Ralf Jung <post@ralfj.de>
Co-authored-by: Jiahao XU <Jiahao_XU@outlook.com>
Co-authored-by: bors <bors@rust-lang.org>
Co-authored-by: 王宇逸 <Strawberry_Str@hotmail.com>
Co-authored-by: Nicholas Nethercote <n.nethercote@gmail.com>
Co-authored-by: Hegui Dai <natural_selection_@outlook.com>
Co-authored-by: Urgau <urgau@numericable.fr>
Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com>
Co-authored-by: bendn <bend.n@outlook.com>
Co-authored-by: Trevor Gross <tmgross@umich.edu>
Co-authored-by: ismailarilik <arilik.ismail@gmail.com>
Co-authored-by: Tobias <206408826+t5kd@users.noreply.github.com>
Co-authored-by: Ethan Wu <ethanwu10@gmail.com>
Co-authored-by: Ayush Singh <ayush@beagleboard.org>
Co-authored-by: Jake Goulding <jake.goulding@gmail.com>
Co-authored-by: Michael Howell <michael@notriddle.com>
Co-authored-by: Christopher Durham <cad97@cad97.com>
Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>
Co-authored-by: LemonJ <1632798336@qq.com>
Co-authored-by: SabrinaJewson <sejewson@gmail.com>
Co-authored-by: joboet <jonasboettiger@icloud.com>
Co-authored-by: Andrew Zhogin <andrew.zhogin@gmail.com>
Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com>
Co-authored-by: Lieselotte <52315535+she3py@users.noreply.github.com>
Co-authored-by: Sean Cross <sean@xobs.io>
Co-authored-by: Trevor Gross <t.gross35@gmail.com>
Co-authored-by: Jon Bauman <baumanj@users.noreply.github.com>
Co-authored-by: binarycat <binarycat@envs.net>
Co-authored-by: Mara Bos <m-ou.se@m-ou.se>
Co-authored-by: Mathis B <mathis.bottinelli@student-cs.fr>
Co-authored-by: Zachary S <zasample18+github@gmail.com>
Co-authored-by: Amanieu d'Antras <amanieu@gmail.com>
Co-authored-by: sayantn <sayantn05@gmail.com>
Co-authored-by: Eyal Kalderon <ebkalderon@gmail.com>
Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com>
Co-authored-by: Lynnesbian <lynne@bune.city>
Co-authored-by: Christopher Berner <me@cberner.com>
Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com>
Co-authored-by: Paolo Barbolini <paolo.barbolini@m4ss.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: The 8472 <git@infinite-source.de>
Co-authored-by: Nick Kocharhook <nick@kocharhook.com>
Co-authored-by: Vladimir Krivopalov <vladimir@krivopalov.ru>
Co-authored-by: Vilim Lendvaj <vilim.lendvaj@sk.t-com.hr>
Co-authored-by: David Tolnay <dtolnay@gmail.com>
Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com>
Co-authored-by: Jacob Pratt <jacob@jhpratt.dev>
Co-authored-by: ivmarkov <ivan.markov@gmail.com>
Co-authored-by: Martin Kröning <martin.kroening@eonerc.rwth-aachen.de>
Co-authored-by: Daniel Paoliello <danpao@microsoft.com>
Co-authored-by: Luca Versari <veluca93@gmail.com>
Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn>
Co-authored-by: Ben Kimock <kimockb@gmail.com>
Co-authored-by: Dietrich Daroch <Dietrich@Daroch.me>
Co-authored-by: León Orell Valerian Liehr <me@fmease.dev>
Co-authored-by: Pietro Albini <pietro@pietroalbini.org>
Co-authored-by: Julian Knodt <julianknodt@gmail.com>
Co-authored-by: Michael Goulet <michael@errs.io>
Co-authored-by: Michał Łowicki <michal.lowicki@datadoghq.com>
Co-authored-by: Samuel Tardieu <sam@rfc1149.net>
Co-authored-by: B I Mohammed Abbas <bimohammadabbas@gmail.com>
Co-authored-by: Federico Terzi <federicoterzi96@gmail.com>
Co-authored-by: sam skeoch <djscythe@noreply.codeberg.org>
Co-authored-by: est31 <MTest31@outlook.com>
Co-authored-by: Speedy_Lex <alex.ciocildau@gmail.com>
Co-authored-by: Mario Pastorelli <pastorelli.mario@gmail.com>
Co-authored-by: gitbot <git@bot>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
* Move autoharness_analyzer to `scripts/` (#350)
Move `autoharness_analyzer` to this repository so it can be
community-owned and maintained.
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>
* Add preconditions for disjoint_bitor (#347)
Uses the verbatim SAFETY comment as precondition to avoid spurious proof
failures.
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>
* Update Kani Metrics (#365)
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>
* Merge subtree update for toolchain nightly-2025-05-22 (#364)
This is an automated PR to merge library subtree updates from 2025-05-20
(rust-lang/rust@60dabef95a3de3ec974dcb50926e4bfe743f078f) to 2025-05-22
(rust-lang/rust@bf64d66bd58719fac2585eae5e546e5e1d9947f5) (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: 02d93290db5d37dc78ac1646dcf838f46304c4e4
---------
Signed-off-by: Ayush Singh <ayush@beagleboard.org>
Signed-off-by: Sean Cross <sean@xobs.io>
Signed-off-by: Vladimir Krivopalov <vladimir.krivopalov@gmail.com>
Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn>
Co-authored-by: Hegui Dai <natural_selection_@outlook.com>
Co-authored-by: Urgau <urgau@numericable.fr>
Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com>
Co-authored-by: bendn <bend.n@outlook.com>
Co-authored-by: Ralf Jung <post@ralfj.de>
Co-authored-by: bors <bors@rust-lang.org>
Co-authored-by: Trevor Gross <tmgross@umich.edu>
Co-authored-by: The Miri Cronjob Bot <miri@cron.bot>
Co-authored-by: ismailarilik <arilik.ismail@gmail.com>
Co-authored-by: Tobias <206408826+t5kd@users.noreply.github.com>
Co-authored-by: Ethan Wu <ethanwu10@gmail.com>
Co-authored-by: Ayush Singh <ayush@beagleboard.org>
Co-authored-by: Jake Goulding <jake.goulding@gmail.com>
Co-authored-by: Michael Howell <michael@notriddle.com>
Co-authored-by: Christopher Durham <cad97@cad97.com>
Co-authored-by: Pavel Grigorenko <GrigorenkoPV@ya.ru>
Co-authored-by: LemonJ <1632798336@qq.com>
Co-authored-by: SabrinaJewson <sejewson@gmail.com>
Co-authored-by: Nicholas Nethercote <n.nethercote@gmail.com>
Co-authored-by: Chris Denton <chris@chrisdenton.dev>
Co-authored-by: joboet <jonasboettiger@icloud.com>
Co-authored-by: Andrew Zhogin <andrew.zhogin@gmail.com>
Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com>
Co-authored-by: Lieselotte <52315535+she3py@users.noreply.github.com>
Co-authored-by: Sean Cross <sean@xobs.io>
Co-authored-by: Trevor Gross <t.gross35@gmail.com>
Co-authored-by: Jon Bauman <baumanj@users.noreply.github.com>
Co-authored-by: binarycat <binarycat@envs.net>
Co-authored-by: Mara Bos <m-ou.se@m-ou.se>
Co-authored-by: Mathis B <mathis.bottinelli@student-cs.fr>
Co-authored-by: Zachary S <zasample18+github@gmail.com>
Co-authored-by: Thalia Archibald <thalia@archibald.dev>
Co-authored-by: Amanieu d'Antras <amanieu@gmail.com>
Co-authored-by: sayantn <sayantn05@gmail.com>
Co-authored-by: Artur Roos <artur.roos@ktnlvr.dev>
Co-authored-by: Eyal Kalderon <ebkalderon@gmail.com>
Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com>
Co-authored-by: Lynnesbian <lynne@bune.city>
Co-authored-by: Christopher Berner <me@cberner.com>
Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com>
Co-authored-by: Paolo Barbolini <paolo.barbolini@m4ss.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: The 8472 <git@infinite-source.de>
Co-authored-by: Nick Kocharhook <nick@kocharhook.com>
Co-authored-by: Vladimir Krivopalov <vladimir@krivopalov.ru>
Co-authored-by: Vilim Lendvaj <vilim.lendvaj@sk.t-com.hr>
Co-authored-by: David Tolnay <dtolnay@gmail.com>
Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com>
Co-authored-by: Jacob Pratt <jacob@jhpratt.dev>
Co-authored-by: 王宇逸 <Strawberry_Str@hotmail.com>
Co-authored-by: ivmarkov <ivan.markov@gmail.com>
Co-authored-by: Martin Kröning <martin.kroening@eonerc.rwth-aachen.de>
Co-authored-by: Daniel Paoliello <danpao@microsoft.com>
Co-authored-by: Luca Versari <veluca93@gmail.com>
Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn>
Co-authored-by: Ben Kimock <kimockb@gmail.com>
Co-authored-by: Dietrich Daroch <Dietrich@Daroch.me>
Co-authored-by: León Orell Valerian Liehr <me@fmease.dev>
Co-authored-by: Pietro Albini <pietro@pietroalbini.org>
Co-authored-by: Julian Knodt <julianknodt@gmail.com>
Co-authored-by: Michael Goulet <michael@errs.io>
Co-authored-by: Michał Łowicki <michal.lowicki@datadoghq.com>
Co-authored-by: Samuel Tardieu <sam@rfc1149.net>
Co-authored-by: B I Mohammed Abbas <bimohammadabbas@gmail.com>
Co-authored-by: Federico Terzi <federicoterzi96@gmail.com>
Co-authored-by: sam skeoch <djscythe@noreply.codeberg.org>
Co-authored-by: est31 <MTest31@outlook.com>
Co-authored-by: Fluid <90795031+fluiderson@users.noreply.github.com>
Co-authored-by: Speedy_Lex <alex.ciocildau@gmail.com>
Co-authored-by: Mario Pastorelli <pastorelli.mario@gmail.com>
Co-authored-by: Daniel McNab <36049421+DJMcNab@users.noreply.github.com>
Co-authored-by: Josh Triplett <josh@joshtriplett.org>
Co-authored-by: gitbot <git@bot>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
* additional transmute and transmute_unchecked harnesses (#264)
Toward solving #19
This pr adds some additional harnesses for transmute_unchecked and
transmute.
With this, we suspect that the main harnesses for part 1 of challenge 1
(verifying the transmute intrinsics directly) are there (besides adding
more of the same kinds of harnesses, like the 2-way harnesses for more
types). We go into more detail about what needs to be done for part 1,
as well as what has been done and what can't be done here:
https://docs.google.com/document/d/1zFGANNMx8mZ8fucKrN--ELwKASUPeP20THH6M_fQ7jg/edit?usp=sharing
Just one note: transmute has far fewer harnesses than
transmute_unchecked here -- this is because it is not currently possible
to write a wrapper for transmute, and it is thus not possible to write a
function contract. A lot of the harnesses for transmute_unchecked test
the function contract's validity clause, rather than the function
itself, explaining this disparity.
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: AlexLB99 <marcgolvanian@gmail.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
* Use uname -m instead of uname -p (#372)
On my Debian machine, uname -p returns "unknown" and the manpage says -p
is non-portable. I do get x86_64 on from uname -m and that doesn't have
the non-portable disclaimer on it.
> 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.
>
Resolves #ISSUE-NUMBER
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
* Add missing `proof_for_contract` to `mut_ptr::offset_from` harness (#358)
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>
* Derive `Arbitrary` for various `core_arch::x86` types (#348)
This enables autoharness to generate an additional 4067 harnesses (and
successfully prove 363 of them).
Using a patch instead of directly modifying the source code here for
`library/stdarch` is a git submodule. Modifying the source code directly
would require forking that other repository, tweaking our submodule
pointer, and thereby causing additional challenges for our fork update
automation.
The long-term solution should be automated derive-arbitrary support in
autoharness.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
* Merge subtree update for toolchain nightly-2025-05-28 (#370)
This is an automated PR to merge library subtree updates from 2025-05-22
(rust-lang/rust@bf64d66bd58719fac2585eae5e546e5e1d9947f5) to 2025-05-28
(rust-lang/rust@45f256d9d7cffb66185c0bf1b8a864cba79db90c) (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: 725b0dbbc7fc0e2d1757d91366d7c181cc6a64ac
---------
Signed-off-by: Sean Cross <sean@xobs.io>
Signed-off-by: Vladimir Krivopalov <vladimir.krivopalov@gmail.com>
Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn>
Signed-off-by: Paul Mabileau <paul.mabileau@harfanglab.fr>
Signed-off-by: Ayush Singh <ayush@beagleboard.org>
Co-authored-by: Chris Denton <chris@chrisdenton.dev>
Co-authored-by: bors <bors@rust-lang.org>
Co-authored-by: joboet <jonasboettiger@icloud.com>
Co-authored-by: Andrew Zhogin <andrew.zhogin@gmail.com>
Co-authored-by: DaniPopes <57450786+DaniPopes@users.noreply.github.com>
Co-authored-by: Lieselotte <52315535+she3py@users.noreply.github.com>
Co-authored-by: Sean Cross <sean@xobs.io>
Co-authored-by: The Miri Cronjob Bot <miri@cron.bot>
Co-authored-by: Ralf Jung <post@ralfj.de>
Co-authored-by: Trevor Gross <t.gross35@gmail.com>
Co-authored-by: Jon Bauman <baumanj@users.noreply.github.com>
Co-authored-by: binarycat <binarycat@envs.net>
Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com>
Co-authored-by: Mara Bos <m-ou.se@m-ou.se>
Co-authored-by: Mathis B <mathis.bottinelli@student-cs.fr>
Co-authored-by: Natrix <osken_o.s@hotmail.com>
Co-authored-by: Zachary S <zasample18+github@gmail.com>
Co-authored-by: Thalia Archibald <thalia@archibald.dev>
Co-authored-by: Amanieu d'Antras <amanieu@gmail.com>
Co-authored-by: sayantn <sayantn05@gmail.com>
Co-authored-by: Artur Roos <artur.roos@ktnlvr.dev>
Co-authored-by: Eyal Kalderon <ebkalderon@gmail.com>
Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com>
Co-authored-by: Lynnesbian <lynne@bune.city>
Co-authored-by: Christopher Berner <me@cberner.com>
Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com>
Co-authored-by: Paolo Barbolini <paolo.barbolini@m4ss.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: The 8472 <git@infinite-source.de>
Co-authored-by: Nick Kocharhook <nick@kocharhook.com>
Co-authored-by: Trevor Gross <tmgross@umich.edu>
Co-authored-by: Vladimir Krivopalov <vladimir@krivopalov.ru>
Co-authored-by: Vilim Lendvaj <vilim.lendvaj@sk.t-com.hr>
Co-authored-by: David Tolnay <dtolnay@gmail.com>
Co-authored-by: Marijn Schouten <hkBst@users.noreply.github.com>
Co-authored-by: Jacob Pratt <jacob@jhpratt.dev>
Co-authored-by: 王宇逸 <Strawberry_Str@hotmail.com>
Co-authored-by: ivmarkov <ivan.markov@gmail.com>
Co-authored-by: Martin Kröning <martin.kroening@eonerc.rwth-aachen.de>
Co-authored-by: Daniel Paoliello <danpao@microsoft.com>
Co-authored-by: Luca Versari <veluca93@…
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
4 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.
This PR adds Challenge 19: Safety of RawVec
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.