Concrete trait impl checks

[Trzyq0712]

Instead of using axiomatized version of the trait check encoding, we will instead use a function with a concrete body.

This makes it clearer which types implement a specific trait without having to resort to making "negative implementations" for types that do not.

• Change encoding from axioms to concrete functions
• Unknown types
• Implementation blocks with trait bounds
• Support for projections with type generics

  impl<T: Foo<i32, Item = bool>> Bar for T {}

  let T_impl == (Self_trait) in
  Self_trait == T_impl &&
  Foo_impl(T_impl) && 
  Foo_assoc_Item(T_impl, i32_type()) == bool_type()
  

• Support for projections with const generics

  impl<T, const N: usize> Bar for T
  where
      T: Foo<CONST = { N }>,
      T: Baz<C = { N }>,
  {}

  let T_impl == (Self_trait) in
  let N_impl == (Foo_assoc_const_CONST(T_impl)) in
  Self_trait == T_impl &&
  Foo_assoc_const_CONST(T_impl) == N_impl && 
  Baz_assoc_const_C(T_impl) == N_impl && 
  Baz_impl(T_impl) && Foo_impl(T_impl)
  

[Aurel300]

@JonasAlaif Do we really want to go with existentials for the generics? It makes sense semantically but (apart from vaguely worrying about performance) I wonder if we need this at all? From our previous discussion about this I assumed it suffices to do, e.g., with struct Foo<T> { ... } and struct Bar<T> { ... }:

• type.is_Foo to encode that Foo<T> implements the trait;
• type.is_Foo && type.Foo_T1.is_i32 (or whatever the names are) to encode that Foo<i32> implements it;
• type.is_Foo && type.Foo_T1.is_Bar to encode that Foo<Bar<T>> implements it; and etc.

[Trzyq0712]

@JonasAlaif Do we really want to go with existentials for the generics? It makes sense semantically but (apart from vaguely worrying about performance) I wonder if we need this at all? From our previous discussion about this I assumed it suffices to do, e.g., with struct Foo<T> { ... } and struct Bar<T> { ... }:

* `type.is_Foo` to encode that `Foo<T>` implements the trait;

* `type.is_Foo && type.Foo_T1.is_i32` (or whatever the names are) to encode that `Foo<i32>` implements it;

* `type.is_Foo && type.Foo_T1.is_Bar` to encode that `Foo<Bar<T>>` implements it; and etc.

I started implementing it that way, but then ran into some issues in more complicated cases. For example this "legal" impl block:

impl<U, V: Foo<U>> Foo<U> for V {}

I would try to encode it as:

function Foo_impl(Self: Type, T: Type): Bool {
    (...)
    Foo_impl(Self, U) // What do we actually put for U
    (...)
}

Even to get to this one has to do some "thinking" and simplifying.

Additionally, the discriminator + destructor style encoding makes it much more verbose for more complex types, for example impl ... for ((i32, bool), (u32, i32, i64)). Though, this is a rather minor concern.

Lastly, I have simply found this easier to implement 😞.

[Trzyq0712]

One other issue that popped up is the Sized trait. Whenever there is a generic, the Sized constraint is automatically added. As the Sized trait is auto-implemented for all types by default, there are no actual impls for Sized making all our types !Sized by default. We can either always skip the Sized bounds, or make special-case it to be implemented by all types. What do you think?

[Trzyq0712]

I believe this is now a mostly final version for the encoding. Ready for review.

[Aurel300]

As the Sized trait is auto-implemented for all types by default, there are no actual impls for Sized making all our types !Sized by default.

Is this the case only for Sized? What about other (user-defined) auto traits? What about the other built-in ones, like Send or Sync?

Besides the minor comments, I worry a bit about:

• The fact that we have so much machinery for dealing with Sized trait specifically; the CanonicalTy seems to only exist for that, right?
• All the type disassembling and reassembling going on in trait_impls is quite a lot of logic.
• How much of this is rebase-able on #127 (if you know)? Some of the changes in traits.rs and trait_impls.rs seem quite similar to that PR's.

