Documentation for Type-Conditional Spec Refinements

[Pointerbender]

I'm playing around with the recently stabilized Type-Conditional Spec Refinements feature. I have a question about how to use it. For example, reading the docs I would expect that I would be able to do this:

use prusti_contracts::*;

pub unsafe trait Foo {}

pub trait Bar {
    #[refine_spec(where Self: Foo, [pure])]
    fn baz(&self) -> usize;
}

but this fails with the compilation error:

error: [Prusti: unsupported feature] Type-conditional spec refinements can only be applied to trusted functions
  --> src/lib.rs:33:5
   |
33 |     fn baz(&self) -> usize;
   |     ^^^^^^^^^^^^^^^^^^^^^^^

which is a bit confusing because there is no method body. However, this does seem to compile:

use prusti_contracts::*;

pub unsafe trait Foo {}

pub trait Bar {
    #[trusted]
    #[refine_spec(where Self: Foo, [pure])]
    fn baz(&self) -> usize;
}

and so does this:

use prusti_contracts::*;

pub unsafe trait Foo {}

pub trait Bar {
    fn baz(&self) -> usize;
}

#[extern_spec]
pub trait Bar {
    #[refine_spec(where Self: Foo, [pure])]
    fn baz(&self) -> usize;
}

What is the correct usage of #[refine_spec] on trait methods without a body? :) As an aside question, why can type-conditional spec refinements only be applied to trusted functions? Thanks!

[Aurel300]

The main motivation for refine_spec was for extern specs (see usage in #1249), which are trusted. Checking a refine_spec attached to a function with an implementation is difficult: in the general case, we might need to check a method multiple times, and we should check behavioural subtyping of the refined contract against the base one. We might work on this in the future but I would like to see a good use case first. Maybe you have one?

On the other hand, refine_spec on a trait method without a default implementation sounds reasonable. We should allow this, PRs welcome :)

[Pointerbender]

We might work on this in the future but I would like to see a good use case first. Maybe you have one?

Thanks for the explanation! Originally I wanted to be able to implement the same trait on both pure and impure types, which would then inherit the #[pure] attribute on their trait methods for pure types only. I chose a different approach by making separate pure and impure traits for now.