Trivial intermediate assertions failed between two FnMut calls

[boulme]

Hello,

The following code is proved with Creusot/Alt-Ergo. But if I decomment the two intermediate assertions on a@, they both fail (while everything else still works). This seems very weird to me!

fn bar1() {
    let mut a = 0;
    let mut b = 10;
    let mut f =
        #[requires((*d)@ <= 100)]
        #[requires(a@ <= 100)]
        #[ensures((^d)@ == (*d)@ + 1)]
        #[ensures(a@ == old(a)@ + 1)]
          |d: &mut u32| {
              *d += 1;
              a += 1;
          };
//    proof_assert!(a@ == 0);
    proof_assert!(b@ == 10);
    f(&mut b);
//    proof_assert!(a@ == 1);
    proof_assert!(b@ == 11);
    f(&mut b);
    proof_assert!(a@ == 2);
    proof_assert!(b@ == 12);
}

[xldenis]

I think this is an unintuitive consequence of the prophetic model of Creusot. I'm not sure what we could do to improve the ergonomics here: perhaps forbid asserting anything about a until the closure b is dropped (and you recover permission to a)?

The issue here is that a is borrowed by mutable capture in b. Thus it is provided with a prophetic value representing the final value that b will have. Each individual closure call reborrows that prophecy but never actually resolves the whole prophecy, that only occurs when the closurre is dropped.

Note: Using a assert! instead of a proof_assert! would cause Rust to complain about a being borrowed. While what we do is sound I don't think there's a practical use for it and we should forbid it as well.

[boulme]

