Floating Point Verification Issues

[ifndefJOSH]

I don't know if this is a "bug" so much as a "limitation", but I figured I'd report it here anyway. Take the simple program

from nagini_contracts.contracts import *

def sqr(num : float) -> float:
    Requires(num >= 0)
    Ensures(Result() >= 0)
    Ensures(num * num == Result())
    return num * num

It is evident that num * num > 0.0 will hold (regardless of the sign of num, although we do restrict it to positive numbers), however the Nagini verifier reports:

Verification failed
Errors:
Postcondition of sqr might not hold. Assertion (Result() >= 0) might not hold. (test3.py@5.12)

For comparison, here is a (nearly) equivalent program written in Dafny which does verify:

method Sqr(num : real) returns (n : real)
        requires num >= 0.0
        ensures n >= 0.0
        ensures num * num == n
{
        n := num * num;
}

Now, I'm aware that Dafny's real is not an IEEE floating point type, but Python doesn't seem to natively provide a fixed-point type which can be checked. Perhaps Nagini could detect when the type is a float and indicate this might happen?

[marcoeilers]

Nagini currently treats all floating point operations as uninterpreted functions, i.e., it essentially knows nothing about what they do and therefore cannot prove anything about them.

I've created a branch with experimental support for interpreted floating point values: https://github.com/marcoeilers/nagini/tree/floats
The Nagini version on that branch has an additional command line parameter "--float-encoding=x", where x must be either "real" or "ieee32". So you can verify your example using "--float-encoding=real". Theoretically, "--float-encoding=ieee32" should also work, but reasoning about floating point numbers is incredibly slow, so this may or may not terminate within the next 100 years.

The code isn't properly tested yet, and I'll probably add a warning when uninterpreted floats are used as you suggested.

[marcoeilers]

I tried using the ieee32 option on your example and a few variations and Nagini did actually terminate in ca. 42 minutes, but it could not prove the original example correct. However, this one worked:

def sqr2(num : float) -> float:
    Requires(num >= 0.0)  # 0.0 instead of 0
    Ensures(Result() >= 0.0)  # same here
    Ensures(num * num == Result())
    return num * num

This may mean that I got the encoding from integer literals to floats wrong, or that Z3 is incomplete here; I'll look at it when I have time.

[marcoeilers]

PR #160 is merged now. That means:

• Nagini now outputs a warning when floating point operations are used in the default (uninterpreted floats) mode
• The --float-encoding=real and --float-encoding=ieee32 modes are now available in the main branch.