Upgrade Rust toolchain to 2025-07-29 (#4247)

Relevant upstream PRs:
- rust-lang/rust#144389 (MIR-build: No longer
emit assumes in enum-as casting)
- rust-lang/rust#144392 (rustc_public: Remove
movability from `RigidTy/AggregateKind::Coroutine`)
- rust-lang/rust#144377 (Rename impl_of_method
and trait_of_item)

Resolves: #4246

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

Author: tautschnig

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -734,7 +734,7 @@ impl GotocCtx<'_> {
                     }
                 }
             }
-            AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(operands, res_ty),
+            AggregateKind::Coroutine(_, _) => self.codegen_rvalue_coroutine(operands, res_ty),
             AggregateKind::CoroutineClosure(_, _) => {
                 let ty = self.codegen_ty_stable(res_ty);
                 self.codegen_unimplemented_expr(

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -183,7 +183,7 @@ impl MirVisitor for StubConstChecker<'_> {
                         [one] => one.as_type().unwrap(),
                         _ => unreachable!(),
                     };
-                    let trait_ = tcx.trait_of_item(mono_const.def).unwrap();
+                    let trait_ = tcx.trait_of_assoc(mono_const.def).unwrap();
                     let msg = format!(
                         "Type `{implementor}` does not implement trait `{}`. \
         This is likely because `{}` is used as a stub but its \

kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs

@@ -394,7 +394,7 @@ fn data_bytes_for_ty(
                 RigidTy::FnDef(_, _)
                 | RigidTy::FnPtr(_)
                 | RigidTy::Closure(_, _)
-                | RigidTy::Coroutine(_, _, _)
+                | RigidTy::Coroutine(_, _)
                 | RigidTy::CoroutineClosure(_, _)
                 | RigidTy::CoroutineWitness(_, _)
                 | RigidTy::Foreign(_)

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -687,7 +687,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
                 // Only aggregate value.
                 AggregateKind::Array(_)
                 | AggregateKind::Closure(_, _)
-                | AggregateKind::Coroutine(_, _, _)
+                | AggregateKind::Coroutine(_, _)
                 | AggregateKind::CoroutineClosure(_, _)
                 | AggregateKind::RawPtr(_, _)
                 | AggregateKind::Tuple => {}
@@ -1057,7 +1057,7 @@ pub fn ty_validity_per_offset(
                 RigidTy::FnDef(_, _)
                 | RigidTy::FnPtr(_)
                 | RigidTy::Closure(_, _)
-                | RigidTy::Coroutine(_, _, _)
+                | RigidTy::Coroutine(_, _)
                 | RigidTy::CoroutineClosure(_, _)
                 | RigidTy::CoroutineWitness(_, _)
                 | RigidTy::Foreign(_)

kani-compiler/src/kani_middle/transform/internal_mir.rs

@@ -50,7 +50,7 @@ impl RustcInternalMir for AggregateKind {
                     internal(tcx, generic_args),
                 )
             }
-            AggregateKind::Coroutine(coroutine_def, generic_args, _) => {
+            AggregateKind::Coroutine(coroutine_def, generic_args) => {
                 rustc_middle::mir::AggregateKind::Coroutine(
                     internal(tcx, coroutine_def.0),
                     internal(tcx, generic_args),

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-07-24"
+channel = "nightly-2025-07-29"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/script-based-pre/cargo_autoharness_contracts/contracts.expected

@@ -40,10 +40,6 @@ arithmetic_overflow\
 
 Autoharness: Checking function should_pass::alignment::Alignment::as_usize's contract against all possible inputs...
 
-should_pass::alignment::Alignment::as_usize\
-	 - Status: SUCCESS\
-	 - Description: "Rust intrinsic assumption failed"
-
 should_pass::alignment::Alignment::as_usize\
 	 - Status: SUCCESS\
 	 - Description: "|result| result.is_power_of_two()"