Verification successful when it should fail

[nielstron]

The following code

from nagini_contracts.contracts import *

def gcd(a: int, b: int) -> int:
    Ensures(a % Result() == 0)
    Ensures(b % Result() == 0)
    while b != 0:
        Invariant(False)
        Invariant((b % a) == 0)
        a, b = b, 4
    return abs(a)

Should IMO definitely fail, but still:

(venv) ➜  opshin git:(feat/nagini) nagini opshin/std/math.py
Verification successful
Verification took 5.80 seconds.

I simply followed the instructions to pip install nagini and then run the command on Ubuntu 22 LTS Python 3.8.16

[nielstron]

Trying to narrow it down I get to this being verifiable

from nagini_contracts.contracts import *

def gcd(a: int, b: int) -> int:
    Ensures(False)
    return a

UPDATE my current minimal example (False also works but this looks wrong much more obviously)

def foo(a: int) -> int:
    Ensures(a != Result())
    return a

[marcoeilers]

I can't reproduce this. For the original example (with Python 3.8 and just pip install nagini), I get

Verification failed
Errors:
The precondition of (a % Result()) might not hold.  (huh.py@4.12)

For the last minimal example, I get

Verification failed
Errors:
Postcondition of foo might not hold. Assertion (a != Result()) might not hold. (huh.py@4.12)
Verification took 6.40 seconds.

[nielstron]

Ah yes my bad, I was actually checking the wrong file... (in a mirrored directory)

That said, I am now also getting The precondition of (a % Result()) might not hold. (huh.py@4.12) - this is a bit confusing as I have not specified a precondition? I am assuming it points to another error (which may or may not be that the _post_condition is wrong). Do you know what this error message points to?

[nielstron]

Okay I think I found it - it points to a potentially being 0, which I assume is translated somewhere into a precondition for ... % Result().

[marcoeilers]

Nagini checks for all divisions and modulo operations that the second argument is not zero - those are implicit preconditions of division and modulo. I agree the error should be clearer. So you could fix that by writing Ensures(Result() != 0 and ...)