Upgrade Rust toolchain to nightly-2026-07-01

[feliperodri]

Important

Draft: do not review until #4760 (nightly-2026-06-01) is merged.

This branch is stacked on #4760, so its diff currently contains that commit too. Once #4760 lands this rebases down to the single nightly-2026-07-01 commit. Review only the last commit.

Description

Bumps rust-toolchain.toml from nightly-2026-06-01 to nightly-2026-07-01.

A much smaller upgrade than the previous two (25 compile errors vs. 66 for 06-01): no verification behaviour changed and no test needed adjusting. Every change is a mechanical adaptation to a moved or renamed API.

1. FieldDef moved to the crate_def_with_ty! macro

// nightly-2026-06-01
pub struct FieldDef { pub(crate) def: DefId, pub name: Symbol }
impl FieldDef {
    pub fn ty_with_args(&self, args: &GenericArgs) -> Ty { .. }
    pub fn ty(&self) -> Ty { .. }
}

// nightly-2026-07-01
crate_def_with_ty! { pub FieldDef { pub name: Symbol } }

ty() and ty_with_args() are no longer inherent methods; they come from the CrateDefType trait, which the macro implements. The 17 call sites across 10 files therefore only need that trait in scope. The semantics are identical — both the old inherent methods and the trait defaults resolve to def_ty/def_ty_with_args — so this is a pure import change.

Imports were added per file to match each file's existing use rustc_public::.. style. Worth noting for future upgrades: as more rustc_public types migrate onto these macros, this particular adaptation is likely to recur, so a shared import point may eventually be worth it.

2. EarlyBinder::bind takes the interner

EarlyBinder::bind(value) becomes EarlyBinder::bind(tcx, value) — five sites in stubbing/mod.rs, transform/mod.rs and codegen/typ.rs.

3. Terminator gained MIR-level attributes

pub struct Terminator<'tcx> {
    pub source_info: SourceInfo,
    pub kind: TerminatorKind<'tcx>,
    pub attributes: ThinVec<AttributeKind>,   // new
}

The stable (rustc_public) representation has no equivalent, and terminators Kani synthesizes carry none, so the internal_mir conversion passes an empty vector.

4. TerminatorKind::Drop lost async_fut

That field is dropped from the internal_mir conversion.

5. Work products are an UnordMap

CodegenBackend::join_codegen's return type changed from FxIndexMap<WorkProductId, WorkProduct> to UnordMap<..>. Updated in both backends, including the downcast target and the empty map each returns.

Testing

Local, macOS aarch64, CBMC 6.10.0 (cbmc-6.9.0-214-g45436eea34). Clean on the first attempt — no test changes were needed:

Suite	Result
kani	607 passed, 0 failed, 23 ignored
cargo-kani	71 passed, 0 failed
script-based-pre	68 passed, 0 failed, 1 ignored
std-checks	5 passed, 0 failed
cargo-ui	30 passed, 0 failed
coverage	20 passed, 0 failed
prusti / smack / kani-docs / json-handler / cargo-coverage / firecracker	8 / 40 / 13 / 5 / 2 / 0 passed, 0 failed
ui	151 passed, 2 failed — both the cadical tests, see below

Other gates, all clean:

• cargo build-dev
• cargo build-dev -- --features cprover --features llbc
• cargo clippy --workspace --tests -- -D warnings and RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings
• RUSTFLAGS="-D warnings" cargo build --no-default-features --features cprover
• ./scripts/kani-fmt.sh --check
• Unit tests: cprover_bindings, kani-compiler, kani-driver, kani_metadata, kani --features concrete_playback, kani_macros

Environment caveat: this CBMC build has no cadical, so ui/solver-{attribute,option}/cadical fail locally on output text only ("The specified solver, 'cadical', is not available"). Both are expected to be clean on CI.

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