From 9eb3e261aaa556280ba72c96a604a5c169ef75e0 Mon Sep 17 00:00:00 2001 From: sunbreak1211 <129470872+sunbreak1211@users.noreply.github.com> Date: Mon, 21 Oct 2024 11:16:20 -0300 Subject: [PATCH] Add Certora specs (#48) * Certora setup (#37) * builtin sanity, pre_condition rule * folders * more rules with advanced CVL properties * document examples * more options for ClipperCallee concrete implementations * fix also fr Clipper * where am I taken from * fix * remove kick summarization * remove kick * update links * added rule sanity to configs * added basic multicall spec * adds a test solidity contract for multicall * final setup touches and multicall * added certora files and vim to gitignore --------- Co-authored-by: EyalHochCertora Co-authored-by: EyalHCertora <91595356+EyalHochCertora@users.noreply.github.com> * LockstakeUrn * Fix file header * Use real Vat code and some changes to urn conf * Use double quotes * Add LockstakeMkr spec * Fix * Revert removal of end line * LockstakeEngine (WIP) + Minor change for LockstakeUrn * Remove space * Remove factory from voteDelegate file * Add missing check for selectVoteDelegate + add selectFarm and selectFarm_revert specs * Add lock spec + minor changes to others * lock_revert spec * Improve comments * lockNgt and lockNgt_revert specs * Add free and feeeNgt specs * Add free_revert and freeNgt_revert specs * Add some new invariant rules + tidy up * Add freeNoFee and freeNoFee_revert specs * Simplify messages for non revert rules * Add draw and draw_revert specs * Add wipe, wipeAll and getReward specs * Add wipe_revert and onKick specs * Add wipeAll_revert spec * Add getReward_revert spec * farm renaming + minor changes * Add onKick_revert spec + minor comments fix * Fixes for inkMatchesLsmkrFarm * Add onTake and onTake_revert specs * Add onRemove and onRemove_revert specs * Separate Multicall rules to different file + fix wipe_revert * Minor changes * Comment change * First batch of LocstakeClipper specs * Add redo and redo_specs + fix in storageAffected * Clean up * Fix specs timeouts for LockstakeEngine * Add take spec + changes to storageAffected * stopped revert conditions better matching with code * Add take_revert spec * Clipper: some variables renaming * Add upchost upchost_revert specs * Fix for take spec + add yank and yank_revert specs * Engine: Rename several variables * Update specs to newer version * Remove unused function * Fix CI * Fix missing solc versions CI * Fix timeouts * Fix * Change * Some cleaning in multicall specs * Add more invariants to LockstakeEngine * Improve invariants for staking * Fix * Changes in invariants * Include view functions invariants as well * Fix --------- Co-authored-by: Shoham Shamir <123297287+shoham-certora@users.noreply.github.com> Co-authored-by: EyalHochCertora Co-authored-by: EyalHCertora <91595356+EyalHochCertora@users.noreply.github.com> --- .github/workflows/certora.yml | 54 + .gitignore | 6 + Makefile | 6 + certora/LockstakeClipper.conf | 88 + certora/LockstakeClipper.spec | 1034 +++++++++++ certora/LockstakeEngine.conf | 99 + certora/LockstakeEngine.spec | 2197 +++++++++++++++++++++++ certora/LockstakeEngineMulticall.conf | 57 + certora/LockstakeEngineMulticall.spec | 97 + certora/LockstakeMkr.conf | 12 + certora/LockstakeMkr.spec | 329 ++++ certora/LockstakeUrn.conf | 34 + certora/LockstakeUrn.spec | 180 ++ certora/harness/MulticallExecutor.sol | 43 + certora/harness/StakingRewards2Mock.sol | 11 + certora/harness/VoteDelegate2Mock.sol | 11 + certora/harness/dss/ClipperCallee.sol | 102 ++ certora/harness/dss/Dog.sol | 249 +++ certora/harness/dss/Jug.sol | 154 ++ certora/harness/dss/Spotter.sol | 133 ++ certora/harness/dss/Vat.sol | 270 +++ certora/harness/tokens/MkrMock.sol | 11 + certora/harness/tokens/RewardsMock.sol | 11 + certora/harness/tokens/SkyMock.sol | 11 + 24 files changed, 5199 insertions(+) create mode 100644 .github/workflows/certora.yml create mode 100644 Makefile create mode 100644 certora/LockstakeClipper.conf create mode 100644 certora/LockstakeClipper.spec create mode 100644 certora/LockstakeEngine.conf create mode 100644 certora/LockstakeEngine.spec create mode 100644 certora/LockstakeEngineMulticall.conf create mode 100644 certora/LockstakeEngineMulticall.spec create mode 100644 certora/LockstakeMkr.conf create mode 100644 certora/LockstakeMkr.spec create mode 100644 certora/LockstakeUrn.conf create mode 100644 certora/LockstakeUrn.spec create mode 100644 certora/harness/MulticallExecutor.sol create mode 100644 certora/harness/StakingRewards2Mock.sol create mode 100644 certora/harness/VoteDelegate2Mock.sol create mode 100644 certora/harness/dss/ClipperCallee.sol create mode 100644 certora/harness/dss/Dog.sol create mode 100644 certora/harness/dss/Jug.sol create mode 100644 certora/harness/dss/Spotter.sol create mode 100644 certora/harness/dss/Vat.sol create mode 100644 certora/harness/tokens/MkrMock.sol create mode 100644 certora/harness/tokens/RewardsMock.sol create mode 100644 certora/harness/tokens/SkyMock.sol diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 00000000..105bdf0e --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,54 @@ +name: Certora + +on: [push, pull_request] + +jobs: + certora: + name: Certora + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + lockstake: + - urn + - lsmkr + - engine + - engine-multicall + - clipper + + steps: + - name: Checkout + uses: actions/checkout@v3 + with: + submodules: recursive + + - uses: actions/setup-java@v2 + with: + distribution: 'zulu' + java-version: '11' + java-package: jre + + - name: Set up Python 3.8 + uses: actions/setup-python@v3 + with: + python-version: 3.8 + + - name: Install solc-select + run: pip3 install solc-select + + - name: Solc Select 0.8.21 + run: solc-select install 0.8.21 + + - name: Solc Select 0.6.12 + run: solc-select install 0.6.12 + + - name: Solc Select 0.5.12 + run: solc-select install 0.5.12 + + - name: Install Certora + run: pip3 install certora-cli-beta + + - name: Verify ${{ matrix.lockstake }} + run: make certora-${{ matrix.lockstake }} results=1 + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.gitignore b/.gitignore index 85198aaa..f665798a 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,9 @@ docs/ # Dotenv file .env + +# Certora +.certora_internal + +# Vim +.*.swp diff --git a/Makefile b/Makefile new file mode 100644 index 00000000..7d592993 --- /dev/null +++ b/Makefile @@ -0,0 +1,6 @@ +PATH := ~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts/solc-0.6.12:~/.solc-select/artifacts/solc-0.8.21:$(PATH) +certora-urn :; PATH=${PATH} certoraRun certora/LockstakeUrn.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-lsmkr :; PATH=${PATH} certoraRun certora/LockstakeMkr.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-engine :; PATH=${PATH} certoraRun certora/LockstakeEngine.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-engine-multicall :; PATH=${PATH} certoraRun certora/LockstakeEngineMulticall.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-clipper :; PATH=${PATH} certoraRun certora/LockstakeClipper.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) diff --git a/certora/LockstakeClipper.conf b/certora/LockstakeClipper.conf new file mode 100644 index 00000000..94c4b77f --- /dev/null +++ b/certora/LockstakeClipper.conf @@ -0,0 +1,88 @@ +{ + "files": [ + "src/LockstakeClipper.sol", + "src/LockstakeEngine.sol", + "src/LockstakeUrn.sol", + "src/LockstakeMkr.sol", + "certora/harness/dss/Vat.sol", + "certora/harness/dss/Spotter.sol", + "certora/harness/dss/Dog.sol", + "certora/harness/dss/ClipperCallee.sol:BadGuy", + "certora/harness/dss/ClipperCallee.sol:RedoGuy", + "certora/harness/dss/ClipperCallee.sol:KickGuy", + "certora/harness/dss/ClipperCallee.sol:FileUintGuy", + "certora/harness/dss/ClipperCallee.sol:FileAddrGuy", + "certora/harness/dss/ClipperCallee.sol:YankGuy", + "test/mocks/VoteDelegateMock.sol", + "certora/harness/tokens/MkrMock.sol", + "test/mocks/StakingRewardsMock.sol" + ], + "solc_map": { + "LockstakeClipper": "solc-0.8.21", + "LockstakeEngine": "solc-0.8.21", + "LockstakeUrn": "solc-0.8.21", + "LockstakeMkr": "solc-0.8.21", + "Vat": "solc-0.5.12", + "Spotter": "solc-0.5.12", + "Dog": "solc-0.6.12", + "BadGuy": "solc-0.8.21", + "RedoGuy": "solc-0.8.21", + "KickGuy": "solc-0.8.21", + "FileUintGuy": "solc-0.8.21", + "FileAddrGuy": "solc-0.8.21", + "YankGuy": "solc-0.8.21", + "VoteDelegateMock": "solc-0.8.21", + "MkrMock": "solc-0.8.21", + "StakingRewardsMock": "solc-0.8.21" + }, + "solc_optimize_map": { + "LockstakeClipper": "200", + "LockstakeEngine": "200", + "LockstakeUrn": "200", + "LockstakeMkr": "200", + "Vat": "0", + "Spotter": "0", + "Dog": "0", + "BadGuy": "0", + "RedoGuy": "0", + "KickGuy": "0", + "FileUintGuy": "0", + "FileAddrGuy": "0", + "YankGuy": "0", + "VoteDelegateMock": "0", + "MkrMock": "0", + "StakingRewardsMock": "0", + }, + "link": [ + "LockstakeClipper:vat=Vat", + "LockstakeClipper:engine=LockstakeEngine", + "LockstakeClipper:dog=Dog", + "LockstakeClipper:spotter=Spotter", + "LockstakeEngine:vat=Vat", + "LockstakeEngine:mkr=MkrMock", + "LockstakeEngine:lsmkr=LockstakeMkr", + "LockstakeUrn:engine=LockstakeEngine", + "VoteDelegateMock:gov=MkrMock", + "StakingRewardsMock:stakingToken=LockstakeMkr", + "Dog:vat=Vat", + "BadGuy:clip=LockstakeClipper", + "RedoGuy:clip=LockstakeClipper", + "KickGuy:clip=LockstakeClipper", + "FileUintGuy:clip=LockstakeClipper", + "FileAddrGuy:clip=LockstakeClipper", + "YankGuy:clip=LockstakeClipper" + ], + "verify": "LockstakeClipper:certora/LockstakeClipper.spec", + "prover_args": [ + "-rewriteMSizeAllocations true" + ], + "smt_timeout": "7000", + "rule_sanity": "basic", + "optimistic_loop": true, + "optimistic_contract_recursion": true, + "contract_recursion_limit": "2", + "multi_assert_check": true, + "parametric_contracts": ["LockstakeClipper"], + "build_cache": true, + "msg": "LockstakeClipper" +} diff --git a/certora/LockstakeClipper.spec b/certora/LockstakeClipper.spec new file mode 100644 index 00000000..3db6b1f8 --- /dev/null +++ b/certora/LockstakeClipper.spec @@ -0,0 +1,1034 @@ +// LockstakeClipper.spec + +using LockstakeEngine as lockstakeEngine; +using LockstakeUrn as lockstakeUrn; +using LockstakeMkr as lsmkr; +using MkrMock as mkr; +using Vat as vat; +using Spotter as spotter; +using Dog as dog; +using VoteDelegateMock as voteDelegate; +using StakingRewardsMock as stakingRewards; +using BadGuy as badGuy; +using RedoGuy as redoGuy; +using KickGuy as kickGuy; +using FileUintGuy as fileUintGuy; +using FileAddrGuy as fileAddrGuy; +using YankGuy as yankGuy; + +methods { + // storage variables + function wards(address) external returns (uint256) envfree; + function dog() external returns (address) envfree; + function vow() external returns (address) envfree; + function spotter() external returns (address) envfree; + function calc() external returns (address) envfree; + function buf() external returns (uint256) envfree; + function tail() external returns (uint256) envfree; + function cusp() external returns (uint256) envfree; + function chip() external returns (uint64) envfree; + function tip() external returns (uint192) envfree; + function chost() external returns (uint256) envfree; + function kicks() external returns (uint256) envfree; + function active(uint256) external returns (uint256) envfree; + function sales(uint256) external returns (uint256,uint256,uint256,uint256,address,uint96,uint256) envfree; + function stopped() external returns (uint256) envfree; + function count() external returns (uint256) envfree; + function active(uint256) external returns (uint256) envfree; + // immutables + function ilk() external returns (bytes32) envfree; + // + function lockstakeEngine.wards(address) external returns (uint256) envfree; + function lockstakeEngine.urnAuctions(address) external returns (uint256) envfree; + function lockstakeEngine.urnVoteDelegates(address) external returns (address) envfree; + function lockstakeEngine.urnFarms(address) external returns (address) envfree; + function lockstakeEngine.ilk() external returns (bytes32) envfree; + function lockstakeEngine.fee() external returns (uint256) envfree; + function mkr.totalSupply() external returns (uint256) envfree; + function mkr.balanceOf(address) external returns (uint256) envfree; + function lsmkr.wards(address) external returns (uint256) envfree; + function lsmkr.totalSupply() external returns (uint256) envfree; + function lsmkr.allowance(address,address) external returns (uint256) envfree; + function lsmkr.balanceOf(address) external returns (uint256) envfree; + function stakingRewards.balanceOf(address) external returns (uint256) envfree; + function stakingRewards.totalSupply() external returns (uint256) envfree; + function voteDelegate.stake(address) external returns (uint256) envfree; + function vat.wards(address) external returns (uint256) envfree; + function vat.live() external returns (uint256) envfree; + function vat.can(address, address) external returns (uint256) envfree; + function vat.debt() external returns (uint256) envfree; + function vat.vice() external returns (uint256) envfree; + function vat.dai(address) external returns (uint256) envfree; + function vat.sin(address) external returns (uint256) envfree; + function vat.gem(bytes32,address) external returns (uint256) envfree; + function vat.ilks(bytes32) external returns (uint256,uint256,uint256,uint256,uint256) envfree; + function vat.urns(bytes32, address) external returns (uint256,uint256) envfree; + function spotter.ilks(bytes32) external returns (address,uint256) envfree; + function spotter.par() external returns (uint256) envfree; + function dog.wards(address) external returns (uint256) envfree; + function dog.chop(bytes32) external returns (uint256) envfree; + function dog.Dirt() external returns (uint256) envfree; + function dog.ilks(bytes32) external returns (address,uint256,uint256,uint256) envfree; + // + function _.peek() external => peekSummary() expect (uint256, bool); + function _.price(uint256,uint256) external => calcPriceSummary() expect (uint256); + function _.free(uint256) external => DISPATCHER(true); + function _.withdraw(uint256) external => DISPATCHER(true); + function _.withdraw(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + // `ClipperCallee` + // NOTE: this might result in recursion, since we linked all the `ClipperCallee` + // to the `LockstakeClipper`. + function _.clipperCall( + address, uint256, uint256, bytes + ) external => DISPATCHER(true); +} + +definition addrZero() returns address = 0x0000000000000000000000000000000000000000; +definition max_int256() returns mathint = 2^255 - 1; +definition WAD() returns mathint = 10^18; +definition RAY() returns mathint = 10^27; +definition _min(mathint x, mathint y) returns mathint = x < y ? x : y; + +ghost uint256 pipVal; +ghost bool pipOk; +function peekSummary() returns (uint256, bool) { + return (pipVal, pipOk); +} + +ghost uint256 calcPrice; +function calcPriceSummary() returns uint256 { + return calcPrice; +} + +ghost lockedGhost() returns uint256; + +hook Sstore locked uint256 n_locked { + havoc lockedGhost assuming lockedGhost@new() == n_locked; +} + +hook Sload uint256 value locked { + require lockedGhost() == value; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + uint256 anyUint256; + + mathint wardsBefore = wards(anyAddr); + address dogBefore = dog(); + address vowBefore = vow(); + address spotterBefore = spotter(); + address calcBefore = calc(); + mathint bufBefore = buf(); + mathint tailBefore = tail(); + mathint cuspBefore = cusp(); + mathint chipBefore = chip(); + mathint tipBefore = tip(); + mathint chostBefore = chost(); + mathint kicksBefore = kicks(); + mathint activeBefore = active(anyUint256); + mathint countBefore = count(); + mathint salesAnyPosBefore; mathint salesAnyTabBefore; mathint salesAnyLotBefore; mathint salesAnyTotBefore; address salesAnyUsrBefore; mathint salesAnyTicBefore; mathint salesAnyTopBefore; + salesAnyPosBefore, salesAnyTabBefore, salesAnyLotBefore, salesAnyTotBefore, salesAnyUsrBefore, salesAnyTicBefore, salesAnyTopBefore = sales(anyUint256); + mathint stoppedBefore = stopped(); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + address dogAfter = dog(); + address vowAfter = vow(); + address spotterAfter = spotter(); + address calcAfter = calc(); + mathint bufAfter = buf(); + mathint tailAfter = tail(); + mathint cuspAfter = cusp(); + mathint chipAfter = chip(); + mathint tipAfter = tip(); + mathint chostAfter = chost(); + mathint kicksAfter = kicks(); + mathint activeAfter = active(anyUint256); + mathint countAfter = count(); + mathint salesAnyPosAfter; mathint salesAnyTabAfter; mathint salesAnyLotAfter; mathint salesAnyTotAfter; address salesAnyUsrAfter; mathint salesAnyTicAfter; mathint salesAnyTopAfter; + salesAnyPosAfter, salesAnyTabAfter, salesAnyLotAfter, salesAnyTotAfter, salesAnyUsrAfter, salesAnyTicAfter, salesAnyTopAfter = sales(anyUint256); + mathint stoppedAfter = stopped(); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1"; + assert dogAfter != dogBefore => f.selector == sig:file(bytes32,address).selector, "Assert 2"; + assert vowAfter != vowBefore => f.selector == sig:file(bytes32,address).selector, "Assert 3"; + assert spotterAfter != spotterBefore => f.selector == sig:file(bytes32,address).selector, "Assert 4"; + assert calcAfter != calcBefore => f.selector == sig:file(bytes32,address).selector, "Assert 5"; + assert bufAfter != bufBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 6"; + assert tailAfter != tailBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 7"; + assert cuspAfter != cuspBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 8"; + assert chipAfter != chipBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 9"; + assert tipAfter != tipBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 10"; + assert chostAfter != chostBefore => f.selector == sig:upchost().selector, "Assert 11"; + assert kicksAfter != kicksBefore => f.selector == sig:kick(uint256,uint256,address,address).selector, "Assert 12"; + assert countAfter != countBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 13"; + assert activeAfter != activeBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 14"; + assert salesAnyPosAfter != salesAnyPosBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 15"; + assert salesAnyTabAfter != salesAnyTabBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 16"; + assert salesAnyLotAfter != salesAnyLotBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 17"; + assert salesAnyTotAfter != salesAnyTotBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 18"; + assert salesAnyUsrAfter != salesAnyUsrBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 19"; + assert salesAnyTicAfter != salesAnyTicBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:redo(uint256,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 20"; + assert salesAnyTopAfter != salesAnyTopBefore => f.selector == sig:kick(uint256,uint256,address,address).selector || f.selector == sig:redo(uint256,address).selector || f.selector == sig:take(uint256,uint256,uint256,address,bytes).selector || f.selector == sig:yank(uint256).selector, "Assert 21"; + assert stoppedAfter != stoppedBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 22"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 1, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on rely +rule rely_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting deny +rule deny(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + deny(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 0, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on deny +rule deny_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting file +rule file_uint256(bytes32 what, uint256 data) { + env e; + + mathint bufBefore = buf(); + mathint tailBefore = tail(); + mathint cuspBefore = cusp(); + mathint chipBefore = chip(); + mathint tipBefore = tip(); + mathint stoppedBefore = stopped(); + + file(e, what, data); + + mathint bufAfter = buf(); + mathint tailAfter = tail(); + mathint cuspAfter = cusp(); + mathint chipAfter = chip(); + mathint tipAfter = tip(); + mathint stoppedAfter = stopped(); + + assert what == to_bytes32(0x6275660000000000000000000000000000000000000000000000000000000000) => bufAfter == to_mathint(data), "Assert 1"; + assert what != to_bytes32(0x6275660000000000000000000000000000000000000000000000000000000000) => bufAfter == bufBefore, "Assert 2"; + assert what == to_bytes32(0x7461696c00000000000000000000000000000000000000000000000000000000) => tailAfter == to_mathint(data), "Assert 3"; + assert what != to_bytes32(0x7461696c00000000000000000000000000000000000000000000000000000000) => tailAfter == tailBefore, "Assert 4"; + assert what == to_bytes32(0x6375737000000000000000000000000000000000000000000000000000000000) => cuspAfter == to_mathint(data), "Assert 5"; + assert what != to_bytes32(0x6375737000000000000000000000000000000000000000000000000000000000) => cuspAfter == cuspBefore, "Assert 6"; + assert what == to_bytes32(0x6368697000000000000000000000000000000000000000000000000000000000) => chipAfter == data % (max_uint64 + 1), "Assert 7"; + assert what != to_bytes32(0x6368697000000000000000000000000000000000000000000000000000000000) => chipAfter == chipBefore, "Assert 8"; + assert what == to_bytes32(0x7469700000000000000000000000000000000000000000000000000000000000) => tipAfter == data % (max_uint192 + 1), "Assert 9"; + assert what != to_bytes32(0x7469700000000000000000000000000000000000000000000000000000000000) => tipAfter == tipBefore, "Assert 10"; + assert what == to_bytes32(0x73746f7070656400000000000000000000000000000000000000000000000000) => stoppedAfter == to_mathint(data), "Assert 11"; + assert what != to_bytes32(0x73746f7070656400000000000000000000000000000000000000000000000000) => stoppedAfter == stoppedBefore, "Assert 12"; +} + +// Verify revert rules on file +rule file_uint256_revert(bytes32 what, uint256 data) { + env e; + + mathint wardsSender = wards(e.msg.sender); + mathint locked = lockedGhost(); + + file@withrevert(e, what, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = locked != 0; + bool revert4 = what != to_bytes32(0x6275660000000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x7461696c00000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x6375737000000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x6368697000000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x7469700000000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x73746f7070656400000000000000000000000000000000000000000000000000); + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting file +rule file_address(bytes32 what, address data) { + env e; + + address spotterBefore = spotter(); + address dogBefore = dog(); + address vowBefore = vow(); + address calcBefore = calc(); + + file(e, what, data); + + address spotterAfter = spotter(); + address dogAfter = dog(); + address vowAfter = vow(); + address calcAfter = calc(); + + assert what == to_bytes32(0x73706f7474657200000000000000000000000000000000000000000000000000) => spotterAfter == data, "Assert 1"; + assert what != to_bytes32(0x73706f7474657200000000000000000000000000000000000000000000000000) => spotterAfter == spotterBefore, "Assert 2"; + assert what == to_bytes32(0x646f670000000000000000000000000000000000000000000000000000000000) => dogAfter == data, "Assert 3"; + assert what != to_bytes32(0x646f670000000000000000000000000000000000000000000000000000000000) => dogAfter == dogBefore, "Assert 4"; + assert what == to_bytes32(0x766f770000000000000000000000000000000000000000000000000000000000) => vowAfter == data, "Assert 5"; + assert what != to_bytes32(0x766f770000000000000000000000000000000000000000000000000000000000) => vowAfter == vowBefore, "Assert 6"; + assert what == to_bytes32(0x63616c6300000000000000000000000000000000000000000000000000000000) => calcAfter == data, "Assert 7"; + assert what != to_bytes32(0x63616c6300000000000000000000000000000000000000000000000000000000) => calcAfter == calcBefore, "Assert 8"; +} + +// Verify revert rules on file +rule file_address_revert(bytes32 what, address data) { + env e; + + mathint wardsSender = wards(e.msg.sender); + mathint locked = lockedGhost(); + + file@withrevert(e, what, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = locked != 0; + bool revert4 = what != to_bytes32(0x73706f7474657200000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x646f670000000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x766f770000000000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x63616c6300000000000000000000000000000000000000000000000000000000); + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting kick +rule kick(uint256 tab, uint256 lot, address usr, address kpr) { + env e; + + mathint kicksBefore = kicks(); + mathint countBefore = count(); + mathint id = kicksBefore + 1; + uint256 otherUint256; + require to_mathint(otherUint256) != id; + mathint salesOtherPosBefore; mathint salesOtherTabBefore; mathint salesOtherLotBefore; mathint salesOtherTotBefore; address salesOtherUsrBefore; mathint salesOtherTicBefore; mathint salesOtherTopBefore; + salesOtherPosBefore, salesOtherTabBefore, salesOtherLotBefore, salesOtherTotBefore, salesOtherUsrBefore, salesOtherTicBefore, salesOtherTopBefore = sales(otherUint256); + mathint vatDaiKprBefore = vat.dai(kpr); + address vow = vow(); + mathint vatSinVowBefore = vat.sin(vow); + bytes32 ilk = ilk(); + mathint engineUrnAuctionsUsrBefore = lockstakeEngine.urnAuctions(usr); + + mathint par = spotter.par(); + // Avoid division by zero + require par > 0; + mathint val; bool b; + val, b = peekSummary(); + mathint feedPrice = val * 10^9 * RAY() / par; + mathint buf = buf(); + mathint coin = tip() + tab * chip() / WAD(); + + kick(e, tab, lot, usr, kpr); + + mathint kicksAfter = kicks(); + mathint countAfter = count(); + mathint activeCountAfter = active(require_uint256(countAfter - 1)); + mathint salesIdPosAfter; mathint salesIdTabAfter; mathint salesIdLotAfter; mathint salesIdTotAfter; address salesIdUsrAfter; mathint salesIdTicAfter; mathint salesIdTopAfter; + salesIdPosAfter, salesIdTabAfter, salesIdLotAfter, salesIdTotAfter, salesIdUsrAfter, salesIdTicAfter, salesIdTopAfter = sales(require_uint256(id)); + mathint salesOtherPosAfter; mathint salesOtherTabAfter; mathint salesOtherLotAfter; mathint salesOtherTotAfter; address salesOtherUsrAfter; mathint salesOtherTicAfter; mathint salesOtherTopAfter; + salesOtherPosAfter, salesOtherTabAfter, salesOtherLotAfter, salesOtherTotAfter, salesOtherUsrAfter, salesOtherTicAfter, salesOtherTopAfter = sales(otherUint256); + mathint vatDaiKprAfter= vat.dai(kpr); + mathint vatSinVowAfter= vat.sin(vow); + mathint engineUrnAuctionsUsrAfter = lockstakeEngine.urnAuctions(usr); + + assert kicksAfter == kicksBefore + 1, "Assert 1"; + assert countAfter == countBefore + 1, "Assert 2"; + assert activeCountAfter == id, "Assert 3"; + assert salesIdPosAfter == countAfter - 1, "Assert 4"; + assert salesIdTabAfter == to_mathint(tab), "Assert 5"; + assert salesIdLotAfter == to_mathint(lot), "Assert 6"; + assert salesIdTotAfter == to_mathint(lot), "Assert 7"; + assert salesIdUsrAfter == usr, "Assert 8"; + assert salesIdTicAfter == e.block.timestamp % (max_uint96 + 1), "Assert 9"; + assert salesIdTopAfter == feedPrice * buf / RAY(), "Assert 10"; + assert salesOtherPosAfter == salesOtherPosBefore, "Assert 11"; + assert salesOtherTabAfter == salesOtherTabBefore, "Assert 12"; + assert salesOtherLotAfter == salesOtherLotBefore, "Assert 13"; + assert salesOtherTotAfter == salesOtherTotBefore, "Assert 14"; + assert salesOtherUsrAfter == salesOtherUsrBefore, "Assert 15"; + assert salesOtherTicAfter == salesOtherTicBefore, "Assert 16"; + assert salesOtherTopAfter == salesOtherTopBefore, "Assert 17"; + assert vatDaiKprAfter == vatDaiKprBefore + coin, "Assert 18"; + assert vatSinVowAfter == vatSinVowBefore + coin, "Assert 19"; + assert engineUrnAuctionsUsrAfter == engineUrnAuctionsUsrBefore + 1, "Assert 20"; +} + +// Verify revert rules on kick +rule kick_revert(uint256 tab, uint256 lot, address usr, address kpr) { + env e; + + require usr == lockstakeUrn; + address prevVoteDelegate = lockstakeEngine.urnVoteDelegates(usr); + require prevVoteDelegate == addrZero() || prevVoteDelegate == voteDelegate; + address prevFarm = lockstakeEngine.urnFarms(usr); + require prevFarm == addrZero() || prevFarm == stakingRewards; + + mathint wardsSender = wards(e.msg.sender); + mathint locked = lockedGhost(); + mathint stopped = stopped(); + mathint kicks = kicks(); + mathint count = count(); + mathint buf = buf(); + mathint par = spotter.par(); + bytes32 ilk = ilk(); + mathint vatUrnsIlkUsrInk; mathint a; + vatUrnsIlkUsrInk, a = vat.urns(ilk, usr); + // Avoid division by zero + require par > 0; + mathint val; bool has; + val, has = peekSummary(); + mathint feedPrice = val * 10^9 * RAY() / par; + mathint chip = chip(); + mathint coin = tip() + tab * chip / WAD(); + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lockstakeEngine.wards(currentContract) == 1; + // Happening in urn (usr) init + require lsmkr.allowance(usr, lockstakeEngine) == max_uint256; + // Tokens invariants + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(prevFarm) + lsmkr.balanceOf(usr) + lsmkr.balanceOf(lockstakeEngine); + require stakingRewards.totalSupply() >= stakingRewards.balanceOf(usr); + // VoteDelegate assumptions + require prevVoteDelegate == addrZero() || to_mathint(voteDelegate.stake(lockstakeEngine)) >= vatUrnsIlkUsrInk + lot; + require prevVoteDelegate == addrZero() || mkr.balanceOf(voteDelegate) >= voteDelegate.stake(lockstakeEngine); + // StakingRewards assumptions + require prevFarm == addrZero() && lsmkr.balanceOf(usr) >= lot || + prevFarm != addrZero() && to_mathint(stakingRewards.balanceOf(usr)) >= vatUrnsIlkUsrInk + lot && to_mathint(lsmkr.balanceOf(prevFarm)) >= vatUrnsIlkUsrInk + lot; + // Practical Vat assumptions + require vat.sin(vow()) + coin <= max_uint256; + require vat.dai(kpr) + coin <= max_uint256; + require vat.vice() + coin <= max_uint256; + require vat.debt() + coin <= max_uint256; + // Practical assumption (vatUrnsIlkUsrInk + lot should be the same than the vatUrnsIlkUsrInk prev to the kick call) + require vatUrnsIlkUsrInk + lot <= max_uint256; + // LockstakeEngine assumption + require lockstakeEngine.urnAuctions(usr) < max_uint256; + require lockstakeEngine.ilk() == ilk; + + kick@withrevert(e, tab, lot, usr, kpr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = locked != 0; + bool revert4 = stopped >= 1; + bool revert5 = tab == 0; + bool revert6 = lot == 0; + bool revert7 = to_mathint(lot) > max_int256(); + bool revert8 = usr == addrZero(); + bool revert9 = kicks == max_uint256; + bool revert10 = count == max_uint256; + bool revert11 = !has; + bool revert12 = val * 10^9 * RAY() > max_uint256; + bool revert13 = feedPrice * buf > max_uint256; + bool revert14 = feedPrice * buf / RAY() == 0; + bool revert15 = tab * chip > max_uint256; + bool revert16 = coin > max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7 || revert8 || revert9 || + revert10 || revert11 || revert12 || + revert13 || revert14 || revert15 || + revert16, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting redo +rule redo(uint256 id, address kpr) { + env e; + + uint256 otherUint256; + require otherUint256 != id; + + mathint chost = chost(); + mathint a; address b; + mathint salesIdTab; mathint salesIdLot; mathint salesIdTicBefore; mathint salesIdTopBefore; + a, salesIdTab, salesIdLot, a, b, salesIdTicBefore, salesIdTopBefore = sales(id); + mathint salesOtherTicBefore; mathint salesOtherTopBefore; + a, a, a, a, b, salesOtherTicBefore, salesOtherTopBefore = sales(otherUint256); + mathint vatDaiKprBefore = vat.dai(kpr); + address vow = vow(); + mathint vatSinVowBefore = vat.sin(vow); + + mathint par = spotter.par(); + // Avoid division by zero + require par > 0; + mathint val; bool c; + val, c = peekSummary(); + mathint feedPrice = val * 10^9 * RAY() / par; + mathint buf = buf(); + mathint coin = tip() + salesIdTab * chip() / WAD(); + bool paysKpr = salesIdTab >= chost && salesIdLot * feedPrice >= chost; + + redo(e, id, kpr); + + mathint salesIdTicAfter; mathint salesIdTopAfter; + a, a, a, a, b, salesIdTicAfter, salesIdTopAfter = sales(id); + mathint salesOtherTicAfter; mathint salesOtherTopAfter; + a, a, a, a, b, salesOtherTicAfter, salesOtherTopAfter = sales(otherUint256); + mathint vatDaiKprAfter = vat.dai(kpr); + mathint vatSinVowAfter = vat.sin(vow); + + assert salesIdTicAfter == e.block.timestamp % (max_uint96 + 1), "Assert 1"; + assert salesIdTopAfter == feedPrice * buf / RAY(), "Assert 2"; + assert salesOtherTicAfter == salesOtherTicBefore, "Assert 3"; + assert salesOtherTopAfter == salesOtherTopBefore, "Assert 4"; + assert paysKpr => vatDaiKprAfter == vatDaiKprBefore + coin, "Assert 5"; + assert !paysKpr => vatDaiKprAfter == vatDaiKprBefore, "Assert 6"; + assert paysKpr => vatSinVowAfter == vatSinVowBefore + coin, "Assert 7"; + assert !paysKpr => vatSinVowAfter == vatSinVowBefore, "Assert 8"; +} + +// Verify revert rules on redo +rule redo_revert(uint256 id, address kpr) { + env e; + + mathint locked = lockedGhost(); + mathint stopped = stopped(); + mathint tail = tail(); + mathint cusp = cusp(); + mathint chost = chost(); + + mathint a; + mathint salesIdTab; mathint salesIdLot; address salesIdUsr; mathint salesIdTic; mathint salesIdTop; + a, salesIdTab, salesIdLot, a, salesIdUsr, salesIdTic, salesIdTop = sales(id); + + require to_mathint(e.block.timestamp) >= salesIdTic; + mathint price = calcPriceSummary(); + // Avoid division by zero + require salesIdTop > 0; + bool done = e.block.timestamp - salesIdTic > tail || price * RAY() / salesIdTop < cusp; + + mathint par = spotter.par(); + // Avoid division by zero + require par > 0; + mathint val; bool has; + val, has = peekSummary(); + mathint feedPrice = val * 10^9 * RAY() / par; + mathint buf = buf(); + mathint tip = tip(); + mathint chip = chip(); + mathint coin = tip + salesIdTab * chip() / WAD(); + bool paysKpr = salesIdTab >= chost && salesIdLot * feedPrice >= chost; + + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + // Practical Vat assumptions + require vat.sin(vow()) + coin <= max_uint256; + require vat.dai(kpr) + coin <= max_uint256; + require vat.vice() + coin <= max_uint256; + require vat.debt() + coin <= max_uint256; + + redo@withrevert(e, id, kpr); + + bool revert1 = e.msg.value > 0; + bool revert2 = locked != 0; + bool revert3 = stopped >= 2; + bool revert4 = salesIdUsr == addrZero(); + bool revert5 = to_mathint(e.block.timestamp) < salesIdTic; + bool revert6 = e.block.timestamp - salesIdTic <= tail && price * RAY() > max_uint256; + bool revert7 = !done; + bool revert8 = !has; + bool revert9 = val * 10^9 * RAY() > max_uint256; + bool revert10 = feedPrice * buf > max_uint256; + bool revert11 = feedPrice * buf / RAY() == 0; + bool revert12 = (tip > 0 || chip > 0) && salesIdTab >= chost && salesIdLot * feedPrice > max_uint256; + bool revert13 = paysKpr && salesIdTab * chip > max_uint256; + bool revert14 = paysKpr && coin > max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7 || revert8 || revert9 || + revert10 || revert11 || revert12 || + revert13 || revert14, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting take +rule take(uint256 id, uint256 amt, uint256 max, address who, bytes data) { + env e; + + bytes32 ilk = ilk(); + address vow = vow(); + + mathint countBefore = count(); + uint256 otherUint256; + require otherUint256 != id; + mathint activeLastBefore; + if (countBefore > 0) { + activeLastBefore = active(assert_uint256(countBefore - 1)); + } else { + activeLastBefore = 0; + } + + mathint salesIdPosBefore; mathint salesIdTabBefore; mathint salesIdLotBefore; mathint salesIdTotBefore; address salesIdUsrBefore; mathint salesIdTicBefore; mathint salesIdTopBefore; + salesIdPosBefore, salesIdTabBefore, salesIdLotBefore, salesIdTotBefore, salesIdUsrBefore, salesIdTicBefore, salesIdTopBefore = sales(id); + require salesIdUsrBefore == lockstakeUrn; + mathint salesOtherPosBefore; mathint salesOtherTabBefore; mathint salesOtherLotBefore; mathint salesOtherTotBefore; address salesOtherUsrBefore; mathint salesOtherTicBefore; mathint salesOtherTopBefore; + salesOtherPosBefore, salesOtherTabBefore, salesOtherLotBefore, salesOtherTotBefore, salesOtherUsrBefore, salesOtherTicBefore, salesOtherTopBefore = sales(otherUint256); + mathint vatGemIlkClipperBefore = vat.gem(ilk, currentContract); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(lockstakeEngine); + mathint mkrBalanceOfWhoBefore = mkr.balanceOf(who); + mathint vatDaiSenderBefore = vat.dai(e.msg.sender); + mathint vatDaiVowBefore = vat.dai(vow); + mathint dogDirtBefore = dog.Dirt(); + address a; mathint b; + mathint dogIlkDirtBefore; + a, b, b, dogIlkDirtBefore = dog.ilks(ilk); + mathint vatUrnsIlkUsrInkBefore; + vatUrnsIlkUsrInkBefore, b = vat.urns(ilk, salesIdUsrBefore); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUsrBefore = lsmkr.balanceOf(salesIdUsrBefore); + mathint engineUrnAuctionsUsrBefore = lockstakeEngine.urnAuctions(salesIdUsrBefore); + + mathint price = calcPriceSummary(); + // Avoid division by zero + require price > 0; + // Token invariants + require mkrTotalSupplyBefore >= mkrBalanceOfEngineBefore + mkrBalanceOfWhoBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUsrBefore; + // LockstakeEngine assumption + require lockstakeEngine.ilk() == ilk; + // Governance setting assumption + require vow != e.msg.sender; + + mathint sliceAux = _min(salesIdLotBefore, amt); + mathint oweAux = sliceAux * price; + mathint chost = chost(); + mathint slice; mathint owe; + if (oweAux > salesIdTabBefore) { + owe = salesIdTabBefore; + slice = owe / price; + } else { + if (oweAux < salesIdTabBefore && sliceAux < salesIdLotBefore) { + if (salesIdTabBefore - oweAux < chost) { + owe = salesIdTabBefore - chost; + slice = owe / price; + } else { + owe = oweAux; + slice = sliceAux; + } + } else { + owe = oweAux; + slice = sliceAux; + } + } + mathint calcTabAfter = salesIdTabBefore - owe; + mathint calcLotAfter = salesIdLotBefore - slice; + bool isRemoved = calcLotAfter == 0 || calcTabAfter == 0; + mathint fee = lockstakeEngine.fee(); + // Happening in kick + require salesIdLotBefore <= max_int256(); + require salesIdTotBefore >= salesIdLotBefore; + // Happening in Engine constructor + require fee < WAD(); + mathint sold = calcLotAfter == 0 ? salesIdTotBefore : (calcTabAfter == 0 ? salesIdTotBefore - calcLotAfter : 0); + mathint left = calcTabAfter == 0 ? calcLotAfter : 0; + mathint burn = _min(sold * fee / (WAD() - fee), left); + mathint refund = left - burn; + + take(e, id, amt, max, who, data); + + mathint kicksAfter = kicks(); + mathint countAfter = count(); + mathint activeCountAfter = active(require_uint256(countAfter - 1)); + mathint salesIdPosAfter; mathint salesIdTabAfter; mathint salesIdLotAfter; mathint salesIdTotAfter; address salesIdUsrAfter; mathint salesIdTicAfter; mathint salesIdTopAfter; + salesIdPosAfter, salesIdTabAfter, salesIdLotAfter, salesIdTotAfter, salesIdUsrAfter, salesIdTicAfter, salesIdTopAfter = sales(id); + mathint salesOtherPosAfter; mathint salesOtherTabAfter; mathint salesOtherLotAfter; mathint salesOtherTotAfter; address salesOtherUsrAfter; mathint salesOtherTicAfter; mathint salesOtherTopAfter; + salesOtherPosAfter, salesOtherTabAfter, salesOtherLotAfter, salesOtherTotAfter, salesOtherUsrAfter, salesOtherTicAfter, salesOtherTopAfter = sales(otherUint256); + mathint vatGemIlkClipperAfter = vat.gem(ilk, currentContract); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(lockstakeEngine); + mathint mkrBalanceOfWhoAfter = mkr.balanceOf(who); + mathint vatDaiSenderAfter = vat.dai(e.msg.sender); + mathint vatDaiVowAfter = vat.dai(vow); + mathint dogDirtAfter = dog.Dirt(); + mathint dogIlkDirtAfter; + a, b, b, dogIlkDirtAfter = dog.ilks(ilk); + mathint vatUrnsIlkUsrInkAfter; + vatUrnsIlkUsrInkAfter, b = vat.urns(ilk, salesIdUsrBefore); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUsrAfter = lsmkr.balanceOf(salesIdUsrBefore); + mathint engineUrnAuctionsUsrAfter = lockstakeEngine.urnAuctions(salesIdUsrBefore); + + assert countAfter == (isRemoved ? countBefore - 1 : countBefore), "Assert 1"; + assert salesIdPosAfter == (isRemoved ? 0 : salesIdPosBefore), "Assert 2"; + assert salesIdTabAfter == (isRemoved ? 0 : calcTabAfter), "Assert 3"; + assert salesIdLotAfter == (isRemoved ? 0 : calcLotAfter), "Assert 4"; + assert salesIdTotAfter == (isRemoved ? 0 : salesIdTotBefore), "Assert 5"; + assert salesIdUsrAfter == (isRemoved ? addrZero() : salesIdUsrBefore), "Assert 6"; + assert salesIdTicAfter == (isRemoved ? 0 : salesIdTicBefore), "Assert 7"; + assert salesIdTopAfter == (isRemoved ? 0 : salesIdTopBefore), "Assert 8"; + assert salesOtherPosAfter == (to_mathint(otherUint256) == activeLastBefore && isRemoved ? salesIdPosBefore : salesOtherPosBefore), "Assert 9"; + assert salesOtherTabAfter == salesOtherTabBefore, "Assert 10"; + assert salesOtherLotAfter == salesOtherLotBefore, "Assert 11"; + assert salesOtherTotAfter == salesOtherTotBefore, "Assert 12"; + assert salesOtherUsrAfter == salesOtherUsrBefore, "Assert 13"; + assert salesOtherTicAfter == salesOtherTicBefore, "Assert 14"; + assert salesOtherTopAfter == salesOtherTopBefore, "Assert 15"; + assert vatGemIlkClipperAfter == vatGemIlkClipperBefore - (calcLotAfter > 0 && calcTabAfter == 0 ? salesIdLotBefore : slice), "Assert 16"; + assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - burn, "Assert 17"; + assert who == lockstakeEngine => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - burn, "Assert 18"; + assert who != lockstakeEngine => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - slice - burn, "Assert 19"; + assert who != lockstakeEngine && who != salesIdUsrBefore => mkrBalanceOfWhoAfter == mkrBalanceOfWhoBefore + slice, "Assert 20"; + assert vatDaiSenderAfter == vatDaiSenderBefore - owe, "Assert 21"; + assert vatDaiVowAfter == vatDaiVowBefore + owe, "Assert 22"; + assert dogDirtAfter == dogDirtBefore - (calcLotAfter == 0 ? salesIdTabBefore : owe), "Assert 23"; + assert dogIlkDirtAfter == dogIlkDirtBefore - (calcLotAfter == 0 ? salesIdTabBefore : owe), "Assert 24"; + assert vatUrnsIlkUsrInkAfter == vatUrnsIlkUsrInkBefore + refund, "Assert 25"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore + refund, "Assert 26"; + assert lsmkrBalanceOfUsrAfter == lsmkrBalanceOfUsrBefore + refund, "Assert 27"; + assert engineUrnAuctionsUsrAfter == engineUrnAuctionsUsrBefore - (isRemoved ? 1 : 0), "Assert 28"; +} + +// Verify revert rules on take +rule take_revert(uint256 id, uint256 amt, uint256 max, address who, bytes data) { + env e; + + require e.msg.sender != currentContract; + + bytes32 ilk = ilk(); + address vow = vow(); + mathint locked = lockedGhost(); + mathint stopped = stopped(); + mathint tail = tail(); + mathint cusp = cusp(); + mathint chost = chost(); + mathint count = count(); + mathint activeLast; + if (count > 0) { + activeLast = active(assert_uint256(count - 1)); + } else { + activeLast = 0; + } + + mathint salesIdPos; mathint salesIdTab; mathint salesIdLot; mathint salesIdTot; address salesIdUsr; mathint salesIdTic; mathint salesIdTop; + salesIdPos, salesIdTab, salesIdLot, salesIdTot, salesIdUsr, salesIdTic, salesIdTop = sales(id); + + mathint vatGemIlkClipper = vat.gem(ilk, currentContract); + mathint vatCanSenderClipper = vat.can(e.msg.sender, currentContract); + mathint vatDaiSender = vat.dai(e.msg.sender); + + mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkDust; mathint a; + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, a, vatIlksIlkDust = vat.ilks(ilk); + mathint vatUrnsIlkUsrInk; mathint vatUrnsIlkUsrArt; + vatUrnsIlkUsrInk, vatUrnsIlkUsrArt = vat.urns(ilk, salesIdUsr); + + mathint dogDirt = dog.Dirt(); + address b; mathint dogIlkDirt; + b, a, a, dogIlkDirt = dog.ilks(ilk); + + require to_mathint(e.block.timestamp) >= salesIdTic; + mathint price = calcPriceSummary(); + // Avoid division by zero + require salesIdTop > 0; + bool done = e.block.timestamp - salesIdTic > tail || price * RAY() / salesIdTop < cusp; + + mathint sliceAux = _min(salesIdLot, amt); + mathint oweAux = sliceAux * price; + mathint slice; mathint owe; + if (oweAux > salesIdTab) { + owe = salesIdTab; + slice = owe / price; + } else { + if (oweAux < salesIdTab && sliceAux < salesIdLot) { + if (salesIdTab - oweAux < chost) { + owe = salesIdTab - chost; + slice = price > 0 ? owe / price : max_uint256; // Just a placeholder if price == 0 + } else { + owe = oweAux; + slice = sliceAux; + } + } else { + owe = oweAux; + slice = sliceAux; + } + } + mathint calcTabAfter = salesIdTab - owe; + mathint calcLotAfter = salesIdLot - slice; + mathint digAmt = calcLotAfter == 0 ? salesIdTab : owe; + bool isRemoved = calcLotAfter == 0 || calcTabAfter == 0; + mathint fee = lockstakeEngine.fee(); + + // Happening in kick + require salesIdLot <= max_int256(); + require salesIdTot >= salesIdLot; + // Happening in Engine constructor + require fee < WAD(); + require lsmkr.wards(lockstakeEngine) == 1; + mathint sold = calcLotAfter == 0 ? salesIdTot : (calcTabAfter == 0 ? salesIdTot - calcLotAfter : 0); + mathint left = calcTabAfter == 0 ? calcLotAfter : 0; + mathint burn = _min(sold * fee / (WAD() - fee), left); + mathint refund = left - burn; + // Happening in urn init + require vat.can(salesIdUsr, lockstakeEngine) == 1; + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(lockstakeEngine) + mkr.balanceOf(who); + require lsmkr.totalSupply() >= mkr.balanceOf(salesIdUsr); + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require vat.wards(lockstakeEngine) == 1; + require dog.wards(currentContract) == 1; + require lockstakeEngine.wards(currentContract) == 1; + // LockstakeEngine assumtions + require lockstakeEngine.ilk() == ilk; + require to_mathint(mkr.balanceOf(lockstakeEngine)) >= slice + burn; + require lockstakeEngine.urnAuctions(salesIdUsr) > 0; + require sold * fee <= max_uint256; + require refund <= max_int256(); + require vat.gem(ilk, salesIdUsr) + refund <= max_uint256; + require salesIdUsr != addrZero() && salesIdUsr != lsmkr; + require lsmkr.totalSupply() + refund <= max_uint256; + // Dog assumptions + require dogDirt >= digAmt; + require dogIlkDirt >= digAmt; + // Practical Vat assumptions + require vat.live() == 1; + require vat.dai(vow) + owe <= max_uint256; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require vatUrnsIlkUsrInk + refund <= max_uint256; + require (vatUrnsIlkUsrInk + refund) * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUsrArt; + require vatUrnsIlkUsrArt == 0 || vatIlksIlkRate * vatUrnsIlkUsrArt >= vatIlksIlkDust; + + take@withrevert(e, id, amt, max, who, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = locked != 0; + bool revert3 = stopped >= 3; + bool revert4 = salesIdUsr == addrZero(); + bool revert5 = price * RAY() > max_uint256; + bool revert6 = done; + bool revert7 = to_mathint(max) < price; + bool revert8 = sliceAux * price > max_uint256; + bool revert9 = oweAux < salesIdTab && sliceAux < salesIdLot && salesIdTab - oweAux < chost && salesIdTab <= chost; + bool revert10 = oweAux < salesIdTab && sliceAux < salesIdLot && salesIdTab - oweAux < chost && price == 0; + bool revert11 = vatGemIlkClipper < slice; + bool revert12 = data.length > 0 && (who == badGuy || who == redoGuy || who == kickGuy || who == fileUintGuy || who == fileAddrGuy || who == yankGuy); + bool revert13 = vatCanSenderClipper != 1; + bool revert14 = vatDaiSender < owe; + bool revert15 = (calcLotAfter == 0 || calcTabAfter == 0) && count == 0; + bool revert16 = (calcLotAfter == 0 || calcTabAfter == 0) && to_mathint(id) != activeLast && salesIdPos > count - 1; + bool revert17 = calcLotAfter > 0 && calcTabAfter == 0 && vatGemIlkClipper < salesIdLot; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7 || revert8 || revert9 || + revert10 || revert11 || revert12 || + revert13 || revert14 || revert15 || + revert16 || revert17, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting upchost +rule upchost() { + env e; + + bytes32 ilk = ilk(); + + mathint vatIlksIlkDust; mathint a; + a, a, a, a, vatIlksIlkDust = vat.ilks(ilk); + + mathint dogChopIlk = dog.chop(ilk); + + upchost(e); + + mathint chostAfter = chost(); + + assert chostAfter == vatIlksIlkDust * dogChopIlk / WAD(), "Assert 1"; +} + +// Verify revert rules on upchost +rule upchost_revert() { + env e; + + bytes32 ilk = ilk(); + + mathint vatIlksIlkDust; mathint a; + a, a, a, a, vatIlksIlkDust = vat.ilks(ilk); + + mathint dogChopIlk = dog.chop(ilk); + + upchost@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = vatIlksIlkDust * dogChopIlk > max_uint256; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting yank +rule yank(uint256 id) { + env e; + + require e.msg.sender != currentContract; + + bytes32 ilk = ilk(); + // address vow = vow(); + + mathint countBefore = count(); + uint256 otherUint256; + require otherUint256 != id; + mathint activeLastBefore; + if (countBefore > 0) { + activeLastBefore = active(assert_uint256(countBefore - 1)); + } else { + activeLastBefore = 0; + } + mathint a; address b; + mathint salesIdPosBefore; mathint salesIdTabBefore; mathint salesIdLotBefore; address salesIdUsrBefore; + salesIdPosBefore, salesIdTabBefore, salesIdLotBefore, a, salesIdUsrBefore, a, a = sales(id); + mathint salesOtherPosBefore; mathint salesOtherTabBefore; mathint salesOtherLotBefore; mathint salesOtherTotBefore; address salesOtherUsrBefore; mathint salesOtherTicBefore; mathint salesOtherTopBefore; + salesOtherPosBefore, salesOtherTabBefore, salesOtherLotBefore, salesOtherTotBefore, salesOtherUsrBefore, salesOtherTicBefore, salesOtherTopBefore = sales(otherUint256); + mathint dogDirtBefore = dog.Dirt(); + mathint dogIlkDirtBefore; + b, a, a, dogIlkDirtBefore = dog.ilks(ilk); + mathint vatGemIlkClipperBefore = vat.gem(ilk, currentContract); + mathint vatGemIlkSenderBefore = vat.gem(ilk, e.msg.sender); + mathint engineUrnAuctionsUsrBefore = lockstakeEngine.urnAuctions(salesIdUsrBefore); + + yank(e, id); + + mathint countAfter = count(); + mathint salesIdPosAfter; mathint salesIdTabAfter; mathint salesIdLotAfter; mathint salesIdTotAfter; address salesIdUsrAfter; mathint salesIdTicAfter; mathint salesIdTopAfter; + salesIdPosAfter, salesIdTabAfter, salesIdLotAfter, salesIdTotAfter, salesIdUsrAfter, salesIdTicAfter, salesIdTopAfter = sales(id); + mathint salesOtherPosAfter; mathint salesOtherTabAfter; mathint salesOtherLotAfter; mathint salesOtherTotAfter; address salesOtherUsrAfter; mathint salesOtherTicAfter; mathint salesOtherTopAfter; + salesOtherPosAfter, salesOtherTabAfter, salesOtherLotAfter, salesOtherTotAfter, salesOtherUsrAfter, salesOtherTicAfter, salesOtherTopAfter = sales(otherUint256); + mathint dogDirtAfter = dog.Dirt(); + mathint dogIlkDirtAfter; + b, a, a, dogIlkDirtAfter = dog.ilks(ilk); + mathint vatGemIlkClipperAfter = vat.gem(ilk, currentContract); + mathint vatGemIlkSenderAfter = vat.gem(ilk, e.msg.sender); + mathint engineUrnAuctionsUsrAfter = lockstakeEngine.urnAuctions(salesIdUsrBefore); + + assert countAfter == countBefore - 1, "Assert 1"; + assert salesIdPosAfter == 0, "Assert 2"; + assert salesIdTabAfter == 0, "Assert 3"; + assert salesIdLotAfter == 0, "Assert 4"; + assert salesIdTotAfter == 0, "Assert 5"; + assert salesIdUsrAfter == addrZero(), "Assert 6"; + assert salesIdTicAfter == 0, "Assert 7"; + assert salesIdTopAfter == 0, "Assert 8"; + assert salesOtherPosAfter == (to_mathint(otherUint256) == activeLastBefore ? salesIdPosBefore : salesOtherPosBefore), "Assert 9"; + assert salesOtherTabAfter == salesOtherTabBefore, "Assert 10"; + assert salesOtherLotAfter == salesOtherLotBefore, "Assert 11"; + assert salesOtherTotAfter == salesOtherTotBefore, "Assert 12"; + assert salesOtherUsrAfter == salesOtherUsrBefore, "Assert 13"; + assert salesOtherTicAfter == salesOtherTicBefore, "Assert 14"; + assert salesOtherTopAfter == salesOtherTopBefore, "Assert 15"; + assert dogDirtAfter == dogDirtBefore - salesIdTabBefore, "Assert 16"; + assert dogIlkDirtAfter == dogIlkDirtBefore - salesIdTabBefore, "Assert 17"; + assert vatGemIlkClipperAfter == vatGemIlkClipperBefore - salesIdLotBefore, "Assert 18"; + assert vatGemIlkSenderAfter == vatGemIlkSenderBefore + salesIdLotBefore, "Assert 19"; + assert engineUrnAuctionsUsrAfter == engineUrnAuctionsUsrBefore - 1, "Assert 20"; +} + +// Verify revert rules on yank +rule yank_revert(uint256 id) { + env e; + + require e.msg.sender != currentContract; + + mathint wardsSender = wards(e.msg.sender); + mathint locked = lockedGhost(); + bytes32 ilk = ilk(); + + mathint count = count(); + mathint activeLast; + if (count > 0) { + activeLast = active(assert_uint256(count - 1)); + } else { + activeLast = 0; + } + + mathint salesIdPos; mathint salesIdTab; mathint salesIdLot; address salesIdUsr; mathint a; + salesIdPos, salesIdTab, salesIdLot, a, salesIdUsr, a, a = sales(id); + + mathint engineWardsClipper = lockstakeEngine.wards(currentContract); + + mathint dogWardsClipper = dog.wards(currentContract); + mathint dogDirt = dog.Dirt(); + address b; mathint dogIlkDirt; + b, a, a, dogIlkDirt = dog.ilks(ilk); + + mathint vatGemIlkClipper = vat.gem(ilk, currentContract); + mathint vatGemIlkSender = vat.gem(ilk, e.msg.sender); + + // LockstakeEngine assumptions + require engineWardsClipper == 1; + require lockstakeEngine.urnAuctions(salesIdUsr) > 0; + // Dog assumptions + require dogWardsClipper == 1; + require dogDirt >= salesIdTab; + require dogIlkDirt >= salesIdTab; + // Vat assumption + require vatGemIlkSender + salesIdLot <= max_uint256; + + yank@withrevert(e, id); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = locked != 0; + bool revert4 = salesIdUsr == addrZero(); + bool revert5 = vatGemIlkClipper < salesIdLot; + bool revert6 = count == 0 || to_mathint(id) != activeLast && salesIdPos > count - 1; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6, "Revert rules failed"; +} diff --git a/certora/LockstakeEngine.conf b/certora/LockstakeEngine.conf new file mode 100644 index 00000000..a6d5fb03 --- /dev/null +++ b/certora/LockstakeEngine.conf @@ -0,0 +1,99 @@ +{ + "files": [ + "src/LockstakeEngine.sol", + "src/LockstakeUrn.sol", + "src/LockstakeMkr.sol", + "certora/harness/dss/Jug.sol", + "certora/harness/dss/Vat.sol", + "test/mocks/VoteDelegateMock.sol", + "certora/harness/VoteDelegate2Mock.sol", + "test/mocks/VoteDelegateMock.sol:VoteDelegateFactoryMock", + "test/mocks/UsdsJoinMock.sol", + "test/mocks/UsdsMock.sol", + "certora/harness/tokens/MkrMock.sol", + "test/mocks/MkrSkyMock.sol", + "certora/harness/tokens/SkyMock.sol", + "certora/harness/tokens/RewardsMock.sol", + "test/mocks/StakingRewardsMock.sol", + "certora/harness/StakingRewards2Mock.sol" + ], + "solc_map": { + "LockstakeEngine": "solc-0.8.21", + "LockstakeUrn": "solc-0.8.21", + "LockstakeMkr": "solc-0.8.21", + "Jug": "solc-0.5.12", + "Vat": "solc-0.5.12", + "VoteDelegateMock": "solc-0.8.21", + "VoteDelegate2Mock": "solc-0.8.21", + "VoteDelegateFactoryMock": "solc-0.8.21", + "UsdsJoinMock": "solc-0.8.21", + "UsdsMock": "solc-0.8.21", + "MkrMock": "solc-0.8.21", + "MkrSkyMock": "solc-0.8.21", + "SkyMock": "solc-0.8.21", + "StakingRewardsMock": "solc-0.8.21", + "StakingRewards2Mock": "solc-0.8.21", + "RewardsMock": "solc-0.8.21" + }, + "solc_optimize_map": { + "LockstakeEngine": "200", + "LockstakeUrn": "200", + "LockstakeMkr": "200", + "Jug": "0", + "Vat": "0", + "UsdsJoinMock": "0", + "UsdsMock": "0", + "MkrMock": "0", + "MkrSkyMock": "0", + "SkyMock": "0", + "VoteDelegateMock": "0", + "VoteDelegate2Mock": "0", + "VoteDelegateFactoryMock": "0", + "StakingRewardsMock": "0", + "StakingRewards2Mock": "0", + "RewardsMock": "0" + }, + "link": [ + "LockstakeEngine:jug=Jug", + "LockstakeEngine:voteDelegateFactory=VoteDelegateFactoryMock", + "LockstakeEngine:vat=Vat", + "LockstakeEngine:usdsJoin=UsdsJoinMock", + "LockstakeEngine:usds=UsdsMock", + "LockstakeEngine:mkr=MkrMock", + "LockstakeEngine:lsmkr=LockstakeMkr", + "LockstakeEngine:mkrSky=MkrSkyMock", + "LockstakeEngine:sky=SkyMock", + "LockstakeEngine:urnImplementation=LockstakeUrn", + "LockstakeUrn:engine=LockstakeEngine", + "LockstakeUrn:lsmkr=LockstakeMkr", + "LockstakeUrn:vat=Vat", + "Jug:vat=Vat", + "UsdsJoinMock:vat=Vat", + "UsdsJoinMock:usds=UsdsMock", + "MkrSkyMock:mkr=MkrMock", + "MkrSkyMock:sky=SkyMock", + "VoteDelegateMock:gov=MkrMock", + "VoteDelegate2Mock:gov=MkrMock", + "VoteDelegateFactoryMock:gov=MkrMock", + "StakingRewardsMock:rewardsToken=RewardsMock", + "StakingRewardsMock:stakingToken=LockstakeMkr", + "StakingRewards2Mock:rewardsToken=RewardsMock", + "StakingRewards2Mock:stakingToken=LockstakeMkr" + ], + "verify": "LockstakeEngine:certora/LockstakeEngine.spec", + "prover_args": [ + "-rewriteMSizeAllocations true", + "-smt_easy_LIA true" + ], + "smt_timeout": "7000", + "rule_sanity": "basic", + "optimistic_loop": true, + "multi_assert_check": true, + "parametric_contracts": ["LockstakeEngine"], + "build_cache": true, + "dynamic_bound": "1", + "prototype": [ + "3d602d80600a3d3981f3363d3d373d3d3d363d73=LockstakeUrn" + ], + "msg": "LockstakeEngine" +} diff --git a/certora/LockstakeEngine.spec b/certora/LockstakeEngine.spec new file mode 100644 index 00000000..6e68a596 --- /dev/null +++ b/certora/LockstakeEngine.spec @@ -0,0 +1,2197 @@ +// LockstakeEngine.spec + +using LockstakeUrn as lockstakeUrn; +using Vat as vat; +using MkrMock as mkr; +using LockstakeMkr as lsmkr; +using VoteDelegateMock as voteDelegate; +using VoteDelegate2Mock as voteDelegate2; +using VoteDelegateFactoryMock as voteDelegateFactory; +using StakingRewardsMock as stakingRewards; +using StakingRewards2Mock as stakingRewards2; +using MkrSkyMock as mkrSky; +using SkyMock as sky; +using UsdsMock as usds; +using UsdsJoinMock as usdsJoin; +using Jug as jug; +using RewardsMock as rewardsToken; + +methods { + // storage variables + function wards(address) external returns (uint256) envfree; + function farms(address) external returns (LockstakeEngine.FarmStatus) envfree; + function ownerUrnsCount(address) external returns (uint256) envfree; + function ownerUrns(address,uint256) external returns (address) envfree; + function urnOwners(address) external returns (address) envfree; + function urnCan(address,address) external returns (uint256) envfree; + function urnVoteDelegates(address) external returns (address) envfree; + function urnFarms(address) external returns (address) envfree; + function urnAuctions(address) external returns (uint256) envfree; + function jug() external returns (address) envfree; + function fee() external returns (uint256) envfree; + // immutables + function voteDelegateFactory() external returns (address) envfree; + function vat() external returns (address) envfree; + function usdsJoin() external returns (address) envfree; + function usds() external returns (address) envfree; + function ilk() external returns (bytes32) envfree; + function mkr() external returns (address) envfree; + function lsmkr() external returns (address) envfree; + function usds() external returns (address) envfree; + function sky() external returns (address) envfree; + function mkrSkyRate() external returns (uint256) envfree; + function urnImplementation() external returns (address) envfree; + // + function lockstakeUrn.engine() external returns (address) envfree; + function vat.live() external returns (uint256) envfree; + function vat.Line() external returns (uint256) envfree; + function vat.debt() external returns (uint256) envfree; + function vat.ilks(bytes32) external returns (uint256,uint256,uint256,uint256,uint256) envfree; + function vat.dai(address) external returns (uint256) envfree; + function vat.gem(bytes32,address) external returns (uint256) envfree; + function vat.urns(bytes32,address) external returns (uint256,uint256) envfree; + function vat.can(address,address) external returns (uint256) envfree; + function vat.wards(address) external returns (uint256) envfree; + function mkr.allowance(address,address) external returns (uint256) envfree; + function mkr.balanceOf(address) external returns (uint256) envfree; + function mkr.totalSupply() external returns (uint256) envfree; + function sky.allowance(address,address) external returns (uint256) envfree; + function sky.balanceOf(address) external returns (uint256) envfree; + function sky.totalSupply() external returns (uint256) envfree; + function lsmkr.allowance(address,address) external returns (uint256) envfree; + function lsmkr.balanceOf(address) external returns (uint256) envfree; + function lsmkr.totalSupply() external returns (uint256) envfree; + function lsmkr.wards(address) external returns (uint256) envfree; + function stakingRewards.balanceOf(address) external returns (uint256) envfree; + function stakingRewards.totalSupply() external returns (uint256) envfree; + function stakingRewards.rewardsToken() external returns (address) envfree; + function stakingRewards.rewards(address) external returns (uint256) envfree; + function stakingRewards2.balanceOf(address) external returns (uint256) envfree; + function stakingRewards2.totalSupply() external returns (uint256) envfree; + function mkrSky.rate() external returns (uint256) envfree; + function usds.allowance(address,address) external returns (uint256) envfree; + function usds.balanceOf(address) external returns (uint256) envfree; + function usds.totalSupply() external returns (uint256) envfree; + function jug.vow() external returns (address) envfree; + function rewardsToken.balanceOf(address) external returns (uint256) envfree; + function rewardsToken.totalSupply() external returns (uint256) envfree; + function voteDelegate.stake(address) external returns (uint256) envfree; + function voteDelegate2.stake(address) external returns (uint256) envfree; + function voteDelegateFactory.created(address) external returns (uint256) envfree; + // + function jug.drip(bytes32 ilk) external returns (uint256) => dripSummary(ilk); + function _.mul(uint256 x,int256 y) internal => mulISummary(x,y) expect int256; + function _.mul(uint256 x,uint256 y) internal => mulSummary(x,y) expect uint256; + function _.hope(address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.init() external => DISPATCHER(true); + function _.lock(uint256) external => DISPATCHER(true); + function _.free(uint256) external => DISPATCHER(true); + function _.stake(address,uint256,uint16) external => DISPATCHER(true); + function _.withdraw(address,uint256) external => DISPATCHER(true); + function _.stake(uint256,uint16) external => DISPATCHER(true); + function _.withdraw(uint256) external => DISPATCHER(true); + function _.getReward(address,address) external => DISPATCHER(true); + function _.getReward() external => DISPATCHER(true); + function _.rewardsToken() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); +} + +definition addrZero() returns address = 0x0000000000000000000000000000000000000000; +definition max_int256() returns mathint = 2^255 - 1; +definition min_int256() returns mathint = -2^255; +definition WAD() returns mathint = 10^18; +definition RAY() returns mathint = 10^27; +definition _divup(mathint x, mathint y) returns mathint = x != 0 ? ((x - 1) / y) + 1 : 0; +definition _min(mathint x, mathint y) returns mathint = x < y ? x : y; + +function mulISummary(uint256 x, int256 y) returns int256 { + require x <= max_int256(); + mathint z = x * y; + return require_int256(z); +} + +function mulSummary(uint256 x, uint256 y) returns uint256 { + mathint z = x * y; + return require_uint256(z); +} + +persistent ghost address createdUrn; +hook CREATE1(uint value, uint offset, uint length) address v { + createdUrn = v; +} + +persistent ghost address queriedUrn; +hook Sload address v ownerUrns[KEY address owner][KEY uint256 index] { + queriedUrn = v; +} + +persistent ghost address passedUrn; +hook Sload uint256 v urnAuctions[KEY address urn] { + passedUrn = urn; +} + +ghost mathint duty; +ghost mathint timeDiff; +function dripSummary(bytes32 ilk) returns uint256 { + env e; + require duty >= RAY(); + uint256 prev; uint256 a; + a, prev, a, a, a = vat.ilks(ilk); + uint256 rate = timeDiff == 0 ? prev : require_uint256(duty * timeDiff * prev / RAY()); + timeDiff = 0; + vat.fold(e, ilk, jug.vow(), require_int256(rate - prev)); + return rate; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } { + env e; + + address anyAddr; + address anyAddr2; + uint256 anyUint256; + + bytes32 ilk = ilk(); + + mathint wardsBefore = wards(anyAddr); + LockstakeEngine.FarmStatus farmsBefore = farms(anyAddr); + mathint ownerUrnsCountBefore = ownerUrnsCount(anyAddr); + address ownerUrnsBefore = ownerUrns(anyAddr, anyUint256); + address urnOwnersBefore = urnOwners(anyAddr); + mathint urnCanBefore = urnCan(anyAddr, anyAddr2); + address urnVoteDelegatesBefore = urnVoteDelegates(anyAddr); + address urnFarmsBefore = urnFarms(anyAddr); + mathint urnAuctionsBefore = urnAuctions(anyAddr); + address jugBefore = jug(); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + LockstakeEngine.FarmStatus farmsAfter = farms(anyAddr); + mathint ownerUrnsCountAfter = ownerUrnsCount(anyAddr); + address ownerUrnsAfter = ownerUrns(anyAddr, anyUint256); + address urnOwnersAfter = urnOwners(anyAddr); + mathint urnCanAfter = urnCan(anyAddr, anyAddr2); + address urnVoteDelegatesAfter = urnVoteDelegates(anyAddr); + address urnFarmsAfter = urnFarms(anyAddr); + mathint urnAuctionsAfter = urnAuctions(anyAddr); + address jugAfter = jug(); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1"; + assert farmsAfter != farmsBefore => f.selector == sig:addFarm(address).selector || f.selector == sig:delFarm(address).selector, "Assert 2"; + assert ownerUrnsCountAfter != ownerUrnsCountBefore => f.selector == sig:open(uint256).selector, "Assert 3"; + assert ownerUrnsAfter != ownerUrnsBefore => f.selector == sig:open(uint256).selector, "Assert 4"; + assert urnOwnersAfter != urnOwnersBefore => f.selector == sig:open(uint256).selector, "Assert 5"; + assert urnCanAfter != urnCanBefore => f.selector == sig:hope(address,uint256,address).selector || f.selector == sig:nope(address,uint256,address).selector, "Assert 6"; + assert urnVoteDelegatesAfter != urnVoteDelegatesBefore => f.selector == sig:selectVoteDelegate(address,uint256,address).selector || f.selector == sig:onKick(address,uint256).selector, "Assert 7"; + assert urnFarmsAfter != urnFarmsBefore => f.selector == sig:selectFarm(address,uint256,address,uint16).selector || f.selector == sig:onKick(address,uint256).selector, "Assert 8"; + assert urnAuctionsAfter != urnAuctionsBefore => f.selector == sig:onKick(address,uint256).selector || f.selector == sig:onRemove(address,uint256,uint256).selector, "Assert 9"; + assert jugAfter != jugBefore => f.selector == sig:file(bytes32,address).selector, "Assert 10"; +} + +rule vatGemKeepsUnchanged(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } { + env e; + + address anyAddr; + + bytes32 ilk = ilk(); + + mathint vatGemIlkAnyBefore = vat.gem(ilk, anyAddr); + + calldataarg args; + f(e, args); + + mathint vatGemIlkAnyAfter = vat.gem(ilk, anyAddr); + + assert vatGemIlkAnyAfter == vatGemIlkAnyBefore, "Assert 1"; +} + +rule inkChangeMatchesMkrChange(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } { + env e; + + createdUrn = 0; + queriedUrn = 0; + passedUrn = 0; + storage init = lastStorage; + address onTakeWho; + uint256 onTakeWad; + if (f.selector == sig:free(address,uint256,address,uint256).selector || + f.selector == sig:freeNoFee(address,uint256,address,uint256).selector) { + address owner; + uint256 index; + address to; + uint256 wad; + require to != currentContract && to != voteDelegate && to != voteDelegate2; + if (f.selector == sig:free(address,uint256,address,uint256).selector) { + free(e, owner, index, to, wad); + } else { + freeNoFee(e, owner, index, to, wad); + } + } else { + calldataarg args; + f(e, args); + } + storage final = lastStorage; + + address urn = createdUrn != 0 ? createdUrn : (queriedUrn != 0 ? queriedUrn : (passedUrn != 0 ? passedUrn : 0)); + require urn != currentContract && urn != voteDelegate && urn != voteDelegate2; + + address voteDelegateAfter = urnVoteDelegates(urn); + require voteDelegateAfter == addrZero() || voteDelegateAfter == voteDelegate || voteDelegateAfter == voteDelegate2; + + ilk() at init; + + require e.msg.sender != currentContract && e.msg.sender != voteDelegate && e.msg.sender != voteDelegate2; + require mkrSkyRate() == mkrSky.rate(); + + bytes32 ilk = ilk(); + + address voteDelegateBefore = urnVoteDelegates(urn); + require voteDelegateBefore == addrZero() || voteDelegateBefore == voteDelegate; + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBeforeBefore = voteDelegateBefore == addrZero() ? 0 : mkr.balanceOf(voteDelegateBefore); + mathint mkrBalanceOfVoteDelegateAfterBefore = voteDelegateAfter == addrZero() ? 0 : mkr.balanceOf(voteDelegateAfter); + require mkr.balanceOf(e.msg.sender) + mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBeforeBefore + mkrBalanceOfVoteDelegateAfterBefore <= mkr.totalSupply(); + require mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBeforeBefore >= vatUrnsIlkUrnInkBefore; + + ilk() at final; + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBeforeAfter = voteDelegateBefore == addrZero() ? 0 : mkr.balanceOf(voteDelegateBefore); + mathint mkrBalanceOfVoteDelegateAfterAfter = voteDelegateAfter == addrZero() ? 0 : mkr.balanceOf(voteDelegateAfter); + require f.selector == sig:onRemove(address,uint256,uint256).selector => voteDelegateBefore == addrZero(); + mathint burntOnRemove = f.selector == sig:onRemove(address,uint256,uint256).selector ? mkrTotalSupplyBefore - mkrTotalSupplyAfter + vatUrnsIlkUrnInkAfter - vatUrnsIlkUrnInkBefore : 0; + mathint transferredOnTake = f.selector == sig:onTake(address,address,uint256).selector ? mkrBalanceOfEngineBefore - mkrBalanceOfEngineAfter : 0; + mathint receivedOnTake = f.selector == sig:onTake(address,address,uint256).selector ? mkrBalanceOfVoteDelegateBeforeAfter - mkrBalanceOfVoteDelegateBeforeBefore : 0; + + // It checks that the ink change matches the MKR balance change + that is all or nothing delegated + assert voteDelegateAfter == voteDelegateBefore && voteDelegateBefore == addrZero() => + vatUrnsIlkUrnInkAfter - vatUrnsIlkUrnInkBefore == mkrBalanceOfEngineAfter - mkrBalanceOfEngineBefore + burntOnRemove + transferredOnTake, "Assert 1"; + assert voteDelegateAfter == voteDelegateBefore && voteDelegateBefore != addrZero() => + vatUrnsIlkUrnInkAfter - vatUrnsIlkUrnInkBefore == mkrBalanceOfVoteDelegateBeforeAfter - mkrBalanceOfVoteDelegateBeforeBefore - receivedOnTake && + mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - transferredOnTake, "Assert 2"; + assert voteDelegateAfter != voteDelegateBefore && voteDelegateBefore != addrZero() && voteDelegateAfter != addrZero() => + mkrBalanceOfVoteDelegateBeforeAfter - mkrBalanceOfVoteDelegateBeforeBefore == mkrBalanceOfVoteDelegateAfterBefore - mkrBalanceOfVoteDelegateAfterAfter, "Assert3"; +} + +rule inkChangeMatchesLsmkrChange(method f) filtered { f -> f.selector != sig:multicall(bytes[]).selector } { + env e; + + createdUrn = 0; + queriedUrn = 0; + passedUrn = 0; + storage init = lastStorage; + calldataarg args; + f(e, args); + storage final = lastStorage; + + address urn = createdUrn != 0 ? createdUrn : (queriedUrn != 0 ? queriedUrn : (passedUrn != 0 ? passedUrn : 0)); + + address farmAfter = urnFarms(urn); + require farmAfter == addrZero() || farmAfter == stakingRewards || farmAfter == stakingRewards2; + + ilk() at init; + + bytes32 ilk = ilk(); + + address farmBefore = urnFarms(urn); + require farmBefore == addrZero() || farmBefore == stakingRewards; + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBeforeBefore = farmBefore == addrZero() ? 0 : lsmkr.balanceOf(farmBefore); + mathint lsmkrBalanceOfFarmAfterBefore = farmAfter == addrZero() ? 0 : lsmkr.balanceOf(farmAfter); + require lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBeforeBefore + lsmkrBalanceOfFarmAfterBefore <= lsmkrTotalSupplyBefore; + require vatUrnsIlkUrnInkBefore <= lsmkrTotalSupplyBefore; + mathint farmBeforeBalanceOfUrnBefore = 0; + if (farmBefore != addrZero()) { + farmBeforeBalanceOfUrnBefore = farmBefore.balanceOf(e, urn); + require farmBeforeBalanceOfUrnBefore <= to_mathint(farmBefore.totalSupply(e)); + } + mathint farmAfterBalanceOfUrnBefore = 0; + if (farmAfter != addrZero()) { + farmAfterBalanceOfUrnBefore = farmAfter.balanceOf(e, urn); + require farmAfterBalanceOfUrnBefore <= to_mathint(farmAfter.totalSupply(e)); + } + mathint stakingRewardsBalanceOfUrnBefore = stakingRewards.balanceOf(urn); + mathint stakingRewards2BalanceOfUrnBefore = stakingRewards2.balanceOf(urn); + + ilk() at final; + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBeforAfter = farmBefore == addrZero() ? 0 : lsmkr.balanceOf(farmBefore); + mathint lsmkrBalanceOfFarmAfterAfter = farmAfter == addrZero() ? 0 : lsmkr.balanceOf(farmAfter); + mathint farmBeforeBalanceOfUrnAfter = 0; + if (farmBefore != addrZero()) { + farmBeforeBalanceOfUrnAfter = farmBefore.balanceOf(e, urn); + require farmBeforeBalanceOfUrnAfter <= to_mathint(farmBefore.totalSupply(e)); + } + mathint farmAfterBalanceOfUrnAfter = 0; + if (farmAfter != addrZero()) { + farmAfterBalanceOfUrnAfter = farmAfter.balanceOf(e, urn); + require farmAfterBalanceOfUrnAfter <= to_mathint(farmAfter.totalSupply(e)); + } + mathint stakingRewardsBalanceOfUrnAfter = stakingRewards.balanceOf(urn); + mathint stakingRewards2BalanceOfUrnAfter = stakingRewards2.balanceOf(urn); + + require farmBefore != addrZero() => lsmkrBalanceOfUrnBefore == 0; + require farmBefore == stakingRewards => stakingRewards2BalanceOfUrnBefore == 0; + require farmBefore == stakingRewards2 => stakingRewardsBalanceOfUrnBefore == 0; + require farmBefore == addrZero() => stakingRewardsBalanceOfUrnBefore == 0 && stakingRewards2BalanceOfUrnBefore == 0; + mathint burntOnKick = f.selector == sig:onKick(address,uint256).selector ? lsmkrTotalSupplyBefore - lsmkrTotalSupplyAfter : 0; + require vatUrnsIlkUrnInkBefore == lsmkrBalanceOfUrnBefore + stakingRewardsBalanceOfUrnBefore + stakingRewards2BalanceOfUrnBefore - burntOnKick; + require f.selector == sig:onRemove(address,uint256,uint256).selector => farmBefore == addrZero(); + + assert vatUrnsIlkUrnInkAfter - vatUrnsIlkUrnInkBefore == lsmkrTotalSupplyAfter - lsmkrTotalSupplyBefore + burntOnKick, "Assert 1"; + assert farmAfter == farmBefore && farmBefore == addrZero() => + vatUrnsIlkUrnInkAfter - vatUrnsIlkUrnInkBefore == lsmkrBalanceOfUrnAfter - lsmkrBalanceOfUrnBefore + burntOnKick, "Assert 2"; + assert farmAfter == farmBefore && farmBefore != addrZero() => + vatUrnsIlkUrnInkAfter - vatUrnsIlkUrnInkBefore == lsmkrBalanceOfFarmBeforAfter - lsmkrBalanceOfFarmBeforeBefore, "Assert 3"; + assert farmAfter != farmBefore && farmBefore == addrZero() => + vatUrnsIlkUrnInkAfter == lsmkrBalanceOfFarmAfterAfter - lsmkrBalanceOfFarmAfterBefore && + vatUrnsIlkUrnInkBefore == lsmkrBalanceOfUrnBefore - lsmkrBalanceOfUrnAfter, "Assert 4"; + assert farmAfter != farmBefore && farmAfter == addrZero() => + vatUrnsIlkUrnInkAfter == lsmkrBalanceOfUrnAfter - lsmkrBalanceOfUrnBefore && + vatUrnsIlkUrnInkBefore == lsmkrBalanceOfFarmBeforeBefore - lsmkrBalanceOfFarmBeforAfter - burntOnKick, "Assert 5"; + assert farmAfter != farmBefore && farmBefore != addrZero() && farmAfter != addrZero() => + vatUrnsIlkUrnInkAfter == lsmkrBalanceOfFarmAfterAfter - lsmkrBalanceOfFarmAfterBefore && + vatUrnsIlkUrnInkBefore == lsmkrBalanceOfFarmBeforeBefore - lsmkrBalanceOfFarmBeforAfter, "Assert 6"; + assert farmAfter == addrZero() => + lsmkrBalanceOfUrnAfter == vatUrnsIlkUrnInkAfter && stakingRewardsBalanceOfUrnAfter == 0 && stakingRewards2BalanceOfUrnAfter == 0, "Assert 7"; + assert farmAfter == stakingRewards => + stakingRewardsBalanceOfUrnAfter == vatUrnsIlkUrnInkAfter && lsmkrBalanceOfUrnAfter == 0 && stakingRewards2BalanceOfUrnAfter == 0, "Assert 8"; + assert farmAfter == stakingRewards2 => + stakingRewards2BalanceOfUrnAfter == vatUrnsIlkUrnInkAfter && lsmkrBalanceOfUrnAfter == 0 && stakingRewardsBalanceOfUrnAfter == 0, "Assert 9"; +} + +rule inkMatchesLsmkrFarmOnKick(address urn, uint256 wad) { + env e; + + address anyUrn; + require anyUrn != stakingRewards && anyUrn != stakingRewards2; + + bytes32 ilk = ilk(); + + address farmBefore = urnFarms(anyUrn); + require farmBefore == addrZero() || farmBefore == stakingRewards; + + mathint vatUrnsIlkAnyUrnInkBefore; mathint a; + vatUrnsIlkAnyUrnInkBefore, a = vat.urns(ilk, anyUrn); + + mathint lsmkrBalanceOfAnyUrnBefore = lsmkr.balanceOf(anyUrn); + mathint farmBalanceOfAnyUrnBefore = farmBefore == addrZero() ? 0 : stakingRewards.balanceOf(anyUrn); + + require stakingRewards2.balanceOf(anyUrn) == 0; + require lsmkrBalanceOfAnyUrnBefore == 0 || farmBalanceOfAnyUrnBefore == 0; + require lsmkrBalanceOfAnyUrnBefore > 0 => farmBefore == addrZero(); + require farmBalanceOfAnyUrnBefore > 0 => farmBefore != addrZero(); + require vatUrnsIlkAnyUrnInkBefore == lsmkrBalanceOfAnyUrnBefore + farmBalanceOfAnyUrnBefore; + + onKick(e, urn, wad); + + address farmAfter = urnFarms(anyUrn); + require farmAfter == addrZero() || farmAfter == farmBefore || farmAfter != farmBefore && farmAfter == stakingRewards2; + + mathint vatUrnsIlkAnyUrnInkAfter; + vatUrnsIlkAnyUrnInkAfter, a = vat.urns(ilk, anyUrn); + + mathint lsmkrBalanceOfAnyUrnAfter = lsmkr.balanceOf(anyUrn); + mathint farmBalanceOfAnyUrnAfter = farmAfter == addrZero() ? 0 : (farmAfter == farmBefore ? stakingRewards.balanceOf(anyUrn) : stakingRewards2.balanceOf(anyUrn)); + + assert urn != anyUrn => vatUrnsIlkAnyUrnInkAfter == lsmkrBalanceOfAnyUrnAfter + farmBalanceOfAnyUrnAfter, "Assert 1"; + assert urn == anyUrn => vatUrnsIlkAnyUrnInkAfter == lsmkrBalanceOfAnyUrnAfter + farmBalanceOfAnyUrnAfter + wad, "Assert 2"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 1, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on rely +rule rely_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting deny +rule deny(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + deny(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 0, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on deny +rule deny_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting file +rule file(bytes32 what, address data) { + env e; + + file(e, what, data); + + address jugAfter = jug(); + + assert jugAfter == data, "Assert 1"; +} + +// Verify revert rules on file +rule file_revert(bytes32 what, address data) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + file@withrevert(e, what, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = what != to_bytes32(0x6a75670000000000000000000000000000000000000000000000000000000000); + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting addFarm +rule addFarm(address farm) { + env e; + + address other; + require other != farm; + + LockstakeEngine.FarmStatus farmsOtherBefore = farms(other); + + addFarm(e, farm); + + LockstakeEngine.FarmStatus farmsFarmAfter = farms(farm); + LockstakeEngine.FarmStatus farmsOtherAfter = farms(other); + + assert farmsFarmAfter == LockstakeEngine.FarmStatus.ACTIVE, "Assert 1"; + assert farmsOtherAfter == farmsOtherBefore, "Assert 2"; +} + +// Verify revert rules on addFarm +rule addFarm_revert(address farm) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + addFarm@withrevert(e, farm); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting delFarm +rule delFarm(address farm) { + env e; + + address other; + require other != farm; + + LockstakeEngine.FarmStatus farmsOtherBefore = farms(other); + + delFarm(e, farm); + + LockstakeEngine.FarmStatus farmsFarmAfter = farms(farm); + LockstakeEngine.FarmStatus farmsOtherAfter = farms(other); + + assert farmsFarmAfter == LockstakeEngine.FarmStatus.DELETED, "Assert 1"; + assert farmsOtherAfter == farmsOtherBefore, "Assert 2"; +} + +// Verify revert rules on delFarm +rule delFarm_revert(address farm) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + delFarm@withrevert(e, farm); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting open +rule open(uint256 index) { + env e; + + address other; + require other != e.msg.sender; + address anyAddr; uint256 anyUint256; + require anyAddr != e.msg.sender || anyUint256 != index; + + mathint ownerUrnsCountSenderBefore = ownerUrnsCount(e.msg.sender); + mathint ownerUrnsCountOtherBefore = ownerUrnsCount(other); + address ownerUrnsOtherBefore = ownerUrns(anyAddr, anyUint256); + + address urn = open(e, index); + require urn.lsmkr(e) == lsmkr; + + mathint ownerUrnsCountSenderAfter = ownerUrnsCount(e.msg.sender); + mathint ownerUrnsCountOtherAfter = ownerUrnsCount(other); + address ownerUrnsSenderIndexAfter = ownerUrns(e.msg.sender, index); + address ownerUrnsOtherAfter = ownerUrns(anyAddr, anyUint256); + address urnOwnersUrnAfter = urnOwners(urn); + mathint vatCanUrnEngineAfter = vat.can(urn, currentContract); + mathint lsmkrAllowanceUrnEngine = lsmkr.allowance(urn, currentContract); + + assert ownerUrnsCountSenderAfter == ownerUrnsCountSenderBefore + 1, "Assert 1"; + assert ownerUrnsCountOtherAfter == ownerUrnsCountOtherBefore, "Assert 2"; + assert ownerUrnsSenderIndexAfter == urn, "Assert 3"; + assert ownerUrnsOtherAfter == ownerUrnsOtherBefore, "Assert 4"; + assert urnOwnersUrnAfter == e.msg.sender, "Assert 5"; + assert vatCanUrnEngineAfter == 1, "Assert 6"; + assert lsmkrAllowanceUrnEngine == max_uint256, "Assert 7"; +} + +// Verify revert rules on open +rule open_revert(uint256 index) { + env e; + + createdUrn = 0; // Now we can identify if the urn was created + + mathint ownerUrnsCountSender = ownerUrnsCount(e.msg.sender); + + open@withrevert(e, index); + bool reverted = lastReverted; // `lastReverted` will be modified by `createdUrn.engine(e)` + if (createdUrn != 0) { + require createdUrn.engine(e) == currentContract; + } + + bool revert1 = e.msg.value > 0; + bool revert2 = to_mathint(index) != ownerUrnsCountSender; + bool revert3 = ownerUrnsCountSender == max_uint256; + + assert reverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting hope +rule hope(address owner, uint256 index, address usr) { + env e; + + address other; + address other2; + address urn = ownerUrns(owner, index); + require other != urn || other2 != usr; + + mathint urnCanOtherBefore = urnCan(other, other2); + + hope(e, owner, index, usr); + + mathint urnCanUrnUsrAfter = urnCan(urn, usr); + mathint urnCanOtherAfter = urnCan(other, other2); + + assert urnCanUrnUsrAfter == 1, "Assert 1"; + assert urnCanOtherAfter == urnCanOtherBefore, "Assert 2"; +} + +// Verify revert rules on hope +rule hope_revert(address owner, uint256 index, address usr) { + env e; + + address urn = ownerUrns(owner, index); + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + + hope@withrevert(e, owner, index, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting nope +rule nope(address owner, uint256 index, address usr) { + env e; + + address other; + address other2; + address urn = ownerUrns(owner, index); + require other != urn || other2 != usr; + + mathint urnCanOtherBefore = urnCan(other, other2); + + nope(e, owner, index, usr); + + mathint urnCanUrnUsrAfter = urnCan(urn, usr); + mathint urnCanOtherAfter = urnCan(other, other2); + + assert urnCanUrnUsrAfter == 0, "Assert 1"; + assert urnCanOtherAfter == urnCanOtherBefore, "Assert 2"; +} + +// Verify revert rules on nope +rule nope_revert(address owner, uint256 index, address usr) { + env e; + + address urn = ownerUrns(owner, index); + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + + nope@withrevert(e, owner, index, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting selectVoteDelegate +rule selectVoteDelegate(address owner, uint256 index, address voteDelegate_) { + env e; + + address urn = ownerUrns(owner, index); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address prevVoteDelegate = urnVoteDelegates(urn); + require prevVoteDelegate == addrZero() || prevVoteDelegate == voteDelegate2; + + address other; + require other != urn; + address other2; + require other2 != voteDelegate_ && other2 != prevVoteDelegate && other2 != currentContract; + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint a; + vatUrnsIlkUrnInk, a = vat.urns(ilk, urn); + + address urnVoteDelegatesOtherBefore = urnVoteDelegates(other); + mathint mkrBalanceOfPrevVoteDelegateBefore = mkr.balanceOf(prevVoteDelegate); + mathint mkrBalanceOfNewVoteDelegateBefore = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2); + + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkrBalanceOfPrevVoteDelegateBefore + mkrBalanceOfNewVoteDelegateBefore + mkrBalanceOfEngineBefore + mkrBalanceOfOtherBefore; + + selectVoteDelegate(e, owner, index, voteDelegate_); + + address urnVoteDelegatesUrnAfter = urnVoteDelegates(urn); + address urnVoteDelegatesOtherAfter = urnVoteDelegates(other); + mathint mkrBalanceOfPrevVoteDelegateAfter = mkr.balanceOf(prevVoteDelegate); + mathint mkrBalanceOfNewVoteDelegateAfter = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2); + + assert urnVoteDelegatesUrnAfter == voteDelegate_, "Assert 1"; + assert urnVoteDelegatesOtherAfter == urnVoteDelegatesOtherBefore, "Assert 2"; + assert prevVoteDelegate == addrZero() => mkrBalanceOfPrevVoteDelegateAfter == mkrBalanceOfPrevVoteDelegateBefore, "Assert 3"; + assert prevVoteDelegate != addrZero() => mkrBalanceOfPrevVoteDelegateAfter == mkrBalanceOfPrevVoteDelegateBefore - vatUrnsIlkUrnInk, "Assert 4"; + assert voteDelegate_ == addrZero() => mkrBalanceOfNewVoteDelegateAfter == mkrBalanceOfNewVoteDelegateBefore, "Assert 5"; + assert voteDelegate_ != addrZero() => mkrBalanceOfNewVoteDelegateAfter == mkrBalanceOfNewVoteDelegateBefore + vatUrnsIlkUrnInk, "Assert 6"; + assert prevVoteDelegate == addrZero() && voteDelegate_ == addrZero() || prevVoteDelegate != addrZero() && voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 7"; + assert prevVoteDelegate == addrZero() && voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - vatUrnsIlkUrnInk, "Assert 8"; + assert prevVoteDelegate != addrZero() && voteDelegate_ == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore + vatUrnsIlkUrnInk, "Assert 9"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 10"; +} + +// Verify revert rules on selectVoteDelegate +rule selectVoteDelegate_revert(address owner, uint256 index, address voteDelegate_) { + env e; + + address urn = ownerUrns(owner, index); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address prevVoteDelegate = urnVoteDelegates(urn); + require prevVoteDelegate == addrZero() || prevVoteDelegate == voteDelegate2; + + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + mathint urnAuctions = urnAuctions(urn); + mathint voteDelegateFactoryCreatedVoteDelegate = voteDelegateFactory.created(voteDelegate_); + bytes32 ilk = ilk(); + mathint vatIlksIlkSpot; mathint a; + a, a, vatIlksIlkSpot, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + mathint calcVatIlksIlkRateAfter = dripSummary(ilk); + + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(prevVoteDelegate) + mkr.balanceOf(voteDelegate_) + mkr.balanceOf(currentContract); + // Practical Vat assumptions + require vatUrnsIlkUrnInk * vatIlksIlkSpot <= max_uint256; + require vatUrnsIlkUrnArt * calcVatIlksIlkRateAfter <= max_uint256; + // TODO: this might be nice to prove in some sort + require prevVoteDelegate == addrZero() && to_mathint(mkr.balanceOf(currentContract)) >= vatUrnsIlkUrnInk || prevVoteDelegate != addrZero() && to_mathint(mkr.balanceOf(prevVoteDelegate)) >= vatUrnsIlkUrnInk && to_mathint(voteDelegate2.stake(currentContract)) >= vatUrnsIlkUrnInk; // TODO: this might be interesting to be proved + require voteDelegate.stake(currentContract) + vatUrnsIlkUrnInk <= max_uint256; + + selectVoteDelegate@withrevert(e, owner, index, voteDelegate_); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert4 = urnAuctions > 0; + bool revert5 = voteDelegate_ != addrZero() && voteDelegateFactoryCreatedVoteDelegate != 1; + bool revert6 = voteDelegate_ == prevVoteDelegate; + bool revert7 = vatUrnsIlkUrnArt > 0 && voteDelegate_ != addrZero() && vatUrnsIlkUrnInk * vatIlksIlkSpot < vatUrnsIlkUrnArt * calcVatIlksIlkRateAfter; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting selectFarm +rule selectFarm(address owner, uint256 index, address farm, uint16 ref) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + require farm == addrZero() || farm == stakingRewards; + address prevFarm = urnFarms(urn); + require prevFarm == addrZero() || prevFarm == stakingRewards2; + + address other; + require other != urn; + address other2; + require other2 != farm && other2 != prevFarm && other2 != urn; + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint a; + vatUrnsIlkUrnInk, a = vat.urns(ilk, urn); + + address urnFarmsOtherBefore = urnFarms(other); + mathint lsmkrBalanceOfPrevFarmBefore = lsmkr.balanceOf(prevFarm); + mathint lsmkrBalanceOfNewFarmBefore = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other2); + + // Tokens invariants + require to_mathint(lsmkr.totalSupply()) >= lsmkrBalanceOfPrevFarmBefore + lsmkrBalanceOfNewFarmBefore + lsmkrBalanceOfUrnBefore + lsmkrBalanceOfOtherBefore; + + selectFarm(e, owner, index, farm, ref); + + address urnFarmsUrnAfter = urnFarms(urn); + address urnFarmsOtherAfter = urnFarms(other); + mathint lsmkrBalanceOfPrevFarmAfter = lsmkr.balanceOf(prevFarm); + mathint lsmkrBalanceOfNewFarmAfter = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other2); + + assert urnFarmsUrnAfter == farm, "Assert 1"; + assert urnFarmsOtherAfter == urnFarmsOtherBefore, "Assert 2"; + assert prevFarm == addrZero() => lsmkrBalanceOfPrevFarmAfter == lsmkrBalanceOfPrevFarmBefore, "Assert 3"; + assert prevFarm != addrZero() => lsmkrBalanceOfPrevFarmAfter == lsmkrBalanceOfPrevFarmBefore - vatUrnsIlkUrnInk, "Assert 4"; + assert farm == addrZero() => lsmkrBalanceOfNewFarmAfter == lsmkrBalanceOfNewFarmBefore, "Assert 5"; + assert farm != addrZero() => lsmkrBalanceOfNewFarmAfter == lsmkrBalanceOfNewFarmBefore + vatUrnsIlkUrnInk, "Assert 6"; + assert prevFarm == addrZero() && farm == addrZero() || prevFarm != addrZero() && farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 7"; + assert prevFarm == addrZero() && farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore - vatUrnsIlkUrnInk, "Assert 8"; + assert prevFarm != addrZero() && farm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore + vatUrnsIlkUrnInk, "Assert 9"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 10"; +} + +// Verify revert rules on selectFarm +rule selectFarm_revert(address owner, uint256 index, address farm, uint16 ref) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + require farm == addrZero() || farm == stakingRewards; + address prevFarm = urnFarms(urn); + require prevFarm == addrZero() || prevFarm == stakingRewards2; + + address urnOwnersUrn = urnOwners(urn); + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + mathint urnAuctions = urnAuctions(urn); + LockstakeEngine.FarmStatus farmsFarm = farms(farm); + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint a; + vatUrnsIlkUrnInk, a = vat.urns(ilk, urn); + + // TODO: this might be nice to prove in some sort + require prevFarm == addrZero() && to_mathint(lsmkr.balanceOf(urn)) >= vatUrnsIlkUrnInk || prevFarm != addrZero() && to_mathint(lsmkr.balanceOf(prevFarm)) >= vatUrnsIlkUrnInk && to_mathint(stakingRewards2.balanceOf(urn)) >= vatUrnsIlkUrnInk; + // Token invariants + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(prevFarm) + lsmkr.balanceOf(farm) + lsmkr.balanceOf(urn); + require stakingRewards2.totalSupply() >= stakingRewards2.balanceOf(urn); + require stakingRewards.totalSupply() >= stakingRewards.balanceOf(urn); + // Assumption + require stakingRewards.totalSupply() + vatUrnsIlkUrnInk <= max_uint256; + + selectFarm@withrevert(e, owner, index, farm, ref); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert4 = urnAuctions > 0; + bool revert5 = farm != addrZero() && farmsFarm != LockstakeEngine.FarmStatus.ACTIVE; + bool revert6 = farm == prevFarm; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting lock +rule lock(address owner, uint256 index, uint256 wad, uint16 ref) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + address other; + require other != e.msg.sender && other != currentContract && other != voteDelegate_; + address other2; + require other2 != urn && other2 != farm; + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint mkrBalanceOfSenderBefore = mkr.balanceOf(e.msg.sender); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBefore = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other2); + + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkrBalanceOfSenderBefore + mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore + lsmkrBalanceOfOtherBefore; + + lock(e, owner, index, wad, ref); + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint mkrBalanceOfSenderAfter = mkr.balanceOf(e.msg.sender); + mathint mkrBalanceOfVoteDelegateAfter = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other2); + + assert vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore + wad, "Assert 1"; + assert mkrBalanceOfSenderAfter == mkrBalanceOfSenderBefore - wad, "Assert 2"; + assert voteDelegate_ == addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore, "Assert 3"; + assert voteDelegate_ != addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore + wad, "Assert 4"; + assert voteDelegate_ == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore + wad, "Assert 5"; + assert voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 6"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 7"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore + wad, "Assert 8"; + assert farm == addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore, "Assert 9"; + assert farm != addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore + wad, "Assert 10"; + assert farm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore + wad, "Assert 11"; + assert farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 12"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 13"; +} + +// Verify revert rules on lock +rule lock_revert(address owner, uint256 index, uint256 wad, uint16 ref) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkDust; mathint a; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, a, vatIlksIlkDust = vat.ilks(ilk); + + // Happening in urn init + require vat.can(urn, currentContract) == 1; + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lsmkr.wards(currentContract) == 1; + // User balance and approval + require mkr.balanceOf(e.msg.sender) >= wad && mkr.allowance(e.msg.sender, currentContract) >= wad; + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(e.msg.sender) + mkr.balanceOf(currentContract) + mkr.balanceOf(voteDelegate_); + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(urn) + lsmkr.balanceOf(farm); + // TODO: this might be nice to prove in some sort + require mkr.balanceOf(voteDelegate_) >= voteDelegate.stake(currentContract); + require stakingRewards.totalSupply() == stakingRewards.balanceOf(urn); + require lsmkr.balanceOf(farm) == stakingRewards.totalSupply(); + require lsmkr.totalSupply() + wad <= to_mathint(mkr.totalSupply()); + // Practical Vat assumptions + require vat.live() == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require (vatUrnsIlkUrnInk + wad) * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatUrnsIlkUrnArt == 0 || vatIlksIlkRate * vatUrnsIlkUrnArt >= vatIlksIlkDust; + // Safe to assume as Engine doesn't modify vat.gem(ilk,urn) (rule vatGemKeepsUnchanged) + require vat.gem(ilk, urn) == 0; + // Safe to assume as Engine keeps the invariant (rule inkMatchesLsmkrFarm) + require lsmkr.balanceOf(urn) == 0 || stakingRewards.balanceOf(urn) == 0; + require vatUrnsIlkUrnInk == lsmkr.balanceOf(urn) + stakingRewards.balanceOf(urn); + + LockstakeEngine.FarmStatus farmsFarm = farms(farm); + + lock@withrevert(e, owner, index, wad, ref); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = to_mathint(wad) > max_int256(); + bool revert4 = farm != addrZero() && farmsFarm != LockstakeEngine.FarmStatus.ACTIVE; + bool revert5 = farm != addrZero() && wad == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting lockSky +rule lockSky(address owner, uint256 index, uint256 skyWad, uint16 ref) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + address other; + require other != e.msg.sender && other != currentContract && other != voteDelegate_; + address other2; + require other2 != urn && other2 != farm; + + mathint mkrSkyRate = mkrSkyRate(); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint skyTotalSupplyBefore = sky.totalSupply(); + mathint skyBalanceOfSenderBefore = sky.balanceOf(e.msg.sender); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfSenderBefore = mkr.balanceOf(e.msg.sender); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBefore = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other2); + + // Happening in constructor + require mkrSkyRate == to_mathint(mkrSky.rate()); + // Tokens invariants + require skyTotalSupplyBefore >= skyBalanceOfSenderBefore + sky.balanceOf(currentContract) + sky.balanceOf(mkrSky); + require mkrTotalSupplyBefore >= mkrBalanceOfSenderBefore + mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore + lsmkrBalanceOfOtherBefore; + + lockSky(e, owner, index, skyWad, ref); + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint skyTotalSupplyAfter = sky.totalSupply(); + mathint skyBalanceOfSenderAfter = sky.balanceOf(e.msg.sender); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfSenderAfter = mkr.balanceOf(e.msg.sender); + mathint mkrBalanceOfVoteDelegateAfter = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other2); + + assert vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore + skyWad/mkrSkyRate, "Assert 1"; + assert skyTotalSupplyAfter == skyTotalSupplyBefore - skyWad, "Assert 2"; + assert skyBalanceOfSenderAfter == skyBalanceOfSenderBefore - skyWad, "Assert 3"; + assert mkrTotalSupplyAfter == mkrTotalSupplyBefore + skyWad/mkrSkyRate, "Assert 4"; + assert voteDelegate_ == addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore, "Assert 5"; + assert voteDelegate_ != addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore + skyWad/mkrSkyRate, "Assert 6"; + assert voteDelegate_ == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore + skyWad/mkrSkyRate, "Assert 7"; + assert voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 8"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 9"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore + skyWad/mkrSkyRate, "Assert 10"; + assert farm == addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore, "Assert 11"; + assert farm != addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore + skyWad/mkrSkyRate, "Assert 12"; + assert farm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore + skyWad/mkrSkyRate, "Assert 13"; + assert farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 14"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 15"; +} + +// Verify revert rules on lockSky +rule lockSky_revert(address owner, uint256 index, uint256 skyWad, uint16 ref) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + mathint mkrSkyRate = mkrSkyRate(); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkDust; mathint a; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, a, vatIlksIlkDust = vat.ilks(ilk); + + // Happening in constructor + require mkrSkyRate == to_mathint(mkrSky.rate()); + // Avoid division by zero + require mkrSkyRate > 0; + // Happening in urn init + require vat.can(urn, currentContract) == 1; + require sky.allowance(currentContract, mkrSky) == max_uint256; + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lsmkr.wards(currentContract) == 1; + // User balance and approval + require sky.balanceOf(e.msg.sender) >= skyWad && sky.allowance(e.msg.sender, currentContract) >= skyWad; + // Tokens invariants + require to_mathint(sky.totalSupply()) >= sky.balanceOf(e.msg.sender) + sky.balanceOf(currentContract) + sky.balanceOf(mkrSky); + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(e.msg.sender) + mkr.balanceOf(currentContract) + mkr.balanceOf(voteDelegate_); + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(urn) + lsmkr.balanceOf(farm); + // Assumption + require to_mathint(mkr.totalSupply()) <= max_uint256 - skyWad/mkrSkyRate; + // TODO: this might be nice to prove in some sort + require mkr.balanceOf(voteDelegate_) >= voteDelegate.stake(currentContract); + require stakingRewards.totalSupply() == stakingRewards.balanceOf(urn); + require lsmkr.balanceOf(farm) == stakingRewards.totalSupply(); + require lsmkr.totalSupply() + skyWad/mkrSkyRate <= to_mathint(mkr.totalSupply()); + // Practical Vat assumptions + require vat.live() == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require (vatUrnsIlkUrnInk + skyWad/mkrSkyRate) * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatUrnsIlkUrnArt == 0 || vatIlksIlkRate * vatUrnsIlkUrnArt >= vatIlksIlkDust; + // Safe to assume as Engine doesn't modify vat.gem(ilk,urn) (rule vatGemKeepsUnchanged) + require vat.gem(ilk, urn) == 0; + // Safe to assume as Engine keeps the invariant (rule vatUrnsIlkUrnInkMatchesLsmkrFarm) + require lsmkr.balanceOf(urn) == 0 || stakingRewards.balanceOf(urn) == 0; + require vatUrnsIlkUrnInk == lsmkr.balanceOf(urn) + stakingRewards.balanceOf(urn); + + LockstakeEngine.FarmStatus farmsFarm = farms(farm); + + lockSky@withrevert(e, owner, index, skyWad, ref); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = skyWad/mkrSkyRate > max_int256(); + bool revert4 = farm != addrZero() && farmsFarm != LockstakeEngine.FarmStatus.ACTIVE; + bool revert5 = farm != addrZero() && skyWad/mkrSkyRate == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting free +rule free(address owner, uint256 index, address to, uint256 wad) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + address other; + require other != to && other != currentContract && other != voteDelegate_; + address other2; + require other2 != urn && other2 != farm; + + mathint fee = fee(); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfToBefore = mkr.balanceOf(to); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBefore = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other2); + + // Happening in constructor + require fee < WAD(); + // Tokens invariants + require mkrTotalSupplyBefore >= mkrBalanceOfToBefore + mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore + lsmkrBalanceOfOtherBefore; + + free(e, owner, index, to, wad); + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfToAfter = mkr.balanceOf(to); + mathint mkrBalanceOfVoteDelegateAfter = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other2); + + assert vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore - wad, "Assert 1"; + assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - wad * fee / WAD(), "Assert 2"; + assert to != currentContract && to != voteDelegate_ || + to == currentContract && voteDelegate_ != addrZero() || + to == voteDelegate_ && voteDelegate_ == addrZero() => mkrBalanceOfToAfter == mkrBalanceOfToBefore + (wad - wad * fee / WAD()), "Assert 3"; + assert to == currentContract && voteDelegate_ == addrZero() || + to == voteDelegate_ && voteDelegate_ != addrZero() => mkrBalanceOfToAfter == mkrBalanceOfToBefore - wad * fee / WAD(), "Assert 4"; + assert to != voteDelegate_ && voteDelegate_ == addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore, "Assert 5"; + assert to != voteDelegate_ && voteDelegate_ != addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore - wad, "Assert 6"; + assert to != currentContract && voteDelegate_ == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - wad, "Assert 7"; + assert to != currentContract && voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 8"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 9"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore - wad, "Assert 10"; + assert farm == addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore, "Assert 11"; + assert farm != addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore - wad, "Assert 12"; + assert farm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore - wad, "Assert 13"; + assert farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 14"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 15"; +} + +// Verify revert rules on free +rule free_revert(address owner, uint256 index, address to, uint256 wad) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + mathint fee = fee(); + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkDust; mathint a; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, a, vatIlksIlkDust = vat.ilks(ilk); + + // Hapenning in constructor + require fee < WAD(); + // Happening in urn init + require vat.can(urn, currentContract) == 1; + require lsmkr.allowance(urn, currentContract) == max_uint256; + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lsmkr.wards(currentContract) == 1; + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(e.msg.sender) + mkr.balanceOf(currentContract) + mkr.balanceOf(voteDelegate_); + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(urn) + lsmkr.balanceOf(farm); + // TODO: this might be nice to prove in some sort + require mkr.balanceOf(voteDelegate_) >= voteDelegate.stake(currentContract); + require voteDelegate_ != addrZero() => to_mathint(voteDelegate.stake(currentContract)) >= vatUrnsIlkUrnInk; + require voteDelegate_ == addrZero() => to_mathint(mkr.balanceOf(currentContract)) >= vatUrnsIlkUrnInk; + require stakingRewards.totalSupply() == stakingRewards.balanceOf(urn); + require lsmkr.balanceOf(farm) == stakingRewards.totalSupply(); + // Practical Vat assumptions + require vat.live() == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require (vatUrnsIlkUrnInk - wad) * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatUrnsIlkUrnArt == 0 || vatIlksIlkRate * vatUrnsIlkUrnArt >= vatIlksIlkDust; + // Safe to assume as Engine doesn't modify vat.gem(ilk,urn) (rule vatGemKeepsUnchanged) + require vat.gem(ilk, urn) == 0; + // Safe to assume as Engine keeps the invariant (rule inkMatchesLsmkrFarm) + require lsmkr.balanceOf(urn) == 0 || stakingRewards.balanceOf(urn) == 0; + require lsmkr.balanceOf(urn) > 0 => farm == addrZero(); + require stakingRewards.balanceOf(urn) > 0 => farm != addrZero(); + require vatUrnsIlkUrnInk == lsmkr.balanceOf(urn) + stakingRewards.balanceOf(urn); + + free@withrevert(e, owner, index, to, wad); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert4 = to_mathint(wad) > max_int256(); + bool revert5 = vatUrnsIlkUrnInk < to_mathint(wad) || wad > 0 && (vatUrnsIlkUrnInk - wad) * vatIlksIlkSpot < vatUrnsIlkUrnArt * vatIlksIlkRate; + bool revert6 = farm != 0 && wad == 0; + bool revert7 = wad * fee > max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting freeSky +rule freeSky(address owner, uint256 index, address to, uint256 skyWad) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + address other; + require other != currentContract && other != voteDelegate_; + address other2; + require other2 != urn && other2 != farm; + address other3; + require other3 != to; + + mathint mkrSkyRate = mkrSkyRate(); + mathint fee = fee(); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint skyTotalSupplyBefore = sky.totalSupply(); + mathint skyBalanceOfToBefore = sky.balanceOf(to); + mathint skyBalanceOfOtherBefore = sky.balanceOf(other3); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBefore = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other2); + + // Happening in constructor + require mkrSkyRate == to_mathint(mkrSky.rate()); + require fee < WAD(); + // Tokens invariants + require skyTotalSupplyBefore >= skyBalanceOfToBefore + skyBalanceOfOtherBefore; + require mkrTotalSupplyBefore >= mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore + lsmkrBalanceOfOtherBefore; + + freeSky(e, owner, index, to, skyWad); + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint skyTotalSupplyAfter = sky.totalSupply(); + mathint skyBalanceOfToAfter = sky.balanceOf(to); + mathint skyBalanceOfOtherAfter = sky.balanceOf(other3); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfVoteDelegateAfter = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other2); + + assert vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore - skyWad/mkrSkyRate, "Assert 1"; + assert skyTotalSupplyAfter == skyTotalSupplyBefore + (skyWad/mkrSkyRate - skyWad/mkrSkyRate * fee / WAD()) * mkrSkyRate, "Assert 2"; + assert skyBalanceOfToAfter == skyBalanceOfToBefore + (skyWad/mkrSkyRate - skyWad/mkrSkyRate * fee / WAD()) * mkrSkyRate, "Assert 3"; + assert skyBalanceOfOtherAfter == skyBalanceOfOtherBefore, "Assert 4"; + assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - skyWad/mkrSkyRate, "Assert 5"; + assert to != voteDelegate_ && voteDelegate_ == addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore, "Assert 6"; + assert to != voteDelegate_ && voteDelegate_ != addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore - skyWad/mkrSkyRate, "Assert 7"; + assert to != currentContract && voteDelegate_ == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - skyWad/mkrSkyRate, "Assert 8"; + assert to != currentContract && voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 9"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 10"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore - skyWad/mkrSkyRate, "Assert 11"; + assert farm == addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore, "Assert 12"; + assert farm != addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore - skyWad/mkrSkyRate, "Assert 13"; + assert farm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore - skyWad/mkrSkyRate, "Assert 14"; + assert farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 15"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 16"; +} + +// Verify revert rules on freeSky +rule freeSky_revert(address owner, uint256 index, address to, uint256 skyWad) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + + mathint mkrSkyRate = mkrSkyRate(); + mathint fee = fee(); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkDust; mathint a; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, a, vatIlksIlkDust = vat.ilks(ilk); + + // Happening in constructor + require mkrSkyRate == to_mathint(mkrSky.rate()); + require fee < WAD(); + require mkr.allowance(currentContract, mkrSky) == max_uint256; + // Avoid division by zero + require mkrSkyRate > 0; + // Happening in urn init + require vat.can(urn, currentContract) == 1; + require lsmkr.allowance(urn, currentContract) == max_uint256; + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lsmkr.wards(currentContract) == 1; + // Tokens invariants + require sky.totalSupply() >= sky.balanceOf(to); + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(e.msg.sender) + mkr.balanceOf(currentContract) + mkr.balanceOf(voteDelegate_); + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(urn) + lsmkr.balanceOf(farm); + // Practical assumption + require sky.totalSupply() + skyWad <= max_uint256; + // TODO: this might be nice to prove in some sort + require mkr.balanceOf(voteDelegate_) >= voteDelegate.stake(currentContract); + require voteDelegate_ != addrZero() => to_mathint(voteDelegate.stake(currentContract)) >= vatUrnsIlkUrnInk; + require voteDelegate_ == addrZero() => to_mathint(mkr.balanceOf(currentContract)) >= vatUrnsIlkUrnInk; + require stakingRewards.totalSupply() == stakingRewards.balanceOf(urn); + require lsmkr.balanceOf(farm) == stakingRewards.totalSupply(); + // Practical Vat assumptions + require vat.live() == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require (vatUrnsIlkUrnInk - skyWad/mkrSkyRate) * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatUrnsIlkUrnArt == 0 || vatIlksIlkRate * vatUrnsIlkUrnArt >= vatIlksIlkDust; + // Safe to assume as Engine doesn't modify vat.gem(ilk,urn) (rule vatGemKeepsUnchanged) + require vat.gem(ilk, urn) == 0; + // Safe to assume as Engine keeps the invariant (rule inkMatchesLsmkrFarm) + require lsmkr.balanceOf(urn) == 0 || stakingRewards.balanceOf(urn) == 0; + require lsmkr.balanceOf(urn) > 0 => farm == addrZero(); + require stakingRewards.balanceOf(urn) > 0 => farm != addrZero(); + require vatUrnsIlkUrnInk == lsmkr.balanceOf(urn) + stakingRewards.balanceOf(urn); + + freeSky@withrevert(e, owner, index, to, skyWad); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert4 = to_mathint(skyWad/mkrSkyRate) > max_int256(); + bool revert5 = vatUrnsIlkUrnInk < to_mathint(skyWad/mkrSkyRate) || skyWad/mkrSkyRate > 0 && (vatUrnsIlkUrnInk - skyWad/mkrSkyRate) * vatIlksIlkSpot < vatUrnsIlkUrnArt * vatIlksIlkRate; + bool revert6 = farm != 0 && skyWad/mkrSkyRate == 0; + bool revert7 = skyWad/mkrSkyRate * fee > max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting freeNoFee +rule freeNoFee(address owner, uint256 index, address to, uint256 wad) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + address other; + require other != to && other != currentContract && other != voteDelegate_; + address other2; + require other2 != urn && other2 != farm; + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfToBefore = mkr.balanceOf(to); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfVoteDelegateBefore = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other2); + + // Tokens invariants + require mkrTotalSupplyBefore >= mkrBalanceOfToBefore + mkrBalanceOfEngineBefore + mkrBalanceOfVoteDelegateBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore + lsmkrBalanceOfOtherBefore; + + freeNoFee(e, owner, index, to, wad); + + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfToAfter = mkr.balanceOf(to); + mathint mkrBalanceOfVoteDelegateAfter = mkr.balanceOf(voteDelegate_); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other2); + + assert vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore - wad, "Assert 1"; + assert mkrTotalSupplyAfter == mkrTotalSupplyBefore, "Assert 2"; + assert to != currentContract && to != voteDelegate_ || + to == currentContract && voteDelegate_ != addrZero() || + to == voteDelegate_ && voteDelegate_ == addrZero() => mkrBalanceOfToAfter == mkrBalanceOfToBefore + wad, "Assert 3"; + assert to == currentContract && voteDelegate_ == addrZero() || + to == voteDelegate_ && voteDelegate_ != addrZero() => mkrBalanceOfToAfter == mkrBalanceOfToBefore, "Assert 4"; + assert to != voteDelegate_ && voteDelegate_ == addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore, "Assert 5"; + assert to != voteDelegate_ && voteDelegate_ != addrZero() => mkrBalanceOfVoteDelegateAfter == mkrBalanceOfVoteDelegateBefore - wad, "Assert 6"; + assert to != currentContract && voteDelegate_ == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - wad, "Assert 7"; + assert to != currentContract && voteDelegate_ != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 8"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 9"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore - wad, "Assert 10"; + assert farm == addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore, "Assert 11"; + assert farm != addrZero() => lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore - wad, "Assert 12"; + assert farm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore - wad, "Assert 13"; + assert farm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 14"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 15"; +} + +// Verify revert rules on freeNoFee +rule freeNoFee_revert(address owner, uint256 index, address to, uint256 wad) { + env e; + + address urn = ownerUrns(owner, index); + require urn == lockstakeUrn; + + mathint wardsSender = wards(e.msg.sender); + + address voteDelegate_ = urnVoteDelegates(urn); + require voteDelegate_ == addrZero() || voteDelegate_ == voteDelegate; + address farm = urnFarms(urn); + require farm == addrZero() || farm == stakingRewards; + + require e.msg.sender != voteDelegate_ && e.msg.sender != currentContract; + + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkDust; mathint a; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, a, vatIlksIlkDust = vat.ilks(ilk); + + // Happening in urn init + require vat.can(urn, currentContract) == 1; + require lsmkr.allowance(urn, currentContract) == max_uint256; + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lsmkr.wards(currentContract) == 1; + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkr.balanceOf(e.msg.sender) + mkr.balanceOf(currentContract) + mkr.balanceOf(voteDelegate_); + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(urn) + lsmkr.balanceOf(farm); + // TODO: this might be nice to prove in some sort + require mkr.balanceOf(voteDelegate_) >= voteDelegate.stake(currentContract); + require voteDelegate_ != addrZero() => to_mathint(voteDelegate.stake(currentContract)) >= vatUrnsIlkUrnInk; + require voteDelegate_ == addrZero() => to_mathint(mkr.balanceOf(currentContract)) >= vatUrnsIlkUrnInk; + require stakingRewards.totalSupply() == stakingRewards.balanceOf(urn); + require lsmkr.balanceOf(farm) == stakingRewards.totalSupply(); + // Practical Vat assumptions + require vat.live() == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require (vatUrnsIlkUrnInk - wad) * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatUrnsIlkUrnArt == 0 || vatIlksIlkRate * vatUrnsIlkUrnArt >= vatIlksIlkDust; + // Safe to assume as Engine doesn't modify vat.gem(ilk,urn) (rule vatGemKeepsUnchanged) + require vat.gem(ilk, urn) == 0; + // Safe to assume as Engine keeps the invariant (rule inkMatchesLsmkrFarm) + require lsmkr.balanceOf(urn) == 0 || stakingRewards.balanceOf(urn) == 0; + require lsmkr.balanceOf(urn) > 0 => farm == addrZero(); + require stakingRewards.balanceOf(urn) > 0 => farm != addrZero(); + require vatUrnsIlkUrnInk == lsmkr.balanceOf(urn) + stakingRewards.balanceOf(urn); + + freeNoFee@withrevert(e, owner, index, to, wad); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = urn == addrZero(); + bool revert4 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert5 = to_mathint(wad) > max_int256(); + bool revert6 = vatUrnsIlkUrnInk < to_mathint(wad) || wad > 0 && (vatUrnsIlkUrnInk - wad) * vatIlksIlkSpot < vatUrnsIlkUrnArt * vatIlksIlkRate; + bool revert7 = farm != 0 && wad == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting draw +rule draw(address owner, uint256 index, address to, uint256 wad) { + env e; + + address other; + require other != to; + + address urn = ownerUrns(owner, index); + bytes32 ilk = ilk(); + mathint vatIlksIlkArtBefore; mathint a; + vatIlksIlkArtBefore, a, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnArtBefore; + a, vatUrnsIlkUrnArtBefore = vat.urns(ilk, urn); + mathint usdsTotalSupplyBefore = usds.totalSupply(); + mathint usdsBalanceOfToBefore = usds.balanceOf(to); + mathint usdsBalanceOfOtherBefore = usds.balanceOf(other); + + // Tokens invariants + require usdsTotalSupplyBefore >= usdsBalanceOfToBefore + usdsBalanceOfOtherBefore; + + draw(e, owner, index, to, wad); + + mathint vatIlksIlkArtAfter; mathint vatIlksIlkRateAfter; + vatIlksIlkArtAfter, vatIlksIlkRateAfter, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnArtAfter; + a, vatUrnsIlkUrnArtAfter = vat.urns(ilk, urn); + mathint usdsTotalSupplyAfter = usds.totalSupply(); + mathint usdsBalanceOfToAfter = usds.balanceOf(to); + mathint usdsBalanceOfOtherAfter = usds.balanceOf(other); + + assert vatIlksIlkArtAfter == vatIlksIlkArtBefore + _divup(wad * RAY(), vatIlksIlkRateAfter), "Assert 1"; + assert vatUrnsIlkUrnArtAfter == vatUrnsIlkUrnArtBefore + _divup(wad * RAY(), vatIlksIlkRateAfter), "Assert 2"; + assert usdsTotalSupplyAfter == usdsTotalSupplyBefore + wad, "Assert 3"; + assert usdsBalanceOfToAfter == usdsBalanceOfToBefore + wad, "Assert 4"; + assert usdsBalanceOfOtherAfter == usdsBalanceOfOtherBefore, "Assert 5"; +} + +// Verify revert rules on draw +rule draw_revert(address owner, uint256 index, address to, uint256 wad) { + env e; + + address urn = ownerUrns(owner, index); + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + + bytes32 ilk = ilk(); + mathint vatDebt = vat.debt(); + mathint vatLine = vat.Line(); + mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkLine; mathint vatIlksIlkDust; mathint a; + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, vatIlksIlkLine, vatIlksIlkDust = vat.ilks(ilk); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + mathint usdsTotalSupply = usds.totalSupply(); + mathint usdsBalanceOfTo = usds.balanceOf(to); + + storage init = lastStorage; + mathint calcVatIlksIlkRateAfter = dripSummary(ilk); + // Avoid division by zero + require calcVatIlksIlkRateAfter > 0; + + mathint dart = _divup(wad * RAY(), calcVatIlksIlkRateAfter); + + // Happening in constructor + require vat.can(currentContract, usdsJoin) == 1; + // Happening in urn init + require vat.can(urn, currentContract) == 1; + // Tokens invariants + require usdsTotalSupply >= usdsBalanceOfTo; + // Practical token assumtiopns + require usdsTotalSupply + wad <= max_uint256; + // Practical Vat assumptions + require vat.live() == 1; + require vat.wards(jug) == 1; + require calcVatIlksIlkRateAfter >= RAY() && calcVatIlksIlkRateAfter <= max_int256(); + require vatUrnsIlkUrnInk * vatIlksIlkSpot <= max_uint256; + require calcVatIlksIlkRateAfter * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatIlksIlkArt + dart <= max_uint256; + require calcVatIlksIlkRateAfter * dart <= max_int256(); + require vatDebt + vatIlksIlkArt * (calcVatIlksIlkRateAfter - vatIlksIlkRate) + (calcVatIlksIlkRateAfter * dart) <= max_int256(); + require vat.dai(currentContract) + (dart * calcVatIlksIlkRateAfter) <= max_uint256; + require vat.dai(usdsJoin) + (dart * calcVatIlksIlkRateAfter) <= max_uint256; + // Other assumptions + require wad * RAY() <= max_uint256; + + draw@withrevert(e, owner, index, to, wad) at init; + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert4 = to_mathint(dart) > max_int256(); + bool revert5 = dart > 0 && ((vatIlksIlkArt + dart) * calcVatIlksIlkRateAfter > vatIlksIlkLine || vatDebt + vatIlksIlkArt * (calcVatIlksIlkRateAfter - vatIlksIlkRate) + (calcVatIlksIlkRateAfter * dart) > vatLine); + bool revert6 = dart > 0 && vatUrnsIlkUrnInk * vatIlksIlkSpot < (vatUrnsIlkUrnArt + dart) * calcVatIlksIlkRateAfter; + bool revert7 = vatUrnsIlkUrnArt + dart > 0 && calcVatIlksIlkRateAfter * (vatUrnsIlkUrnArt + dart) < vatIlksIlkDust; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting wipe +rule wipe(address owner, uint256 index, uint256 wad) { + env e; + + address other; + require other != e.msg.sender; + + address urn = ownerUrns(owner, index); + bytes32 ilk = ilk(); + mathint vatIlksIlkArtBefore; mathint vatIlksIlkRate; mathint a; + vatIlksIlkArtBefore, vatIlksIlkRate, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnArtBefore; + a, vatUrnsIlkUrnArtBefore = vat.urns(ilk, urn); + mathint usdsTotalSupplyBefore = usds.totalSupply(); + mathint usdsBalanceOfSenderBefore = usds.balanceOf(e.msg.sender); + mathint usdsBalanceOfOtherBefore = usds.balanceOf(other); + + // Tokens invariants + require usdsTotalSupplyBefore >= usdsBalanceOfSenderBefore + usdsBalanceOfOtherBefore; + + wipe(e, owner, index, wad); + + mathint vatIlksIlkArtAfter; + vatIlksIlkArtAfter, a, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnArtAfter; + a, vatUrnsIlkUrnArtAfter = vat.urns(ilk, urn); + mathint usdsTotalSupplyAfter = usds.totalSupply(); + mathint usdsBalanceOfSenderAfter = usds.balanceOf(e.msg.sender); + mathint usdsBalanceOfOtherAfter = usds.balanceOf(other); + + assert vatIlksIlkArtAfter == vatIlksIlkArtBefore - wad * RAY() / vatIlksIlkRate, "Assert 1"; + assert vatUrnsIlkUrnArtAfter == vatUrnsIlkUrnArtBefore - wad * RAY() / vatIlksIlkRate, "Assert 2"; + assert usdsTotalSupplyAfter == usdsTotalSupplyBefore - wad, "Assert 3"; + assert usdsBalanceOfSenderAfter == usdsBalanceOfSenderBefore - wad, "Assert 4"; + assert usdsBalanceOfOtherAfter == usdsBalanceOfOtherBefore, "Assert 5"; +} + +// Verify revert rules on wipe +rule wipe_revert(address owner, uint256 index, uint256 wad) { + env e; + + address urn = ownerUrns(owner, index); + bytes32 ilk = ilk(); + mathint vatDebt = vat.debt(); + mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkLine; mathint vatIlksIlkDust; mathint a; + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, vatIlksIlkLine, vatIlksIlkDust = vat.ilks(ilk); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + mathint usdsTotalSupply = usds.totalSupply(); + mathint usdsBalanceOfSender = usds.balanceOf(e.msg.sender); + + // Avoid division by zero + require vatIlksIlkRate > 0; + + mathint dart = wad * RAY() / vatIlksIlkRate; + + // Happening in constructor + require usds.allowance(currentContract, usdsJoin) == max_uint256; + // Happening in urn init + require vat.can(urn, currentContract) == 1; + // Tokens invariants + require usdsTotalSupply >= usdsBalanceOfSender + usds.balanceOf(currentContract) + usds.balanceOf(usdsJoin); + // Practical token assumtiopns + require usdsBalanceOfSender >= to_mathint(wad); + require usds.allowance(e.msg.sender, currentContract) >= wad; + // Practical Vat assumptions + require vat.live() == 1; + require vat.wards(jug) == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require vatUrnsIlkUrnInk * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatIlksIlkRate * -dart >= min_int256(); + require vatDebt >= vatIlksIlkRate * dart; + require vat.dai(currentContract) + wad * RAY() <= max_uint256; + require to_mathint(vat.dai(usdsJoin)) >= wad * RAY(); + // Other assumptions + require wad * RAY() <= max_uint256; + + wipe@withrevert(e, owner, index, wad); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = to_mathint(dart) > max_int256(); + bool revert4 = vatUrnsIlkUrnArt < dart; + bool revert5 = vatUrnsIlkUrnArt - dart > 0 && vatIlksIlkRate * (vatUrnsIlkUrnArt - dart) < vatIlksIlkDust; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting wipeAll +rule wipeAll(address owner, uint256 index) { + env e; + + address other; + require other != e.msg.sender; + + address urn = ownerUrns(owner, index); + bytes32 ilk = ilk(); + mathint vatIlksIlkArtBefore; mathint vatIlksIlkRate; mathint a; + vatIlksIlkArtBefore, vatIlksIlkRate, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnArtBefore; + a, vatUrnsIlkUrnArtBefore = vat.urns(ilk, urn); + mathint wad = _divup(vatUrnsIlkUrnArtBefore * vatIlksIlkRate, RAY()); + mathint usdsTotalSupplyBefore = usds.totalSupply(); + mathint usdsBalanceOfSenderBefore = usds.balanceOf(e.msg.sender); + mathint usdsBalanceOfOtherBefore = usds.balanceOf(other); + + // Tokens invariants + require usdsTotalSupplyBefore >= usdsBalanceOfSenderBefore + usdsBalanceOfOtherBefore; + + wipeAll(e, owner, index); + + mathint vatIlksIlkArtAfter; + vatIlksIlkArtAfter, a, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnArtAfter; + a, vatUrnsIlkUrnArtAfter = vat.urns(ilk, urn); + mathint usdsTotalSupplyAfter = usds.totalSupply(); + mathint usdsBalanceOfSenderAfter = usds.balanceOf(e.msg.sender); + mathint usdsBalanceOfOtherAfter = usds.balanceOf(other); + + assert vatIlksIlkArtAfter == vatIlksIlkArtBefore - vatUrnsIlkUrnArtBefore, "Assert 1"; + assert vatUrnsIlkUrnArtAfter == 0, "Assert 2"; + assert usdsTotalSupplyAfter == usdsTotalSupplyBefore - wad, "Assert 3"; + assert usdsBalanceOfSenderAfter == usdsBalanceOfSenderBefore - wad, "Assert 4"; + assert usdsBalanceOfOtherAfter == usdsBalanceOfOtherBefore, "Assert 5"; +} + +// Verify revert rules on wipeAll +rule wipeAll_revert(address owner, uint256 index) { + env e; + + address urn = ownerUrns(owner, index); + bytes32 ilk = ilk(); + mathint vatDebt = vat.debt(); + mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint vatIlksIlkSpot; mathint vatIlksIlkLine; mathint vatIlksIlkDust; mathint a; + vatIlksIlkArt, vatIlksIlkRate, vatIlksIlkSpot, vatIlksIlkLine, vatIlksIlkDust = vat.ilks(ilk); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + mathint usdsTotalSupply = usds.totalSupply(); + mathint usdsBalanceOfSender = usds.balanceOf(e.msg.sender); + + mathint wad = _divup(vatUrnsIlkUrnArt * vatIlksIlkRate, RAY()); + + // Happening in constructor + require usds.allowance(currentContract, usdsJoin) == max_uint256; + // Happening in urn init + require vat.can(urn, currentContract) == 1; + // Tokens invariants + require usdsTotalSupply >= usdsBalanceOfSender + usds.balanceOf(currentContract) + usds.balanceOf(usdsJoin); + // Practical token assumtiopns + require usdsBalanceOfSender >= to_mathint(wad); + require to_mathint(usds.allowance(e.msg.sender, currentContract)) >= wad; + // Practical Vat assumptions + require vat.live() == 1; + require vat.wards(jug) == 1; + require vatIlksIlkRate >= RAY() && vatIlksIlkRate <= max_int256(); + require vatUrnsIlkUrnInk * vatIlksIlkSpot <= max_uint256; + require vatIlksIlkRate * vatIlksIlkArt <= max_uint256; + require vatIlksIlkArt >= vatUrnsIlkUrnArt; + require vatIlksIlkRate * -vatUrnsIlkUrnArt >= min_int256(); + require vatDebt >= vatIlksIlkRate * vatUrnsIlkUrnArt; + require vat.dai(currentContract) + wad * RAY() <= max_uint256; + require to_mathint(vat.dai(usdsJoin)) >= wad * RAY(); + // Other assumptions + require wad * RAY() <= max_uint256; + + wipeAll@withrevert(e, owner, index); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = to_mathint(vatUrnsIlkUrnArt) > max_int256(); + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting getReward +rule getReward(address owner, uint256 index, address farm, address to) { + env e; + + address urn = ownerUrns(owner, index); + address other; + require other != to && other != urn && other != farm; + + require urn == lockstakeUrn; + require farm == stakingRewards; + require stakingRewards.rewardsToken() == rewardsToken; + + mathint farmRewardsUrnBefore = stakingRewards.rewards(urn); + mathint rewardsTokenBalanceOfToBefore = rewardsToken.balanceOf(to); + mathint rewardsTokenBalanceOfUrnBefore = rewardsToken.balanceOf(urn); + mathint rewardsTokenBalanceOfFarmBefore = rewardsToken.balanceOf(farm); + mathint rewardsTokenBalanceOfOtherBefore = rewardsToken.balanceOf(other); + + // Tokens invariants + require to_mathint(rewardsToken.totalSupply()) >= rewardsTokenBalanceOfToBefore + rewardsTokenBalanceOfUrnBefore + rewardsTokenBalanceOfFarmBefore + rewardsTokenBalanceOfOtherBefore; + + getReward(e, owner, index, farm, to); + + mathint farmRewardsUrnAfter = stakingRewards.rewards(urn); + mathint rewardsTokenBalanceOfToAfter = rewardsToken.balanceOf(to); + mathint rewardsTokenBalanceOfUrnAfter = rewardsToken.balanceOf(urn); + mathint rewardsTokenBalanceOfFarmAfter = rewardsToken.balanceOf(farm); + mathint rewardsTokenBalanceOfOtherAfter = rewardsToken.balanceOf(other); + + assert farmRewardsUrnAfter == 0, "Assert 1"; + assert to != urn && to != farm => rewardsTokenBalanceOfToAfter == rewardsTokenBalanceOfToBefore + rewardsTokenBalanceOfUrnBefore + farmRewardsUrnBefore, "Assert 2"; + assert to == urn => rewardsTokenBalanceOfToAfter == rewardsTokenBalanceOfToBefore + farmRewardsUrnBefore, "Assert 3"; + assert to == farm => rewardsTokenBalanceOfToAfter == rewardsTokenBalanceOfToBefore + rewardsTokenBalanceOfUrnBefore, "Assert 4"; + assert to != urn => rewardsTokenBalanceOfUrnAfter == 0, "Assert 5"; + assert to != farm => rewardsTokenBalanceOfFarmAfter == rewardsTokenBalanceOfFarmBefore - farmRewardsUrnBefore, "Assert 6"; + assert rewardsTokenBalanceOfOtherAfter == rewardsTokenBalanceOfOtherBefore, "Assert 7"; +} + +// Verify revert rules on getReward +rule getReward_revert(address owner, uint256 index, address farm, address to) { + env e; + + address urn = ownerUrns(owner, index); + require farm == stakingRewards; + require stakingRewards.rewardsToken() == rewardsToken; + + mathint urnCanUrnSender = urnCan(urn, e.msg.sender); + LockstakeEngine.FarmStatus farmsFarm = farms(farm); + + // Tokens invariants + require to_mathint(rewardsToken.totalSupply()) >= rewardsToken.balanceOf(to) + rewardsToken.balanceOf(urn) + rewardsToken.balanceOf(farm); + + // Assumption from the farm + require rewardsToken.balanceOf(farm) >= stakingRewards.rewards(urn); + + getReward@withrevert(e, owner, index, farm, to); + + bool revert1 = e.msg.value > 0; + bool revert2 = urn == addrZero(); + bool revert3 = owner != e.msg.sender && urnCanUrnSender != 1; + bool revert4 = farmsFarm == LockstakeEngine.FarmStatus.UNSUPPORTED; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting onKick +rule onKick(address urn, uint256 wad) { + env e; + + require urn == lockstakeUrn; + address prevVoteDelegate = urnVoteDelegates(urn); + require prevVoteDelegate == addrZero() || prevVoteDelegate == voteDelegate; + address prevFarm = urnFarms(urn); + require prevFarm == addrZero() || prevFarm == stakingRewards; + + address other; + require other != urn; + address other2; + require other2 != prevVoteDelegate && other2 != currentContract; + address other3; + require other3 != prevFarm && other3 != urn; + + bytes32 ilk = ilk(); + mathint vatUrnsIlkUrnInk; mathint a; + vatUrnsIlkUrnInk, a = vat.urns(ilk, urn); + + address urnVoteDelegatesOtherBefore = urnVoteDelegates(other); + address urnFarmsOtherBefore = urnFarms(other); + mathint urnAuctionsUrnBefore = urnAuctions(urn); + mathint urnAuctionsOtherBefore = urnAuctions(other); + mathint mkrBalanceOfPrevVoteDelegateBefore = mkr.balanceOf(prevVoteDelegate); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfPrevFarmBefore = lsmkr.balanceOf(prevFarm); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other3); + + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkrBalanceOfPrevVoteDelegateBefore + mkrBalanceOfEngineBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfPrevFarmBefore + lsmkrBalanceOfUrnBefore + lsmkrBalanceOfOtherBefore; + + onKick(e, urn, wad); + + address urnVoteDelegatesUrnAfter = urnVoteDelegates(urn); + address urnVoteDelegatesOtherAfter = urnVoteDelegates(other); + address urnFarmsUrnAfter = urnFarms(urn); + address urnFarmsOtherAfter = urnFarms(other); + mathint urnAuctionsUrnAfter = urnAuctions(urn); + mathint urnAuctionsOtherAfter = urnAuctions(other); + mathint mkrBalanceOfPrevVoteDelegateAfter = mkr.balanceOf(prevVoteDelegate); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfPrevFarmAfter = lsmkr.balanceOf(prevFarm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other3); + + assert urnVoteDelegatesUrnAfter == addrZero(), "Assert 1"; + assert urnVoteDelegatesOtherAfter == urnVoteDelegatesOtherBefore, "Assert 2"; + assert urnFarmsUrnAfter == addrZero(), "Assert 3"; + assert urnFarmsOtherAfter == urnFarmsOtherBefore, "Assert 4"; + assert urnAuctionsUrnAfter == urnAuctionsUrnBefore + 1, "Assert 5"; + assert urnAuctionsOtherAfter == urnAuctionsOtherBefore, "Assert 6"; + assert prevVoteDelegate == addrZero() => mkrBalanceOfPrevVoteDelegateAfter == mkrBalanceOfPrevVoteDelegateBefore, "Assert 7"; + assert prevVoteDelegate != addrZero() => mkrBalanceOfPrevVoteDelegateAfter == mkrBalanceOfPrevVoteDelegateBefore - vatUrnsIlkUrnInk - wad, "Assert 8"; + assert prevVoteDelegate == addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore, "Assert 9"; + assert prevVoteDelegate != addrZero() => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore + vatUrnsIlkUrnInk + wad, "Assert 10"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 11"; + assert lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore - wad, "Assert 12"; + assert prevFarm == addrZero() => lsmkrBalanceOfPrevFarmAfter == lsmkrBalanceOfPrevFarmBefore, "Assert 13"; + assert prevFarm != addrZero() => lsmkrBalanceOfPrevFarmAfter == lsmkrBalanceOfPrevFarmBefore - vatUrnsIlkUrnInk - wad, "Assert 14"; + assert prevFarm == addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore - wad, "Assert 15"; + assert prevFarm != addrZero() => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore + vatUrnsIlkUrnInk, "Assert 16"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 17"; +} + +// Verify revert rules on onKick +rule onKick_revert(address urn, uint256 wad) { + env e; + + require urn == lockstakeUrn; + address prevVoteDelegate = urnVoteDelegates(urn); + require prevVoteDelegate == addrZero() || prevVoteDelegate == voteDelegate; + address prevFarm = urnFarms(urn); + require prevFarm == addrZero() || prevFarm == stakingRewards; + + mathint wardsSender = wards(e.msg.sender); + mathint urnAuctionsUrn = urnAuctions(urn); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk(), urn); + + // Happening in urn init + require lsmkr.allowance(urn, currentContract) == max_uint256; + // Tokens invariants + require to_mathint(lsmkr.totalSupply()) >= lsmkr.balanceOf(prevFarm) + lsmkr.balanceOf(urn) + lsmkr.balanceOf(currentContract); + require stakingRewards.totalSupply() >= stakingRewards.balanceOf(urn); + // VoteDelegate assumptions + require prevVoteDelegate == addrZero() || to_mathint(voteDelegate.stake(currentContract)) >= vatUrnsIlkUrnInk + wad; + require prevVoteDelegate == addrZero() || mkr.balanceOf(voteDelegate) >= voteDelegate.stake(currentContract); + // StakingRewards assumptions + require prevFarm == addrZero() && lsmkr.balanceOf(urn) >= wad || + prevFarm != addrZero() && to_mathint(stakingRewards.balanceOf(urn)) >= vatUrnsIlkUrnInk + wad && to_mathint(lsmkr.balanceOf(prevFarm)) >= vatUrnsIlkUrnInk + wad; + // LockstakeClipper assumption + require wad > 0; + // Practical assumption (vatUrnsIlkUrnInk + wad should be the same than the vatUrnsIlkUrnInk prev to the kick call) + require vatUrnsIlkUrnInk + wad <= max_uint256; + + onKick@withrevert(e, urn, wad); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = urnAuctionsUrn == max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting onTake +rule onTake(address urn, address who, uint256 wad) { + env e; + + address other; + require other != currentContract && other != who; + + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfWhoBefore = mkr.balanceOf(who); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other); + + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkrBalanceOfEngineBefore + mkrBalanceOfWhoBefore + mkrBalanceOfOtherBefore; + + onTake(e, urn, who, wad); + + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfWhoAfter = mkr.balanceOf(who); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other); + + assert who != currentContract => mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - wad, "Assert 1"; + assert who != currentContract => mkrBalanceOfWhoAfter == mkrBalanceOfWhoBefore + wad, "Assert 2"; + assert who == currentContract => mkrBalanceOfWhoAfter == mkrBalanceOfWhoBefore, "Assert 3"; +} + +// Verify revert rules on onTake +rule onTake_revert(address urn, address who, uint256 wad) { + env e; + + mathint wardsSender = wards(e.msg.sender); + mathint mkrBalanceOfEngine = mkr.balanceOf(currentContract); + + // Tokens invariants + require to_mathint(mkr.totalSupply()) >= mkrBalanceOfEngine + mkr.balanceOf(who); + // LockstakeClipper assumption + require mkrBalanceOfEngine >= to_mathint(wad); + + onTake@withrevert(e, urn, who, wad); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting onRemove +rule onRemove(address urn, uint256 sold, uint256 left) { + env e; + + address other; + require other != urn; + address other2; + require other2 != currentContract; + + bytes32 ilk = ilk(); + mathint fee = fee(); + mathint urnAuctionsUrnBefore = urnAuctions(urn); + mathint urnAuctionsOtherBefore = urnAuctions(other); + mathint vatUrnsIlkUrnInkBefore; mathint a; + vatUrnsIlkUrnInkBefore, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyBefore = mkr.totalSupply(); + mathint mkrBalanceOfEngineBefore = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2); + mathint lsmkrTotalSupplyBefore = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherBefore = lsmkr.balanceOf(other); + + // Happening in constructor + require fee < WAD(); + // Tokens invariants + require mkrTotalSupplyBefore >= mkrBalanceOfEngineBefore + mkrBalanceOfOtherBefore; + require lsmkrTotalSupplyBefore >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfOtherBefore; + + mathint burn = _min(sold * fee / (WAD() - fee), left); + mathint refund = left - burn; + + onRemove(e, urn, sold, left); + + mathint urnAuctionsUrnAfter = urnAuctions(urn); + mathint urnAuctionsOtherAfter = urnAuctions(other); + mathint vatUrnsIlkUrnInkAfter; + vatUrnsIlkUrnInkAfter, a = vat.urns(ilk, urn); + mathint mkrTotalSupplyAfter = mkr.totalSupply(); + mathint mkrBalanceOfEngineAfter = mkr.balanceOf(currentContract); + mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2); + mathint lsmkrTotalSupplyAfter = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(urn); + mathint lsmkrBalanceOfOtherAfter = lsmkr.balanceOf(other); + + assert urnAuctionsUrnAfter == urnAuctionsUrnBefore - 1, "Assert 1"; + assert urnAuctionsOtherAfter == urnAuctionsOtherBefore, "Assert 2"; + assert refund > 0 => vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore + refund, "Assert 3"; + assert refund == 0 => vatUrnsIlkUrnInkAfter == vatUrnsIlkUrnInkBefore, "Assert 4"; + assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - burn, "Assert 5"; + assert mkrBalanceOfEngineAfter == mkrBalanceOfEngineBefore - burn, "Assert 6"; + assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "Assert 7"; + assert refund > 0 => lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore + refund, "Assert 8"; + assert refund == 0 => lsmkrTotalSupplyAfter == lsmkrTotalSupplyBefore, "Assert 9"; + assert refund > 0 => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore + refund, "Assert 10"; + assert refund == 0 => lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore, "Assert 11"; + assert lsmkrBalanceOfOtherAfter == lsmkrBalanceOfOtherBefore, "Assert 12"; +} + +// Verify revert rules on onRemove +rule onRemove_revert(address urn, uint256 sold, uint256 left) { + env e; + + mathint wardsSender = wards(e.msg.sender); + bytes32 ilk = ilk(); + mathint fee = fee(); + mathint urnAuctionsUrn = urnAuctions(urn); + mathint vatIlksIlkArt; mathint vatIlksIlkRate; mathint a; + vatIlksIlkArt, vatIlksIlkRate, a, a, a = vat.ilks(ilk); + mathint vatUrnsIlkUrnInk; mathint vatUrnsIlkUrnArt; + vatUrnsIlkUrnInk, vatUrnsIlkUrnArt = vat.urns(ilk, urn); + mathint mkrTotalSupply = mkr.totalSupply(); + mathint mkrBalanceOfEngine = mkr.balanceOf(currentContract); + mathint lsmkrTotalSupply = lsmkr.totalSupply(); + mathint lsmkrBalanceOfUrn = lsmkr.balanceOf(urn); + + // Happening in constructor + require fee < WAD(); + // Happening in urn init + require vat.can(urn, currentContract) == 1; + // Happening in deploy scripts + require vat.wards(currentContract) == 1; + require lsmkr.wards(currentContract) == 1; + // Tokens invariants + require mkrTotalSupply >= mkrBalanceOfEngine; + require lsmkrTotalSupply >= lsmkrBalanceOfUrn; + + require sold * fee < max_uint256; + mathint burn = _min(sold * fee / (WAD() - fee), left); + mathint refund = left - burn; + + // Practical Vat assumptions + require vat.live() == 1; + require vat.wards(currentContract) == 1; + require vatUrnsIlkUrnInk + refund <= max_uint256; + require vatIlksIlkRate <= max_int256(); + // Safe to assume as Engine doesn't modify vat.gem(ilk,urn) (rule vatGemKeepsUnchanged) + require vat.gem(ilk, urn) == 0; + // Practical token assumptions + require lsmkrTotalSupply + refund <= max_uint256; + // Assumption from LockstakeClipper + require mkrBalanceOfEngine >= burn; + require urn != lsmkr && urn != addrZero(); + + onRemove@withrevert(e, urn, sold, left); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = refund > max_int256(); + bool revert4 = urnAuctionsUrn == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} diff --git a/certora/LockstakeEngineMulticall.conf b/certora/LockstakeEngineMulticall.conf new file mode 100644 index 00000000..5534cab3 --- /dev/null +++ b/certora/LockstakeEngineMulticall.conf @@ -0,0 +1,57 @@ +{ + "files": [ + "src/LockstakeEngine.sol", + "src/LockstakeUrn.sol", + "src/LockstakeMkr.sol", + "certora/harness/dss/Vat.sol", + "test/mocks/VoteDelegateMock.sol", + "certora/harness/tokens/MkrMock.sol", + "test/mocks/StakingRewardsMock.sol", + "certora/harness/MulticallExecutor.sol" + ], + "solc_map": { + "LockstakeEngine": "solc-0.8.21", + "LockstakeUrn": "solc-0.8.21", + "LockstakeMkr": "solc-0.8.21", + "Vat": "solc-0.5.12", + "VoteDelegateMock": "solc-0.8.21", + "MkrMock": "solc-0.8.21", + "StakingRewardsMock": "solc-0.8.21", + "MulticallExecutor": "solc-0.8.21" + }, + "solc_optimize_map": { + "LockstakeEngine": "200", + "LockstakeUrn": "200", + "LockstakeMkr": "200", + "Vat": "0", + "MkrMock": "0", + "VoteDelegateMock": "0", + "StakingRewardsMock": "0", + "MulticallExecutor": "0" + }, + "link": [ + "LockstakeEngine:vat=Vat", + "LockstakeEngine:mkr=MkrMock", + "LockstakeEngine:lsmkr=LockstakeMkr", + "LockstakeUrn:engine=LockstakeEngine", + "LockstakeUrn:lsmkr=LockstakeMkr", + "LockstakeUrn:vat=Vat", + "VoteDelegateMock:gov=MkrMock", + "MulticallExecutor:engine=LockstakeEngine" + ], + "verify": "LockstakeEngine:certora/LockstakeEngineMulticall.spec", + "prover_args": [ + "-rewriteMSizeAllocations true", + "-depth 0" + ], + "smt_timeout": "7000", + "rule_sanity": "basic", + "optimistic_loop": true, + // NOTE: The number of loop iterations should be at least the length of the arrays + // given to `multicall`. + "loop_iter": "4", + "multi_assert_check": true, + "parametric_contracts": ["LockstakeEngine"], + "build_cache": true, + "msg": "LockstakeEngine" +} diff --git a/certora/LockstakeEngineMulticall.spec b/certora/LockstakeEngineMulticall.spec new file mode 100644 index 00000000..72b07c7d --- /dev/null +++ b/certora/LockstakeEngineMulticall.spec @@ -0,0 +1,97 @@ +// Basic spec checking the `multicall` function + +using MulticallExecutor as multicallExecutor; +using MkrMock as mkr; +using LockstakeUrn as lockstakeUrn; + +methods { + function farms(address) external returns (LockstakeEngine.FarmStatus) envfree; + function ownerUrns(address,uint256) external returns (address) envfree; + function urnCan(address,address) external returns (uint256) envfree; + function urnFarms(address) external returns (address) envfree; + function mkr.allowance(address,address) external returns (uint256) envfree; + function mkr.balanceOf(address) external returns (uint256) envfree; + function mkr.totalSupply() external returns (uint256) envfree; + // + function _.lock(address, uint256, uint256, uint16) external => DISPATCHER(true); + function _.lock(uint256) external => DISPATCHER(true); + function _.stake(address,uint256,uint16) external => DISPATCHER(true); + function _.withdraw(address,uint256) external => DISPATCHER(true); + function _.stake(uint256,uint16) external => DISPATCHER(true); + function _.withdraw(uint256) external => DISPATCHER(true); + function _.mint(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); + // The Prover will attempt to dispatch to the following functions any unresolved + // call, if the signature fits. Otherwise it will use the summary defined by the + // `default` keyword. + function _._ external => DISPATCH [ + // currentContract.open(uint256), + currentContract.hope(address,uint256,address), + currentContract.nope(address,uint256,address), + // currentContract.selectVoteDelegate(address,uint256,address), + currentContract.selectFarm(address,uint256,address,uint16), + currentContract.lock(address,uint256,uint256,uint16), + // currentContract.lockSky(address,uint256,uint256,uint16), + // currentContract.free(address,uint256,address,uint256), + // currentContract.freeSky(address,uint256,address,uint256), + // currentContract.freeNoFee(address,uint256,address,uint256), + // currentContract.draw(address,uint256,address,uint256), + // currentContract.wipe(address,uint256,uint256), + // currentContract.wipeAll(address,uint256), + // currentContract.getReward(address,uint256,address,address) + ] default HAVOC_ALL; +} + +definition addrZero() returns address = 0x0000000000000000000000000000000000000000; + +rule hopeAndHope(address owner1, uint256 index1, address owner2, uint256 index2, address usr) { + env e; + + storage init = lastStorage; + + hope(e, owner1, index1, usr); + hope(e, owner2, index2, usr); + + storage twoCalls = lastStorage; + + multicallExecutor.hopeAndHope(e, owner1, index1, owner2, index2, usr) at init; + + assert twoCalls == lastStorage; +} + +rule hopeAndNope(address owner, uint256 index, address usr) { + env e; + + multicallExecutor.hopeAndNope(e, owner, index, usr); + + mathint urnCanUrnAfter = urnCan(ownerUrns(owner, index), usr); + + assert urnCanUrnAfter == 0; +} + + +rule selectFarmAndLock(address owner, uint256 index, address farm, uint16 ref, uint256 wad) { + env e; + + mathint mkrBalanceOfExecutorBefore = mkr.balanceOf(multicallExecutor); + mathint mkrAllowanceExecutorEngineBefore = mkr.allowance(multicallExecutor, currentContract); + + // Token invariants + require to_mathint(mkr.totalSupply()) >= mkrBalanceOfExecutorBefore + mkrAllowanceExecutorEngineBefore; + + multicallExecutor.selectFarmAndLock(e, owner, index, farm, ref, wad); + + mathint mkrBalanceOfExecutorAfter = mkr.balanceOf(multicallExecutor); + mathint mkrAllowanceExecutorEngineAfter = mkr.allowance(multicallExecutor, currentContract); + address urn = ownerUrns(owner, index); + require lockstakeUrn == urn; + address urnFarmsUrnAfter = urnFarms(urn); + + assert mkrBalanceOfExecutorAfter == mkrBalanceOfExecutorBefore - wad, "Assert 1"; + assert mkrAllowanceExecutorEngineBefore < max_uint256 => mkrAllowanceExecutorEngineAfter == mkrAllowanceExecutorEngineBefore - wad, "Assert 2"; + assert mkrAllowanceExecutorEngineBefore == max_uint256 => mkrAllowanceExecutorEngineAfter == mkrAllowanceExecutorEngineBefore, "Assert 3"; + assert urnFarmsUrnAfter == farm, "Assert 4"; + + assert farm == addrZero() || farms(farm) == LockstakeEngine.FarmStatus.ACTIVE, "farm is active"; +} diff --git a/certora/LockstakeMkr.conf b/certora/LockstakeMkr.conf new file mode 100644 index 00000000..fc9b72ad --- /dev/null +++ b/certora/LockstakeMkr.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "src/LockstakeMkr.sol" + ], + "solc": "solc-0.8.21", + "solc_optimize": "200", + "verify": "LockstakeMkr:certora/LockstakeMkr.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "build_cache": true, + "msg": "LockstakeMkr" +} diff --git a/certora/LockstakeMkr.spec b/certora/LockstakeMkr.spec new file mode 100644 index 00000000..0d7037b8 --- /dev/null +++ b/certora/LockstakeMkr.spec @@ -0,0 +1,329 @@ +// LockstakeMkr.spec + +methods { + function wards(address) external returns (uint256) envfree; + function name() external returns (string) envfree; + function symbol() external returns (string) envfree; + function version() external returns (string) envfree; + function decimals() external returns (uint8) envfree; + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; +} + +ghost balanceSum() returns mathint { + init_state axiom balanceSum() == 0; +} + +hook Sstore balanceOf[KEY address a] uint256 balance (uint256 old_balance) { + havoc balanceSum assuming balanceSum@new() == balanceSum@old() + balance - old_balance && balanceSum@new() >= 0; +} + +invariant balanceSum_equals_totalSupply() balanceSum() == to_mathint(totalSupply()); + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + address anyAddr2; + + mathint wardsBefore = wards(anyAddr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfBefore = balanceOf(anyAddr); + mathint allowanceBefore = allowance(anyAddr, anyAddr2); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfAfter = balanceOf(anyAddr); + mathint allowanceAfter = allowance(anyAddr, anyAddr2); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1"; + assert totalSupplyAfter != totalSupplyBefore => f.selector == sig:mint(address,uint256).selector || f.selector == sig:burn(address,uint256).selector, "Assert 2"; + assert balanceOfAfter != balanceOfBefore => f.selector == sig:mint(address,uint256).selector || f.selector == sig:burn(address,uint256).selector || f.selector == sig:transfer(address,uint256).selector || f.selector == sig:transferFrom(address,address,uint256).selector, "Assert 3"; + assert allowanceAfter != allowanceBefore => f.selector == sig:burn(address,uint256).selector || f.selector == sig:transferFrom(address,address,uint256).selector || f.selector == sig:approve(address,uint256).selector, "Assert 4"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 1, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on rely +rule rely_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting deny +rule deny(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + deny(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 0, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on deny +rule deny_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting transfer +rule transfer(address to, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != e.msg.sender && other != to; + + mathint balanceOfSenderBefore = balanceOf(e.msg.sender); + mathint balanceOfToBefore = balanceOf(to); + mathint balanceOfOtherBefore = balanceOf(other); + + transfer(e, to, value); + + mathint balanceOfSenderAfter = balanceOf(e.msg.sender); + mathint balanceOfToAfter = balanceOf(to); + mathint balanceOfOtherAfter = balanceOf(other); + + assert e.msg.sender != to => balanceOfSenderAfter == balanceOfSenderBefore - value, "Assert 1"; + assert e.msg.sender != to => balanceOfToAfter == balanceOfToBefore + value, "Assert 2"; + assert e.msg.sender == to => balanceOfSenderAfter == balanceOfSenderBefore, "Assert 3"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "Assert 4"; +} + +// Verify revert rules on transfer +rule transfer_revert(address to, uint256 value) { + env e; + + mathint balanceOfSender = balanceOf(e.msg.sender); + + transfer@withrevert(e, to, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = to == 0 || to == currentContract; + bool revert3 = balanceOfSender < to_mathint(value); + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting transferFrom +rule transferFrom(address from, address to, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != from && other != to; + address other2; address other3; + require other2 != from || other3 != e.msg.sender; + address anyUsr; address anyUsr2; + + mathint balanceOfFromBefore = balanceOf(from); + mathint balanceOfToBefore = balanceOf(to); + mathint balanceOfOtherBefore = balanceOf(other); + mathint allowanceFromSenderBefore = allowance(from, e.msg.sender); + mathint allowanceOtherBefore = allowance(other2, other3); + + transferFrom(e, from, to, value); + + mathint balanceOfFromAfter = balanceOf(from); + mathint balanceOfToAfter = balanceOf(to); + mathint balanceOfOtherAfter = balanceOf(other); + mathint allowanceFromSenderAfter = allowance(from, e.msg.sender); + mathint allowanceOtherAfter = allowance(other2, other3); + + assert from != to => balanceOfFromAfter == balanceOfFromBefore - value, "Assert 1"; + assert from != to => balanceOfToAfter == balanceOfToBefore + value, "Assert 2"; + assert from == to => balanceOfFromAfter == balanceOfFromBefore, "Assert 3"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "Assert 4"; + assert e.msg.sender != from && allowanceFromSenderBefore != max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore - value, "Assert 5"; + assert e.msg.sender == from => allowanceFromSenderAfter == allowanceFromSenderBefore, "Assert 6"; + assert allowanceFromSenderBefore == max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore, "Assert 7"; + assert allowanceOtherAfter == allowanceOtherBefore, "Assert 8"; +} + +// Verify revert rules on transferFrom +rule transferFrom_revert(address from, address to, uint256 value) { + env e; + + mathint balanceOfFrom = balanceOf(from); + mathint allowanceFromSender = allowance(from, e.msg.sender); + + transferFrom@withrevert(e, from, to, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = to == 0 || to == currentContract; + bool revert3 = balanceOfFrom < to_mathint(value); + bool revert4 = allowanceFromSender < to_mathint(value) && e.msg.sender != from; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting approve +rule approve(address spender, uint256 value) { + env e; + + address other; address other2; + require other != e.msg.sender || other2 != spender; + + mathint allowanceOtherBefore = allowance(other, other2); + + approve(e, spender, value); + + mathint allowanceSenderSpenderAfter = allowance(e.msg.sender, spender); + mathint allowanceOtherAfter = allowance(other, other2); + + assert allowanceSenderSpenderAfter == to_mathint(value), "Assert 1"; + assert allowanceOtherAfter == allowanceOtherBefore, "Assert 2"; +} + +// Verify revert rules on approve +rule approve_revert(address spender, uint256 value) { + env e; + + approve@withrevert(e, spender, value); + + bool revert1 = e.msg.value > 0; + + assert lastReverted <=> revert1, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting mint +rule mint(address to, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != to; + + bool senderSameAsTo = e.msg.sender == to; + + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfToBefore = balanceOf(to); + mathint balanceOfOtherBefore = balanceOf(other); + + mint(e, to, value); + + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfToAfter = balanceOf(to); + mathint balanceOfOtherAfter = balanceOf(other); + + assert totalSupplyAfter == totalSupplyBefore + value, "Assert 1"; + assert balanceOfToAfter == balanceOfToBefore + value, "Assert 2"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "Assert 3"; +} + +// Verify revert rules on mint +rule mint_revert(address to, uint256 value) { + env e; + + // Save the totalSupply and sender balance before minting + mathint totalSupply = totalSupply(); + mathint wardsSender = wards(e.msg.sender); + + mint@withrevert(e, to, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = totalSupply + value > max_uint256; + bool revert4 = to == 0 || to == currentContract; + + assert lastReverted <=> revert1 || revert2 || revert3 || revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting burn +rule burn(address from, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != from; + address other2; address other3; + require other2 != from || other3 != e.msg.sender; + + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfFromBefore = balanceOf(from); + mathint balanceOfOtherBefore = balanceOf(other); + mathint allowanceFromSenderBefore = allowance(from, e.msg.sender); + mathint allowanceOtherBefore = allowance(other2, other3); + + burn(e, from, value); + + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfSenderAfter = balanceOf(e.msg.sender); + mathint balanceOfFromAfter = balanceOf(from); + mathint balanceOfOtherAfter = balanceOf(other); + mathint allowanceFromSenderAfter = allowance(from, e.msg.sender); + mathint allowanceOtherAfter = allowance(other2, other3); + + assert totalSupplyAfter == totalSupplyBefore - value, "Assert 1"; + assert balanceOfFromAfter == balanceOfFromBefore - value, "Assert 2"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "Assert 3"; + assert e.msg.sender != from && allowanceFromSenderBefore != max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore - value, "Assert 4"; + assert e.msg.sender == from => allowanceFromSenderAfter == allowanceFromSenderBefore, "Assert 5"; + assert allowanceFromSenderBefore == max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore, "Assert 6"; + assert allowanceOtherAfter == allowanceOtherBefore, "Assert 7"; +} + +// Verify revert rules on burn +rule burn_revert(address from, uint256 value) { + env e; + + mathint balanceOfFrom = balanceOf(from); + mathint allowanceFromSender = allowance(from, e.msg.sender); + + burn@withrevert(e, from, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = balanceOfFrom < to_mathint(value); + bool revert3 = from != e.msg.sender && allowanceFromSender < to_mathint(value); + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} diff --git a/certora/LockstakeUrn.conf b/certora/LockstakeUrn.conf new file mode 100644 index 00000000..d6b43ebc --- /dev/null +++ b/certora/LockstakeUrn.conf @@ -0,0 +1,34 @@ +{ + "files": [ + "src/LockstakeUrn.sol", + "src/LockstakeMkr.sol", + "certora/harness/dss/Vat.sol", + "test/mocks/StakingRewardsMock.sol", + "certora/harness/tokens/RewardsMock.sol", + ], + "solc_map": { + "LockstakeUrn": "solc-0.8.21", + "LockstakeMkr": "solc-0.8.21", + "Vat": "solc-0.5.12", + "StakingRewardsMock": "solc-0.8.21", + "RewardsMock": "solc-0.8.21", + }, + "solc_optimize_map": { + "LockstakeUrn": "200", + "LockstakeMkr": "200", + "Vat": "0", + "StakingRewardsMock": "200", + "RewardsMock": "200", + }, + "link": [ + "StakingRewardsMock:rewardsToken=RewardsMock", + "StakingRewardsMock:stakingToken=LockstakeMkr", + "LockstakeUrn:lsmkr=LockstakeMkr", + "LockstakeUrn:vat=Vat" + ], + "verify": "LockstakeUrn:certora/LockstakeUrn.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "build_cache": true, + "msg": "LockstakeUrn" +} diff --git a/certora/LockstakeUrn.spec b/certora/LockstakeUrn.spec new file mode 100644 index 00000000..bd96ecc4 --- /dev/null +++ b/certora/LockstakeUrn.spec @@ -0,0 +1,180 @@ +// LockstakeUrn.spec + +using Vat as vat; +using LockstakeMkr as lsmkr; +using StakingRewardsMock as stakingRewards; +using RewardsMock as rewardsToken; + +methods { + function engine() external returns (address) envfree; + function vat.can(address,address) external returns (uint256) envfree; + function lsmkr.allowance(address,address) external returns (uint256) envfree; + function lsmkr.balanceOf(address) external returns (uint256) envfree; + function lsmkr.totalSupply() external returns (uint256) envfree; + function stakingRewards.balanceOf(address) external returns (uint256) envfree; + function stakingRewards.totalSupply() external returns (uint256) envfree; + function stakingRewards.rewards(address) external returns (uint256) envfree; + function _.stake(uint256,uint16) external => DISPATCHER(true); + function _.withdraw(uint256) external => DISPATCHER(true); + function _.getReward() external => DISPATCHER(true); + function _.rewardsToken() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function rewardsToken.balanceOf(address) external returns (uint256) envfree; + function rewardsToken.totalSupply() external returns (uint256) envfree; +} + +// Verify correct storage changes for non reverting init +rule init() { + env e; + + address engine = engine(); + + init(e); + + mathint vatCanUrnEngineAfter = vat.can(currentContract, engine); + mathint lsmkrAllowanceUrnEngineAfter = lsmkr.allowance(currentContract, engine); + + assert vatCanUrnEngineAfter == 1, "Assert 1"; + assert lsmkrAllowanceUrnEngineAfter == max_uint256, "Assert 2"; +} + +// Verify revert rules on init +rule init_revert() { + env e; + + address engine = engine(); + + init@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = engine != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting stake +rule stake(address farm, uint256 wad, uint16 ref) { + env e; + + require farm == stakingRewards; + + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(currentContract); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + require to_mathint(lsmkr.totalSupply()) >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore; + mathint farmBalanceOfUrnBefore = stakingRewards.balanceOf(currentContract); + + stake(e, farm, wad, ref); + + mathint lsmkrAllowanceUrnFarmAfter = lsmkr.allowance(currentContract, farm); + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(currentContract); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint farmBalanceOfUrnAfter = stakingRewards.balanceOf(currentContract); + + assert lsmkrAllowanceUrnFarmAfter == 0 || lsmkrAllowanceUrnFarmAfter == max_uint256, "Assert 1"; + assert lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore - wad, "Assert 2"; + assert lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore + wad, "Assert 3"; + assert farmBalanceOfUrnAfter == farmBalanceOfUrnBefore + wad, "Assert 4"; +} + +// Verify revert rules on stake +rule stake_revert(address farm, uint256 wad, uint16 ref) { + env e; + + require farm == stakingRewards; + + require wad > 0; + require lsmkr.balanceOf(currentContract) >= wad; + require lsmkr.totalSupply() >= wad; + require stakingRewards.balanceOf(currentContract) + wad <= max_uint256; + require stakingRewards.totalSupply() + wad <= max_uint256; + + address engine = engine(); + + stake@withrevert(e, farm, wad, ref); + + bool revert1 = e.msg.value > 0; + bool revert2 = engine != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting withdraw +rule withdraw(address farm, uint256 wad) { + env e; + + require farm == stakingRewards; + + mathint lsmkrBalanceOfUrnBefore = lsmkr.balanceOf(currentContract); + mathint lsmkrBalanceOfFarmBefore = lsmkr.balanceOf(farm); + require to_mathint(lsmkr.totalSupply()) >= lsmkrBalanceOfUrnBefore + lsmkrBalanceOfFarmBefore; + mathint farmBalanceOfUrnBefore = stakingRewards.balanceOf(currentContract); + + withdraw(e, farm, wad); + + mathint lsmkrBalanceOfUrnAfter = lsmkr.balanceOf(currentContract); + mathint lsmkrBalanceOfFarmAfter = lsmkr.balanceOf(farm); + mathint farmBalanceOfUrnAfter = stakingRewards.balanceOf(currentContract); + + assert lsmkrBalanceOfUrnAfter == lsmkrBalanceOfUrnBefore + wad, "Assert 1"; + assert lsmkrBalanceOfFarmAfter == lsmkrBalanceOfFarmBefore - wad, "Assert 2"; + assert farmBalanceOfUrnAfter == farmBalanceOfUrnBefore - wad, "Assert 3"; +} + +// Verify revert rules on withdraw +rule withdraw_revert(address farm, uint256 wad) { + env e; + + require farm == stakingRewards; + + require wad > 0; + require lsmkr.balanceOf(farm) >= wad; + require lsmkr.balanceOf(currentContract) + wad <= max_uint256; + require lsmkr.totalSupply() + wad <= max_uint256; + require stakingRewards.balanceOf(currentContract) >= wad; + require stakingRewards.totalSupply() >= wad; + + address engine = engine(); + + withdraw@withrevert(e, farm, wad); + + bool revert1 = e.msg.value > 0; + bool revert2 = engine != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting getReward +rule getReward(address farm, address to) { + env e; + + require farm == stakingRewards; + + mathint rewardsTokenBalanceOfToBefore = rewardsToken.balanceOf(to); + require rewardsTokenBalanceOfToBefore <= to_mathint(rewardsToken.totalSupply()); + require rewardsTokenBalanceOfToBefore + rewardsToken.balanceOf(currentContract) + rewardsToken.balanceOf(stakingRewards) <= to_mathint(rewardsToken.totalSupply()); + + getReward(e, farm, to); + + mathint rewardsTokenBalanceOfToAfter = rewardsToken.balanceOf(to); + + assert rewardsTokenBalanceOfToAfter >= rewardsTokenBalanceOfToBefore, "Assert 1"; +} + +// Verify revert rules on getReward +rule getReward_revert(address farm, address to) { + env e; + + require farm == stakingRewards; + + require rewardsToken.balanceOf(stakingRewards) >= stakingRewards.rewards(currentContract); + + address engine = engine(); + + getReward@withrevert(e, farm, to); + + bool revert1 = e.msg.value > 0; + bool revert2 = engine != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} diff --git a/certora/harness/MulticallExecutor.sol b/certora/harness/MulticallExecutor.sol new file mode 100644 index 00000000..36d5ccd7 --- /dev/null +++ b/certora/harness/MulticallExecutor.sol @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.21; + +import { LockstakeEngine } from "../../src/LockstakeEngine.sol"; + + +contract MulticallExecutor { + + LockstakeEngine public engine; + + function hopeAndHope(address owner1, uint256 index1, address owner2, uint256 index2, address usr) public { + + bytes[] memory calls = new bytes[](2); + calls[0] = abi.encodeWithSignature("hope(address,uint256,address)", owner1, index1, usr); + calls[1] = abi.encodeWithSignature("hope(address,uint256,address)", owner2, index2, usr); + engine.multicall(calls); + } + + function hopeAndNope(address owner, uint256 index, address usr) public { + bytes[] memory calls = new bytes[](2); + calls[0] = abi.encodeWithSignature("hope(address,uint256,address)", owner, index, usr); + calls[1] = abi.encodeWithSignature("nope(address,uint256,address)", owner, index, usr); + engine.multicall(calls); + } + + function selectFarmAndLock( + address owner, + uint256 index, + address farm, + uint16 ref, + uint256 wad + ) public { + + bytes[] memory calls = new bytes[](2); + calls[0] = abi.encodeWithSignature( + "selectFarm(address,uint256,address,uint16)", owner, index, farm, ref + ); + calls[1] = abi.encodeWithSignature( + "lock(address,uint256,uint256,uint16)", owner, index, wad, ref + ); + engine.multicall(calls); + } +} diff --git a/certora/harness/StakingRewards2Mock.sol b/certora/harness/StakingRewards2Mock.sol new file mode 100644 index 00000000..251806b6 --- /dev/null +++ b/certora/harness/StakingRewards2Mock.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import {StakingRewardsMock} from "../../test/mocks/StakingRewardsMock.sol"; + +contract StakingRewards2Mock is StakingRewardsMock { + + constructor(address rewardsToken, address stakingToken) StakingRewardsMock(rewardsToken, stakingToken) { + } +} diff --git a/certora/harness/VoteDelegate2Mock.sol b/certora/harness/VoteDelegate2Mock.sol new file mode 100644 index 00000000..83595f18 --- /dev/null +++ b/certora/harness/VoteDelegate2Mock.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import {VoteDelegateMock} from "../../test/mocks/VoteDelegateMock.sol"; + +contract VoteDelegate2Mock is VoteDelegateMock { + + constructor(address gov) VoteDelegateMock(gov) { + } +} diff --git a/certora/harness/dss/ClipperCallee.sol b/certora/harness/dss/ClipperCallee.sol new file mode 100644 index 00000000..4ff4e53a --- /dev/null +++ b/certora/harness/dss/ClipperCallee.sol @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +// taken from: ./LockstakeClipper.t.sol + +pragma solidity ^0.8.21; + +import { LockstakeClipper } from "src/LockstakeClipper.sol"; + +contract BadGuy { + LockstakeClipper clip; + + constructor(LockstakeClipper clip_) { + clip = clip_; + } + + function clipperCall(address sender, uint256 owe, uint256 slice, bytes calldata data) + external { + sender; owe; slice; data; + clip.take({ // attempt reentrancy + id: 1, + amt: 25 ether, + max: 5 ether * 10E27, + who: address(this), + data: "" + }); + } +} + +contract RedoGuy { + LockstakeClipper clip; + + constructor(LockstakeClipper clip_) { + clip = clip_; + } + + function clipperCall( + address sender, uint256 owe, uint256 slice, bytes calldata data + ) external { + owe; slice; data; + clip.redo(1, sender); + } +} + +contract KickGuy { + LockstakeClipper clip; + + constructor(LockstakeClipper clip_) { + clip = clip_; + } + + function clipperCall( + address sender, uint256 owe, uint256 slice, bytes calldata data + ) external { + sender; owe; slice; data; + clip.kick(1, 1, address(0), address(0)); + } +} + +contract FileUintGuy { + LockstakeClipper clip; + + constructor(LockstakeClipper clip_) { + clip = clip_; + } + + function clipperCall( + address sender, uint256 owe, uint256 slice, bytes calldata data + ) external { + sender; owe; slice; data; + clip.file("stopped", 1); + } +} + +contract FileAddrGuy { + LockstakeClipper clip; + + constructor(LockstakeClipper clip_) { + clip = clip_; + } + + function clipperCall( + address sender, uint256 owe, uint256 slice, bytes calldata data + ) external { + sender; owe; slice; data; + clip.file("vow", address(123)); + } +} + +contract YankGuy { + LockstakeClipper clip; + + constructor(LockstakeClipper clip_) { + clip = clip_; + } + + function clipperCall( + address sender, uint256 owe, uint256 slice, bytes calldata data + ) external { + sender; owe; slice; data; + clip.yank(1); + } +} diff --git a/certora/harness/dss/Dog.sol b/certora/harness/dss/Dog.sol new file mode 100644 index 00000000..d941d80f --- /dev/null +++ b/certora/harness/dss/Dog.sol @@ -0,0 +1,249 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +/// dog.sol -- Dai liquidation module 2.0 + +// Copyright (C) 2020-2022 Dai Foundation +// +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. +// +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. +// +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . + +pragma solidity ^0.6.12; + +interface ClipperLike { + function ilk() external view returns (bytes32); + function kick( + uint256 tab, + uint256 lot, + address usr, + address kpr + ) external returns (uint256); +} + +interface VatLike { + function ilks(bytes32) external view returns ( + uint256 Art, // [wad] + uint256 rate, // [ray] + uint256 spot, // [ray] + uint256 line, // [rad] + uint256 dust // [rad] + ); + function urns(bytes32,address) external view returns ( + uint256 ink, // [wad] + uint256 art // [wad] + ); + function grab(bytes32,address,address,address,int256,int256) external; + function hope(address) external; + function nope(address) external; +} + +interface VowLike { + function fess(uint256) external; +} + +contract Dog { + // --- Auth --- + mapping (address => uint256) public wards; + function rely(address usr) external auth { wards[usr] = 1; emit Rely(usr); } + function deny(address usr) external auth { wards[usr] = 0; emit Deny(usr); } + modifier auth { + require(wards[msg.sender] == 1, "Dog/not-authorized"); + _; + } + + // --- Data --- + struct Ilk { + address clip; // Liquidator + uint256 chop; // Liquidation Penalty [wad] + uint256 hole; // Max DAI needed to cover debt+fees of active auctions per ilk [rad] + uint256 dirt; // Amt DAI needed to cover debt+fees of active auctions per ilk [rad] + } + + VatLike immutable public vat; // CDP Engine + + mapping (bytes32 => Ilk) public ilks; + + VowLike public vow; // Debt Engine + uint256 public live; // Active Flag + uint256 public Hole; // Max DAI needed to cover debt+fees of active auctions [rad] + uint256 public Dirt; // Amt DAI needed to cover debt+fees of active auctions [rad] + + // --- Events --- + event Rely(address indexed usr); + event Deny(address indexed usr); + + event File(bytes32 indexed what, uint256 data); + event File(bytes32 indexed what, address data); + event File(bytes32 indexed ilk, bytes32 indexed what, uint256 data); + event File(bytes32 indexed ilk, bytes32 indexed what, address clip); + + event Bark( + bytes32 indexed ilk, + address indexed urn, + uint256 ink, + uint256 art, + uint256 due, + address clip, + uint256 indexed id + ); + event Digs(bytes32 indexed ilk, uint256 rad); + event Cage(); + + // --- Init --- + constructor(address vat_) public { + vat = VatLike(vat_); + live = 1; + wards[msg.sender] = 1; + emit Rely(msg.sender); + } + + // --- Math --- + uint256 constant WAD = 10 ** 18; + + function min(uint256 x, uint256 y) internal pure returns (uint256 z) { + z = x <= y ? x : y; + } + 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 mul(uint256 x, uint256 y) internal pure returns (uint256 z) { + require(y == 0 || (z = x * y) / y == x); + } + + // --- Administration --- + function file(bytes32 what, address data) external auth { + if (what == "vow") vow = VowLike(data); + else revert("Dog/file-unrecognized-param"); + emit File(what, data); + } + function file(bytes32 what, uint256 data) external auth { + if (what == "Hole") Hole = data; + else revert("Dog/file-unrecognized-param"); + emit File(what, data); + } + function file(bytes32 ilk, bytes32 what, uint256 data) external auth { + if (what == "chop") { + require(data >= WAD, "Dog/file-chop-lt-WAD"); + ilks[ilk].chop = data; + } else if (what == "hole") ilks[ilk].hole = data; + else revert("Dog/file-unrecognized-param"); + emit File(ilk, what, data); + } + function file(bytes32 ilk, bytes32 what, address clip) external auth { + if (what == "clip") { + require(ilk == ClipperLike(clip).ilk(), "Dog/file-ilk-neq-clip.ilk"); + ilks[ilk].clip = clip; + } else revert("Dog/file-unrecognized-param"); + emit File(ilk, what, clip); + } + + function chop(bytes32 ilk) external view returns (uint256) { + return ilks[ilk].chop; + } + + // --- CDP Liquidation: all bark and no bite --- + // + // Liquidate a Vault and start a Dutch auction to sell its collateral for DAI. + // + // The third argument is the address that will receive the liquidation reward, if any. + // + // The entire Vault will be liquidated except when the target amount of DAI to be raised in + // the resulting auction (debt of Vault + liquidation penalty) causes either Dirt to exceed + // Hole or ilk.dirt to exceed ilk.hole by an economically significant amount. In that + // case, a partial liquidation is performed to respect the global and per-ilk limits on + // outstanding DAI target. The one exception is if the resulting auction would likely + // have too little collateral to be interesting to Keepers (debt taken from Vault < ilk.dust), + // in which case the function reverts. Please refer to the code and comments within if + // more detail is desired. + function bark(bytes32 ilk, address urn, address kpr) external returns (uint256 id) { + require(live == 1, "Dog/not-live"); + + (uint256 ink, uint256 art) = vat.urns(ilk, urn); + Ilk memory milk = ilks[ilk]; + uint256 dart; + uint256 rate; + uint256 dust; + { + uint256 spot; + (,rate, spot,, dust) = vat.ilks(ilk); + require(spot > 0 && mul(ink, spot) < mul(art, rate), "Dog/not-unsafe"); + + // Get the minimum value between: + // 1) Remaining space in the general Hole + // 2) Remaining space in the collateral hole + require(Hole > Dirt && milk.hole > milk.dirt, "Dog/liquidation-limit-hit"); + uint256 room = min(Hole - Dirt, milk.hole - milk.dirt); + + // uint256.max()/(RAD*WAD) = 115,792,089,237,316 + dart = min(art, mul(room, WAD) / rate / milk.chop); + + // Partial liquidation edge case logic + if (art > dart) { + if (mul(art - dart, rate) < dust) { + + // If the leftover Vault would be dusty, just liquidate it entirely. + // This will result in at least one of dirt_i > hole_i or Dirt > Hole becoming true. + // The amount of excess will be bounded above by ceiling(dust_i * chop_i / WAD). + // This deviation is assumed to be small compared to both hole_i and Hole, so that + // the extra amount of target DAI over the limits intended is not of economic concern. + dart = art; + } else { + + // In a partial liquidation, the resulting auction should also be non-dusty. + require(mul(dart, rate) >= dust, "Dog/dusty-auction-from-partial-liquidation"); + } + } + } + + uint256 dink = mul(ink, dart) / art; + + require(dink > 0, "Dog/null-auction"); + require(dart <= 2**255 && dink <= 2**255, "Dog/overflow"); + + vat.grab( + ilk, urn, milk.clip, address(vow), -int256(dink), -int256(dart) + ); + + uint256 due = mul(dart, rate); + vow.fess(due); + + { // Avoid stack too deep + // This calcuation will overflow if dart*rate exceeds ~10^14 + uint256 tab = mul(due, milk.chop) / WAD; + Dirt = add(Dirt, tab); + ilks[ilk].dirt = add(milk.dirt, tab); + + id = ClipperLike(milk.clip).kick({ + tab: tab, + lot: dink, + usr: urn, + kpr: kpr + }); + } + + emit Bark(ilk, urn, dink, dart, due, milk.clip, id); + } + + function digs(bytes32 ilk, uint256 rad) external auth { + Dirt = sub(Dirt, rad); + ilks[ilk].dirt = sub(ilks[ilk].dirt, rad); + emit Digs(ilk, rad); + } + + function cage() external auth { + live = 0; + emit Cage(); + } +} diff --git a/certora/harness/dss/Jug.sol b/certora/harness/dss/Jug.sol new file mode 100644 index 00000000..c9ec7086 --- /dev/null +++ b/certora/harness/dss/Jug.sol @@ -0,0 +1,154 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +/// jug.sol -- Dai Lending Rate + +// Copyright (C) 2018 Rain +// +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. +// +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. +// +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . + +pragma solidity >=0.5.12; + +contract LibNote { + event LogNote( + bytes4 indexed sig, + address indexed usr, + bytes32 indexed arg1, + bytes32 indexed arg2, + bytes data + ) anonymous; + + modifier note { + _; + assembly { + // log an 'anonymous' event with a constant 6 words of calldata + // and four indexed topics: selector, caller, arg1 and arg2 + let mark := msize() // end of memory ensures zero + mstore(0x40, add(mark, 288)) // update free memory pointer + mstore(mark, 0x20) // bytes type data offset + mstore(add(mark, 0x20), 224) // bytes size (padded) + calldatacopy(add(mark, 0x40), 0, 224) // bytes payload + log4(mark, 288, // calldata + shl(224, shr(224, calldataload(0))), // msg.sig + caller(), // msg.sender + calldataload(4), // arg1 + calldataload(36) // arg2 + ) + } + } +} + +interface VatLike { + function ilks(bytes32) external returns ( + uint256 Art, // [wad] + uint256 rate // [ray] + ); + function fold(bytes32,address,int) external; +} + +contract Jug is LibNote { + // --- Auth --- + mapping (address => uint) public wards; + function rely(address usr) external note auth { wards[usr] = 1; } + function deny(address usr) external note auth { wards[usr] = 0; } + modifier auth { + require(wards[msg.sender] == 1, "Jug/not-authorized"); + _; + } + + // --- Data --- + struct Ilk { + uint256 duty; // Collateral-specific, per-second stability fee contribution [ray] + uint256 rho; // Time of last drip [unix epoch time] + } + + mapping (bytes32 => Ilk) public ilks; + VatLike public vat; // CDP Engine + address public vow; // Debt Engine + uint256 public base; // Global, per-second stability fee contribution [ray] + + // --- Init --- + constructor(address vat_) public { + wards[msg.sender] = 1; + vat = VatLike(vat_); + } + + // --- Math --- + function rpow(uint x, uint n, uint b) internal pure returns (uint z) { + assembly { + switch x case 0 {switch n case 0 {z := b} default {z := 0}} + default { + switch mod(n, 2) case 0 { z := b } default { z := x } + let half := div(b, 2) // for rounding. + for { n := div(n, 2) } n { n := div(n,2) } { + let xx := mul(x, x) + if iszero(eq(div(xx, x), x)) { revert(0,0) } + let xxRound := add(xx, half) + if lt(xxRound, xx) { revert(0,0) } + x := div(xxRound, b) + if mod(n,2) { + let zx := mul(z, x) + if and(iszero(iszero(x)), iszero(eq(div(zx, x), z))) { revert(0,0) } + let zxRound := add(zx, half) + if lt(zxRound, zx) { revert(0,0) } + z := div(zxRound, b) + } + } + } + } + } + uint256 constant ONE = 10 ** 27; + function add(uint x, uint y) internal pure returns (uint z) { + z = x + y; + require(z >= x); + } + function diff(uint x, uint y) internal pure returns (int z) { + z = int(x) - int(y); + require(int(x) >= 0 && int(y) >= 0); + } + function rmul(uint x, uint y) internal pure returns (uint z) { + z = x * y; + require(y == 0 || z / y == x); + z = z / ONE; + } + + // --- Administration --- + function init(bytes32 ilk) external note auth { + Ilk storage i = ilks[ilk]; + require(i.duty == 0, "Jug/ilk-already-init"); + i.duty = ONE; + i.rho = now; + } + function file(bytes32 ilk, bytes32 what, uint data) external note auth { + require(now == ilks[ilk].rho, "Jug/rho-not-updated"); + if (what == "duty") ilks[ilk].duty = data; + else revert("Jug/file-unrecognized-param"); + } + function file(bytes32 what, uint data) external note auth { + if (what == "base") base = data; + else revert("Jug/file-unrecognized-param"); + } + function file(bytes32 what, address data) external note auth { + if (what == "vow") vow = data; + else revert("Jug/file-unrecognized-param"); + } + + // --- Stability Fee Collection --- + function drip(bytes32 ilk) external note returns (uint rate) { + require(now >= ilks[ilk].rho, "Jug/invalid-now"); + (, uint prev) = vat.ilks(ilk); + rate = rmul(rpow(add(base, ilks[ilk].duty), now - ilks[ilk].rho, ONE), prev); + vat.fold(ilk, vow, diff(rate, prev)); + ilks[ilk].rho = now; + } +} diff --git a/certora/harness/dss/Spotter.sol b/certora/harness/dss/Spotter.sol new file mode 100644 index 00000000..a7785d87 --- /dev/null +++ b/certora/harness/dss/Spotter.sol @@ -0,0 +1,133 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +/// spot.sol -- Spotter + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. +// +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. +// +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . + +pragma solidity >=0.5.12; + +contract LibNote { + event LogNote( + bytes4 indexed sig, + address indexed usr, + bytes32 indexed arg1, + bytes32 indexed arg2, + bytes data + ) anonymous; + + modifier note { + _; + assembly { + // log an 'anonymous' event with a constant 6 words of calldata + // and four indexed topics: selector, caller, arg1 and arg2 + let mark := msize() // end of memory ensures zero + mstore(0x40, add(mark, 288)) // update free memory pointer + mstore(mark, 0x20) // bytes type data offset + mstore(add(mark, 0x20), 224) // bytes size (padded) + calldatacopy(add(mark, 0x40), 0, 224) // bytes payload + log4(mark, 288, // calldata + shl(224, shr(224, calldataload(0))), // msg.sig + caller(), // msg.sender + calldataload(4), // arg1 + calldataload(36) // arg2 + ) + } + } +} + +interface VatLike { + function file(bytes32, bytes32, uint) external; +} + +interface PipLike { + function peek() external returns (bytes32, bool); +} + +contract Spotter is LibNote { + // --- Auth --- + mapping (address => uint) public wards; + function rely(address guy) external note auth { wards[guy] = 1; } + function deny(address guy) external note auth { wards[guy] = 0; } + modifier auth { + require(wards[msg.sender] == 1, "Spotter/not-authorized"); + _; + } + + // --- Data --- + struct Ilk { + PipLike pip; // Price Feed + uint256 mat; // Liquidation ratio [ray] + } + + mapping (bytes32 => Ilk) public ilks; + + VatLike public vat; // CDP Engine + uint256 public par; // ref per dai [ray] + + uint256 public live; + + // --- Events --- + event Poke( + bytes32 ilk, + bytes32 val, // [wad] + uint256 spot // [ray] + ); + + // --- Init --- + constructor(address vat_) public { + wards[msg.sender] = 1; + vat = VatLike(vat_); + par = ONE; + live = 1; + } + + // --- Math --- + uint constant ONE = 10 ** 27; + + function mul(uint x, uint y) internal pure returns (uint z) { + require(y == 0 || (z = x * y) / y == x); + } + function rdiv(uint x, uint y) internal pure returns (uint z) { + z = mul(x, ONE) / y; + } + + // --- Administration --- + function file(bytes32 ilk, bytes32 what, address pip_) external note auth { + require(live == 1, "Spotter/not-live"); + if (what == "pip") ilks[ilk].pip = PipLike(pip_); + else revert("Spotter/file-unrecognized-param"); + } + function file(bytes32 what, uint data) external note auth { + require(live == 1, "Spotter/not-live"); + if (what == "par") par = data; + else revert("Spotter/file-unrecognized-param"); + } + function file(bytes32 ilk, bytes32 what, uint data) external note auth { + require(live == 1, "Spotter/not-live"); + if (what == "mat") ilks[ilk].mat = data; + else revert("Spotter/file-unrecognized-param"); + } + + // --- Update value --- + function poke(bytes32 ilk) external { + (bytes32 val, bool has) = ilks[ilk].pip.peek(); + uint256 spot = has ? rdiv(rdiv(mul(uint(val), 10 ** 9), par), ilks[ilk].mat) : 0; + vat.file(ilk, "spot", spot); + emit Poke(ilk, val, spot); + } + + function cage() external note auth { + live = 0; + } +} diff --git a/certora/harness/dss/Vat.sol b/certora/harness/dss/Vat.sol new file mode 100644 index 00000000..b3f9cbd2 --- /dev/null +++ b/certora/harness/dss/Vat.sol @@ -0,0 +1,270 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +/// vat.sol -- Dai CDP database + +// Copyright (C) 2018 Rain +// +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. +// +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. +// +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . + +pragma solidity >=0.5.12; + +contract Vat { + // --- Auth --- + mapping (address => uint) public wards; + function rely(address usr) external note auth { require(live == 1, "Vat/not-live"); wards[usr] = 1; } + function deny(address usr) external note auth { require(live == 1, "Vat/not-live"); wards[usr] = 0; } + modifier auth { + require(wards[msg.sender] == 1, "Vat/not-authorized"); + _; + } + + mapping(address => mapping (address => uint)) public can; + function hope(address usr) external note { can[msg.sender][usr] = 1; } + function nope(address usr) external note { can[msg.sender][usr] = 0; } + function wish(address bit, address usr) internal view returns (bool) { + return either(bit == usr, can[bit][usr] == 1); + } + + // --- Data --- + struct Ilk { + uint256 Art; // Total Normalised Debt [wad] + uint256 rate; // Accumulated Rates [ray] + uint256 spot; // Price with Safety Margin [ray] + uint256 line; // Debt Ceiling [rad] + uint256 dust; // Urn Debt Floor [rad] + } + struct Urn { + uint256 ink; // Locked Collateral [wad] + uint256 art; // Normalised Debt [wad] + } + + mapping (bytes32 => Ilk) public ilks; + mapping (bytes32 => mapping (address => Urn )) public urns; + mapping (bytes32 => mapping (address => uint)) public gem; // [wad] + mapping (address => uint256) public dai; // [rad] + mapping (address => uint256) public sin; // [rad] + + uint256 public debt; // Total Dai Issued [rad] + uint256 public vice; // Total Unbacked Dai [rad] + uint256 public Line; // Total Debt Ceiling [rad] + uint256 public live; // Active Flag + + // --- Logs --- + event LogNote( + bytes4 indexed sig, + bytes32 indexed arg1, + bytes32 indexed arg2, + bytes32 indexed arg3, + bytes data + ) anonymous; + + modifier note { + _; + assembly { + // log an 'anonymous' event with a constant 6 words of calldata + // and four indexed topics: the selector and the first three args + let mark := msize() // end of memory ensures zero + mstore(0x40, add(mark, 288)) // update free memory pointer + mstore(mark, 0x20) // bytes type data offset + mstore(add(mark, 0x20), 224) // bytes size (padded) + calldatacopy(add(mark, 0x40), 0, 224) // bytes payload + log4(mark, 288, // calldata + shl(224, shr(224, calldataload(0))), // msg.sig + calldataload(4), // arg1 + calldataload(36), // arg2 + calldataload(68) // arg3 + ) + } + } + + // --- Init --- + constructor() public { + wards[msg.sender] = 1; + live = 1; + } + + // --- Math --- + function add(uint x, int y) internal pure returns (uint z) { + z = x + uint(y); + require(y >= 0 || z <= x); + require(y <= 0 || z >= x); + } + function sub(uint x, int y) internal pure returns (uint z) { + z = x - uint(y); + require(y <= 0 || z <= x); + require(y >= 0 || z >= x); + } + function mul(uint x, int y) internal pure returns (int z) { + z = int(x) * y; + require(int(x) >= 0); + require(y == 0 || z / y == int(x)); + } + function add(uint x, uint y) internal pure returns (uint z) { + require((z = x + y) >= x); + } + function sub(uint x, uint y) internal pure returns (uint z) { + require((z = x - y) <= x); + } + function mul(uint x, uint y) internal pure returns (uint z) { + require(y == 0 || (z = x * y) / y == x); + } + + // --- Administration --- + function init(bytes32 ilk) external note auth { + require(ilks[ilk].rate == 0, "Vat/ilk-already-init"); + ilks[ilk].rate = 10 ** 27; + } + function file(bytes32 what, uint data) external note auth { + require(live == 1, "Vat/not-live"); + if (what == "Line") Line = data; + else revert("Vat/file-unrecognized-param"); + } + function file(bytes32 ilk, bytes32 what, uint data) external note auth { + require(live == 1, "Vat/not-live"); + if (what == "spot") ilks[ilk].spot = data; + else if (what == "line") ilks[ilk].line = data; + else if (what == "dust") ilks[ilk].dust = data; + else revert("Vat/file-unrecognized-param"); + } + function cage() external note auth { + live = 0; + } + + // --- Fungibility --- + function slip(bytes32 ilk, address usr, int256 wad) external note auth { + gem[ilk][usr] = add(gem[ilk][usr], wad); + } + function flux(bytes32 ilk, address src, address dst, uint256 wad) external note { + require(wish(src, msg.sender), "Vat/not-allowed"); + gem[ilk][src] = sub(gem[ilk][src], wad); + gem[ilk][dst] = add(gem[ilk][dst], wad); + } + function move(address src, address dst, uint256 rad) external note { + require(wish(src, msg.sender), "Vat/not-allowed"); + dai[src] = sub(dai[src], rad); + dai[dst] = add(dai[dst], rad); + } + + function either(bool x, bool y) internal pure returns (bool z) { + assembly{ z := or(x, y)} + } + function both(bool x, bool y) internal pure returns (bool z) { + assembly{ z := and(x, y)} + } + + // --- CDP Manipulation --- + function frob(bytes32 i, address u, address v, address w, int dink, int dart) external note { + // system is live + require(live == 1, "Vat/not-live"); + + Urn memory urn = urns[i][u]; + Ilk memory ilk = ilks[i]; + // ilk has been initialised + require(ilk.rate != 0, "Vat/ilk-not-init"); + + urn.ink = add(urn.ink, dink); + urn.art = add(urn.art, dart); + ilk.Art = add(ilk.Art, dart); + + int dtab = mul(ilk.rate, dart); + uint tab = mul(ilk.rate, urn.art); + debt = add(debt, dtab); + + // either debt has decreased, or debt ceilings are not exceeded + require(either(dart <= 0, both(mul(ilk.Art, ilk.rate) <= ilk.line, debt <= Line)), "Vat/ceiling-exceeded"); + // urn is either less risky than before, or it is safe + require(either(both(dart <= 0, dink >= 0), tab <= mul(urn.ink, ilk.spot)), "Vat/not-safe"); + + // urn is either more safe, or the owner consents + require(either(both(dart <= 0, dink >= 0), wish(u, msg.sender)), "Vat/not-allowed-u"); + // collateral src consents + require(either(dink <= 0, wish(v, msg.sender)), "Vat/not-allowed-v"); + // debt dst consents + require(either(dart >= 0, wish(w, msg.sender)), "Vat/not-allowed-w"); + + // urn has no debt, or a non-dusty amount + require(either(urn.art == 0, tab >= ilk.dust), "Vat/dust"); + + gem[i][v] = sub(gem[i][v], dink); + dai[w] = add(dai[w], dtab); + + urns[i][u] = urn; + ilks[i] = ilk; + } + // --- CDP Fungibility --- + function fork(bytes32 ilk, address src, address dst, int dink, int dart) external note { + Urn storage u = urns[ilk][src]; + Urn storage v = urns[ilk][dst]; + Ilk storage i = ilks[ilk]; + + u.ink = sub(u.ink, dink); + u.art = sub(u.art, dart); + v.ink = add(v.ink, dink); + v.art = add(v.art, dart); + + uint utab = mul(u.art, i.rate); + uint vtab = mul(v.art, i.rate); + + // both sides consent + require(both(wish(src, msg.sender), wish(dst, msg.sender)), "Vat/not-allowed"); + + // both sides safe + require(utab <= mul(u.ink, i.spot), "Vat/not-safe-src"); + require(vtab <= mul(v.ink, i.spot), "Vat/not-safe-dst"); + + // both sides non-dusty + require(either(utab >= i.dust, u.art == 0), "Vat/dust-src"); + require(either(vtab >= i.dust, v.art == 0), "Vat/dust-dst"); + } + // --- CDP Confiscation --- + function grab(bytes32 i, address u, address v, address w, int dink, int dart) external note auth { + Urn storage urn = urns[i][u]; + Ilk storage ilk = ilks[i]; + + urn.ink = add(urn.ink, dink); + urn.art = add(urn.art, dart); + ilk.Art = add(ilk.Art, dart); + + int dtab = mul(ilk.rate, dart); + + gem[i][v] = sub(gem[i][v], dink); + sin[w] = sub(sin[w], dtab); + vice = sub(vice, dtab); + } + + // --- Settlement --- + function heal(uint rad) external note { + address u = msg.sender; + sin[u] = sub(sin[u], rad); + dai[u] = sub(dai[u], rad); + vice = sub(vice, rad); + debt = sub(debt, rad); + } + function suck(address u, address v, uint rad) external note auth { + sin[u] = add(sin[u], rad); + dai[v] = add(dai[v], rad); + vice = add(vice, rad); + debt = add(debt, rad); + } + + // --- Rates --- + function fold(bytes32 i, address u, int rate) external note auth { + require(live == 1, "Vat/not-live"); + Ilk storage ilk = ilks[i]; + ilk.rate = add(ilk.rate, rate); + int rad = mul(ilk.Art, rate); + dai[u] = add(dai[u], rad); + debt = add(debt, rad); + } +} diff --git a/certora/harness/tokens/MkrMock.sol b/certora/harness/tokens/MkrMock.sol new file mode 100644 index 00000000..aba48514 --- /dev/null +++ b/certora/harness/tokens/MkrMock.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import {GemMock} from "../../../test/mocks/GemMock.sol"; + +contract MkrMock is GemMock { + + constructor(uint256 initialSupply) GemMock(initialSupply) { + } +} diff --git a/certora/harness/tokens/RewardsMock.sol b/certora/harness/tokens/RewardsMock.sol new file mode 100644 index 00000000..0e8e582b --- /dev/null +++ b/certora/harness/tokens/RewardsMock.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import {GemMock} from "../../../test/mocks/GemMock.sol"; + +contract RewardsMock is GemMock { + + constructor(uint256 initialSupply) GemMock(initialSupply) { + } +} diff --git a/certora/harness/tokens/SkyMock.sol b/certora/harness/tokens/SkyMock.sol new file mode 100644 index 00000000..7ea9079b --- /dev/null +++ b/certora/harness/tokens/SkyMock.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import {GemMock} from "../../../test/mocks/GemMock.sol"; + +contract SkyMock is GemMock { + + constructor(uint256 initialSupply) GemMock(initialSupply) { + } +}