Merge branch 'certora/integrationStep2' into 'master'

Integrating Certora FV into the CI: Step 2

Closes #106

See merge request aave-tech/protocol-v2!182
This commit is contained in:
The-3D 2020-12-03 14:44:09 +00:00
commit dbd77ad931
9 changed files with 166 additions and 111 deletions

View File

@ -24,3 +24,20 @@ 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-beta==0.4.1
- 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 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableDebtToken --staging
- certoraRun specs/harness/UserConfigurationHarness.sol --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging
- 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 --staging

View File

@ -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 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --staging

View File

@ -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 --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging

View File

@ -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 --staging

View File

@ -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 balanceBBefore = sinvoke balanceOf(e,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);
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 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 );
uint256 balanceAAfter = sinvoke balanceOf(e,a);
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));
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 balanceABefore = sinvoke balanceOf(e, a);
uint256 totalSupplyBefore = sinvoke totalSupply(e);
uint256 x;
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));
else
assert (totalSupplyAfter == 0 );
if(totalSupplyBefore > x) {
/* The amount being burned (x) is smaller than the total supply */
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(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
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.
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,a,y,index);
uint256 balanceScenario1 = sinvoke balanceOf(e,a);
sinvoke mint(e, delegatedUser, a, x, index);
sinvoke mint(e, delegatedUser, a, y, index);
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
Thus, totalSupply is back to initial state
BalanceOf user is back to initial state */
Mint and burn are inverse operations.
Therefore, both totalSupply and BalanceOf user are back to the 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);
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";
}
uint256 balancebefore = sinvoke balanceOf(e, a);
sinvoke mint(e, delegatedUser, a, x, index);
sinvoke burn(e, a, x);
uint256 balanceAfter = sinvoke balanceOf(e, a);
assert balancebefore == balanceAfter, "burn is not the inverse of mint";
}

View File

@ -1,15 +1,12 @@
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
/**
Checks 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, method f )
rule integirtyBalanceOfTotalSupplyOnBurn(address a)
{
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);
uint256 balanceAAfter = balanceOf(e, a);
sinvoke mint(e, delegatedUser, u, x, index);
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.
{ b= balanceOf(u,t) }
mint(u,x,index)
{ balanceOf(u,t) = b + x }
Minting an amount of x tokens for user u increases her balance by x, up to rounding errors.
{ b = balanceOf(u,t) }
mint(delegatedUser, u, x, index)
{ 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);
sinvoke mint(e, a, x, index);
uint256 balanceUBefore = balanceOf(e, u);
uint256 balanceDelegatedUBefore = balanceOf(e, delegatedUser);
sinvoke mint(e, delegatedUser, u, x, index);
uint256 balanceAfter = balanceOf(e, a);
assert balanceAfter == balancebefore+x;
uint256 balanceUAfter = balanceOf(e, u);
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(u,x); mint(u,y) ~ mint(u,x+y) at the same timestamp
Mint is additive, namely it can performed either all at once or gradually:
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, a, y, index);
sinvoke mint(e, delegatedUser, a, x, index);
sinvoke mint(e, delegatedUser, a, y, index);
uint256 balanceScenario1 = balanceOf(e, a);
uint t = x + y;
sinvoke mint(e, a, t ,index) at initialStorage;
uint256 t = x + y;
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
{bu = balanceOf(u) }
burn(u, u, x)
{balanceOf(u) = bu - x }
Burning an amount of x tokens for user u decreases her balance by x, up to rounding errors.
{ bu = balanceOf(u) }
burn(u, 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.
burn(u, u, x); burn(u, u, y) ~ burn(u, u, x+y)
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.
*/
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.
{bu = balanceOf(u) }
Minting and burning are inverse operations:
{ 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";
}
uint256 balanceAfter = balanceOf(e, a);
assert balancebefore == balanceAfter, "burn is not the inverse of mint";
}

View File

@ -2,9 +2,9 @@ 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
ILendingPoolAddressesProvider
} from '../../contracts/interfaces/ILendingPoolAddressesProvider.sol';
import {DataTypes} from '../protocol/libraries/types/DataTypes.sol';
@ -101,7 +101,7 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool {
override
returns (
uint256 totalCollateralETH,
uint256 totalBorrowsETH,
uint256 totalDebtETH,
uint256 availableBorrowsETH,
uint256 currentLiquidationThreshold,
uint256 ltv,

View File

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

View File

@ -1,7 +1,7 @@
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';
/*
A wrapper contract for calling functions from the library UserConfiguration.