aave-protocol-v2/specs/StableDebtToken.spec

184 lines
5.4 KiB
RPMSpec
Raw Normal View History

2020-10-14 21:59:12 +00:00
methods {
getUserLastUpdated(address) returns uint40 envfree
}
rule integrityTimeStamp(address user, method f) {
env e;
require sinvoke getIncentivesController(e) == 0;
require getUserLastUpdated(user) <= e.block.timestamp;
calldataarg arg;
sinvoke f(e,arg);
assert getUserLastUpdated(user) <= e.block.timestamp;
}
/**
TotalSupply is the sum of all users balances
2020-11-22 21:19:56 +00:00
totalSupply(t) = Σaddress u. balanceOf(u,t).
2020-10-14 21:59:12 +00:00
2020-11-22 21:19:56 +00:00
Checks that each possible operation changes the balance of at most one user.
2020-10-14 21:59:12 +00:00
*/
2020-11-22 21:19:56 +00:00
rule balanceOfChange(address a, address b, method f)
2020-10-14 21:59:12 +00:00
{
env e;
require a!=b;
require sinvoke getIncentivesController(e) == 0;
2020-11-22 21:19:56 +00:00
uint256 balanceABefore = sinvoke balanceOf(e, a);
uint256 balanceBBefore = sinvoke balanceOf(e, b);
2020-10-14 21:59:12 +00:00
calldataarg arg;
sinvoke f(e, arg);
2020-11-22 21:19:56 +00:00
uint256 balanceAAfter = sinvoke balanceOf(e, a);
uint256 balanceBAfter = sinvoke balanceOf(e, b);
2020-10-14 21:59:12 +00:00
2020-11-22 21:19:56 +00:00
assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
2020-10-14 21:59:12 +00:00
}
/**
Checks that the change to total supply is coherent with the change to user balance due to an operation
2020-11-22 21:19:56 +00:00
(which is not burn).
2020-10-14 21:59:12 +00:00
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
{
env e;
require sinvoke getIncentivesController(e) == 0;
2020-11-22 21:19:56 +00:00
uint256 balanceABefore = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
uint256 totalSupplyBefore = sinvoke totalSupply(e);
calldataarg arg;
sinvoke f(e, arg);
2020-11-22 21:19:56 +00:00
require (f.selector != burn(address, uint256).selector);
uint256 balanceAAfter = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
uint256 totalSupplyAfter = sinvoke totalSupply(e);
2020-11-22 21:19:56 +00:00
assert (balanceAAfter != balanceABefore => (balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
2020-10-14 21:59:12 +00:00
}
2020-11-22 21:19:56 +00:00
/**
Checks that the change to total supply is coherent with the change to user balance due to a burn operation.
2020-10-14 21:59:12 +00:00
*/
rule integirtyBalanceOfTotalSupplyOnBurn(address a, uint256 x)
2020-10-14 21:59:12 +00:00
{
env e;
require sinvoke getIncentivesController(e) == 0;
2020-11-22 21:19:56 +00:00
uint256 balanceABefore = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
uint256 totalSupplyBefore = sinvoke totalSupply(e);
uint256 averageStableRateBefore = sinvoke getAverageStableRate(e);
uint256 debtSupplyBefore = sinvoke rayWadMul(e, averageStableRateBefore, totalSupplyBefore);
uint256 stableRateA = sinvoke getUserStableRate(e, a);
uint256 repaidDebtA = sinvoke rayWadMul(e, stableRateA, x);
2020-10-14 21:59:12 +00:00
sinvoke burn(e, a, x);
2020-11-22 21:19:56 +00:00
uint256 balanceAAfter = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
uint256 totalSupplyAfter = sinvoke totalSupply(e);
if(totalSupplyBefore > x) {
/* The amount being burned (x) is smaller than the total supply */
if(repaidDebtA >= debtSupplyBefore) {
/*
The user debt being repaid is at least the debt supply.
The total supply becomes 0.
*/
assert(totalSupplyAfter == 0);
}
else {
assert(balanceAAfter != balanceABefore =>
(balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
}
else {
/* The amount being burned (x) is at least the total supply.
The total supply becomes 0.
*/
2020-11-22 21:19:56 +00:00
assert (totalSupplyAfter == 0);
}
2020-10-14 21:59:12 +00:00
}
/**
2020-11-22 21:19:56 +00:00
Mint increases the balanceOf user a as expected.
2020-10-14 21:59:12 +00:00
*/
rule integrityMint(address a, uint256 x) {
env e;
2020-11-22 21:19:56 +00:00
address delegatedUser;
2020-10-14 21:59:12 +00:00
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
2020-11-22 21:19:56 +00:00
sinvoke mint(e, delegatedUser, a, x, index);
2020-10-14 21:59:12 +00:00
uint256 balanceAfter = sinvoke balanceOf(e,a);
assert balanceAfter == balancebefore+x;
}
/**
2020-11-22 21:19:56 +00:00
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,
and therefore it is currently excluded from the CI.
2020-10-14 21:59:12 +00:00
*/
rule additiveMint(address a, uint256 x, uint256 y) {
env e;
2020-11-22 21:19:56 +00:00
address delegatedUser;
2020-10-14 21:59:12 +00:00
require sinvoke getIncentivesController(e) == 0;
2020-11-22 21:19:56 +00:00
require getUserStableRate(e, a) == 0;
2020-10-14 21:59:12 +00:00
uint256 index;
storage initialStorage = lastStorage;
2020-11-22 21:19:56 +00:00
sinvoke mint(e, delegatedUser, a, x, index);
sinvoke mint(e, delegatedUser, a, y, index);
uint256 balanceScenario1 = sinvoke balanceOf(e, a);
uint256 t = x + y;
2020-11-22 21:19:56 +00:00
sinvoke mint(e, delegatedUser, a, t ,index) at initialStorage;
2020-11-22 21:19:56 +00:00
uint256 balanceScenario2 = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
rule integrityBurn(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
2020-11-22 21:19:56 +00:00
uint256 balancebefore = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
sinvoke burn(e,a,x);
2020-11-22 21:19:56 +00:00
uint256 balanceAfter = sinvoke balanceOf(e, a);
2020-10-14 21:59:12 +00:00
assert balanceAfter == balancebefore - x;
}
rule additiveBurn(address a, uint256 x, uint256 y) {
env e;
require sinvoke getIncentivesController(e) == 0;
storage initialStorage = lastStorage;
sinvoke burn(e, a, x);
sinvoke burn(e, a, y);
uint256 balanceScenario1 = balanceOf(e, a);
uint256 t = x + y;
2020-10-14 21:59:12 +00:00
sinvoke burn(e, a, t) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "burn is not additive";
}
/**
2020-11-22 21:19:56 +00:00
Mint and burn are inverse operations.
Therefore, both totalSupply and BalanceOf user are back to the initial state.
*/
2020-10-14 21:59:12 +00:00
rule inverseMintBurn(address a, uint256 x) {
env e;
2020-11-22 21:19:56 +00:00
address delegatedUser;
2020-10-14 21:59:12 +00:00
require sinvoke getIncentivesController(e) == 0;
uint256 index;
2020-11-22 21:19:56 +00:00
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";
}