(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]

There is one regression related to generics (not providing the correct substs, somewhere?). @JonasAlaif can you have a look at the overall structure in traits.rs and trait_impls.rs in particular? Feel free to ignore cosmetics, formatting, etc, for now.

[JonasAlaif]

I didn't fully go through everything, but for now these changes should make things nicer and then I can go through the rest

[JonasAlaif]

All uses pass in the same DefId for both? It also doesn't make sense to have a different spec from the point of view of different contexts? Let's remove the second DefId?

[Aurel300]

This is needed to encode the behavioural subtyping checks: in the proof methods, we need to check the contract of the trait from the context of the implementor, i.e., we need to instantiate the contract with the correct TraitRef substitutions applied.

[JonasAlaif]

Where is that? When I find all uses of MirSpecEnc it always takes the exact same two DefIds as input (i.e. (def_id, def_id, ...))

[Aurel300]

prusti-dev/prusti-encoder/src/encoders/ty/generics/trait_impls.rs

Line 280 in df298b2

(trait_item_def_id, impl_item_def_id, MirSpecEncMode::Impure),

[JonasAlaif]

Ah ok, sorry yeah.

we need to instantiate the contract with the correct TraitRef substitutions applied

So you mean casting to concrete/generic correctly? It still seems like a lot of extra complication in MirSpecEnc for this one case - could we not add something like a MirSpecUseEnc wrapper that provides an api with the casts applied as necessary?

[JonasAlaif]

We should think about if these are necessary (since we're also skipping all the traits defined outside this crate anyway). Or do we need this to check behavioural subtyping? In #137 the hir::def::DefKind::Impl case is removed, since the TraitEnc goes through all impls anyway.

[Aurel300]

Yes, TraitImplEnc causes the behavioural subtyping checks to be emitted. Any crate can define:

• types
  We don't have to force the encoding of a type if it appears in a crate but doesn't get used; though it would be surprising from a Prusti user perspective if a type that causes Prusti to error out only does this when verifying a downstream crate that uses that type.
• traits
  When there are method bodies, we already encode them (it is a body owner in the crate). For methods without a default implementation, we should make sure the specs are well-formed, which will happen in (WIP) Encode spec items as methods #138. Associated types etc probably don't matter much when the trait is not used.
• trait impl blocks connecting (sets of) types to traits, where either the type or the trait may be coming from an upstream crate
  Here we should emit the behavioural subtyping check, and it shouldn't be pushed to downstream crates, i.e., iterating through all known impls (as in Concrete trait impl checks #137) seems wrong to me here.

[JonasAlaif]

We should have a deep think about if this caller_def_id is necessary. Maybe there should be a MirPureUseEnc which does all the required casting of arguments to/from generic?

[Aurel300]

Ok I guess this is ultimately a question of whether we want to trust that our encoding of generics will lead to the same results as rustc monomorphisation. A different caller_def_ids here will cause MirPureEnc to request a different body monomorphisation, which eventually affects the choice of the typing environment here:

prusti-dev/prusti-interface/src/environment/body.rs

Line 174 in 60ee0c0

let typing_env = TypingEnv::post_analysis(self.tcx, caller_def_id.unwrap_or(def_id));

(Which can then change whether we know a particular associated type resolves to a concrete type, for example.)

Either way I would prefer to postpone this to after this PR.

[Aurel300]

Ok so this causes a cycle:

trait Bar {
    type Target;
    fn deref(x: Self::Target);
}

And of course it would -- in trying to create the function identifier for deref, we need to already have a way to refer to the associated type (and it's a different encoder, MirLocalDefEnc, that's actually responsible for creating the types for the variables).

So as you suggested at some point @JonasAlaif I think I need to change this to have a separate encoder for the trait itself (its impl_* function, its associated types) and one for trait methods and functions.

[Aurel300]

Merged to unblock other PRs, in particular #137.