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

Merge branch 'master' into fix/51

Browse Source
This commit is contained in:
emilio 2020-10-30 16:21:37 +01:00
commit 96d00edd00
23 changed files with 854 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
contracts/interfaces/ILendingPool.sol
View File

@ -33,11 +33,11 @@ interface ILendingPool {
event Withdraw(address indexed reserve, address indexed user, address indexed to, uint256 amount);
event BorrowAllowanceDelegated(
address indexed asset,
address indexed fromUser,
address indexed toUser,
uint256 interestRateMode,
uint256 amount
address[] assets,
uint256[] interestRateModes,
uint256[] amounts
);
/**
* @dev emitted on borrow
@ -100,20 +100,18 @@ interface ILendingPool {
/**
* @dev emitted when a flashloan is executed
* @param target the address of the flashLoanReceiver
* @param mode Type of the debt to open if the flash loan is not returned. 0 -> Don't open any debt, just revert, 1 -> stable, 2 -> variable
* @param onBehalfOf the address incurring the debt, if borrow mode is not 0
* @param assets the address of the assets being flashborrowed
* @param amounts the amount requested
* @param premiums the total fee on the amount
* @param initiator the address initiating the flash loan
* @param asset the address of the asset being flashborrowed
* @param amount the amount requested
* @param premium the total fee on the amount
* @param referralCode the referral code of the caller
**/
event FlashLoan(
address indexed target,
uint256 mode,
address indexed onBehalfOf,
address[] assets,
uint256[] amounts,
uint256[] premiums,
address indexed initiator,
address indexed asset,
uint256 amount,
uint256 premium,
uint16 referralCode
);
@ -198,17 +196,17 @@ interface ILendingPool {
) external;
/**
* @dev Sets allowance to borrow on a certain type of debt asset for a certain user address
* @param asset The underlying asset of the debt token
* @dev Sets allowance to borrow on a certain type of debt assets for a certain user address
* @param assets The underlying asset of each debt token
* @param user The user to give allowance to
* @param interestRateMode Type of debt: 1 for stable, 2 for variable
* @param amount Allowance amount to borrow
* @param interestRateModes Types of debt: 1 for stable, 2 for variable
* @param amounts Allowance amounts to borrow
**/
function delegateBorrowAllowance(
address asset,
address[] calldata assets,
address user,
uint256 interestRateMode,
uint256 amount
uint256[] calldata interestRateModes,
uint256[] calldata amounts
) external;
function getBorrowAllowance(
@ -295,7 +293,7 @@ interface ILendingPool {
* @param receiver The address of the contract receiving the funds. The receiver should implement the IFlashLoanReceiver interface.
* @param assets the address of the principal reserve
* @param amounts the amount requested for this flashloan
* @param mode the flashloan mode
* @param modes the flashloan borrow modes
* @param params a bytes array to be sent to the flashloan executor
* @param referralCode the referral code of the caller
**/
@ -303,7 +301,7 @@ interface ILendingPool {
address receiver,
address[] calldata assets,
uint256[] calldata amounts,
uint256 mode,
uint256[] calldata modes,
address onBehalfOf,
bytes calldata params,
uint16 referralCode

71
contracts/lendingpool/LendingPool.sol
View File

@ -186,23 +186,32 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
}
/**
* @dev Sets allowance to borrow on a certain type of debt asset for a certain user address
* @param asset The underlying asset of the debt token
* @dev Sets allowance to borrow on a certain type of debt assets for a certain user address
* @param assets The underlying asset of each debt token
* @param user The user to give allowance to
* @param interestRateMode Type of debt: 1 for stable, 2 for variable
* @param amount Allowance amount to borrow
* @param interestRateModes Types of debt: 1 for stable, 2 for variable
* @param amounts Allowance amounts to borrow
**/
function delegateBorrowAllowance(
address asset,
address[] calldata assets,
address user,
uint256 interestRateMode,
uint256 amount
uint256[] calldata interestRateModes,
uint256[] calldata amounts
) external override {
_whenNotPaused();
address debtToken = _reserves[asset].getDebtTokenAddress(interestRateMode);
_borrowAllowance[debtToken][msg.sender][user] = amount;
emit BorrowAllowanceDelegated(asset, msg.sender, user, interestRateMode, amount);
uint256 countAssets = assets.length;
require(
countAssets == interestRateModes.length && countAssets == amounts.length,
Errors.INCONSISTENT_PARAMS_LENGTH
);
for (uint256 i = 0; i < countAssets; i++) {
address debtToken = _reserves[assets[i]].getDebtTokenAddress(interestRateModes[i]);
_borrowAllowance[debtToken][msg.sender][user] = amounts[i];
}
emit BorrowAllowanceDelegated(msg.sender, user, assets, interestRateModes, amounts);
}
/**
@ -493,13 +502,13 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
struct FlashLoanLocalVars {
IFlashLoanReceiver receiver;
address oracle;
ReserveLogic.InterestRateMode debtMode;
uint256 i;
address currentAsset;
address currentATokenAddress;
uint256 currentAmount;
uint256 currentPremium;
uint256 currentAmountPlusPremium;
address debtToken;
}
/**
@ -509,7 +518,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
* @param receiverAddress The address of the contract receiving the funds. The receiver should implement the IFlashLoanReceiver interface.
* @param assets The addresss of the assets being flashborrowed
* @param amounts The amounts requested for this flashloan for each asset
* @param mode Type of the debt to open if the flash loan is not returned. 0 -> Don't open any debt, just revert, 1 -> stable, 2 -> variable
* @param modes Types of the debt to open if the flash loan is not returned. 0 -> Don't open any debt, just revert, 1 -> stable, 2 -> variable
* @param onBehalfOf If mode is not 0, then the address to take the debt onBehalfOf. The onBehalfOf address must already have approved `msg.sender` to incur the debt on their behalf.
* @param params Variadic packed params to pass to the receiver as extra information
* @param referralCode Referral code of the flash loan
@ -518,7 +527,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
address receiverAddress,
address[] calldata assets,
uint256[] calldata amounts,
uint256 mode,
uint256[] calldata modes,
address onBehalfOf,
bytes calldata params,
uint16 referralCode
@ -527,13 +536,12 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
FlashLoanLocalVars memory vars;
ValidationLogic.validateFlashloan(assets, amounts, mode);
ValidationLogic.validateFlashloan(assets, amounts);
address[] memory aTokenAddresses = new address[](assets.length);
uint256[] memory premiums = new uint256[](assets.length);
vars.receiver = IFlashLoanReceiver(receiverAddress);
vars.debtMode = ReserveLogic.InterestRateMode(mode);
for (vars.i = 0; vars.i < assets.length; vars.i++) {
aTokenAddresses[vars.i] = _reserves[assets[vars.i]].aTokenAddress;
@ -555,10 +563,9 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
vars.currentAmount = amounts[vars.i];
vars.currentPremium = premiums[vars.i];
vars.currentATokenAddress = aTokenAddresses[vars.i];
vars.currentAmountPlusPremium = vars.currentAmount.add(vars.currentPremium);
if (vars.debtMode == ReserveLogic.InterestRateMode.NONE) {
if (ReserveLogic.InterestRateMode(modes[vars.i]) == ReserveLogic.InterestRateMode.NONE) {
_reserves[vars.currentAsset].updateState();
_reserves[vars.currentAsset].cumulateToLiquidityIndex(
IERC20(vars.currentATokenAddress).totalSupply(),
@ -578,13 +585,11 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
);
} else {
if (msg.sender != onBehalfOf) {
address debtToken = _reserves[vars.currentAsset].getDebtTokenAddress(mode);
vars.debtToken = _reserves[vars.currentAsset].getDebtTokenAddress(modes[vars.i]);
_borrowAllowance[debtToken][onBehalfOf][msg
.sender] = _borrowAllowance[debtToken][onBehalfOf][msg.sender].sub(
vars.currentAmount,
Errors.BORROW_ALLOWANCE_ARE_NOT_ENOUGH
);
_borrowAllowance[vars.debtToken][onBehalfOf][msg.sender] = _borrowAllowance[vars
.debtToken][onBehalfOf][msg.sender]
.sub(vars.currentAmount, Errors.BORROW_ALLOWANCE_ARE_NOT_ENOUGH);
}
//if the user didn't choose to return the funds, the system checks if there
@ -595,14 +600,21 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
msg.sender,
onBehalfOf,
vars.currentAmount,
mode,
modes[vars.i],
vars.currentATokenAddress,
referralCode,
false
)
);
}
emit FlashLoan(receiverAddress, mode, onBehalfOf, assets, amounts, premiums, referralCode);
emit FlashLoan(
receiverAddress,
msg.sender,
vars.currentAsset,
vars.currentAmount,
vars.currentPremium,
referralCode
);
}
}
@ -698,7 +710,13 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
* @param asset the address of the reserve
* @return the reserve normalized income
*/
function getReserveNormalizedIncome(address asset) external override view returns (uint256) {
function getReserveNormalizedIncome(address asset)
external
virtual
override
view
returns (uint256)
{
return _reserves[asset].getNormalizedIncome();
}
@ -882,6 +900,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
);
ValidationLogic.validateBorrow(
vars.asset,
reserve,
vars.onBehalfOf,
vars.amount,

18
contracts/lendingpool/LendingPoolConfigurator.sol
View File

@ -155,7 +155,11 @@ contract LendingPoolConfigurator is VersionedInitializable {
* @param proxy the aToken proxy address
* @param implementation the new aToken implementation
**/
event ATokenUpgraded(address indexed asset, address indexed proxy, address indexed implementation);
event ATokenUpgraded(
address indexed asset,
address indexed proxy,
address indexed implementation
);
/**
* @dev emitted when the implementation of a stable debt token is upgraded
@ -163,7 +167,11 @@ contract LendingPoolConfigurator is VersionedInitializable {
* @param proxy the stable debt token proxy address
* @param implementation the new aToken implementation
**/
event StableDebtTokenUpgraded(address indexed asset, address indexed proxy, address indexed implementation);
event StableDebtTokenUpgraded(
address indexed asset,
address indexed proxy,
address indexed implementation
);
/**
* @dev emitted when the implementation of a variable debt token is upgraded
@ -171,7 +179,11 @@ contract LendingPoolConfigurator is VersionedInitializable {
* @param proxy the variable debt token proxy address
* @param implementation the new aToken implementation
**/
event VariableDebtTokenUpgraded(address indexed asset, address indexed proxy, address indexed implementation);
event VariableDebtTokenUpgraded(
address indexed asset,
address indexed proxy,
address indexed implementation
);
ILendingPoolAddressesProvider internal addressesProvider;
ILendingPool internal pool;

2
contracts/libraries/helpers/Errors.sol
View File

@ -99,6 +99,8 @@ library Errors {
string public constant INVALID_DECIMALS = '73';
string public constant INVALID_RESERVE_FACTOR = '74';
// Credit delegation
string public constant INCONSISTENT_PARAMS_LENGTH = '75';
enum CollateralManagerErrors {
NO_ERROR,

19
contracts/libraries/logic/ValidationLogic.sol
View File

@ -33,7 +33,7 @@ library ValidationLogic {
* @param reserve the reserve state on which the user is depositing
* @param amount the amount to be deposited
*/
function validateDeposit(ReserveLogic.ReserveData storage reserve, uint256 amount) internal view {
function validateDeposit(ReserveLogic.ReserveData storage reserve, uint256 amount) external view {
(bool isActive, bool isFreezed, , ) = reserve.configuration.getFlags();
require(amount > 0, Errors.AMOUNT_NOT_GREATER_THAN_0);
@ -61,7 +61,7 @@ library ValidationLogic {
mapping(uint256 => address) storage reserves,
uint256 reservesCount,
address oracle
) internal view {
) external view {
require(amount > 0, Errors.AMOUNT_NOT_GREATER_THAN_0);
require(amount <= userBalance, Errors.NOT_ENOUGH_AVAILABLE_USER_BALANCE);
@ -104,6 +104,7 @@ library ValidationLogic {
/**
* @dev validates a borrow.
* @param asset the address of the asset to borrow
* @param reserve the reserve state from which the user is borrowing
* @param userAddress the address of the user
* @param amount the amount to be borrowed
@ -117,6 +118,7 @@ library ValidationLogic {
*/
function validateBorrow(
address asset,
ReserveLogic.ReserveData storage reserve,
address userAddress,
uint256 amount,
@ -203,6 +205,8 @@ library ValidationLogic {
Errors.CALLATERAL_SAME_AS_BORROWING_CURRENCY
);
vars.availableLiquidity = IERC20(asset).balanceOf(reserve.aTokenAddress);
//calculate the max available loan size in stable rate mode as a percentage of the
//available liquidity
uint256 maxLoanSizeStable = vars.availableLiquidity.percentMul(maxStableLoanPercent);
@ -283,8 +287,7 @@ library ValidationLogic {
require(
!userConfig.isUsingAsCollateral(reserve.id) ||
reserve.configuration.getLtv() == 0 ||
stableDebt.add(variableDebt) >
IERC20(reserve.aTokenAddress).balanceOf(msg.sender),
stableDebt.add(variableDebt) > IERC20(reserve.aTokenAddress).balanceOf(msg.sender),
Errors.CALLATERAL_SAME_AS_BORROWING_CURRENCY
);
} else {
@ -331,16 +334,10 @@ library ValidationLogic {
/**
* @dev validates a flashloan action
* @param mode the flashloan mode (0 = classic flashloan, 1 = open a stable rate loan, 2 = open a variable rate loan)
* @param assets the assets being flashborrowed
* @param amounts the amounts for each asset being borrowed
**/
function validateFlashloan(
address[] memory assets,
uint256[] memory amounts,
uint256 mode
) internal pure {
require(mode <= uint256(ReserveLogic.InterestRateMode.VARIABLE), Errors.INVALID_FLASHLOAN_MODE);
function validateFlashloan(address[] memory assets, uint256[] memory amounts) internal pure {
require(assets.length == amounts.length, Errors.INCONSISTENT_FLASHLOAN_PARAMS);
}

4
contracts/tokenization/StableDebtToken.sol
View File

@ -97,7 +97,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
address user,
uint256 amount,
uint256 rate
) external override onlyLendingPool returns(bool) {
) external override onlyLendingPool returns (bool) {
MintLocalVars memory vars;
//cumulates the user debt
@ -288,7 +288,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
* @param avgRate the average rate at which calculate the total supply
* @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();
if (principalSupply == 0) {

2
contracts/tokenization/interfaces/IStableDebtToken.sol
View File

@ -62,7 +62,7 @@ interface IStableDebtToken {
address user,
uint256 amount,
uint256 rate
) external returns(bool);
) external returns (bool);
/**
* @dev burns debt of the target user.

2
deployed-contracts.json
View File

@ -266,4 +266,4 @@
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
}
}
}
}

1
helpers/contracts-deployments.ts
View File

@ -140,7 +140,6 @@ export const deployAaveLibraries = async (
return {
['__$5201a97c05ba6aa659e2f36a933dd51801$__']: validationLogic.address,
['__$d3b4366daeb9cadc7528af6145b50b2183$__']: reserveLogic.address,
['__$4c26be947d349222af871a3168b3fe584b$__']: genericLogic.address,
};
};

1
runStableTokenCLI.sh Normal file
View File

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

1
runUserConfigCLI.sh Normal file
View File

@ -0,0 +1 @@
certoraRun specs/harness/UserConfigurationHarness.sol --solc solc6.8 --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging master

1
runVariableTokenCLI.sh Normal file
View File

@ -0,0 +1 @@
certoraRun contracts/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.8 --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic --cache VariableDebtToken --staging

155
specs/StableDebtToken.spec Normal file
View File

@ -0,0 +1,155 @@
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
totalSupply(t) = Σaddress u. balanceOf(u,t)
Check that each possible opertaion changes the balance of at most one user
*/
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);
calldataarg arg;
sinvoke f(e, arg);
uint256 balanceAAfter = sinvoke balanceOf(e,a);
uint256 balanceBAfter = sinvoke balanceOf(e,b);
assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
}
/**
Check that the change to total supply is coherent with the changes to balance
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
{
env e;
require sinvoke getIncentivesController(e) == 0;
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);
uint256 totalSupplyAfter = sinvoke totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/* 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 totalSupplyBefore = sinvoke totalSupply(e);
uint256 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
assert (totalSupplyAfter == 0 );
}
/**
Mint inceases the balanceOf user a as expected
*/
rule integrityMint(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke mint(e,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
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);
uint256 t = x + y;
sinvoke mint(e,a, t ,index) at initialStorage;
uint256 balanceScenario2 = sinvoke balanceOf(e,a);
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
rule integrityBurn(address a, uint256 x) {
env e;
require sinvoke getIncentivesController(e) == 0;
uint256 index;
uint256 balancebefore = sinvoke balanceOf(e,a);
sinvoke burn(e,a,x);
uint256 balanceAfter = sinvoke balanceOf(e,a);
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;
sinvoke burn(e, a, t) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "burn is not additive";
}
/**
mint and burn are inverse operations
Thus, totalSupply is back to initial state
BalanceOf user is back to initial state */
rule inverseMintBurn(address a, uint256 x) {
env e;
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";
}

66
specs/UserConfiguration.spec Normal file
View File

@ -0,0 +1,66 @@
methods {
setBorrowing(address, uint256, bool) envfree
setUsingAsCollateral(address, uint256, bool) envfree
isUsingAsCollateralOrBorrowing(address, uint256) returns bool envfree
isBorrowing(address, uint256) returns bool envfree
isUsingAsCollateral(address, uint256) returns bool envfree
isBorrowingAny(address ) returns bool envfree
isEmpty(address ) returns bool envfree
}
invariant empty(address user, uint256 reserveIndex )
isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex)
invariant notEmpty(address user, uint256 reserveIndex )
( isBorrowingAny(user) || isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user)
invariant borrowing(address user, uint256 reserveIndex )
isBorrowing(user, reserveIndex) => isBorrowingAny(user)
invariant collateralOrBorrowing(address user, uint256 reserveIndex )
( isUsingAsCollateral(user, reserveIndex) || isBorrowing(user, reserveIndex) ) <=> isUsingAsCollateralOrBorrowing(user, reserveIndex)
rule setBorrowing(address user, uint256 reserveIndex, bool borrowing)
{
require reserveIndex < 128;
setBorrowing(user, reserveIndex, borrowing);
assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result";
}
rule setBorrowingNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
setBorrowing(user, reserveIndex, borrowing);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
}
rule setUsingAsCollateral(address user, uint256 reserveIndex, bool usingAsCollateral)
{
require reserveIndex < 128;
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result";
}
rule setUsingAsCollateralNoChangeToOther(address user, uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral)
{
require reserveIndexOther != reserveIndex;
require reserveIndexOther < 128 && reserveIndex < 128;
bool otherReserveBorrowing = isBorrowing(user, reserveIndexOther);
bool otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther);
setUsingAsCollateral(user, reserveIndex, usingAsCollateral);
assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) &&
otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve";
}

173
specs/VariableDebtToken.spec Normal file
View File

@ -0,0 +1,173 @@
using LendingPoolHarnessForVariableDebtToken as POOL
/**
TotalSupply is the sum of all users’ balances
totalSupply(t) = Σaddress u. balanceOf(u,t)
Check that each possible opertaion changes the balance of at most one user
*/
rule balanceOfChange(address a, address b, method f)
{
env e;
require a!=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);
assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
}
/*
Check that the changed to total supply is coherent with the changes to balance
*/
rule integirtyBalanceOfTotalSupply(address a, method f )
{
env e;
uint256 balanceABefore = balanceOf(e, a);
uint256 totalSupplyBefore = totalSupply(e);
calldataarg arg;
sinvoke f(e, arg);
require (f.selector != burn(address, uint256, uint256).selector &&
f.selector != mint(address, uint256, uint256).selector ) ;
uint256 balanceAAfter = balanceOf(e, a);
uint256 totalSupplyAfter = totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/* Burn behaves deferently and due to accumulation errors might hace less total supply then the balance
*/
rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
{
env e;
uint256 balanceABefore = balanceOf(e, a);
uint256 totalSupplyBefore = totalSupply(e);
uint256 x;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
sinvoke burn(e, a, x, index);
uint256 balanceAAfter = balanceOf(e, a);
uint256 totalSupplyAfter = totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
rule integirtyBalanceOfTotalSupplyOnMint(address a, method f )
{
env e;
uint256 balanceABefore = balanceOf(e, a);
uint256 totalSupplyBefore = totalSupply(e);
uint256 x;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
sinvoke mint(e, a, x, index);
uint256 balanceAAfter = balanceOf(e, a);
uint256 totalSupplyAfter = totalSupply(e);
assert (balanceAAfter != balanceABefore => ( balanceAAfter - balanceABefore == totalSupplyAfter - totalSupplyBefore));
}
/**
Minting an amount of x tokens for user u increases their balance by x, up to rounding errors.
{ b= balanceOf(u,t) }
mint(u,x,index)
{ balanceOf(u,t) = b + x }
*/
rule integrityMint(address a, uint256 x) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e,asset);
uint256 balancebefore = balanceOf(e, a);
sinvoke mint(e, a, x, index);
uint256 balanceAfter = 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
*/
rule additiveMint(address a, uint256 x, uint256 y) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
storage initialStorage = lastStorage;
sinvoke mint(e, a, x, index);
sinvoke mint(e, a, y, index);
uint256 balanceScenario1 = balanceOf(e, a);
uint t = x + y;
sinvoke mint(e, a, t ,index) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "mint is not additive";
}
/**
Transfer of x amount of tokens from user u where receiver is user u’
{bu = balanceOf(u) }
burn(u, u’, x)
{balanceOf(u) = bu - x }
*/
rule integrityBurn(address a, uint256 x) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
uint256 balancebefore = balanceOf(e, a);
sinvoke burn(e, a, x, index);
uint256 balanceAfter = balanceOf(e, a);
assert balanceAfter == balancebefore - x;
}
/**
Minting is additive, i.e., it can be performed either all at once or in steps.
burn(u, u’, x); burn(u, u’, y) ~ burn(u, u’, x+y)
*/
rule additiveBurn(address a, uint256 x, uint256 y) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
storage initialStorage = lastStorage;
sinvoke burn(e, a, x, index);
sinvoke burn(e, a, y, index);
uint256 balanceScenario1 = balanceOf(e, a);
uint t = x + y;
sinvoke burn(e, a, t ,index) at initialStorage;
uint256 balanceScenario2 = balanceOf(e, a);
assert balanceScenario1 == balanceScenario2, "burn is not additive";
}
/**
Minting and burning are inverse operations.
{bu = balanceOf(u) }
mint(u,x); burn(u, u, x)
{balanceOf(u) = bu }
*/
rule inverseMintBurn(address a, uint256 x) {
env e;
address asset;
uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
uint256 balancebefore = balanceOf(e, a);
sinvoke mint(e, a, x, index);
sinvoke burn(e, a, x, index);
uint256 balanceAfter = balanceOf(e, a);
assert balancebefore == balanceAfter, "burn is not inverse of mint";
}

214
specs/harness/LendingPoolHarnessForVariableDebtToken.sol Normal file
View File

@ -0,0 +1,214 @@
pragma solidity ^0.6.8;
pragma experimental ABIEncoderV2;
import {
ReserveConfiguration
} from '../../contracts/libraries/configuration/ReserveConfiguration.sol';
import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
import {ReserveLogic} from '../../contracts/libraries/logic/ReserveLogic.sol';
import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
/*
Certora: Harness that delegates calls to the original LendingPool.
Used for the verification of the VariableDebtToken contract.
*/
contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
LendingPool private originalPool;
function deposit(
address asset,
uint256 amount,
address onBehalfOf,
uint16 referralCode
) external override {
originalPool.deposit(asset, amount, onBehalfOf, referralCode);
}
function withdraw(address asset, uint256 amount) external override {
originalPool.withdraw(asset, amount);
}
function getBorrowAllowance(
address fromUser,
address toUser,
address asset,
uint256 interestRateMode
) external override view returns (uint256) {
return originalPool.getBorrowAllowance(fromUser, toUser, asset, interestRateMode);
}
function delegateBorrowAllowance(
address asset,
address user,
uint256 interestRateMode,
uint256 amount
) external override {
originalPool.delegateBorrowAllowance(asset, user, interestRateMode, amount);
}
function borrow(
address asset,
uint256 amount,
uint256 interestRateMode,
uint16 referralCode,
address onBehalfOf
) external override {
originalPool.borrow(asset, amount, interestRateMode, referralCode, onBehalfOf);
}
function repay(
address asset,
uint256 amount,
uint256 rateMode,
address onBehalfOf
) external override {
originalPool.repay(asset, amount, rateMode, onBehalfOf);
}
function swapBorrowRateMode(address asset, uint256 rateMode) external override {
originalPool.swapBorrowRateMode(asset, rateMode);
}
function rebalanceStableBorrowRate(address asset, address user) external override {
originalPool.rebalanceStableBorrowRate(asset, user);
}
function setUserUseReserveAsCollateral(address asset, bool useAsCollateral) external override {
originalPool.setUserUseReserveAsCollateral(asset, useAsCollateral);
}
function liquidationCall(
address collateral,
address asset,
address user,
uint256 purchaseAmount,
bool receiveAToken
) external override {
originalPool.liquidationCall(collateral, asset, user, purchaseAmount, receiveAToken);
}
function getReservesList() external override view returns (address[] memory) {
return originalPool.getReservesList();
}
function getReserveData(address asset)
external
override
view
returns (ReserveLogic.ReserveData memory)
{
return originalPool.getReserveData(asset);
}
function getUserConfiguration(address user)
external
override
view
returns (UserConfiguration.Map memory)
{
return originalPool.getUserConfiguration(user);
}
function getUserAccountData(address user)
external
override
view
returns (
uint256 totalCollateralETH,
uint256 totalBorrowsETH,
uint256 availableBorrowsETH,
uint256 currentLiquidationThreshold,
uint256 ltv,
uint256 healthFactor
)
{
return originalPool.getUserAccountData(user);
}
function initReserve(
address asset,
address aTokenAddress,
address stableDebtAddress,
address variableDebtAddress,
address interestRateStrategyAddress
) external override {
originalPool.initReserve(
asset,
aTokenAddress,
stableDebtAddress,
variableDebtAddress,
interestRateStrategyAddress
);
}
function setReserveInterestRateStrategyAddress(address asset, address rateStrategyAddress)
external
override
{
originalPool.setReserveInterestRateStrategyAddress(asset, rateStrategyAddress);
}
function setConfiguration(address asset, uint256 configuration) external override {
originalPool.setConfiguration(asset, configuration);
}
function getConfiguration(address asset)
external
override
view
returns (ReserveConfiguration.Map memory)
{
return originalPool.getConfiguration(asset);
}
mapping(uint256 => uint256) private reserveNormalizedIncome;
function getReserveNormalizedIncome(address asset) external override view returns (uint256) {
require(reserveNormalizedIncome[block.timestamp] == 1e27);
return reserveNormalizedIncome[block.timestamp];
}
mapping(uint256 => uint256) private reserveNormalizedVariableDebt;
function getReserveNormalizedVariableDebt(address asset)
external
override
view
returns (uint256)
{
require(reserveNormalizedVariableDebt[block.timestamp] == 1e27);
return reserveNormalizedVariableDebt[block.timestamp];
}
function setPause(bool val) external override {
originalPool.setPause(val);
}
function paused() external override view returns (bool) {
return originalPool.paused();
}
function flashLoan(
address receiver,
address[] calldata assets,
uint256[] calldata amounts,
uint256 mode,
address onBehalfOf,
bytes calldata params,
uint16 referralCode
) external override {
originalPool.flashLoan(receiver, assets, amounts, mode, onBehalfOf, params, referralCode);
}
function finalizeTransfer(
address asset,
address from,
address to,
uint256 amount,
uint256 balanceFromAfter,
uint256 balanceToBefore
) external override {
originalPool.finalizeTransfer(asset, from, to, amount, balanceFromAfter, balanceToBefore);
}
}

26
specs/harness/StableDebtTokenHarness.sol Normal file
View File

@ -0,0 +1,26 @@
pragma solidity ^0.6.8;
import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';
contract StableDebtTokenHarness is StableDebtToken {
constructor(
address pool,
address underlyingAsset,
string memory name,
string memory symbol,
address incentivesController
) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
function balanceOf(address account) public override view returns (uint256) {
return IncentivizedERC20.balanceOf(account);
}
function _calcTotalSupply(uint256 avgRate) internal override view returns (uint256) {
return IncentivizedERC20.totalSupply();
}
function getIncentivesController() public view returns (address) {
return address(_incentivesController);
}
}

56
specs/harness/UserConfigurationHarness.sol Normal file
View File

@ -0,0 +1,56 @@
pragma solidity ^0.6.8;
pragma experimental ABIEncoderV2;
import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
/*
A wrapper contract for calling functions from the library UserConfiguration.
*/
contract UserConfigurationHarness {
UserConfiguration.Map internal usersConfig;
function setBorrowing(
address user,
uint256 reserveIndex,
bool borrowing
) public {
UserConfiguration.setBorrowing(usersConfig, reserveIndex, borrowing);
}
function setUsingAsCollateral(
address user,
uint256 reserveIndex,
bool _usingAsCollateral
) public {
UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral);
}
function isUsingAsCollateralOrBorrowing(address user, uint256 reserveIndex)
public
view
returns (bool)
{
return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex);
}
function isBorrowing(address user, uint256 reserveIndex) public view returns (bool) {
return UserConfiguration.isBorrowing(usersConfig, reserveIndex);
}
function isUsingAsCollateral(address user, uint256 reserveIndex) public view returns (bool) {
return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex);
}
function isBorrowingAny(address user) public view returns (bool) {
return UserConfiguration.isBorrowingAny(usersConfig);
}
function isEmpty(address user) public view returns (bool) {
return UserConfiguration.isEmpty(usersConfig);
}
/*
Mimics the original constructor of the contract.
*/
function init_state() public {}
}

14
test/atoken-transfer.spec.ts
View File

@ -71,8 +71,11 @@ makeSuite('AToken: Transfer', (testEnv: TestEnv) => {
users[1].address
);
const userReserveData = await helpersContract.getUserReserveData(weth.address, users[1].address);
const userReserveData = await helpersContract.getUserReserveData(
weth.address,
users[1].address
);
expect(userReserveData.currentStableDebt.toString()).to.be.eq(ethers.utils.parseEther('0.1'));
});
@ -80,7 +83,7 @@ makeSuite('AToken: Transfer', (testEnv: TestEnv) => {
const {users, pool, aDai, dai, weth} = testEnv;
const aDAItoTransfer = await convertToCurrencyDecimals(dai.address, '1000');
await expect(
aDai.connect(users[1].signer).transfer(users[0].address, aDAItoTransfer),
TRANSFER_NOT_ALLOWED
@ -88,15 +91,14 @@ makeSuite('AToken: Transfer', (testEnv: TestEnv) => {
});
it('User 1 tries to transfer a small amount of DAI used as collateral back to user 0', async () => {
const {users, pool, aDai, dai, weth} = testEnv;
const aDAItoTransfer = await convertToCurrencyDecimals(dai.address, '100');
await aDai.connect(users[1].signer).transfer(users[0].address, aDAItoTransfer);
const user0Balance = await aDai.balanceOf(users[0].address);
expect(user0Balance.toString()).to.be.eq(aDAItoTransfer.toString());
});
});
});

50
test/flashloan.spec.ts
View File

@ -48,7 +48,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[ethers.utils.parseEther('0.8')],
0,
[0],
_mockFlashLoanReceiver.address,
'0x10',
'0'
@ -78,7 +78,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
['1000720000000000000'],
0,
[0],
_mockFlashLoanReceiver.address,
'0x10',
'0'
@ -110,7 +110,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[ethers.utils.parseEther('0.8')],
0,
[0],
caller.address,
'0x10',
'0'
@ -131,7 +131,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[ethers.utils.parseEther('0.8')],
0,
[0],
caller.address,
'0x10',
'0'
@ -152,12 +152,12 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[ethers.utils.parseEther('0.8')],
4,
[4],
caller.address,
'0x10',
'0'
)
).to.be.revertedWith(INVALID_FLASHLOAN_MODE);
).to.be.reverted;
});
it('Caller deposits 1000 DAI as collateral, Takes WETH flashloan with mode = 2, does not return the funds. A variable loan for caller is created', async () => {
@ -181,7 +181,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[ethers.utils.parseEther('0.8')],
2,
[2],
caller.address,
'0x10',
'0'
@ -209,7 +209,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
['1004415000000000000'], //slightly higher than the available liquidity
2,
[2],
caller.address,
'0x10',
'0'
@ -223,7 +223,15 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
const caller = users[1];
await expect(
pool.flashLoan(deployer.address, [weth.address], ['1000000000000000000'], 2, caller.address, '0x10', '0')
pool.flashLoan(
deployer.address,
[weth.address],
['1000000000000000000'],
[2],
caller.address,
'0x10',
'0'
)
).to.be.reverted;
});
@ -251,7 +259,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[usdc.address],
[flashloanAmount],
0,
[0],
_mockFlashLoanReceiver.address,
'0x10',
'0'
@ -294,7 +302,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[usdc.address],
[flashloanAmount],
2,
[2],
caller.address,
'0x10',
'0'
@ -321,7 +329,15 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
await pool
.connect(caller.signer)
.flashLoan(_mockFlashLoanReceiver.address, [usdc.address], [flashloanAmount], 2, caller.address, '0x10', '0');
.flashLoan(
_mockFlashLoanReceiver.address,
[usdc.address],
[flashloanAmount],
[2],
caller.address,
'0x10',
'0'
);
const {variableDebtTokenAddress} = await helpersContract.getReserveTokensAddresses(
usdc.address
);
@ -360,7 +376,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[flashAmount],
0,
[0],
caller.address,
'0x10',
'0'
@ -383,7 +399,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[flashAmount],
1,
[1],
caller.address,
'0x10',
'0'
@ -429,7 +445,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[flashAmount],
1,
[1],
onBehalfOf.address,
'0x10',
'0'
@ -448,7 +464,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
// Deposited for onBehalfOf user already, delegate borrow allowance
await pool
.connect(onBehalfOf.signer)
.delegateBorrowAllowance(weth.address, caller.address, 1, flashAmount);
.delegateBorrowAllowance([weth.address], caller.address, [1], [flashAmount]);
await _mockFlashLoanReceiver.setFailExecutionTransfer(true);
@ -458,7 +474,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[flashAmount],
1,
[1],
onBehalfOf.address,
'0x10',
'0'

