Improved real float modeling

[PascalDevenoge]

Add support for infinity and NaN values to the real number based float model.

---

This change is 

[PascalDevenoge]

So, the model as written is unsound, as it allows me to coerce the verifier to prove false. I think the problem is about some parts of the __sub__, __mul__ and __eq__ spec, but I'm not entirely sure yet.

[marcoeilers]

Closing parenthesis is in the wrong place, should be after == false, right?

[PascalDevenoge]

Yes, that's definitely a typo. I'll get that fixed...

[marcoeilers]

Same here I believe.

[PascalDevenoge]

Correct

[PascalDevenoge]

So it appears that the main issue was the way I've tested the changes together with the rounding error issue when translating float literals.

The verifier would encounter an assert such as assert 1.2 + 1.3 == 2.5, which due to imprecise representation when translating those floats to ratios will fail verification. When testing, I've had the back-end continue after a failure, so it considers the assertion to be true, and that allowed it to prove false.

I've tried removing the offending assertions and using values with exact representations while keeping all parts involving any special values and the issue goes away.

[marcoeilers]

I think it was the typo in the postcondition? Even if you remove the asserts that didn't pass you could still prove false in the end, or at least I could locally.

[PascalDevenoge]

Oh yes, but I could still make it prove false thanks to the rounding issue (i think...) after fixing the typos.

[PascalDevenoge]

Besides the bug, I've added a contract function isNaN() for convenience, for example to assert that a function parameter is not NaN in a precondition. (Commit 25f28f1) There's a test in float_real/test_float.py as an example.

The cleanest way would have been to model the existing isnan function from the math model. But I guess adding builtin descriptions of standard library functions is not really feasible. Any thoughts?

[marcoeilers]

I think we can merge this now, right?

[PascalDevenoge]

I'd say so, yes.