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

Updates in the specification of StableDebtToken

Browse Source
This commit is contained in:
pistiner 2020-10-29 23:19:11 +02:00
parent d4f0e05f06
commit 5cc6acce86
2 changed files with 11 additions and 5 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,-useNonLinearArithmetic --cache StableDebtToken --staging master
certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master

14
specs/StableDebtToken.spec
View File

@ -90,19 +90,25 @@ rule integrityMint(address a, uint256 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
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.
*/
rule additiveMint(address a, uint256 x, uint256 y) {
env e;
require sinvoke getIncentivesController(e) == 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);
uint t = x + y;
uint256 t = x + y;
sinvoke mint(e,a, t ,index) at initialStorage;
uint256 balanceScenario2 = sinvoke balanceOf(e,a);
uint256 balanceScenario2 = sinvoke balanceOf(e,a);
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
@ -124,7 +130,7 @@ rule additiveBurn(address a, uint256 x, uint256 y) {
sinvoke burn(e, a, x);
sinvoke burn(e, a, y);
uint256 balanceScenario1 = balanceOf(e, a);
uint t = x + y;
uint256 t = x + y;
sinvoke burn(e, a, t) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);