crytic
PRBMath SD59x18 and UD60x18 properties
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.
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 properties
SD59x18
- mul_test_associative - The associative property of multiplication,
(x * y) * z == x * (y * z), constrained to a 0.1% allowed error - log10_test_power -
log10(x ** y) == y * log10(x), constrained to a 1% allowed error - pow_test_product_same_base -
x ** a * x ** b == x ** (a+b), constrained to 9 digits of allowed error - pow_test_power_of_an_exponentiation -
(x ** a) ** b == x ** (a * b), constrained to 9 digits of allowed error - inv_test_division_noncommutativity -
x / y == 1 / (y / x), constrained to a 0.1% allowed error - inv_test_identity -
(1 / x) * x == 1, constrained to a 0.1% allowed error - log2_test_power -
log2(x ** y) == y * log2(x), constrained to a 1% allowed error
UD60x18
- mul_test_associative - The associative property of multiplication,
(x * y) * z == x * (y * z), constrained to a 0.1% allowed error - inv_test_division_noncommutativity -
x / y == 1 / (y / x), constrained to a 0.1% allowed error - inv_test_identity -
(1 / x) * x == 1, constrained to a 0.1% allowed error - pow_test_product_same_base -
x ** a * x ** b == x ** (a+b), constrained to 9 digits of allowed error
If you would like to try these yourself you can do so by cloning the dev-prb-v3 branch, installing the dependencies, and running npm run echidna-prb-sd and npm run echidna-prb-ud , it should catch these failures within 100000 runs.
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 no_fail flag turned on, which will ignore Slither failures. Apart from that the properties are exactly the same between v3 and v4.
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 Common.exp2, which affects other functions, e.g. UD60x18.pow.
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!