Add Echidna Tests

.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.6.0/echidna-test-v1.6.0-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.yml

.gitignore

@@ -1 +1,2 @@
 /out
+crytic-export/

README.md

@@ -1 +1,55 @@
+[![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
+
+## Fuzz
+
+### Install Echidna
+
+- Building using Nix
+  `$ nix-env -i -f https://github.com/crytic/echidna/tarball/master`
+
+- Building using Docker
+  `$ docker build -t echidna .`
+
+Then, run via:
+`docker run -it -v`pwd`:/src echidna echidna-test /src/fuzz/DssVestEchidnaTest.sol`
+
+- Precompiled Binaries
+
+Before starting, make sure Slither is installed:
+`$ pip3 install slither-analyzer`
+
+To quickly test Echidna in Linux or MacOS:
+[release page](https://github.com/crytic/echidna/releases)
+
+### Local Dependencies
+
+- Slither
+  `$ pip3 install slither-analyzer`
+
+- solc-select
+  `$ pip3 install solc-select`
+
+### Local Fuzz Settings
+
+- Edit `echidna.config.yml`
+- Comment `format: "text"`
+- Set `coverage` to true
+- Uncomment `seqLen`
+- Uncomment `testLimit`
+- Uncomment `estimateGas` (optional)
+
+### Run Echidna Tests
+
+- Install solc version:
+  `$ solc-select install 0.6.12`
+
+- Select solc version:
+  `$ solc-select use 0.6.12`
+
+- If using Dapp Tools:
+  `$ 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.yml

@@ -0,0 +1,12 @@
+#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
+#seqLen defines how many transactions are in a test sequence
+#seqLen: 50
+#testLimit is the number of test sequences to run
+#testLimit: 100000
+#estimateGas makes echidna perform analysis of maximum gas costs for functions (experimental)
+#estimateGas: true

src/fuzz/DssVestEchidnaTest.sol

@@ -0,0 +1,82 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+pragma solidity 0.6.12;
+
+import "../DssVest.sol";
+
+contract DssVestEchidnaTest {
+
+    DssVest internal vest;
+    IMKR internal MKR;
+
+    constructor() public {
+      vest = new DssVest(address(MKR));
+    }
+
+    // --- Math ---
+
+    uint256 internal constant WAD = 10**18;
+
+    function add(uint256 x, uint256 y) internal pure returns (uint256 z) {
+        require((z = x + y) >= x);
+    }
+    function sub(uint256 x, uint256 y) internal pure returns (uint256 z) {
+        require((z = x - y) <= x);
+    }
+
+    function test_init_ids(uint256 _amt, uint256 _bgn, uint256 _tau, uint256 _clf, uint256 _pmt, address _mgr) public {
+        _amt = 1 * WAD + _amt % uint128(-1);
+        _bgn = block.timestamp + _bgn % vest.MAX_VEST_PERIOD();
+        _tau = 1 + _tau % vest.MAX_VEST_PERIOD();
+        _clf = 1 + _clf % _tau;
+        _pmt = 1 * WAD + _pmt % _amt;
+        uint256 prevId = vest.ids();
+        uint256 id = vest.init(address(this), _amt, _bgn, _tau, _clf, _pmt, _mgr);
+        assert(vest.ids() == add(prevId, id));
+        assert(vest.valid(id));
+    }
+
+    function test_init_params(uint256 _amt, uint256 _bgn, uint256 _tau, uint256 _clf, uint256 _pmt, address _mgr) public {
+        _amt = 1 * WAD + _amt % uint128(-1);
+        _bgn = block.timestamp + _bgn % vest.MAX_VEST_PERIOD();
+        _tau = 1 + _tau % vest.MAX_VEST_PERIOD();
+        _clf = 1 + _clf % _tau;
+        _pmt = 1 * WAD + _pmt % _amt;
+        uint256 id = vest.init(address(this), _amt, _bgn, _tau, _clf, _pmt, _mgr);
+        (address usr, uint48 bgn, uint48 clf, uint48 fin, uint128 amt, uint128 rxd, address mgr) = vest.awards(id);
+        if (sub(_amt, _pmt) != 0) {
+            assert(usr == (address(this)));
+            assert(bgn == uint48(_bgn));
+            assert(clf == add(_bgn, _clf));
+            assert(fin == add(_bgn, _tau));
+            assert(amt == sub(_amt, _pmt));
+            assert(rxd == uint128(0));
+            assert(mgr == _mgr);
+        }
+    }
+
+    function test_vest(uint256 _amt, uint256 _bgn, uint256 _tau, uint256 _clf, uint256 _pmt, address _mgr, uint256 _tick) public {
+        _amt = 1 * WAD + _amt % uint128(-1);
+        _bgn = block.timestamp + _bgn % vest.MAX_VEST_PERIOD();
+        _tau = 1 + _tau % vest.MAX_VEST_PERIOD();
+        _clf = 1 + _clf % _tau;
+        _pmt = 1 * WAD + _pmt % _amt;
+        _tick = block.timestamp + _tick % uint128(-1);
+        uint256 id = vest.init(address(this), _amt, _bgn, _tau, _clf, _pmt, _mgr);
+        assert(vest.valid(id));
+        uint256 ids = vest.ids();
+        vest.vest(id);
+        (address usr, uint48 bgn, uint48 clf, uint48 fin, uint128 amt, uint128 rxd, address mgr) = vest.awards(id);
+        if (_tick < fin) {
+          assert (vest.ids() == sub(ids, 1));
+        } else if (_tick >= clf) {
+          uint256 t = (_tick - bgn) * WAD / (fin - bgn);
+          assert(t >= 0);
+          assert(t < WAD);
+          uint256 mkr = (amt * t) / WAD;
+          assert(mkr >= 0);
+          assert(mkr < amt);
+          assert(rxd == uint128(mkr));
+        }
+    }
+}