Cannot add `#[requires]` annotation to trait function

[zgrannan]

The following code:

extern crate prusti_contracts;
use prusti_contracts::*;

trait Foo {
  fn bar();
}

impl Foo for i32 {
  #[requires(true)]
  fn bar() {}
}


fn main() {}

fails with an error:

error[E0407]: method `prusti_pre_item_bar_6327fa48bb9046e192245691bf8cacfc` is not a member of trait `Foo`
  --> test.rs:10:3
   |
10 |   fn bar() {}
   |   ^^^^^^^^^^^ not a member of trait `Foo`

The semantics of how #[requires] should work across the definition / implementations of a trait are uncertain to me, but in any case this error message should probably be changed.

[dario23]

i briefly looked into this when preparing for the API invariants goal of my masters' thesis (which was eventually replaced with another goal), and the core problem seems to be that the macros generate the auxiliary functions at the exact location where they are defined, and then rustc doesn't like those additional functions. i think prusti could

• either require a proc-macro attribute on traits where methods have such attributes, so that in that proc macro we can move the generated functions out of the trait definition, or
• figure out how we can move them out after proc macro expansion, e.g. in the after_analysis step in prusti/src/callbacks.rs; i superficially don't see how we get mutable access to the AST or HIR from there; maybe the compilerconfig allows us to override passes::parse and we can call the original parse and modify the result afterwards?

[Aurel300]

Requiring an extra attribute for this would not be very user friendly. There is actually a way to do a mutable visit over the AST; @LDY1998 was trying something similar in a different context (extern specs). Lastly, although we generate the prusti_*_item_... methods as siblings of the original one, this is not something we have to do. They just need to be put somewhere. Putting them inside the annotated method should work in most cases, but not e.g. when the annotated method has no body (as in unimplemented trait items).

[zgrannan]

So it seems like the macro expansion forces the precondition function to be placed inside the impl block as it's defined there. Then, this error is reported during macro expansion, before after_analysis or after_expansion.

Would either of the following work?:

1. Somehow disable the error message during macro expansion and move the precondition function to the top-level in after_expansion
2. Instead of using a macro to expand the attribute, search the AST for the attribute in after_expansion and modify the AST to include the function.

I guess the second option is a larger architectural change

[vakaras]

We do not have mutable access to the AST. The only way we can change something is via procedural macros.

[vl0w]

We can annotate Foo with #[refine_trait_spec] to solve the issue. Maybe we should consider to simply throw a more meaningful error when this annotation is missing.