[Bug-Candidate]: ABDKMath64x64PropertyTests.sol: Tests output false negatives about properties

[glarregay-tob]

Hey, thanks for your submission!
This is an interesting point. I'll test this and the PR locally and get back to you.

[glarregay-tob]

Hey @beber89, sorry for the delay. I ran some tests on this issue, thanks again for bringing it up.

The way that the add and sub functions are implemented in ABDKMath64x64 make the add_test_range and sub_test_range tests to be unnecesary, as you stated. This is due to the fact that ABDKMath's implementations of add and sub are using type casting from int256 to int128, and in the case where the result doesn't fit, the implementation just drops the higher order bits. In summary, there is no way it can overflow, as the result will always be in int128 range, and it is exactly the same range as the valid results.

Your PR addresses a condition that we weren't directly checking, that is overflow. I mean "directly" in the sense that if those functions were to overflow, the issue would be quite probably detected by the other failing tests that you mentioned in your report (add_test_values, add_test_maximum_value_plus_one, etc), but there is no specific test for it with fuzzable parameters.

Another point is that even if the math tests are now tailored to ABDKMath64x64, they are meant to be reusable for other libraries too. So we shouldn't assume that all libraries will implement overflow checks the same way, tests should be created for them. I think the overflow test you implemented can be useful in the cases where the valid result range is different than the underlying type range (for example, a 32x32 fixed point lib implemented with int128 as underlying). I am not aware if such libraries exist, though.

So, in summary, I think we can add your suggestions to the repo as a new overflow test. Before defining how it should be implemented, I'd like to read your opinion on this @ggrieco-tob.

[beber89]

Hey @glarregay-tob , sorry for all that time it took me to respond.

I wrote that test based on the fact that the require statement applied on int128 is not actually checking anything and I assumed that testing for overflow/underflow can be seen as checking that the value is confined within the int128 range afterall.

But I got your point now, I understand that the pull request which I am suggesting looks like it tests a different thing. It can be a general overflow/underflow test but not a range test. I had another idea also then but it still contradicts the purpose of the test I think as this one.

I think the overflow test you implemented can be useful in the cases where the valid result range is different than the underlying type range (for example, a 32x32 fixed point lib implemented with int128 as underlying). I am not aware if such libraries exist, though.

I took a look but I could not find a library among the ones I know that does this .