Add trait_conflicts.rs to detect conflicting trait implementations at the VIR/AST level

[Chris-Hawblitzel]

This pull request addresses https://github.com/verus-lang/verus/issues/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 https://github.com/verus-lang/verus/issues/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 and Sized, which it should not do. VIR should include these marker traits, and that would fix the specific problem in https://github.com/verus-lang/verus/issues/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 https://github.com/verus-lang/verus/issues/1094 ). For example, the following implementations would conflict with each other and cause contradictory axioms saying that bool::f() == 3 and bool::f() == 4:

impl T for bool { spec fn f() -> int { 3 } }
impl T for bool { spec fn f() -> int { 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 and Sized, 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 module trait_conflicts that adds code into the code generated by lifetime.rs:

fn emit_check_tracked_lifetimes<'tcx>(
    cmd_line_args: crate::config::Args,
    tcx: TyCtxt<'tcx>,
    verus_items: std::sync::Arc<VerusItems>,
    spans: &SpanContext,
    krate: &'tcx Crate<'tcx>,
    emit_state: &mut EmitState,
    erasure_hints: &ErasureHints,
    item_to_module_map: &crate::rust_to_vir::ItemToModuleMap,
    vir_crate: &vir::ast::Krate,
) -> State {
    let mut gen_state = crate::lifetime_generate::gen_check_tracked_lifetimes(
        cmd_line_args,
        tcx,
        verus_items,
        krate,
        erasure_hints,
        item_to_module_map,
    );
    crate::trait_conflicts::gen_check_trait_impl_conflicts(spans, vir_crate, &mut gen_state);

    for line in PRELUDE.split('\n') {
        emit_state.writeln(line.replace("\r", ""));
    }

    for t in gen_state.trait_decls.iter() {
        emit_trait_decl(emit_state, t);
    }
    for d in gen_state.datatype_decls.iter() {
        emit_datatype_decl(emit_state, d);
    }
    for t in gen_state.trait_impls.iter() {
        emit_trait_impl(emit_state, t);
    }
    for f in gen_state.fun_decls.iter() {
        emit_fun_decl(emit_state, f);
    }
    gen_state
}

The code generated by lifetime.rs and the code generated by trait_conflicts.rs share the same prelude (declared in lifetime.rs) but are otherwise independent. A new function state.restart_names() allows generated by lifetime.rs and the code generated by trait_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 https://github.com/verus-lang/verus/issues/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 on Sized, I was particularly struck by this comment in rustc's is_sized function ( https://github.com/rust-lang/rust/blob/c1b336cb6b491b3be02cd821774f03af4992f413/compiler/rustc_middle/src/ty/util.rs#L1244C1-L1252C6 ):

    /// Checks whether values of this type `T` have a size known at
    /// compile time (i.e., whether `T: Sized`). Lifetimes are ignored
    /// for the purposes of this check, so it can be an
    /// over-approximation in generic contexts, where one can have
    /// strange rules like `<T as Foo<'static>>::Bar: Sized` that
    /// actually carry lifetime requirements.
    pub fn is_sized(self, tcx: TyCtxt<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool {
        self.is_trivially_sized(tcx) || tcx.is_sized_raw(param_env.and(self))
    }

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.