Contract variable declarations

[dawidl022]

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-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 #144438 (which has now been merged).

Contracts tracking issue: #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:

  #[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.

[rustbot]

r? @jackh726

rustbot has assigned @jackh726.
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