From ebcd47d93553dfce2869fd832d6fd1379eefb540 Mon Sep 17 00:00:00 2001 From: Sam MacPherson Date: Fri, 12 May 2023 20:32:10 +0100 Subject: [PATCH] Certora CVL2 port (#111) * CVL2 port * fixing specs for port * remove art v assets compare * revert assetsAfter spec * change tranfer to exit * re-add require that was previously deleted * remove unused line * Fix requires and missing asserts (#113) * Remove not necessary constraints (#114) * re-add struct link --------- Co-authored-by: Shelly Grossman Co-authored-by: sunbreak1211 <129470872+sunbreak1211@users.noreply.github.com> --- .github/workflows/certora.yml | 2 +- Makefile | 2 +- certora/D3MHub.spec | 1341 +++++++++++++++------------------ 3 files changed, 629 insertions(+), 716 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 30202fa8..780ce205 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -48,7 +48,7 @@ jobs: run: solc-select install 0.8.14 - name: Install Certora - run: pip3 install certora-cli + run: pip3 install certora-cli-beta - name: Certora ${{ matrix.name }} run: make certora-hub short=1 rule="${{ matrix.rules }}" diff --git a/Makefile b/Makefile index 583770d1..532060d4 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ all :; FOUNDRY_OPTIMIZER=true FOUNDRY_OPTIMIZER_RUNS=200 forge build --use solc:0.8.14 clean :; forge clean -certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,TokenMock=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,TokenMock=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol certora/d3m/D3MTestPlan.sol certora/d3m/D3MTestPool.sol src/tests/mocks/TokenMock.sol --link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=TokenMock --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=1200,-solver=z3,-adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,) +certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,TokenMock=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,TokenMock=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol certora/d3m/D3MTestPlan.sol certora/d3m/D3MTestPool.sol src/tests/mocks/TokenMock.sol --link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=TokenMock --structLink D3MHub:pool=D3MTestPool D3MHub:plan=D3MTestPlan --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=1200,-solver=z3,-adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,) deploy :; ./deploy.sh config="$(config)" deploy-core :; ./deploy-core.sh diff --git a/certora/D3MHub.spec b/certora/D3MHub.spec index 23234f5f..e6121286 100644 --- a/certora/D3MHub.spec +++ b/certora/D3MHub.spec @@ -1,76 +1,61 @@ // D3MHub.spec -using Vat as vat -using Dai as dai -using DaiJoin as daiJoin -using End as end -using D3MTestPool as pool -using D3MTestPlan as plan -using TokenMock as share +using Vat as vat; +using Dai as dai; +using DaiJoin as daiJoin; +using End as end; +using D3MTestPool as pool; +using D3MTestPlan as plan; +using TokenMock as share; methods { - vat() returns (address) envfree - daiJoin() returns (address) envfree - vow() returns (address) envfree - end() returns (address) envfree - ilks(bytes32) returns (address, address, uint256, uint256, uint256) envfree - locked() returns (uint256) envfree - plan(bytes32) returns (address) envfree => DISPATCHER(true) - pool(bytes32) returns (address) envfree => DISPATCHER(true) - tic(bytes32) returns (uint256) envfree - tau(bytes32) returns (uint256) envfree - culled(bytes32) returns (uint256) envfree - wards(address) returns (uint256) envfree - vat.can(address, address) returns (uint256) envfree - vat.debt() returns (uint256) envfree - vat.dai(address) returns (uint256) envfree - vat.gem(bytes32, address) returns (uint256) envfree - vat.Line() returns (uint256) envfree - vat.live() returns (uint256) envfree - vat.ilks(bytes32) returns (uint256, uint256, uint256, uint256, uint256) envfree - vat.sin(address) returns (uint256) envfree - vat.urns(bytes32, address) returns (uint256, uint256) envfree - vat.vice() returns (uint256) envfree - vat.wards(address) returns (uint256) envfree - dai.allowance(address, address) returns (uint256) envfree - dai.balanceOf(address) returns (uint256) envfree - dai.totalSupply() returns (uint256) envfree - dai.wards(address) returns (uint256) envfree - daiJoin.dai() returns (address) envfree - daiJoin.live() returns (uint256) envfree - daiJoin.vat() returns (address) envfree - end.debt() returns (uint256) envfree - end.gap(bytes32) returns (uint256) envfree - end.tag(bytes32) returns (uint256) envfree - end.vat() returns (address) envfree - end.vow() returns (address) envfree - plan.dai() returns (address) envfree - pool.hub() returns (address) envfree - pool.vat() returns (address) envfree - pool.dai() returns (address) envfree - pool.share() returns (address) envfree - share.balanceOf(address) returns (uint256) envfree - share.totalSupply() returns (uint256) envfree - share.wards(address) returns (uint256) envfree - debt() returns (uint256) => DISPATCHER(true) - skim(bytes32, address) => DISPATCHER(true) - active() returns (bool) => DISPATCHER(true) - getTargetAssets(uint256) returns (uint256) => DISPATCHER(true) - assetBalance() returns (uint256) => DISPATCHER(true) - maxDeposit() returns (uint256) => DISPATCHER(true) - maxWithdraw() returns (uint256) => DISPATCHER(true) - deposit(uint256) => DISPATCHER(true) - withdraw(uint256) => DISPATCHER(true) - preDebtChange() => DISPATCHER(true) - postDebtChange() => DISPATCHER(true) - exit(address, uint256) => DISPATCHER(true) - balanceOf(address) returns (uint256) => DISPATCHER(true) - burn(address, uint256) => DISPATCHER(true) - mint(address, uint256) => DISPATCHER(true) + function vat() external returns (address) envfree; + function daiJoin() external returns (address) envfree; + function vow() external returns (address) envfree; + function end() external returns (address) envfree; + function ilks(bytes32) external returns (address, address, uint256, uint256, uint256) envfree; + function locked() external returns (uint256) envfree; + function plan(bytes32) external returns (address) envfree; + function pool(bytes32) external returns (address) envfree; + function tic(bytes32) external returns (uint256) envfree; + function tau(bytes32) external returns (uint256) envfree; + function culled(bytes32) external returns (uint256) envfree; + function wards(address) external returns (uint256) envfree; + function vat.can(address, address) external returns (uint256) envfree; + function vat.debt() external returns (uint256) envfree; + function vat.dai(address) external returns (uint256) envfree; + function vat.gem(bytes32, address) external returns (uint256) envfree; + function vat.Line() external returns (uint256) envfree; + function vat.live() external returns (uint256) envfree; + function vat.ilks(bytes32) external returns (uint256, uint256, uint256, uint256, uint256) envfree; + function vat.sin(address) external returns (uint256) envfree; + function vat.urns(bytes32, address) external returns (uint256, uint256) envfree; + function vat.vice() external returns (uint256) envfree; + function vat.wards(address) external returns (uint256) envfree; + function dai.allowance(address, address) external returns (uint256) envfree; + function dai.balanceOf(address) external returns (uint256) envfree; + function dai.totalSupply() external returns (uint256) envfree; + function dai.wards(address) external returns (uint256) envfree; + function daiJoin.dai() external returns (address) envfree; + function daiJoin.live() external returns (uint256) envfree; + function daiJoin.vat() external returns (address) envfree; + function end.debt() external returns (uint256) envfree; + function end.gap(bytes32) external returns (uint256) envfree; + function end.tag(bytes32) external returns (uint256) envfree; + function end.vat() external returns (address) envfree; + function end.vow() external returns (address) envfree; + function plan.dai() external returns (address) envfree; + function pool.hub() external returns (address) envfree; + function pool.vat() external returns (address) envfree; + function pool.dai() external returns (address) envfree; + function pool.share() external returns (address) envfree; + function share.balanceOf(address) external returns (uint256) envfree; + function share.totalSupply() external returns (uint256) envfree; + function share.wards(address) external returns (uint256) envfree; } -definition WAD() returns uint256 = 10^18; -definition RAY() returns uint256 = 10^27; +definition WAD() returns mathint = 10^18; +definition RAY() returns mathint = 10^27; definition min_int256() returns mathint = -1 * 2^255; definition max_int256() returns mathint = 2^255 - 1; @@ -85,13 +70,13 @@ rule rely(address usr) { env e; address other; - require(other != usr); + require other != usr; uint256 wardOther = wards(other); rely(e, usr); - assert(wards(usr) == 1, "rely did not set the wards as expected"); - assert(wards(other) == wardOther, "rely affected other wards which wasn't expected"); + assert wards(usr) == 1, "rely did not set the wards as expected"; + assert wards(other) == wardOther, "rely affected other wards which wasn't expected"; } rule rely_revert(address usr) { @@ -104,23 +89,23 @@ rule rely_revert(address usr) { bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; - assert(lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"); + assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"; } rule deny(address usr) { env e; address other; - require(other != usr); + require other != usr; uint256 wardOther = wards(other); deny(e, usr); - assert(wards(usr) == 0, "deny did not set the wards as expected"); - assert(wards(other) == wardOther, "deny affected other wards which wasn't expected"); + assert wards(usr) == 0, "deny did not set the wards as expected"; + assert wards(other) == wardOther, "deny affected other wards which wasn't expected"; } rule deny_revert(address usr) { @@ -133,10 +118,10 @@ rule deny_revert(address usr) { bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; - assert(lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"); + assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"; } rule file_ilk_uint256(bytes32 ilk, bytes32 what, uint256 data) { @@ -144,7 +129,7 @@ rule file_ilk_uint256(bytes32 ilk, bytes32 what, uint256 data) { file(e, ilk, what, data); - assert(tau(ilk) == data, "file did not set tau as expected"); + assert tau(ilk) == data, "file did not set tau as expected"; } rule file_ilk_uint256_revert(bytes32 ilk, bytes32 what, uint256 data) { @@ -156,13 +141,13 @@ rule file_ilk_uint256_revert(bytes32 ilk, bytes32 what, uint256 data) { bool revert1 = e.msg.value > 0; bool revert2 = ward != 1; - bool revert3 = what != 0x7461750000000000000000000000000000000000000000000000000000000000; + bool revert3 = what != to_bytes32(0x7461750000000000000000000000000000000000000000000000000000000000); - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; - assert(lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases"); + assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases"; } rule file_ilk_address(bytes32 ilk, bytes32 what, address data) { @@ -170,8 +155,8 @@ rule file_ilk_address(bytes32 ilk, bytes32 what, address data) { file(e, ilk, what, data); - assert(what == 0x706f6f6c00000000000000000000000000000000000000000000000000000000 => pool(ilk) == data, "file did not set pool as expected"); - assert(what == 0x706c616e00000000000000000000000000000000000000000000000000000000 => plan(ilk) == data, "file did not set plan as expected"); + assert what == to_bytes32(0x706f6f6c00000000000000000000000000000000000000000000000000000000) => pool(ilk) == data, "file did not set pool as expected"; + assert what == to_bytes32(0x706c616e00000000000000000000000000000000000000000000000000000000) => plan(ilk) == data, "file did not set plan as expected"; } rule file_ilk_address_revert(bytes32 ilk, bytes32 what, address data) { @@ -187,27 +172,27 @@ rule file_ilk_address_revert(bytes32 ilk, bytes32 what, address data) { bool revert2 = ward != 1; bool revert3 = vatLive != 1; bool revert4 = tic != 0; - bool revert5 = what != 0x706f6f6c00000000000000000000000000000000000000000000000000000000 && what != 0x706c616e00000000000000000000000000000000000000000000000000000000; + bool revert5 = what != to_bytes32(0x706f6f6c00000000000000000000000000000000000000000000000000000000) && what != to_bytes32(0x706c616e00000000000000000000000000000000000000000000000000000000); - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; - assert(lastReverted => revert1 || revert2 || revert3 || - revert4 || revert5, "Revert rules are not covering all the cases"); + assert lastReverted => revert1 || revert2 || revert3 || + revert4 || revert5, "Revert rules are not covering all the cases"; } rule ilk_getters() { bytes32 ilk; address pool_; address plan_; uint256 tau; uint256 culled; uint256 tic; pool_, plan_, tau, culled, tic = ilks(ilk); - assert(pool_ == pool(ilk), "pool getter did not return ilk.pool"); - assert(plan_ == plan(ilk), "plan getter did not return ilk.plan"); - assert(tau == tau(ilk), "tau getter did not return ilk.tau"); - assert(culled == culled(ilk), "culled getter did not return ilk.culled"); - assert(tic == tic(ilk), "tic getter did not return ilk.tic"); + assert pool_ == pool(ilk), "pool getter did not return ilk.pool"; + assert plan_ == plan(ilk), "plan getter did not return ilk.plan"; + assert tau == tau(ilk), "tau getter did not return ilk.tau"; + assert culled == culled(ilk), "culled getter did not return ilk.culled"; + assert tic == tic(ilk), "tic getter did not return ilk.tic"; } rule exec_normal(bytes32 ilk) { @@ -215,62 +200,54 @@ rule exec_normal(bytes32 ilk) { address vow = vow(); - require(vat() == vat); - require(daiJoin() == daiJoin); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(vow != daiJoin); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); + require plan(ilk) == plan; + require pool(ilk) == pool; + require vow != daiJoin; - uint256 tic = tic(ilk); - uint256 culled = culled(ilk); - - uint256 LineBefore = vat.Line(); - uint256 debtBefore = vat.debt(); - uint256 ArtBefore; - uint256 rateBefore; - uint256 spotBefore; - uint256 lineBefore; - uint256 dustBefore; + mathint tic = tic(ilk); + mathint culled = culled(ilk); + + mathint LineBefore = vat.Line(); + mathint debtBefore = vat.debt(); + mathint ArtBefore; + mathint rateBefore; + mathint spotBefore; + mathint lineBefore; + mathint dustBefore; ArtBefore, rateBefore, spotBefore, lineBefore, dustBefore = vat.ilks(ilk); - uint256 inkBefore; - uint256 artBefore; + mathint inkBefore; + mathint artBefore; inkBefore, artBefore = vat.urns(ilk, pool); bool active = plan.active(e); - uint256 maxDeposit = pool.maxDeposit(e); + mathint maxDeposit = pool.maxDeposit(e); mathint maxWithdraw = min(to_mathint(pool.maxWithdraw(e)), safe_max()); - uint256 assetsBefore = pool.assetBalance(e); - uint256 targetAssets = plan.getTargetAssets(e, assetsBefore); - uint256 vatDaiVowBefore = vat.dai(vow); + mathint assetsBefore = pool.assetBalance(e); + mathint targetAssets = plan.getTargetAssets(e, assert_uint256(assetsBefore)); + mathint vatDaiVowBefore = vat.dai(vow); - require(vat.live() == 1); - require(culled == 0); + require vat.live() == 1; + require culled == 0; exec(e, ilk); - uint256 LineAfter = vat.Line(); - uint256 debtAfter = vat.debt(); - uint256 ArtAfter; - uint256 rateAfter; - uint256 spotAfter; - uint256 lineAfter; - uint256 dustAfter; + mathint LineAfter = vat.Line(); + mathint debtAfter = vat.debt(); + mathint ArtAfter; + mathint rateAfter; + mathint spotAfter; + mathint lineAfter; + mathint dustAfter; ArtAfter, rateAfter, spotAfter, lineAfter, dustAfter = vat.ilks(ilk); - uint256 inkAfter; - uint256 artAfter; + mathint inkAfter; + mathint artAfter; inkAfter, artAfter = vat.urns(ilk, pool); - uint256 assetsAfter = pool.assetBalance(e); - uint256 vatDaiVowAfter = vat.dai(vow); + mathint assetsAfter = pool.assetBalance(e); + mathint vatDaiVowAfter = vat.dai(vow); - uint256 lineWad = lineBefore / RAY(); - uint256 underLine = inkBefore < lineWad ? lineWad - inkBefore : 0; + mathint lineWad = lineBefore / RAY(); + mathint underLine = inkBefore < lineWad ? lineWad - inkBefore : 0; mathint fixInk = assetsBefore > inkBefore ? min( min( @@ -284,15 +261,15 @@ rule exec_normal(bytes32 ilk) { mathint debtMiddle = debtBefore + fixArt * RAY(); // General asserts - assert(LineAfter == LineBefore, "Line should not change"); - assert(lineAfter == lineBefore, "line should not change"); - assert(artAfter == ArtAfter, "art should be same than Art"); - assert(inkAfter == artAfter, "ink and art should end up being the same"); - assert(inkAfter <= lineWad || inkAfter <= inkBefore, "ink can not overpass debt ceiling or be higher than prev one"); - assert(inkAfter <= safe_max(), "ink can not overpass max_int256 / RAY"); - assert(vatDaiVowAfter == vatDaiVowBefore + fixArt * RAY(), "vatDaiVow did not increase as expected"); + assert LineAfter == LineBefore, "Line should not change"; + assert lineAfter == lineBefore, "line should not change"; + assert artAfter == ArtAfter, "art should be same than Art"; + assert inkAfter == artAfter, "ink and art should end up being the same"; + assert inkAfter <= lineWad || inkAfter <= inkBefore, "ink can not overpass debt ceiling or be higher than prev one"; + assert inkAfter <= safe_max(), "ink can not overpass max_int256 / RAY"; + assert vatDaiVowAfter == vatDaiVowBefore + fixArt * RAY(), "vatDaiVow did not increase as expected"; // Winding to targetAssets - assert( + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) maxDeposit >= targetAssets - assetsBefore && // target IS NOT restricted by maxDeposit @@ -301,8 +278,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == targetAssets && assetsAfter == artAfter, "wind: error 1" - ); - assert( + ; + assert tic == 0 && active && inkBefore > assetsBefore && inkBefore - assetsBefore <= WAD() && // regular path in normal path but assets right below ink targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) maxDeposit >= targetAssets - assetsBefore && // target IS NOT restricted by maxDeposit @@ -311,9 +288,9 @@ rule exec_normal(bytes32 ilk) { => artAfter == targetAssets + (inkBefore - assetsBefore) && assetsAfter == targetAssets, "wind: error 2" - ); + ; // Winding to ilk line - assert( + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) maxDeposit >= targetAssets - assetsBefore && // target IS NOT restricted by maxDeposit @@ -323,8 +300,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == lineWad && assetsAfter >= artAfter, "wind: error 3" - ); - assert( + ; + assert tic == 0 && active && inkBefore > assetsBefore && inkBefore - assetsBefore <= WAD() && // regular path in normal path but assets right below ink targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) maxDeposit >= targetAssets - assetsBefore && // target IS NOT restricted by maxDeposit @@ -334,8 +311,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == lineWad && assetsAfter == artAfter - (inkBefore - assetsBefore), "wind: error 4" - ); - assert( + ; + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) maxDeposit >= targetAssets - assetsBefore && // target IS NOT restricted by maxDeposit @@ -346,9 +323,9 @@ rule exec_normal(bytes32 ilk) { => artAfter == lineWad && assetsAfter == artAfter, "wind: error 5" - ); + ; // Unwinding to targetAssets - assert( + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets <= assetsBefore && // plan determines we need to go down (or keep the same) targetAssets <= lineWad && // target IS NOT restricted by ilk line @@ -358,8 +335,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == targetAssets && assetsAfter == artAfter, "unwind: error 1" - ); - assert( + ; + assert tic == 0 && active && inkBefore > assetsBefore && inkBefore - assetsBefore <= WAD() && // regular path in normal path but assets right below ink targetAssets <= assetsBefore && // plan determines we need to go down (or keep the same) targetAssets + (inkBefore - assetsBefore) <= lineWad && // target IS NOT restricted by ilk line @@ -369,9 +346,9 @@ rule exec_normal(bytes32 ilk) { => artAfter == targetAssets + (inkBefore - assetsBefore) && assetsAfter == targetAssets, "unwind: error 2" - ); + ; // Unwinding due to targetAssets but restricted - assert( + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets <= assetsBefore && // plan determines we need to go down (or keep the same) targetAssets <= lineWad && // target IS NOT restricted by ilk line @@ -381,8 +358,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == assetsBefore - maxWithdraw && assetsAfter == artAfter, "unwind: error 3" - ); - assert( + ; + assert tic == 0 && active && inkBefore > assetsBefore && inkBefore - assetsBefore <= WAD() && // regular path in normal path but assets right below ink targetAssets <= assetsBefore && // plan determines we need to go down (or keep the same) targetAssets <= lineWad && // target IS NOT restricted by ilk line @@ -392,8 +369,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == assetsAfter + (inkBefore - assetsBefore) && assetsAfter == assetsBefore - maxWithdraw, "unwind: error 4" - ); - assert( + ; + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets <= assetsBefore && // plan determines we need to go down (or keep the same) targetAssets <= lineWad && // target IS NOT restricted by ilk line @@ -404,9 +381,9 @@ rule exec_normal(bytes32 ilk) { assetsBefore - inkBefore > maxWithdraw => artAfter == inkBefore, "unwind: error 5" - ); + ; // Unwinding due to line - assert( + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) targetAssets > lineWad && // target IS restricted by ilk line @@ -417,8 +394,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == lineWad && assetsAfter == artAfter, "unwind: error 6" - ); - assert( + ; + assert tic == 0 && active && inkBefore > assetsBefore && inkBefore - assetsBefore <= WAD() && // regular path in normal path but assets right below ink targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) targetAssets + (inkBefore - assetsBefore) > lineWad && // target IS restricted by ilk line @@ -429,8 +406,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == lineWad && assetsAfter == artAfter - (inkBefore - assetsBefore), "unwind: error 7" - ); - assert( + ; + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) targetAssets > lineWad && // target IS restricted by ilk line @@ -441,8 +418,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == inkBefore && assetsAfter > artAfter, "unwind: error 8" - ); - assert( + ; + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) targetAssets > lineWad && // target IS restricted by ilk line @@ -452,8 +429,8 @@ rule exec_normal(bytes32 ilk) { => artAfter == inkBefore + fixInk - maxWithdraw && assetsAfter >= artAfter, "unwind: error 9" - ); - assert( + ; + assert tic == 0 && active && assetsBefore >= inkBefore && // regular path in normal path targetAssets >= assetsBefore && // plan determines we need to go up (or keep the same) targetAssets > lineWad && // target IS restricted by ilk line @@ -467,39 +444,39 @@ rule exec_normal(bytes32 ilk) { artAfter >= lineWad && assetsAfter == artAfter, "unwind: error 10" - ); + ; // Force unwinding due to ilk caged (but not culled yet) or plan inactive or assets being missing: - assert( + assert (tic > 0 || !active || assetsBefore + WAD() < inkBefore) && assetsBefore <= safe_max() && // full unwinding is NOT restricted by safe maxint256 wad assetsBefore >= inkBefore && assetsBefore <= maxWithdraw => artAfter == 0, "unwind: error 11" - ); - assert( + ; + assert (tic > 0 || !active || assetsBefore + WAD() < inkBefore) && assetsBefore <= safe_max() && // full unwinding is NOT restricted by safe maxint256 wad assetsBefore >= inkBefore && assetsBefore > maxWithdraw && assetsBefore - maxWithdraw < lineWad => artAfter == assetsBefore - maxWithdraw, "unwind: error 12" - ); - assert( + ; + assert (tic > 0 || !active || assetsBefore + WAD() < inkBefore) && assetsBefore <= safe_max() && // full unwinding is NOT restricted by safe maxint256 wad assetsBefore > maxWithdraw && assetsBefore - maxWithdraw >= lineWad && inkBefore <= lineWad => artAfter == lineWad, "unwind: error 13" - ); - assert( + ; + assert (tic > 0 || !active || assetsBefore + WAD() < inkBefore) && assetsBefore <= safe_max() && // full unwinding is NOT restricted by safe maxint256 wad assetsBefore > maxWithdraw && assetsBefore - maxWithdraw >= inkBefore && inkBefore > lineWad => artAfter == inkBefore, "unwind: error 14" - ); + ; } rule exec_normal_revert(bytes32 ilk) { @@ -507,43 +484,35 @@ rule exec_normal_revert(bytes32 ilk) { address vow = vow(); - require(vat() == vat); - require(daiJoin() == daiJoin); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(vow != currentContract); - require(vow != daiJoin); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); - - uint256 locked = locked(); - uint256 Line = vat.Line(); - uint256 Art; - uint256 rate; - uint256 spot; - uint256 line; - uint256 dust; + require plan(ilk) == plan; + require pool(ilk) == pool; + require vow != currentContract; + require vow != daiJoin; + + mathint locked = locked(); + mathint Line = vat.Line(); + mathint Art; + mathint rate; + mathint spot; + mathint line; + mathint dust; Art, rate, spot, line, dust = vat.ilks(ilk); - uint256 ink; - uint256 art; + mathint ink; + mathint art; ink, art = vat.urns(ilk, pool); - uint256 assets = pool.assetBalance(e); + mathint assets = pool.assetBalance(e); - require(vat.live() == 1); - require(culled(ilk) == 0); - require(dust == 0); - require(dai.wards(daiJoin) == 1); - require(share.wards(pool) == 1); + require vat.live() == 1; + require culled(ilk) == 0; + require dust == 0; + require dai.wards(daiJoin) == 1; + require share.wards(pool) == 1; mathint maxWithdraw = min(to_mathint(pool.maxWithdraw(e)), safe_max()); - uint256 maxDeposit = pool.maxDeposit(e); - uint256 lineWad = line / RAY(); - uint256 debt = vat.debt(); - uint256 underLine = ink < lineWad ? lineWad - ink : 0; + mathint maxDeposit = pool.maxDeposit(e); + mathint lineWad = line / RAY(); + mathint debt = vat.debt(); + mathint underLine = ink < lineWad ? lineWad - ink : 0; mathint fixInk = assets > ink ? min( min( @@ -558,10 +527,10 @@ rule exec_normal_revert(bytes32 ilk) { mathint artFixed = art + fixArt; mathint debtMiddle = debt + fixArt * RAY(); - uint256 tic = tic(ilk); + mathint tic = tic(ilk); bool active = plan.active(e); - uint256 targetAssets = plan.getTargetAssets(e, assets); + mathint targetAssets = plan.getTargetAssets(e, assert_uint256(assets)); mathint toUnwindAux = max( max( @@ -588,29 +557,29 @@ rule exec_normal_revert(bytes32 ilk) { ) : 0; - uint256 vatGemPool = vat.gem(ilk, pool); - require(ink == 0 || vatGemPool == 0); // To ensure correct behavior - uint256 vatWardHub = vat.wards(currentContract); - uint256 shareBalPool = share.balanceOf(pool); - uint256 shareSupply = share.totalSupply(); - require(shareSupply >= shareBalPool); // To ensure correct behaviour - uint256 daiBalShare = dai.balanceOf(share); - uint256 daiBalPool = dai.balanceOf(pool); - uint256 daiSupply = dai.totalSupply(); - require(daiSupply >= daiBalShare + daiBalPool); // To ensure correct behaviour - uint256 daiAllowanceSharePool = dai.allowance(share, pool); - uint256 daiBalHub = dai.balanceOf(currentContract); - uint256 vatDaiDaiJoin = vat.dai(daiJoin); - uint256 vatDaiHub = vat.dai(currentContract); - uint256 daiAllowanceHubDaiJoin = dai.allowance(currentContract, daiJoin); - uint256 vatSinVow = vat.sin(vow); - uint256 vatDaiVow = vat.dai(vow); - uint256 vatVice = vat.vice(); - uint256 vatDebt = vat.debt(); - require(vatDebt >= art * rate); // To ensure correct behaviour - uint256 vatCanPoolHub = vat.can(pool, currentContract); - uint256 vatCanHubDaiJoin = vat.can(currentContract, daiJoin); - uint256 daiJoinLive = daiJoin.live(); + mathint vatGemPool = vat.gem(ilk, pool); + require ink == 0 || vatGemPool == 0; // To ensure correct behaviour + mathint vatWardHub = vat.wards(currentContract); + mathint shareBalPool = share.balanceOf(pool); + mathint shareSupply = share.totalSupply(); + require shareSupply >= shareBalPool; // To ensure correct behaviour + mathint daiBalShare = dai.balanceOf(share); + mathint daiBalPool = dai.balanceOf(pool); + mathint daiSupply = dai.totalSupply(); + require daiSupply >= daiBalShare + daiBalPool; // To ensure correct behaviour + mathint daiAllowanceSharePool = dai.allowance(share, pool); + mathint daiBalHub = dai.balanceOf(currentContract); + mathint vatDaiDaiJoin = vat.dai(daiJoin); + mathint vatDaiHub = vat.dai(currentContract); + mathint daiAllowanceHubDaiJoin = dai.allowance(currentContract, daiJoin); + mathint vatSinVow = vat.sin(vow); + mathint vatDaiVow = vat.dai(vow); + mathint vatVice = vat.vice(); + mathint vatDebt = vat.debt(); + require vatDebt >= art * rate; // To ensure correct behaviour + mathint vatCanPoolHub = vat.can(pool, currentContract); + mathint vatCanHubDaiJoin = vat.can(currentContract, daiJoin); + mathint daiJoinLive = daiJoin.live(); exec@withrevert(e, ilk); @@ -666,46 +635,46 @@ rule exec_normal_revert(bytes32 ilk) { // pool.deposit: bool revert38 = toWind > 0 && shareSupply + toWind > max_uint256; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); - assert(revert6 => lastReverted, "revert6 failed"); - assert(revert7 => lastReverted, "revert7 failed"); - assert(revert8 => lastReverted, "revert8 failed"); - assert(revert9 => lastReverted, "revert9 failed"); - assert(revert10 => lastReverted, "revert10 failed"); - assert(revert11 => lastReverted, "revert11 failed"); - assert(revert12 => lastReverted, "revert12 failed"); - assert(revert13 => lastReverted, "revert13 failed"); - assert(revert14 => lastReverted, "revert14 failed"); - assert(revert15 => lastReverted, "revert15 failed"); - assert(revert16 => lastReverted, "revert16 failed"); - assert(revert17 => lastReverted, "revert17 failed"); - assert(revert18 => lastReverted, "revert18 failed"); - assert(revert19 => lastReverted, "revert19 failed"); - assert(revert20 => lastReverted, "revert20 failed"); - assert(revert21 => lastReverted, "revert21 failed"); - assert(revert22 => lastReverted, "revert22 failed"); - assert(revert23 => lastReverted, "revert23 failed"); - assert(revert24 => lastReverted, "revert24 failed"); - assert(revert25 => lastReverted, "revert25 failed"); - assert(revert26 => lastReverted, "revert26 failed"); - assert(revert27 => lastReverted, "revert27 failed"); - assert(revert28 => lastReverted, "revert28 failed"); - assert(revert29 => lastReverted, "revert29 failed"); - assert(revert30 => lastReverted, "revert30 failed"); - assert(revert31 => lastReverted, "revert31 failed"); - assert(revert32 => lastReverted, "revert32 failed"); - assert(revert33 => lastReverted, "revert33 failed"); - assert(revert34 => lastReverted, "revert34 failed"); - assert(revert35 => lastReverted, "revert35 failed"); - assert(revert36 => lastReverted, "revert36 failed"); - assert(revert37 => lastReverted, "revert37 failed"); - assert(revert38 => lastReverted, "revert38 failed"); - - assert(lastReverted => revert1 || revert2 || revert3 || + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; + assert revert6 => lastReverted, "revert6 failed"; + assert revert7 => lastReverted, "revert7 failed"; + assert revert8 => lastReverted, "revert8 failed"; + assert revert9 => lastReverted, "revert9 failed"; + assert revert10 => lastReverted, "revert10 failed"; + assert revert11 => lastReverted, "revert11 failed"; + assert revert12 => lastReverted, "revert12 failed"; + assert revert13 => lastReverted, "revert13 failed"; + assert revert14 => lastReverted, "revert14 failed"; + assert revert15 => lastReverted, "revert15 failed"; + assert revert16 => lastReverted, "revert16 failed"; + assert revert17 => lastReverted, "revert17 failed"; + assert revert18 => lastReverted, "revert18 failed"; + assert revert19 => lastReverted, "revert19 failed"; + assert revert20 => lastReverted, "revert20 failed"; + assert revert21 => lastReverted, "revert21 failed"; + assert revert22 => lastReverted, "revert22 failed"; + assert revert23 => lastReverted, "revert23 failed"; + assert revert24 => lastReverted, "revert24 failed"; + assert revert25 => lastReverted, "revert25 failed"; + assert revert26 => lastReverted, "revert26 failed"; + assert revert27 => lastReverted, "revert27 failed"; + assert revert28 => lastReverted, "revert28 failed"; + assert revert29 => lastReverted, "revert29 failed"; + assert revert30 => lastReverted, "revert30 failed"; + assert revert31 => lastReverted, "revert31 failed"; + assert revert32 => lastReverted, "revert32 failed"; + assert revert33 => lastReverted, "revert33 failed"; + assert revert34 => lastReverted, "revert34 failed"; + assert revert35 => lastReverted, "revert35 failed"; + assert revert36 => lastReverted, "revert36 failed"; + assert revert37 => lastReverted, "revert37 failed"; + assert revert38 => lastReverted, "revert38 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8 || revert9 || revert10 || revert11 || revert12 || @@ -717,7 +686,7 @@ rule exec_normal_revert(bytes32 ilk) { revert28 || revert29 || revert30 || revert31 || revert32 || revert33 || revert34 || revert35 || revert36 || - revert37 || revert38, "Revert rules are not covering all the cases"); + revert37 || revert38, "Revert rules are not covering all the cases"; } rule exec_ilk_culled(bytes32 ilk) { @@ -725,71 +694,63 @@ rule exec_ilk_culled(bytes32 ilk) { address vow = vow(); - require(vat() == vat); - require(daiJoin() == daiJoin); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(vow != daiJoin); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); - - uint256 LineBefore = vat.Line(); - uint256 debtBefore = vat.debt(); - uint256 ArtBefore; - uint256 rateBefore; - uint256 spotBefore; - uint256 lineBefore; - uint256 dustBefore; + require plan(ilk) == plan; + require pool(ilk) == pool; + require vow != daiJoin; + + mathint LineBefore = vat.Line(); + mathint debtBefore = vat.debt(); + mathint ArtBefore; + mathint rateBefore; + mathint spotBefore; + mathint lineBefore; + mathint dustBefore; ArtBefore, rateBefore, spotBefore, lineBefore, dustBefore = vat.ilks(ilk); - uint256 inkBefore; - uint256 artBefore; + mathint inkBefore; + mathint artBefore; inkBefore, artBefore = vat.urns(ilk, pool); - uint256 maxWithdraw = pool.maxWithdraw(e); - uint256 assetsBefore = pool.assetBalance(e); - uint256 targetAssets = plan.getTargetAssets(e, assetsBefore); + mathint maxWithdraw = pool.maxWithdraw(e); + mathint assetsBefore = pool.assetBalance(e); + mathint targetAssets = plan.getTargetAssets(e, assert_uint256(assetsBefore)); - require(vat.live() == 1); - require(inkBefore >= artBefore); - require(assetsBefore >= inkBefore); + require vat.live() == 1; + require inkBefore >= artBefore; + require assetsBefore >= inkBefore; cull(e, ilk); - uint256 vatGemPoolBefore = vat.gem(ilk, pool); - uint256 vatDaiVowBefore = vat.dai(vow); + mathint vatGemPoolBefore = vat.gem(ilk, pool); + mathint vatDaiVowBefore = vat.dai(vow); exec(e, ilk); - uint256 LineAfter = vat.Line(); - uint256 debtAfter = vat.debt(); - uint256 ArtAfter; - uint256 rateAfter; - uint256 spotAfter; - uint256 lineAfter; - uint256 dustAfter; + mathint LineAfter = vat.Line(); + mathint debtAfter = vat.debt(); + mathint ArtAfter; + mathint rateAfter; + mathint spotAfter; + mathint lineAfter; + mathint dustAfter; ArtAfter, rateAfter, spotAfter, lineAfter, dustAfter = vat.ilks(ilk); - uint256 inkAfter; - uint256 artAfter; + mathint inkAfter; + mathint artAfter; inkAfter, artAfter = vat.urns(ilk, pool); - uint256 assetsAfter = pool.assetBalance(e); + mathint assetsAfter = pool.assetBalance(e); - uint256 vatGemPoolAfter = vat.gem(ilk, pool); - uint256 vatDaiVowAfter = vat.dai(vow); + mathint vatGemPoolAfter = vat.gem(ilk, pool); + mathint vatDaiVowAfter = vat.dai(vow); // General asserts - assert(LineAfter == LineBefore, "Line should not change"); - assert(lineAfter == lineBefore, "line should not change"); - assert(artAfter == 0, "art should end up being 0"); - assert(inkAfter == 0, "ink should end up being 0"); - - assert(assetsAfter == 0 || assetsAfter == assetsBefore - maxWithdraw, "assets should be 0 or decreased by maxWithdraw"); - assert(vatGemPoolAfter == 0 || vatGemPoolAfter == vatGemPoolBefore - maxWithdraw, "vatGemPool should be 0 or decreased by maxWithdraw"); - assert(vatDaiVowAfter == vatDaiVowBefore + (assetsBefore - assetsAfter) * RAY(), "vatDaiVow did not increase as expected"); + assert LineAfter == LineBefore, "Line should not change"; + assert lineAfter == lineBefore, "line should not change"; + assert artAfter == 0, "art should end up being 0"; + assert inkAfter == 0, "ink should end up being 0"; + + assert assetsAfter == 0 || assetsAfter == assetsBefore - maxWithdraw, "assets should be 0 or decreased by maxWithdraw"; + assert vatGemPoolAfter == 0 || vatGemPoolAfter == vatGemPoolBefore - maxWithdraw, "vatGemPool should be 0 or decreased by maxWithdraw"; + assert vatDaiVowAfter == vatDaiVowBefore + (assetsBefore - assetsAfter) * RAY(), "vatDaiVow did not increase as expected"; } rule exec_ilk_culled_revert(bytes32 ilk) { @@ -797,55 +758,47 @@ rule exec_ilk_culled_revert(bytes32 ilk) { address vow = vow(); - require(vat() == vat); - require(daiJoin() == daiJoin); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(vow != daiJoin); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); - - uint256 locked = locked(); - uint256 Art; - uint256 rate; - uint256 spot; - uint256 line; - uint256 dust; + require plan(ilk) == plan; + require pool(ilk) == pool; + require vow != daiJoin; + + mathint locked = locked(); + mathint Art; + mathint rate; + mathint spot; + mathint line; + mathint dust; Art, rate, spot, line, dust = vat.ilks(ilk); - uint256 ink; - uint256 art; + mathint ink; + mathint art; ink, art = vat.urns(ilk, pool); - require(Art >= art); + require Art >= art; - uint256 maxWithdraw = pool.maxWithdraw(e); - uint256 assets = pool.assetBalance(e); + mathint maxWithdraw = pool.maxWithdraw(e); + mathint assets = pool.assetBalance(e); - require(vat.live() == 1); - require(ink >= art); - require(assets >= ink); + require vat.live() == 1; + require ink >= art; + require assets >= ink; cull(e, ilk); - uint256 vatGemPool = vat.gem(ilk, pool); - require(ink == 0 || vatGemPool == 0); // To ensure correct behavior - uint256 toSlip = vatGemPool < maxWithdraw ? vatGemPool : maxWithdraw; - uint256 vatWardHub = vat.wards(currentContract); - uint256 shareBalPool = share.balanceOf(pool); - uint256 shareSupply = share.totalSupply(); - require(shareSupply >= shareBalPool); // To ensure correct behaviour - uint256 daiBalShare = dai.balanceOf(share); - uint256 daiSupply = dai.totalSupply(); - require(daiSupply >= daiBalShare); // To ensure correct behaviour - uint256 daiAllowanceSharePool = dai.allowance(share, pool); - uint256 daiBalHub = dai.balanceOf(currentContract); - uint256 vatDaiDaiJoin = vat.dai(daiJoin); - uint256 daiAllowanceHubDaiJoin = dai.allowance(currentContract, daiJoin); - uint256 vatDaiHub = vat.dai(currentContract); - uint256 vatDaiVow = vat.dai(vow); + mathint vatGemPool = vat.gem(ilk, pool); + require ink == 0 || vatGemPool == 0; // To ensure correct behaviour + mathint toSlip = vatGemPool < maxWithdraw ? vatGemPool : maxWithdraw; + mathint vatWardHub = vat.wards(currentContract); + mathint shareBalPool = share.balanceOf(pool); + mathint shareSupply = share.totalSupply(); + require shareSupply >= shareBalPool; // To ensure correct behaviour + mathint daiBalShare = dai.balanceOf(share); + mathint daiSupply = dai.totalSupply(); + require daiSupply >= daiBalShare; // To ensure correct behaviour + mathint daiAllowanceSharePool = dai.allowance(share, pool); + mathint daiBalHub = dai.balanceOf(currentContract); + mathint vatDaiDaiJoin = vat.dai(daiJoin); + mathint daiAllowanceHubDaiJoin = dai.allowance(currentContract, daiJoin); + mathint vatDaiHub = vat.dai(currentContract); + mathint vatDaiVow = vat.dai(vow); exec@withrevert(e, ilk); @@ -864,26 +817,26 @@ rule exec_ilk_culled_revert(bytes32 ilk) { bool revert13 = maxWithdraw > 0 && vatDaiHub + maxWithdraw * RAY() > max_uint256; bool revert14 = maxWithdraw > 0 && vatDaiVow + maxWithdraw * RAY() > max_uint256; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); - assert(revert6 => lastReverted, "revert6 failed"); - assert(revert7 => lastReverted, "revert7 failed"); - assert(revert8 => lastReverted, "revert8 failed"); - assert(revert9 => lastReverted, "revert9 failed"); - assert(revert10 => lastReverted, "revert10 failed"); - assert(revert11 => lastReverted, "revert11 failed"); - assert(revert12 => lastReverted, "revert12 failed"); - assert(revert13 => lastReverted, "revert13 failed"); - assert(revert14 => lastReverted, "revert14 failed"); - - assert(lastReverted => revert1 || revert2 || revert3 || + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; + assert revert6 => lastReverted, "revert6 failed"; + assert revert7 => lastReverted, "revert7 failed"; + assert revert8 => lastReverted, "revert8 failed"; + assert revert9 => lastReverted, "revert9 failed"; + assert revert10 => lastReverted, "revert10 failed"; + assert revert11 => lastReverted, "revert11 failed"; + assert revert12 => lastReverted, "revert12 failed"; + assert revert13 => lastReverted, "revert13 failed"; + assert revert14 => lastReverted, "revert14 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8 || revert9 || revert10 || revert11 || revert12 || - revert13 || revert14, "Revert rules are not covering all the cases"); + revert13 || revert14, "Revert rules are not covering all the cases"; } rule exec_vat_caged(bytes32 ilk) { @@ -891,75 +844,65 @@ rule exec_vat_caged(bytes32 ilk) { address vow = vow(); - require(vat() == vat); - require(daiJoin() == daiJoin); - require(end() == end); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(vow != daiJoin); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(end.vat() == vat); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); - - uint256 LineBefore = vat.Line(); - uint256 debtBefore = vat.debt(); - uint256 ArtBefore; - uint256 rateBefore; - uint256 spotBefore; - uint256 lineBefore; - uint256 dustBefore; + require plan(ilk) == plan; + require pool(ilk) == pool; + require vow != daiJoin; + + mathint LineBefore = vat.Line(); + mathint debtBefore = vat.debt(); + mathint ArtBefore; + mathint rateBefore; + mathint spotBefore; + mathint lineBefore; + mathint dustBefore; ArtBefore, rateBefore, spotBefore, lineBefore, dustBefore = vat.ilks(ilk); - uint256 inkBefore; - uint256 artBefore; + mathint inkBefore; + mathint artBefore; inkBefore, artBefore = vat.urns(ilk, pool); - uint256 maxWithdraw = pool.maxWithdraw(e); - uint256 assetsBefore = pool.assetBalance(e); - uint256 targetAssets = plan.getTargetAssets(e, assetsBefore); + mathint maxWithdraw = pool.maxWithdraw(e); + mathint assetsBefore = pool.assetBalance(e); + mathint targetAssets = plan.getTargetAssets(e, assert_uint256(assetsBefore)); - require(vat.live() == 0); - require(end.tag(ilk) == RAY()); - require(inkBefore >= artBefore); - require(assetsBefore >= inkBefore); + require vat.live() == 0; + require to_mathint(end.tag(ilk)) == RAY(); + require inkBefore >= artBefore; + require assetsBefore >= inkBefore; - uint256 vatGemEndBeforeOriginal = vat.gem(ilk, end); - require(inkBefore == 0 || vatGemEndBeforeOriginal == 0); // To ensure correct behavior - uint256 vatGemEndBefore = vatGemEndBeforeOriginal != 0 ? vatGemEndBeforeOriginal : artBefore; - uint256 vatDaiVowBefore = vat.dai(vow); + mathint vatGemEndBeforeOriginal = vat.gem(ilk, end); + require inkBefore == 0 || vatGemEndBeforeOriginal == 0; // To ensure correct behaviour + mathint vatGemEndBefore = vatGemEndBeforeOriginal != 0 ? vatGemEndBeforeOriginal : artBefore; + mathint vatDaiVowBefore = vat.dai(vow); - require(assetsBefore >= vatGemEndBefore); + require assetsBefore >= vatGemEndBefore; exec(e, ilk); - uint256 LineAfter = vat.Line(); - uint256 debtAfter = vat.debt(); - uint256 ArtAfter; - uint256 rateAfter; - uint256 spotAfter; - uint256 lineAfter; - uint256 dustAfter; + mathint LineAfter = vat.Line(); + mathint debtAfter = vat.debt(); + mathint ArtAfter; + mathint rateAfter; + mathint spotAfter; + mathint lineAfter; + mathint dustAfter; ArtAfter, rateAfter, spotAfter, lineAfter, dustAfter = vat.ilks(ilk); - uint256 inkAfter; - uint256 artAfter; + mathint inkAfter; + mathint artAfter; inkAfter, artAfter = vat.urns(ilk, pool); - uint256 assetsAfter = pool.assetBalance(e); + mathint assetsAfter = pool.assetBalance(e); - uint256 vatGemEndAfter = vat.gem(ilk, end); - uint256 vatDaiVowAfter = vat.dai(vow); + mathint vatGemEndAfter = vat.gem(ilk, end); + mathint vatDaiVowAfter = vat.dai(vow); // General asserts - assert(LineAfter == LineBefore, "Line should not change"); - assert(lineAfter == lineBefore, "line should not change"); - assert(artAfter == 0, "art should end up being 0"); + assert LineAfter == LineBefore, "Line should not change"; + assert lineAfter == lineBefore, "line should not change"; + assert artAfter == 0, "art should end up being 0"; - assert(assetsAfter == 0 || assetsAfter == assetsBefore - maxWithdraw, "assets should be 0 or decreased by maxWithdraw"); - assert(vatGemEndAfter == 0 || vatGemEndAfter == vatGemEndBefore - maxWithdraw, "vatGemEnd should be 0 or decreased by maxWithdraw"); - assert(vatDaiVowAfter == vatDaiVowBefore + (assetsBefore - assetsAfter) * RAY(), "vatDaiVow did not increase as expected"); + assert assetsAfter == 0 || assetsAfter == assetsBefore - maxWithdraw, "assets should be 0 or decreased by maxWithdraw"; + assert vatGemEndAfter == 0 || vatGemEndAfter == vatGemEndBefore - maxWithdraw, "vatGemEnd should be 0 or decreased by maxWithdraw"; + assert vatDaiVowAfter == vatDaiVowBefore + (assetsBefore - assetsAfter) * RAY(), "vatDaiVow did not increase as expected"; } rule exec_vat_caged_revert(bytes32 ilk) { @@ -967,66 +910,56 @@ rule exec_vat_caged_revert(bytes32 ilk) { address vow = vow(); - require(vat() == vat); - require(daiJoin() == daiJoin); - require(end() == end); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(vow != daiJoin); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(end.vat() == vat); - require(end.vow() == vow); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); - - uint256 locked = locked(); - uint256 Art; - uint256 rate; - uint256 spot; - uint256 line; - uint256 dust; + require plan(ilk) == plan; + require pool(ilk) == pool; + require vow != daiJoin; + require end.vow() == vow; + + mathint locked = locked(); + mathint Art; + mathint rate; + mathint spot; + mathint line; + mathint dust; Art, rate, spot, line, dust = vat.ilks(ilk); - uint256 ink; - uint256 art; + mathint ink; + mathint art; ink, art = vat.urns(ilk, pool); - require(Art >= art); - uint256 endDebt = end.debt(); - uint256 culled = culled(ilk); - - uint256 maxWithdraw = pool.maxWithdraw(e); - uint256 assets = pool.assetBalance(e); - - require(vat.live() == 0); - uint256 tag = end.tag(ilk); - require(tag == RAY()); - require(ink >= art); - require(assets >= ink); - - uint256 vatWardEnd = vat.wards(end); - uint256 gap = end.gap(ilk); - uint256 owe = art * rate / RAY() * tag / RAY(); - uint256 wad = ink < owe ? ink : owe; - uint256 vatGemEnd = vat.gem(ilk, end); - require(ink == 0 || vatGemEnd == 0); // To ensure correct behavior - uint256 vatSinVow = vat.sin(vow); - uint256 vatVice = vat.vice(); - uint256 toSlip = vatGemEnd < maxWithdraw ? vatGemEnd : maxWithdraw; - uint256 vatWardHub = vat.wards(currentContract); - uint256 shareBalPool = share.balanceOf(pool); - uint256 shareSupply = share.totalSupply(); - require(shareSupply >= shareBalPool); // To ensure correct behaviour - uint256 daiBalShare = dai.balanceOf(share); - uint256 daiSupply = dai.totalSupply(); - require(daiSupply >= daiBalShare); // To ensure correct behaviour - uint256 daiAllowanceSharePool = dai.allowance(share, pool); - uint256 daiBalHub = dai.balanceOf(currentContract); - uint256 vatDaiDaiJoin = vat.dai(daiJoin); - uint256 daiAllowanceHubDaiJoin = dai.allowance(currentContract, daiJoin); - uint256 vatDaiHub = vat.dai(currentContract); - uint256 vatDaiVow = vat.dai(vow); + require Art >= art; + mathint endDebt = end.debt(); + mathint culled = culled(ilk); + + mathint maxWithdraw = pool.maxWithdraw(e); + mathint assets = pool.assetBalance(e); + + require vat.live() == 0; + mathint tag = end.tag(ilk); + require tag == RAY(); + require ink >= art; + require assets >= ink; + + mathint vatWardEnd = vat.wards(end); + mathint gap = end.gap(ilk); + mathint owe = art * rate / RAY() * tag / RAY(); + mathint wad = ink < owe ? ink : owe; + mathint vatGemEnd = vat.gem(ilk, end); + require ink == 0 || vatGemEnd == 0; // To ensure correct behaviour + mathint vatSinVow = vat.sin(vow); + mathint vatVice = vat.vice(); + mathint toSlip = vatGemEnd < maxWithdraw ? vatGemEnd : maxWithdraw; + mathint vatWardHub = vat.wards(currentContract); + mathint shareBalPool = share.balanceOf(pool); + mathint shareSupply = share.totalSupply(); + require shareSupply >= shareBalPool; // To ensure correct behaviour + mathint daiBalShare = dai.balanceOf(share); + mathint daiSupply = dai.totalSupply(); + require daiSupply >= daiBalShare; // To ensure correct behaviour + mathint daiAllowanceSharePool = dai.allowance(share, pool); + mathint daiBalHub = dai.balanceOf(currentContract); + mathint vatDaiDaiJoin = vat.dai(daiJoin); + mathint daiAllowanceHubDaiJoin = dai.allowance(currentContract, daiJoin); + mathint vatDaiHub = vat.dai(currentContract); + mathint vatDaiVow = vat.dai(vow); exec@withrevert(e, ilk); @@ -1058,35 +991,35 @@ rule exec_vat_caged_revert(bytes32 ilk) { bool revert26 = maxWithdraw > 0 && vatDaiHub + maxWithdraw * RAY() > max_uint256; bool revert27 = maxWithdraw > 0 && vatDaiVow + maxWithdraw * RAY() > max_uint256; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); - assert(revert6 => lastReverted, "revert6 failed"); - assert(revert7 => lastReverted, "revert7 failed"); - assert(revert8 => lastReverted, "revert8 failed"); - assert(revert9 => lastReverted, "revert9 failed"); - assert(revert10 => lastReverted, "revert10 failed"); - assert(revert11 => lastReverted, "revert11 failed"); - assert(revert12 => lastReverted, "revert12 failed"); - assert(revert13 => lastReverted, "revert13 failed"); - assert(revert14 => lastReverted, "revert14 failed"); - assert(revert15 => lastReverted, "revert15 failed"); - assert(revert16 => lastReverted, "revert16 failed"); - assert(revert17 => lastReverted, "revert17 failed"); - assert(revert18 => lastReverted, "revert18 failed"); - assert(revert19 => lastReverted, "revert19 failed"); - assert(revert20 => lastReverted, "revert20 failed"); - assert(revert21 => lastReverted, "revert21 failed"); - assert(revert22 => lastReverted, "revert22 failed"); - assert(revert23 => lastReverted, "revert23 failed"); - assert(revert24 => lastReverted, "revert24 failed"); - assert(revert25 => lastReverted, "revert25 failed"); - assert(revert26 => lastReverted, "revert26 failed"); - assert(revert27 => lastReverted, "revert27 failed"); - - assert(lastReverted => revert1 || revert2 || revert3 || + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; + assert revert6 => lastReverted, "revert6 failed"; + assert revert7 => lastReverted, "revert7 failed"; + assert revert8 => lastReverted, "revert8 failed"; + assert revert9 => lastReverted, "revert9 failed"; + assert revert10 => lastReverted, "revert10 failed"; + assert revert11 => lastReverted, "revert11 failed"; + assert revert12 => lastReverted, "revert12 failed"; + assert revert13 => lastReverted, "revert13 failed"; + assert revert14 => lastReverted, "revert14 failed"; + assert revert15 => lastReverted, "revert15 failed"; + assert revert16 => lastReverted, "revert16 failed"; + assert revert17 => lastReverted, "revert17 failed"; + assert revert18 => lastReverted, "revert18 failed"; + assert revert19 => lastReverted, "revert19 failed"; + assert revert20 => lastReverted, "revert20 failed"; + assert revert21 => lastReverted, "revert21 failed"; + assert revert22 => lastReverted, "revert22 failed"; + assert revert23 => lastReverted, "revert23 failed"; + assert revert24 => lastReverted, "revert24 failed"; + assert revert25 => lastReverted, "revert25 failed"; + assert revert26 => lastReverted, "revert26 failed"; + assert revert27 => lastReverted, "revert27 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8 || revert9 || revert10 || revert11 || revert12 || @@ -1094,127 +1027,110 @@ rule exec_vat_caged_revert(bytes32 ilk) { revert16 || revert17 || revert18 || revert19 || revert20 || revert21 || revert22 || revert23 || revert24 || - revert25 || revert26 || revert27, "Revert rules are not covering all the cases"); + revert25 || revert26 || revert27, "Revert rules are not covering all the cases"; } rule exec_exec(bytes32 ilk) { env e; - require(vat() == vat); - require(daiJoin() == daiJoin); - require(plan(ilk) == plan); - require(pool(ilk) == pool); - require(daiJoin.dai() == dai); - require(daiJoin.vat() == vat); - require(plan.dai() == dai); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.dai() == dai); + require plan(ilk) == plan; + require pool(ilk) == pool; - uint256 maxDeposit = pool.maxDeposit(e); - uint256 assetsBefore = pool.assetBalance(e); - uint256 targetAssets = plan.getTargetAssets(e, assetsBefore); + mathint maxDeposit = pool.maxDeposit(e); + mathint assetsBefore = pool.assetBalance(e); + mathint targetAssets = plan.getTargetAssets(e, assert_uint256(assetsBefore)); - require(maxDeposit > targetAssets - assetsBefore); - require(assetsBefore <= safe_max()); + require maxDeposit > targetAssets - assetsBefore; + require assetsBefore <= safe_max(); exec(e, ilk); - uint256 assetsAfter1 = pool.assetBalance(e); + mathint assetsAfter1 = pool.assetBalance(e); - uint256 inkAfter1; - uint256 artAfter1; + mathint inkAfter1; + mathint artAfter1; inkAfter1, artAfter1 = vat.urns(ilk, pool); exec(e, ilk); - uint256 assetsAfter2 = pool.assetBalance(e); + mathint assetsAfter2 = pool.assetBalance(e); - uint256 inkAfter2; - uint256 artAfter2; + mathint inkAfter2; + mathint artAfter2; inkAfter2, artAfter2 = vat.urns(ilk, pool); - assert(assetsAfter2 == assetsAfter1, "assetsAfter did not remain as expected"); - assert(inkAfter2 == inkAfter1, "inkAfter did not remain as expected"); - assert(artAfter2 == artAfter1, "artAfter did not remain as expected"); + assert assetsAfter2 == assetsAfter1, "assetsAfter did not remain as expected"; + assert inkAfter2 == inkAfter1, "inkAfter did not remain as expected"; + assert artAfter2 == artAfter1, "artAfter did not remain as expected"; } rule exit(bytes32 ilk, address usr, uint256 wad) { env e; - require(vat() == vat); - require(pool(ilk) == pool); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.share() == share); + require pool(ilk) == pool; - uint256 vatGemSenderBefore = vat.gem(ilk, e.msg.sender); - uint256 poolShareUsrBefore = share.balanceOf(usr); + mathint vatGemSenderBefore = vat.gem(ilk, e.msg.sender); + mathint poolShareUsrBefore = share.balanceOf(usr); exit(e, ilk, usr, wad); - uint256 vatGemSenderAfter = vat.gem(ilk, e.msg.sender); - uint256 poolShareUsrAfter = share.balanceOf(usr); + mathint vatGemSenderAfter = vat.gem(ilk, e.msg.sender); + mathint poolShareUsrAfter = share.balanceOf(usr); - assert(vatGemSenderAfter == vatGemSenderBefore - wad, "vatGemSender did not decrease by wad amount"); - assert(usr != pool => poolShareUsrAfter == poolShareUsrBefore + wad, "poolShareUsr did not increase by wad amount"); + assert vatGemSenderAfter == vatGemSenderBefore - wad, "vatGemSender did not decrease by wad amount"; + assert usr != pool => poolShareUsrAfter == poolShareUsrBefore + wad, "poolShareUsr did not increase by wad amount"; } rule exit_revert(bytes32 ilk, address usr, uint256 wad) { env e; - require(vat() == vat); - require(pool(ilk) == pool); - require(pool.hub() == currentContract); - require(pool.vat() == vat); - require(pool.share() == share); + require pool(ilk) == pool; - uint256 locked = locked(); - uint256 gem = vat.gem(ilk, e.msg.sender); - uint256 vatWard = vat.wards(currentContract); - uint256 balPool = share.balanceOf(pool); - uint256 balUsr = share.balanceOf(usr); + mathint locked = locked(); + mathint gem = vat.gem(ilk, e.msg.sender); + mathint vatWard = vat.wards(currentContract); + mathint balPool = share.balanceOf(pool); + mathint balUsr = share.balanceOf(usr); exit@withrevert(e, ilk, usr, wad); bool revert1 = e.msg.value > 0; bool revert2 = locked != 0; - bool revert3 = wad > max_int256(); + bool revert3 = to_mathint(wad) > max_int256(); bool revert4 = vatWard != 1; - bool revert5 = gem < wad; - bool revert6 = balPool < wad; + bool revert5 = gem < to_mathint(wad); + bool revert6 = balPool < to_mathint(wad); bool revert7 = pool != usr && balUsr + wad > max_uint256; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); - assert(revert6 => lastReverted, "revert6 failed"); - assert(revert7 => lastReverted, "revert7 failed"); + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; + assert revert6 => lastReverted, "revert6 failed"; + assert revert7 => lastReverted, "revert7 failed"; - assert(lastReverted => revert1 || revert2 || revert3 || + assert lastReverted => revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || - revert7, "Revert rules are not covering all the cases"); + revert7, "Revert rules are not covering all the cases"; } rule cage(bytes32 ilk) { env e; - require(vat() == vat); cage(e, ilk); - assert(tic(ilk) == e.block.timestamp + tau(ilk), "tic was not set as expected"); + assert to_mathint(tic(ilk)) == e.block.timestamp + tau(ilk), "tic was not set as expected"; } rule cage_revert(bytes32 ilk) { env e; - uint256 ward = wards(e.msg.sender); - uint256 vatLive = vat.live(); - uint256 tic = tic(ilk); - uint256 tau = tau(ilk); + mathint ward = wards(e.msg.sender); + mathint vatLive = vat.live(); + mathint tic = tic(ilk); + mathint tau = tau(ilk); cage@withrevert(e, ilk); @@ -1224,87 +1140,85 @@ rule cage_revert(bytes32 ilk) { bool revert4 = tic != 0; bool revert5 = e.block.timestamp + tau > max_uint256; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; - assert(lastReverted => revert1 || revert2 || revert3 || - revert4 || revert5, "Revert rules are not covering all the cases"); + assert lastReverted => revert1 || revert2 || revert3 || + revert4 || revert5, "Revert rules are not covering all the cases"; } rule cull(bytes32 ilk) { env e; - require(vat() == vat); - - uint256 ArtBefore; - uint256 rateBefore; - uint256 spotBefore; - uint256 lineBefore; - uint256 dustBefore; + mathint ArtBefore; + mathint rateBefore; + mathint spotBefore; + mathint lineBefore; + mathint dustBefore; ArtBefore, rateBefore, spotBefore, lineBefore, dustBefore = vat.ilks(ilk); - require(rateBefore == RAY()); + require rateBefore == RAY(); - uint256 inkBefore; - uint256 artBefore; + mathint inkBefore; + mathint artBefore; inkBefore, artBefore = vat.urns(ilk, pool(ilk)); - uint256 vatGemPoolBefore = vat.gem(ilk, pool(ilk)); - uint256 vatSinVowBefore = vat.sin(vow()); - uint256 vatViceBefore = vat.vice(); + mathint vatGemPoolBefore = vat.gem(ilk, pool(ilk)); + mathint vatSinVowBefore = vat.sin(vow()); + mathint vatViceBefore = vat.vice(); cull(e, ilk); - uint256 inkAfter; - uint256 artAfter; + mathint inkAfter; + mathint artAfter; inkAfter, artAfter = vat.urns(ilk, pool(ilk)); - uint256 vatGemPoolAfter = vat.gem(ilk, pool(ilk)); + mathint vatGemPoolAfter = vat.gem(ilk, pool(ilk)); - uint256 culledAfter = culled(ilk); - uint256 vatSinVowAfter = vat.sin(vow()); - uint256 vatViceAfter = vat.vice(); + mathint culledAfter = culled(ilk); + mathint vatSinVowAfter = vat.sin(vow()); + mathint vatViceAfter = vat.vice(); - assert(inkAfter == 0, "ink did not go to 0 as expected"); - assert(artAfter == 0, "art did not go to 0 as expected"); - assert(vatGemPoolAfter == vatGemPoolBefore + inkBefore, "vatGemPool did not increase as expected"); - assert(culledAfter == 1, "culled was not set to 1 as expected"); - assert(vatSinVowAfter == vatSinVowBefore + artBefore * RAY(), "vatSinVow did not increase as expected"); - assert(vatViceAfter == vatViceBefore + artBefore * RAY(), "vatVice did not increase as expected"); + assert inkAfter == 0, "ink did not go to 0 as expected"; + assert artAfter == 0, "art did not go to 0 as expected"; + assert vatGemPoolAfter == vatGemPoolBefore + inkBefore, "vatGemPool did not increase as expected"; + assert culledAfter == 1, "culled was not set to 1 as expected"; + assert vatSinVowAfter == vatSinVowBefore + artBefore * RAY(), "vatSinVow did not increase as expected"; + assert vatViceAfter == vatViceBefore + artBefore * RAY(), "vatVice did not increase as expected"; } rule cull_revert(bytes32 ilk) { env e; - uint256 vatLive = vat.live(); - uint256 tic = tic(ilk); - uint256 ward = wards(e.msg.sender); - uint256 culled = culled(ilk); - uint256 ink; - uint256 art; + mathint vatLive = vat.live(); + mathint tic = tic(ilk); + mathint ward = wards(e.msg.sender); + mathint culled = culled(ilk); + mathint ink; + mathint art; ink, art = vat.urns(ilk, pool(ilk)); - uint256 vatWard = vat.wards(currentContract); - uint256 Art; - uint256 rate; - uint256 spot; - uint256 line; - uint256 dust; + mathint vatWard = vat.wards(currentContract); + mathint Art; + mathint rate; + mathint spot; + mathint line; + mathint dust; Art, rate, spot, line, dust = vat.ilks(ilk); - require(Art >= art); - require(rate == RAY()); - uint256 vatGemPool = vat.gem(ilk, pool(ilk)); - uint256 vatSinVow = vat.sin(vow()); - uint256 vatVice = vat.vice(); + require Art >= art; + require rate == RAY(); + mathint vatGemPool = vat.gem(ilk, pool(ilk)); + mathint vatSinVow = vat.sin(vow()); + mathint vatVice = vat.vice(); cull@withrevert(e, ilk); bool revert1 = e.msg.value > 0; bool revert2 = vatLive != 1; bool revert3 = tic == 0; - bool revert4 = tic > e.block.timestamp && ward != 1; + bool revert4 = tic > to_mathint(e.block.timestamp) && ward != 1; bool revert5 = culled != 0; bool revert6 = ink > max_int256(); bool revert7 = art > max_int256(); @@ -1314,84 +1228,83 @@ rule cull_revert(bytes32 ilk) { bool revert11 = vatSinVow + art * RAY() > max_uint256; bool revert12 = vatVice + art * RAY() > max_uint256; - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); - assert(revert6 => lastReverted, "revert6 failed"); - assert(revert7 => lastReverted, "revert7 failed"); - assert(revert8 => lastReverted, "revert8 failed"); - assert(revert9 => lastReverted, "revert9 failed"); - assert(revert10 => lastReverted, "revert10 failed"); - assert(revert11 => lastReverted, "revert11 failed"); - assert(revert12 => lastReverted, "revert12 failed"); - - assert(lastReverted => revert1 || revert2 || revert3 || + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; + assert revert6 => lastReverted, "revert6 failed"; + assert revert7 => lastReverted, "revert7 failed"; + assert revert8 => lastReverted, "revert8 failed"; + assert revert9 => lastReverted, "revert9 failed"; + assert revert10 => lastReverted, "revert10 failed"; + assert revert11 => lastReverted, "revert11 failed"; + assert revert12 => lastReverted, "revert12 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8 || revert9 || - revert10 || revert11 || revert12, "Revert rules are not covering all the cases"); + revert10 || revert11 || revert12, "Revert rules are not covering all the cases"; } rule uncull(bytes32 ilk) { env e; - require(vat() == vat); - uint256 ArtBefore; - uint256 rateBefore; - uint256 spotBefore; - uint256 lineBefore; - uint256 dustBefore; + mathint ArtBefore; + mathint rateBefore; + mathint spotBefore; + mathint lineBefore; + mathint dustBefore; ArtBefore, rateBefore, spotBefore, lineBefore, dustBefore = vat.ilks(ilk); - require(rateBefore == RAY()); + require rateBefore == RAY(); - uint256 inkBefore; - uint256 artBefore; + mathint inkBefore; + mathint artBefore; inkBefore, artBefore = vat.urns(ilk, pool(ilk)); - uint256 vatGemPoolBefore = vat.gem(ilk, pool(ilk)); - uint256 vatDaiVowBefore = vat.dai(vow()); + mathint vatGemPoolBefore = vat.gem(ilk, pool(ilk)); + mathint vatDaiVowBefore = vat.dai(vow()); uncull(e, ilk); - uint256 inkAfter; - uint256 artAfter; + mathint inkAfter; + mathint artAfter; inkAfter, artAfter = vat.urns(ilk, pool(ilk)); - uint256 vatGemPoolAfter = vat.gem(ilk, pool(ilk)); + mathint vatGemPoolAfter = vat.gem(ilk, pool(ilk)); - uint256 culledAfter = culled(ilk); - uint256 vatDaiVowAfter = vat.dai(vow()); + mathint culledAfter = culled(ilk); + mathint vatDaiVowAfter = vat.dai(vow()); - assert(inkAfter == inkBefore + vatGemPoolBefore, "ink did not increase by prev value of vatGemPool as expected"); - assert(artAfter == artBefore + vatGemPoolBefore, "art did not increase by prev value of vatGemPool as expected"); - assert(vatGemPoolAfter == 0, "vatGemPool did not descrease to 0 as expected"); - assert(culledAfter == 0, "culled was not set to 0 as expected"); - assert(vatDaiVowAfter == vatDaiVowBefore + vatGemPoolBefore * RAY(), "vatDaiVow did not increase as expected"); + assert inkAfter == inkBefore + vatGemPoolBefore, "ink did not increase by prev value of vatGemPool as expected"; + assert artAfter == artBefore + vatGemPoolBefore, "art did not increase by prev value of vatGemPool as expected"; + assert vatGemPoolAfter == 0, "vatGemPool did not descrease to 0 as expected"; + assert culledAfter == 0, "culled was not set to 0 as expected"; + assert vatDaiVowAfter == vatDaiVowBefore + vatGemPoolBefore * RAY(), "vatDaiVow did not increase as expected"; } rule uncull_revert(bytes32 ilk) { env e; - uint256 culled = culled(ilk); - uint256 vatLive = vat.live(); - uint256 vatGemPool = vat.gem(ilk, pool(ilk)); - uint256 vatWard = vat.wards(currentContract); - uint256 vatSinVow = vat.sin(vow()); - uint256 vatDaiVow = vat.dai(vow()); - uint256 vatVice = vat.vice(); - uint256 vatDebt = vat.debt(); - uint256 Art; - uint256 rate; - uint256 spot; - uint256 line; - uint256 dust; + mathint culled = culled(ilk); + mathint vatLive = vat.live(); + mathint vatGemPool = vat.gem(ilk, pool(ilk)); + mathint vatWard = vat.wards(currentContract); + mathint vatSinVow = vat.sin(vow()); + mathint vatDaiVow = vat.dai(vow()); + mathint vatVice = vat.vice(); + mathint vatDebt = vat.debt(); + mathint Art; + mathint rate; + mathint spot; + mathint line; + mathint dust; Art, rate, spot, line, dust = vat.ilks(ilk); - require(rate == RAY()); - uint256 ink; - uint256 art; + require rate == RAY(); + mathint ink; + mathint art; ink, art = vat.urns(ilk, pool(ilk)); uncull@withrevert(e, ilk); @@ -1409,21 +1322,21 @@ rule uncull_revert(bytes32 ilk) { bool revert11 = Art + vatGemPool > max_uint256; bool revert12 = rate * vatGemPool > max_int256(); - assert(revert1 => lastReverted, "revert1 failed"); - assert(revert2 => lastReverted, "revert2 failed"); - assert(revert3 => lastReverted, "revert3 failed"); - assert(revert4 => lastReverted, "revert4 failed"); - assert(revert5 => lastReverted, "revert5 failed"); - assert(revert6 => lastReverted, "revert6 failed"); - assert(revert7 => lastReverted, "revert7 failed"); - assert(revert8 => lastReverted, "revert8 failed"); - assert(revert9 => lastReverted, "revert9 failed"); - assert(revert10 => lastReverted, "revert10 failed"); - assert(revert11 => lastReverted, "revert11 failed"); - assert(revert12 => lastReverted, "revert12 failed"); - - assert(lastReverted => revert1 || revert2 || revert3 || + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert revert5 => lastReverted, "revert5 failed"; + assert revert6 => lastReverted, "revert6 failed"; + assert revert7 => lastReverted, "revert7 failed"; + assert revert8 => lastReverted, "revert8 failed"; + assert revert9 => lastReverted, "revert9 failed"; + assert revert10 => lastReverted, "revert10 failed"; + assert revert11 => lastReverted, "revert11 failed"; + assert revert12 => lastReverted, "revert12 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || revert4 || revert5 || revert6 || revert7 || revert8 || revert9 || - revert10 || revert11 || revert12, "Revert rules are not covering all the cases"); + revert10 || revert11 || revert12, "Revert rules are not covering all the cases"; }