diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 9dac7145..99da437e 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -32,6 +32,9 @@ jobs: - name: Install solc-select run: pip3 install solc-select + - name: Solc Select 0.5.12 + run: solc-select install 0.5.12 + - name: Solc Select 0.6.12 run: solc-select install 0.6.12 diff --git a/Makefile b/Makefile index 710a2761..b6f422b6 100644 --- a/Makefile +++ b/Makefile @@ -1,13 +1,14 @@ +PATH := ~/.solc-select/artifacts/solc-0.6.12:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:$(PATH) all :; DAPP_BUILD_OPTIMIZE=1 DAPP_BUILD_OPTIMIZE_RUNS=200 dapp --use solc:0.6.12 build clean :; dapp clean && rm -rf crytic-export corpus test :; ./test.sh match="$(match)" block="$(block)" match-test="$(match-test)" match-contract="$(match-contract)" -solc-select :; pip3 install solc-select && solc-select install 0.6.12 +solc-select :; pip3 install solc-select && solc-select install 0.5.12 && solc-select install 0.6.12 echidna-mintable :; ./echidna/echidna.sh mintable echidna-suckable :; ./echidna/echidna.sh suckable echidna-transferrable :; ./echidna/echidna.sh transferrable -certora-mintable :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/solc-0.6.12 src/DssVest.sol:DssVestMintable certora/DSToken.sol certora/MockAuthority.sol --link DssVestMintable:gem=DSToken DSToken:authority=MockAuthority --verify DssVestMintable:certora/DssVestMintable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity $(if $(rule),--rule $(rule),) --multi_assert_check --short_output -certora-suckable :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/solc-0.6.12 src/DssVest.sol:DssVestSuckable certora/ChainLog.sol certora/Vat.sol certora/DaiJoin.sol certora/Dai.sol --link DssVestSuckable:chainlog=ChainLog DssVestSuckable:vat=Vat DssVestSuckable:daiJoin=DaiJoin DaiJoin:vat=Vat DaiJoin:dai=Dai --verify DssVestSuckable:certora/DssVestSuckable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity $(if $(rule),--rule $(rule),) --multi_assert_check --short_output -certora-transferrable :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/solc-0.6.12 src/DssVest.sol:DssVestTransferrable certora/Dai.sol --link DssVestTransferrable:gem=Dai --verify DssVestTransferrable:certora/DssVestTransferrable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity $(if $(rule),--rule $(rule),) --multi_assert_check --short_output +certora-mintable :; PATH=${PATH} certoraRun certora/DssVestMintable.conf $(if $(rule), --rule $(rule),) +certora-suckable :; PATH=${PATH} certoraRun certora/DssVestSuckable.conf $(if $(rule), --rule $(rule),) +certora-transferrable :; PATH=${PATH} certoraRun certora/DssVestTransferrable.conf $(if $(rule), --rule $(rule),) deploy-mintable :; make && dapp create DssVestMintable $(gem) deploy-suckable :; make && dapp create DssVestSuckable 0xdA0Ab1e0017DEbCd72Be8599041a2aa3bA7e740F deploy-transferrable :; make && dapp create DssVestTransferrable $(owner) $(gem) diff --git a/README.md b/README.md index c4e4bf97..21113495 100644 --- a/README.md +++ b/README.md @@ -32,7 +32,9 @@ After deployment, governance must set the `cap` value using the `file` function. #### DssVestSuckable -Pass the MCD [chainlog](https://github.com/makerdao/dss-chain-log) address to the constructor to set up the contract for scheduled Dai `suck`s. Note: this contract must be given authority to `suck()` Dai from the `vat`'s surplus buffer. +Pass the MCD [chainlog](https://github.com/makerdao/dss-chain-log) address to the constructor to set up the contract for scheduled Dai or USDS `suck`s. Note: this contract must be given authority to `suck()` Dai from the `vat`'s surplus buffer. + +To choose between Dai and USDS, supply the relevant join (`MCD_JOIN_DAI` or `USDS_JOIN`) as the `address _join` constructor parameter. A `vat.live` check is introduced to disable `vest()` in the event of Emergency Shutdown (aka Global Settlement). diff --git a/certora/DssVestMintable.conf b/certora/DssVestMintable.conf new file mode 100644 index 00000000..682a5e92 --- /dev/null +++ b/certora/DssVestMintable.conf @@ -0,0 +1,25 @@ +{ + "verify": "DssVestMintable:certora/DssVestMintable.spec", + "parametric_contracts": [ + "DssVestMintable" + ], + "files": [ + "src/DssVest.sol:DssVestMintable", + "certora/harness/DSToken.sol", + "certora/harness/MockAuthority.sol" + ], + "solc": "solc-0.6.12", + "solc_optimize_map": { + "DssVestMintable": "200", + "DSToken": "0", + "MockAuthority": "0" + }, + "link": [ + "DssVestMintable:gem=DSToken", + "DSToken:authority=MockAuthority" + ], + "build_cache": true, + "rule_sanity": "basic", + "multi_assert_check": true, + "wait_for_results": "all" +} diff --git a/certora/DssVestMintable.spec b/certora/DssVestMintable.spec index 67eab95a..41ca972d 100644 --- a/certora/DssVestMintable.spec +++ b/certora/DssVestMintable.spec @@ -1,53 +1,48 @@ // DssVestMintable.spec -// certoraRun src/DssVest.sol:DssVestMintable certora/DSToken.sol certora/MockAuthority.sol --link DssVestMintable:gem=DSToken DSToken:authority=MockAuthority --verify DssVestMintable:certora/DssVestMintable.spec --rule_sanity - -using DSToken as token -using MockAuthority as authority +using DSToken as token; +using MockAuthority as authority; methods { - TWENTY_YEARS() returns (uint256) envfree - wards(address) returns (uint256) envfree - awards(uint256) returns (address, uint48, uint48, uint48, address, uint8, uint128, uint128) envfree - ids() returns (uint256) envfree - cap() returns (uint256) envfree - usr(uint256) returns (address) envfree - bgn(uint256) returns (uint256) envfree - clf(uint256) returns (uint256) envfree - fin(uint256) returns (uint256) envfree - mgr(uint256) returns (address) envfree - res(uint256) returns (uint256) envfree - tot(uint256) returns (uint256) envfree - rxd(uint256) returns (uint256) envfree - valid(uint256) returns (bool) envfree - gem() returns (address) envfree - token.authority() returns (address) envfree - token.owner() returns (address) envfree - token.stopped() returns (bool) envfree - token.totalSupply() returns (uint256) envfree - token.balanceOf(address) returns (uint256) envfree -} - -definition max_uint48() returns uint256 = 2^48 - 1; + function TWENTY_YEARS() external returns (uint256) envfree; + function wards(address) external returns (uint256) envfree; + function awards(uint256) external returns (address, uint48, uint48, uint48, address, uint8, uint128, uint128) envfree; + function ids() external returns (uint256) envfree; + function cap() external returns (uint256) envfree; + function usr(uint256) external returns (address) envfree; + function bgn(uint256) external returns (uint256) envfree; + function clf(uint256) external returns (uint256) envfree; + function fin(uint256) external returns (uint256) envfree; + function mgr(uint256) external returns (address) envfree; + function res(uint256) external returns (uint256) envfree; + function tot(uint256) external returns (uint256) envfree; + function rxd(uint256) external returns (uint256) envfree; + function valid(uint256) external returns (bool) envfree; + function gem() external returns (address) envfree; + function token.authority() external returns (address) envfree; + function token.owner() external returns (address) envfree; + function token.stopped() external returns (bool) envfree; + function token.totalSupply() external returns (uint256) envfree; + function token.balanceOf(address) external returns (uint256) envfree; +} ghost lockedGhost() returns uint256; -hook Sstore locked uint256 n_locked STORAGE { +hook Sstore locked uint256 n_locked { havoc lockedGhost assuming lockedGhost@new() == n_locked; } -hook Sload uint256 value locked STORAGE { +hook Sload uint256 value locked { require lockedGhost() == value; } -invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0 -filtered { f -> !f.isFallback } -invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0 -filtered { f -> !f.isFallback } -invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id) -filtered { f -> !f.isFallback } -invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id) -filtered { f -> !f.isFallback } +invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0; + +invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0; + +invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id); + +invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id); // The following invariant is replaced with a rule as it was kind of difficult to be finished this way. // Leaving this commented for possible future option to be finished. @@ -64,7 +59,7 @@ filtered { f -> !f.isFallback } // init_state axiom rxd(_id) == 0; // } -rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } { +rule rxdLessOrEqualTot(method f) { env e; uint256 _id; @@ -81,14 +76,13 @@ rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } { } // Verify fallback always reverts -// Important as we are filtering it out from invariants and some rules -rule fallback_revert(method f) filtered { f -> f.isFallback } { +rule fallback_revert(method f) { env e; calldataarg arg; f@withrevert(e, arg); - assert(lastReverted, "Fallback did not revert"); + assert(f.isFallback => lastReverted, "Fallback did not revert"); } // Verify that returned value is what expected in TWENTY_YEARS @@ -241,7 +235,7 @@ rule file_revert(bytes32 what, uint256 data) { bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; bool revert3 = locked != 0; - bool revert4 = what != 0x6361700000000000000000000000000000000000000000000000000000000000; // what != "cap" + bool revert4 = what != to_bytes32(0x6361700000000000000000000000000000000000000000000000000000000000); // what != "cap" assert(revert1 => lastReverted, "Sending ETH did not revert"); assert(revert2 => lastReverted, "Lack of auth did not revert"); @@ -288,8 +282,8 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 create@withrevert(e, _usr, _tot, _bgn, _tau, _eta, _mgr); - uint256 clf = _bgn + _eta; - uint256 fin = _bgn + _tau; + mathint clf = _bgn + _eta; + mathint fin = _bgn + _tau; bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; @@ -300,15 +294,14 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 bool revert7 = _bgn >= e.block.timestamp + twenty_years; bool revert8 = e.block.timestamp < twenty_years; bool revert9 = _bgn <= e.block.timestamp - twenty_years; - bool revert10 = _tau == 0; - bool revert11 = _tot / _tau > _cap; - bool revert12 = _tau > twenty_years; - bool revert13 = _eta > _tau; - bool revert14 = _ids == max_uint256; - bool revert15 = _bgn > max_uint48(); - bool revert16 = clf > max_uint48(); - bool revert17 = fin > max_uint48(); - bool revert18 = _tot > max_uint128; + bool revert10 = _tau == 0 || _tot / _tau > _cap; + bool revert11 = _tau > twenty_years; + bool revert12 = _eta > _tau; + bool revert13 = _ids == max_uint256; + bool revert14 = _bgn > max_uint48; + bool revert15 = clf > max_uint48; + bool revert16 = fin > max_uint48; + bool revert17 = _tot > max_uint128; assert(revert1 => lastReverted, "Sending ETH did not revert"); assert(revert2 => lastReverted, "Lack of auth did not revert"); @@ -319,15 +312,14 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 assert(revert7 => lastReverted, "Starting timestamp too far did not revert"); assert(revert8 => lastReverted, "Subtraction underflow did not revert"); assert(revert9 => lastReverted, "Starting timestamp too long ago did not revert"); - assert(revert10 => lastReverted, "Zero tau did not revert"); - assert(revert11 => lastReverted, "Rate too high did not revert"); - assert(revert12 => lastReverted, "Too long tau did not revert"); - assert(revert13 => lastReverted, "Too long clf did not revert"); - assert(revert14 => lastReverted, "Overflow ids did not revert"); - assert(revert15 => lastReverted, "Starting timestamp toUint48 cast did not revert"); - assert(revert16 => lastReverted, "Overflow toUint48 clf cast did not revert"); - assert(revert17 => lastReverted, "Overflow toUint48 fin cast did not revert"); - assert(revert18 => lastReverted, "Overflow toUint128 tot cast did not revert"); + assert(revert10 => lastReverted, "Zero tau or rate too high did not revert"); + assert(revert11 => lastReverted, "Too long tau did not revert"); + assert(revert12 => lastReverted, "Too long clf did not revert"); + assert(revert13 => lastReverted, "Overflow ids did not revert"); + assert(revert14 => lastReverted, "Starting timestamp toUint48 cast did not revert"); + assert(revert15 => lastReverted, "Overflow toUint48 clf cast did not revert"); + assert(revert16 => lastReverted, "Overflow toUint48 fin cast did not revert"); + assert(revert17 => lastReverted, "Overflow toUint128 tot cast did not revert"); assert(lastReverted => revert1 || revert2 || revert3 || @@ -335,7 +327,7 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 revert7 || revert8 || revert9 || revert10 || revert11 || revert12 || revert13 || revert14 || revert15 || - revert16 || revert17 || revert18, "Revert rules are not covering all the cases"); + revert16 || revert17, "Revert rules are not covering all the cases"); } // Verify that awards behave correctly on vest @@ -350,7 +342,7 @@ rule vest(uint256 _id) { requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -359,21 +351,21 @@ rule vest(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 balanceBefore = token.balanceOf(usr); - uint256 supplyBefore = token.totalSupply(); + mathint balanceBefore = token.balanceOf(usr); + mathint supplyBefore = token.totalSupply(); vest(e, _id); address usr2; uint48 bgn2; uint48 clf2; uint48 fin2; address mgr2; uint8 res2; uint128 tot2; uint128 rxd2; usr2, bgn2, clf2, fin2, mgr2, res2, tot2, rxd2 = awards(_id); - uint256 balanceAfter = token.balanceOf(usr); - uint256 supplyAfter = token.totalSupply(); + mathint balanceAfter = token.balanceOf(usr); + mathint supplyAfter = token.totalSupply(); assert(usr2 == usr, "usr changed"); assert(bgn2 == bgn, "bgn changed"); @@ -406,15 +398,15 @@ rule vest_revert(uint256 _id) { requireInvariant finGreaterOrEqualClf(_id); address tokenOwner = token.owner(); - bool canCall = authority.canCall(e, currentContract, token, 0x40c10f1900000000000000000000000000000000000000000000000000000000); + bool canCall = authority.canCall(e, currentContract, token, to_bytes4(0x40c10f19)); bool stop = token.stopped(); address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 usrBalance = token.balanceOf(usr); - uint256 supply = token.totalSupply(); - uint256 locked = lockedGhost(); + mathint usrBalance = token.balanceOf(usr); + mathint supply = token.totalSupply(); + mathint locked = lockedGhost(); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -423,7 +415,7 @@ rule vest_revert(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; @@ -475,7 +467,7 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -484,23 +476,23 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; + mathint amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; - uint256 balanceBefore = token.balanceOf(usr); - uint256 supplyBefore = token.totalSupply(); + mathint balanceBefore = token.balanceOf(usr); + mathint supplyBefore = token.totalSupply(); vest(e, _id, _maxAmt); address usr2; uint48 bgn2; uint48 clf2; uint48 fin2; address mgr2; uint8 res2; uint128 tot2; uint128 rxd2; usr2, bgn2, clf2, fin2, mgr2, res2, tot2, rxd2 = awards(_id); - uint256 balanceAfter = token.balanceOf(usr); - uint256 supplyAfter = token.totalSupply(); + mathint balanceAfter = token.balanceOf(usr); + mathint supplyAfter = token.totalSupply(); assert(usr2 == usr, "usr changed"); assert(bgn2 == bgn, "bgn changed"); @@ -532,15 +524,15 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { requireInvariant finGreaterOrEqualClf(_id); address tokenOwner = token.owner(); - bool canCall = authority.canCall(e, currentContract, token, 0x40c10f1900000000000000000000000000000000000000000000000000000000); + bool canCall = authority.canCall(e, currentContract, token, to_bytes4(0x40c10f19)); bool stop = token.stopped(); address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 usrBalance = token.balanceOf(usr); - uint256 supply = token.totalSupply(); - uint256 locked = lockedGhost(); + mathint usrBalance = token.balanceOf(usr); + mathint supply = token.totalSupply(); + mathint locked = lockedGhost(); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -549,12 +541,12 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; + mathint amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; vest@withrevert(e, _id, _maxAmt); @@ -598,7 +590,7 @@ rule accrued(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -607,7 +599,7 @@ rule accrued(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 amt = accrued(e, _id); + mathint amt = accrued(e, _id); assert(e.block.timestamp >= bgn && e.block.timestamp < fin => amt == accruedAmt, "accrued did not return amt as expected"); } @@ -619,7 +611,7 @@ rule accrued_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -651,7 +643,7 @@ rule unpaid(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -660,7 +652,7 @@ rule unpaid(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 amt = unpaid(e, _id); + mathint amt = unpaid(e, _id); assert(e.block.timestamp < clf => amt == 0, "unpaid did not return amt equal to zero as expected"); assert(e.block.timestamp >= clf => amt == accruedAmt - rxd, "unpaid did not return amt as expected"); @@ -673,7 +665,7 @@ rule unpaid_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -776,7 +768,7 @@ rule yank(uint256 _id) { requireInvariant finGreaterOrEqualClf(_id); require(rxd <= tot); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via yank but it's here for completeness : e.block.timestamp >= fin @@ -785,7 +777,7 @@ rule yank(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -818,7 +810,7 @@ rule yank_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via yank but it's here for completeness : e.block.timestamp >= fin @@ -827,7 +819,7 @@ rule yank_revert(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -838,7 +830,7 @@ rule yank_revert(uint256 _id) { bool revert2 = locked != 0; bool revert3 = ward != 1 && mgr != e.msg.sender; bool revert4 = usr == 0; - bool revert5 = e.block.timestamp < fin && e.block.timestamp > max_uint48(); + bool revert5 = e.block.timestamp < fin && e.block.timestamp > max_uint48; bool revert6 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && tot * (e.block.timestamp - bgn) > max_uint256; bool revert7 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && fin == bgn; bool revert8 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && accruedAmt < rxd; @@ -871,8 +863,8 @@ rule yank_end(uint256 _id, uint256 _end) { requireInvariant finGreaterOrEqualClf(_id); require(rxd <= tot); - uint256 _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; - uint256 accruedAmt = + mathint _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; + mathint accruedAmt = _end2 < bgn ? 0 // This case actually never enters via yank but it's here for completeness : _end2 >= fin @@ -881,7 +873,7 @@ rule yank_end(uint256 _id, uint256 _end) { ? (tot * (_end2 - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = _end2 < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -914,8 +906,8 @@ rule yank_end_revert(uint256 _id, uint256 _end) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; - uint256 accruedAmt = + mathint _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; + mathint accruedAmt = _end2 < bgn ? 0 // This case actually never enters via yank but it's here for completeness : _end2 >= fin @@ -924,7 +916,7 @@ rule yank_end_revert(uint256 _id, uint256 _end) { ? (tot * (_end2 - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = _end2 < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -935,7 +927,7 @@ rule yank_end_revert(uint256 _id, uint256 _end) { bool revert2 = locked != 0; bool revert3 = ward != 1 && mgr != e.msg.sender; bool revert4 = usr == 0; - bool revert5 = _end2 < fin && _end2 > max_uint48(); + bool revert5 = _end2 < fin && _end2 > max_uint48; bool revert6 = _end2 < fin && _end2 >= bgn && _end2 >= clf && tot * (_end2 - bgn) > max_uint256; bool revert7 = _end2 < fin && _end2 >= bgn && _end2 >= clf && fin == bgn; bool revert8 = _end2 < fin && _end2 >= bgn && _end2 >= clf && accruedAmt < rxd; diff --git a/certora/DssVestSuckable.conf b/certora/DssVestSuckable.conf new file mode 100644 index 00000000..ca9d4760 --- /dev/null +++ b/certora/DssVestSuckable.conf @@ -0,0 +1,38 @@ +{ + "verify": "DssVestSuckable:certora/DssVestSuckable.spec", + "parametric_contracts": [ + "DssVestSuckable" + ], + "files": [ + "src/DssVest.sol:DssVestSuckable", + "certora/harness/ChainLog.sol", + "certora/harness/Dai.sol", + "certora/harness/DaiJoin.sol", + "certora/harness/Vat.sol" + ], + "solc_map": { + "DssVestSuckable": "solc-0.6.12", + "ChainLog": "solc-0.6.12", + "Dai": "solc-0.5.12", + "DaiJoin": "solc-0.5.12", + "Vat": "solc-0.5.12" + }, + "solc_optimize_map": { + "DssVestSuckable": "200", + "ChainLog": "0", + "Dai": "0", + "DaiJoin": "0", + "Vat": "0" + }, + "link": [ + "DssVestSuckable:chainlog=ChainLog", + "DssVestSuckable:join=DaiJoin", + "DssVestSuckable:vat=Vat", + "DaiJoin:vat=Vat", + "DaiJoin:dai=Dai" + ], + "build_cache": true, + "rule_sanity": "basic", + "multi_assert_check": true, + "wait_for_results": "all" +} diff --git a/certora/DssVestSuckable.spec b/certora/DssVestSuckable.spec index 26ebc2d2..0ed05e38 100644 --- a/certora/DssVestSuckable.spec +++ b/certora/DssVestSuckable.spec @@ -1,64 +1,61 @@ // DssVestSuckable.spec -// certoraRun src/DssVest.sol:DssVestSuckable certora/ChainLog.sol certora/Vat.sol certora/DaiJoin.sol certora/Dai.sol --link DssVestSuckable:chainlog=ChainLog DssVestSuckable:vat=Vat DssVestSuckable:daiJoin=DaiJoin DaiJoin:vat=Vat DaiJoin:dai=Dai --verify DssVestSuckable:certora/DssVestSuckable.spec --rule_sanity - -using ChainLog as chainlog -using DaiJoin as daiJoin -using Vat as vat -using Dai as dai +using ChainLog as chainlog; +using DaiJoin as join; +using Vat as vat; +using Dai as dai; methods { - TWENTY_YEARS() returns (uint256) envfree - wards(address) returns (uint256) envfree - awards(uint256) returns (address, uint48, uint48, uint48, address, uint8, uint128, uint128) envfree - ids() returns (uint256) envfree - cap() returns (uint256) envfree - usr(uint256) returns (address) envfree - bgn(uint256) returns (uint256) envfree - clf(uint256) returns (uint256) envfree - fin(uint256) returns (uint256) envfree - mgr(uint256) returns (address) envfree - res(uint256) returns (uint256) envfree - tot(uint256) returns (uint256) envfree - rxd(uint256) returns (uint256) envfree - valid(uint256) returns (bool) envfree - chainlog.getAddress(bytes32) returns (address) - daiJoin.vat() returns (address) envfree - daiJoin.dai() returns (address) envfree - daiJoin.live() returns (uint256) envfree - vat.wards(address) returns (uint256) envfree - vat.can(address, address) returns (uint256) envfree - vat.dai(address) returns (uint256) envfree - vat.sin(address) returns (uint256) envfree - vat.debt() returns (uint256) envfree - vat.vice() returns (uint256) envfree - vat.live() returns (uint256) envfree - dai.wards(address) returns (uint256) envfree - dai.totalSupply() returns (uint256) envfree - dai.balanceOf(address) returns (uint256) envfree + function TWENTY_YEARS() external returns (uint256) envfree; + function wards(address) external returns (uint256) envfree; + function awards(uint256) external returns (address, uint48, uint48, uint48, address, uint8, uint128, uint128) envfree; + function ids() external returns (uint256) envfree; + function cap() external returns (uint256) envfree; + function usr(uint256) external returns (address) envfree; + function bgn(uint256) external returns (uint256) envfree; + function clf(uint256) external returns (uint256) envfree; + function fin(uint256) external returns (uint256) envfree; + function mgr(uint256) external returns (address) envfree; + function res(uint256) external returns (uint256) envfree; + function tot(uint256) external returns (uint256) envfree; + function rxd(uint256) external returns (uint256) envfree; + function valid(uint256) external returns (bool) envfree; + function chainlog.getAddress(bytes32) external returns (address) envfree; + function join.vat() external returns (address) envfree; + function join.dai() external returns (address) envfree; + function join.live() external returns (uint256) envfree; + function vat.wards(address) external returns (uint256) envfree; + function vat.can(address, address) external returns (uint256) envfree; + function vat.dai(address) external returns (uint256) envfree; + function vat.sin(address) external returns (uint256) envfree; + function vat.debt() external returns (uint256) envfree; + function vat.vice() external returns (uint256) envfree; + function vat.live() external returns (uint256) envfree; + function dai.wards(address) external returns (uint256) envfree; + function dai.totalSupply() external returns (uint256) envfree; + function dai.balanceOf(address) external returns (uint256) envfree; } -definition max_uint48() returns uint256 = 2^48 - 1; definition RAY() returns uint256 = 10^27; ghost lockedGhost() returns uint256; -hook Sstore locked uint256 n_locked STORAGE { +hook Sstore locked uint256 n_locked { havoc lockedGhost assuming lockedGhost@new() == n_locked; } -hook Sload uint256 value locked STORAGE { +hook Sload uint256 value locked { require lockedGhost() == value; } -invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0 -filtered { f -> !f.isFallback } -invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0 -filtered { f -> !f.isFallback } -invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id) -filtered { f -> !f.isFallback } -invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id) -filtered { f -> !f.isFallback } +invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0; + +invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0; + +invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id); + +invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id); + // The following invariant is replaced with a rule as it was kind of difficult to be finished this way. // Leaving this commented for possible future option to be finished. @@ -75,7 +72,7 @@ filtered { f -> !f.isFallback } // init_state axiom rxd(_id) == 0; // } -rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } { +rule rxdLessOrEqualTot(method f) { env e; uint256 _id; @@ -92,14 +89,13 @@ rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } { } // Verify fallback always reverts -// Important as we are filtering it out from invariants and some rules -rule fallback_revert(method f) filtered { f -> f.isFallback } { +rule fallback_revert(method f) { env e; calldataarg arg; f@withrevert(e, arg); - assert(lastReverted, "Fallback did not revert"); + assert(f.isFallback => lastReverted, "Fallback did not revert"); } // Verify that returned value is what expected in TWENTY_YEARS @@ -252,7 +248,7 @@ rule file_revert(bytes32 what, uint256 data) { bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; bool revert3 = locked != 0; - bool revert4 = what != 0x6361700000000000000000000000000000000000000000000000000000000000; // what != "cap" + bool revert4 = what != to_bytes32(0x6361700000000000000000000000000000000000000000000000000000000000); // what != "cap" assert(revert1 => lastReverted, "Sending ETH did not revert"); assert(revert2 => lastReverted, "Lack of auth did not revert"); @@ -299,8 +295,8 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 create@withrevert(e, _usr, _tot, _bgn, _tau, _eta, _mgr); - uint256 clf = _bgn + _eta; - uint256 fin = _bgn + _tau; + mathint clf = _bgn + _eta; + mathint fin = _bgn + _tau; bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; @@ -311,15 +307,14 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 bool revert7 = _bgn >= e.block.timestamp + twenty_years; bool revert8 = e.block.timestamp < twenty_years; bool revert9 = _bgn <= e.block.timestamp - twenty_years; - bool revert10 = _tau == 0; - bool revert11 = _tot / _tau > _cap; - bool revert12 = _tau > twenty_years; - bool revert13 = _eta > _tau; - bool revert14 = _ids == max_uint256; - bool revert15 = _bgn > max_uint48(); - bool revert16 = clf > max_uint48(); - bool revert17 = fin > max_uint48(); - bool revert18 = _tot > max_uint128; + bool revert10 = _tau == 0 || _tot / _tau > _cap; + bool revert11 = _tau > twenty_years; + bool revert12 = _eta > _tau; + bool revert13 = _ids == max_uint256; + bool revert14 = _bgn > max_uint48; + bool revert15 = clf > max_uint48; + bool revert16 = fin > max_uint48; + bool revert17 = _tot > max_uint128; assert(revert1 => lastReverted, "Sending ETH did not revert"); assert(revert2 => lastReverted, "Lack of auth did not revert"); @@ -330,15 +325,14 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 assert(revert7 => lastReverted, "Starting timestamp too far did not revert"); assert(revert8 => lastReverted, "Subtraction underflow did not revert"); assert(revert9 => lastReverted, "Starting timestamp too long ago did not revert"); - assert(revert10 => lastReverted, "Zero tau did not revert"); - assert(revert11 => lastReverted, "Rate too high did not revert"); - assert(revert12 => lastReverted, "Too long tau did not revert"); - assert(revert13 => lastReverted, "Too long clf did not revert"); - assert(revert14 => lastReverted, "Overflow ids did not revert"); - assert(revert15 => lastReverted, "Starting timestamp toUint48 cast did not revert"); - assert(revert16 => lastReverted, "Overflow toUint48 clf cast did not revert"); - assert(revert17 => lastReverted, "Overflow toUint48 fin cast did not revert"); - assert(revert18 => lastReverted, "Overflow toUint128 tot cast did not revert"); + assert(revert10 => lastReverted, "Zero tau or rate too high did not revert"); + assert(revert11 => lastReverted, "Too long tau did not revert"); + assert(revert12 => lastReverted, "Too long clf did not revert"); + assert(revert13 => lastReverted, "Overflow ids did not revert"); + assert(revert14 => lastReverted, "Starting timestamp toUint48 cast did not revert"); + assert(revert15 => lastReverted, "Overflow toUint48 clf cast did not revert"); + assert(revert16 => lastReverted, "Overflow toUint48 fin cast did not revert"); + assert(revert17 => lastReverted, "Overflow toUint128 tot cast did not revert"); assert(lastReverted => revert1 || revert2 || revert3 || @@ -346,15 +340,15 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 revert7 || revert8 || revert9 || revert10 || revert11 || revert12 || revert13 || revert14 || revert15 || - revert16 || revert17 || revert18, "Revert rules are not covering all the cases"); + revert16 || revert17, "Revert rules are not covering all the cases"); } // Verify that awards behave correctly on vest rule vest(uint256 _id) { env e; - require(vat == daiJoin.vat()); - require(dai == daiJoin.dai()); + require(vat == join.vat()); + require(dai == join.dai()); address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); @@ -362,7 +356,7 @@ rule vest(uint256 _id) { requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -371,21 +365,21 @@ rule vest(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 balanceBefore = dai.balanceOf(usr); - uint256 supplyBefore = dai.totalSupply(); + mathint balanceBefore = dai.balanceOf(usr); + mathint supplyBefore = dai.totalSupply(); vest(e, _id); address usr2; uint48 bgn2; uint48 clf2; uint48 fin2; address mgr2; uint8 res2; uint128 tot2; uint128 rxd2; usr2, bgn2, clf2, fin2, mgr2, res2, tot2, rxd2 = awards(_id); - uint256 balanceAfter = dai.balanceOf(usr); - uint256 supplyAfter = dai.totalSupply(); + mathint balanceAfter = dai.balanceOf(usr); + mathint supplyAfter = dai.totalSupply(); assert(usr2 == usr, "usr changed"); assert(bgn2 == bgn, "bgn changed"); @@ -411,8 +405,8 @@ rule vest(uint256 _id) { rule vest_revert(uint256 _id) { env e; - require(vat == daiJoin.vat()); - require(dai == daiJoin.dai()); + require(vat == join.vat()); + require(dai == join.dai()); requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); @@ -423,18 +417,18 @@ rule vest_revert(uint256 _id) { uint256 supply = dai.totalSupply(); uint256 locked = lockedGhost(); uint256 vatLive = vat.live(); - address vow = chainlog.getAddress(e, 0x4d43445f564f5700000000000000000000000000000000000000000000000000); - uint256 daiJoinLive = daiJoin.live(); + address vow = chainlog.getAddress(e, to_bytes32(0x4d43445f564f5700000000000000000000000000000000000000000000000000)); + uint256 daiJoinLive = join.live(); uint256 wardVat = vat.wards(currentContract); - uint256 canVestDaiJoin = vat.can(currentContract, daiJoin); - uint256 wardDai = dai.wards(daiJoin); + uint256 canVestDaiJoin = vat.can(currentContract, join); + uint256 wardDai = dai.wards(join); uint256 sinVow = vat.sin(vow); uint256 vatDaiVest = vat.dai(currentContract); uint256 vice = vat.vice(); uint256 debt = vat.debt(); - uint256 vatDaiDaiJoin = vat.dai(daiJoin); + uint256 vatDaiDaiJoin = vat.dai(join); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -443,12 +437,12 @@ rule vest_revert(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 unpaidAmtRad = RAY() * unpaidAmt; + mathint unpaidAmtRad = RAY() * unpaidAmt; vest@withrevert(e, _id); @@ -469,7 +463,7 @@ rule vest_revert(uint256 _id) { bool revert15 = vice + unpaidAmtRad > max_uint256; bool revert16 = debt + unpaidAmtRad > max_uint256; bool revert17 = daiJoinLive != 1; - bool revert18 = currentContract != daiJoin && canVestDaiJoin != 1; + bool revert18 = currentContract != join && canVestDaiJoin != 1; bool revert19 = vatDaiDaiJoin + unpaidAmtRad > max_uint256; bool revert20 = wardDai != 1; bool revert21 = usrBalance + unpaidAmt > max_uint256; @@ -491,10 +485,10 @@ rule vest_revert(uint256 _id) { assert(revert14 => lastReverted, "Overflow dai + rad did not revert"); assert(revert15 => lastReverted, "Overflow vice + rad did not revert"); assert(revert16 => lastReverted, "Overflow debt + rad did not revert"); - assert(revert17 => lastReverted, "Not live daiJoin did not revert"); + assert(revert17 => lastReverted, "Not live join did not revert"); assert(revert18 => lastReverted, "The function wish did not revert"); assert(revert19 => lastReverted, "Overflow dst + rad did not revert"); - assert(revert20 => lastReverted, "Lack of dai auth on daiJoin did not revert"); + assert(revert20 => lastReverted, "Lack of dai auth on join did not revert"); assert(revert21 => lastReverted, "Overflow usr balance did not revert"); assert(revert22 => lastReverted, "Overflow totalSupply did not revert"); @@ -513,8 +507,8 @@ rule vest_revert(uint256 _id) { rule vest_amt(uint256 _id, uint256 _maxAmt) { env e; - require(vat == daiJoin.vat()); - require(dai == daiJoin.dai()); + require(vat == join.vat()); + require(dai == join.dai()); address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); @@ -522,7 +516,7 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -531,23 +525,23 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; + mathint amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; - uint256 balanceBefore = dai.balanceOf(usr); - uint256 supplyBefore = dai.totalSupply(); + mathint balanceBefore = dai.balanceOf(usr); + mathint supplyBefore = dai.totalSupply(); vest(e, _id, _maxAmt); address usr2; uint48 bgn2; uint48 clf2; uint48 fin2; address mgr2; uint8 res2; uint128 tot2; uint128 rxd2; usr2, bgn2, clf2, fin2, mgr2, res2, tot2, rxd2 = awards(_id); - uint256 balanceAfter = dai.balanceOf(usr); - uint256 supplyAfter = dai.totalSupply(); + mathint balanceAfter = dai.balanceOf(usr); + mathint supplyAfter = dai.totalSupply(); assert(usr2 == usr, "usr changed"); assert(bgn2 == bgn, "bgn changed"); @@ -572,8 +566,8 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { env e; - require(vat == daiJoin.vat()); - require(dai == daiJoin.dai()); + require(vat == join.vat()); + require(dai == join.dai()); requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); @@ -584,18 +578,18 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { uint256 supply = dai.totalSupply(); uint256 locked = lockedGhost(); uint256 vatLive = vat.live(); - address vow = chainlog.getAddress(e, 0x4d43445f564f5700000000000000000000000000000000000000000000000000); - uint256 daiJoinLive = daiJoin.live(); + address vow = chainlog.getAddress(e, to_bytes32(0x4d43445f564f5700000000000000000000000000000000000000000000000000)); + uint256 daiJoinLive = join.live(); uint256 wardVat = vat.wards(currentContract); - uint256 canVestDaiJoin = vat.can(currentContract, daiJoin); - uint256 wardDai = dai.wards(daiJoin); + uint256 canVestDaiJoin = vat.can(currentContract, join); + uint256 wardDai = dai.wards(join); uint256 sinVow = vat.sin(vow); uint256 vatDaiVest = vat.dai(currentContract); uint256 vice = vat.vice(); uint256 debt = vat.debt(); - uint256 vatDaiDaiJoin = vat.dai(daiJoin); + uint256 vatDaiDaiJoin = vat.dai(join); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -604,14 +598,14 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; + mathint amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; - uint256 amtRad = RAY() * amt; + mathint amtRad = RAY() * amt; vest@withrevert(e, _id, _maxAmt); @@ -632,7 +626,7 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { bool revert15 = vice + amtRad > max_uint256; bool revert16 = debt + amtRad > max_uint256; bool revert17 = daiJoinLive != 1; - bool revert18 = currentContract != daiJoin && canVestDaiJoin != 1; + bool revert18 = currentContract != join && canVestDaiJoin != 1; bool revert19 = vatDaiDaiJoin + amtRad > max_uint256; bool revert20 = wardDai != 1; bool revert21 = usrBalance + amt > max_uint256; @@ -654,10 +648,10 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { assert(revert14 => lastReverted, "Overflow dai + rad did not revert"); assert(revert15 => lastReverted, "Overflow vice + rad did not revert"); assert(revert16 => lastReverted, "Overflow debt + rad did not revert"); - assert(revert17 => lastReverted, "Not live daiJoin did not revert"); + assert(revert17 => lastReverted, "Not live join did not revert"); assert(revert18 => lastReverted, "The function wish did not revert"); assert(revert19 => lastReverted, "Overflow dst + rad did not revert"); - assert(revert20 => lastReverted, "Lack of dai auth on daiJoin did not revert"); + assert(revert20 => lastReverted, "Lack of dai auth on join did not revert"); assert(revert21 => lastReverted, "Overflow usr balance did not revert"); assert(revert22 => lastReverted, "Overflow totalSupply did not revert"); @@ -679,7 +673,7 @@ rule accrued(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -688,7 +682,7 @@ rule accrued(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 amt = accrued(e, _id); + mathint amt = accrued(e, _id); assert(e.block.timestamp >= bgn && e.block.timestamp < fin => amt == accruedAmt, "accrued did not return amt as expected"); } @@ -700,7 +694,7 @@ rule accrued_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -732,7 +726,7 @@ rule unpaid(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -741,7 +735,7 @@ rule unpaid(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 amt = unpaid(e, _id); + mathint amt = unpaid(e, _id); assert(e.block.timestamp < clf => amt == 0, "unpaid did not return amt equal to zero as expected"); assert(e.block.timestamp >= clf => amt == accruedAmt - rxd, "unpaid did not return amt as expected"); @@ -754,7 +748,7 @@ rule unpaid_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -794,8 +788,8 @@ rule restrict(uint256 _id) { rule restrict_revert(uint256 _id) { env e; - uint256 locked = lockedGhost(); - uint256 ward = wards(e.msg.sender); + mathint locked = lockedGhost(); + mathint ward = wards(e.msg.sender); address _usr = usr(_id); restrict@withrevert(e, _id); @@ -826,8 +820,8 @@ rule unrestrict(uint256 _id) { rule unrestrict_revert(uint256 _id) { env e; - uint256 locked = lockedGhost(); - uint256 ward = wards(e.msg.sender); + mathint locked = lockedGhost(); + mathint ward = wards(e.msg.sender); address _usr = usr(_id); unrestrict@withrevert(e, _id); @@ -856,7 +850,7 @@ rule yank(uint256 _id) { requireInvariant finGreaterOrEqualClf(_id); require(rxd <= tot); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via yank but it's here for completeness : e.block.timestamp >= fin @@ -865,7 +859,7 @@ rule yank(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -893,12 +887,12 @@ rule yank(uint256 _id) { rule yank_revert(uint256 _id) { env e; - uint256 locked = lockedGhost(); - uint256 ward = wards(e.msg.sender); + mathint locked = lockedGhost(); + mathint ward = wards(e.msg.sender); address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via yank but it's here for completeness : e.block.timestamp >= fin @@ -907,7 +901,7 @@ rule yank_revert(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -918,7 +912,7 @@ rule yank_revert(uint256 _id) { bool revert2 = locked != 0; bool revert3 = ward != 1 && mgr != e.msg.sender; bool revert4 = usr == 0; - bool revert5 = e.block.timestamp < fin && e.block.timestamp > max_uint48(); + bool revert5 = e.block.timestamp < fin && e.block.timestamp > max_uint48; bool revert6 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && tot * (e.block.timestamp - bgn) > max_uint256; bool revert7 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && fin == bgn; bool revert8 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && accruedAmt < rxd; @@ -951,8 +945,8 @@ rule yank_end(uint256 _id, uint256 _end) { requireInvariant finGreaterOrEqualClf(_id); require(rxd <= tot); - uint256 _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; - uint256 accruedAmt = + mathint _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; + mathint accruedAmt = _end2 < bgn ? 0 // This case actually never enters via yank but it's here for completeness : _end2 >= fin @@ -961,7 +955,7 @@ rule yank_end(uint256 _id, uint256 _end) { ? (tot * (_end2 - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = _end2 < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -989,13 +983,13 @@ rule yank_end(uint256 _id, uint256 _end) { rule yank_end_revert(uint256 _id, uint256 _end) { env e; - uint256 locked = lockedGhost(); - uint256 ward = wards(e.msg.sender); + mathint locked = lockedGhost(); + mathint ward = wards(e.msg.sender); address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; - uint256 accruedAmt = + mathint _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; + mathint accruedAmt = _end2 < bgn ? 0 // This case actually never enters via yank but it's here for completeness : _end2 >= fin @@ -1004,7 +998,7 @@ rule yank_end_revert(uint256 _id, uint256 _end) { ? (tot * (_end2 - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = _end2 < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -1015,7 +1009,7 @@ rule yank_end_revert(uint256 _id, uint256 _end) { bool revert2 = locked != 0; bool revert3 = ward != 1 && mgr != e.msg.sender; bool revert4 = usr == 0; - bool revert5 = _end2 < fin && _end2 > max_uint48(); + bool revert5 = _end2 < fin && _end2 > max_uint48; bool revert6 = _end2 < fin && _end2 >= bgn && _end2 >= clf && tot * (_end2 - bgn) > max_uint256; bool revert7 = _end2 < fin && _end2 >= bgn && _end2 >= clf && fin == bgn; bool revert8 = _end2 < fin && _end2 >= bgn && _end2 >= clf && accruedAmt < rxd; @@ -1050,7 +1044,7 @@ rule move(uint256 _id, address _dst) { rule move_revert(uint256 _id, address _dst) { env e; - uint256 locked = lockedGhost(); + mathint locked = lockedGhost(); address _usr = usr(_id); move@withrevert(e, _id, _dst); @@ -1070,8 +1064,8 @@ rule move_revert(uint256 _id, address _dst) { // Verify that ids behave correctly on valid rule valid(uint256 _id) { - uint256 _tot = tot(_id); - uint256 _rxd = rxd(_id); + mathint _tot = tot(_id); + mathint _rxd = rxd(_id); bool validContract = _rxd < _tot; diff --git a/certora/DssVestTransferrable.conf b/certora/DssVestTransferrable.conf new file mode 100644 index 00000000..cb406787 --- /dev/null +++ b/certora/DssVestTransferrable.conf @@ -0,0 +1,22 @@ +{ + "verify": "DssVestTransferrable:certora/DssVestTransferrable.spec", + "parametric_contracts": [ + "DssVestTransferrable" + ], + "files": [ + "src/DssVest.sol:DssVestTransferrable", + "certora/harness/Dai.sol" + ], + "solc": "solc-0.6.12", + "solc_optimize_map": { + "DssVestTransferrable": "200", + "Dai": "0" + }, + "link": [ + "DssVestTransferrable:gem=Dai" + ], + "build_cache": true, + "rule_sanity": "basic", + "multi_assert_check": true, + "wait_for_results": "all" +} diff --git a/certora/DssVestTransferrable.spec b/certora/DssVestTransferrable.spec index 04330a14..07e8e9a6 100644 --- a/certora/DssVestTransferrable.spec +++ b/certora/DssVestTransferrable.spec @@ -1,51 +1,47 @@ // DssVestTransferrable.spec -// certoraRun src/DssVest.sol:DssVestTransferrable certora/Dai.sol --link DssVestTransferrable:gem=Dai --verify DssVestTransferrable:certora/DssVestTransferrable.spec --rule_sanity - -using Dai as dai +using Dai as dai; methods { - TWENTY_YEARS() returns (uint256) envfree - wards(address) returns (uint256) envfree - awards(uint256) returns (address, uint48, uint48, uint48, address, uint8, uint128, uint128) envfree - ids() returns (uint256) envfree - cap() returns (uint256) envfree - usr(uint256) returns (address) envfree - bgn(uint256) returns (uint256) envfree - clf(uint256) returns (uint256) envfree - fin(uint256) returns (uint256) envfree - mgr(uint256) returns (address) envfree - res(uint256) returns (uint256) envfree - tot(uint256) returns (uint256) envfree - rxd(uint256) returns (uint256) envfree - valid(uint256) returns (bool) envfree - czar() returns (address) envfree - gem() returns (address) envfree - dai.totalSupply() returns (uint256) envfree - dai.balanceOf(address) returns (uint256) envfree - dai.allowance(address, address) returns (uint256) envfree -} - -definition max_uint48() returns uint256 = 2^48 - 1; + function TWENTY_YEARS() external returns (uint256) envfree; + function wards(address) external returns (uint256) envfree; + function awards(uint256) external returns (address, uint48, uint48, uint48, address, uint8, uint128, uint128) envfree; + function ids() external returns (uint256) envfree; + function cap() external returns (uint256) envfree; + function usr(uint256) external returns (address) envfree; + function bgn(uint256) external returns (uint256) envfree; + function clf(uint256) external returns (uint256) envfree; + function fin(uint256) external returns (uint256) envfree; + function mgr(uint256) external returns (address) envfree; + function res(uint256) external returns (uint256) envfree; + function tot(uint256) external returns (uint256) envfree; + function rxd(uint256) external returns (uint256) envfree; + function valid(uint256) external returns (bool) envfree; + function czar() external returns (address) envfree; + function gem() external returns (address) envfree; + function dai.totalSupply() external returns (uint256) envfree; + function dai.balanceOf(address) external returns (uint256) envfree; + function dai.allowance(address, address) external returns (uint256) envfree; +} ghost lockedGhost() returns uint256; -hook Sstore locked uint256 n_locked STORAGE { +hook Sstore locked uint256 n_locked { havoc lockedGhost assuming lockedGhost@new() == n_locked; } -hook Sload uint256 value locked STORAGE { +hook Sload uint256 value locked { require lockedGhost() == value; } -invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0 -filtered { f -> !f.isFallback } -invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0 -filtered { f -> !f.isFallback } -invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id) -filtered { f -> !f.isFallback } -invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id) -filtered { f -> !f.isFallback } +invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0; + +invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0; + +invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id); + +invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id); + // The following invariant is replaced with a rule as it was kind of difficult to be finished this way. // Leaving this commented for possible future option to be finished. @@ -62,7 +58,7 @@ filtered { f -> !f.isFallback } // init_state axiom rxd(_id) == 0; // } -rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } { +rule rxdLessOrEqualTot(method f) { env e; uint256 _id; @@ -79,14 +75,13 @@ rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } { } // Verify fallback always reverts -// Important as we are filtering it out from invariants and some rules -rule fallback_revert(method f) filtered { f -> f.isFallback } { +rule fallback_revert(method f) { env e; calldataarg arg; f@withrevert(e, arg); - assert(lastReverted, "Fallback did not revert"); + assert(f.isFallback => lastReverted, "Fallback did not revert"); } // Verify that returned value is what expected in TWENTY_YEARS @@ -239,7 +234,7 @@ rule file_revert(bytes32 what, uint256 data) { bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; bool revert3 = locked != 0; - bool revert4 = what != 0x6361700000000000000000000000000000000000000000000000000000000000; // what != "cap" + bool revert4 = what != to_bytes32(0x6361700000000000000000000000000000000000000000000000000000000000); // what != "cap" assert(revert1 => lastReverted, "Sending ETH did not revert"); assert(revert2 => lastReverted, "Lack of auth did not revert"); @@ -286,8 +281,8 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 create@withrevert(e, _usr, _tot, _bgn, _tau, _eta, _mgr); - uint256 clf = _bgn + _eta; - uint256 fin = _bgn + _tau; + mathint clf = _bgn + _eta; + mathint fin = _bgn + _tau; bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; @@ -298,15 +293,14 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 bool revert7 = _bgn >= e.block.timestamp + twenty_years; bool revert8 = e.block.timestamp < twenty_years; bool revert9 = _bgn <= e.block.timestamp - twenty_years; - bool revert10 = _tau == 0; - bool revert11 = _tot / _tau > _cap; - bool revert12 = _tau > twenty_years; - bool revert13 = _eta > _tau; - bool revert14 = _ids == max_uint256; - bool revert15 = _bgn > max_uint48(); - bool revert16 = clf > max_uint48(); - bool revert17 = fin > max_uint48(); - bool revert18 = _tot > max_uint128; + bool revert10 = _tau == 0 || _tot / _tau > _cap; + bool revert11 = _tau > twenty_years; + bool revert12 = _eta > _tau; + bool revert13 = _ids == max_uint256; + bool revert14 = _bgn > max_uint48; + bool revert15 = clf > max_uint48; + bool revert16 = fin > max_uint48; + bool revert17 = _tot > max_uint128; assert(revert1 => lastReverted, "Sending ETH did not revert"); assert(revert2 => lastReverted, "Lack of auth did not revert"); @@ -317,15 +311,14 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 assert(revert7 => lastReverted, "Starting timestamp too far did not revert"); assert(revert8 => lastReverted, "Subtraction underflow did not revert"); assert(revert9 => lastReverted, "Starting timestamp too long ago did not revert"); - assert(revert10 => lastReverted, "Zero tau did not revert"); - assert(revert11 => lastReverted, "Rate too high did not revert"); - assert(revert12 => lastReverted, "Too long tau did not revert"); - assert(revert13 => lastReverted, "Too long clf did not revert"); - assert(revert14 => lastReverted, "Overflow ids did not revert"); - assert(revert15 => lastReverted, "Starting timestamp toUint48 cast did not revert"); - assert(revert16 => lastReverted, "Overflow toUint48 clf cast did not revert"); - assert(revert17 => lastReverted, "Overflow toUint48 fin cast did not revert"); - assert(revert18 => lastReverted, "Overflow toUint128 tot cast did not revert"); + assert(revert10 => lastReverted, "Zero tau or rate too high did not revert"); + assert(revert11 => lastReverted, "Too long tau did not revert"); + assert(revert12 => lastReverted, "Too long clf did not revert"); + assert(revert13 => lastReverted, "Overflow ids did not revert"); + assert(revert14 => lastReverted, "Starting timestamp toUint48 cast did not revert"); + assert(revert15 => lastReverted, "Overflow toUint48 clf cast did not revert"); + assert(revert16 => lastReverted, "Overflow toUint48 fin cast did not revert"); + assert(revert17 => lastReverted, "Overflow toUint128 tot cast did not revert"); assert(lastReverted => revert1 || revert2 || revert3 || @@ -333,7 +326,7 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2 revert7 || revert8 || revert9 || revert10 || revert11 || revert12 || revert13 || revert14 || revert15 || - revert16 || revert17 || revert18, "Revert rules are not covering all the cases"); + revert16 || revert17, "Revert rules are not covering all the cases"); } // Verify that awards behave correctly on vest @@ -349,7 +342,7 @@ rule vest(uint256 _id) { requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -358,23 +351,23 @@ rule vest(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 czarBalanceBefore = dai.balanceOf(_czar); - uint256 usrBalanceBefore = dai.balanceOf(usr); - uint256 supplyBefore = dai.totalSupply(); + mathint czarBalanceBefore = dai.balanceOf(_czar); + mathint usrBalanceBefore = dai.balanceOf(usr); + mathint supplyBefore = dai.totalSupply(); vest(e, _id); address usr2; uint48 bgn2; uint48 clf2; uint48 fin2; address mgr2; uint8 res2; uint128 tot2; uint128 rxd2; usr2, bgn2, clf2, fin2, mgr2, res2, tot2, rxd2 = awards(_id); - uint256 czarBalanceAfter = dai.balanceOf(_czar); - uint256 usrBalanceAfter = dai.balanceOf(usr); - uint256 supplyAfter = dai.totalSupply(); + mathint czarBalanceAfter = dai.balanceOf(_czar); + mathint usrBalanceAfter = dai.balanceOf(usr); + mathint supplyAfter = dai.totalSupply(); assert(usr2 == usr, "usr changed"); assert(bgn2 == bgn, "bgn changed"); @@ -414,7 +407,7 @@ rule vest_revert(uint256 _id) { uint256 usrBalance = dai.balanceOf(usr); uint256 allowed = dai.allowance(_czar, currentContract); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -423,7 +416,7 @@ rule vest_revert(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; @@ -476,7 +469,7 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { requireInvariant clfGreaterOrEqualBgn(_id); requireInvariant finGreaterOrEqualClf(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -485,16 +478,16 @@ rule vest_amt(uint256 _id, uint256 _maxAmt) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; + mathint amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; - uint256 czarBalanceBefore = dai.balanceOf(_czar); - uint256 usrBalanceBefore = dai.balanceOf(usr); - uint256 supplyBefore = dai.totalSupply(); + mathint czarBalanceBefore = dai.balanceOf(_czar); + mathint usrBalanceBefore = dai.balanceOf(usr); + mathint supplyBefore = dai.totalSupply(); vest(e, _id, _maxAmt); @@ -542,7 +535,7 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { uint256 usrBalance = dai.balanceOf(usr); uint256 allowed = dai.allowance(_czar, currentContract); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via vest but it's here for completeness : e.block.timestamp >= fin @@ -551,12 +544,12 @@ rule vest_amt_revert(uint256 _id, uint256 _maxAmt) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 : accruedAmt - rxd; - uint256 amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; + mathint amt = _maxAmt > unpaidAmt ? unpaidAmt : _maxAmt; vest@withrevert(e, _id, _maxAmt); @@ -600,7 +593,7 @@ rule accrued(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -609,7 +602,7 @@ rule accrued(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 amt = accrued(e, _id); + mathint amt = accrued(e, _id); assert(e.block.timestamp >= bgn && e.block.timestamp < fin => amt == accruedAmt, "accrued did not return amt as expected"); } @@ -621,7 +614,7 @@ rule accrued_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -653,7 +646,7 @@ rule unpaid(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -662,7 +655,7 @@ rule unpaid(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 amt = unpaid(e, _id); + mathint amt = unpaid(e, _id); assert(e.block.timestamp < clf => amt == 0, "unpaid did not return amt equal to zero as expected"); assert(e.block.timestamp >= clf => amt == accruedAmt - rxd, "unpaid did not return amt as expected"); @@ -675,7 +668,7 @@ rule unpaid_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 : e.block.timestamp >= fin @@ -776,7 +769,7 @@ rule yank(uint256 _id) { requireInvariant finGreaterOrEqualClf(_id); require(rxd <= tot); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via yank but it's here for completeness : e.block.timestamp >= fin @@ -785,7 +778,7 @@ rule yank(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -818,7 +811,7 @@ rule yank_revert(uint256 _id) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 accruedAmt = + mathint accruedAmt = e.block.timestamp < bgn ? 0 // This case actually never enters via yank but it's here for completeness : e.block.timestamp >= fin @@ -827,7 +820,7 @@ rule yank_revert(uint256 _id) { ? (tot * (e.block.timestamp - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = e.block.timestamp < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -838,7 +831,7 @@ rule yank_revert(uint256 _id) { bool revert2 = locked != 0; bool revert3 = ward != 1 && mgr != e.msg.sender; bool revert4 = usr == 0; - bool revert5 = e.block.timestamp < fin && e.block.timestamp > max_uint48(); + bool revert5 = e.block.timestamp < fin && e.block.timestamp > max_uint48; bool revert6 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && tot * (e.block.timestamp - bgn) > max_uint256; bool revert7 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && fin == bgn; bool revert8 = e.block.timestamp < fin && e.block.timestamp >= bgn && e.block.timestamp >= clf && accruedAmt < rxd; @@ -871,8 +864,8 @@ rule yank_end(uint256 _id, uint256 _end) { requireInvariant finGreaterOrEqualClf(_id); require(rxd <= tot); - uint256 _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; - uint256 accruedAmt = + mathint _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; + mathint accruedAmt = _end2 < bgn ? 0 // This case actually never enters via yank but it's here for completeness : _end2 >= fin @@ -881,7 +874,7 @@ rule yank_end(uint256 _id, uint256 _end) { ? (tot * (_end2 - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = _end2 < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -914,8 +907,8 @@ rule yank_end_revert(uint256 _id, uint256 _end) { address usr; uint48 bgn; uint48 clf; uint48 fin; address mgr; uint8 res; uint128 tot; uint128 rxd; usr, bgn, clf, fin, mgr, res, tot, rxd = awards(_id); - uint256 _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; - uint256 accruedAmt = + mathint _end2 = _end < e.block.timestamp ? e.block.timestamp : _end; + mathint accruedAmt = _end2 < bgn ? 0 // This case actually never enters via yank but it's here for completeness : _end2 >= fin @@ -924,7 +917,7 @@ rule yank_end_revert(uint256 _id, uint256 _end) { ? (tot * (_end2 - bgn)) / (fin - bgn) : 9999; // Random value as tx will revert in this case - uint256 unpaidAmt = + mathint unpaidAmt = _end2 < clf ? 0 // This case actually never enters via yank but it's here for completeness : accruedAmt - rxd; @@ -935,7 +928,7 @@ rule yank_end_revert(uint256 _id, uint256 _end) { bool revert2 = locked != 0; bool revert3 = ward != 1 && mgr != e.msg.sender; bool revert4 = usr == 0; - bool revert5 = _end2 < fin && _end2 > max_uint48(); + bool revert5 = _end2 < fin && _end2 > max_uint48; bool revert6 = _end2 < fin && _end2 >= bgn && _end2 >= clf && tot * (_end2 - bgn) > max_uint256; bool revert7 = _end2 < fin && _end2 >= bgn && _end2 >= clf && fin == bgn; bool revert8 = _end2 < fin && _end2 >= bgn && _end2 >= clf && accruedAmt < rxd; diff --git a/certora/ChainLog.sol b/certora/harness/ChainLog.sol similarity index 100% rename from certora/ChainLog.sol rename to certora/harness/ChainLog.sol diff --git a/certora/DSToken.sol b/certora/harness/DSToken.sol similarity index 100% rename from certora/DSToken.sol rename to certora/harness/DSToken.sol diff --git a/certora/Dai.sol b/certora/harness/Dai.sol similarity index 100% rename from certora/Dai.sol rename to certora/harness/Dai.sol diff --git a/certora/DaiJoin.sol b/certora/harness/DaiJoin.sol similarity index 100% rename from certora/DaiJoin.sol rename to certora/harness/DaiJoin.sol diff --git a/certora/MockAuthority.sol b/certora/harness/MockAuthority.sol similarity index 100% rename from certora/MockAuthority.sol rename to certora/harness/MockAuthority.sol diff --git a/certora/Vat.sol b/certora/harness/Vat.sol similarity index 100% rename from certora/Vat.sol rename to certora/harness/Vat.sol diff --git a/echidna/DssVestSuckableEchidnaTest.sol b/echidna/DssVestSuckableEchidnaTest.sol index 0220d9cd..56ed117f 100644 --- a/echidna/DssVestSuckableEchidnaTest.sol +++ b/echidna/DssVestSuckableEchidnaTest.sol @@ -55,7 +55,7 @@ contract DssVestSuckableEchidnaTest { chainlog.setAddress("MCD_VAT", address(vat)); chainlog.setAddress("MCD_JOIN_DAI", address(daiJoin)); chainlog.setAddress("MCD_VOW", vow); - sVest = new DssVestSuckable(address(chainlog)); + sVest = new DssVestSuckable(address(chainlog), address(daiJoin)); sVest.file("cap", MIN * WAD / TIME); dai.rely(address(daiJoin)); vat.rely(address(sVest)); diff --git a/src/DssVest.sol b/src/DssVest.sol index 59e52d34..99082c9f 100644 --- a/src/DssVest.sol +++ b/src/DssVest.sol @@ -27,8 +27,9 @@ interface ChainlogLike { function getAddress(bytes32) external view returns (address); } -interface DaiJoinLike { +interface JoinLike { function exit(address, uint256) external; + function vat() external view returns (address); } interface VatLike { @@ -428,19 +429,23 @@ contract DssVestSuckable is DssVest { ChainlogLike public immutable chainlog; VatLike public immutable vat; - DaiJoinLike public immutable daiJoin; + JoinLike public immutable join; /** @dev This contract must be authorized to 'suck' on the vat @param _chainlog The contract address of the MCD chainlog + @param _join The native join contract from MCD */ - constructor(address _chainlog) public DssVest() { - require(_chainlog != address(0), "DssVestSuckable/Invalid-chainlog-address"); + constructor(address _chainlog, address _join) public DssVest() { + require(_chainlog != address(0), "DssVestSuckable/invalid-chainlog-address"); ChainlogLike chainlog_ = chainlog = ChainlogLike(_chainlog); + VatLike vat_ = vat = VatLike(chainlog_.getAddress("MCD_VAT")); - DaiJoinLike daiJoin_ = daiJoin = DaiJoinLike(chainlog_.getAddress("MCD_JOIN_DAI")); - vat_.hope(address(daiJoin_)); + require(JoinLike(_join).vat() == address(vat_), "DssVestSuckable/invalid-join-vat"); + join = JoinLike(_join); + + vat_.hope(_join); } /** @@ -451,7 +456,14 @@ contract DssVestSuckable is DssVest { function pay(address _guy, uint256 _amt) override internal { require(vat.live() == 1, "DssVestSuckable/vat-not-live"); vat.suck(chainlog.getAddress("MCD_VOW"), address(this), mul(_amt, RAY)); - daiJoin.exit(_guy, _amt); + join.exit(_guy, _amt); + } + + /** + @dev Compatibility with older implementations of `DssVestSuckable` + */ + function daiJoin() external view returns (address) { + return address(join); } } diff --git a/src/DssVest.t.sol b/src/DssVest.t.sol index 3d8d35dd..60a1dbfc 100644 --- a/src/DssVest.t.sol +++ b/src/DssVest.t.sol @@ -26,7 +26,7 @@ interface GemLike { function approve(address, uint256) external returns (bool); } -interface DaiLike is GemLike { +interface ERC20Like is GemLike { function balanceOf(address) external returns (uint256); } @@ -90,6 +90,7 @@ contract DssVestTest is DSTest { DssVestMintable mVest; DssVestSuckable sVest; + DssVestSuckable sVestUsds; DssVestTransferrable tVest; Manager boss; @@ -97,7 +98,10 @@ contract DssVestTest is DSTest { DSTokenLike gem; MkrAuthorityLike authority; VatLike vat; - DaiLike dai; + ERC20Like dai; + address daiJoin; + ERC20Like usds; + address usdsJoin; EndLike end; address VOW; @@ -109,14 +113,19 @@ contract DssVestTest is DSTest { gem = DSTokenLike ( chainlog.getAddress("MCD_GOV")); authority = MkrAuthorityLike( chainlog.getAddress("GOV_GUARD")); vat = VatLike( chainlog.getAddress("MCD_VAT")); - dai = DaiLike( chainlog.getAddress("MCD_DAI")); + dai = ERC20Like( chainlog.getAddress("MCD_DAI")); + daiJoin = chainlog.getAddress("MCD_JOIN_DAI"); + usds = ERC20Like( chainlog.getAddress("USDS")); + usdsJoin = chainlog.getAddress("USDS_JOIN"); end = EndLike( chainlog.getAddress("MCD_END")); VOW = chainlog.getAddress("MCD_VOW"); mVest = new DssVestMintable(address(gem)); mVest.file("cap", (2000 * WAD) / (4 * 365 days)); - sVest = new DssVestSuckable(address(chainlog)); + sVest = new DssVestSuckable(address(chainlog), daiJoin); sVest.file("cap", (2000 * WAD) / (4 * 365 days)); + sVestUsds = new DssVestSuckable(address(chainlog), usdsJoin); + sVestUsds.file("cap", (2000 * WAD) / (4 * 365 days)); boss = new Manager(); tVest = new DssVestTransferrable(address(boss), address(dai)); tVest.file("cap", (2000 * WAD) / (4 * 365 days)); @@ -139,6 +148,13 @@ contract DssVestTest is DSTest { ); assertEq(vat.wards(address(sVest)), 1); + hevm.store( + address(vat), + keccak256(abi.encode(address(sVestUsds), uint256(0))), + bytes32(uint256(1)) + ); + assertEq(vat.wards(address(sVestUsds)), 1); + // Give boss 10000 DAI hevm.store( address(dai), @@ -146,6 +162,14 @@ contract DssVestTest is DSTest { bytes32(uint256(10000 * WAD)) ); assertEq(dai.balanceOf(address(boss)), 10000 * WAD); + + // Give boss 10000 USDS + hevm.store( + address(usds), + keccak256(abi.encode(address(boss), uint(2))), + bytes32(uint256(10000 * WAD)) + ); + assertEq(usds.balanceOf(address(boss)), 10000 * WAD); } function testCost() public { @@ -670,6 +694,24 @@ contract DssVestTest is DSTest { assertEq(vat.sin(VOW), originalSin + 100 * days_vest * RAY); } + function testSuckableVestUsds() public { + uint256 originalSin = vat.sin(VOW); + uint256 id = sVestUsds.create(address(this), 100 * days_vest, block.timestamp, 100 days, 0, address(0)); + assertTrue(sVestUsds.valid(id)); + hevm.warp(block.timestamp + 1 days); + sVestUsds.vest(id); + assertEq(usds.balanceOf(address(this)), 1 * days_vest); + assertEq(vat.sin(VOW), originalSin + 1 * days_vest * RAY); + hevm.warp(block.timestamp + 9 days); + sVestUsds.vest(id); + assertEq(usds.balanceOf(address(this)), 10 * days_vest); + assertEq(vat.sin(VOW), originalSin + 10 * days_vest * RAY); + hevm.warp(block.timestamp + 365 days); + sVestUsds.vest(id); + assertEq(usds.balanceOf(address(this)), 100 * days_vest); + assertEq(vat.sin(VOW), originalSin + 100 * days_vest * RAY); + } + function testSuckableVestCaged() public { uint256 originalSin = vat.sin(VOW); uint256 id = sVest.create(address(this), 100 * days_vest, block.timestamp, 100 days, 0, address(0));