Inheritance of Purity from Trait Specs

[juliand665]

In specifying the standard library (#1249), I wanted to mark e.g. PartialEq::eq as pure by default (perhaps with an auto trait so people can opt out of that). However, I had to drop this spec due to unfortunate interaction with derive(PartialEq), a very common way for people to implement this for their types. Here is a snippet producing the error in combination with the specs in #1249:

#[derive(Clone, Copy, Default)]
struct Special {
    x: i32,
}

Unlike pre- and postconditions, purity is not applied to/inherited by trait implementations by default, requiring users to annotate them manually. This same issue arises for other commonly-derived traits, including PartialOrd and Default (though for the latter I decided to include the spec anyway, as it's significantly less common.) A workaround is to provide an extern spec for this:

#[extern_spec]
impl Default for Special {
    #[pure]
    fn default() -> Self;
}

This has two main caveats:

1. It is not reasonable to expect users to annotate all their derived implementations like this, especially for more complex ones like PartialOrd.
2. We lose the usual transparency feature of purity, where Prusti understands the contents of the function, so Special::default().x == 0 cannot be verified like this.

There are a few possible solutions:

1. Accept that users have to write this boilerplate. This is obviously problematic because derive implementations exist to avoid this kind of boilerplate.
2. Switch from an opt-out mechanism (auto trait) to an opt-in mechanism (non-auto trait) for this spec. This is undesirable because the point of making it opt-out is that it can reasonably be expected of most implementations.
3. Add a derive macro for each such trait that users simply have to add to the list, e.g. #[derive(Default, PureDefault)]. This could be a no-op when the prusti feature is not active.
4. Make methods inherit not just pre-/postconditions but also purity from the trait member they implement. I'm not sure about the soundness implications of this, but it feels like a simple, consistent solution.
5. The above, but hardcoded or otherwise made to apply only to certain traits. This could also be an "argument" to pure, e.g. pure(inherited = true), or perhaps inherited_pure, probably better than hardcoding.

Personally, I think 4. or 5. would make the most sense, and I would even slightly favor 4., though as said it's possible there's a major flaw with it in general.