Upgrade Rust toolchain to 2025-07-04 (#4199)

Relevant upstream PRs:
- rust-lang/rust#143214 (Remove let_chains
unstable feature)
- rust-lang/rust#143036 (Remove support for
`dyn*` from the compiler)

The latter was tracked as an unsupported feature in Kani, whereby we can
resolve one of our own issues as well.

Resolves: #4196
Resolves: #1784

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

@@ -791,15 +791,6 @@ impl GotocCtx<'_> {
                 e,
                 t,
             ) => self.codegen_misc_cast(e, *t),
-            Rvalue::Cast(CastKind::DynStar, _, _) => {
-                let ty = self.codegen_ty_stable(res_ty);
-                self.codegen_unimplemented_expr(
-                    "CastKind::DynStar",
-                    ty,
-                    loc,
-                    "https://github.com/model-checking/kani/issues/1784",
-                )
-            }
             Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => {
                 self.codegen_pointer_cast(k, e, *t, loc)
             }

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

@@ -17,7 +17,6 @@ use crate::args::ExtraChecks;
 use crate::kani_middle::transform::body::{
     CheckType, InsertPosition, MutableBody, SourceInstruction,
 };
-use crate::kani_middle::transform::check_values::SourceOp::UnsupportedCheck;
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::{Const, TyCtxt};
@@ -640,12 +639,6 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
                         })
                     }
                 }
-                // `DynStar` is not currently supported in Kani.
-                // TODO: https://github.com/model-checking/kani/issues/1784
-                CastKind::DynStar => self.push_target(UnsupportedCheck {
-                    check: "Dyn*".to_string(),
-                    ty: (rvalue.ty(self.locals).unwrap()),
-                }),
                 CastKind::PointerExposeAddress
                 | CastKind::PointerWithExposedProvenance
                 | CastKind::PointerCoercion(_)

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

@@ -139,10 +139,6 @@ impl RustcInternalMir for CastKind {
                     CoercionSource::Implicit,
                 )
             }
-            CastKind::DynStar => rustc_middle::mir::CastKind::PointerCoercion(
-                rustc_ty::adjustment::PointerCoercion::DynStar,
-                CoercionSource::Implicit,
-            ),
             CastKind::IntToInt => rustc_middle::mir::CastKind::IntToInt,
             CastKind::FloatToInt => rustc_middle::mir::CastKind::FloatToInt,
             CastKind::FloatToFloat => rustc_middle::mir::CastKind::FloatToFloat,

kani-compiler/src/main.rs

@@ -12,7 +12,6 @@
 #![feature(rustc_private)]
 #![feature(more_qualified_paths)]
 #![feature(iter_intersperse)]
-#![feature(let_chains)]
 #![feature(f128)]
 #![feature(f16)]
 #![feature(non_exhaustive_omitted_patterns_lint)]

kani-driver/src/main.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-#![feature(let_chains)]
 use std::ffi::OsString;
 use std::process::ExitCode;
 

rust-toolchain.toml

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