Attribute shorthand for check blocks that could just be an expression

[ErichDonGubler]

@Johnny_Bob on Reddit made this interesting comment on the v0.4.0 release notice thread posted there:

This looks very useful. BTW in some simple situations it could be nice to use decorators to specify contracts. Did you consider adding something like this?

#[pre(x != i32::MAX, "cannot add one to input at max of number range")]
#[post(y, y - 1 == x, "reverse operation did not produce input")]
fn add_one(x: i32) -> i32 {
        x + 1
}

@ErichDonGubler's response was:

Huh, I hadn't considered this before, but this actually sounds really interesting. I would only want to list some concerns I have with this:

1. Do you consider it worthwhile to implement this in Adhesion when this functionality already exists in libhoare? There are several arguments I can think of, but I'm uncertain of their value and wanted your thoughts:
   • Especially nice is keeping the check names the same (i.e., pre instead of libhoare's precond, double_check instead of invariant)
   • It lets users depend on a single library.
2. I don't believe that we can use non-string expressions in attributes right now, but I could be wrong. That's an implementation detail, though. :)
3. Adhesion currently is expected to work on stable, while custom attributes generally involve some hackery to work. I'm not sure how to get this to work, and would need some support to ship this (if it's possible). As an alternative, however, we might be able to make an alternate syntax possible when considering the next point...
4. How should this interact with the contract! macro? I might actually be able to implement an alternate syntax if the expectation is that a short version a la your suggestion will only work inside of a contract! block -- but I wonder if users might get confused if they try this outside of the macro usage. Some cases:
   1. Attempted usage outside of contract! macro?
   2. Attempted usage INSIDE a contract! macro?
   3. Trying to specify pre and post blocks at the same time as the shorthand version should do...what? Should we accept it (if so, doing what?), fail silently, or throw an error? How important is it that the error be a good one?
5. Currently, Adhesion doesn't control conditional compilation -- that's still determined by individual statements and cfgs in the different check blocks. It would be necessary to offer similar control here, and some brief bikeshedding ( ;) ) on associated syntax would be necessary.

What do you think? I'm more than happy to do the work to implement this suggestion, because I really like it -- I'm just worried that it may not be possible or worth the effort yet.

EDIT: more details and grammar fixes.

[hellow554]

I'd like to have this feature too. I saw it on libhoare and there it worked (a long time ago) maybe you could just adopt the old code to work with the current rustc?

[ErichDonGubler]

Maybe -- I'd definitely want to add it as an unstable feature for now, since adding new attributes is unstable.

I would definitely be open to experimenting, though. Looks like the code libhoare uses isn't too bad, if somewhat boilerplate-ish.