Upgrade Rust toolchain to nightly-2026-08-21

[feliperodri]

All three dependencies — #4764 (nightly-2026-07-01), #4766 (cargo target layout) and #4767 (nightly-2026-08-01) — have merged, so this is now rebased onto main as a single commit and is ready for review.

Description

nightly-2026-08-21 is the first 1.100 nightly. Only 14 compile errors came with it — a much smaller upgrade than 08-01's 91 — but one runtime change broke the entire sysroot. That one first:

1. The sysroot needs -Zembed-metadata=yes

Cargo builds Kani's library/std and library/kani with metadata embedding off, so the rlib holds only a metadata stub and the full .rmeta is left behind in the build directory. Kani copies just the rlib into its sysroot and later compiles against it standalone, so every verification failed:

error: only metadata stub found for `rlib` dependency `std`
       please provide path to the corresponding .rmeta file with full metadata

That took out 534 of 607 kani tests. The symptom was visible in the artifacts — the sysroot's libstd.rlib was 1024 bytes, and ar t showed nothing but a stub:

$ ar t target/kani/lib/libstd.rlib
__.SYMDEF
lib.rmeta          # 440 bytes -- the stub
lib.rmeta-link

Asking for full metadata in the sysroot build keeps those rlibs self-contained (they grow to 32 KB / 596 KB) and takes the failures from 534 to 2.

2. Mechanical API adaptations

Change	Adaptation
LangItem moved from rustc_hir to rustc_hir::attrs::lang_items	3 imports, matching the path the compiler itself uses
CodegenBackend::join_codegen gained Option<&IncrCompSession>	added in both backends
Analysis::apply_primary_terminator_effect no longer returns TerminatorEdges	the framework computes them itself; drop the return value and the now-unused 'mir lifetime
BackendRepr::SimdVector's lane count is BackendLaneCount (a NonZero<u16>), not u64	codegen_vector calls as_u64()
TargetConfig's target_features + unstable_target_features → one internal_target_features: UnordSet<Symbol>	also removes the FIXME do unstable_target_features properly, since there is no longer an unstable list
TyCtxt no longer implements rustc_hir_pretty::PpAnn	the impl is on &dyn HirTyCtxt, which TyCtxt does implement, so syn_attr coerces through it
evaluate_obligations_error_on_ambiguity returns a TraitErrors enum, not a vector	the emptiness check becomes no_errors()
LocalModDefId renamed LocalModId	rename

3. fn_abi_of_instance now refuses LLVM intrinsics

fn_abi_adjust_for_abi asserts that the ABI is not Unadjusted. InstanceKind::LlvmIntrinsic already existed on nightly-2026-08-01 — where computing an ABI for one was still allowed, so codegen could treat it as an ordinary item — but on 1.100 that aborts the compiler:

assertion `left != right` failed: fn_abi_of_instance should not be called on LLVM intrinsics

There is no way to obtain a FnAbi for one: the assert sits in the shared fn_abi_new_uncached, so deriving it from the signature trips it too. Without an ABI Kani cannot codegen the call or even its arguments, and it has no model for LLVM intrinsics anyway, so codegen_funcall now reports the call as an unsupported construct (#4770) before touching the ABI:

call to LLVM intrinsic `llvm.aarch64.neon.uqadd.i64` is not currently supported by Kani.
Please post your example at https://github.com/model-checking/kani/issues/4770

This preserves the earlier behaviour. Before 1.100 these were foreign items (DefKind::Fn declarations in stdarch's extern "unadjusted" blocks), so they went through Kani's FFI shim, which raised an equivalent unsupported-construct check. As then, reaching one fails verification and code that never reaches one still verifies.

4. New CastKind::BoxDerefTransmute

An elaborated Box deref that turns the inner pointer into a raw one. Its documentation calls it a regular transmute that is additionally UB if the input is not valid as a Box<T>, and states that backends may treat it as a plain transmute. So codegen and the value checks group it with Transmute (as cranelift does) — Kani checks pointer validity separately at the deref itself. The stable-to-internal conversion maps it faithfully rather than collapsing it to Transmute, because MIR validation distinguishes the two (Cannot BoxDerefTransmute to non-pointer type).

Worth a reviewer's eye: the extra "input not valid as Box<T>" UB is not separately modelled. If we want a dedicated check there, that is a follow-up rather than part of a toolchain bump.

Test changes (3 files)

atomic_load and atomic_store gained a VOLATILE: bool const parameter. Each call passes false, matching what the ordinary atomic types in core pass, and borrows their /* VOLATILE */ annotation so the bare bool reads clearly:

atomic_store::<_, { AtomicOrdering::SeqCst }, /* VOLATILE */ false>(ptr_a1, 0);

I checked every atomic intrinsic signature rather than only the ones the suites happened to flag — no other atomic intrinsic changed (cxchg, cxchgweak, xchg, xadd, xsub, and, nand, or, xor, max, min, umin, umax, fence, singlethreadfence are all unchanged). This matters because 27 of the 29 Intrinsics/Atomic tests are fixme-ignored, so the compiler never type-checks them.

No verification behaviour changed.

Testing

Local, macOS aarch64, CBMC 6.10.0 (cbmc-6.9.0-214-g45436eea34), on this branch rebased onto current main (8fcd6d90e):

Suite	Result
kani	607 passed, 0 failed (matches the 08-01 baseline exactly)
cargo-kani	71 passed, 0 failed
cargo-ui	30 passed, 0 failed
expected	472 passed, 0 real failures — see below
ui	150 passed, 2 failed — environmental, see below

Also clean: both the CPROVER and LLBC builds, cargo clippy --workspace --tests -- -D warnings, RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings, and ./scripts/kani-fmt.sh --check.

Re-verified after rebasing onto merged main: the cherry-pick was clean, and main's squashed versions of the three dependencies matched what I had locally apart from one comment touch-up (predicates_of -> clauses_of) that main already carries.

The LLVM-intrinsic abort was caught by CI on kani/SizeAndAlignOfDst/main_assert.rs, which passes vacuously on macOS (its body is #[cfg(not(target_os = "macos"))]) and so could not reproduce on my machine. I reproduced the same abort locally with a targeted probe instead, confirmed the identical assertion, and confirmed the fix resolves it:

#[kani::proof]
fn check_scalar_saturating_add() {
    use std::arch::aarch64::vqaddd_u64;   // -> llvm.aarch64.neon.uqadd.i64
    let (x, y): (u64, u64) = (kani::any(), kani::any());
    let _ = unsafe { vqaddd_u64(x, y) };
}

Before the fix: signal: 6 (SIGABRT) with fn_abi_of_instance should not be called on LLVM intrinsics. After: the unsupported-construct check shown above.

Two caveats, stated rather than omitted:

• expected/shadow/slices/slice_split is unverified locally. It spends >20 minutes in CBMC's SAT solver and I interrupted it. It is not a regression from this upgrade or from 08-01: I timed it on the 07-01 branch as a control and it is equally slow there. CI covers it.

• The two ui failures are solver-attribute/cadical and solver-option/cadical, both expecting Solving with CaDiCaL. My local CBMC reports The specified solver, 'cadical', is not available — a missing solver in my environment, independent of the Rust toolchain, and failing identically on 08-01.

• Was this change tested? Yes

• Is this a breaking change? No

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