[Prusti: invalid specification] use of impure function "std::cmp::PartialEq::eq" in pure code is not allowed

[Pointerbender]

The following Rust program:

use prusti_contracts::*;

#[derive(Clone, Copy)]
pub struct A;

impl PartialEq for A {
    #[pure]
    fn eq(&self, other: &Self) -> bool {
        true
    }
}

impl Eq for A {}

impl A {
    #[pure] // removing this attribute makes `foo` verify
    #[requires(*self == *a)]
    pub fn foo(&self, a: &A) {}

    #[pure] // fails verification of `bar` both with and without this attribute
    #[requires(self == a)]
    pub fn bar(&self, a: &A) {}
}

fails verification with errors:

[2022-04-06T11:50:11Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_example::A::foo (prusti_example::{impl#2}::foo)
error: [Prusti: invalid specification] use of impure function "std::cmp::PartialEq::eq" in pure code is not allowed
  --> src/lib.rs:31:16
   |
31 |     #[requires(*self == *a)]
   |                ^^^^^^^^^^^

[2022-04-06T11:50:11Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_example::A::bar (prusti_example::{impl#2}::bar)
error: [Prusti: invalid specification] use of impure function "std::cmp::PartialEq::eq" in pure code is not allowed
  --> src/lib.rs:35:16
   |
35 |     #[requires(self == a)]
   |                ^^^^^^^^^

In the case of foo, Prusti should be able to be see that A implements Copy (i.e. no interior mutability) and that #[pure] std::cmp::PartialEq::eq (and core::cmp::PartialEq::eq) are legal to call for the equality check in a pure context.

For bar this is slightly more nuanced, because here it is comparing two references to A instead of instances of A, but I believe Prusti should be able to allow this as long as both A and &A implement Copy and eq is annotated with a #[pure] contract. The reason this might be more difficult is because Rust desugars this to <&A as PartialEq>::eq instead of <A as PartialEq>::eq.