30
test/helpers/actions.ts
View File

@ -277,9 +277,9 @@ export const withdraw = async (
};
export const delegateBorrowAllowance = async (
reserveSymbol: string,
amount: string,
interestRateMode: string,
reserveSymbols: string[],
amounts: string[],
interestRateModes: string[],
user: SignerWithAddress,
receiver: tEthereumAddress,
expectedResult: string,
@ -288,20 +288,32 @@ export const delegateBorrowAllowance = async (
) => {
const {pool} = testEnv;
const reserve = await getReserveAddressFromSymbol(reserveSymbol);
const amountToDelegate = await convertToCurrencyDecimals(reserve, amount);
const reserves: tEthereumAddress[] = [];
const amountsToDelegate: tEthereumAddress[] = [];
for (const reserveSymbol of reserveSymbols) {
const newLength = reserves.push(await getReserveAddressFromSymbol(reserveSymbol));
amountsToDelegate.push(
await (
await convertToCurrencyDecimals(reserves[newLength - 1], amounts[newLength - 1])
).toString()
);
}
const delegateAllowancePromise = pool
.connect(user.signer)
.delegateBorrowAllowance(reserve, receiver, interestRateMode, amountToDelegate.toString());
.delegateBorrowAllowance(reserves, receiver, interestRateModes, amountsToDelegate);
if (expectedResult === 'revert') {
await expect(delegateAllowancePromise, revertMessage).to.be.reverted;
return;
} else {
await delegateAllowancePromise;
expect(
(await pool.getBorrowAllowance(user.address, receiver, reserve, interestRateMode)).toString()
).to.be.equal(amountToDelegate.toString(), 'borrowAllowance are set incorrectly');
for (const [i, reserve] of reserves.entries()) {
expect(
(
await pool.getBorrowAllowance(user.address, receiver, reserve, interestRateModes[i])
).toString()
).to.be.equal(amountsToDelegate[i], 'borrowAllowance are set incorrectly');
}
}
};

6
test/helpers/scenario-engine.ts
View File

@ -121,9 +121,9 @@ const executeAction = async (action: Action, users: SignerWithAddress[], testEnv
}
await delegateBorrowAllowance(
reserve,
amount,
rateMode,
[reserve],
[amount],
[rateMode],
user,
toUser,
expected,

4
test/pausable-functions.spec.ts
View File

@ -133,7 +133,7 @@ makeSuite('Pausable Pool', (testEnv: TestEnv) => {
// Try to execute liquidation
await expect(
pool.connect(user.signer).delegateBorrowAllowance(dai.address, toUser.address, '1', '1')
pool.connect(user.signer).delegateBorrowAllowance([dai.address], toUser.address, ['1'], ['1'])
).revertedWith(IS_PAUSED);
// Unpause the pool
@ -191,7 +191,7 @@ makeSuite('Pausable Pool', (testEnv: TestEnv) => {
_mockFlashLoanReceiver.address,
[weth.address],
[flashAmount],
1,
[1],
caller.address,
'0x10',
'0'