Solve conflicts

.gitlab-ci.yml

@@ -24,3 +24,19 @@ deploy-mainnet-fork:
   after_script:
     - docker-compose -p ${CI_JOB_ID} -f docker-compose.test.yml run contracts-env npm run ci:clean
     - docker-compose -p ${CI_JOB_ID} -f docker-compose.test.yml down
+
+certora-test:
+  stage: checks
+  image: python:latest
+  before_script:
+    - apt-get update || apt-get update
+    - apt-get install -y software-properties-common
+    - pip3 install certora-cli
+    - wget https://github.com/ethereum/solidity/releases/download/v0.6.12/solc-static-linux
+    - chmod +x solc-static-linux
+    - mv solc-static-linux /usr/bin/solc
+    - export PATH=$PATH:/usr/bin/solc/solc-static-linux
+  script:
+    - certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc_args '--optimize' --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --cloud
+    - certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --cache UserConfiguration --cloud
+    - certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -assumeUnwindCond,-useNonLinearArithmetic,-b=4 --cache VariableDebtToken --cloud

README.md

@@ -1,3 +1,16 @@
+```
+        .///.                .///.     //.            .//  `/////////////-
+       `++:++`              .++:++`    :++`          `++:  `++:......---.`
+      `/+: -+/`            `++- :+/`    /+/         `/+/   `++.
+      /+/   :+/            /+:   /+/    `/+/        /+/`   `++.
+  -::/++::`  /+:       -::/++::` `/+:    `++:      :++`    `++/:::::::::.
+  -:+++::-`  `/+:      --++/---`  `++-    .++-    -++.     `++/:::::::::.
+   -++.       .++-      -++`       .++.    .++.  .++-      `++.
+  .++-         -++.    .++.         -++.    -++``++-       `++.
+ `++:           :++`  .++-           :++`    :+//+:        `++:----------`
+ -/:             :/-  -/:             :/.     ://:         `/////////////-
+```
+
 # Aave Protocol v2
 
 This repository contains the smart contracts source code and markets configuration for Aave Protocol V2. The repository uses Docker Compose and Hardhat as development enviroment for compilation, testing and deployment tasks.
@@ -8,13 +21,23 @@ Aave is a decentralized non-custodial liquidity markets protocol where users can
 
 ## Documentation
 
-The documentation of Aave V2 is in the following [Aave V2 documentation](https://docs.aave.com/v2/-MJXUluJ2u1DiL-VU6MM) link. At the documentation you can learn more about the protocol, see the contract interfaces, integration guides and audits.
+The documentation of Aave V2 is in the following [Aave V2 documentation](https://docs.aave.com/developers/v/2.0/) link. At the documentation you can learn more about the protocol, see the contract interfaces, integration guides and audits.
 
-For getting the latest contracts addresses, please check the [Deployed contracts](https://docs.aave.com/v2/-MJXUluJ2u1DiL-VU6MM/deployed-contracts) page at the documentation to stay up to date.
+For getting the latest contracts addresses, please check the [Deployed contracts](https://docs.aave.com/developers/v/2.0/deployed-contracts/deployed-contracts) page at the documentation to stay up to date.
+
+A more detailed and technical description of the protocol can be found in this repository, [here](./aave-v2-whitepaper.pdf)
+
+## Audits
+
+- MixBytes (16/09/2020 - 03/12/2020): [report](./audits/Mixbytes-aave-v2-03-12-2020.pdf)
+- PeckShield (29/09/2020 - 03/12/2020) : [report](./audits/Peckshield-aave-v2-03-12-2020-EN.pdf) (Also available in Chinese in the same folder)
+- CertiK (28/09/2020 - 02/12/2020): [report](./audits/Certik-aave-v2-03-12-2020.pdf)
+- Consensys Diligence (09/09/2020 - 09/10/2020): [report](https://consensys.net/diligence/audits/2020/09/aave-protocol-v2/)
+- Certora, formal verification (02/08/2020 - 29/10/2020): [report](./audits/Certora-FV-aave-v2-03-12-2020.pdf)
 
 ## Connect with the community
 
-You can join at the [Discord](https://discord.com/invite/CJm5Jt3) channel or at the [Governance Forum](https://governance.aave.com/) for asking questions about the protocol or talk about Aave with other peers.
+You can join at the [Discord](http://aave.com/discord) channel or at the [Governance Forum](https://governance.aave.com/) for asking questions about the protocol or talk about Aave with other peers.
 
 ## Setup
 
@@ -83,41 +106,87 @@ npm run aave:kovan:full:migration
 
 ### Mainnet fork deployment
 
-You can deploy Aave Protocol v2 in a forked Mainnet chain using Hardhat built-in feature:
+You can deploy Aave Protocol v2 in a forked Mainnet chain using Hardhat built-in fork feature:
 
 ```
-# In one terminal, run a hardhat note with mainnet fork enabled
+docker-compose run contracts-env npm run aave:fork:main
-MAINNET_FORK=true npx hardhat node
+```
 
-# In another terminal, run docker-compose
+### Deploy Aave into a Mainnet Fork via console
-docker-compose up
 
-# Open another tab or terminal
+You can deploy Aave into the Hardhat console in fork mode, to interact with the protocol inside the fork or for testing purposes.
-docker-compose exec contracts-env bash
 
-# A new Bash terminal is prompted, connected to the container
+Run the console in Mainnet fork mode:
-npm run aave:fork:main
 
-# Contracts are now deployed at Hardhat node with Mainnet fork.
+```
+docker-compose run contracts-env npm run console:fork
+```
 
-# You can interact with them via Hardhat console
+At the Hardhat console, interact with the Aave protocol in Mainnet fork mode:
-MAINNET_FORK=true npx hardhat console
+
-# Or your custom Hardhat task
+```
-MAINNET_FORK=true npx hardhat your-custom-task
+// Deploy the Aave protocol in fork mode
+await run('aave:mainnet')
+
+// Or your custom Hardhat task
+await run('your-custom-task');
+
+// After you initialize the HRE via 'set-DRE' task, you can import any TS/JS file
+run('set-DRE');
+
+// Import contract getters to retrieve an Ethers.js Contract instance
+const contractGetters = require('./helpers/contracts-getters'); // Import a TS/JS file
+
+// Lending pool instance
+const lendingPool = await contractGetters.getLendingPool("LendingPool address from 'aave:mainnet' task");
+
+// You can impersonate any Ethereum address
+await network.provider.request({ method: "hardhat_impersonateAccount",  params: ["0xb1adceddb2941033a090dd166a462fe1c2029484"]});
+
+const signer = await ethers.provider.getSigner("0xb1adceddb2941033a090dd166a462fe1c2029484")
+
+// ERC20 token DAI Mainnet instance
+const DAI = await contractGetters.getIErc20Detailed("0x6B175474E89094C44Da98b954EedeAC495271d0F");
+
+// Approve 100 DAI to LendingPool address
+await DAI.connect(signer).approve(lendingPool.address, ethers.utils.parseUnits('100'));
+
+// Deposit 100 DAI
+await lendingPool.connect(signer).deposit(DAI.address, ethers.utils.parseUnits('100'), await signer.getAddress(), '0');
 
 ```
 
-### Mainnet fork - Run the check list
+## Interact with Aave in Mainnet via console
 
-For testing the deployment scripts for Mainnet release, you can run the check-list tests in a Mainnet fork using Hardhat built-in feature:
+You can interact with Aave at Mainnet network using the Hardhat console, in the scenario where the frontend is down or you want to interact directly. You can check the deployed addresses at https://docs.aave.com/developers/deployed-contracts.
+
+Run the Hardhat console pointing to the Mainnet network:
 
 ```
