PRBMath SD59x18 and UD60x18 properties

.gitmodules

@@ -18,3 +18,11 @@
 	path = lib/openzeppelin-contracts
 	url = https://github.com/openzeppelin/openzeppelin-contracts
 	branch = v4.8.0
+[submodule "lib/prb-math"]
+	path = lib/prb-math
+	url = https://github.com/PaulRBerg/prb-math
+	branch = v4
+[submodule "lib/prb-math-v3"]
+	path = lib/prb-math-v3
+	url = https://github.com/PaulRBerg/prb-math
+	branch = v3

CONTRIBUTING.md

@@ -10,7 +10,7 @@ Bug reports and feature suggestions can be submitted to our issue tracker. For b
 
 ## Questions
 
-Questions can be submitted to the issue tracker, but you may get a faster response if you ask in our [chat room](https://empireslacking.herokuapp.com/) (in the #ethereum channel).
+Questions can be submitted to the issue tracker, but you may get a faster response if you ask in our [chat room](https://slack.empirehacking.nyc/) (in the #ethereum channel).
 
 ## Code
 

README.md

@@ -7,6 +7,7 @@
     - [ERC721 Tests](#erc721-tests)
     - [ERC4626 Tests](#erc4626-tests)
     - [ABDKMath64x64 tests](#abdkmath64x64-tests)
+    - [PRBMath tests](#prbmath-tests)
   - [Additional resources](#additional-resources)
 - [Helper functions](#helper-functions)
   - [Usage examples](#usage-examples)
@@ -26,6 +27,7 @@ This repository contains 168 code properties for:
 - [ERC721](https://ethereum.org/en/developers/docs/standards/tokens/erc-721/) token: mintable, burnable, and transferable invariants ([19 properties](PROPERTIES.md#erc721)).
 - [ERC4626](https://ethereum.org/en/developers/docs/standards/tokens/erc-4626/) vaults: strict specification and additional security invariants ([37 properties](PROPERTIES.md#erc4626)).
 - [ABDKMath64x64](https://github.com/abdk-consulting/abdk-libraries-solidity/blob/master/ABDKMath64x64.md) fixed-point library invariants ([106 properties](PROPERTIES.md#abdkmath64x64)).
+- [PRBMath](https://github.com/PaulRBerg/prb-math/blob/main/README.md) fixed-point library invariants ([132 properties](PROPERTIES.md#prbmath-sd59x18)) for SD59x18, and ([96 properties](PROPERTIES.md#prbmath-ud60x18)) for UD60x18.
 
 The goals of these properties are to:
 
@@ -47,6 +49,7 @@ The properties can be used through unit tests or through fuzzing with [Echidna](
    - [ERC20 tests](#erc20-tests)
    - [ERC4626 test](#erc4626-tests)
    - [ABDKMath64x64 tests](#abdkmath64x64-tests)
+   - [PRBMath tests](#prbmath-tests)
 
 ### ERC20 tests
 
@@ -414,10 +417,48 @@ contract CryticABDKMath64x64Harness is CryticABDKMath64x64PropertyTests {
 
 Run the test suite using `echidna . --contract CryticABDKMath64x64Harness --seq-len 1 --test-mode assertion --corpus-dir tests/echidna-corpus` and inspect the coverage report in `tests/echidna-corpus` when it finishes.
 
+### PRBMath tests
+
+The Solidity smart contract programming language does not have any inbuilt feature for working with decimal numbers, so for contracts dealing with non-integer values, a third party solution is needed. [PRBMath](https://github.com/PaulRBerg/prb-math) is Solidity library for advanced fixed-point math that operates with signed 59.18-decimal fixed-point and unsigned 60.18-decimal fixed-point numbers
+
+SD59x18 library implements [19 arithmetic operations](https://github.com/PaulRBerg/prb-math/blob/main/README.md#mathematical-functions "19 arithmetic operations") using fixed-point numbers and [11 conversion functions](https://github.com/PaulRBerg/prb-math/blob/main/README.md#mathematical-functions "6 conversion functions") between integer types and fixed-point types.
+
+We provide a number of tests related with fundamental mathematical properties of the floating point numbers. To include these tests into your repository, follow these steps:
+
+1. [Integration](#integration-4)
+2. [Run](#run-4)
+
+
+#### Integration
+
+Create a new Solidity file containing the `PRBMathSD59x18Harness` or `PRBMath60x18Harness` contract:
+
+```Solidity
+pragma solidity ^0.8.0;
+import "@crytic/properties/contracts/Math/PRBMath/v3/PRBMathSD59x18PropertyTests.sol;
+
+contract CryticPRBMath59x18Harness is CryticPRBMath59x18Propertiesv3 {
+    /* Any additional test can be added here */
+}
+```
+
+```Solidity
+pragma solidity ^0.8.0;
+import "@crytic/properties/contracts/Math/PRBMath/v3/PRBMathSD60x18PropertyTests.sol;
+
+contract CryticPRBMath60x18Harness is CryticPRBMath60x18Propertiesv3 {
+    /* Any additional test can be added here */
+}
+```
+
+#### Run
+
+Run the test suite using `echidna-test . --contract CryticPRBMath59x18Harness --seq-len 1 --test-mode assertion --corpus-dir tests/echidna-corpus` and inspect the coverage report in `tests/echidna-corpus` when it finishes.
+
 ## Additional resources
 
 - [Building secure contracts](https://secure-contracts.com/program-analysis/index.html)
-- Our [EmpireSlacking](https://empireslacking.herokuapp.com/) slack server, channel #ethereum
+- Our [EmpireSlacking](https://slack.empirehacking.nyc/) slack server, channel #ethereum
 - Watch our [fuzzing workshop](https://www.youtube.com/watch?v=QofNQxW_K08&list=PLciHOL_J7Iwqdja9UH4ZzE8dP1IxtsBXI)
 
 # Helper functions

contracts/Math/PRBMath/README.md

@@ -0,0 +1,36 @@
+# PRBMath test suite for Echidna
+
+## What is PRBMath?
+
+The Solidity smart contract programming language does not have any inbuilt feature for working with decimal numbers, so for contracts dealing with non-integer values, a third party solution is needed. PRBMath is a fixed-point arithmetic Solidity library that operates on signed 59x18-decimal fixed-point and unsigned 60.18-decimal fixed-point numbers. This library was developed by [Paul Razvan Berg](https://github.com/PaulRBerg "Paul Razvan Berg") and is [open source](https://github.com/PaulRBerg/prb-math "open source") under the MIT License.
+
+## Why are tests needed?
+
+Solidity libraries are used in smart contracts that at some point in time can hold important value in tokens or other assets. The security of those assets is directly related to the robustness and reliability of the smart contract source code.
+
+While testing does not guarantee the absence of errors, it helps the developers in assessing what the risky operations are, how they work, and ultimately how can they fail. Furthermore, having a working test suite with common and edge cases is useful to ensure that code does not behave unexpectedly, and that future versions of the library do not break compatibility.
+
+Echidna testing can be integrated into CI/CD pipelines, so bugs are caught early and the developers are notified about security risks in their contracts.
+
+## Who are these tests designed for?
+
+In principle, these tests are meant to be an entry level practice to learn how to use Echidna for assertion-based fuzz tests, targeting a stand-alone library. It is a self contained exercise that shows how to determine the contract invariants, create proper tests, and configure the relevant Echidna parameters for the campaign.
+
+Determining the invariants is a process that involves an intermediate-level comprehension of the library and the math properties behind the operations implemented. For example, the addition function has the `x+y == y+x` commutative property. This statement should always be true, no matter the values of `x` and `y`, therefore it should be a good invariant for the system. More complex operations can demand more complex invariants.
+
+The next step, creating the tests, means to implement Solidity functions that verify the previously defined invariants. Echidna is a fuzz tester, so it can quickly test different values for the arguments of a function. For example, the commutative property can be tested using a function that takes two parameters and performs the additions, as shown below:
+
+```solidity
+// Test for commutative property
+// x + y == y + x
+function add_test_commutative(SD59x18 x, SD59x18 y) public pure {
+  SD59x18 x_y = x.add(y);
+  SD59x18 y_x = y.add(x);
+
+  assert(x_y.eq(y_x));
+}
+```
+
+Finally, the fuzzer has to be instructed to perform the correct type of test, the number of test runs to be made, among other configuration parameters. Since the invariant is checked using an assertion, Echidna must be configured to try to find assertion violations. In this mode, different argument values are passed to `add_test_commutative()`, and the result of the `assert(x_y == y_x)` expression is evaluated for each call: if the assertion is false, the invariant was broken, and it is a sign that there can be an issue with the library implementation.
+
+However, even if this particular test suite is meant as an exercise, it can be used as a template to create tests for other fixed-point arithmetic libraries implementations.