Add trait_conflicts.rs to detect conflicting trait implementations at the VIR/AST level #1172
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.
This pull request addresses #1094 . There's more work that should be done for this issue, but this pull request should at least fix the current unsoundness and prevent the same unsoundness from reappearing in the future. The high-level problem in #1094 is that the VIR representation of trait implementations abstracted away some parts of the real Rust trait implementations. In particular, VIR omitted several marker traits, including
Copy
andSized
, which it should not do. VIR should include these marker traits, and that would fix the specific problem in #1094 . However, this pull request does something slightly different: it makes Verus more defensive against such problems in case they reappear in the future. Specifically, it checks that the axioms generated for trait implementations don't conflict (overlap) with each other, since such conflicts can lead to contradictory axioms that imply false (this was the issue in #1094 ). For example, the following implementations would conflict with each other and cause contradictory axioms saying thatbool::f() == 3
andbool::f() == 4
:Now, Rust already rejects this particular code, so this particular example didn't need fixing. However, if there's any mismatch between Rust's conflict checker and Verus's axioms, there's a danger that the axioms will conflict even if the original Rust code contained no conflicts. Therefore, I believe it is prudent to double-check the conflicts directly at the VIR level to avoid ever again generating contradictory axioms for trait implementations. This pull request does this be translating the VIR-level trait implementations back into Rust code (not necessarily the same as the original Rust code) that expresses the VIR-level representation of the trait implementations. For example, if VIR (incorrectly) omits traits like
Copy
andSized
, then the generated Rust code will also omit these traits, and the Rust conflict checker will then catch the conflicts that result from these omissions and report an error.This generated Rust code is packaged and checked with the existing generated Rust code from
lifetime.rs
. Specifically,lifetime.rs
calls out to a new moduletrait_conflicts
that adds code into the code generated bylifetime.rs
:The code generated by
lifetime.rs
and the code generated bytrait_conflicts.rs
share the same prelude (declared inlifetime.rs
) but are otherwise independent. A new functionstate.restart_names()
allows generated bylifetime.rs
and the code generated bytrait_conflicts.rs
to have differently named traits and datatypes generated from the same original Rust code so that these generated traits and datatypes don't interfere with each other.Independently, I still think the marker traits like
Sized
should also be added to VIR, which would also fix #1094 . However, I think even after this is done, this pull request can still be useful to guard against similar issues in the future. While working onSized
, I was particularly struck by this comment in rustc'sis_sized
function ( https://github.com/rust-lang/rust/blob/c1b336cb6b491b3be02cd821774f03af4992f413/compiler/rustc_middle/src/ty/util.rs#L1244C1-L1252C6 ):In other words, even inside rustc, it's hard to match every nuance of trait dispatch. If Verus fails to match these nuances, the consequences should be that Verus might reject some valid Rust trait implementations, not that it generates contradictory axioms.