Merge subtree update for toolchain nightly-2025-06-03 (model-checking#380)

This is an automated PR to merge library subtree updates from 2025-06-02
(rust-lang/rust@99e7c15) to 2025-06-03
(rust-lang/rust@5d707b0), 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: 018adbd

---------

Signed-off-by: Paul Mabileau <paul.mabileau@harfanglab.fr>
Signed-off-by: xizheyin <xizheyin@smail.nju.edu.cn>
Signed-off-by: Ayush Singh <ayush@beagleboard.org>
Co-authored-by: Matthias Krüger <476013+matthiaskrgr@users.noreply.github.com>
Co-authored-by: Paolo Barbolini <paolo.barbolini@m4ss.net>
Co-authored-by: León Orell Valerian Liehr <me@fmease.dev>
Co-authored-by: Urgau <urgau@numericable.fr>
Co-authored-by: Pietro Albini <pietro@pietroalbini.org>
Co-authored-by: Simon Sapin <simon@apollographql.com>
Co-authored-by: Julian Knodt <julianknodt@gmail.com>
Co-authored-by: Michael Goulet <michael@errs.io>
Co-authored-by: Trevor Gross <tmgross@umich.edu>
Co-authored-by: Michał Łowicki <michal.lowicki@datadoghq.com>
Co-authored-by: Mathis Bottinelli <mathis.bottinelli@student-cs.fr>
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: teor <teor@riseup.net>
Co-authored-by: Eric Huss <eric@huss.org>
Co-authored-by: joboet <jonasboettiger@icloud.com>
Co-authored-by: bors <bors@rust-lang.org>
Co-authored-by: Ryan van Polen <ryan@radix-security.com>
Co-authored-by: sam skeoch <djscythe@noreply.codeberg.org>
Co-authored-by: Benoît du Garreau <benoit@dugarreau.fr>
Co-authored-by: est31 <MTest31@outlook.com>
Co-authored-by: GrantBirki <grant.birkinbine@gmail.com>
Co-authored-by: Paul Mabileau <paul.mabileau@harfanglab.fr>
Co-authored-by: Jack O'Connor <oconnor663@gmail.com>
Co-authored-by: mejrs <59372212+mejrs@users.noreply.github.com>
Co-authored-by: sayantn <sayantn05@gmail.com>
Co-authored-by: Fluid <90795031+fluiderson@users.noreply.github.com>
Co-authored-by: xizheyin <xizheyin@smail.nju.edu.cn>
Co-authored-by: Speedy_Lex <alex.ciocildau@gmail.com>
Co-authored-by: Stuart Cook <Zalathar@users.noreply.github.com>
Co-authored-by: Jeremy Smart <jeremy3141592@gmail.com>
Co-authored-by: Ralf Jung <post@ralfj.de>
Co-authored-by: Mario Pastorelli <pastorelli.mario@gmail.com>
Co-authored-by: Marcelo Domínguez <69964857+Sa4dUs@users.noreply.github.com>
Co-authored-by: Daniel McNab <36049421+DJMcNab@users.noreply.github.com>
Co-authored-by: Josh Triplett <josh@joshtriplett.org>
Co-authored-by: Christopher Berner <me@cberner.com>
Co-authored-by: Amanieu d'Antras <amanieu@gmail.com>
Co-authored-by: Jonas Platte <jplatte+git@posteo.de>
Co-authored-by: Marcelo Domínguez <dmmarcelo27@gmail.com>
Co-authored-by: Ben Kimock <kimockb@gmail.com>
Co-authored-by: Folkert de Vries <folkert@folkertdev.nl>
Co-authored-by: waffle <waffle.lapkin@gmail.com>
Co-authored-by: Dannyyy93 <dannymotydnd@gmail.com>
Co-authored-by: Ayush Singh <ayush@beagleboard.org>
Co-authored-by: Tamir Duberstein <tamird@gmail.com>
Co-authored-by: Guillaume Gomez <guillaume1.gomez@gmail.com>
Co-authored-by: Tshepang Mbambo <hopsi@tuta.io>
Co-authored-by: Jacob Pratt <jacob@jhpratt.dev>
Co-authored-by: Chris Denton <chris@chrisdenton.dev>
Co-authored-by: bendn <bend.n@outlook.com>
Co-authored-by: 许杰友 Jieyou Xu (Joe) <39484203+jieyouxu@users.noreply.github.com>
Co-authored-by: binarycat <binarycat@envs.net>
Co-authored-by: The Miri Cronjob Bot <miri@cron.bot>
Co-authored-by: Sidney Cammeresi <sac@readyset.io>
Co-authored-by: bjorn3 <17426603+bjorn3@users.noreply.github.com>
Co-authored-by: tk <49250442+tkr-sh@users.noreply.github.com>
Co-authored-by: Trevor Gross <t.gross35@gmail.com>
Co-authored-by: Jakub Beránek <berykubik@gmail.com>
Co-authored-by: Orson Peters <orsonpeters@gmail.com>
Co-authored-by: Patrick-6 <pamu99@gmx.ch>
Co-authored-by: WANG Rui <wangrui@loongson.cn>
Co-authored-by: Scott McMurray <scottmcm@users.noreply.github.com>
Co-authored-by: Jubilee <workingjubilee@gmail.com>
Co-authored-by: Ruan Comelli <ruancomelli@gmail.com>
Co-authored-by: zacryol <60046681+zacryol@users.noreply.github.com>
Co-authored-by: usamoi <usamoi@outlook.com>
Co-authored-by: gitbot <git@bot>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: thanhnguyen-aws <ntson@amazon.com>

Author: 70 people

library/core/src/marker.rs

@@ -200,7 +200,7 @@ pub trait Unsize<T: ?Sized> {
 ///
 /// Constants are only allowed as patterns if (a) their type implements
 /// `PartialEq`, and (b) interpreting the value of the constant as a pattern
-/// is equialent to calling `PartialEq`. This ensures that constants used as
+/// is equivalent to calling `PartialEq`. This ensures that constants used as
 /// patterns cannot expose implementation details in an unexpected way or
 /// cause semver hazards.
 ///

library/core/src/num/f128.rs

@@ -177,6 +177,7 @@ impl f128 {
     /// [Machine epsilon]: https://en.wikipedia.org/wiki/Machine_epsilon
     /// [`MANTISSA_DIGITS`]: f128::MANTISSA_DIGITS
     #[unstable(feature = "f128", issue = "116909")]
+    #[rustc_diagnostic_item = "f128_epsilon"]
     pub const EPSILON: f128 = 1.92592994438723585305597794258492732e-34_f128;
 
     /// Smallest finite `f128` value.

library/core/src/num/f16.rs

@@ -174,6 +174,7 @@ impl f16 {
     /// [Machine epsilon]: https://en.wikipedia.org/wiki/Machine_epsilon
     /// [`MANTISSA_DIGITS`]: f16::MANTISSA_DIGITS
     #[unstable(feature = "f16", issue = "116909")]
+    #[rustc_diagnostic_item = "f16_epsilon"]
     pub const EPSILON: f16 = 9.7656e-4_f16;
 
     /// Smallest finite `f16` value.

library/core/src/slice/ascii.rs

@@ -478,6 +478,7 @@ const fn is_ascii(bytes: &[u8]) -> bool {
 
     let mut i = 0;
 
+    #[safety::loop_invariant(i <= bytes.len())]
     while i + CHUNK_SIZE <= bytes.len() {
         let chunk_end = i + CHUNK_SIZE;
 
@@ -486,6 +487,7 @@ const fn is_ascii(bytes: &[u8]) -> bool {
         // ASCII bytes are less than 128 (0x80), so their most significant
         // bit is unset.
         let mut count = 0;
+        #[safety::loop_invariant(i <= chunk_end && chunk_end - i <= CHUNK_SIZE && i - (chunk_end - CHUNK_SIZE) >= count as usize)]
         while i < chunk_end {
             count += bytes[i].is_ascii() as u8;
             i += 1;
@@ -499,6 +501,7 @@ const fn is_ascii(bytes: &[u8]) -> bool {
 
     // Process the remaining `bytes.len() % N` bytes.
     let mut is_ascii = true;
+    #[safety::loop_invariant(i <= bytes.len())]
     while i < bytes.len() {
         is_ascii &= bytes[i].is_ascii();
         i += 1;
@@ -514,6 +517,10 @@ pub mod verify {
 
     #[kani::proof]
     #[kani::unwind(8)]
+    // FIXME: the loop invariant in the x_64 & sse2 version of is_ascii
+    // fails because Kani does not yet support modifies clauses for loop invariants.
+    // Once it does, remove this cfg.
+    #[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
     pub fn check_is_ascii() {
         if kani::any() {
             // TODO: ARR_SIZE can be much larger with cbmc argument

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # standard library we currently track.
 
 [toolchain]
-channel = "nightly-2025-06-02"
+channel = "nightly-2025-06-03"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

scripts/check_rustc.sh

@@ -112,12 +112,15 @@ else
     fi
 fi
 
+# TODO: this logic is broken because the stage 0 bootstrap sequence was redesigned, c.f. https://blog.rust-lang.org/inside-rust/2025/05/29/redesigning-the-initial-bootstrap-sequence/
+# However, changing the command to --stage 1 as suggested does not work; the compiler complains that there is an old version of the `safety` crate
+# compiled by the beta compiler. For now, comment it out and see if continued work on this feature (e.g. https://github.com/rust-lang/rust/pull/142002) fixes it.
 # Run tests
-cd "$TMP_RUST_DIR"
-echo "Running tests..."
-./x test --stage 0 library/std
+# cd "$TMP_RUST_DIR"
+# echo "Running tests..."
+# ./x test --stage 0 library/std
 
-echo "Tests completed."
+# echo "Tests completed."
 
 # Clean up the temporary directory
 rm -rf "$TMP_RUST_DIR"

tool_config/kani-version.toml

@@ -2,4 +2,4 @@
 # incompatible with the verify-std repo.
 
 [kani]
-commit = "ef6ad3b518676c3492ca5871ea61a441bb1d5b1e"
+commit = "931661b0cdbf9354eba3902608efadad00b1cbb3"