Extend the lifetime checker to support specialized trait implementations from rust standard lib

[ziqiaozhou]

Lifetime checker could not support some specialized trait implementations in rust standard lib. I am wondering whether the lifetime checker could give some exceptions to the trait implementation from standard lib.

use vstd::prelude::*;

verus!{
#[verifier::external_trait_specification]
pub trait ExTryFrom<T>: Sized {
    type Error;
    type ExternalTraitSpecificationFor: core::convert::TryFrom<T>;

    fn try_from(v: T) -> (ret: Result<Self, <Self as core::convert::TryFrom<T>>::Error>) where Self: core::convert::TryFrom<T>;
}

#[verifier::external_trait_specification]
pub trait ExTryInto<T>: Sized {
    type Error;
    type ExternalTraitSpecificationFor: core::convert::TryInto<T>;

    fn try_into(self) -> (ret: Result<T, <Self as core::convert::TryInto<T>>::Error>) where Self: core::convert::TryInto<T>;
}
}

fn main() {}

verus outputs the following errors.

error: conflicting implementations of trait `T29_TryFrom<Vec<_, std::alloc::Global>>` for type `std::boxed::Box<[_; _]>`
    --> .rustup/toolchains/1.82.0-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/convert/mod.rs:805:1
     |
805  | / impl<T, U> TryFrom<U> for T
806  | | where
807  | |     U: Into<T>,
808  | | {
809  | |     type Error = Infallible;
     | |____________________^
     |
    ::: .rustup/toolchains/1.82.0-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1906:1
     |
1906 | / impl<T, const N: usize> TryFrom<Vec<T>> for Box<[T; N]> {
1907 | |     type Error = Vec<T>;
1908 | |
1909 | |     /// Attempts to convert a `Vec<T>` into a `Box<[T; N]>`.
     | |__________________________________^

error: aborting due to 1 previous error

note: This error was found in Verus pass: ownership checking of tracked code

error: aborting due to 2 previous errors

Even after adding #![feature(specialization)] to generated crate-lifetime.rs, it still cannot work well A26_Error` specializes an item from a parent `impl`, but that item is not marked `default

[utaal]

@ziqiaozhou I moved this to feature requests. We're currently planning a replacement for the lifetime checker, and we'll take this into account.