From 1ce83f27afa4f2b63aabfdadab065acf49d48cea Mon Sep 17 00:00:00 2001 From: pistiner <59415933+orpistiner@users.noreply.github.com> Date: Thu, 3 Dec 2020 17:01:13 +0200 Subject: [PATCH 1/7] Fixed imports --- specs/harness/LendingPoolHarnessForVariableDebtToken.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol index 7717c9d5..351f54aa 100644 --- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol +++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol @@ -1,7 +1,7 @@ pragma solidity 0.6.12; pragma experimental ABIEncoderV2; -import {ILendingPool} from '../../contracts/protocol/interfaces/ILendingPool.sol'; +import {ILendingPool} from '../../contracts/interfaces/ILendingPool.sol'; import {LendingPool} from '../../contracts/protocol/lendingpool/LendingPool.sol'; import { ILendingPoolAddressesProvider From 6b9bed65c4490694fada3dd454be89d520d8b42b Mon Sep 17 00:00:00 2001 From: pistiner <59415933+orpistiner@users.noreply.github.com> Date: Thu, 3 Dec 2020 17:20:11 +0200 Subject: [PATCH 2/7] Fix compilation errors --- specs/UserConfiguration.spec | 66 +++++++++++----------- specs/harness/UserConfigurationHarness.sol | 14 ++--- 2 files changed, 40 insertions(+), 40 deletions(-) diff --git a/specs/UserConfiguration.spec b/specs/UserConfiguration.spec index 14fce3a6..41a4f93e 100644 --- a/specs/UserConfiguration.spec +++ b/specs/UserConfiguration.spec @@ -1,66 +1,66 @@ methods { - setBorrowing(address, uint256, bool) envfree - setUsingAsCollateral(address, uint256, bool) envfree - isUsingAsCollateralOrBorrowing(address, uint256) returns bool envfree - isBorrowing(address, uint256) returns bool envfree - isUsingAsCollateral(address, uint256) returns bool envfree - isBorrowingAny(address ) returns bool envfree - isEmpty(address ) returns bool envfree + setBorrowing(uint256, bool) envfree + setUsingAsCollateral(uint256, bool) envfree + isUsingAsCollateralOrBorrowing(uint256) returns bool envfree + isBorrowing(uint256) returns bool envfree + isUsingAsCollateral(uint256) returns bool envfree + isBorrowingAny() returns bool envfree + isEmpty() returns bool envfree } -invariant empty(address user, uint256 reserveIndex ) - isEmpty(user) => !isBorrowingAny(user) && !isUsingAsCollateralOrBorrowing(user, reserveIndex) +invariant empty(uint256 reserveIndex) + isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(reserveIndex) -invariant notEmpty(address user, uint256 reserveIndex ) - ( isBorrowingAny(user) || isUsingAsCollateral(user, reserveIndex)) => !isEmpty(user) +invariant notEmpty(uint256 reserveIndex) + (isBorrowingAny() || isUsingAsCollateral(reserveIndex)) => !isEmpty() -invariant borrowing(address user, uint256 reserveIndex ) - isBorrowing(user, reserveIndex) => isBorrowingAny(user) +invariant borrowing(uint256 reserveIndex ) + isBorrowing(reserveIndex) => isBorrowingAny() -invariant collateralOrBorrowing(address user, uint256 reserveIndex ) - ( isUsingAsCollateral(user, reserveIndex) || isBorrowing(user, reserveIndex) ) <=> isUsingAsCollateralOrBorrowing(user, reserveIndex) +invariant collateralOrBorrowing(uint256 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); - assert isBorrowing(user, reserveIndex) == borrowing, "unexpected result"; + setBorrowing(reserveIndex, borrowing); + 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 otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther); + bool otherReserveBorrowing = isBorrowing(reserveIndexOther); + bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther); - setBorrowing(user, reserveIndex, borrowing); - assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) && - otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve"; + setBorrowing(reserveIndex, borrowing); + assert otherReserveBorrowing == isBorrowing(reserveIndexOther) && + 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); - assert isUsingAsCollateral(user, reserveIndex) == usingAsCollateral, "unexpected result"; + setUsingAsCollateral(reserveIndex, usingAsCollateral); + 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 otherReserveCollateral = isUsingAsCollateral(user,reserveIndexOther); + bool otherReserveBorrowing = isBorrowing(reserveIndexOther); + bool otherReserveCollateral = isUsingAsCollateral(reserveIndexOther); - setUsingAsCollateral(user, reserveIndex, usingAsCollateral); - assert otherReserveBorrowing == isBorrowing(user, reserveIndexOther) && - otherReserveCollateral == isUsingAsCollateral(user,reserveIndexOther), "changed to other reserve"; + setUsingAsCollateral(reserveIndex, usingAsCollateral); + assert otherReserveBorrowing == isBorrowing(reserveIndexOther) && + otherReserveCollateral == isUsingAsCollateral(reserveIndexOther), "changed to other reserve"; } diff --git a/specs/harness/UserConfigurationHarness.sol b/specs/harness/UserConfigurationHarness.sol index 00a8da90..4487773b 100644 --- a/specs/harness/UserConfigurationHarness.sol +++ b/specs/harness/UserConfigurationHarness.sol @@ -2,15 +2,16 @@ pragma solidity 0.6.12; pragma experimental ABIEncoderV2; 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. */ contract UserConfigurationHarness { + DataTypes.UserConfigurationMap internal usersConfig; function setBorrowing( - address user, uint256 reserveIndex, bool borrowing ) public { @@ -18,14 +19,13 @@ contract UserConfigurationHarness { } function setUsingAsCollateral( - 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) @@ -33,19 +33,19 @@ contract UserConfigurationHarness { 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); } From 0293b082a946c696bd06627363557b04b98fcfb4 Mon Sep 17 00:00:00 2001 From: pistiner <59415933+orpistiner@users.noreply.github.com> Date: Thu, 3 Dec 2020 17:28:25 +0200 Subject: [PATCH 3/7] Fixed imports --- specs/harness/LendingPoolHarnessForVariableDebtToken.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol index 351f54aa..b2d2e878 100644 --- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol +++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol @@ -6,7 +6,7 @@ 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. From 291b92b5a36cbb14e879e00e6e9efe04c51bdd27 Mon Sep 17 00:00:00 2001 From: pistiner <59415933+orpistiner@users.noreply.github.com> Date: Thu, 3 Dec 2020 17:33:23 +0200 Subject: [PATCH 4/7] Fixed compilation errors --- ...LendingPoolHarnessForVariableDebtToken.sol | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol index b2d2e878..02b5a4b7 100644 --- a/specs/harness/LendingPoolHarnessForVariableDebtToken.sol +++ b/specs/harness/LendingPoolHarnessForVariableDebtToken.sol @@ -28,8 +28,8 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool { address asset, uint256 amount, address to - ) external override { - originalPool.withdraw(asset, amount, to); + ) external override returns (uint256) { + return originalPool.withdraw(asset, amount, to); } function borrow( @@ -47,8 +47,8 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool { uint256 amount, uint256 rateMode, address onBehalfOf - ) external override { - originalPool.repay(asset, amount, rateMode, onBehalfOf); + ) external override returns (uint256) { + return originalPool.repay(asset, amount, rateMode, onBehalfOf); } function swapBorrowRateMode(address asset, uint256 rateMode) external override { @@ -96,17 +96,17 @@ contract LendingPoolHarnessForVariableDebtToken is ILendingPool { } function getUserAccountData(address user) - external - view - override - returns ( - uint256 totalCollateralETH, - uint256 totalBorrowsETH, - uint256 availableBorrowsETH, - uint256 currentLiquidationThreshold, - uint256 ltv, - uint256 healthFactor - ) + external + view + override + returns ( + uint256 totalCollateralETH, + uint256 totalDebtETH, + uint256 availableBorrowsETH, + uint256 currentLiquidationThreshold, + uint256 ltv, + uint256 healthFactor + ) { return originalPool.getUserAccountData(user); } From cd851770206a89daf941cd836863e2dd0e4e5119 Mon Sep 17 00:00:00 2001 From: pistiner Date: Thu, 3 Dec 2020 15:46:05 +0000 Subject: [PATCH 5/7] Update .gitlab-ci.yml --- .gitlab-ci.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a722497e..bbe8b021 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -31,13 +31,13 @@ certora-test: before_script: - apt-get update || apt-get update - apt-get install -y software-properties-common - - pip3 install certora-cli-beta==0.4.1 + - 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 --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 + - 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 From 38039a3b751cf6e19f31df398209e0670a7eb7d3 Mon Sep 17 00:00:00 2001 From: pistiner <59415933+orpistiner@users.noreply.github.com> Date: Thu, 3 Dec 2020 18:13:22 +0200 Subject: [PATCH 6/7] Updated runners --- runStableTokenCLI.sh | 2 +- runUserConfigCLI.sh | 2 +- runVariableTokenCLI.sh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh index 653eaff1..36de9b31 100644 --- a/runStableTokenCLI.sh +++ b/runStableTokenCLI.sh @@ -1 +1 @@ -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 +certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --solc_args '--optimize' --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cloud \ No newline at end of file diff --git a/runUserConfigCLI.sh b/runUserConfigCLI.sh index 776c032e..fbf2104f 100644 --- a/runUserConfigCLI.sh +++ b/runUserConfigCLI.sh @@ -1 +1 @@ -certoraRun specs/harness/UserConfigurationHarness.sol --solc solc6.12 --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --staging +certoraRun specs/harness/UserConfigurationHarness.sol --solc solc6.12 --solc_args '--optimize' --verify UserConfigurationHarness:specs/UserConfiguration.spec --solc_args '--optimize' --settings -useBitVectorTheory --cloud diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh index 5d549a8b..28f94145 100644 --- a/runVariableTokenCLI.sh +++ b/runVariableTokenCLI.sh @@ -1 +1 @@ -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 +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 --cloud \ No newline at end of file From 2fb53195f519c2d971c6d00e45e98f77e6b616d8 Mon Sep 17 00:00:00 2001 From: pistiner <59415933+orpistiner@users.noreply.github.com> Date: Thu, 3 Dec 2020 18:17:31 +0200 Subject: [PATCH 7/7] Updated runners --- runStableTokenCLI.sh | 2 +- runVariableTokenCLI.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/runStableTokenCLI.sh b/runStableTokenCLI.sh index 36de9b31..25a7daef 100644 --- a/runStableTokenCLI.sh +++ b/runStableTokenCLI.sh @@ -1 +1 @@ -certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --solc_args '--optimize' --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cloud \ No newline at end of file +certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --solc_args '--optimize' --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --cache StableToken --cloud \ No newline at end of file diff --git a/runVariableTokenCLI.sh b/runVariableTokenCLI.sh index 28f94145..2618d57c 100644 --- a/runVariableTokenCLI.sh +++ b/runVariableTokenCLI.sh @@ -1 +1 @@ -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 --cloud \ 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 --cache VariableToken --cloud \ No newline at end of file