Files
rust/compiler/rustc_builtin_macros
Matthias Krüger 4602127362 Rollup merge of #144444 - dawidl022:contracts/variable-scoping-rebased, r=jackh726
Contract variable declarations

This change adds contract variables that can be declared in the `requires` clause and can be referenced both in `requires` and `ensures`, subject to usual borrow checking rules. This allows any setup common to both the `requires` and `ensures` clauses to only be done once.

In particular, one future use case would be for [Fulminate](https://dl.acm.org/doi/10.1145/3704879)-like ownership assertions in contracts, that are essentially side-effects, and executing them twice would alter the semantics of the contract.

As of this change, `requires` can now be an arbitrary sequence of statements, with the final expression being of type `bool`. They are executed in sequence as expected, before checking if the final `bool` expression holds.

This PR depends on rust-lang/rust#144438 (which has now been merged).

Contracts tracking issue: https://github.com/rust-lang/rust/issues/128044

**Other changes introduced**:
- Contract macros now wrap the content in braces to produce blocks, meaning there's no need to wrap the content in `{}` when using multiple statements. The change is backwards compatible, in that wrapping the content in `{}` still works as before. The macros also now treat `requires` and `ensures` uniformally, meaning the `requires` closure is built inside the parser, as opposed to in the macro.

**Known limiatations**:
- Contracts with variable declarations are subject to the regular borrow checking rules, and the way contracts are currently lowered limits the usefulness of contract variable declarations. Consider the below example:

  ```rust
  #[requires(let init_x = *x; true)]
  #[ensures(move |_| *x == 2 * init_x)]
  fn double_in_place(x: &mut i32) {
      *x *= 2;
  }
  ```

  We have used the new variable declarations feature to remember the initial value pointed to by `x`, however, moving `x` into the `ensures` does not pass the borrow checker, meaning the above function contract is illegal. Ideally, something like the above should be expressable in contracts.
2025-10-29 08:07:49 +01:00
..
2025-10-20 12:20:15 -06:00