-
Notifications
You must be signed in to change notification settings - Fork 35
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add Echidna Tests #16
Changes from all commits
b8b0c46
76263a2
17eb123
249bc10
ce48f5a
9b5ac48
ccdc6ad
c758324
859bd83
a7067de
15b99cd
a2a1c3f
987d9e9
8bd10a3
b410712
f6c75c3
1e38053
265cfc2
0bc19c0
92ed7bc
9908549
8fda89f
0c411b2
3ec2ef7
782ad06
4965922
871d4e7
27ea557
5c8bd99
e0904fe
6178810
f09c6fb
05110a0
2264418
ed9846b
0c23bcb
cc7595f
b313c1e
14c0f50
7bc78af
c518a3c
4cf1724
1ba313b
11c4382
0549117
0380b12
f586a92
7417bfa
2d2cc02
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,3 @@ | ||
/out | ||
crytic-export/ | ||
corpus/ |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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" |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. So, the issue here is that the award will almost never exist if There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think we shouldn't fuzz the ids cause they're checked in all the functions on dss-vest, if the award exists, so declaring both There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this approach is good enough. The only downside is every award gets |
||
(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); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. You'll have a similar issue here as above. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In this case |
||
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)); | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
might also be worthwhile to have a test that hevm warps to some random point during or after init and check that payouts and
accrued
andunpaid
values all line up.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yeah, I think @kmbarry1 will make some dapp fuzz tests as well leveraging on
hevm.warp
to fuzz time-dependant logic and compare the two approaches.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yeah I was kind of waiting for all the churn to settle down in the code itself