False negative on multiplication

[Pointerbender]

trafficstars

The following Rust program:

use prusti_contracts::*;

fn main() {}

pub struct A {
    foo: usize,
    bar: usize,
}

predicate! {
    fn invariant(a: &A) -> bool {
        a.foo * a.bar < 256
    }
}

impl A {
    #[pure]
    #[requires(invariant(self))]
    pub const fn test(&self) -> usize {
        self.foo * self.bar
    }
}

fails verification in Prusti with the error message:

error: [Prusti: verification error] assertion might fail with "attempt to multiply with overflow"
  --> src/lib.rs:40:9
   |
40 |         self.foo * self.bar
   |         ^^^^^^^^^^^^^^^^^^^

However, if I open the corresponding Viper file, then Viper IDE successfully verifies the program! There seems to be a discrepancy between invoking Viper through JNI from Prusti and through Viper IDE. This happens on both the release and debug versions of Prusti with overflow checks enabled and a clean cache.

Strangely, this example does verify okay in Prusti:

#[pure]
#[requires(a * b < 256)]
pub const fn multiply(a: usize, b: usize) -> usize {
    a * b
}

Any idea what might be causing this? :)

[vakaras]

Could you check whether setting USE_MORE_COMPLETE_EXHALE setting to false fixes the issue?

[Pointerbender]

Could you check whether setting USE_MORE_COMPLETE_EXHALE setting to false fixes the issue?

Indeed it does!

[Pointerbender]

Are there any known down-sides to setting USE_MORE_COMPLETE_EXHALE to false with Prusti? This work-around seems to work when it is true instead and wondering which work-around to choose :smile:

use prusti_contracts::*;

fn main() {}

pub struct A {
    foo: usize,
    bar: usize,
}

predicate! {
    fn invariant(a: &A) -> bool {
        a.foo * a.bar < 256
    }
}

impl A {
    #[pure]
    #[requires(invariant(self))]
    pub const fn test(&self) -> usize {
        #[pure]
        #[requires(a.foo * a.bar < 256)]
        pub const fn inner(a: &A) -> usize {
            a.foo * a.bar
        }
        inner(self)
    }
}

[Pointerbender]

I've got another example that fails in all cases:

• use_more_complete_exhale = false
• use_more_complete_exhale = true
• both with Prusti and Viper IDE (Viper file)

use prusti_contracts::*;

fn main() {}

const N: usize = 10;

pub struct A {
    foo: usize,
    bar: usize,
}

impl A {
    #[pure]
    #[requires(N + (self.foo - 1) * (self.bar + N) >= 2 * N + 1)]
    #[requires(N + (self.foo - 1) * (self.bar + N) <= isize::MAX as usize)]
    #[ensures(result >= 2 * N + 1)]
    #[ensures(result <= isize::MAX as usize)]
    pub const fn test(&self) -> usize {
        N + (self.foo - 1) * (self.bar + N)
    }
}

fails Prusti with error:

error: [Prusti: verification error] assertion might fail with "attempt to multiply with overflow"
  --> src/lib.rs:56:13
   |
56 |         N + (self.foo - 1) * (self.bar + N)
   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

and in Viper IDE it times out.

Is there another way than #[trusted] to work around this or did I hit some kind of solver limitation/bug? :)

[vakaras]

The problem here is most likely non-linear integer arithmetic, which is undecidable. If #[trusted] is acceptable, I would suggest using it.