Repository navigation
Upgrade the Rust toolchain to nightly-2026-10-21 - #5042
Merged
feliperodri merged 2 commits intoOct 22, 2026
Merged
Conversation
- Const::from_target_usize is an inherent method again, so drop the ConstExt imports. - core::bstr is now core::byte_str, behind the byte_str feature (rust-lang/rust#160912). Update the ByteStr model, the name match that recognizes ByteStr for autoharness, and the autoharness test that pins it. Resolves model-checking#5009.
core::ptr::Unique was removed (rust-lang/rust#164146). The test crate's copy of RawVec held one; hold the NonNull it wrapped instead, and drop the ptr_internals feature.
github-actions
Bot
added
Z-EndToEndBenchCI
feliperodri
enabled auto-merge
October 22, 2026 01:19
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Resolves #5009.
The automatic upgrade has been stuck at nightly-2026-10-12 since 10-13. This moves Kani to nightly-2026-10-21. Two upstream changes needed source changes, and one of them would have silently broken autoharness if a test hadn't pinned it:
core::bstris nowcore::byte_str, behind thebyte_strfeature (Renamebstrmodule/feature tobyte_strrust-lang/rust#160912). Besides the#![feature]and theByteStrmodel inkani_core, Kani recognizesByteStrfor autoharness by its module name (it has no diagnostic item). Left alone, that check would have quietly stopped matching, putting&ByteStrfunctions back on the skipped list.cargo_autoharness_byte_strcaught it, as it was written to.core::ptr::Uniquewas removed (NukeUnique(andptr_internals) rust-lang/rust#164146). Kani itself doesn't use it (Boxalready held aBoxRawbefore this range), but thevecdeque-cvetest crate's copy ofRawVecdid. It now holds theNonNullthatUniquewrapped.The third change is mechanical:
Const::from_target_usizeis an inherent method again, so theConstExtimports go.I also read the
rustc_publicandcore::intrinsicsdiffs over the range for changes that compile but behave differently.rustc_publichas none, and the one new intrinsic (codeview_annotation) has a no-op fallback body and isn't called fromstd.Verified locally (CBMC 6.11.0): the full
kani-regression.shandkani-llbc-regression.sh; the only failures werepush_slowandcell_stub, which run out of memory under my 6 GB CBMC cap, as they do onmain. Also clean:kani-fmt.sh --check,cargo clippy --workspace --tests -- -D warningsand the--cfg=kani_sysrootclippy.FYI for verify-rust-std:
kani_core'sByteStrmodel now namescore_path::byte_str, so a verify-rust-std branch picks this Kani up together with a library that has the rename.