Document well-definedness of specifications

[safinaskar]

Consider this code:

#[requires(a + b == c)]
pub fn f(a: i32, b: i32, c: i32) {
}

What is its semantics? a + b doesn't always have meaning, because a + b may overflow. So, what is intended semantics of this code? Is it true that above code is equivalent to this hypothetical code?

// Pseudocode
#[requires(has_meaning(a + b))]
#[requires(a + b == c)]
pub fn f(a: i32, b: i32, c: i32) {
}

Please, document this. Same applies to other situations when code has no meaning (for example, out of range) and all constructs recognized by prusti (assert, body_invariant, etc)

[fpoli]

In Prusti the well-definedness of the specification is an implicit requirement. So, it's like in your second example. In the case of preconditions, each call of f(...) will check that the arguments are such that there are no overflows in the precondition. Thanks for pointing out that this is not described in the user guide. I think it should go at least in docs/user-guide/src/verify/prepost.md, or in a place that also covers invariants etc.

[fpoli]

One way to explain it is that every operation (sum of integers, array lookup, ...) adds a condition that ensures that executing the operation would not panic if executed in debug mode. This makes it easy to reuse or copy-paste code between specifications and executable code, because the semantics is the same.

Regarding assert!(a + b == c);, it's equivalent to let x = a + b == c; assert!(x);. Specifications are not involved there; it's just executable code that is checked to have no panics/overflows at runtime.

[safinaskar]

@fpoli . To which of these two fragments prusti_assume!(a + b == c) equivalent to?

// A
prusti_assume!(defined(a + b));
prusti_assume!(a + b == c);

// B
prusti_assert!(defined(a + b));
prusti_assume!(a + b == c);

And to which of these two fragments prusti_assert!(a + b == c) equivalent to?

// C
prusti_assume!(defined(a + b));
prusti_assert!(a + b == c);

// D
prusti_assert!(defined(a + b));
prusti_assert!(a + b == c);

[fpoli]

For prusti_assert! the only sound choice is D. If you notice otherwise, it's a bug.

Regarding prusti_assume!, it is currently implemented as A, but we are discussing to switch to B in the future.

[safinaskar]

@fpoli , thanks a lot! Please, add this to documentation.

but we are discussing to switch to B in the future

I agree this would be good decision.

I think in ideal world addition should take as an implicit argument proof object stating that there is no overflow. From this point of view, of course, B is correct and A is not (because A essentially means that we have no proof object, and we simply assume it exists.)

Now consider this:

prusti_assert!(b != 0 ==> a / b == c);

I hope prusti_assert!(b != 0) is not implicitly inserted before this statement, right?

[fpoli]

Yes, prusti_assert!(b != 0 ==> a / b == c); implicitly requires b != 0 ==> defined(a / b) to hold, which is a tautology.

[safinaskar]

@fpoli . Ok, this is good that it is not inserted. Now consider this:

// E
prusti_assert!(a / b == c ==> d + e == f);

Is this equivalent to this?

// F
prusti_assert!(b != 0);
prusti_assert!(a / b == c ==> d + e == f);

I hope answer is yes

[fpoli]

Yes, like in F. The general rule is that the requirement of every operation is checked to hold under the condition that the operation is reached.

This is also why

use prusti_contracts::*;
fn test(b: u32) {
  prusti_assert!(true || 10 / b == 10 / b);
}

verifies but

use prusti_contracts::*;
fn test(b: u32) {
  prusti_assert!(10 / b == 10 / b || true);
}

does not verify. In the first case the short-circuit evaluation of || doesn't execute the division.

[safinaskar]

@fpoli . Thanks a lot. Is this

// G
prusti_assert!((b != 0 && a / b == c) ==> d + e == f);

equivalent to this:

// H
prusti_assert!(b != 0);
prusti_assert!((b != 0 && a / b == c) ==> d + e == f);

? And is this

// I
prusti_assert!((a / b == c && b != 0) ==> d + e == f);

equivalent to this

// J
prusti_assert!(b != 0);
prusti_assert!((a / b == c && b != 0) ==> d + e == f);

? I think that "I" should be equivalent to J and G should not be equivalent to H. I think so because of my proof object interpretation

[fpoli]

Yes, I think the same. G succeeds when b == 0, but H fails. Both I and J fail on b == 0 and agree on the b != 0 requirement.

[safinaskar]

@fpoli . Thanks a lot! I hope you will add some of this to documentation and possibly tests