requires and ensure clauses on traits: add inheritance

[W95Psp]

We want the default requires and ensures on an impl to be inherited from the ones specified on the trait.

Currently we are forced to repeat them:

    #[hax_lib::attributes]
    trait Operation {
        #[requires(x.lift() <= int!(127))]
        #[ensures(|result| x.lift() * int!(2) == result.lift())]
        fn double(x: u8) -> u8;
    }

    struct ViaAdd;

    #[hax_lib::attributes]
    impl Operation for ViaAdd {
        #[requires(x.lift() <= int!(127))]
        #[ensures(|result| x.lift() * int!(2) == result.lift())]
        fn double(x: u8) -> u8 {
            x + x
        }
    }

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

That's still something we need, that's one big reason for the ergonomics being bad around traits+specs

[W95Psp]

Another example from #1125:

trait Encode {
fn encode();
}

impl<T: Encode> Encode for Option {
fn encode() {
T::encode();
}
}
Open this code snippet in the playground