Fix documentation for pow_test_distributive

In `CryticABDKMath64x64Properties`, two functions had the same name, `pow_test_product_same_base`, while clearly one was not referring to the product of the same base. Instead, one of the functions referred to the distributive property of the exponentiation.
crytic · Sep 27, 2023 · d573bf6 · d573bf6
1 parent c25de70
commit d573bf6
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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