diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3838193e..a722497e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -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 + diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh index 8903f2f9..653eaff1 100644 --- a/runStableTokenCLI.sh +++ b/runStableTokenCLI.sh @@ -1 +1 @@ -certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.8 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond --cache StableDebtToken --staging master \ No newline at end of file +certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --staging \ No newline at end of file diff --git a/runUserConfigCLI.sh b/runUserConfigCLI.sh index f3ddbacc..776c032e 100644 --- a/runUserConfigCLI.sh +++ b/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 --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh index 483e152e..5d549a8b 100644 --- a/runVariableTokenCLI.sh +++ b/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 \ No newline at end of file +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 \ No newline at end of file diff --git a/specs/StableDebtToken.spec b/specs/StableDebtToken.spec index 0d6e0c5d..a486d335 100644 --- a/specs/StableDebtToken.spec +++ b/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 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"; +} \ No newline at end of file diff --git a/specs/VariableDebtToken.spec b/specs/VariableDebtToken.spec index 73e7e39c..eb19d1b4 100644 --- a/specs/VariableDebtToken.spec +++ b/specs/VariableDebtToken.spec @@ -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"; +} \ No newline at end of file diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol index b366d22a..57752c58 100644 --- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol +++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol @@ -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, diff --git a/specs/harness/StableDebtTokenHarness.sol b/specs/harness/StableDebtTokenHarness.sol index 69a9aa8a..1218e0d9 100644 --- a/specs/harness/StableDebtTokenHarness.sol +++ b/specs/harness/StableDebtTokenHarness.sol @@ -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()); + } } diff --git a/specs/harness/UserConfigurationHarness.sol b/specs/harness/UserConfigurationHarness.sol index 38ca2686..00a8da90 100644 --- a/specs/harness/UserConfigurationHarness.sol +++ b/specs/harness/UserConfigurationHarness.sol @@ -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.