Inconsistent Assertion Behavior

[norhh]

I encountered an issue where the behavior of two similar assertions is inconsistent. In the code snippet below, the first assertion succeeds, while the second assertion fails during verification, even though they logically seem equivalent.

def make_bigger(n: int) -> int:
  return 2 * n + 1

def check(n: int) -> bool:
    assert 2 * n + 1 != 2
    assert make_bigger(n) != 2
    return True

output:

> nagini --counterexample example.py
Verification failed
Errors:
Assert might fail. Assertion (make_bigger(n) != 2) might not hold. (example.py@7.11--7.30).
Old store:
  n -> False
Old heap: Empty.
Current store:
  n -> False,
  Result() -> ?
Current heap: Empty.

Verification took 6.86 seconds.

The first assertion assert 2 n + 1 != 2 passes, which indicates that 2 n + 1 is not equal to 2. However, the second assertion assert make_bigger(n) != 2 fails, even though make_bigger(n) is defined as 2 * n + 1, which should behave identically to the first assertion.

Could you please explain why this discrepancy occurs? It seems there might be an issue with how the verification tool interprets the function make_bigger(n) compared to the direct expression 2 * n + 1.

[marcoeilers]

Nagini verifies functions modularly, which means that when you verify one function, it does not take the bodies of any other functions it calls into account, only their specifications. In your example, make_bigger does not have any specification, so when verifying check, Nagini knows nothing about the result of the call. You could change that by giving make_bigger a postcondition, e.g.

Ensures(Result() == 2 * n + 1)

or some weaker postcondition like

Ensures(Implies(n > 0, Result() > n))

Or you declare make_bigger to be a pure function using the Pure decorator:

@Pure
def make_bigger(n: int) -> int:
  ...

This works only for side-effect free functions, but it has the effect that the definition of the function is known wherever it is called.

[norhh]

Hi @marcoeilers, thanks for your response. Is there a quick way to check if two functions are equivalent using nagini? Does nagini provide a method of extracting function summaries or something similar? (as that makes it easy to check equivalence)

[marcoeilers]

If they don't have side effects and just compute some result, you can declare them both to be pure, call them, and assert they're the same. Otherwise it's going to be a lot more difficult. No, Nagini does not compute summaries or anything like that.

[norhh]

Thanks for the help!