Contracts allow side effect expressions

[celinval]

I tried this code:

#![feature(contracts)]

#[core::contracts::ensures({*x = 0; |_ret| true})]
fn buggy_add(x: &mut u32, y: u32 ) {
    *x = *x + y;
}

fn main() {
    let mut x = 10;
    buggy_add(&mut x, 100);
    assert_eq!(x, 110);
}

I expected to see this happen: The assertions should succeed

Instead, this happened: The assertion fails because x == 100. Note that this bad behavior happens even with the contract checks disabled. I.e.: with -Zcontract-checks=no

Meta

rustc --version --verbose:

rustc 1.86.0 (05f9846f8 2025-03-31)
binary: rustc
commit-hash: 05f9846f893b09a1be1fc8560e33fc3c815cfecb
commit-date: 2025-03-31
host: x86_64-unknown-linux-gnu
release: 1.86.0
LLVM version: 19.1.7

Context

We currently instantiate the ensures clause in the function body as is. This logic is different than how we handle requires, where we wrap it around a closure. This has a neat property that allow users to capture input values to implement old terms.

Unfortunately, this allows users to also mutate the input, which is rather dangerous. So I believe we should also wrap the ensures clause in a closure. We can keep the capture input behavior, but this will create another layer of indirection.

[compiler-errors]

doesn't wrapping in a closure still allow modifying through &Cell? and technically you can still modify globals?

[celinval]

Yes, this will be as side effect free as a Fn.