#[contracts::requires(...)] + #[contracts::ensures(...)]

[pnkfelix]

cc #128044

Updated contract support: attribute syntax for preconditions and postconditions, implemented via a series of desugarings that culminates in:

1. a compile-time flag (-Z contract-checks) that, similar to -Z ub-checks, attempts to ensure that the decision of enabling/disabling contract checks is delayed until the end user program is compiled,
2. invocations of lang-items that handle invoking the precondition, building a checker for the post-condition, and invoking that post-condition checker at the return sites for the function, and
3. intrinsics for the actual evaluation of pre- and post-condition predicates that third-party verification tools can intercept and reinterpret for their own purposes (e.g. creating shims of behavior that abstract away the function body and replace it solely with the pre- and post-conditions).

Known issues:

• My original intent, as described in the MCP (Contracts: Experimental attributes and language intrinsics compiler-team#759) was to have a rustc-prefixed attribute namespace (like rustc_contracts::requires). But I could not get things working when I tried to do rewriting via a rustc-prefixed builtin attribute-macro. So for now it is called contracts::requires.

• Our attribute macro machinery does not provide direct support for attribute arguments that are parsed like rust expressions. I spent some time trying to add that (e.g. something that would parse the attribute arguments as an AST while treating the remainder of the items as a token-tree), but its too big a lift for me to undertake. So instead I hacked in something approximating that goal, by semi-trivially desugaring the token-tree attribute contents into internal AST constucts. This may be too fragile for the long-term.

  • (In particular, it definitely breaks when you try to add a contract to a function like this: fn foo1(x: i32) -> S<{ 23 }> { ... }, because its token-tree based search for where to inject the internal AST constructs cannot immediately see that the { 23 } is within a generics list. I think we can live for this for the short-term, i.e. land the work, and continue working on it while in parallel adding a new attribute variant that takes a token-tree attribute alongside an AST annotation, which would completely resolve the issue here.)

• the intent of -Z contract-checks is that it behaves like -Z ub-checks, in that we do not prematurely commit to including or excluding the contract evaluation in upstream crates (most notably, core and std). But the current test suite does not actually check that this is the case. Ideally the test suite would be extended with a multi-crate test that explores the matrix of enabling/disabling contracts on both the upstream lib and final ("leaf") bin crates.

[rustbot]

r? @fee1-dead

rustbot has assigned @fee1-dead.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[rustbot]

Some changes occurred to MIR optimizations

cc @rust-lang/wg-mir-opt

[oli-obk]

Please add a ui test with an attribute proc-macro aux build that conflicts with contracts::requires (so I guess a crate contracts with a requires proc-macro attribute?)

[petrochenkov]

This macro should be able to use register_attr! above.

[jieyouxu]

I'm not sure if we actually can, if we want to support arbitrary syntax within the contracts::require(...) -- doesn't register_attr! mandate that the requires expression conform to ast::MetaItem, which imposes restrictions on what the syntax can be, i.e. x > 0 wouldn't work?

[jieyouxu]

I took a closer look at this, and this is very unfortunate. I don't believe the current builtin macro setup allows for "path segments"-like namespacing (like rustc_contracts::require). I've tried to change the builtin macro support to allow multiple "segments" via SmallVec<[Symbol; 2]>, but as one would expect, that change kept propagating outwards to attributes.

[pnkfelix]

sorry for my delay in responding here.

@jieyouxu is exactly right.

specifically, register_attr! expands to a SyntaxExtensionKind::LegacyAttr, which is where the conformance to ast::MetaItem is enforced IIRC.

The plan here to support code snippets like x > 0 in a contract form means that we cannot conform to ast::MetaItem.

(In theory I could try to extend the register_attr! macro to support expansion to non LegacyAttr. Is that what you are asking for, @petrochenkov ?)

[celinval]

@petrochenkov let me know if you want me to make any changes here. Per @pnkfelix comment, using register_attr! would restrict the input of the contract attributes which is not desirable here. Thanks!

[RalfJung]

If that is the reason, at the very least a comment is needed to explain that.

[celinval]

There are comments in the builtin macro implementation. Would you like me to add comments to this file as well?

[fee1-dead]

r? compiler

[chenyukang]

r? compiler

[Nadrieril]

I don't know that part of the compiler

r? @petrochenkov would you like to review this?

[petrochenkov]

would you like to review this?

No.
r? compiler

[petrochenkov]

r? compiler

[jieyouxu]

I'll ask T-compiler for another suitable reviewer to take a look at the HIR/MIR parts of the PR, or take over the review. In the mean time, I'll also roll a T-libs reviewer for the libs part.

r? jieyouxu
r? libs

[traviscross]

Suggested change

	/// Allows use of contracts attributes.
	(unstable, rustc_contracts, "CURRENT_RUSTC_VERSION", Some(133866)),
	/// Allows access to internal machinery used to implement contracts.
	(unstable, rustc_contracts_internals, "CURRENT_RUSTC_VERSION", Some(133866)),
	/// Allows use of contracts attributes.
	(incomplete, contracts, "CURRENT_RUSTC_VERSION", Some(133866)),
	/// Allows access to internal machinery used to implement contracts.
	(internal, contracts_internals, "CURRENT_RUSTC_VERSION", Some(133866)),

As a lang experiment, these should go in with the experimental warning. Also, the rustc_ bit should be removed from the feature flag.

[celinval]

Should I go ahead and rename all usages of RustcContract with just Contract?

I also just noticed that contracts_internals feature should be in fact marked as internal. So I'll do that instead.

[celinval]

@rustbot ready

@oli-obk I believe I addressed the pending comments. Let me know if I forgot anything.

[bors]

☔ The latest upstream changes (presumably #136371) made this pull request unmergeable. Please resolve the merge conflicts.

[oli-obk]

since you need to rebase anyway, here's also some style nits that you can take or ignore 😆

r=me

[celinval]

@bors rollup r=@oli-obk

[bors]

📌 Commit ddbf54b has been approved by oli-obk

It is now in the queue for this repository.

[mkovaxx]

@pnkfelix @celinval I'm trying to use this, and ran into an issue with "stacking" attributes.

For example, the following causes a macro expansion error:

#![feature(contracts)]

#[core::contracts::requires(true)]
#[core::contracts::requires(true)]      // This line causes an error.
#[core::contracts::ensures(|_| true)]
#[core::contracts::ensures(|_| true)]
fn some_function() {}

Running it like so causes an error:

$ cargo +nightly test --test simple_test
  |
4 | #[core::contracts::requires(true)]
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected one of `.`, `?`, `where`, `{`, or an operator

Is this expected? Am I doing something wrong?

More info about the toolchain:

$ cargo +nightly --version              
cargo 1.92.0-nightly (966f94733 2025-09-16)

[celinval]

Hi @mkovaxx, the current implementation support up to one occurrence of each contract attribute per item.