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 integirtyBalanceOfTotalSupplyOnBurn rule for StableDebtToken.

Browse Source
This commit is contained in:
pistiner 2020-11-23 19:25:47 +02:00
parent 9e07c03f33
commit 296f1046ad
3 changed files with 43 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
runStableTokenCLI.sh
View File

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

41
specs/StableDebtToken.spec
View File

@ -36,7 +36,7 @@ rule balanceOfChange(address a, address b, method f)
}
/**
Checks that the change to total supply is coherent with the change to balance due to an operation
Checks that the change to total supply is coherent with the change to user balance due to an operation
(which is not burn).
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
@ -55,24 +55,49 @@ rule integirtyBalanceOfTotalSupply(address a, method f )
assert (balanceAAfter != balanceABefore => (balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/**
Burn behaves differently and due to accumulation errors might have less total supply than the balance.
Checks that the change to total supply is coherent with the change to user balance due to a burn operation.
*/
rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
rule integirtyBalanceOfTotalSupplyOnBurn(address a, uint256 x)
{
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 balanceABefore = sinvoke balanceOf(e, a);
uint256 totalSupplyBefore = sinvoke totalSupply(e);
uint256 x;
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);
sinvoke burn(e, a, x);
uint256 balanceAAfter = sinvoke balanceOf(e, a);
uint256 totalSupplyAfter = sinvoke totalSupply(e);
if (totalSupplyBefore > x)
assert (balanceAAfter != balanceABefore => (balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
else
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.
*/
assert (totalSupplyAfter == 0);
}
}
/**

10
specs/harness/StableDebtTokenHarness.sol
View File

@ -11,7 +11,11 @@ contract StableDebtTokenHarness is StableDebtToken {
string memory symbol,
address incentivesController
) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
/**
Simplification: The user accumulates no interest (the balance increase is always 0).
**/
function balanceOf(address account) public override view returns (uint256) {
return IncentivizedERC20.balanceOf(account);
}
@ -23,4 +27,8 @@ contract StableDebtTokenHarness is StableDebtToken {
function getIncentivesController() public view returns (address) {
return address(_incentivesController);
}
function rayWadMul(uint256 aRay, uint256 bWad) external view returns(uint256) {
return aRay.rayMul(bWad.wadToRay());
}
}