-# In another terminal, run docker-compose
+docker-compose run contracts-env npx hardhat --network main console
-docker-compose up
+```
-
+
-# Open another tab or terminal
+At the Hardhat console, you can interact with the protocol:
-docker-compose exec contracts-env bash
+
-
+```
-# A new Bash terminal is prompted, connected to the container
+// Load the HRE into helpers to access signers
-npm run test:main:check-list
+run("set-DRE")
+
+// Import getters to instance any Aave contract
+const contractGetters = require('./helpers/contracts-getters');
+
+// Load the first signer
+const signer = await contractGetters.getFirstSigner();
+
+// Lending pool instance
+const lendingPool = await contractGetters.getLendingPool("0x7d2768dE32b0b80b7a3454c06BdAc94A69DDc7A9");
+
+// ERC20 token DAI Mainnet instance
+const DAI = await contractGetters.getIErc20Detailed("0x6B175474E89094C44Da98b954EedeAC495271d0F");
+
+// Approve 100 DAI to LendingPool address
+await DAI.connect(signer).approve(lendingPool.address, ethers.utils.parseUnits('100'));
+
+// Deposit 100 DAI
+await lendingPool.connect(signer).deposit(DAI.address, ethers.utils.parseUnits('100'), await signer.getAddress(), '0');
 ```

hardhat.config.ts

@@ -29,25 +29,26 @@ const MAINNET_FORK = process.env.MAINNET_FORK === 'true';
 
 // Prevent to load scripts before compilation and typechain
 if (!SKIP_LOAD) {
-  ['misc', 'migrations', 'dev', 'full', 'verifications', 'deployments'].forEach((folder) => {
+  ['misc', 'migrations', 'dev', 'full', 'verifications', 'deployments', 'helpers'].forEach(
+    (folder) => {
       const tasksPath = path.join(__dirname, 'tasks', folder);
       fs.readdirSync(tasksPath)
         .filter((pth) => pth.includes('.ts'))
         .forEach((task) => {
           require(`${tasksPath}/${task}`);
         });
-  });
+    }
+  );
 }
 
 require(`${path.join(__dirname, 'tasks/misc')}/set-bre.ts`);
 
 const getCommonNetworkConfig = (networkName: eEthereumNetwork, networkId: number) => {
+  const net = networkName === 'main' ? 'mainnet' : networkName;
   return {
     url: ALCHEMY_KEY
-      ? `https://eth-${
+      ? `https://eth-${net}.alchemyapi.io/v2/${ALCHEMY_KEY}`
-          networkName === 'main' ? 'mainnet' : networkName
+      : `https://${net}.infura.io/v3/${INFURA_KEY}`,
-        }.alchemyapi.io/v2/${ALCHEMY_KEY}`
-      : `https://${networkName === 'main' ? 'mainnet' : networkName}.infura.io/v3/${INFURA_KEY}`,
     hardfork: HARDFORK,
     blockGasLimit: DEFAULT_BLOCK_GAS_LIMIT,
     gasMultiplier: DEFAULT_GAS_MUL,
