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

Fixes to run on StableDebtToken contract

Browse Source
This commit is contained in:
pistiner 2020-10-29 01:57:15 +02:00
parent a63e337222
commit 4030d48787
3 changed files with 1 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
contracts/tokenization/StableDebtToken.sol
View File

@ -286,7 +286,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
* @param avgRate the average rate at which calculate the total supply * @param avgRate the average rate at which calculate the total supply
* @return The debt balance of the user since the last burn/mint action * @return The debt balance of the user since the last burn/mint action
**/ **/
function _calcTotalSupply(uint256 avgRate) internal view returns (uint256) { function _calcTotalSupply(uint256 avgRate) internal virtual view returns (uint256) {
uint256 principalSupply = super.totalSupply(); uint256 principalSupply = super.totalSupply();
if (principalSupply == 0) { if (principalSupply == 0) {

16
specs/StableDebtToken.spec
View File

@ -2,13 +2,6 @@ methods {
getUserLastUpdated(address) returns uint40 envfree getUserLastUpdated(address) returns uint40 envfree
} }
ghost ghostSupply() returns uint256;
hook Sstore (slot 0)[address a] uint256 balance (uint256 old_balance) STORAGE {
require old_balance <= ghostSupply();
havoc ghostSupply assuming ghostSupply@new() == ghostSupply@old() + (balance - old_balance);
}
rule integrityTimeStamp(address user, method f) { rule integrityTimeStamp(address user, method f) {
env e; env e;
require sinvoke getIncentivesController(e) == 0; require sinvoke getIncentivesController(e) == 0;
@ -18,15 +11,6 @@ rule integrityTimeStamp(address user, method f) {
assert getUserLastUpdated(user) <= e.block.timestamp; assert getUserLastUpdated(user) <= e.block.timestamp;
} }
rule totalSupplyInvariant(method f) {
env e;
require sinvoke getIncentivesController(e) == 0;
require totalSupply(e) == ghostSupply();
calldataarg arg;
sinvoke f(e, arg);
assert totalSupply(e) == ghostSupply();
}
/** /**
TotalSupply is the sum of all users’ balances TotalSupply is the sum of all users’ balances

3
specs/harness/StableDebtTokenHarness.sol
View File

@ -1,8 +1,5 @@
pragma solidity ^0.6.8; pragma solidity ^0.6.8;
import {Context} from '@openzeppelin/contracts/GSN/Context.sol';
import {IERC20} from '@openzeppelin/contracts/token/ERC20/IERC20.sol';
import {SafeMath} from '@openzeppelin/contracts/math/SafeMath.sol';
import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol'; import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol'; import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';