Fix panic from cross-crate FnDef impl-path collision#2559
Merged
Conversation
mmcloughlin
commented
Jun 14, 2026
Comment on lines
+2045
to
+2047
| // The test defines 12 `Clone` impls in the crate root, which are enough to | ||
| // collide with the `Clone` impls for `Ghost` and `Tracked` in | ||
| // `verus_builtin` at the same disambiguator (brought in by `["vstd"]`). |
Collaborator
Author
There was a problem hiding this comment.
This is quite a fragile test in that it relies on a disambiguator collision with definitions in verus_builtin.
The ideal test would setup two synthetic crates to force a collision. However, I'm not sure there's an easy way to setup multi-crate tests? Most rust_verify_test tests are single file.
tjhance
reviewed
Jun 14, 2026
tjhance
left a comment
tjhance
left a comment
Collaborator
There was a problem hiding this comment.
The definition of impl_fndef still seems a little dubious to me:
pub(crate) fn impl_fndef(fun: &Fun, kind: ClosureKind) -> Ident {
let joined =
fun.path.segments.iter().map(|s| s.as_str()).collect::<Vec<_>>().join(PATH_SEPARATOR);
Arc::new(format!("{}{}{}", PREFIX_IMPL_FNDEF, kind, joined))
}
e.g. it seems like there could be a collision if the first segment of joined starts with "Once" or "Mut"?
Can we come up with a different strategy entirely here? There doesnt' seem to be any reason to collapse the segments. We could do something like:
fun.path.push_segment(format!("{}{}", PREFIX_IMPL_FNDEF, kind))
mmcloughlin
added a commit
to mmcloughlin/verus
that referenced
this pull request
Jun 14, 2026
Per review feedback on verus-lang#2559: rather than flattening the function's path segments into a single `impl_fndef` ident and stamping the crate back on, push the per-kind marker as its own segment onto the function's path. This keeps the crate in `Path.krate` and avoids ambiguity at the kind/segment boundary (e.g. kind `Fn` followed by a segment starting with `Once` vs kind `FnOnce`).
The synthetic `FnDef : Fn{,Mut,Once}` trait-impl that Verus generates for
each `clone` method built its impl path from the function's path segments
only, dropping the crate and placing it under CrateId::Internal. Two
crate-root impls in different crates can share a rustc disambiguator
(e.g. `impl&%7` is both verus_builtin's `Clone for Ghost` and a user
crate's clone impl), so their synthetic paths collided, tripping the
`!trait_impl_map.contains_key(..)` assertion in GlobalCtx::new.
Carry the function's own crate in the impl path instead. Adds a
regression test.
Per review feedback on verus-lang#2559: rather than flattening the function's path segments into a single `impl_fndef` ident and stamping the crate back on, push the per-kind marker as its own segment onto the function's path. This keeps the crate in `Path.krate` and avoids ambiguity at the kind/segment boundary (e.g. kind `Fn` followed by a segment starting with `Once` vs kind `FnOnce`).
mmcloughlin
force-pushed
the
derive-copy-panic
branch
from
950dfb8 to
67f7e9a
Compare
Collaborator
Author
Much nicer! Implemented. Please take another look @tjhance. |
tjhance
approved these changes
Jun 14, 2026
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
2 participants
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.
The synthetic
FnDeftrait-impl that Verus generates for eachclonemethod built its impl path from the function's path segments only, dropping the crate and placing it underCrateId::Internal.Two crate-root impls in different crates can share a
rustcdisambiguator. For exampleverus_builtinhasClone for Ghostassigned toimpl&%7, which can collide with a definition in a user crate.This PR uses the function's krate in the path instead of
CrateId::Internal. Adds a regression test.Related: #2474
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.