mirror of
https://github.com/Instadapp/aave-protocol-v2.git
synced 2024-07-29 21:47:30 +00:00
Merge branch 'master' into feat/uniswap-adapter-flashloan
This commit is contained in:
commit
8278d2e6d8
|
@ -19,16 +19,11 @@ contract LendingPoolAddressesProvider is Ownable, ILendingPoolAddressesProvider
|
||||||
mapping(bytes32 => address) private _addresses;
|
mapping(bytes32 => address) private _addresses;
|
||||||
|
|
||||||
bytes32 private constant LENDING_POOL = 'LENDING_POOL';
|
bytes32 private constant LENDING_POOL = 'LENDING_POOL';
|
||||||
bytes32 private constant LENDING_POOL_CORE = 'LENDING_POOL_CORE';
|
|
||||||
bytes32 private constant LENDING_POOL_CONFIGURATOR = 'LENDING_POOL_CONFIGURATOR';
|
bytes32 private constant LENDING_POOL_CONFIGURATOR = 'LENDING_POOL_CONFIGURATOR';
|
||||||
bytes32 private constant AAVE_ADMIN = 'AAVE_ADMIN';
|
bytes32 private constant AAVE_ADMIN = 'AAVE_ADMIN';
|
||||||
bytes32 private constant LENDING_POOL_COLLATERAL_MANAGER = 'COLLATERAL_MANAGER';
|
bytes32 private constant LENDING_POOL_COLLATERAL_MANAGER = 'COLLATERAL_MANAGER';
|
||||||
bytes32 private constant LENDING_POOL_FLASHLOAN_PROVIDER = 'FLASHLOAN_PROVIDER';
|
|
||||||
bytes32 private constant DATA_PROVIDER = 'DATA_PROVIDER';
|
|
||||||
bytes32 private constant ETHEREUM_ADDRESS = 'ETHEREUM_ADDRESS';
|
|
||||||
bytes32 private constant PRICE_ORACLE = 'PRICE_ORACLE';
|
bytes32 private constant PRICE_ORACLE = 'PRICE_ORACLE';
|
||||||
bytes32 private constant LENDING_RATE_ORACLE = 'LENDING_RATE_ORACLE';
|
bytes32 private constant LENDING_RATE_ORACLE = 'LENDING_RATE_ORACLE';
|
||||||
bytes32 private constant WALLET_BALANCE_PROVIDER = 'WALLET_BALANCE_PROVIDER';
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev Sets an address for an id, allowing to cover it or not with a proxy
|
* @dev Sets an address for an id, allowing to cover it or not with a proxy
|
||||||
|
|
|
@ -12,6 +12,7 @@ interface IFlashLoanReceiver {
|
||||||
address[] calldata assets,
|
address[] calldata assets,
|
||||||
uint256[] calldata amounts,
|
uint256[] calldata amounts,
|
||||||
uint256[] calldata premiums,
|
uint256[] calldata premiums,
|
||||||
|
address initiator,
|
||||||
bytes calldata params
|
bytes calldata params
|
||||||
) external returns (bool);
|
) external returns (bool);
|
||||||
}
|
}
|
||||||
|
|
|
@ -27,9 +27,10 @@ interface ILendingPool {
|
||||||
* @dev emitted during a withdraw action.
|
* @dev emitted during a withdraw action.
|
||||||
* @param reserve the address of the reserve
|
* @param reserve the address of the reserve
|
||||||
* @param user the address of the user
|
* @param user the address of the user
|
||||||
|
* @param to address that will receive the underlying
|
||||||
* @param amount the amount to be withdrawn
|
* @param amount the amount to be withdrawn
|
||||||
**/
|
**/
|
||||||
event Withdraw(address indexed reserve, address indexed user, uint256 amount);
|
event Withdraw(address indexed reserve, address indexed user, address indexed to, uint256 amount);
|
||||||
|
|
||||||
event BorrowAllowanceDelegated(
|
event BorrowAllowanceDelegated(
|
||||||
address indexed asset,
|
address indexed asset,
|
||||||
|
@ -74,7 +75,7 @@ interface ILendingPool {
|
||||||
* @param reserve the address of the reserve
|
* @param reserve the address of the reserve
|
||||||
* @param user the address of the user executing the swap
|
* @param user the address of the user executing the swap
|
||||||
**/
|
**/
|
||||||
event Swap(address indexed reserve, address indexed user);
|
event Swap(address indexed reserve, address indexed user, uint256 rateMode);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when a user enables a reserve as collateral
|
* @dev emitted when a user enables a reserve as collateral
|
||||||
|
@ -99,20 +100,18 @@ interface ILendingPool {
|
||||||
/**
|
/**
|
||||||
* @dev emitted when a flashloan is executed
|
* @dev emitted when a flashloan is executed
|
||||||
* @param target the address of the flashLoanReceiver
|
* @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 initiator the address initiating the flash loan
|
||||||
* @param onBehalfOf the address incurring the debt, if borrow mode is not 0
|
* @param asset the address of the asset being flashborrowed
|
||||||
* @param assets the address of the assets being flashborrowed
|
* @param amount the amount requested
|
||||||
* @param amounts the amount requested
|
* @param premium the total fee on the amount
|
||||||
* @param premiums the total fee on the amount
|
|
||||||
* @param referralCode the referral code of the caller
|
* @param referralCode the referral code of the caller
|
||||||
**/
|
**/
|
||||||
event FlashLoan(
|
event FlashLoan(
|
||||||
address indexed target,
|
address indexed target,
|
||||||
uint256 mode,
|
address indexed initiator,
|
||||||
address indexed onBehalfOf,
|
address indexed asset,
|
||||||
address[] assets,
|
uint256 amount,
|
||||||
uint256[] amounts,
|
uint256 premium,
|
||||||
uint256[] premiums,
|
|
||||||
uint16 referralCode
|
uint16 referralCode
|
||||||
);
|
);
|
||||||
|
|
||||||
|
@ -188,8 +187,13 @@ interface ILendingPool {
|
||||||
* @dev withdraws the assets of user.
|
* @dev withdraws the assets of user.
|
||||||
* @param reserve the address of the reserve
|
* @param reserve the address of the reserve
|
||||||
* @param amount the underlying amount to be redeemed
|
* @param amount the underlying amount to be redeemed
|
||||||
|
* @param to address that will receive the underlying
|
||||||
**/
|
**/
|
||||||
function withdraw(address reserve, uint256 amount) external;
|
function withdraw(
|
||||||
|
address reserve,
|
||||||
|
uint256 amount,
|
||||||
|
address to
|
||||||
|
) external;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev Sets allowance to borrow on a certain type of debt asset for a certain user address
|
* @dev Sets allowance to borrow on a certain type of debt asset for a certain user address
|
||||||
|
@ -289,7 +293,7 @@ interface ILendingPool {
|
||||||
* @param receiver The address of the contract receiving the funds. The receiver should implement the IFlashLoanReceiver interface.
|
* @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 assets the address of the principal reserve
|
||||||
* @param amounts the amount requested for this flashloan
|
* @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 params a bytes array to be sent to the flashloan executor
|
||||||
* @param referralCode the referral code of the caller
|
* @param referralCode the referral code of the caller
|
||||||
**/
|
**/
|
||||||
|
@ -297,7 +301,7 @@ interface ILendingPool {
|
||||||
address receiver,
|
address receiver,
|
||||||
address[] calldata assets,
|
address[] calldata assets,
|
||||||
uint256[] calldata amounts,
|
uint256[] calldata amounts,
|
||||||
uint256 mode,
|
uint256[] calldata modes,
|
||||||
address onBehalfOf,
|
address onBehalfOf,
|
||||||
bytes calldata params,
|
bytes calldata params,
|
||||||
uint16 referralCode
|
uint16 referralCode
|
||||||
|
|
|
@ -1,20 +0,0 @@
|
||||||
// SPDX-License-Identifier: agpl-3.0
|
|
||||||
pragma solidity ^0.6.8;
|
|
||||||
|
|
||||||
interface ISwapAdapter {
|
|
||||||
/**
|
|
||||||
* @dev Swaps an `amountToSwap` of an asset to another, approving a `fundsDestination` to pull the funds
|
|
||||||
* @param assetToSwapFrom Origin asset
|
|
||||||
* @param assetToSwapTo Destination asset
|
|
||||||
* @param amountToSwap How much `assetToSwapFrom` needs to be swapped
|
|
||||||
* @param fundsDestination Address that will be pulling the swapped funds
|
|
||||||
* @param params Additional variadic field to include extra params
|
|
||||||
*/
|
|
||||||
function executeOperation(
|
|
||||||
address assetToSwapFrom,
|
|
||||||
address assetToSwapTo,
|
|
||||||
uint256 amountToSwap,
|
|
||||||
address fundsDestination,
|
|
||||||
bytes calldata params
|
|
||||||
) external;
|
|
||||||
}
|
|
|
@ -20,7 +20,6 @@ import {IStableDebtToken} from '../tokenization/interfaces/IStableDebtToken.sol'
|
||||||
import {IVariableDebtToken} from '../tokenization/interfaces/IVariableDebtToken.sol';
|
import {IVariableDebtToken} from '../tokenization/interfaces/IVariableDebtToken.sol';
|
||||||
import {DebtTokenBase} from '../tokenization/base/DebtTokenBase.sol';
|
import {DebtTokenBase} from '../tokenization/base/DebtTokenBase.sol';
|
||||||
import {IFlashLoanReceiver} from '../flashloan/interfaces/IFlashLoanReceiver.sol';
|
import {IFlashLoanReceiver} from '../flashloan/interfaces/IFlashLoanReceiver.sol';
|
||||||
import {ISwapAdapter} from '../interfaces/ISwapAdapter.sol';
|
|
||||||
import {LendingPoolCollateralManager} from './LendingPoolCollateralManager.sol';
|
import {LendingPoolCollateralManager} from './LendingPoolCollateralManager.sol';
|
||||||
import {IPriceOracleGetter} from '../interfaces/IPriceOracleGetter.sol';
|
import {IPriceOracleGetter} from '../interfaces/IPriceOracleGetter.sol';
|
||||||
import {SafeERC20} from '../dependencies/openzeppelin/contracts/SafeERC20.sol';
|
import {SafeERC20} from '../dependencies/openzeppelin/contracts/SafeERC20.sol';
|
||||||
|
@ -120,8 +119,13 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
* @dev withdraws the _reserves of user.
|
* @dev withdraws the _reserves of user.
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param amount the underlying amount to be redeemed
|
* @param amount the underlying amount to be redeemed
|
||||||
|
* @param to address that will receive the underlying
|
||||||
**/
|
**/
|
||||||
function withdraw(address asset, uint256 amount) external override {
|
function withdraw(
|
||||||
|
address asset,
|
||||||
|
uint256 amount,
|
||||||
|
address to
|
||||||
|
) external override {
|
||||||
_whenNotPaused();
|
_whenNotPaused();
|
||||||
ReserveLogic.ReserveData storage reserve = _reserves[asset];
|
ReserveLogic.ReserveData storage reserve = _reserves[asset];
|
||||||
|
|
||||||
|
@ -155,9 +159,9 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
_usersConfig[msg.sender].setUsingAsCollateral(reserve.id, false);
|
_usersConfig[msg.sender].setUsingAsCollateral(reserve.id, false);
|
||||||
}
|
}
|
||||||
|
|
||||||
IAToken(aToken).burn(msg.sender, msg.sender, amountToWithdraw, reserve.liquidityIndex);
|
IAToken(aToken).burn(msg.sender, to, amountToWithdraw, reserve.liquidityIndex);
|
||||||
|
|
||||||
emit Withdraw(asset, msg.sender, amountToWithdraw);
|
emit Withdraw(asset, msg.sender, to, amountToWithdraw);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -352,7 +356,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
|
|
||||||
reserve.updateInterestRates(asset, reserve.aTokenAddress, 0, 0);
|
reserve.updateInterestRates(asset, reserve.aTokenAddress, 0, 0);
|
||||||
|
|
||||||
emit Swap(asset, msg.sender);
|
emit Swap(asset, msg.sender, rateMode);
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -486,13 +490,13 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
struct FlashLoanLocalVars {
|
struct FlashLoanLocalVars {
|
||||||
IFlashLoanReceiver receiver;
|
IFlashLoanReceiver receiver;
|
||||||
address oracle;
|
address oracle;
|
||||||
ReserveLogic.InterestRateMode debtMode;
|
|
||||||
uint256 i;
|
uint256 i;
|
||||||
address currentAsset;
|
address currentAsset;
|
||||||
address currentATokenAddress;
|
address currentATokenAddress;
|
||||||
uint256 currentAmount;
|
uint256 currentAmount;
|
||||||
uint256 currentPremium;
|
uint256 currentPremium;
|
||||||
uint256 currentAmountPlusPremium;
|
uint256 currentAmountPlusPremium;
|
||||||
|
address debtToken;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -502,7 +506,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 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 assets The addresss of the assets being flashborrowed
|
||||||
* @param amounts The amounts requested for this flashloan for each asset
|
* @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 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 params Variadic packed params to pass to the receiver as extra information
|
||||||
* @param referralCode Referral code of the flash loan
|
* @param referralCode Referral code of the flash loan
|
||||||
|
@ -511,7 +515,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
address receiverAddress,
|
address receiverAddress,
|
||||||
address[] calldata assets,
|
address[] calldata assets,
|
||||||
uint256[] calldata amounts,
|
uint256[] calldata amounts,
|
||||||
uint256 mode,
|
uint256[] calldata modes,
|
||||||
address onBehalfOf,
|
address onBehalfOf,
|
||||||
bytes calldata params,
|
bytes calldata params,
|
||||||
uint16 referralCode
|
uint16 referralCode
|
||||||
|
@ -520,13 +524,12 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
|
|
||||||
FlashLoanLocalVars memory vars;
|
FlashLoanLocalVars memory vars;
|
||||||
|
|
||||||
ValidationLogic.validateFlashloan(assets, amounts, mode);
|
ValidationLogic.validateFlashloan(assets, amounts);
|
||||||
|
|
||||||
address[] memory aTokenAddresses = new address[](assets.length);
|
address[] memory aTokenAddresses = new address[](assets.length);
|
||||||
uint256[] memory premiums = new uint256[](assets.length);
|
uint256[] memory premiums = new uint256[](assets.length);
|
||||||
|
|
||||||
vars.receiver = IFlashLoanReceiver(receiverAddress);
|
vars.receiver = IFlashLoanReceiver(receiverAddress);
|
||||||
vars.debtMode = ReserveLogic.InterestRateMode(mode);
|
|
||||||
|
|
||||||
for (vars.i = 0; vars.i < assets.length; vars.i++) {
|
for (vars.i = 0; vars.i < assets.length; vars.i++) {
|
||||||
aTokenAddresses[vars.i] = _reserves[assets[vars.i]].aTokenAddress;
|
aTokenAddresses[vars.i] = _reserves[assets[vars.i]].aTokenAddress;
|
||||||
|
@ -539,7 +542,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
|
|
||||||
//execute action of the receiver
|
//execute action of the receiver
|
||||||
require(
|
require(
|
||||||
vars.receiver.executeOperation(assets, amounts, premiums, params),
|
vars.receiver.executeOperation(assets, amounts, premiums, msg.sender, params),
|
||||||
Errors.INVALID_FLASH_LOAN_EXECUTOR_RETURN
|
Errors.INVALID_FLASH_LOAN_EXECUTOR_RETURN
|
||||||
);
|
);
|
||||||
|
|
||||||
|
@ -548,10 +551,9 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
vars.currentAmount = amounts[vars.i];
|
vars.currentAmount = amounts[vars.i];
|
||||||
vars.currentPremium = premiums[vars.i];
|
vars.currentPremium = premiums[vars.i];
|
||||||
vars.currentATokenAddress = aTokenAddresses[vars.i];
|
vars.currentATokenAddress = aTokenAddresses[vars.i];
|
||||||
|
|
||||||
vars.currentAmountPlusPremium = vars.currentAmount.add(vars.currentPremium);
|
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].updateState();
|
||||||
_reserves[vars.currentAsset].cumulateToLiquidityIndex(
|
_reserves[vars.currentAsset].cumulateToLiquidityIndex(
|
||||||
IERC20(vars.currentATokenAddress).totalSupply(),
|
IERC20(vars.currentATokenAddress).totalSupply(),
|
||||||
|
@ -571,13 +573,11 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
);
|
);
|
||||||
} else {
|
} else {
|
||||||
if (msg.sender != onBehalfOf) {
|
if (msg.sender != onBehalfOf) {
|
||||||
address debtToken = _reserves[vars.currentAsset].getDebtTokenAddress(mode);
|
vars.debtToken = _reserves[vars.currentAsset].getDebtTokenAddress(modes[vars.i]);
|
||||||
|
|
||||||
_borrowAllowance[debtToken][onBehalfOf][msg
|
_borrowAllowance[vars.debtToken][onBehalfOf][msg.sender] = _borrowAllowance[vars
|
||||||
.sender] = _borrowAllowance[debtToken][onBehalfOf][msg.sender].sub(
|
.debtToken][onBehalfOf][msg.sender]
|
||||||
vars.currentAmount,
|
.sub(vars.currentAmount, Errors.BORROW_ALLOWANCE_ARE_NOT_ENOUGH);
|
||||||
Errors.BORROW_ALLOWANCE_ARE_NOT_ENOUGH
|
|
||||||
);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
//if the user didn't choose to return the funds, the system checks if there
|
//if the user didn't choose to return the funds, the system checks if there
|
||||||
|
@ -588,14 +588,21 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
msg.sender,
|
msg.sender,
|
||||||
onBehalfOf,
|
onBehalfOf,
|
||||||
vars.currentAmount,
|
vars.currentAmount,
|
||||||
mode,
|
modes[vars.i],
|
||||||
vars.currentATokenAddress,
|
vars.currentATokenAddress,
|
||||||
referralCode,
|
referralCode,
|
||||||
false
|
false
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
emit FlashLoan(receiverAddress, mode, onBehalfOf, assets, amounts, premiums, referralCode);
|
emit FlashLoan(
|
||||||
|
receiverAddress,
|
||||||
|
msg.sender,
|
||||||
|
vars.currentAsset,
|
||||||
|
vars.currentAmount,
|
||||||
|
vars.currentPremium,
|
||||||
|
referralCode
|
||||||
|
);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -691,7 +698,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @return the reserve normalized income
|
* @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();
|
return _reserves[asset].getNormalizedIncome();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -875,6 +882,7 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
);
|
);
|
||||||
|
|
||||||
ValidationLogic.validateBorrow(
|
ValidationLogic.validateBorrow(
|
||||||
|
vars.asset,
|
||||||
reserve,
|
reserve,
|
||||||
vars.onBehalfOf,
|
vars.onBehalfOf,
|
||||||
vars.amount,
|
vars.amount,
|
||||||
|
@ -888,34 +896,34 @@ contract LendingPool is VersionedInitializable, ILendingPool, LendingPoolStorage
|
||||||
oracle
|
oracle
|
||||||
);
|
);
|
||||||
|
|
||||||
uint256 reserveId = reserve.id;
|
|
||||||
if (!userConfig.isBorrowing(reserveId)) {
|
|
||||||
userConfig.setBorrowing(reserveId, true);
|
|
||||||
}
|
|
||||||
|
|
||||||
reserve.updateState();
|
reserve.updateState();
|
||||||
|
|
||||||
//caching the current stable borrow rate
|
//caching the current stable borrow rate
|
||||||
uint256 currentStableRate = 0;
|
uint256 currentStableRate = 0;
|
||||||
|
|
||||||
|
bool isFirstBorrowing = false;
|
||||||
if (
|
if (
|
||||||
ReserveLogic.InterestRateMode(vars.interestRateMode) == ReserveLogic.InterestRateMode.STABLE
|
ReserveLogic.InterestRateMode(vars.interestRateMode) == ReserveLogic.InterestRateMode.STABLE
|
||||||
) {
|
) {
|
||||||
currentStableRate = reserve.currentStableBorrowRate;
|
currentStableRate = reserve.currentStableBorrowRate;
|
||||||
|
|
||||||
IStableDebtToken(reserve.stableDebtTokenAddress).mint(
|
isFirstBorrowing = IStableDebtToken(reserve.stableDebtTokenAddress).mint(
|
||||||
vars.onBehalfOf,
|
vars.onBehalfOf,
|
||||||
vars.amount,
|
vars.amount,
|
||||||
currentStableRate
|
currentStableRate
|
||||||
);
|
);
|
||||||
} else {
|
} else {
|
||||||
IVariableDebtToken(reserve.variableDebtTokenAddress).mint(
|
isFirstBorrowing = IVariableDebtToken(reserve.variableDebtTokenAddress).mint(
|
||||||
vars.onBehalfOf,
|
vars.onBehalfOf,
|
||||||
vars.amount,
|
vars.amount,
|
||||||
reserve.variableBorrowIndex
|
reserve.variableBorrowIndex
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (isFirstBorrowing) {
|
||||||
|
userConfig.setBorrowing(reserve.id, true);
|
||||||
|
}
|
||||||
|
|
||||||
reserve.updateInterestRates(
|
reserve.updateInterestRates(
|
||||||
vars.asset,
|
vars.asset,
|
||||||
vars.aTokenAddress,
|
vars.aTokenAddress,
|
||||||
|
|
|
@ -15,7 +15,6 @@ import {Helpers} from '../libraries/helpers/Helpers.sol';
|
||||||
import {WadRayMath} from '../libraries/math/WadRayMath.sol';
|
import {WadRayMath} from '../libraries/math/WadRayMath.sol';
|
||||||
import {PercentageMath} from '../libraries/math/PercentageMath.sol';
|
import {PercentageMath} from '../libraries/math/PercentageMath.sol';
|
||||||
import {SafeERC20} from '../dependencies/openzeppelin/contracts/SafeERC20.sol';
|
import {SafeERC20} from '../dependencies/openzeppelin/contracts/SafeERC20.sol';
|
||||||
import {ISwapAdapter} from '../interfaces/ISwapAdapter.sol';
|
|
||||||
import {Errors} from '../libraries/helpers/Errors.sol';
|
import {Errors} from '../libraries/helpers/Errors.sol';
|
||||||
import {ValidationLogic} from '../libraries/logic/ValidationLogic.sol';
|
import {ValidationLogic} from '../libraries/logic/ValidationLogic.sol';
|
||||||
import {LendingPoolStorage} from './LendingPoolStorage.sol';
|
import {LendingPoolStorage} from './LendingPoolStorage.sol';
|
||||||
|
|
|
@ -47,7 +47,7 @@ contract LendingPoolConfigurator is VersionedInitializable {
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param stableRateEnabled true if stable rate borrowing is enabled, false otherwise
|
* @param stableRateEnabled true if stable rate borrowing is enabled, false otherwise
|
||||||
**/
|
**/
|
||||||
event BorrowingEnabledOnReserve(address asset, bool stableRateEnabled);
|
event BorrowingEnabledOnReserve(address indexed asset, bool stableRateEnabled);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when borrowing is disabled on a reserve
|
* @dev emitted when borrowing is disabled on a reserve
|
||||||
|
@ -116,42 +116,42 @@ contract LendingPoolConfigurator is VersionedInitializable {
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param ltv the new value for the loan to value
|
* @param ltv the new value for the loan to value
|
||||||
**/
|
**/
|
||||||
event ReserveBaseLtvChanged(address asset, uint256 ltv);
|
event ReserveBaseLtvChanged(address indexed asset, uint256 ltv);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when a reserve factor is updated
|
* @dev emitted when a reserve factor is updated
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param factor the new reserve factor
|
* @param factor the new reserve factor
|
||||||
**/
|
**/
|
||||||
event ReserveFactorChanged(address asset, uint256 factor);
|
event ReserveFactorChanged(address indexed asset, uint256 factor);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when a reserve liquidation threshold is updated
|
* @dev emitted when a reserve liquidation threshold is updated
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param threshold the new value for the liquidation threshold
|
* @param threshold the new value for the liquidation threshold
|
||||||
**/
|
**/
|
||||||
event ReserveLiquidationThresholdChanged(address asset, uint256 threshold);
|
event ReserveLiquidationThresholdChanged(address indexed asset, uint256 threshold);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when a reserve liquidation bonus is updated
|
* @dev emitted when a reserve liquidation bonus is updated
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param bonus the new value for the liquidation bonus
|
* @param bonus the new value for the liquidation bonus
|
||||||
**/
|
**/
|
||||||
event ReserveLiquidationBonusChanged(address asset, uint256 bonus);
|
event ReserveLiquidationBonusChanged(address indexed asset, uint256 bonus);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when the reserve decimals are updated
|
* @dev emitted when the reserve decimals are updated
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param decimals the new decimals
|
* @param decimals the new decimals
|
||||||
**/
|
**/
|
||||||
event ReserveDecimalsChanged(address asset, uint256 decimals);
|
event ReserveDecimalsChanged(address indexed asset, uint256 decimals);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when a reserve interest strategy contract is updated
|
* @dev emitted when a reserve interest strategy contract is updated
|
||||||
* @param asset the address of the reserve
|
* @param asset the address of the reserve
|
||||||
* @param strategy the new address of the interest strategy contract
|
* @param strategy the new address of the interest strategy contract
|
||||||
**/
|
**/
|
||||||
event ReserveInterestRateStrategyChanged(address asset, address strategy);
|
event ReserveInterestRateStrategyChanged(address indexed asset, address strategy);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when an aToken implementation is upgraded
|
* @dev emitted when an aToken implementation is upgraded
|
||||||
|
@ -159,7 +159,11 @@ contract LendingPoolConfigurator is VersionedInitializable {
|
||||||
* @param proxy the aToken proxy address
|
* @param proxy the aToken proxy address
|
||||||
* @param implementation the new aToken implementation
|
* @param implementation the new aToken implementation
|
||||||
**/
|
**/
|
||||||
event ATokenUpgraded(address asset, address proxy, address implementation);
|
event ATokenUpgraded(
|
||||||
|
address indexed asset,
|
||||||
|
address indexed proxy,
|
||||||
|
address indexed implementation
|
||||||
|
);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when the implementation of a stable debt token is upgraded
|
* @dev emitted when the implementation of a stable debt token is upgraded
|
||||||
|
@ -167,7 +171,11 @@ contract LendingPoolConfigurator is VersionedInitializable {
|
||||||
* @param proxy the stable debt token proxy address
|
* @param proxy the stable debt token proxy address
|
||||||
* @param implementation the new aToken implementation
|
* @param implementation the new aToken implementation
|
||||||
**/
|
**/
|
||||||
event StableDebtTokenUpgraded(address asset, address proxy, address implementation);
|
event StableDebtTokenUpgraded(
|
||||||
|
address indexed asset,
|
||||||
|
address indexed proxy,
|
||||||
|
address indexed implementation
|
||||||
|
);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev emitted when the implementation of a variable debt token is upgraded
|
* @dev emitted when the implementation of a variable debt token is upgraded
|
||||||
|
@ -175,7 +183,11 @@ contract LendingPoolConfigurator is VersionedInitializable {
|
||||||
* @param proxy the variable debt token proxy address
|
* @param proxy the variable debt token proxy address
|
||||||
* @param implementation the new aToken implementation
|
* @param implementation the new aToken implementation
|
||||||
**/
|
**/
|
||||||
event VariableDebtTokenUpgraded(address asset, address proxy, address implementation);
|
event VariableDebtTokenUpgraded(
|
||||||
|
address indexed asset,
|
||||||
|
address indexed proxy,
|
||||||
|
address indexed implementation
|
||||||
|
);
|
||||||
|
|
||||||
ILendingPoolAddressesProvider internal addressesProvider;
|
ILendingPoolAddressesProvider internal addressesProvider;
|
||||||
ILendingPool internal pool;
|
ILendingPool internal pool;
|
||||||
|
|
|
@ -98,7 +98,6 @@ library Errors {
|
||||||
string public constant INVALID_DECIMALS = '73';
|
string public constant INVALID_DECIMALS = '73';
|
||||||
string public constant INVALID_RESERVE_FACTOR = '74';
|
string public constant INVALID_RESERVE_FACTOR = '74';
|
||||||
|
|
||||||
|
|
||||||
enum CollateralManagerErrors {
|
enum CollateralManagerErrors {
|
||||||
NO_ERROR,
|
NO_ERROR,
|
||||||
NO_COLLATERAL_AVAILABLE,
|
NO_COLLATERAL_AVAILABLE,
|
||||||
|
|
|
@ -104,6 +104,7 @@ library ValidationLogic {
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev validates a borrow.
|
* @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 reserve the reserve state from which the user is borrowing
|
||||||
* @param userAddress the address of the user
|
* @param userAddress the address of the user
|
||||||
* @param amount the amount to be borrowed
|
* @param amount the amount to be borrowed
|
||||||
|
@ -117,6 +118,7 @@ library ValidationLogic {
|
||||||
*/
|
*/
|
||||||
|
|
||||||
function validateBorrow(
|
function validateBorrow(
|
||||||
|
address asset,
|
||||||
ReserveLogic.ReserveData storage reserve,
|
ReserveLogic.ReserveData storage reserve,
|
||||||
address userAddress,
|
address userAddress,
|
||||||
uint256 amount,
|
uint256 amount,
|
||||||
|
@ -203,6 +205,8 @@ library ValidationLogic {
|
||||||
Errors.CALLATERAL_SAME_AS_BORROWING_CURRENCY
|
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
|
//calculate the max available loan size in stable rate mode as a percentage of the
|
||||||
//available liquidity
|
//available liquidity
|
||||||
uint256 maxLoanSizeStable = vars.availableLiquidity.percentMul(maxStableLoanPercent);
|
uint256 maxLoanSizeStable = vars.availableLiquidity.percentMul(maxStableLoanPercent);
|
||||||
|
@ -251,15 +255,15 @@ library ValidationLogic {
|
||||||
* @dev validates a swap of borrow rate mode.
|
* @dev validates a swap of borrow rate mode.
|
||||||
* @param reserve the reserve state on which the user is swapping the rate
|
* @param reserve the reserve state on which the user is swapping the rate
|
||||||
* @param userConfig the user reserves configuration
|
* @param userConfig the user reserves configuration
|
||||||
* @param stableBorrowBalance the stable borrow balance of the user
|
* @param stableDebt the stable debt of the user
|
||||||
* @param variableBorrowBalance the stable borrow balance of the user
|
* @param variableDebt the variable debt of the user
|
||||||
* @param currentRateMode the rate mode of the borrow
|
* @param currentRateMode the rate mode of the borrow
|
||||||
*/
|
*/
|
||||||
function validateSwapRateMode(
|
function validateSwapRateMode(
|
||||||
ReserveLogic.ReserveData storage reserve,
|
ReserveLogic.ReserveData storage reserve,
|
||||||
UserConfiguration.Map storage userConfig,
|
UserConfiguration.Map storage userConfig,
|
||||||
uint256 stableBorrowBalance,
|
uint256 stableDebt,
|
||||||
uint256 variableBorrowBalance,
|
uint256 variableDebt,
|
||||||
ReserveLogic.InterestRateMode currentRateMode
|
ReserveLogic.InterestRateMode currentRateMode
|
||||||
) external view {
|
) external view {
|
||||||
(bool isActive, bool isFreezed, , bool stableRateEnabled) = reserve.configuration.getFlags();
|
(bool isActive, bool isFreezed, , bool stableRateEnabled) = reserve.configuration.getFlags();
|
||||||
|
@ -268,9 +272,9 @@ library ValidationLogic {
|
||||||
require(!isFreezed, Errors.NO_UNFREEZED_RESERVE);
|
require(!isFreezed, Errors.NO_UNFREEZED_RESERVE);
|
||||||
|
|
||||||
if (currentRateMode == ReserveLogic.InterestRateMode.STABLE) {
|
if (currentRateMode == ReserveLogic.InterestRateMode.STABLE) {
|
||||||
require(stableBorrowBalance > 0, Errors.NO_STABLE_RATE_LOAN_IN_RESERVE);
|
require(stableDebt > 0, Errors.NO_STABLE_RATE_LOAN_IN_RESERVE);
|
||||||
} else if (currentRateMode == ReserveLogic.InterestRateMode.VARIABLE) {
|
} else if (currentRateMode == ReserveLogic.InterestRateMode.VARIABLE) {
|
||||||
require(variableBorrowBalance > 0, Errors.NO_VARIABLE_RATE_LOAN_IN_RESERVE);
|
require(variableDebt > 0, Errors.NO_VARIABLE_RATE_LOAN_IN_RESERVE);
|
||||||
/**
|
/**
|
||||||
* user wants to swap to stable, before swapping we need to ensure that
|
* user wants to swap to stable, before swapping we need to ensure that
|
||||||
* 1. stable borrow rate is enabled on the reserve
|
* 1. stable borrow rate is enabled on the reserve
|
||||||
|
@ -283,8 +287,7 @@ library ValidationLogic {
|
||||||
require(
|
require(
|
||||||
!userConfig.isUsingAsCollateral(reserve.id) ||
|
!userConfig.isUsingAsCollateral(reserve.id) ||
|
||||||
reserve.configuration.getLtv() == 0 ||
|
reserve.configuration.getLtv() == 0 ||
|
||||||
stableBorrowBalance.add(variableBorrowBalance) >
|
stableDebt.add(variableDebt) > IERC20(reserve.aTokenAddress).balanceOf(msg.sender),
|
||||||
IERC20(reserve.aTokenAddress).balanceOf(msg.sender),
|
|
||||||
Errors.CALLATERAL_SAME_AS_BORROWING_CURRENCY
|
Errors.CALLATERAL_SAME_AS_BORROWING_CURRENCY
|
||||||
);
|
);
|
||||||
} else {
|
} else {
|
||||||
|
@ -331,16 +334,10 @@ library ValidationLogic {
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev validates a flashloan action
|
* @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 assets the assets being flashborrowed
|
||||||
* @param amounts the amounts for each asset being borrowed
|
* @param amounts the amounts for each asset being borrowed
|
||||||
**/
|
**/
|
||||||
function validateFlashloan(
|
function validateFlashloan(address[] memory assets, uint256[] memory amounts) internal pure {
|
||||||
address[] memory assets,
|
|
||||||
uint256[] memory amounts,
|
|
||||||
uint256 mode
|
|
||||||
) internal pure {
|
|
||||||
require(mode <= uint256(ReserveLogic.InterestRateMode.VARIABLE), Errors.INVALID_FLASHLOAN_MODE);
|
|
||||||
require(assets.length == amounts.length, Errors.INCONSISTENT_FLASHLOAN_PARAMS);
|
require(assets.length == amounts.length, Errors.INCONSISTENT_FLASHLOAN_PARAMS);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -47,9 +47,11 @@ contract MockFlashLoanReceiver is FlashLoanReceiverBase {
|
||||||
address[] memory assets,
|
address[] memory assets,
|
||||||
uint256[] memory amounts,
|
uint256[] memory amounts,
|
||||||
uint256[] memory premiums,
|
uint256[] memory premiums,
|
||||||
|
address initiator,
|
||||||
bytes memory params
|
bytes memory params
|
||||||
) public override returns (bool) {
|
) public override returns (bool) {
|
||||||
params;
|
params;
|
||||||
|
initiator;
|
||||||
|
|
||||||
if (_failExecution) {
|
if (_failExecution) {
|
||||||
emit ExecutedWithFail(assets, amounts, premiums);
|
emit ExecutedWithFail(assets, amounts, premiums);
|
||||||
|
|
|
@ -97,7 +97,7 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
|
||||||
address user,
|
address user,
|
||||||
uint256 amount,
|
uint256 amount,
|
||||||
uint256 rate
|
uint256 rate
|
||||||
) external override onlyLendingPool {
|
) external override onlyLendingPool returns (bool) {
|
||||||
MintLocalVars memory vars;
|
MintLocalVars memory vars;
|
||||||
|
|
||||||
//cumulates the user debt
|
//cumulates the user debt
|
||||||
|
@ -148,6 +148,8 @@ contract StableDebtToken is IStableDebtToken, DebtTokenBase {
|
||||||
vars.newStableRate,
|
vars.newStableRate,
|
||||||
vars.currentAvgStableRate
|
vars.currentAvgStableRate
|
||||||
);
|
);
|
||||||
|
|
||||||
|
return currentBalance == 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -286,7 +288,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) {
|
||||||
|
|
|
@ -62,7 +62,7 @@ interface IStableDebtToken {
|
||||||
address user,
|
address user,
|
||||||
uint256 amount,
|
uint256 amount,
|
||||||
uint256 rate
|
uint256 rate
|
||||||
) external;
|
) external returns (bool);
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @dev burns debt of the target user.
|
* @dev burns debt of the target user.
|
||||||
|
|
|
@ -163,25 +163,26 @@
|
||||||
},
|
},
|
||||||
"ReserveLogic": {
|
"ReserveLogic": {
|
||||||
"buidlerevm": {
|
"buidlerevm": {
|
||||||
"address": "0xFAe0fd738dAbc8a0426F47437322b6d026A9FD95",
|
"address": "0x78Ee8Fb9fE5abD5e347Fc94c2fb85596d1f60e3c",
|
||||||
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"GenericLogic": {
|
"GenericLogic": {
|
||||||
"buidlerevm": {
|
"buidlerevm": {
|
||||||
"address": "0x6082731fdAba4761277Fb31299ebC782AD3bCf24",
|
"address": "0x920d847fE49E54C19047ba8bc236C45A8068Bca7",
|
||||||
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"ValidationLogic": {
|
"ValidationLogic": {
|
||||||
"buidlerevm": {
|
"buidlerevm": {
|
||||||
"address": "0x8456161947DFc1fC159A0B26c025cD2b4bba0c3e",
|
"address": "0xA4765Ff72A9F3CfE73089bb2c3a41B838DF71574",
|
||||||
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"LendingPool": {
|
"LendingPool": {
|
||||||
"buidlerevm": {
|
"buidlerevm": {
|
||||||
"address": "0xD9273d497eDBC967F39d419461CfcF382a0A822e"
|
"address": "0x35c1419Da7cf0Ff885B8Ef8EA9242FEF6800c99b",
|
||||||
|
"deployer": "0xc783df8a850f42e7F7e57013759C285caa701eB6"
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"LendingPoolConfigurator": {
|
"LendingPoolConfigurator": {
|
||||||
|
|
1
runStableTokenCLI.sh
Normal file
1
runStableTokenCLI.sh
Normal 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
1
runUserConfigCLI.sh
Normal 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
1
runVariableTokenCLI.sh
Normal 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
155
specs/StableDebtToken.spec
Normal 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
66
specs/UserConfiguration.spec
Normal 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
173
specs/VariableDebtToken.spec
Normal 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";
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
198
specs/harness/LendingPoolHarnessForVariableDebtToken.sol
Normal file
198
specs/harness/LendingPoolHarnessForVariableDebtToken.sol
Normal file
|
@ -0,0 +1,198 @@
|
||||||
|
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);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
28
specs/harness/StableDebtTokenHarness.sol
Normal file
28
specs/harness/StableDebtTokenHarness.sol
Normal file
|
@ -0,0 +1,28 @@
|
||||||
|
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);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
77
specs/harness/UserConfigurationHarness.sol
Normal file
77
specs/harness/UserConfigurationHarness.sol
Normal file
|
@ -0,0 +1,77 @@
|
||||||
|
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 { }
|
||||||
|
}
|
||||||
|
|
|
@ -71,7 +71,10 @@ makeSuite('AToken: Transfer', (testEnv: TestEnv) => {
|
||||||
users[1].address
|
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'));
|
expect(userReserveData.currentStableDebt.toString()).to.be.eq(ethers.utils.parseEther('0.1'));
|
||||||
});
|
});
|
||||||
|
@ -88,7 +91,6 @@ makeSuite('AToken: Transfer', (testEnv: TestEnv) => {
|
||||||
});
|
});
|
||||||
|
|
||||||
it('User 1 tries to transfer a small amount of DAI used as collateral back to user 0', async () => {
|
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 {users, pool, aDai, dai, weth} = testEnv;
|
||||||
|
|
||||||
const aDAItoTransfer = await convertToCurrencyDecimals(dai.address, '100');
|
const aDAItoTransfer = await convertToCurrencyDecimals(dai.address, '100');
|
||||||
|
|
|
@ -48,7 +48,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[ethers.utils.parseEther('0.8')],
|
[ethers.utils.parseEther('0.8')],
|
||||||
0,
|
[0],
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -78,7 +78,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
['1000720000000000000'],
|
['1000720000000000000'],
|
||||||
0,
|
[0],
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -110,7 +110,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[ethers.utils.parseEther('0.8')],
|
[ethers.utils.parseEther('0.8')],
|
||||||
0,
|
[0],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -131,7 +131,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[ethers.utils.parseEther('0.8')],
|
[ethers.utils.parseEther('0.8')],
|
||||||
0,
|
[0],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -152,12 +152,12 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[ethers.utils.parseEther('0.8')],
|
[ethers.utils.parseEther('0.8')],
|
||||||
4,
|
[4],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'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 () => {
|
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,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[ethers.utils.parseEther('0.8')],
|
[ethers.utils.parseEther('0.8')],
|
||||||
2,
|
[2],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -209,7 +209,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
['1004415000000000000'], //slightly higher than the available liquidity
|
['1004415000000000000'], //slightly higher than the available liquidity
|
||||||
2,
|
[2],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -223,7 +223,15 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
const caller = users[1];
|
const caller = users[1];
|
||||||
|
|
||||||
await expect(
|
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;
|
).to.be.reverted;
|
||||||
});
|
});
|
||||||
|
|
||||||
|
@ -251,7 +259,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[usdc.address],
|
[usdc.address],
|
||||||
[flashloanAmount],
|
[flashloanAmount],
|
||||||
0,
|
[0],
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -294,7 +302,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[usdc.address],
|
[usdc.address],
|
||||||
[flashloanAmount],
|
[flashloanAmount],
|
||||||
2,
|
[2],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -321,7 +329,15 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
|
|
||||||
await pool
|
await pool
|
||||||
.connect(caller.signer)
|
.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(
|
const {variableDebtTokenAddress} = await helpersContract.getReserveTokensAddresses(
|
||||||
usdc.address
|
usdc.address
|
||||||
);
|
);
|
||||||
|
@ -360,7 +376,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[flashAmount],
|
[flashAmount],
|
||||||
0,
|
[0],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -383,7 +399,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[flashAmount],
|
[flashAmount],
|
||||||
1,
|
[1],
|
||||||
caller.address,
|
caller.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -429,7 +445,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[flashAmount],
|
[flashAmount],
|
||||||
1,
|
[1],
|
||||||
onBehalfOf.address,
|
onBehalfOf.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
@ -458,7 +474,7 @@ makeSuite('LendingPool FlashLoan function', (testEnv: TestEnv) => {
|
||||||
_mockFlashLoanReceiver.address,
|
_mockFlashLoanReceiver.address,
|
||||||
[weth.address],
|
[weth.address],
|
||||||
[flashAmount],
|
[flashAmount],
|
||||||
1,
|
[1],
|
||||||
onBehalfOf.address,
|
onBehalfOf.address,
|
||||||
'0x10',
|
'0x10',
|
||||||
'0'
|
'0'
|
||||||
|
|
|
@ -231,7 +231,7 @@ export const withdraw = async (
|
||||||
|
|
||||||
if (expectedResult === 'success') {
|
if (expectedResult === 'success') {
|
||||||
const txResult = await waitForTx(
|
const txResult = await waitForTx(
|
||||||
await pool.connect(user.signer).withdraw(reserve, amountToWithdraw)
|
await pool.connect(user.signer).withdraw(reserve, amountToWithdraw, user.address)
|
||||||
);
|
);
|
||||||
|
|
||||||
const {
|
const {
|
||||||
|
@ -269,8 +269,10 @@ export const withdraw = async (
|
||||||
// );
|
// );
|
||||||
// });
|
// });
|
||||||
} else if (expectedResult === 'revert') {
|
} else if (expectedResult === 'revert') {
|
||||||
await expect(pool.connect(user.signer).withdraw(reserve, amountToWithdraw), revertMessage).to.be
|
await expect(
|
||||||
.reverted;
|
pool.connect(user.signer).withdraw(reserve, amountToWithdraw, user.address),
|
||||||
|
revertMessage
|
||||||
|
).to.be.reverted;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -116,7 +116,7 @@ makeSuite('Pausable Pool', (testEnv: TestEnv) => {
|
||||||
|
|
||||||
// user tries to burn
|
// user tries to burn
|
||||||
await expect(
|
await expect(
|
||||||
pool.connect(users[0].signer).withdraw(dai.address, amountDAItoDeposit)
|
pool.connect(users[0].signer).withdraw(dai.address, amountDAItoDeposit, users[0].address)
|
||||||
).to.revertedWith(IS_PAUSED);
|
).to.revertedWith(IS_PAUSED);
|
||||||
|
|
||||||
// Configurator unpauses the pool
|
// Configurator unpauses the pool
|
||||||
|
@ -187,7 +187,15 @@ makeSuite('Pausable Pool', (testEnv: TestEnv) => {
|
||||||
await expect(
|
await expect(
|
||||||
pool
|
pool
|
||||||
.connect(caller.signer)
|
.connect(caller.signer)
|
||||||
.flashLoan(_mockFlashLoanReceiver.address, [weth.address], [flashAmount], 1, caller.address, '0x10', '0')
|
.flashLoan(
|
||||||
|
_mockFlashLoanReceiver.address,
|
||||||
|
[weth.address],
|
||||||
|
[flashAmount],
|
||||||
|
[1],
|
||||||
|
caller.address,
|
||||||
|
'0x10',
|
||||||
|
'0'
|
||||||
|
)
|
||||||
).revertedWith(IS_PAUSED);
|
).revertedWith(IS_PAUSED);
|
||||||
|
|
||||||
// Unpause pool
|
// Unpause pool
|
||||||
|
|
Loading…
Reference in New Issue
Block a user