(WIP) Trait specs

[Aurel300]

For each trait:

• const generics
• For each of its associated functions (with or without a default impl):
  • symbolic/abstract pre, post functions
  • same for pledges
  • (later?) separate functions to combine the full base pre/postconditions
  • axioms to connect symbolic functions to base specs
  • stub method which uses symbolic functions
  • pure functions
• For associated functions with a default implementation:
  • method to show the base specs hold for this implementation
    • (method emitted, make sure base specs are used)

For each trait impl:

• const generics
• For each associated function (with a refined spec?)
  • axioms to connect symbolic functions to refined specs
  • methods to verify behavioural subtyping holds (separate for pre, post, pledges for precise error tracking)
  • method to show the refined? specs hold for this implementation
    • (method emitted, but need to use refined specs)

If using generic encoding:

• call stub method instead of trait method
• pure functions?

If monomorphising (which gets us better error tracking):

• try to resolve calls https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/ty/struct.Instance.html#method.try_resolve

[Aurel300]

@zgrannan I think you changed this last? Any chance you remember why if so? I'm not sure if the version using rebase_onto was already introduced in v2 at any point otherwise. V1 uses the version I reverted to.

(The issue was that resolving a trait method call resulted in reporting [Self/#0] as the trait substs instead of [Impl] (the implementor of the trait) as expected.)

[zgrannan]

My recollection is that the V1 logic did not do the correct substitution. For example, if we have:

trait Trait<T> {
    fn f<U>(self)
}

impl<X,Y> Trait<X> for Impl<X, Y> {
  fn f<U>(self){}
}

impl Impl<u8, u32> {
    fn baz<U>(self){
        self.f()
    }
}

and we called this method with the def id / substs for the call to self.f() in baz, then we'd have
the identity of Trait::f is [Self, T, U]
the args for the call are [Impl<u8,u32>,u8,u32,U]
the identity of Trait::f is [Self, T, U]
this method would be expected to return the substitution [Impl<u8, u32>, u8, U], corresponding to Self=Impl<u8,u32>, T = u8, U=U

However, with the current logic I think the output would try to instantiate
[Self, T, U] with the substs [Impl<u8,u32>,u8,u32,U]. I'm not sure if that works due to the arity mismatch but even ignoring that the result would I think be [Impl<u8,u32>, u8, u32].

My understanding is that rebase_onto implements what find_trait_method_substs is intended to do: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/type.GenericArgs.html#method.rebase_onto