Instadapp/aave-protocol-v2
1
0
Fork 0
mirror of https://github.com/Instadapp/aave-protocol-v2.git synced 2024-07-29 21:47:30 +00:00
Code Issues Packages Projects Releases Wiki Activity

Updated StableDebtToken spec

Browse Source
This commit is contained in:
pistiner 2020-11-22 23:19:56 +02:00
parent 219d765f97
commit f90e53293d
2 changed files with 45 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
runStableTokenCLI.sh
View File

@ -1 +1 @@
certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master
certoraRun.py specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging

84
specs/StableDebtToken.spec
View File

@ -14,82 +14,85 @@ rule integrityTimeStamp(address user, method f) {
/**
TotalSupply is the sum of all users’ balances
totalSupply(t) = Σaddress u. balanceOf(u,t)
totalSupply(t) = Σaddress u. balanceOf(u,t).
Check that each possible opertaion changes the balance of at most one user
Checks that each possible operation changes the balance of at most one user.
*/
rule balanceOfChange(address a, address b, method f )
rule balanceOfChange(address a, address b, method f)
{
env e;
require a!=b;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e,a);
uint256 balanceBBefore = sinvoke balanceOf(e,b);
uint256 balanceABefore = sinvoke balanceOf(e, a);
uint256 balanceBBefore = sinvoke balanceOf(e, b);
calldataarg arg;
sinvoke f(e, arg);
uint256 balanceAAfter = sinvoke balanceOf(e,a);
uint256 balanceBAfter = sinvoke balanceOf(e,b);
uint256 balanceAAfter = sinvoke balanceOf(e, a);
uint256 balanceBAfter = sinvoke balanceOf(e, b);
assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
}
/**
Check that the change to total supply is coherent with the changes to balance
Checks that the change to total supply is coherent with the change to balance due to an operation
(which is not burn).
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
{
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e,a);
uint256 balanceABefore = sinvoke balanceOf(e, a);
uint256 totalSupplyBefore = sinvoke totalSupply(e);
calldataarg arg;
sinvoke f(e, arg);
require (f.selector != burn(address,uint256).selector );
uint256 balanceAAfter = sinvoke balanceOf(e,a);
require (f.selector != burn(address, uint256).selector);
uint256 balanceAAfter = sinvoke balanceOf(e, a);
uint256 totalSupplyAfter = sinvoke totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
assert (balanceAAfter != balanceABefore => (balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/* Burn behaves differently and due to accumulation errors might have less total supply than the balance
/**
Burn behaves differently and due to accumulation errors might have less total supply than the balance.
*/
rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
{
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e,a);
uint256 balanceABefore = sinvoke balanceOf(e, a);
uint256 totalSupplyBefore = sinvoke totalSupply(e);
uint256 x;
sinvoke burn(e, a, x);
uint256 balanceAAfter = sinvoke balanceOf(e,a);
uint256 balanceAAfter = sinvoke balanceOf(e, a);
uint256 totalSupplyAfter = sinvoke totalSupply(e);
if (totalSupplyBefore > x)
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
assert (balanceAAfter != balanceABefore => (balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
else
assert (totalSupplyAfter == 0 );
assert (totalSupplyAfter == 0);
}
/**
Mint inceases the balanceOf user a as expected
Mint increases the balanceOf user a as expected.
*/
rule integrityMint(address a, uint256 x) {
env e;
address delegatedUser;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke mint(e,a,x,index);
sinvoke mint(e, delegatedUser, a, x, index);
uint256 balanceAfter = sinvoke balanceOf(e,a);
assert balanceAfter == balancebefore+x;
}
/**
Mint is additive, can performed either all at once or gradually
mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
Mint is additive, namely it can performed either all at once or gradually:
mint(u, x); mint(u, y) ~ mint(u, x+y) at the same timestamp.
Note: We assume that the stable rate of the user is 0.
The case where the rate is non-zero takes much more time to prove,
@ -97,18 +100,19 @@ and therefore it is currently excluded from the CI.
*/
rule additiveMint(address a, uint256 x, uint256 y) {
env e;
address delegatedUser;
require sinvoke getIncentivesController(e) == 0;
require getUserStableRate(e,a) == 0;
require getUserStableRate(e, a) == 0;
uint256 index;
storage initialStorage = lastStorage;
sinvoke mint(e,a,x,index);
sinvoke mint(e,a,y,index);
uint256 balanceScenario1 = sinvoke balanceOf(e,a);
sinvoke mint(e, delegatedUser, a, x, index);
sinvoke mint(e, delegatedUser, a, y, index);
uint256 balanceScenario1 = sinvoke balanceOf(e, a);
uint256 t = x + y;
sinvoke mint(e,a, t ,index) at initialStorage;
sinvoke mint(e, delegatedUser, a, t ,index) at initialStorage;
uint256 balanceScenario2 = sinvoke balanceOf(e,a);
uint256 balanceScenario2 = sinvoke balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
@ -116,10 +120,10 @@ rule integrityBurn(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
uint256 balancebefore = sinvoke balanceOf(e, a);
sinvoke burn(e,a,x);
uint256 balanceAfter = sinvoke balanceOf(e,a);
uint256 balanceAfter = sinvoke balanceOf(e, a);
assert balanceAfter == balancebefore - x;
}
@ -139,17 +143,17 @@ rule additiveBurn(address a, uint256 x, uint256 y) {
/**
mint and burn are inverse operations
Thus, totalSupply is back to initial state
BalanceOf user is back to initial state */
Mint and burn are inverse operations.
Therefore, both totalSupply and BalanceOf user are back to the initial state.
*/
rule inverseMintBurn(address a, uint256 x) {
env e;
address delegatedUser;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke mint(e,a,x,index);
sinvoke burn(e,a,x);
uint256 balanceAfter = sinvoke balanceOf(e,a);
assert balancebefore == balanceAfter, "burn is not inverse of mint";
}
uint256 balancebefore = sinvoke balanceOf(e, a);
sinvoke mint(e, delegatedUser, a, x, index);
sinvoke burn(e, a, x);
uint256 balanceAfter = sinvoke balanceOf(e, a);
assert balancebefore == balanceAfter, "burn is not the inverse of mint";
}