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.
Fixes #1627 (Verus crashing on an external
impl Trait
when that trait has an associated type).@Chris-Hawblitzel or whoever wrote the trait logic should definitely confirm this, but below is why I think this fix is sound.
In
rust_to_vir_impl.rs:608
, we look uptrait_map[&trait_path]
. Here,trait_map
contains all the traits in the current crate, whiletrait_path
is iterating throughauto_import_impls
, which contains allimpl
s that are either for "new" traits (traits from the current crate), or externalimpl
s from the current crate. Then, thefor
loop starting on line 576 iterates through all of theauto_import_impls
(theimpl
s that might be visible to Verus), looking up their traits in thetrait_map
.The error case in #1627 comes from an external
impl
for an external trait, so the external trait doesn't appear intrait_map
. But since it is an externalimpl
for an external trait, Verus shouldn't be able to see it, so I think it shouldn't need to check whether there is an associated type match for it in the list of local traits.If my reasoning is incorrect, please let me know---I'd be happy to implement a different fix!
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.