Thanks. I got it (despite the fact that your answer may say b instead of `f``): observing a borrowed location before the end of its borrow is meaningless. Exactly, like in this simpler example:

fn meaningless_observations_while_borrowed() {
    let mut a = 0;
    let mut c = &mut a;
    proof_assert!(a@ == 0);
    *c += 1;
    proof_assert!(a@ == 1);
    *c += 1;
    proof_assert!(a@ == 2);
    *c += 1;
    proof_assert!(a@ == 3);
}

Yes, for ergonomics: 1) it would be great to have a variant of borrow-checking that forbids about such meaningless Pearlite clause. 2) at some point, it could be useful (for expressivity) to have some way to speak in Pearlite clauses about the borrow of a in closure fabove. This would allow to speak about the state of a at least indirectly, such as in the simpler example, which becomes meaningful, if we replace the intermediate a@ by (*c)@.

[boulme]

I am not sure whether this is related, but I have difficulties to make FnMut closure work with reborrowing. For example, foo_ok is proved by Creusot/Alt-Ergo:

fn foo_ok() {
    let mut b1 = 20;
    let f =
        #[requires((*c)@ <= 100)]
        #[ensures((^c)@ == (*c)@ + 1)]
         |c: &mut u32| {
              let x = &mut *c;
              *x += 1;
         };
    let c = &mut b1;    
    f(c);
    f(c);      
    proof_assert!(b1@ == 22);
}

But, foo_ko is not: both the postcondition of the closure and the precondition of the second call are not provable.

 fn foo_ko() {
    let mut b1 = 20;
    let c = &mut b1;
    let mut f =
        #[requires((*c)@ <= 100)]
        #[ensures((^c)@ == (*c)@ + 1)]
         || {
              let x = &mut *c;
              *x += 1;
          };
    f();
    f();      
    proof_assert!(b1@ == 22);
}

Is the postcondition incorrect ? What happens here ?

[jhjourdan]

Is the postcondition incorrect ? What happens here ?

The postcondition of the closure is not correct. In the post-condition, c is the value of the variable c in the parent scope. So, its prophecy is the value of c at the end of its life, i.e., at the end of foo_ko. It is not the value of c at the end of the closure call.

In the ensures clause, the reference to variable c is interpreted by the value of c at the end of the closure call, while old(c) is the value of c at the beginning of the closure call. Hence, the postcondition should be written: (*c)@ == (*old(c))@ + 1. Note, in addition, that there is no reason to create the borrow c : the closure could manipulate b1 directly.

The situation of captured variables is different to the situation of parameters. Indeed, the only relevant value of a parameter is its value at function entry (the parameter does not exists at function exit): if we want mutability, we pass a mutable borrow, and give a specification on the propphecy; but there, we speak in the postcondition of the prophecy passed at function entry. For captured values, the situation is different: their type is not a borrow (at least, not a borrow function call lifetime), but they have both a relevant value at entry and at exit. So we use the more traditional x/old(x) approach here. (Of course, behind the scenes, this is encoded using mutable borrows and prophecies, but this is not what the user sees.)

[boulme]

Thank you for your answer @jhjourdan, it clarifies a lot the picture for me.

I know that there is no reason to create the borrow c, except that I wanted to better understand the interplay of old, borrows and prophecies. Actually, your solution was one of my first attempt, but Creusot crashes on this version, with the error message given below. Used to Frama-C, I also tried old(*c) instead of *old(c). On this variant, cargo creusot does not crash, but why3 complains that at and old can only be used in program annotations.

cargo creusot -- --features=contracts --verbose
       Fresh autocfg v1.1.0
       Fresh unicode-ident v1.0.12
       Fresh cfg-if v1.0.0
       Fresh proc-macro2 v1.0.67
       Fresh libc v0.2.148
       Fresh num-traits v0.2.16
       Fresh quote v1.0.33
       Fresh num-integer v0.1.45
       Fresh getrandom v0.2.10
       Fresh syn v2.0.37
       Fresh num-bigint v0.3.3
       Fresh uuid v1.4.1
       Fresh creusot-contracts-dummy v0.2.0 (https://github.com/xldenis/creusot.git#c522ecc2)
       Fresh pearlite-syn v0.2.0 (https://github.com/xldenis/creusot.git#c522ecc2)
       Fresh num-rational v0.3.2
       Fresh creusot-contracts-proc v0.2.0 (https://github.com/xldenis/creusot.git#c522ecc2)
       Fresh creusot-contracts v0.2.0 (https://github.com/xldenis/creusot.git#c522ecc2)
       Dirty essai_creusot v0.1.0 (/home/boulme/RECH/CompilingRust/essai_creusot): the file `src/main.rs` has changed (1695802059.915676378s, 8m 14s after last build at 1695801565.034905316s)
    Checking essai_creusot v0.1.0 (/home/boulme/RECH/CompilingRust/essai_creusot)
     Running `/home/boulme/.cargo/bin/creusot-rustc /home/boulme/.rustup/toolchains/nightly-2023-06-29-x86_64-unknown-linux-gnu/bin/rustc --crate-name essai_creusot --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=147 --crate-type bin --emit=dep-info,metadata -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="contracts"' -C metadata=3145428dcd2ec551 -C extra-filename=-3145428dcd2ec551 --out-dir /home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps -C incremental=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/incremental -L dependency=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps --extern creusot_contracts=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps/libcreusot_contracts-0c4b753e3128d739.rmeta`
thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', creusot/src/cleanup_spec_closures.rs:88:78
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new

there was a panic while trying to force a dep node
try_mark_green dep node stack:
#0 unsafety_check_result(essai_creusot[9586]::foo::{closure#0})
end of try_mark_green dep node stack
there was a panic while trying to force a dep node
try_mark_green dep node stack:
#0 mir_const(essai_creusot[9586]::foo)
#1 mir_promoted(essai_creusot[9586]::foo)
#2 mir_borrowck(essai_creusot[9586]::foo)
end of try_mark_green dep node stack
error: could not compile `essai_creusot` (bin "essai_creusot")

Caused by:
  process didn't exit successfully: `/home/boulme/.cargo/bin/creusot-rustc /home/boulme/.rustup/toolchains/nightly-2023-06-29-x86_64-unknown-linux-gnu/bin/rustc --crate-name essai_creusot --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=147 --crate-type bin --emit=dep-info,metadata -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="contracts"' -C metadata=3145428dcd2ec551 -C extra-filename=-3145428dcd2ec551 --out-dir /home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps -C incremental=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/incremental -L dependency=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps --extern creusot_contracts=/home/boulme/RECH/CompilingRust/essai_creusot/target/debug/deps/libcreusot_contracts-0c4b753e3128d739.rmeta` (exit status: 101)

[jhjourdan]

Wow, that's definitely a bug.

[xldenis]

Yep agreed, I'd love a report with the problematic examples.

[boulme]

Here is the version with @jhjourdan specification: main.rs.gz

My log above gives the commit of Creusot. Is it enough for the bug report ? For the second issue: what are we supposed to put within old ? If arbitrary expressions should be supported, then I expect that old(*c) is semantically equivalent to *old(c) because c is immutable here. In this case, in the file above, just replace instead of *old(c) by old(*c) and you will get another bug, signaled by why3.

[xldenis]

My log above gives the commit of Creusot. Is it enough for the bug report ?

That's perfect

If arbitrary expressions should be supported, then I expect that old(c) is semantically equivalent to old(c) because c is immutable here.

The only thing I can really guarantee works at the moment is captured variable names.