Merge branch 'certora/integrationStep2' into 'master'

Fixes and Updates to Integration of Certora FV

See merge request aave-tech/protocol-v2!208

.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/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 --staging
+    - 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 --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 --cloud
 

runStableTokenCLI.sh

@@ -1 +1 @@
-certoraRun specs/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness --solc solc6.12 --verify StableDebtTokenHarness:specs/StableDebtToken.spec --settings -assumeUnwindCond,-b=4 --staging
+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.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

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
+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/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/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.
@@ -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 {

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);
   }