Nothing enforces that #[logic]/#[law]/#[predicate] attributes are the same in a trait declaration and in implementation.

[jhjourdan]

Creusot display no error messge for, e.g:

extern crate creusot_contracts;

use creusot_contracts::*;

trait T {
    #[law]
    #[ensures(x == x)]
    fn l(x: Self);
}

impl T for u32 {
    // #[law]
    #[ensures(y == y)]
    fn l(y: Self) {}
}

Or:

extern crate creusot_contracts;

use creusot_contracts::*;

trait T {
    #[logic]
    #[ensures(x == x)]
    fn l(x: Self);
}

impl T for u32 {
    // #[logic]
    #[ensures(y == y)]
    fn l(y: Self) {}
}

Or:

extern crate creusot_contracts;

use creusot_contracts::*;

trait T {
    // #[logic]
    #[ensures(x == x)]
    fn l(x: Self);
}

impl T for u32 {
    #[logic]
    #[ensures(y == y)]
    fn l(y: Self) {}
}

And so on.

[xldenis]

True, but we need to make sure to leave holes for special traits like Add, Index etc

[jhjourdan]

I see, so #403 is a dependency for this.

[xldenis]

Even then, we will need to special case Deref at the very least, but yes.

[jhjourdan]

Is this just because of Ghost ?

[xldenis]

In large part, but actually many functions are implicitly using this especially in top level contracts.

[xldenis]

It's not hard to special case these, in fact they already are.

[jhjourdan]

I don't know what you mean by "special case", but at some point we will need to make sure we do not call program functions in specifications...

[xldenis]

That's already the case: we check that all functions called in logical programs are pure (or are one of a small list of traits we 'overload'). We just need to allow those traits to be the only ones which allow impls to be logical despite the trait signature being a program function.