Kani fails to compile libcore at `nightly-2025-08-07`

[zjp-CN]

Kani CI in verify-rust-std suddenly failed with no commit change of kani or verify-rust-std.

This is a bug in kani.

Commits for record:

• model-checking/verify-rust-std@f66ba41
• https://github.com/model-checking/kani/tree/9deeec1bec16c4b1f1173d5d652f99d330a4650f
• cc libcore is out of sync verify-rust-std#465

---

We can bump toolchain to see if libcore can compile, or fix kani at the rustc version.

NOTE: the current toolchain in kani is nightly-2025-08-16.

[tautschnig]

It seems that contracts and const traits interact in some way. Removing the contract on get_unchecked_mut makes compilation work. Note that the change from ~const to [const] does not actually make a difference, i.e., this fails to compile even when flipping back to ~const.

@zjp-CN in Zulip you said: "Interestingly, at this toolchain version, ~const Trait just compiles!" -- can you elaborate on that?

For me, no past version of Kani compiles this code, which is consistent with our metrics job suddenly failing -- despite neither changing the library source code nor the Kani version used for that particular job. This suggests a change in a dependency. The differences that I can spot between the most recent working version and a failing one are:

• Working: syn v2.0.105, proc-macro2 v1.0.97
• Failing: syn v2.0.106, proc-macro2 v1.0.101
  I am yet to figure out how to force use of the older version (or which dependency actually drags in those newer versions).

[zjp-CN]

Note that the change from ~const to [const] does not actually make a difference, i.e., this fails to compile even when flipping back to ~const.

Yeah. I noticed that too. I was confused by it. Now I think the error may result from syn.

Removing the contract on get_unchecked_mut makes compilation work.
This suggests a change in a dependency.

• Failing: syn v2.0.106

I think the relevent issue is dtolnay/syn#1896 where ~const was replaced by [const] in syn and syn just made a new release v2.0.106 two days ago exactly what CI failed. (I found it early, but forgot it is kani's safety proc-macro crate's dependency.)

"Interestingly, at this toolchain version, ~const Trait just compiles!" -- can you elaborate on that?

I mean cd library/core && cargo build just compiles libcore with ~const Trait syntax. But now I also find cargo build compiles [const] Trait too if get_unchecked_mut's trait bound is modified to it.

(As a tidbit, I find libcore can directly be compiled through cargo build, while kani indirectly compiles libcore through a dummy crate. They are not identical, since kani analyzes code beyond normal compilation. I mentioned this to indicate kani doesn't need the dummy trick to compile libcore. Wrapping cargo's rustc with kani to run cargo build in core crate should just work.)

• figure out how to force use of the older version (or which dependency actually drags in those newer versions)

1. We can use patch to use an older version, but it seems not to prevents multi versions. Only kani's direct syn needs the patch, so maybe no problem to try a syn patch to a repo using the git tag.
2. Or specify =2.0.105 to pin syn's version.
3. Modifying Cargo.lock will work, but not recommened.

cargo tree will help to see dependency graph including computed versions.

I have a question though, why kani's Cargo.lock changed? cargo build won't update lockfiles. AFAIK cargo install without --locked will recompute lockfile to compile, but run-kani.sh doesn't run install command.

Update: Oh, I see verify-rust-std's library folder generates new Cargo.lock. That's the breakage culprint?

Update2: Yep. Pinning syn version in library/contracts/safety/Cargo.toml makes compilation work.

-syn = { version = "2.0.18", features = ["full"] }
+syn = { version = "=2.0.105", features = ["full"] }

Update3: I see the difference between cargo build and kani compilation. safety proc macros gated by kani_host parse ItemFn, while normal cargo build won't enable kani_host which won't parse ItemFns.

[zjp-CN]

We can bump toolchain to see if libcore can compile, or fix kani at the rustc version.

I favor bumping toolchain, though the fix is simple by pinning syn's version in contracs/safety crate which is needless as ~const syntax disappears in new source code of core crate.

Update: another fix is keeping Cargo.lock, which is necessary to avoid such accidental dependency version change.

[tautschnig]

This has been resolved by #4302.