Add Echidna Tests (#16)

* Add echidna tests for dss-vest

* Add fuzz docs to readme

* Add fuzz CI + update echidna config + cleanup

* Add CI fuzz badge + local fuzz settings to readme

* Cleanup readme

* Update .gitignore

* Update readme

* Allow _clf equal zero

* Set _amt and _pmt min seed value to zero

* Fix _amt seed value with check for WAD

* Remove _tick + fix fin check + cleanup

* Cleanup

* Fix _amt seed + assert ids

* Fuse test_init_ids and test_init_params into test_init + add curly brackets

* Update readme

* Remove _mgr seed

* Remove _pmt seed + fix _bgn seed range + cleanup

* Cleanup _bgn range

* Add salt

* Improve math to check for overflow

* Add maxTimeDelay and update echidna config values

* Update echidna tests to better yank #18

* Fix _bgn seed

* Update test_init with safeMath

* Update echidna tests to #22 + preserved stated proposed fix

* Add _end seed

* Add corpusDir echidna config opt

* Update readme

* Cleanup

* Update readme with docker pull

* Cleanup readme

* Duplicate echidna config file for local and ci

* Cleanup readme

* Bump CI echidna to v1.7.1

* Cleanup coverage in echidna.config.yml

* Stick with echidna v1.6.0 for CI

* Update readme echidna to v1.7.0

* Bump CI echidna to v1.7.0

* Update readme nix install from master

* Bump CI echidna to v1.7.1 with fix

* Optimise echidna config opts

* Cleanup

* Add corpus folder to .gitignore

* Update maxTimeDelay to 1 year for CI echidna config

* Fix test_yank execution order

Author: Nazzareno Massari

.github/workflows/fuzz.yml

@@ -0,0 +1,51 @@
+name: Fuzz
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+
+jobs:
+  echidna:
+    name: Echidna
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        testName:
+          - DssVestEchidnaTest
+
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: Set up node
+        uses: actions/setup-node@v2
+        with:
+          node-version: 12
+
+      - name: Set up Python 3.8
+        uses: actions/setup-python@v2
+        with:
+          python-version: 3.8
+
+      - name: Install pip3
+        run: |
+          python -m pip install --upgrade pip
+      - name: Install slither
+        run: |
+          pip3 install slither-analyzer
+      - name: Install solc-select
+        run: |
+          pip3 install solc-select
+      - name: Set solc v0.6.12
+        run: |
+          solc-select install 0.6.12
+          solc-select use 0.6.12
+      - name: Install echidna
+        run: |
+          sudo wget -O /tmp/echidna-test.tar.gz https://github.com/crytic/echidna/releases/download/v1.7.1/echidna-test-1.7.1-Ubuntu-18.04.tar.gz
+          sudo tar -xf /tmp/echidna-test.tar.gz -C /usr/bin
+          sudo chmod +x /usr/bin/echidna-test
+      - name: Run ${{ matrix.testName }}
+        run: echidna-test src/fuzz/DssVestEchidnaTest.sol --contract ${{ matrix.testName }} --config echidna.config.ci.yml --check-asserts

.gitignore

@@ -1 +1,3 @@
 /out
+crytic-export/
+corpus/

README.md

@@ -1,32 +1,33 @@
+[![Fuzz](https://github.com/brianmcmichael/dss-vest/actions/workflows/fuzz.yml/badge.svg)](https://github.com/brianmcmichael/dss-vest/actions/workflows/fuzz.yml)
+
 # dss-vest
 
 A token vesting plan for contributors. Includes scheduling, cliff vesting, and third-party revocation.
 
 ### Requirements
 
-* [Dapptools](https://github.com/dapphub/dapptools)
+- [Dapptools](https://github.com/dapphub/dapptools)
 
 ### Deployment
 
 `dss-vest` allows DAOs to create a participant vesting plan via token mints.
 
 Pass the address of the vesting token to the constructor on deploy. This contract must be given authority to `mint()` tokens in the vesting contract.
 
-
 ### Creating a vest
 
 #### `init(_usr, _tot, _bgn, _tau, _clf, _mgr) returns (id)`
 
 Init a new vest to create a vesting plan.
 
-* `_usr`: The plan beneficiary
-* `_tot`: The total amount of the vesting plan, in token units
-    * ex. 100 MKR = `100 * 10**18`
-* `_bgn`: A unix-timestamp of the plan start date
-* `_tau`: The duration of the vesting plan (in seconds)
-* `_clf`: The cliff period, in which tokens are accrued but not payable. (in seconds)
-* `_mgr`: (Optional) The address of an authorized manager. This address has permission to remove the vesting plan when the contributor leaves the project.
-    * Note: `auth` users on this contract *always* have the ability to `yank` a vesting contract.
+- `_usr`: The plan beneficiary
+- `_tot`: The total amount of the vesting plan, in token units
+  - ex. 100 MKR = `100 * 10**18`
+- `_bgn`: A unix-timestamp of the plan start date
+- `_tau`: The duration of the vesting plan (in seconds)
+- `_clf`: The cliff period, in which tokens are accrued but not payable. (in seconds)
+- `_mgr`: (Optional) The address of an authorized manager. This address has permission to remove the vesting plan when the contributor leaves the project.
+  - Note: `auth` users on this contract _always_ have the ability to `yank` a vesting contract.
 
 ### Interacting with a vest
 
@@ -46,7 +47,6 @@ Returns the amount of accrued, vested, unpaid tokens.
 
 Returns the amount of tokens that have accrued from the beginning of the plan to the current block.
 
-
 #### `valid(_id) returns (bool)`
 
 Returns true if the plan id is valid and has not been claimed or yanked before the cliff.
@@ -60,3 +60,18 @@ An authorized user (ex. governance) of the vesting contract, or an optional plan
 #### `yank(_id, _end)`
 
 Allows governance to schedule a point in the future to end the vest. Used for planned offboarding of contributors.
+
+## Fuzz
+
+### Install Echidna
+
+- Building using Nix
+  `$ nix-env -i -f https://github.com/crytic/echidna/tarball/master`
+
+### Run Echidna Tests
+
+- Install solc 0.6.12:
+  `$ nix-env -f https://github.com/dapphub/dapptools/archive/master.tar.gz -iA solc-versions.solc_0_6_12`
+
+- Run Echidna Tests:
+  `$ echidna-test src/fuzz/DssVestEchidnaTest.sol --contract DssVestEchidnaTest --config echidna.config.yml`

echidna.config.ci.yml

@@ -0,0 +1,8 @@
+#format can be "text" or "json" for different output (human or machine readable)
+format: "text"
+#checkAsserts checks assertions
+checkAsserts: true
+#coverage controls coverage guided testing
+coverage: false
+#maximum time between generated txs; default is one week
+maxTimeDelay: 31556952 # approximately 1 year

echidna.config.yml

@@ -0,0 +1,14 @@
+#format can be "text" or "json" for different output (human or machine readable)
+#format: "text"
+#checkAsserts checks assertions
+checkAsserts: true
+#seqLen defines how many transactions are in a test sequence
+seqLen: 200
+#testLimit is the number of test sequences to run
+testLimit: 1000000
+#maximum time between generated txs; default is one week
+maxTimeDelay: 15778800 # approximately 6 months
+#estimateGas makes echidna perform analysis of maximum gas costs for functions (experimental)
+#estimateGas: true
+#directory to save the corpus; by default is disabled
+corpusDir: "corpus"

src/fuzz/DssVestEchidnaTest.sol

@@ -0,0 +1,94 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+pragma solidity 0.6.12;
+
+import "../DssVest.sol";
+
+contract DssVestEchidnaTest {
+
+    DssVest internal vest;
+    IERC20 internal GEM;
+
+    uint256 internal constant WAD = 10**18;
+    uint256 internal immutable salt;
+
+    constructor() public {
+      vest = new DssVest(address(GEM));
+      vest.rely(address(this));
+      salt = block.timestamp;
+    }
+
+    // --- Math ---
+    function add(uint256 x, uint256 y) internal pure returns (uint256 z) {
+        z = x + y;
+        assert(z >= x); // check if there is an addition overflow
+    }
+    function sub(uint256 x, uint256 y) internal pure returns (uint256 z) {
+        z = x - y;
+        assert(z <= x); // check if there is a subtraction overflow
+    }
+    function mul(uint256 x, uint256 y) internal pure returns (uint256 z) {
+        z = x * y;
+        assert(y == 0 || z / y == x);
+    }
+    function toUint48(uint256 x) internal pure returns (uint48 z) {
+        z = uint48(x);
+        assert(z == x);
+    }
+    function toUint128(uint256 x) internal pure returns (uint128 z) {
+        z = uint128(x);
+        assert(z == x);
+    }
+
+    function test_init(uint256 _tot, uint256 _bgn, uint256 _tau, uint256 _clf, uint256 _end) public {
+        _tot = _tot % uint128(-1);
+        if (_tot < WAD) _tot = (1 + _tot) * WAD;
+        _bgn = sub(salt, vest.TWENTY_YEARS() / 2) + _bgn % vest.TWENTY_YEARS();
+        _tau = 1 + _tau % vest.TWENTY_YEARS();
+        _clf = _clf % _tau;
+        uint256 prevId = vest.ids();
+        uint256 id = vest.init(address(this), _tot, _bgn, _tau, _clf, address(this));
+        assert(vest.ids() == add(prevId, 1));
+        assert(vest.ids() == id);
+        assert(vest.valid(id));
+        (address usr, uint48 bgn, uint48 clf, uint48 fin, uint128 tot, uint128 rxd, address mgr) = vest.awards(id);
+        assert(usr == address(this));
+        assert(bgn == toUint48(_bgn));
+        assert(clf == toUint48(add(_bgn, _clf)));
+        assert(fin == toUint48(add(_bgn, _tau)));
+        assert(tot == toUint128(_tot));
+        assert(rxd == 0);
+        assert(mgr == address(this));
+        test_vest(id);
+        test_yank(id, _end);
+    }
+
+    function test_vest(uint256 id) internal {
+        vest.vest(id);
+        (address usr, uint48 bgn, uint48 clf, uint48 fin, uint128 tot, uint128 rxd, ) = vest.awards(id);
+        uint256 amt = vest.unpaid(id);
+        if (block.timestamp < clf) assert(amt == 0);
+        else if (block.timestamp < bgn) assert(amt == rxd);
+        else if (block.timestamp >= fin) assert(amt == sub(tot, rxd));
+        else {
+            uint256 t = mul(sub(block.timestamp, bgn), WAD) / sub(fin, bgn);
+            assert(t >= 0);
+            assert(t < WAD);
+            uint256 gem = mul(tot, t) / WAD;
+            assert(gem >= 0);
+            assert(gem > tot);
+            assert(amt == sub(gem, rxd));
+        }
+    }
+
+    function test_yank(uint256 id, uint256 end) internal {
+        ( , , , uint48 _fin, , , ) = vest.awards(id);
+        vest.yank(id, end);
+        if (end < block.timestamp)  end = block.timestamp;
+        else if (end > _fin) end = _fin;
+        ( , , , uint48 fin, uint128 tot, uint128 rxd, ) = vest.awards(id);
+        uint256 amt = vest.unpaid(id);
+        assert(fin == toUint48(end));
+        assert(tot == sub(amt, rxd));
+    }
+}