@@ -64,10 +65,10 @@ const getCommonNetworkConfig = (networkName: eEthereumNetwork, networkId: number
 
 const mainnetFork = MAINNET_FORK
   ? {
-      blockNumber: 11361132,
+      blockNumber: 11608298,
       url: ALCHEMY_KEY
         ? `https://eth-mainnet.alchemyapi.io/v2/${ALCHEMY_KEY}`
-        : `https://main.infura.io/v3/${INFURA_KEY}`,
+        : `https://mainnet.infura.io/v3/${INFURA_KEY}`,
     }
   : undefined;
 

helpers/contracts-getters.ts

@@ -323,8 +323,8 @@ export const getLendingPoolCollateralManager = async (address?: tEthereumAddress
     await getFirstSigner()
   );
 
-export const getAddressById = async (id: string) =>
+export const getAddressById = async (id: string): Promise<tEthereumAddress | undefined> =>
-  (await getDb().get(`${id}.${DRE.network.name}`).value()).address;
+  (await getDb().get(`${id}.${DRE.network.name}`).value())?.address || undefined;
 
 export const getAaveOracle = async (address?: tEthereumAddress) =>
   await AaveOracleFactory.connect(

helpers/init-helpers.ts

@@ -1,13 +1,21 @@
-import { eContractid, iMultiPoolsAssets, IReserveParams, tEthereumAddress } from './types';
-import { AaveProtocolDataProvider } from '../types/AaveProtocolDataProvider';
-import { chunk, waitForTx } from './misc-utils';
 import {
+  eContractid,
+  eEthereumNetwork,
+  iMultiPoolsAssets,
+  IReserveParams,
+  tEthereumAddress,
+} from './types';
+import { AaveProtocolDataProvider } from '../types/AaveProtocolDataProvider';
+import { chunk, DRE, getDb, waitForTx } from './misc-utils';
+import {
+  getAaveProtocolDataProvider,
+  getAToken,
   getATokensAndRatesHelper,
   getLendingPoolAddressesProvider,
   getStableAndVariableTokensHelper,
 } from './contracts-getters';
 import { rawInsertContractAddressInDb } from './contracts-helpers';
-import { BigNumber, BigNumberish } from 'ethers';
+import { BigNumber, BigNumberish, Signer } from 'ethers';
 import {
   deployDefaultReserveInterestRateStrategy,
   deployDelegationAwareAToken,
@@ -16,8 +24,9 @@ import {
   deployVariableDebtToken,
 } from './contracts-deployments';
 import { ZERO_ADDRESS } from './constants';
+import { isZeroAddress } from 'ethereumjs-util';
 
-const chooseATokenDeployment = (id: eContractid) => {
+export const chooseATokenDeployment = (id: eContractid) => {
   switch (id) {
     case eContractid.AToken:
       return deployGenericAToken;
@@ -374,3 +383,191 @@ export const configureReservesByHelper = async (
     await waitForTx(await addressProvider.setPoolAdmin(admin));
   }
 };
+
+const getAddressById = async (
+  id: string,
+  network: eEthereumNetwork
+): Promise<tEthereumAddress | undefined> =>
+  (await getDb().get(`${id}.${network}`).value())?.address || undefined;
+
+export const initTokenReservesByHelper = async (
+  reservesParams: iMultiPoolsAssets<IReserveParams>,
+  tokenAddresses: { [symbol: string]: tEthereumAddress },
+  admin: tEthereumAddress,
+  addressesProviderAddress: tEthereumAddress,
+  ratesHelperAddress: tEthereumAddress,
+  dataProviderAddress: tEthereumAddress,
+  signer: Signer,
+  treasuryAddress: tEthereumAddress,
+  verify: boolean
+) => {
+  let gasUsage = BigNumber.from('0');
+  const atokenAndRatesDeployer = await (await getATokensAndRatesHelper(ratesHelperAddress)).connect(
+    signer
+  );
+
+  const addressProvider = await (
+    await getLendingPoolAddressesProvider(addressesProviderAddress)
+  ).connect(signer);
+  const protocolDataProvider = await (
+    await getAaveProtocolDataProvider(dataProviderAddress)
+  ).connect(signer);
+  const poolAddress = await addressProvider.getLendingPool();
+
+  // Set aTokenAndRatesDeployer as temporal admin
+  await waitForTx(await addressProvider.setPoolAdmin(atokenAndRatesDeployer.address));
+
+  // CHUNK CONFIGURATION
+  const initChunks = 4;
+
+  // Initialize variables for future reserves initialization
+  let deployedStableTokens: string[] = [];
+  let deployedVariableTokens: string[] = [];
+  let deployedATokens: string[] = [];
+  let deployedRates: string[] = [];
+  let reserveInitDecimals: string[] = [];
+  let reserveSymbols: string[] = [];
+  const network =
+    process.env.MAINNET_FORK === 'true'
+      ? eEthereumNetwork.main
+      : (DRE.network.name as eEthereumNetwork);
+  // Grab config from DB
+  for (const [symbol, address] of Object.entries(tokenAddresses)) {
+    const { aTokenAddress } = await protocolDataProvider.getReserveTokensAddresses(address);
+    const reserveParamIndex = Object.keys(reservesParams).findIndex((value) => value === symbol);
+    const [, { reserveDecimals: decimals }] = (Object.entries(reservesParams) as [
+      string,
+      IReserveParams
+    ][])[reserveParamIndex];
+
+    if (!isZeroAddress(aTokenAddress)) {
+      console.log(`- Skipping ${symbol} due already initialized`);
+      continue;
+    }
+    let stableTokenImpl = await getAddressById(`stableDebt${symbol}`, network);
+    let variableTokenImpl = await getAddressById(`variableDebt${symbol}`, network);
+    let aTokenImplementation = await getAddressById(`a${symbol}`, network);
+    let strategyImpl = await getAddressById(`strategy${symbol}`, network);
+
+    if (!stableTokenImpl) {
+      const stableDebt = await deployStableDebtToken(
+        [
+          poolAddress,
+          tokenAddresses[symbol],
+          `Aave stable debt bearing ${symbol}`,
+          `stableDebt${symbol}`,
+          ZERO_ADDRESS,
+        ],
+        verify
+      );
+      stableTokenImpl = stableDebt.address;
+    }
+    if (!variableTokenImpl) {
+      const variableDebt = await deployVariableDebtToken(
+        [
+          poolAddress,
+          tokenAddresses[symbol],
+          `Aave variable debt bearing ${symbol}`,
+          `variableDebt${symbol}`,
+          ZERO_ADDRESS,
+        ],
+        verify
+      );
+      variableTokenImpl = variableDebt.address;
+    }
+    if (!aTokenImplementation) {
+      const [, { aTokenImpl }] = (Object.entries(reservesParams) as [string, IReserveParams][])[
+        reserveParamIndex
+      ];
+      const deployCustomAToken = chooseATokenDeployment(aTokenImpl);
+      const aToken = await deployCustomAToken(
+        [
+          poolAddress,
+          tokenAddresses[symbol],
+          treasuryAddress,
+          `Aave interest bearing ${symbol}`,
+          `a${symbol}`,
+          ZERO_ADDRESS,
+        ],
+        verify
+      );
+      aTokenImplementation = aToken.address;
+    }
+    if (!strategyImpl) {
+      const [
+        ,
+        {
+          optimalUtilizationRate,
+          baseVariableBorrowRate,
+          variableRateSlope1,
+          variableRateSlope2,
+          stableRateSlope1,
+          stableRateSlope2,
+        },
+      ] = (Object.entries(reservesParams) as [string, IReserveParams][])[reserveParamIndex];
+      const rates = await deployDefaultReserveInterestRateStrategy(
+        [
+          tokenAddresses[symbol],
+          optimalUtilizationRate,
+          baseVariableBorrowRate,
+          variableRateSlope1,
+          variableRateSlope2,
+          stableRateSlope1,
+          stableRateSlope2,
+        ],
+        verify
+      );
+      strategyImpl = rates.address;
+    }
+    const symbols = [`a${symbol}`, `variableDebt${symbol}`, `stableDebt${symbol}`];
+    const tokens = [aTokenImplementation, variableTokenImpl, stableTokenImpl];
+    for (let index = 0; index < symbols.length; index++) {
+      if (!(await isErc20SymbolCorrect(tokens[index], symbols[index]))) {
+        console.error(`${symbol} and implementation does not match: ${tokens[index]}`);
+        throw Error('Symbol does not match implementation.');
+      }
+    }
+    console.log(`- Added ${symbol} to the initialize batch`);
+    deployedStableTokens.push(stableTokenImpl);
+    deployedVariableTokens.push(variableTokenImpl);
+    deployedATokens.push(aTokenImplementation);
+    deployedRates.push(strategyImpl);
+    reserveInitDecimals.push(decimals.toString());
+    reserveSymbols.push(symbol);
+  }
+
+  // Deploy init reserves per chunks
+  const chunkedStableTokens = chunk(deployedStableTokens, initChunks);
+  const chunkedVariableTokens = chunk(deployedVariableTokens, initChunks);
+  const chunkedAtokens = chunk(deployedATokens, initChunks);
+  const chunkedRates = chunk(deployedRates, initChunks);
+  const chunkedDecimals = chunk(reserveInitDecimals, initChunks);
+  const chunkedSymbols = chunk(reserveSymbols, initChunks);
+
+  console.log(`- Reserves initialization in ${chunkedStableTokens.length} txs`);
+  for (let chunkIndex = 0; chunkIndex < chunkedDecimals.length; chunkIndex++) {
+    const tx3 = await waitForTx(
+      await atokenAndRatesDeployer.initReserve(
+        chunkedStableTokens[chunkIndex],
+        chunkedVariableTokens[chunkIndex],
+        chunkedAtokens[chunkIndex],
+        chunkedRates[chunkIndex],
+        chunkedDecimals[chunkIndex]
+      )
+    );
+
+    console.log(`  - Reserve ready for: ${chunkedSymbols[chunkIndex].join(', ')}`);
+    console.log('    * gasUsed', tx3.gasUsed.toString());
+    gasUsage = gasUsage.add(tx3.gasUsed);
+  }
+
+  // Set deployer back as admin
+  await waitForTx(await addressProvider.setPoolAdmin(admin));
+  return gasUsage;
+};
+
+const isErc20SymbolCorrect = async (token: tEthereumAddress, symbol: string) => {
+  const erc20 = await getAToken(token); // using aToken for ERC20 interface
+  const erc20Symbol = await erc20.symbol();
+  return symbol === erc20Symbol;
+};

package.json

@@ -11,6 +11,7 @@
     "hardhat:main": "hardhat --network main",
     "hardhat:docker": "hardhat --network hardhatevm_docker",
     "compile": "SKIP_LOAD=true hardhat compile",
+    "console:fork": "MAINNET_FORK=true hardhat console",
     "test": "TS_NODE_TRANSPILE_ONLY=1 hardhat test ./test/*.spec.ts",
     "test-scenarios": "npm run test -- test/__setup.spec.ts test/scenario.spec.ts",
     "test-repay-with-collateral": "hardhat test test/__setup.spec.ts test/repay-with-collateral.spec.ts",
@@ -36,6 +37,7 @@
     "aave:fork:main:tenderly": "npm run compile && npm run hardhat:tenderly-main -- aave:mainnet",
     "aave:fork:main": "npm run compile && MAINNET_FORK=true  hardhat aave:mainnet",
     "aave:main:full:migration": "npm run compile && npm run hardhat:main -- aave:mainnet --verify",
+    "aave:main:full:initialize": "npm run compile && MAINNET_FORK=true full:initialize-tokens --pool Aave",
     "dev:prettier": "prettier --write .",
     "ci:test": "npm run compile && npm run test",
     "ci:clean": "rm -rf ./artifacts ./cache ./types",
@@ -54,7 +56,12 @@
     "ropsten:verify:tokens": "npm run hardhat:ropsten verify:tokens -- --pool Aave",
     "mainnet:verify:tokens": "npm run hardhat:main verify:tokens -- --pool Aave",
     "print-config:fork:mainnet": "MAINNET_FORK=true hardhat print-config:fork",
-    "print-config:kovan": "hardhat --network kovan print-config --pool Aave --data-provider 0xA1901785c29cBd48bfA74e46b67C736b26054fa4"
+    "print-config:kovan": "hardhat --network kovan print-config --pool Aave --data-provider 0xA1901785c29cBd48bfA74e46b67C736b26054fa4",
+    "main:fork:initialize-tokens": "npm run compile && MAINNET_FORK=true hardhat full:initialize-tokens --pool Aave",
+    "main:initialize-tokens": "npm run compile && hardhat --network main full:initialize-tokens --pool Aave",
+    "kovan:initialize-tokens": "npm run compile && hardhat --network kovan full:initialize-tokens --pool Aave",
+    "external:deploy-assets-kovan": "npm run compile && hardhat --network kovan external:deploy-new-asset --symbol ${SYMBOL} --verify",
+    "external:deploy-assets-main": "npm run compile && hardhat --network main external:deploy-new-asset --symbol ${SYMBOL} --verify"
   },
   "devDependencies": {
     "@nomiclabs/buidler": "^1.4.7",
@@ -110,14 +117,14 @@
   },
   "author": "Aave",
   "contributors": [
-    {
-      "name": "Ernesto Boado",
-      "email": "ernesto@aave.com"
-    },
     {
       "name": "Emilio Frangella",
       "email": "emilio@aave.com"
     },
+    {
+      "name": "Ernesto Boado",
+      "email": "ernesto@aave.com"
+    },
     {
       "name": "Andrey Kozlov",
       "email": "andrey@aave.com"
@@ -125,6 +132,14 @@
     {
       "name": "David Racero",
       "email": "david.k@aave.com"
+    },
+    {
+      "name": "Pol Sendra",
+      "email": "pol@aave.com"
+    },
+    {
+      "name": "David Truong",
+      "email": "david@aave.com"
     }
   ],
   "license": "AGPLv3",

runStableTokenCLI.sh

@@ -1 +1 @@
-certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master
+certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --solc_args '--optimize' --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableToken --cloud

runUserConfigCLI.sh

@@ -1 +1 @@
-certoraRun specs/harness/UserConfigurationHarness.sol  --solc solc6.8 --verify UserConfigurationHarness:specs/UserConfiguration.spec --settings -useBitVectorTheory --staging master
+certoraRun specs/harness/UserConfigurationHarness.sol  --solc solc6.12 --solc_args '--optimize' --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --cloud

runVariableTokenCLI.sh

@@ -1 +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
+certoraRun contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken specs/harness/LendingPoolHarnessForVariableDebtToken.sol --solc solc6.12 --solc_args '--optimize' --link VariableDebtToken:POOL=LendingPoolHarnessForVariableDebtToken --verify VariableDebtToken:specs/VariableDebtToken.spec --settings -b=4,-assumeUnwindCond,-useNonLinearArithmetic --cache VariableToken --cloud

specs/StableDebtToken.spec

@@ -14,82 +14,110 @@ rule integrityTimeStamp(address user, method f) {
 /**
 TotalSupply is the sum of all users’ balances
 	
-totalSupply(t) = Σaddress u. balanceOf(u,t)
+totalSupply(t) = Σaddress u. balanceOf(u,t).
 
-Check that each possible opertaion changes the balance of at most one user
+Checks that each possible operation changes the balance of at most one user.
 */
-rule balanceOfChange(address a, address b, method f )
+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 balanceABefore = sinvoke balanceOf(e, a);
-	uint256 balanceBBefore = sinvoke balanceOf(e,b);
+	uint256 balanceBBefore = sinvoke balanceOf(e, b);
 	 
 	calldataarg arg;
 	sinvoke f(e, arg); 
 
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
-	uint256 balanceBAfter = sinvoke balanceOf(e,b);
+	uint256 balanceBAfter = sinvoke balanceOf(e, b);
 	
-	assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
+	assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
 }
 
 /**
-Check that the change to total supply is coherent with the changes to balance
+Checks that the change to total supply is coherent with the change to user balance due to an operation
+(which is not burn).
 */
 rule integirtyBalanceOfTotalSupply(address a, method f )
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 totalSupplyBefore = sinvoke totalSupply(e);
 	 
 	calldataarg arg;
 	sinvoke f(e, arg); 
-	require (f.selector != burn(address,uint256).selector );
+	require (f.selector != burn(address, uint256).selector);
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
 
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert  (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
-/* Burn behaves differently and due to accumulation errors might have less total supply than the balance
+
+/**
+Checks that the change to total supply is coherent with the change to user balance due to a burn operation.
 */
-rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f)
+rule integirtyBalanceOfTotalSupplyOnBurn(address a, uint256 x)
 {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
-	uint256 balanceABefore = sinvoke balanceOf(e,a);
-	uint256 totalSupplyBefore = sinvoke totalSupply(e);
 	
-	uint256 x;
+	uint256 balanceABefore = sinvoke balanceOf(e, a);
+	
+	uint256 totalSupplyBefore = sinvoke totalSupply(e);
+	uint256 averageStableRateBefore = sinvoke getAverageStableRate(e);
+	uint256 debtSupplyBefore = sinvoke rayWadMul(e, averageStableRateBefore, totalSupplyBefore);
+	
+	uint256 stableRateA = sinvoke getUserStableRate(e, a);
+	uint256 repaidDebtA = sinvoke rayWadMul(e, stableRateA, x);
+	
+	
 	sinvoke burn(e, a, x); 
-	uint256 balanceAAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 totalSupplyAfter = sinvoke totalSupply(e);
-	if (totalSupplyBefore > x)
+
-		assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	if(totalSupplyBefore > x) {
-	else
+	    /* The amount being burned (x) is smaller than the total supply */
-		assert  (totalSupplyAfter == 0 );
+		if(repaidDebtA >= debtSupplyBefore) {
+			/*
+			The user debt being repaid is at least the debt supply.
+			The total supply becomes 0.
+			*/
+			assert(totalSupplyAfter == 0);
+		}
+		else {
+			assert(balanceAAfter != balanceABefore  =>
+			(balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+		}
+	}
+	else {
+	/* The amount being burned (x) is at least the total supply.
+	   The total supply becomes 0.
+	*/
+		assert (totalSupplyAfter == 0);
+	}
 }
 
 /**
-Mint inceases the balanceOf user a as expected
+Mint increases the balanceOf user a as expected.
 */
 rule integrityMint(address a, uint256 x) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
 	uint256 balancebefore = sinvoke balanceOf(e,a);
-	sinvoke mint(e,a,x,index);
+	sinvoke mint(e, delegatedUser, 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 is additive, namely it can performed either all at once or gradually:
-mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
+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,
@@ -97,18 +125,19 @@ and therefore it is currently excluded from the CI.
 */
 rule additiveMint(address a, uint256 x, uint256 y) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
-	require getUserStableRate(e,a) == 0;
+	require getUserStableRate(e, a) == 0;
 	uint256 index;
 	storage initialStorage = lastStorage;
-	sinvoke mint(e,a,x,index);
+	sinvoke mint(e, delegatedUser, a, x, index);
-	sinvoke mint(e,a,y,index);
+	sinvoke mint(e, delegatedUser, a, y, index);
-	uint256 balanceScenario1 = sinvoke balanceOf(e,a);
+	uint256 balanceScenario1 = sinvoke balanceOf(e, a);
 	
 	uint256 t = x + y;
-	sinvoke mint(e,a, t ,index) at initialStorage;
+	sinvoke mint(e, delegatedUser, a, t ,index) at initialStorage;
 	
-	uint256 balanceScenario2 = sinvoke balanceOf(e,a);
+	uint256 balanceScenario2 = sinvoke balanceOf(e, a);
 	assert balanceScenario1 == balanceScenario2, "mint is not additive";
 }
 
@@ -116,10 +145,10 @@ rule integrityBurn(address a, uint256 x) {
 	env e;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
-	uint256 balancebefore = sinvoke balanceOf(e,a);
+	uint256 balancebefore = sinvoke balanceOf(e, a);
 	sinvoke burn(e,a,x);
 	
-	uint256 balanceAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAfter = sinvoke balanceOf(e, a);
 	assert balanceAfter == balancebefore - x;
 }
 
@@ -139,17 +168,17 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 
 
 /**
-mint and burn are inverse operations
+Mint and burn are inverse operations.
-Thus, totalSupply is back to initial state
+Therefore, both totalSupply and BalanceOf user are back to the initial state.
-BalanceOf user is back to initial state */
+*/
 rule inverseMintBurn(address a, uint256 x) {
 	env e;
+	address delegatedUser;
 	require sinvoke getIncentivesController(e) == 0;
 	uint256 index;
-	uint256 balancebefore = sinvoke balanceOf(e,a);
+	uint256 balancebefore = sinvoke balanceOf(e, a);
-	sinvoke mint(e,a,x,index);
+	sinvoke mint(e, delegatedUser, a, x, index);
-	sinvoke burn(e,a,x);
+	sinvoke burn(e, a, x);
-	uint256 balanceAfter = sinvoke balanceOf(e,a);
+	uint256 balanceAfter = sinvoke balanceOf(e, a);
-	assert balancebefore == balanceAfter, "burn is not inverse of mint";
+	assert balancebefore == balanceAfter, "burn is not the inverse of mint";
 }
-

specs/UserConfiguration.spec

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

specs/VariableDebtToken.spec

@@ -1,15 +1,12 @@
 using LendingPoolHarnessForVariableDebtToken as POOL
+
 /**
-TotalSupply is the sum of all users’ balances
+Checks that each possible opertaion changes the balance of at most one user.
-	
-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 a != b;
 	uint256 balanceABefore = sinvoke balanceOf(e, a);
 	uint256 balanceBBefore = sinvoke balanceOf(e, b);
 	 
@@ -19,14 +16,14 @@ rule balanceOfChange(address a, address b, method f)
 	uint256 balanceAAfter = sinvoke balanceOf(e, a);
 	uint256 balanceBAfter = sinvoke balanceOf(e, b);
 	
-	assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter );
+	assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter);
 }
 
-/*
+/**
-Check that the changed to total supply is coherent with the changes to balance
+Checks that the change to total supply is coherent with the change to the balance due to an operation
+(which is neither a burn nor a mint).
 */
-
+rule integirtyBalanceOfTotalSupply(address a, method f)
-rule integirtyBalanceOfTotalSupply(address a, method f )
 {
 	env e;
 	
@@ -36,17 +33,17 @@ rule integirtyBalanceOfTotalSupply(address a, method f )
 	calldataarg arg;
 	sinvoke f(e, arg); 
 	require (f.selector != burn(address, uint256, uint256).selector  &&
-		f.selector != mint(address, uint256, uint256).selector ) ;
+		f.selector != mint(address, 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
+/**
+Checks that the change to total supply is coherent with the change to the balance due to a burn operation.
 */
-
+rule integirtyBalanceOfTotalSupplyOnBurn(address a)
-rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
 {
 	env e;
 	
@@ -59,67 +56,75 @@ rule integirtyBalanceOfTotalSupplyOnBurn(address a, method f )
 	sinvoke burn(e, a, x, index); 
 	uint256 balanceAAfter = balanceOf(e, a);
 	uint256 totalSupplyAfter = totalSupply(e);
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert (balanceAAfter != balanceABefore  => (balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
-rule integirtyBalanceOfTotalSupplyOnMint(address a, method f )
+/**
+Checks that the change to total supply is coherent with the change to the balance due to a mint operation.
+*/
+rule integirtyBalanceOfTotalSupplyOnMint(address u, address delegatedUser)
 {
 	env e;
 	
-	uint256 balanceABefore = balanceOf(e, a);
+	uint256 balanceUBefore = balanceOf(e, u);
 	uint256 totalSupplyBefore = totalSupply(e);
 	 
 	uint256 x;
 	address asset;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
-	sinvoke mint(e, a, x, index); 
+	sinvoke mint(e, delegatedUser, u, x, index); 
-	uint256 balanceAAfter = balanceOf(e, a);
+	uint256 balanceUAfter = balanceOf(e, u);
 	uint256 totalSupplyAfter = totalSupply(e);
-	assert  (balanceAAfter != balanceABefore  => ( balanceAAfter - balanceABefore  == totalSupplyAfter - totalSupplyBefore));
+	assert (balanceUAfter != balanceUBefore  => (balanceUAfter - balanceUBefore  == totalSupplyAfter - totalSupplyBefore));
 }
 
 /**
-Minting an amount of x tokens for user u increases their balance by x, up to rounding errors. 
+Minting an amount of x tokens for user u increases her balance by x, up to rounding errors. 
-{ b= balanceOf(u,t) } 
+{ b = balanceOf(u,t) } 
-mint(u,x,index) 
+mint(delegatedUser, u, x, index) 
-{ balanceOf(u,t) = b + x }
+{ balanceOf(u,t) = b + x }.
 
+Also, if the minting is done by a user delegatedUser different than u, the balance of delegatedUser
+remains unchanged.
 */
-rule integrityMint(address a, uint256 x) {
+rule integrityMint(address u, address delegatedUser, uint256 x) {
 	env e;
 	address asset;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e,asset);
-	uint256 balancebefore = balanceOf(e, a);
+	uint256 balanceUBefore = balanceOf(e, u);
-	sinvoke mint(e, a, x, index);
+	uint256 balanceDelegatedUBefore = balanceOf(e, delegatedUser);
+	sinvoke mint(e, delegatedUser, u, x, index);
 	
-	uint256 balanceAfter = balanceOf(e, a);
+	uint256 balanceUAfter = balanceOf(e, u);
-	assert balanceAfter == balancebefore+x;
+	uint256 balanceDelegatedUAfter = balanceOf(e, delegatedUser);
+	
+	assert balanceUAfter == balanceUBefore + x && (u != delegatedUser => (balanceDelegatedUAfter == balanceDelegatedUBefore));
 }
 
 /**
-Mint is additive, can performed either all at once or gradually
+Mint is additive, namely it can performed either all at once or gradually:
-mint(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
+mint(delegatedUser, u, x, index); mint(delegatedUser, u, y, index) ~ mint(delegatedUser, u, x+y, index) at the same timestamp.
 */
-rule additiveMint(address a, uint256 x, uint256 y) {
+rule additiveMint(address a, address delegatedUser, 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, delegatedUser, a, x, index);
-	sinvoke mint(e, a, y, index);
+	sinvoke mint(e, delegatedUser, a, y, index);
 	uint256 balanceScenario1 = balanceOf(e, a);
-	uint t = x + y;
+	uint256 t = x + y;
-	sinvoke mint(e, a, t ,index) at initialStorage;
+	sinvoke mint(e, delegatedUser, 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’
+Burning an amount of x tokens for user u decreases her balance by x, up to rounding errors. 
-{bu = balanceOf(u) } 
+{ bu = balanceOf(u) } 
-	burn(u, u’, x)
+	burn(u, x)
-{balanceOf(u) = bu - x } 
+{ balanceOf(u) = bu - x }.
 */
 rule integrityBurn(address a, uint256 x) {
 	env e;
@@ -132,9 +137,8 @@ rule integrityBurn(address a, uint256 x) {
 	assert balanceAfter == balancebefore - x;
 }
 /**
-Minting is additive, i.e., it can be performed either all at once or in steps.
+Minting is additive, i.e., it can be performed either all at once or in steps:
-
+burn(u, x); burn(u, y) ~ burn(u, x+y) at the same timestamp.
-burn(u, u’, x); burn(u, u’, y) ~ burn(u, u’, x+y) 
 */
 rule additiveBurn(address a, uint256 x,  uint256 y) {
 	env e;
@@ -144,7 +148,7 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 	sinvoke burn(e, a, x, index);
 	sinvoke burn(e, a, y, index);
 	uint256 balanceScenario1 = balanceOf(e, a);
-	uint t = x + y;
+	uint256 t = x + y;
 	sinvoke burn(e, a, t ,index) at initialStorage;
 
 	uint256 balanceScenario2 = balanceOf(e, a);
@@ -152,22 +156,19 @@ rule additiveBurn(address a, uint256 x,  uint256 y) {
 }
 
 /**
-Minting and burning are inverse operations.
+Minting and burning are inverse operations:
-
+{ bu = balanceOf(u) } 
-{bu = balanceOf(u) } 
 mint(u,x); burn(u, u, x) 
-	{balanceOf(u) = bu } 
+{ balanceOf(u) = bu }.
 */
 rule inverseMintBurn(address a, uint256 x) {
 	env e;
 	address asset;
+	address delegatedUser;
 	uint256 index = POOL.getReserveNormalizedVariableDebt(e, asset);
 	uint256 balancebefore = balanceOf(e, a);
-	sinvoke mint(e, a, x, index);
+	sinvoke mint(e, delegatedUser, a, x, index);
 	sinvoke burn(e, a, x, index);
 	uint256 balanceAfter = balanceOf(e, a);
-	assert balancebefore == balanceAfter, "burn is not inverse of mint";
+	assert balancebefore == balanceAfter, "burn is not the inverse of mint";
 }
-
-
-

specs/harness/LendingPoolHarnessForVariableDebtToken.sol

@@ -2,11 +2,11 @@ pragma solidity 0.6.12;
 pragma experimental ABIEncoderV2;
 
 import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol';
-import {LendingPool} from '../../contracts/lendingpool/LendingPool.sol';
+import {LendingPool} from '../../contracts/protocol/lendingpool/LendingPool.sol';
 import {
   ILendingPoolAddressesProvider
 } from '../../contracts/interfaces/ILendingPoolAddressesProvider.sol';
-import {DataTypes} from '../protocol/libraries/types/DataTypes.sol';
+import {DataTypes} from '../../contracts/protocol/libraries/types/DataTypes.sol';
 
 /*
 Certora: Harness that delegates calls to the original LendingPool.
@@ -28,8 +28,8 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
     address asset,
     uint256 amount,
     address to
-  ) external override {
+  ) external override returns (uint256) {
-    originalPool.withdraw(asset, amount, to);
+    return originalPool.withdraw(asset, amount, to);
   }
 
   function borrow(
@@ -47,8 +47,8 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
     uint256 amount,
     uint256 rateMode,
     address onBehalfOf
-  ) external override {
+  ) external override returns (uint256) {
-    originalPool.repay(asset, amount, rateMode, onBehalfOf);
+    return originalPool.repay(asset, amount, rateMode, onBehalfOf);
   }
 
   function swapBorrowRateMode(address asset, uint256 rateMode) external override {
@@ -101,7 +101,7 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
     override
     returns (
       uint256 totalCollateralETH,
-      uint256 totalBorrowsETH,
+      uint256 totalDebtETH,
       uint256 availableBorrowsETH,
       uint256 currentLiquidationThreshold,
       uint256 ltv,

specs/harness/StableDebtTokenHarness.sol

@@ -1,7 +1,7 @@
 pragma solidity 0.6.12;
 
-import {StableDebtToken} from '../../contracts/tokenization/StableDebtToken.sol';
+import {StableDebtToken} from '../../contracts/protocol/tokenization/StableDebtToken.sol';
-import {IncentivizedERC20} from '../../contracts/tokenization/IncentivizedERC20.sol';
+import {IncentivizedERC20} from '../../contracts/protocol/tokenization/IncentivizedERC20.sol';
 
 contract StableDebtTokenHarness is StableDebtToken {
   constructor(
@@ -12,15 +12,22 @@ contract StableDebtTokenHarness is StableDebtToken {
     address incentivesController
   ) public StableDebtToken(pool, underlyingAsset, name, symbol, incentivesController) {}
 
-  function balanceOf(address account) public override view returns (uint256) {
+  /**
+   Simplification: The user accumulates no interest (the balance increase is always 0).
+   **/
+  function balanceOf(address account) public view override returns (uint256) {
     return IncentivizedERC20.balanceOf(account);
   }
 
-  function _calcTotalSupply(uint256 avgRate) internal override view returns (uint256) {
+  function _calcTotalSupply(uint256 avgRate) internal view override returns (uint256) {
     return IncentivizedERC20.totalSupply();
   }
 
   function getIncentivesController() public view returns (address) {
     return address(_incentivesController);
   }
+
+  function rayWadMul(uint256 aRay, uint256 bWad) external view returns (uint256) {
+    return aRay.rayMul(bWad.wadToRay());
+  }
 }

specs/harness/UserConfigurationHarness.sol

@@ -1,7 +1,10 @@
 pragma solidity 0.6.12;
 pragma experimental ABIEncoderV2;
 
-import {UserConfiguration} from '../../contracts/libraries/configuration/UserConfiguration.sol';
+import {
+  UserConfiguration
+} from '../../contracts/protocol/libraries/configuration/UserConfiguration.sol';
+import {DataTypes} from '../../contracts/protocol/libraries/types/DataTypes.sol';
 
 /*
 A wrapper contract for calling functions from the library UserConfiguration.
@@ -9,43 +12,31 @@ A wrapper contract for calling functions from the library UserConfiguration.
 contract UserConfigurationHarness {
   DataTypes.UserConfigurationMap internal usersConfig;
 
-  function setBorrowing(
+  function setBorrowing(uint256 reserveIndex, bool borrowing) public {
-    address user,
-    uint256 reserveIndex,
-    bool borrowing
-  ) public {
     UserConfiguration.setBorrowing(usersConfig, reserveIndex, borrowing);
   }
 
-  function setUsingAsCollateral(
+  function setUsingAsCollateral(uint256 reserveIndex, bool _usingAsCollateral) public {
-    address user,
-    uint256 reserveIndex,
-    bool _usingAsCollateral
-  ) public {
     UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral);
   }
 
-  function isUsingAsCollateralOrBorrowing(address user, uint256 reserveIndex)
+  function isUsingAsCollateralOrBorrowing(uint256 reserveIndex) public view returns (bool) {
-    public
-    view
-    returns (bool)
-  {
     return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex);
   }
 
-  function isBorrowing(address user, uint256 reserveIndex) public view returns (bool) {
+  function isBorrowing(uint256 reserveIndex) public view returns (bool) {
     return UserConfiguration.isBorrowing(usersConfig, reserveIndex);
   }
 
-  function isUsingAsCollateral(address user, uint256 reserveIndex) public view returns (bool) {
+  function isUsingAsCollateral(uint256 reserveIndex) public view returns (bool) {
     return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex);
   }
 
-  function isBorrowingAny(address user) public view returns (bool) {
+  function isBorrowingAny() public view returns (bool) {
     return UserConfiguration.isBorrowingAny(usersConfig);
   }
 
-  function isEmpty(address user) public view returns (bool) {
+  function isEmpty() public view returns (bool) {
     return UserConfiguration.isEmpty(usersConfig);
   }
 

tasks/full/1_address_provider.ts

@@ -16,9 +16,10 @@ import {
   getFirstSigner,
   getLendingPoolAddressesProviderRegistry,
 } from '../../helpers/contracts-getters';
-import { isAddress } from 'ethers/lib/utils';
+import { formatEther, isAddress, parseEther } from 'ethers/lib/utils';
 import { isZeroAddress } from 'ethereumjs-util';
 import { Signer } from 'ethers';
+import { parse } from 'path';
 
 task(
   'full:deploy-address-provider',
@@ -59,6 +60,8 @@ task(
         params: [providerRegistryOwner],
       });
       signer = DRE.ethers.provider.getSigner(providerRegistryOwner);
+      const firstAccount = await getFirstSigner();
+      await firstAccount.sendTransaction({ value: parseEther('10'), to: providerRegistryOwner });
     } else {
       signer = await getFirstSigner();
       const deployerAddress = await signer.getAddress();
@@ -69,7 +72,6 @@ task(
       }
     }
     // 1. Address Provider Registry instance
-
     const addressesProviderRegistry = (
       await getLendingPoolAddressesProviderRegistry(providerRegistryAddress)
     ).connect(signer);

tasks/helpers/deploy-new-asset.ts

@@ -0,0 +1,101 @@
+import { task } from 'hardhat/config';
+import { EthereumNetwork } from '../../helpers/types';
+import { getTreasuryAddress } from '../../helpers/configuration';
+import * as marketConfigs from '../../markets/aave';
+import * as reserveConfigs from '../../markets/aave/reservesConfigs';
+import { chooseATokenDeployment } from '../../helpers/init-helpers';
+import { getLendingPoolAddressesProvider } from './../../helpers/contracts-getters';
+import {
+  deployDefaultReserveInterestRateStrategy,
+  deployStableDebtToken,
+  deployVariableDebtToken,
+} from './../../helpers/contracts-deployments';
+import { setDRE } from '../../helpers/misc-utils';
+import { ZERO_ADDRESS } from './../../helpers/constants';
+
+const LENDING_POOL_ADDRESS_PROVIDER = {
+  main: '0xb53c1a33016b2dc2ff3653530bff1848a515c8c5',
+  kovan: '0x652B2937Efd0B5beA1c8d54293FC1289672AFC6b',
+};
+
+const isSymbolValid = (symbol: string, network: EthereumNetwork) =>
+  Object.keys(reserveConfigs).includes('strategy' + symbol) &&
+  marketConfigs.AaveConfig.ReserveAssets[network][symbol] &&
+  marketConfigs.AaveConfig.ReservesConfig[symbol] === reserveConfigs['strategy' + symbol];
+
+task('external:deploy-new-asset', 'Deploy A token, Debt Tokens, Risk Parameters')
+  .addParam('symbol', `Asset symbol, needs to have configuration ready`)
+  .addFlag('verify', 'Verify contracts at Etherscan')
+  .setAction(async ({ verify, symbol }, localBRE) => {
+    const network = localBRE.network.name;
+    if (!isSymbolValid(symbol, network as EthereumNetwork)) {
+      throw new Error(
+        `
+WRONG RESERVE ASSET SETUP:
+        The symbol ${symbol} has no reserve Config and/or reserve Asset setup.
+        update /markets/aave/index.ts and add the asset address for ${network} network
+        update /markets/aave/reservesConfigs.ts and add parameters for ${symbol}
+        `
+      );
+    }
+    setDRE(localBRE);
+    const strategyParams = reserveConfigs['strategy' + symbol];
+    const reserveAssetAddress =
+      marketConfigs.AaveConfig.ReserveAssets[localBRE.network.name][symbol];
+    const deployCustomAToken = chooseATokenDeployment(strategyParams.aTokenImpl);
+    const addressProvider = await getLendingPoolAddressesProvider(
+      LENDING_POOL_ADDRESS_PROVIDER[network]
+    );
+    const poolAddress = await addressProvider.getLendingPool();
+    const treasuryAddress = await getTreasuryAddress(marketConfigs.AaveConfig);
+    const aToken = await deployCustomAToken(
+      [
+        poolAddress,
+        reserveAssetAddress,
+        treasuryAddress,
+        `Aave interest bearing ${symbol}`,
+        `a${symbol}`,
+        ZERO_ADDRESS,
+      ],
+      verify
+    );
+    const stableDebt = await deployStableDebtToken(
+      [
+        poolAddress,
+        reserveAssetAddress,
+        `Aave stable debt bearing ${symbol}`,
+        `stableDebt${symbol}`,
+        ZERO_ADDRESS,
+      ],
+      verify
+    );
+    const variableDebt = await deployVariableDebtToken(
+      [
+        poolAddress,
+        reserveAssetAddress,
+        `Aave variable debt bearing ${symbol}`,
+        `variableDebt${symbol}`,
+        ZERO_ADDRESS,
+      ],
+      verify
+    );
+    const rates = await deployDefaultReserveInterestRateStrategy(
+      [
+        addressProvider.address,
+        strategyParams.optimalUtilizationRate,
+        strategyParams.baseVariableBorrowRate,
+        strategyParams.variableRateSlope1,
+        strategyParams.variableRateSlope2,
+        strategyParams.stableRateSlope1,
+        strategyParams.stableRateSlope2,
+      ],
+      verify
+    );
+    console.log(`
+    New interest bearing asset deployed on ${network}:
+    Interest bearing a${symbol} address: ${aToken.address}
+    Variable Debt variableDebt${symbol} address: ${variableDebt.address}
+    Stable Debt stableDebt${symbol} address: ${stableDebt.address}
+    Strategy Implementation for ${symbol} address: ${rates.address}
+    `);
+  });

tasks/misc/initialize-tokens.ts

@@ -0,0 +1,96 @@
+import { task } from 'hardhat/config';
+import { getParamPerNetwork } from '../../helpers/contracts-helpers';
+import { loadPoolConfig, ConfigNames, getTreasuryAddress } from '../../helpers/configuration';
+import { eEthereumNetwork, ICommonConfiguration } from '../../helpers/types';
+import { waitForTx } from '../../helpers/misc-utils';
+import { initTokenReservesByHelper } from '../../helpers/init-helpers';
+import { exit } from 'process';
+import {
+  getFirstSigner,
+  getLendingPoolAddressesProvider,
+  getLendingPoolAddressesProviderRegistry,
+} from '../../helpers/contracts-getters';
+import { Signer } from 'ethers';
+import { formatEther, parseEther } from 'ethers/lib/utils';
+
+task('full:initialize-tokens', 'Initialize lending pool configuration.')
+  .addParam('pool', `Pool name to retrieve configuration, supported: ${Object.values(ConfigNames)}`)
+  .addParam('ratesDeployer', `RatesHelper address `)
+  .addParam('dataProvider', `Data provider address`)
+  .addFlag('verify')
+  .setAction(async ({ verify, pool, dataProvider, ratesDeployer }, DRE) => {
+    try {
+      await DRE.run('set-DRE');
+      let signer: Signer;
+      const network =
+        process.env.MAINNET_FORK === 'true'
+          ? eEthereumNetwork.main
+          : <eEthereumNetwork>DRE.network.name;
+      const poolConfig = loadPoolConfig(pool);
+      const { ReserveAssets, ReservesConfig } = poolConfig as ICommonConfiguration;
+
+      const reserveAssets = await getParamPerNetwork(ReserveAssets, network);
+
+      const treasuryAddress = await getTreasuryAddress(poolConfig);
+      const providerRegistryAddress = getParamPerNetwork(poolConfig.ProviderRegistry, network);
+      const providerRegistryOwner = getParamPerNetwork(poolConfig.ProviderRegistryOwner, network);
+
+      const providerRegistry = await getLendingPoolAddressesProviderRegistry(
+        providerRegistryAddress
+      );
+
+      const providers = await providerRegistry.getAddressesProvidersList();
+
+      const addressesProvider = await getLendingPoolAddressesProvider(providers[0]); // Checks first provider
+
+      const admin = await addressesProvider.getPoolAdmin();
+      if (!reserveAssets) {
+        throw 'Reserve assets is undefined. Check ReserveAssets configuration at config directory';
+      }
+
+      if (process.env.MAINNET_FORK === 'true') {
+        await DRE.network.provider.request({
+          method: 'hardhat_impersonateAccount',
+          params: [providerRegistryOwner],
+        });
+        signer = DRE.ethers.provider.getSigner(providerRegistryOwner);
+        const user = await getFirstSigner();
+        await waitForTx(
+          await user.sendTransaction({ to: await signer.getAddress(), value: parseEther('10') })
+        );
+
+        const balance = await signer.getBalance();
+        console.log('signer balance', formatEther(balance));
+      } else {
+        signer = await getFirstSigner();
+        const deployerAddress = await signer.getAddress();
+        if (providerRegistryOwner !== (await signer.getAddress())) {
+          throw Error(
+            `Current signer is not provider registry owner. \nCurrent deployer address: ${deployerAddress} \nExpected address: ${poolConfig.ProviderRegistryOwner}`
+          );
+        }
+      }
+
+      // Init unitilialized reserves
+      await initTokenReservesByHelper(
+        ReservesConfig,
+        reserveAssets,
+        admin,
+        addressesProvider.address,
+        ratesDeployer,
+        dataProvider,
+        signer,
+        treasuryAddress,
+        verify
+      );
+
+      // Show contracts state
+      await DRE.run('print-config', {
+        pool: 'Aave',
+        dataProvider,
+      });
+    } catch (err) {
+      console.error(err);
+      exit(1);
+    }
+  });

tasks/misc/print-config.ts

@@ -68,7 +68,7 @@ task('print-config', 'Inits the DRE, to have access to all the plugins')
       const reserveData = await protocolDataProvider.getReserveConfigurationData(address);
       const tokensAddresses = await protocolDataProvider.getReserveTokensAddresses(address);
       fields.forEach((field, index) => {
-        console.log(`  - ${field}:`, reserveData[index].toString());
+        console.log(`  - ${field}:`, reserveData[field].toString());
       });
       tokensFields.forEach((field, index) => {
         console.log(`  - ${field}:`, tokensAddresses[index]);

tasks/verifications/1_general.ts

@@ -1,7 +1,13 @@
-import {zeroAddress} from 'ethereumjs-util';
+import { error } from 'console';
-import {task} from 'hardhat/config';
+import { zeroAddress } from 'ethereumjs-util';
-import {loadPoolConfig, ConfigNames, getWethAddress} from '../../helpers/configuration';
+import { task } from 'hardhat/config';
-import {ZERO_ADDRESS} from '../../helpers/constants';
+import {
+  loadPoolConfig,
+  ConfigNames,
+  getWethAddress,
+  getTreasuryAddress,
+} from '../../helpers/configuration';
+import { ZERO_ADDRESS } from '../../helpers/constants';
 import {
   getAaveProtocolDataProvider,
   getAddressById,
@@ -16,21 +22,31 @@ import {
   getWalletProvider,
   getWETHGateway,
 } from '../../helpers/contracts-getters';
-import {getParamPerNetwork} from '../../helpers/contracts-helpers';
+import { getParamPerNetwork } from '../../helpers/contracts-helpers';
-import {verifyContract} from '../../helpers/etherscan-verification';
+import { verifyContract } from '../../helpers/etherscan-verification';
-import {eEthereumNetwork, ICommonConfiguration} from '../../helpers/types';
+import { notFalsyOrZeroAddress } from '../../helpers/misc-utils';
+import { eEthereumNetwork, ICommonConfiguration } from '../../helpers/types';
 
 task('verify:general', 'Deploy oracles for dev enviroment')
   .addFlag('all', 'Verify all contracts at Etherscan')
   .addParam('pool', `Pool name to retrieve configuration, supported: ${Object.values(ConfigNames)}`)
-  .setAction(async ({all, pool}, localDRE) => {
+  .setAction(async ({ all, pool }, localDRE) => {
     await localDRE.run('set-DRE');
     const network = localDRE.network.name as eEthereumNetwork;
     const poolConfig = loadPoolConfig(pool);
-    const {ReserveAssets, ReservesConfig} = poolConfig as ICommonConfiguration;
+    const {
+      ReserveAssets,
+      ReservesConfig,
+      ProviderRegistry,
+      MarketId,
+    } = poolConfig as ICommonConfiguration;
+    const treasuryAddress = await getTreasuryAddress(poolConfig);
 
+    const registryAddress = getParamPerNetwork(ProviderRegistry, network);
     const addressesProvider = await getLendingPoolAddressesProvider();
-    const addressesProviderRegistry = await getLendingPoolAddressesProviderRegistry();
+    const addressesProviderRegistry = notFalsyOrZeroAddress(registryAddress)
+      ? await getLendingPoolAddressesProviderRegistry(registryAddress)
+      : await getLendingPoolAddressesProviderRegistry();
     const lendingPoolProxy = await getLendingPool();
     const lendingPoolConfigurator = await getLendingPoolConfiguratorProxy();
     const lendingPoolCollateralManager = await getLendingPoolCollateralManager();
@@ -45,7 +61,7 @@ task('verify:general', 'Deploy oracles for dev enviroment')
 
       // Address Provider
       console.log('\n- Verifying address provider...\n');
-      await verifyContract(addressesProvider.address, []);
+      await verifyContract(addressesProvider.address, [MarketId]);
 
       // Address Provider Registry
       console.log('\n- Verifying address provider registry...\n');
@@ -69,7 +85,7 @@ task('verify:general', 'Deploy oracles for dev enviroment')
 
       // Wallet balance provider
       console.log('\n- Verifying  Wallet Balance Provider...\n');
-      await verifyContract(walletProvider.address, [addressesProvider.address]);
+      await verifyContract(walletProvider.address, []);
 
       // WETHGateway
       console.log('\n- Verifying  WETHGateway...\n');
@@ -90,86 +106,22 @@ task('verify:general', 'Deploy oracles for dev enviroment')
     console.log('\n- Verifying  Lending Pool Collateral Manager Proxy...\n');
     await verifyContract(lendingPoolCollateralManager.address, []);
 
-    // Tokens verification
-    const DAI = getParamPerNetwork(ReserveAssets, network).DAI;
-    const stableDebtDai = await getAddressById('stableDebtDAI');
-    const variableDebtDai = await getAddressById('variableDebtDAI');
-    const aDAI = await getAddressById('aDAI');
-    const {
-      stableDebtTokenAddress,
-      variableDebtTokenAddress,
-      aTokenAddress,
-      interestRateStrategyAddress,
-    } = await lendingPoolProxy.getReserveData(DAI);
-    const {
-      baseVariableBorrowRate,
-      variableRateSlope1,
-      variableRateSlope2,
-      stableRateSlope1,
-      stableRateSlope2,
-    } = ReservesConfig.DAI;
-
-    // Proxy Stable Debt
-    console.log('\n- Verifying DAI Stable Debt Token proxy...\n');
-    await verifyContract(stableDebtTokenAddress, [lendingPoolConfigurator.address]);
-
-    // Proxy Variable Debt
-    console.log('\n- Verifying DAI Variable Debt Token proxy...\n');
-    await verifyContract(variableDebtTokenAddress, [lendingPoolConfigurator.address]);
-
-    // Proxy aToken
-    console.log('\n- Verifying aDAI Token proxy...\n');
-    await verifyContract(aTokenAddress, [lendingPoolConfigurator.address]);
-
-    // Strategy Rate
-    console.log('\n- Verifying Strategy rate...\n');
-    await verifyContract(interestRateStrategyAddress, [
-      addressesProvider.address,
-      baseVariableBorrowRate,
-      variableRateSlope1,
-      variableRateSlope2,
-      stableRateSlope1,
-      stableRateSlope2,
-    ]);
-
-    // aToken
-    console.log('\n- Verifying aToken...\n');
-    await verifyContract(aDAI, [
-      lendingPoolProxy.address,
-      DAI,
-      ZERO_ADDRESS,
-      'Aave interest bearing DAI',
-      'aDAI',
-      ZERO_ADDRESS,
-    ]);
-    // stableDebtToken
-    console.log('\n- Verifying StableDebtToken...\n');
-    await verifyContract(stableDebtDai, [
-      lendingPoolProxy.address,
-      DAI,
-      'Aave stable debt bearing DAI',
-      'stableDebtDAI',
-      ZERO_ADDRESS,
-    ]);
-    // variableDebtToken
-    console.log('\n- Verifying VariableDebtToken...\n');
-    await verifyContract(variableDebtDai, [
-      lendingPoolProxy.address,
-      DAI,
-      'Aave variable debt bearing DAI',
-      'variableDebtDAI',
-      ZERO_ADDRESS,
-    ]);
     // DelegatedAwareAToken
     console.log('\n- Verifying DelegatedAwareAToken...\n');
     const UNI = getParamPerNetwork(ReserveAssets, network).UNI;
     const aUNI = await getAddressById('aUNI');
+    if (aUNI) {
+      console.log('Verifying aUNI');
       await verifyContract(aUNI, [
         lendingPoolProxy.address,
         UNI,
-      ZERO_ADDRESS,
+        treasuryAddress,
         'Aave interest bearing UNI',
         'aUNI',
         ZERO_ADDRESS,
       ]);
+    } else {
+      console.error('Missing aUNI address at JSON DB. Skipping...');
+    }
+    console.log('Finished verifications.');
   });

tasks/verifications/2_tokens.ts

@@ -1,5 +1,10 @@
 import { task } from 'hardhat/config';
-import { loadPoolConfig, ConfigNames, getWethAddress } from '../../helpers/configuration';
+import {
+  loadPoolConfig,
+  ConfigNames,
+  getWethAddress,
+  getTreasuryAddress,
+} from '../../helpers/configuration';
 import { ZERO_ADDRESS } from '../../helpers/constants';
 import {
   getAddressById,
@@ -18,6 +23,7 @@ task('verify:tokens', 'Deploy oracles for dev enviroment')
     const network = localDRE.network.name as eEthereumNetwork;
     const poolConfig = loadPoolConfig(pool);
     const { ReserveAssets, ReservesConfig } = poolConfig as ICommonConfiguration;
+    const treasuryAddress = await getTreasuryAddress(poolConfig);
 
     const addressesProvider = await getLendingPoolAddressesProvider();
     const lendingPoolProxy = await getLendingPool();
@@ -77,18 +83,20 @@ task('verify:tokens', 'Deploy oracles for dev enviroment')
       const variableDebt = await getAddressById(`variableDebt${token}`);
       const aToken = await getAddressById(`a${token}`);
 
-      // aToken
+      if (aToken) {
         console.log('\n- Verifying aToken...\n');
         await verifyContract(aToken, [
           lendingPoolProxy.address,
           tokenAddress,
-        ZERO_ADDRESS,
+          treasuryAddress,
           `Aave interest bearing ${token}`,
           `a${token}`,
           ZERO_ADDRESS,
         ]);
-
+      } else {
-      // stableDebtToken
+        console.error(`Skipping aToken verify for ${token}. Missing address at JSON DB.`);
+      }
+      if (stableDebt) {
         console.log('\n- Verifying StableDebtToken...\n');
         await verifyContract(stableDebt, [
           lendingPoolProxy.address,
@@ -97,8 +105,10 @@ task('verify:tokens', 'Deploy oracles for dev enviroment')
           `stableDebt${token}`,
           ZERO_ADDRESS,
         ]);
-
+      } else {
-      // variableDebtToken
+        console.error(`Skipping stable debt verify for ${token}. Missing address at JSON DB.`);
+      }
+      if (variableDebt) {
         console.log('\n- Verifying VariableDebtToken...\n');
         await verifyContract(variableDebt, [
           lendingPoolProxy.address,
@@ -107,5 +117,8 @@ task('verify:tokens', 'Deploy oracles for dev enviroment')
           `variableDebt${token}`,
           ZERO_ADDRESS,
         ]);
+      } else {
+        console.error(`Skipping variable debt verify for ${token}. Missing address at JSON DB.`);
+      }
     }
   });