How to compile modules using Creusot contracts?

[Lysxia]

trafficstars

Following the Quickstart in the Creusot guide, I created a src/lib.rs file with some Creusot contracts. cargo creusot succeeds, but cargo build fails because some features are not enabled (which cargo creusot enabled implicitly to succeed). If I enable the features explicitly:

#![feature(stmt_expr_attributes,proc_macro_hygiene)]

Then cargo creusot complains because the features are enabled twice.

One workaround is to enable the feature conditionally:

#![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]

Am I missing something? Could Creusot not enable those features, or enable them only if they are not already enabled?

[xldenis]

Unfortunately, that's the best way I know of doing things, I suppose the alternative would be for creusot to not enable these features and instead just require all client projects to unconditionally enable them? I'm open to suggestions on this.

[Lysxia]

Yes, I think creusot should let users enable those features unconditionally.

#![feature(stmt_expr_attributes,proc_macro_hygiene)]

[jhjourdan]

I'd like a macro to generate these automatically each time we are using Creusot.

But here it is said that this is impossible:

https://users.rust-lang.org/t/how-to-generate-top-level-macro-calls-with-a-proc-macro/51142

Sad :'(

[xldenis]

The real solution is to just work to stablize these features :P

[jhjourdan]

I'm not confident that we will never use another unstable feature in the future.

[xldenis]

I'm not confident that we will never use another unstable feature in the future.

In our macros? That seems easier to guarantee, in the creusot compiler / contracts sure.

[Lysxia]

If it is a goal to be able to compile verified projects with a stable toolchain, we will need to disable all unstable features when compiling.

stmt_expr_attributes and proc_macro_hygiene are the only two problematic features that I am aware of on that front. They are needed to write loop invariants. A workaround is to replace invariant(_) with cfg_attr(creusot, invariant(_)). It's ugly but I also don't see another way until those features are stabilized, which is not any time soon.

Are there other features needed to make Creusot's annotations just parseable?

If that's the way to go, then I think it makes sense for cargo creusot to keep enabling the features it needs implicitly. (There is a case where a user enables a feature also enabled by Creusot, then they need to guard it with not(creusot). That's much more of a corner case than currently, where users must enable stmt_expr_attributes and proc_macro_hygiene all the time anyway.)

[xldenis]

It would also be worth pushing the rust teams on those features since both are fairly stable.

[Lysxia]

@jhjourdan proposed to have the dummy version of requires/ensures remove loop invariants, that avoids the need for cfg_attr, so I'm trying that now.