Make it possible for derives to emit `check(ghost)`

[Kixunil]

I tried to #[derive(creusot_std::prelude::PartialEq)] on a type and then use check(ghost) on a function that compares values of that type and it failed with error about equality not being ghost-compatible. I don't see any way to solve it other than manually implementing it. An attribute controlling the attributes of the emitted function would be helpful, so that tedious manual implementation can be avoided.

[Lysxia]

I think rather than replicating the derives from std, a better way may be to define new derives that produce extern_spec to attach specifications to the code generated by the std derives. Thoughts @jhjourdan ?

[Kixunil]

Sounds like ideally you'd detect that std derive was used and only attach specification if it was. Kinda like std has StructuralEq.

[jhjourdan]

The main problem here is that derives only give you access to syntax trees, and no typing information or anything more involved. In particular we don't have information about #[check(ghost)] of dependencies.

We could play with a pile of hacks that retrofit specifications on std derives, why not. I'm a bit afraid of the maintenance burden, though.

As far as #[check(ghost)] is concerned, I'd prefer to wait for #1997 to be implemented, because that could give us an easy way to specify derives from the specifications of their deps.