PRBMath SD59x18 and UD60x18 properties #30
Conversation
tuturu-tech
requested review from
glarregay-tob,
bsamuels453,
montyly and
ggrieco-tob
as code owners
|
Hey @PaulRBerg, we've created a draft set of properties testing mathematical invariants of your PRBMath v3 library and wanted to get your input on a couple of failing properties. Both the SD59x18 and UD60x18 libraries have properties that are failing (full list below), however, without performing a full audit of the code it is difficult to ascertain if the failures are due to incorrectly defined allowed error bounds in the properties, or if they indicate a bug in the library implementation. It would be useful if you could help us define the correct allowed error bounds for the various operations so that the properties are not over- or under-constraining the allowed errors. Failing propertiesSD59x18
UD60x18
If you would like to try these yourself you can do so by cloning the dev-prb-v3 branch, installing the dependencies, and running |
|
Thank you SO MUCH for doing this, guys! I will review this in detail in a few weeks, but I want to mention upfront that it would be super duper helpful to target V4 instead of V3. As per the release notes, V4 contains a fix for an important bug that affected all V3 releases. There have been few API changes between V3 and V4, so upgrading should be easy. |
|
Thank you for the quick reply! We opted for targeting v3 since Slither does not (yet) work with user defined operators used in v4. That said, I've just added v4 properties with the caveat that they only work with the Slither |
|
Oh, yes, I forgot that Slither doesn't support operators just yet. In this case, it should be fine to keep targeting V3 for a while, though we should keep in mind that a bug exists in |
There was a problem hiding this comment.
I tried going through a few of the failure cases I saw using echidna 2.2.0. Some of these differed from the ones reported in an earlier comment:
inv_test_double_inversepow_test_high_exponentmul_test_associativesqrt_test_squareinv_test_multiplicationlog10_test_powerinv_test_identitypow_test_product_same_basepow_test_power_of_an_exponentiationinv_test_division_noncommutativitylog2_test_power
There's a learning curve to getting ramped up on this stuff. I felt like I needed more time to provide more insight. On my next IRAD, perhaps I can come back to this review and actually solve some of these failures.
| int256 la = convert(floor(log10(abs(a)))); | ||
| int256 lb = convert(floor(log10(abs(b)))); | ||
| // digits left | ||
| int256 prec = la + lb; |
There was a problem hiding this comment.
This prec is assigned but never used?
There was a problem hiding this comment.
This function is implicated in several of the failures I reviewed. Needs more investigation.
| SD59x18 double_inv_x = inv(inv(x)); | ||
|
|
||
| // The maximum loss of precision will be 2 * log2(x) bits rounded up | ||
| uint256 loss = 2 * significant_digits_lost_in_mult(x, x)+ 2; |
There was a problem hiding this comment.
This property is failing in 2.2.0 echinda. The expectation that significant_digits_lost_in_mult(x, x) is going to calculate the expected precision, given the input, appears to be wrong. Maybe the function isn't working as expected because I think it's just returning 0 every time (or at least in cases where it's not supposed to), which means it's always expecting 2 digits of precision. I changed the end of the equation to add 3, and then 4, and it took longer and longer to find a failure, but always reported it was looking for 2, 3, 4 digits of precision depending on what I changed that value to before the run.
There was a problem hiding this comment.
The issue might be that we're not taking into consideration the precision loss of the division, so doing significant_digits_lost_in_mult(x, inv(x)) might solve this
|
|
||
| SD59x18 result = pow(x, a); | ||
|
|
||
| assertEq(result, ZERO_FP); |
There was a problem hiding this comment.
This fails because it's returning 1e18, so I suspect it's rounding up instead of down. This might have something to do with a bug in the exp2 function of PRBMath v3.
|
|
||
| uint256 digitsLost = significant_digits_lost_in_mult(x, y); | ||
| digitsLost += significant_digits_lost_in_mult(x, z); | ||
|
|
There was a problem hiding this comment.
What about the digits lost multiplying y and z? We might need to add another digitsLost += significant_digits_lost_in_mult(y, z); to get this to work.
| // log10(x ** y) = y * log10(x) | ||
| function log10_test_power(SD59x18 x, SD59x18 y) public { | ||
| require(x.gt(ZERO_FP) && y.gt(ZERO_FP)); | ||
| SD59x18 x_y = pow(x, y); |
There was a problem hiding this comment.
Failing test case was very close to what was expected. Had the tolerance to be off by 1, but was off by 2. Could be an issue with the exp2 function bug that effects pow in v3.
|
Guys just wanted to say that unfortunately I am tied up with my work (on Sablier V2), and I cannot find any time to provide a proper review here. I'm sorry, but I am also very grateful that you wrote these fuzz tests for PRBMath. Thank you! |
Used the ABDKMath properties as a base to create properties for SD59x18 (118 properties) and UD60x18 (90 properties), covering all math functions except for: gm, floor, ceil, frac.