[Trzyq0712]

Is this the case only for Sized? What about other (user-defined) auto traits? What about the other built-in ones, like Send or Sync?

It's most certainly the case for other auto-traits too. I am implementing the Sized trait in this PR as Sized constraint is auto-added to all generics by default. The other auto-traits should be implemented later on.

* The fact that we have so much machinery for dealing with `Sized` trait specifically; the `CanonicalTy` seems to only exist for that, right?

Have mostly merged the logic of CanonicalTy into identity_for_ty. The Sized check is based on the check performed by the compiler in a private function.

* All the type disassembling and reassembling going on in `trait_impls` is quite a lot of logic.

It's quite complicated indeed. Without existentials, we need to "discover" an expression to which we can bind each generic instead and then assert equivalences between subsequent occurrences of the generic.

A way to do this differently would be to introduce the generics using let-expressions. This would reduce the visual clutter of repeating long accessor paths at the cost of more equality assertions. Additionally, with let-bindings for the impl block generics, we could now process the predicates in any order, and would avoid the dependencies between the projections.

* How much of this is rebase-able on #127 (if you know)? Some of the changes in `traits.rs` and `trait_impls.rs` seem quite similar to that PR's.

I tried to mimic or copy #127 where I have found it to do similar things. This could be probably improved.

[Aurel300]

This bit I find rather messy. Is the invariant here that only type declarations will be in the impl_params map? Can there not be conflicts? Can you add a comment to explain this? Either way matching on a Result (and why Result::Ok instead of just Ok?) here seems strange, I would expect Option maybe? There is no actual error occurring here...

[Trzyq0712]

The matching on Result stems from how GenericParams map each generic to a generic type or const (probably it should have been a custom enum there in the first place to avoid confusion).

[JonasAlaif]

@Aurel300 the main things to review are:

• The new "triggers" mechanism: takes an encoder key as input and runs a closure if that encoder is run with that key, these closures are run after all the initial encoding of things in the crate and can start new encoders and thus they are run until a fixpoint.
• The TraitImplEnc vs TraitImplConditionEnc distinction. The former is run for all impls in the current crate and encodes e.g. subtyping checks and unconditionally invokes the latter. The latter is run on any impl which is either in the current crate, or if all the types used in Self (i.e. MyType and OtherType in impl<T> MyTrait for MyType<T, OtherType) are ever constructed and encodes e.g. the boolean disjunct in the function impl_MyTrait(Type): Bool, the associated type axioms, or the subtyping definitional axioms (defining pure fn, pres/posts).

The test failures are because it spots the Clone impls for types declared in prusti-contracts and tries to do RustTyDecomposition::from_ty on them which fails because some are unsupported. I'll merge a PR that implements all those types before this one which will make the tests pass.

[Aurel300]

Quantifiers still differ in that they will have to have their triggers encoded. Add a TODO?

[Aurel300]

(Also this change doesn't really belong in this PR.)

[JonasAlaif]

I'll add a TODO, yeah. And sure it doesn't really belong, but I'm not going to do a separate PR just for this and there were clear issues with the existing code (e.g. for the SpecBlock it would still report forall in the error).

[Aurel300]

Here the watchers are fired before the cache is updated, in encode below it is done after. Firing after seems more reasonable to me (maybe avoiding some weird cycles which expect the key to be in the cache already...?).

[JonasAlaif]

Firing after would require a clone of the task_key. It doesn't actually matter when they fire (maybe the wrong term), since that only means that the closures get moved from one queue to another (from a "waiting for key and won't run if key not seen" queue to a "waiting for regular encoding to be done and will definitely run after that" queue). The latter queue only gets run after all the regular encoding is done (see prusti-encoder/src/lib.rs:72). I'm happy to add the extra clone if that makes it less confusing though, or maybe rename fire_watchers?

[JonasAlaif]

I think that this is basically ready then, it just needs #188 so that there are no regressions