diff --git a/PROPERTIES.md b/PROPERTIES.md index c24d8ae..063dd83 100644 --- a/PROPERTIES.md +++ b/PROPERTIES.md @@ -227,7 +227,7 @@ This file lists all the currently implemented Echidna property tests for ERC20, | ABDKMATH-071 | [pow_test_base_one](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1290) | One to the power of any number should be one. | | ABDKMATH-072 | [pow_test_product_same_base](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1298) | Product of powers of the same base property | | ABDKMATH-073 | [pow_test_power_of_an_exponentiation](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1310) | Power of an exponentiation property | -| ABDKMATH-074 | [pow_test_product_same_base](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1322) | Distributive property for power of a product | +| ABDKMATH-074 | [pow_test_distributive](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1322) | Distributive property for power of a product | | ABDKMATH-075 | [pow_test_values](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1336) | Power result should increase or decrease (in absolute value) depending on exponent's absolute value. | | ABDKMATH-076 | [pow_test_sign](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1352) | Power result sign should change according to the exponent sign. | | ABDKMATH-077 | [pow_test_maximum_base](https://github.com/crytic/properties/blob/main/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol#L1382) | Power edge case: Power of the maximum value should revert if exponent > 1. | diff --git a/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol b/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol index 050b970..efa58fd 100644 --- a/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol +++ b/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol @@ -1312,9 +1312,9 @@ contract CryticABDKMath64x64Properties { assert(equal_within_precision(x_a_b, x_ab, 2)); } - // Test for power of a product + // Test for distributive property for power of a product // (x * y) ** a == x ** a * y ** a - function pow_test_product_same_base( + function pow_test_distributive( int128 x, int128 y, uint256 a