From 63a2cc35bf363715d6b70de92320081e6ab62119 Mon Sep 17 00:00:00 2001 From: nisnislevi Date: Mon, 23 Sep 2024 10:11:04 +0300 Subject: [PATCH] update stata to fit the new directories arrangment of the solidity --- .github/workflows/certora-stata.yml | 3 +- certora/basic/Makefile | 24 ++ certora/{ => basic}/README.md | 0 certora/{ => basic}/applyHarness.patch | 0 certora/basic/conf/AToken.conf | 16 + certora/basic/conf/EModeConfiguration.conf | 14 + .../conf/NEW-pool-no-summarizations.conf | 40 +++ .../conf/NEW-pool-simple-properties.conf | 43 +++ certora/basic/conf/ReserveConfiguration.conf | 16 + certora/basic/conf/UserConfiguration.conf | 17 + certora/basic/conf/VariableDebtToken.conf | 12 + certora/{ => basic}/harness/ATokenHarness.sol | 0 .../harness/EModeConfigurationHarness.sol | 47 +++ certora/basic/harness/PoolHarness.sol | 79 +++++ .../harness/ReserveConfigurationHarness.sol | 322 ++++++++++++++++++ certora/{ => basic}/harness/SimpleERC20.sol | 0 .../harness/SymbolicPriceOracle.sol | 0 .../harness/UserConfigurationHarness.sol | 0 .../harness/VariableDebtTokenHarness.sol | 0 certora/{ => basic}/munged/.gitignore | 0 certora/basic/scripts/run-all.sh | 72 ++++ certora/{ => basic}/specs/AToken.spec | 0 certora/basic/specs/EModeConfiguration.spec | 41 +++ certora/{ => basic}/specs/NEW-CVLMath.spec | 0 certora/basic/specs/NEW-pool-base.spec | 167 +++++++++ .../specs/NEW-pool-no-summarizations.spec | 0 .../specs/NEW-pool-simple-properties.spec | 0 certora/basic/specs/ReserveConfiguration.spec | 177 ++++++++++ .../{ => basic}/specs/UserConfiguration.spec | 0 .../{ => basic}/specs/VariableDebtToken.spec | 0 certora/{ => deprecated}/Makefile | 0 certora/deprecated/README.md | 56 +++ certora/deprecated/applyHarness.patch | 47 +++ certora/{ => deprecated}/conf/AToken.conf | 0 .../conf/NEW-pool-no-summarizations.conf | 0 .../conf/NEW-pool-simple-properties.conf | 0 .../conf/ReserveConfiguration.conf | 0 .../conf/UserConfiguration.conf | 0 .../conf/VariableDebtToken.conf | 0 certora/deprecated/harness/ATokenHarness.sol | 45 +++ .../{ => deprecated}/harness/PoolHarness.sol | 0 .../harness/ReserveConfigurationHarness.sol | 0 certora/deprecated/harness/SimpleERC20.sol | 58 ++++ .../harness/SymbolicPriceOracle.sol | 22 ++ .../harness/UserConfigurationHarness.sol | 74 ++++ .../harness/VariableDebtTokenHarness.sol | 16 + certora/deprecated/munged/.gitignore | 2 + certora/{ => deprecated}/scripts/run-all.sh | 0 certora/deprecated/specs/AToken.spec | 309 +++++++++++++++++ certora/deprecated/specs/NEW-CVLMath.spec | 198 +++++++++++ .../{ => deprecated}/specs/NEW-pool-base.spec | 0 .../specs/NEW-pool-no-summarizations.spec | 156 +++++++++ .../specs/NEW-pool-simple-properties.spec | 207 +++++++++++ .../specs/ReserveConfiguration.spec | 0 .../deprecated/specs/UserConfiguration.spec | 103 ++++++ .../deprecated/specs/VariableDebtToken.spec | 257 ++++++++++++++ certora/stata/applyHarness.patch | 8 +- certora/stata/conf/verifyAToken.conf | 6 +- certora/stata/conf/verifyDoubleClaim.conf | 6 +- certora/stata/conf/verifyERC4626.conf | 8 +- .../verifyERC4626DepositSummarization.conf | 6 +- certora/stata/conf/verifyERC4626Extended.conf | 6 +- ...verifyERC4626MintDepositSummarization.conf | 6 +- certora/stata/conf/verifyStataToken.conf | 6 +- certora/stata/harness/StataTokenV2Harness.sol | 2 +- .../harness/pool/SymbolicLendingPool.sol | 38 +-- .../rewards/RewardsControllerHarness.sol | 2 +- .../rewards/TransferStrategyHarness.sol | 4 +- certora/stata/scripts/run-all.sh | 6 +- 69 files changed, 2689 insertions(+), 55 deletions(-) create mode 100644 certora/basic/Makefile rename certora/{ => basic}/README.md (100%) rename certora/{ => basic}/applyHarness.patch (100%) create mode 100644 certora/basic/conf/AToken.conf create mode 100644 certora/basic/conf/EModeConfiguration.conf create mode 100644 certora/basic/conf/NEW-pool-no-summarizations.conf create mode 100644 certora/basic/conf/NEW-pool-simple-properties.conf create mode 100644 certora/basic/conf/ReserveConfiguration.conf create mode 100644 certora/basic/conf/UserConfiguration.conf create mode 100644 certora/basic/conf/VariableDebtToken.conf rename certora/{ => basic}/harness/ATokenHarness.sol (100%) create mode 100644 certora/basic/harness/EModeConfigurationHarness.sol create mode 100644 certora/basic/harness/PoolHarness.sol create mode 100644 certora/basic/harness/ReserveConfigurationHarness.sol rename certora/{ => basic}/harness/SimpleERC20.sol (100%) rename certora/{ => basic}/harness/SymbolicPriceOracle.sol (100%) rename certora/{ => basic}/harness/UserConfigurationHarness.sol (100%) rename certora/{ => basic}/harness/VariableDebtTokenHarness.sol (100%) rename certora/{ => basic}/munged/.gitignore (100%) create mode 100644 certora/basic/scripts/run-all.sh rename certora/{ => basic}/specs/AToken.spec (100%) create mode 100644 certora/basic/specs/EModeConfiguration.spec rename certora/{ => basic}/specs/NEW-CVLMath.spec (100%) create mode 100644 certora/basic/specs/NEW-pool-base.spec rename certora/{ => basic}/specs/NEW-pool-no-summarizations.spec (100%) rename certora/{ => basic}/specs/NEW-pool-simple-properties.spec (100%) create mode 100644 certora/basic/specs/ReserveConfiguration.spec rename certora/{ => basic}/specs/UserConfiguration.spec (100%) rename certora/{ => basic}/specs/VariableDebtToken.spec (100%) rename certora/{ => deprecated}/Makefile (100%) create mode 100644 certora/deprecated/README.md create mode 100644 certora/deprecated/applyHarness.patch rename certora/{ => deprecated}/conf/AToken.conf (100%) rename certora/{ => deprecated}/conf/NEW-pool-no-summarizations.conf (100%) rename certora/{ => deprecated}/conf/NEW-pool-simple-properties.conf (100%) rename certora/{ => deprecated}/conf/ReserveConfiguration.conf (100%) rename certora/{ => deprecated}/conf/UserConfiguration.conf (100%) rename certora/{ => deprecated}/conf/VariableDebtToken.conf (100%) create mode 100644 certora/deprecated/harness/ATokenHarness.sol rename certora/{ => deprecated}/harness/PoolHarness.sol (100%) rename certora/{ => deprecated}/harness/ReserveConfigurationHarness.sol (100%) create mode 100644 certora/deprecated/harness/SimpleERC20.sol create mode 100644 certora/deprecated/harness/SymbolicPriceOracle.sol create mode 100644 certora/deprecated/harness/UserConfigurationHarness.sol create mode 100644 certora/deprecated/harness/VariableDebtTokenHarness.sol create mode 100644 certora/deprecated/munged/.gitignore rename certora/{ => deprecated}/scripts/run-all.sh (100%) create mode 100644 certora/deprecated/specs/AToken.spec create mode 100644 certora/deprecated/specs/NEW-CVLMath.spec rename certora/{ => deprecated}/specs/NEW-pool-base.spec (100%) create mode 100644 certora/deprecated/specs/NEW-pool-no-summarizations.spec create mode 100644 certora/deprecated/specs/NEW-pool-simple-properties.spec rename certora/{ => deprecated}/specs/ReserveConfiguration.spec (100%) create mode 100644 certora/deprecated/specs/UserConfiguration.spec create mode 100644 certora/deprecated/specs/VariableDebtToken.spec diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml index 8555d4e5..04714798 100644 --- a/.github/workflows/certora-stata.yml +++ b/.github/workflows/certora-stata.yml @@ -56,8 +56,7 @@ jobs: # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1 - - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint - - verifyERC4626Extended.conf --rule maxDepositConstant + - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant - verifyERC4626Extended.conf --rule redeemSum - verifyERC4626Extended.conf --rule redeemATokensSum - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf diff --git a/certora/basic/Makefile b/certora/basic/Makefile new file mode 100644 index 00000000..f43cad49 --- /dev/null +++ b/certora/basic/Makefile @@ -0,0 +1,24 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../../src/ +MUNGED_DIR = munged + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + cp -r $(CONTRACTS_DIR) $@ + patch -p0 -d $@ < $(PATCH) + +record: + diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./src/++g' | sed 's+munged/++g' > $(PATCH) + +clean: + git clean -fdX + touch $(PATCH) + diff --git a/certora/README.md b/certora/basic/README.md similarity index 100% rename from certora/README.md rename to certora/basic/README.md diff --git a/certora/applyHarness.patch b/certora/basic/applyHarness.patch similarity index 100% rename from certora/applyHarness.patch rename to certora/basic/applyHarness.patch diff --git a/certora/basic/conf/AToken.conf b/certora/basic/conf/AToken.conf new file mode 100644 index 00000000..11c6b7ed --- /dev/null +++ b/certora/basic/conf/AToken.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "certora/basic/harness/ATokenHarness.sol", + "certora/basic/harness/SimpleERC20.sol" + ], + "link": [ + "ATokenHarness:_underlyingAsset=SimpleERC20" + ], + "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic". + "optimistic_loop": true, + "process": "emv", + "solc": "solc8.19", + "verify": "ATokenHarness:certora/basic/specs/AToken.spec", + "build_cache": true, + "msg": "aToken spec" +} diff --git a/certora/basic/conf/EModeConfiguration.conf b/certora/basic/conf/EModeConfiguration.conf new file mode 100644 index 00000000..484fb16f --- /dev/null +++ b/certora/basic/conf/EModeConfiguration.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/basic/harness/EModeConfigurationHarness.sol" + ], + "msg": "EModeConfiguration", + "optimistic_loop": true, + "process": "emv", + // "prover_args": [], + "precise_bitwise_ops": true, + "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic" + "solc": "solc8.19", + "build_cache": true, + "verify": "EModeConfigurationHarness:certora/basic/specs/EModeConfiguration.spec" +} diff --git a/certora/basic/conf/NEW-pool-no-summarizations.conf b/certora/basic/conf/NEW-pool-no-summarizations.conf new file mode 100644 index 00000000..3c158029 --- /dev/null +++ b/certora/basic/conf/NEW-pool-no-summarizations.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/basic/harness/ATokenHarness.sol", + "certora/basic/harness/PoolHarness.sol", + "certora/basic/harness/SimpleERC20.sol", + "src/contracts/instances/VariableDebtTokenInstance.sol", + "src/contracts/helpers/AaveProtocolDataProvider.sol", + "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", + "src/contracts/protocol/configuration/ACLManager.sol", + "src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol", + "src/contracts/misc/PriceOracleSentinel.sol", + "src/contracts/protocol/configuration/PoolAddressesProvider.sol", + ], + "link": [ + "ATokenHarness:POOL=PoolHarness", + "ATokenHarness:_underlyingAsset=SimpleERC20", + "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider", + "AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider", + ], + "struct_link": [ + "PoolHarness:aTokenAddress=ATokenHarness", + "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance", + "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2", + ], + "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc. + "optimistic_loop": true, + "process": "emv", + "global_timeout": "7198", + "prover_args": ["-depth 11"], // If reachability passes and the time is ok, this number is ok, dont touch it. + "solc": "solc8.19", + "verify": "PoolHarness:certora/basic/specs/NEW-pool-no-summarizations.spec", + "rule": [ + "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex", + "depositUpdatesUserATokenSuperBalance", + "depositCannotChangeOthersATokenSuperBalance" + ], + "build_cache": true, + "parametric_contracts": ["PoolHarness"], + "msg": "pool-no-summarizations::partial rules", +} diff --git a/certora/basic/conf/NEW-pool-simple-properties.conf b/certora/basic/conf/NEW-pool-simple-properties.conf new file mode 100644 index 00000000..890fcb6a --- /dev/null +++ b/certora/basic/conf/NEW-pool-simple-properties.conf @@ -0,0 +1,43 @@ +{ + "files": [ + "certora/basic/harness/ATokenHarness.sol", + "certora/basic/harness/PoolHarness.sol", + "certora/basic/harness/SimpleERC20.sol", + "src/contracts/instances/VariableDebtTokenInstance.sol", + "src/contracts/helpers/AaveProtocolDataProvider.sol", + "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol", + "src/contracts/protocol/libraries/types/DataTypes.sol", + "src/contracts/protocol/configuration/PoolAddressesProvider.sol", + ], + "link": [ + "ATokenHarness:POOL=PoolHarness", + "ATokenHarness:_underlyingAsset=SimpleERC20", + "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider", + ], + "struct_link": [ + "PoolHarness:aTokenAddress=ATokenHarness", + "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance", + "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2", + ], + "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc. + "optimistic_loop": true, + "process": "emv", + "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it. + "solc": "solc8.19", + "verify": "PoolHarness:certora/basic/specs/NEW-pool-simple-properties.spec", + "rule": [ + "cannotDepositInInactiveReserve", + "cannotDepositInFrozenReserve", + "cannotDepositZeroAmount", + "cannotWithdrawZeroAmount", + "cannotWithdrawFromInactiveReserve", + "cannotBorrowZeroAmount", + "cannotBorrowOnInactiveReserve", + "cannotBorrowOnReserveDisabledForBorrowing", + "cannotBorrowOnFrozenReserve" + ], + "build_cache": true, + "parametric_contracts": ["PoolHarness"], + "smt_timeout": "6000", + "msg": "pool-simple-properties::ALL", +} diff --git a/certora/basic/conf/ReserveConfiguration.conf b/certora/basic/conf/ReserveConfiguration.conf new file mode 100644 index 00000000..404b760f --- /dev/null +++ b/certora/basic/conf/ReserveConfiguration.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "certora/basic/harness/ReserveConfigurationHarness.sol" + ], + "msg": "ReserveConfiguration", + "optimistic_loop": true, + "process": "emv", + // "prover_args": [ + // "-precise_bitwise_ops" + //], + "precise_bitwise_ops": true, + "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic" + "solc": "solc8.19", + "build_cache": true, + "verify": "ReserveConfigurationHarness:certora/basic/specs/ReserveConfiguration.spec" +} diff --git a/certora/basic/conf/UserConfiguration.conf b/certora/basic/conf/UserConfiguration.conf new file mode 100644 index 00000000..e88cbe51 --- /dev/null +++ b/certora/basic/conf/UserConfiguration.conf @@ -0,0 +1,17 @@ +{ + "files": [ + "certora/basic/harness/UserConfigurationHarness.sol" + ], + // No rule sanity because a there are invariant s.t. the invariant can be proven + // without assuming it first. (for some of the functions.) + "msg": "UserConfiguration All spec", + "optimistic_loop": true, + "process": "emv", +// "prover_args": [ + // "-precise_bitwise_ops" + //], + "precise_bitwise_ops": true, + "solc": "solc8.19", + "build_cache": true, + "verify": "UserConfigurationHarness:certora/basic/specs/UserConfiguration.spec" +} diff --git a/certora/basic/conf/VariableDebtToken.conf b/certora/basic/conf/VariableDebtToken.conf new file mode 100644 index 00000000..ab6c780a --- /dev/null +++ b/certora/basic/conf/VariableDebtToken.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/basic/harness/VariableDebtTokenHarness.sol" + ], + "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc. + "msg": "variable debt token", + "optimistic_loop": true, + "process": "emv", + "solc": "solc8.19", + "build_cache": true, + "verify": "VariableDebtTokenHarness:certora/basic/specs/VariableDebtToken.spec" +} diff --git a/certora/harness/ATokenHarness.sol b/certora/basic/harness/ATokenHarness.sol similarity index 100% rename from certora/harness/ATokenHarness.sol rename to certora/basic/harness/ATokenHarness.sol diff --git a/certora/basic/harness/EModeConfigurationHarness.sol b/certora/basic/harness/EModeConfigurationHarness.sol new file mode 100644 index 00000000..71cc3563 --- /dev/null +++ b/certora/basic/harness/EModeConfigurationHarness.sol @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; +pragma experimental ABIEncoderV2; + +import {EModeConfiguration} from '../munged/contracts/protocol/libraries/configuration/EModeConfiguration.sol'; +import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; + +contract EModeConfigurationHarness { + DataTypes.EModeCategory public eModeCategory; + + function setCollateral(uint256 reserveIndex,bool collateral) public { + DataTypes.EModeCategory memory emode_new = eModeCategory; + EModeConfiguration.setCollateral(emode_new, reserveIndex, collateral); + eModeCategory.isCollateralBitmap = emode_new.isCollateralBitmap; + } + + function isCollateralAsset(uint256 reserveIndex) public returns (bool) { + return EModeConfiguration.isCollateralAsset(eModeCategory.isCollateralBitmap, reserveIndex); + } + + + function setBorrowable(uint256 reserveIndex,bool borrowable) public { + DataTypes.EModeCategory memory emode_new = eModeCategory; + EModeConfiguration.setBorrowable(emode_new, reserveIndex, borrowable); + eModeCategory.isBorrowableBitmap = emode_new.isBorrowableBitmap; + } + + function isBorrowableAsset(uint256 reserveIndex) public returns (bool) { + return EModeConfiguration.isBorrowableAsset(eModeCategory.isBorrowableBitmap, reserveIndex); + } + + + /* + + // Sets the Loan to Value of the reserve + function setLtv(uint256 ltv) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setLtv(configNew, ltv); + reservesConfig.data = configNew.data; + } + + // Gets the Loan to Value of the reserve + function getLtv() public view returns (uint256) { + return ReserveConfiguration.getLtv(reservesConfig); + } + */ +} diff --git a/certora/basic/harness/PoolHarness.sol b/certora/basic/harness/PoolHarness.sol new file mode 100644 index 00000000..ae8c239e --- /dev/null +++ b/certora/basic/harness/PoolHarness.sol @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; + +import {PoolInstance} from '../munged/contracts/instances/PoolInstance.sol'; +import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; +import {ReserveLogic} from '../munged/contracts/protocol/libraries/logic/ReserveLogic.sol'; +import {IPoolAddressesProvider} from '../munged/contracts/interfaces/IPoolAddressesProvider.sol'; + +import {IERC20} from '../../../src/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {ReserveConfiguration} from '../munged/contracts/protocol/libraries/configuration/ReserveConfiguration.sol'; + +contract PoolHarness is PoolInstance { + using ReserveLogic for DataTypes.ReserveData; + using ReserveLogic for DataTypes.ReserveCache; + + constructor(IPoolAddressesProvider provider) public PoolInstance(provider) {} + + function getCurrScaledVariableDebt(address asset) public view returns (uint256) { + DataTypes.ReserveData storage reserve = _reserves[asset]; + DataTypes.ReserveCache memory reserveCache = reserve.cache(); + return reserveCache.currScaledVariableDebt; + } + + function getTotalDebt(address asset) public view returns (uint256) { + uint256 totalVariable = IERC20(_reserves[asset].variableDebtTokenAddress).totalSupply(); + return totalVariable; + } + + function getTotalATokenSupply(address asset) public view returns (uint256) { + return IERC20(_reserves[asset].aTokenAddress).totalSupply(); + } + + function getReserveLiquidityIndex(address asset) public view returns (uint256) { + return _reserves[asset].liquidityIndex; + } + + function getReserveVariableBorrowIndex(address asset) public view returns (uint256) { + return _reserves[asset].variableBorrowIndex; + } + + function getReserveVariableBorrowRate(address asset) public view returns (uint256) { + return _reserves[asset].currentVariableBorrowRate; + } + + function updateReserveIndexes(address asset) public returns (bool) { + ReserveLogic._updateIndexes(_reserves[asset], _reserves[asset].cache()); + return true; + } + + function updateReserveIndexesWithCache( + address asset, + DataTypes.ReserveCache memory cache + ) public returns (bool) { + ReserveLogic._updateIndexes(_reserves[asset], cache); + return true; + } + + function cumulateToLiquidityIndex( + address asset, + uint256 totalLiquidity, + uint256 amount + ) public returns (uint256) { + return ReserveLogic.cumulateToLiquidityIndex(_reserves[asset], totalLiquidity, amount); + } + + function getActive(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) { + return ReserveConfiguration.getActive(self); + } + + function getFrozen(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) { + return ReserveConfiguration.getFrozen(self); + } + + function getBorrowingEnabled( + DataTypes.ReserveConfigurationMap memory self + ) external pure returns (bool) { + return ReserveConfiguration.getBorrowingEnabled(self); + } +} diff --git a/certora/basic/harness/ReserveConfigurationHarness.sol b/certora/basic/harness/ReserveConfigurationHarness.sol new file mode 100644 index 00000000..664ad86e --- /dev/null +++ b/certora/basic/harness/ReserveConfigurationHarness.sol @@ -0,0 +1,322 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; +pragma experimental ABIEncoderV2; + +import {ReserveConfiguration} from '../munged/contracts/protocol/libraries/configuration/ReserveConfiguration.sol'; +import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; + +contract ReserveConfigurationHarness { + DataTypes.ReserveConfigurationMap public reservesConfig; + mapping(uint256 => uint256) public intSettersUpperBounds; + mapping(uint256 => uint256) public intSetterslowerBounds; + mapping(uint256 => uint256) public boolSettersCompare; + + // Sets the Loan to Value of the reserve + function setLtv(uint256 ltv) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setLtv(configNew, ltv); + reservesConfig.data = configNew.data; + } + + // Gets the Loan to Value of the reserve + function getLtv() public view returns (uint256) { + return ReserveConfiguration.getLtv(reservesConfig); + } + + // Sets the liquidation threshold of the reserve + function setLiquidationThreshold(uint256 threshold) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setLiquidationThreshold(configNew, threshold); + reservesConfig.data = configNew.data; + } + + // Gets the liquidation threshold of the reserve + function getLiquidationThreshold() public view returns (uint256) { + return ReserveConfiguration.getLiquidationThreshold(reservesConfig); + } + + // Sets the liquidation bonus of the reserve + function setLiquidationBonus(uint256 bonus) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setLiquidationBonus(configNew, bonus); + reservesConfig.data = configNew.data; + } + + // Gets the liquidation bonus of the reserve + function getLiquidationBonus() public view returns (uint256) { + return ReserveConfiguration.getLiquidationBonus(reservesConfig); + } + + // Sets the decimals of the underlying asset of the reserve + function setDecimals(uint256 decimals) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setDecimals(configNew, decimals); + reservesConfig.data = configNew.data; + } + + // Gets the decimals of the underlying asset of the reserve + function getDecimals() public view returns (uint256) { + return ReserveConfiguration.getDecimals(reservesConfig); + } + + // Sets the active state of the reserve + function setActive(bool active) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setActive(configNew, active); + reservesConfig.data = configNew.data; + } + + // Gets the active state of the reserve + function getActive() public view returns (bool) { + return ReserveConfiguration.getActive(reservesConfig); + } + + // Sets the frozen state of the reserve + function setFrozen(bool frozen) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setFrozen(configNew, frozen); + reservesConfig.data = configNew.data; + } + + // Gets the frozen state of the reserve + function getFrozen() public view returns (bool) { + return ReserveConfiguration.getFrozen(reservesConfig); + } + + // Sets the paused state of the reserve + function setPaused(bool paused) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setPaused(configNew, paused); + reservesConfig.data = configNew.data; + } + + // Gets the paused state of the reserve + function getPaused() public view returns (bool) { + return ReserveConfiguration.getPaused(reservesConfig); + } + + // Sets the borrowable in isolation flag for the reserve. + function setBorrowableInIsolation(bool borrowable) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setBorrowableInIsolation(configNew, borrowable); + reservesConfig.data = configNew.data; + } + + // Gets the borrowable in isolation flag for the reserve. + function getBorrowableInIsolation() public view returns (bool) { + return ReserveConfiguration.getBorrowableInIsolation(reservesConfig); + } + + // Sets the siloed borrowing flag for the reserve. + function setSiloedBorrowing(bool siloed) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setSiloedBorrowing(configNew, siloed); + reservesConfig.data = configNew.data; + } + + // Gets the siloed borrowing flag for the reserve. + function getSiloedBorrowing() public view returns (bool) { + return ReserveConfiguration.getSiloedBorrowing(reservesConfig); + } + + // Enables or disables borrowing on the reserve + function setBorrowingEnabled(bool enabled) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setBorrowingEnabled(configNew, enabled); + reservesConfig.data = configNew.data; + } + + // Gets the borrowing state of the reserve + function getBorrowingEnabled() public view returns (bool) { + return ReserveConfiguration.getBorrowingEnabled(reservesConfig); + } + + // Sets the reserve factor of the reserve + function setReserveFactor(uint256 reserveFactor) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setReserveFactor(configNew, reserveFactor); + reservesConfig.data = configNew.data; + } + + // Gets the reserve factor of the reserve + function getReserveFactor() public view returns (uint256) { + return ReserveConfiguration.getReserveFactor(reservesConfig); + } + + // Sets the borrow cap of the reserve + function setBorrowCap(uint256 borrowCap) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setBorrowCap(configNew, borrowCap); + reservesConfig.data = configNew.data; + } + + // Gets the borrow cap of the reserve + function getBorrowCap() public view returns (uint256) { + return ReserveConfiguration.getBorrowCap(reservesConfig); + } + + // Sets the supply cap of the reserve + function setSupplyCap(uint256 supplyCap) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setSupplyCap(configNew, supplyCap); + reservesConfig.data = configNew.data; + } + + // Gets the supply cap of the reserve + function getSupplyCap() public view returns (uint256) { + return ReserveConfiguration.getSupplyCap(reservesConfig); + } + + // Sets the debt ceiling in isolation mode for the asset + function setDebtCeiling(uint256 ceiling) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setDebtCeiling(configNew, ceiling); + reservesConfig.data = configNew.data; + } + + // Gets the debt ceiling for the asset if the asset is in isolation mode + function getDebtCeiling() public view returns (uint256) { + return ReserveConfiguration.getDebtCeiling(reservesConfig); + } + + // Sets the liquidation protocol fee of the reserve + function setLiquidationProtocolFee(uint256 liquidationProtocolFee) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setLiquidationProtocolFee(configNew, liquidationProtocolFee); + reservesConfig.data = configNew.data; + } + + // Gets the liquidation protocol fee + function getLiquidationProtocolFee() public view returns (uint256) { + return ReserveConfiguration.getLiquidationProtocolFee(reservesConfig); + } + + // Sets the unbacked mint cap of the reserve + function setUnbackedMintCap(uint256 unbackedMintCap) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setUnbackedMintCap(configNew, unbackedMintCap); + reservesConfig.data = configNew.data; + } + + // Gets the unbacked mint cap of the reserve + function getUnbackedMintCap() public view returns (uint256) { + return ReserveConfiguration.getUnbackedMintCap(reservesConfig); + } + + // Sets the eMode asset category + // function setEModeCategory(uint256 category) public { + // DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + // ReserveConfiguration.setEModeCategory(configNew, category); + // reservesConfig.data = configNew.data; + //} + + // Gets the eMode asset category + //function getEModeCategory() public view returns (uint256) { + // return ReserveConfiguration.getEModeCategory(reservesConfig); + //} + + // Sets the flashloanble flag for the reserve + function setFlashLoanEnabled(bool flashLoanEnabled) public { + DataTypes.ReserveConfigurationMap memory configNew = reservesConfig; + ReserveConfiguration.setFlashLoanEnabled(configNew, flashLoanEnabled); + reservesConfig.data = configNew.data; + } + + // Gets the flashloanable flag for the reserve + function getFlashLoanEnabled() public view returns (bool) { + return ReserveConfiguration.getFlashLoanEnabled(reservesConfig); + } + + // returns the entire data in form of unit256 + function getData() public view returns (uint256) { + return reservesConfig.data; + } + + // Executes a setter of an int parameter according to the given id + function executeIntSetterById(uint256 id, uint256 val) public { + require(id >= 0 && id <= 10); + if (id == 0) { + setLtv(val); + } else if (id == 1) { + setLiquidationThreshold(val); + } else if (id == 2) { + setLiquidationBonus(val); + } else if (id == 3) { + setDecimals(val); + } else if (id == 4) { + setReserveFactor(val); + } else if (id == 5) { + setBorrowCap(val); + } else if (id == 6) { + setSupplyCap(val); + } else if (id == 7) { + setLiquidationProtocolFee(val); + // } else if (id == 8) { + //setEModeCategory(val); + } else if (id == 8) { + setUnbackedMintCap(val); + } else { + setDebtCeiling(val); + } + } + + // Executes a getter of an int parameter according to the given id + function executeIntGetterById(uint256 id) public view returns (uint256) { + require(id >= 0 && id <= 10); + if (id == 0) { + return getLtv(); + } else if (id == 1) { + return getLiquidationThreshold(); + } else if (id == 2) { + return getLiquidationBonus(); + } else if (id == 3) { + return getDecimals(); + } else if (id == 4) { + return getReserveFactor(); + } else if (id == 5) { + return getBorrowCap(); + } else if (id == 6) { + return getSupplyCap(); + } else if (id == 7) { + return getLiquidationProtocolFee(); + // } else if (id == 8) { + //return getEModeCategory(); + } else if (id == 8) { + return getUnbackedMintCap(); + } else { + return getDebtCeiling(); + } + } + + // Executes a setter of a bool parameter according to the given id + function executeBoolSetterById(uint256 id, bool val) public { + require(id >= 0 && id <= 4); + if (id == 0) { + setActive(val); + } else if (id == 1) { + setFrozen(val); + } else if (id == 2) { + setBorrowingEnabled(val); + } else if (id == 3) { + setPaused(val); + } else { + setBorrowableInIsolation(val); + } + } + + // Executes a getter of a bool parameter according to the given id + function executeBoolGetterById(uint256 id) public view returns (bool) { + require(id >= 0 && id <= 4); + if (id == 0) { + return getActive(); + } else if (id == 1) { + return getFrozen(); + } else if (id == 2) { + return getBorrowingEnabled(); + } else if (id == 3) { + return getPaused(); + } else { + return getBorrowableInIsolation(); + } + } +} diff --git a/certora/harness/SimpleERC20.sol b/certora/basic/harness/SimpleERC20.sol similarity index 100% rename from certora/harness/SimpleERC20.sol rename to certora/basic/harness/SimpleERC20.sol diff --git a/certora/harness/SymbolicPriceOracle.sol b/certora/basic/harness/SymbolicPriceOracle.sol similarity index 100% rename from certora/harness/SymbolicPriceOracle.sol rename to certora/basic/harness/SymbolicPriceOracle.sol diff --git a/certora/harness/UserConfigurationHarness.sol b/certora/basic/harness/UserConfigurationHarness.sol similarity index 100% rename from certora/harness/UserConfigurationHarness.sol rename to certora/basic/harness/UserConfigurationHarness.sol diff --git a/certora/harness/VariableDebtTokenHarness.sol b/certora/basic/harness/VariableDebtTokenHarness.sol similarity index 100% rename from certora/harness/VariableDebtTokenHarness.sol rename to certora/basic/harness/VariableDebtTokenHarness.sol diff --git a/certora/munged/.gitignore b/certora/basic/munged/.gitignore similarity index 100% rename from certora/munged/.gitignore rename to certora/basic/munged/.gitignore diff --git a/certora/basic/scripts/run-all.sh b/certora/basic/scripts/run-all.sh new file mode 100644 index 00000000..9c9cb662 --- /dev/null +++ b/certora/basic/scripts/run-all.sh @@ -0,0 +1,72 @@ +#CMN="--compilation_steps_only" +#CMN="--typecheck_only" + + + +echo "******** Running: 1 ***************" +certoraRun $CMN certora/basic/conf/AToken.conf \ + --msg "1: AToken.conf" + +echo "******** Running: 2 ***************" +certoraRun $CMN certora/basic/conf/ReserveConfiguration.conf \ + --msg "2: ReserveConfiguration.conf" + +echo "******** Running: 3 ***************" +certoraRun $CMN certora/basic/conf/UserConfiguration.conf \ + --msg "3: UserConfiguration.conf" + +echo "******** Running: 4 ***************" +certoraRun $CMN certora/basic/conf/VariableDebtToken.conf \ + --msg "4: VariableDebtToken.conf" + +echo "******** Running: 5 NEW no summarization ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-no-summarizations.conf \ + --msg "5: NEW-pool-no-summarizations" + + +echo "******** Running: simple:1 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotDepositInInactiveReserve \ + --msg "simple:1: NEW :: cannotDepositInInactiveReserve" + +echo "******** Running: simple:2 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotDepositInFrozenReserve \ + --msg "simple:2: NEW :: cannotDepositInFrozenReserve" + +echo "******** Running: simple:3 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotDepositZeroAmount \ + --msg "simple:3: NEW :: cannotDepositZeroAmount" + +echo "******** Running: simple:4 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotWithdrawZeroAmount \ + --msg "simple:4: NEW :: cannotWithdrawZeroAmount" + +echo "******** Running: simple:5 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotWithdrawFromInactiveReserve \ + --msg "simple:5: NEW :: cannotWithdrawFromInactiveReserve" + +echo "******** Running: simple:6 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotBorrowZeroAmount \ + --msg "simple:6: NEW :: cannotBorrowZeroAmount" + +echo "******** Running: simple:7 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotBorrowOnInactiveReserve \ + --msg "simple:7: NEW :: cannotBorrowOnInactiveReserve" + +echo "******** Running: simple:8 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotBorrowOnReserveDisabledForBorrowing \ + --msg "simple:8: NEW :: cannotBorrowOnReserveDisabledForBorrowing" + +echo "******** Running: simple:9 ***************" +certoraRun $CMN certora/basic/conf/NEW-pool-simple-properties.conf \ + --rule cannotBorrowOnFrozenReserve \ + --msg "simple:9: NEW :: cannotBorrowOnFrozenReserve" + + diff --git a/certora/specs/AToken.spec b/certora/basic/specs/AToken.spec similarity index 100% rename from certora/specs/AToken.spec rename to certora/basic/specs/AToken.spec diff --git a/certora/basic/specs/EModeConfiguration.spec b/certora/basic/specs/EModeConfiguration.spec new file mode 100644 index 00000000..00bc917b --- /dev/null +++ b/certora/basic/specs/EModeConfiguration.spec @@ -0,0 +1,41 @@ +methods { + function setCollateral(uint256 reserveIndex,bool collateral) external envfree; + function isCollateralAsset(uint256 reserveIndex) external returns (bool) envfree; + function setBorrowable(uint256 reserveIndex,bool borrowable) external envfree; + function isBorrowableAsset(uint256 reserveIndex) external returns (bool) envfree; +} + + +rule setCollateralIntegrity(uint256 reserveIndex, bool collateral) { + setCollateral(reserveIndex,collateral); + assert isCollateralAsset(reserveIndex) == collateral; +} + +rule independencyOfCollateralSetters(uint256 reserveIndex, bool collateral) { + uint256 reserveIndex_other; + + bool before = isCollateralAsset(reserveIndex_other); + setCollateral(reserveIndex,collateral); + bool after = isCollateralAsset(reserveIndex_other); + + assert (reserveIndex != reserveIndex_other => before == after); +} + + +rule setBorrowableIntegrity(uint256 reserveIndex, bool borrowable) { + setBorrowable(reserveIndex,borrowable); + assert isBorrowableAsset(reserveIndex) == borrowable; +} + +rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) { + uint256 reserveIndex_other; + + bool before = isBorrowableAsset(reserveIndex_other); + setBorrowable(reserveIndex,borrowable); + bool after = isBorrowableAsset(reserveIndex_other); + + assert (reserveIndex != reserveIndex_other => before == after); +} + + + diff --git a/certora/specs/NEW-CVLMath.spec b/certora/basic/specs/NEW-CVLMath.spec similarity index 100% rename from certora/specs/NEW-CVLMath.spec rename to certora/basic/specs/NEW-CVLMath.spec diff --git a/certora/basic/specs/NEW-pool-base.spec b/certora/basic/specs/NEW-pool-base.spec new file mode 100644 index 00000000..cc91ac2e --- /dev/null +++ b/certora/basic/specs/NEW-pool-base.spec @@ -0,0 +1,167 @@ +/* + This is a Base Specification File for Smart Contract Verification with the Certora Prover. + This file is meant to be included +*/ + +import "NEW-CVLMath.spec"; + +/* + Declaration of contracts used in the spec +*/ +using ATokenHarness as _aToken; +using PoolHarness as PH; +using AaveProtocolDataProvider as _dataProvider; +using SimpleERC20 as _underlyingAsset; + +/* + Methods Summerizations and Enviroment-Free (e.g relative to e.msg variables) Declarations +*/ + +methods { + // Pool + function _.handleAction(address, uint256, uint256) external => NONDET; + function _.getAssetPrice(address) external => NONDET; + function _.getPriceOracle() external => ALWAYS(2); + function _.getPriceOracleSentinel() external => ALWAYS(4); + + function _.calculateCompoundedInterest(uint256 x, uint40 t0, uint256 t1) internal => calculateCompoundedInterestSummary(x, t0, t1) expect uint256 ALL; + + // ERC20 + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function _.approve(address, uint256) external => DISPATCHER(true); + // function _.mint(address, uint256) external => DISPATCHER(true); + //function _.burn(uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + + function _.totalSupply() external => DISPATCHER(true); + + // ATOKEN + //function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true); + function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true); + function _.mintToTreasury(uint256 amount, uint256 index) external => DISPATCHER(true); + function _.transferOnLiquidation(address from, address to, uint256 value) external => DISPATCHER(true); + function _.transferUnderlyingTo(address user, uint256 amount) external => DISPATCHER(true); + //function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true); + function _.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) external => DISPATCHER(true); + function _.ATokenBalanceOf(address user) external => DISPATCHER(true); + + // Unsat Core Based + function _.getParams(DataTypes.ReserveConfigurationMap memory self) internal => NONDET; + + function _.calculateUserAccountData(mapping(address => DataTypes.ReserveData) storage reservesData,mapping(uint256 => address) storage reservesList,mapping(uint8 => DataTypes.EModeCategory) storage eModeCategories,DataTypes.CalculateUserAccountDataParams memory params) internal => NONDET; + function _._getUserBalanceInBaseCurrency(address user,DataTypes.ReserveData storage reserve,uint256 assetPrice,uint256 assetUnit) internal => NONDET; + function _.wadDiv(uint256 a, uint256 b) internal => NONDET; + function _.wadToRay(uint256 a) internal => NONDET; + function _._calculateDomainSeparator() internal => NONDET; + + + // Debt Tokens + function _.scaledTotalSupply() external => DISPATCHER(true); + + function _.getReserveNormalizedIncome(address asset) external => DISPATCHER(true); + function _.getReserveNormalizedVariableDebt(address asset) external => DISPATCHER(true); + function _.getACLManager() external => DISPATCHER(true); + // function _.isBridge(address) external => DISPATCHER(true); + + // variableDebt + function _.burn(address user, uint256 amount, uint256 index) external => DISPATCHER(true); + + function getActive(DataTypes.ReserveConfigurationMap) external returns (bool); + function getFrozen(DataTypes.ReserveConfigurationMap) external returns (bool); + function getBorrowingEnabled(DataTypes.ReserveConfigurationMap) external returns (bool); +} + +/* definitions and functions to be used within the spec file */ + +definition IS_UINT256(uint256 x) returns bool = ((x >= 0) && (x <= max_uint256)); + +function first_term(uint256 x, uint256 y) returns uint256 { return x; } + +ghost mapping(uint256 => mapping(uint256 => uint256)) calculateCompoundedInterestSummaryValues; + +function calculateCompoundedInterestSummary(uint256 rate, uint40 t0, uint256 t1) returns uint256 +{ + uint256 deltaT = assert_uint256( (t1-t0) % 2^256 ); + if (deltaT == 0) { + return RAY(); + } + if (rate == RAY()) { + return RAY(); + } + if (rate >= RAY()) { + require calculateCompoundedInterestSummaryValues[rate][deltaT] >= rate; + } + else { + require calculateCompoundedInterestSummaryValues[rate][deltaT] < rate; + } + return calculateCompoundedInterestSummaryValues[rate][deltaT]; +} + +function isActiveReserve(env e, address asset) returns bool { + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveConfigurationMap configuration = data.configuration; + bool isActive = getActive(e, configuration); + + return isActive; +} + +function isFrozenReserve(env e, address asset) returns bool { + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveConfigurationMap configuration = data.configuration; + bool isFrozen = getFrozen(e, configuration); + + return isFrozen; +} + +function isEnabledForBorrow(env e, address asset) returns bool { + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + DataTypes.ReserveConfigurationMap configuration = data.configuration; + bool isBorrowEnabled = getBorrowingEnabled(e, configuration); + + return isBorrowEnabled; +} + +function getCurrentLiquidityRate(env e, address asset) returns mathint { + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + return data.currentLiquidityRate; +} + +function getLiquidityIndex(env e, address asset) returns mathint { + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + return data.liquidityIndex; +} + +function aTokenBalanceOf(env e, address user) returns uint256 { + return _aToken.ATokenBalanceOf(e, user); +} + +function rayMulPreciseSummarization(uint256 x, uint256 y) returns uint256 { + if ((x == 0) || (y == 0)) { + return 0; + } + if (x == RAY()) { + return y; + } + if (y == RAY()) { + return x; + } + + mathint c = x * y; + return require_uint256(c / RAY()); +} + +function rayDivPreciseSummarization(uint256 x, uint256 y) returns uint256 { + require y != 0; + if (x == 0) { + return 0; + } + if (y == RAY()) { + return x; + } + if (y == x) { + return RAY(); + } + mathint c = x * RAY(); + return require_uint256(c / y); +} diff --git a/certora/specs/NEW-pool-no-summarizations.spec b/certora/basic/specs/NEW-pool-no-summarizations.spec similarity index 100% rename from certora/specs/NEW-pool-no-summarizations.spec rename to certora/basic/specs/NEW-pool-no-summarizations.spec diff --git a/certora/specs/NEW-pool-simple-properties.spec b/certora/basic/specs/NEW-pool-simple-properties.spec similarity index 100% rename from certora/specs/NEW-pool-simple-properties.spec rename to certora/basic/specs/NEW-pool-simple-properties.spec diff --git a/certora/basic/specs/ReserveConfiguration.spec b/certora/basic/specs/ReserveConfiguration.spec new file mode 100644 index 00000000..8b992ae2 --- /dev/null +++ b/certora/basic/specs/ReserveConfiguration.spec @@ -0,0 +1,177 @@ +methods { + function setLtv(uint256) external envfree; + function getLtv() external returns (uint256) envfree; + function setLiquidationThreshold(uint256) external envfree; + function getLiquidationThreshold() external returns (uint256) envfree; + function setLiquidationBonus(uint256) external envfree; + function getLiquidationBonus() external returns (uint256) envfree; + function setDecimals(uint256) external envfree; + function getDecimals() external returns (uint256) envfree; + function setActive(bool) external envfree; + function getActive() external returns (bool) envfree; + function setFrozen(bool) external envfree; + function getFrozen() external returns (bool) envfree; + function setPaused(bool) external envfree; + function getPaused() external returns (bool) envfree; + function setBorrowableInIsolation(bool) external envfree; + function getBorrowableInIsolation() external returns (bool) envfree; + function setSiloedBorrowing(bool) external envfree; + function getSiloedBorrowing() external returns (bool) envfree; + function setBorrowingEnabled(bool) external envfree; + function getBorrowingEnabled() external returns (bool) envfree; + function setReserveFactor(uint256) external envfree; + function getReserveFactor() external returns (uint256) envfree; + function setBorrowCap(uint256) external envfree; + function getBorrowCap() external returns (uint256) envfree; + function setSupplyCap(uint256) external envfree; + function getSupplyCap() external returns (uint256) envfree; + function setDebtCeiling(uint256) external envfree; + function getDebtCeiling() external returns (uint256) envfree; + function setLiquidationProtocolFee(uint256) external envfree; + function getLiquidationProtocolFee() external returns (uint256) envfree; + function setUnbackedMintCap(uint256) external envfree; + function getUnbackedMintCap() external returns (uint256) envfree; + // function setEModeCategory(uint256) external envfree; + // function getEModeCategory() external returns (uint256) envfree; + function setFlashLoanEnabled(bool) external envfree; + function getFlashLoanEnabled() external returns (bool) envfree; + function getData() external returns uint256 envfree; + function executeIntSetterById(uint256, uint256) external envfree; + function executeIntGetterById(uint256) external returns uint256 envfree; + function executeBoolSetterById(uint256, bool) external envfree; + function executeBoolGetterById(uint256) external returns bool envfree; +} + +// checks the integrity of set LTV function and correct retrieval of the corresponding getter. +rule setLtvIntegrity(uint256 ltv) { + setLtv(ltv); + assert getLtv() == ltv; +} + +// checks the integrity of set LiquidationThreshold function and correct retrieval of the corresponding getter. +rule setLiquidationThresholdIntegrity(uint256 threshold) { + setLiquidationThreshold(threshold); + assert getLiquidationThreshold() == threshold; +} + +// checks the integrity of set LiquidationBonus function and correct retrieval of the corresponding getter. +rule setLiquidationBonusIntegrity(uint256 bonus) { + setLiquidationBonus(bonus); + assert getLiquidationBonus() == bonus; +} + +// checks the integrity of set Decimals function and correct retrieval of the corresponding getter. +rule setDecimalsIntegrity(uint256 decimals) { + setDecimals(decimals); + assert getDecimals() == decimals; +} + +// checks the integrity of set Active function and correct retrieval of the corresponding getter. +rule setActiveIntegrity(bool active) { + setActive(active); + assert getActive() == active; +} + +// checks the integrity of set Frozen function and correct retrieval of the corresponding getter. +rule setFrozenIntegrity(bool frozen) { + setFrozen(frozen); + assert getFrozen() == frozen; +} + +// checks the integrity of set Paused function and correct retrieval of the corresponding getter. +rule setPausedIntegrity(bool paused) { + setPaused(paused); + assert getPaused() == paused; +} + +// checks the integrity of set BorrowableInIsolation function and correct retrieval of the corresponding getter. +rule setBorrowableInIsolationIntegrity(bool borrowable) { + setBorrowableInIsolation(borrowable); + assert getBorrowableInIsolation() == borrowable; +} + +// checks the integrity of set SiloedBorrowing function and correct retrieval of the corresponding getter. +rule setSiloedBorrowingIntegrity(bool siloed) { + setSiloedBorrowing(siloed); + assert getSiloedBorrowing() == siloed; +} + +// checks the integrity of set BorrowingEnabled function and correct retrieval of the corresponding getter. +rule setBorrowingEnabledIntegrity(bool enabled) { + setBorrowingEnabled(enabled); + assert getBorrowingEnabled() == enabled; +} + +// checks the integrity of set ReserveFactor function and correct retrieval of the corresponding getter. +rule setReserveFactorIntegrity(uint256 reserveFactor) { + setReserveFactor(reserveFactor); + assert getReserveFactor() == reserveFactor; +} + +// checks the integrity of set BorrowCap function and correct retrieval of the corresponding getter. +rule setBorrowCapIntegrity(uint256 borrowCap) { + setBorrowCap(borrowCap); + assert getBorrowCap() == borrowCap; +} + +// checks the integrity of set SupplyCap function and correct retrieval of the corresponding getter. +rule setSupplyCapIntegrity(uint256 supplyCap) { + setSupplyCap(supplyCap); + assert getSupplyCap() == supplyCap; +} + +// checks the integrity of set DebtCeiling function and correct retrieval of the corresponding getter. +rule setDebtCeilingIntegrity(uint256 ceiling) { + setDebtCeiling(ceiling); + assert getDebtCeiling() == ceiling; +} + +// checks the integrity of set LiquidationProtocolFee function and correct retrieval of the corresponding getter. +rule setLiquidationProtocolFeeIntegrity(uint256 liquidationProtocolFee) { + setLiquidationProtocolFee(liquidationProtocolFee); + assert getLiquidationProtocolFee() == liquidationProtocolFee; +} + +// checks the integrity of set UnbackedMintCap function and correct retrieval of the corresponding getter. +rule setUnbackedMintCapIntegrity(uint256 unbackedMintCap) { + setUnbackedMintCap(unbackedMintCap); + assert getUnbackedMintCap() == unbackedMintCap; +} + +// checks the integrity of set EModeCategory function and correct retrieval of the corresponding getter. +//rule setEModeCategoryIntegrity(uint256 category) { +// setEModeCategory(category); +// assert getEModeCategory() == category; +//} + +// checks for independence of int parameters - if one parameter is being set, non of the others is being changed +rule integrityAndIndependencyOfIntSetters(uint256 funcId, uint256 otherFuncId, uint256 val) { + require 0 <= funcId && funcId <= 9; + require 0 <= otherFuncId && otherFuncId <= 9; + uint256 valueBefore = executeIntGetterById(funcId); + uint256 otherValueBefore = executeIntGetterById(otherFuncId); + + executeIntSetterById(funcId, val); + + uint256 valueAfter = executeIntGetterById(funcId); + uint256 otherValueAfter = executeIntGetterById(otherFuncId); + + assert valueAfter == val; + assert (otherFuncId != funcId => otherValueAfter == otherValueBefore); +} + +// checks for independence of bool parameters - if one parameter is being set, non of the others is being changed +rule integrityAndIndependencyOfBoolSetters(uint256 funcId, uint256 otherFuncId, bool val) { + require 0 <= funcId && funcId <= 10; + require 0 <= otherFuncId && otherFuncId <= 10; + bool valueBefore = executeBoolGetterById(funcId); + bool otherValueBefore = executeBoolGetterById(otherFuncId); + + executeBoolSetterById(funcId, val); + + bool valueAfter = executeBoolGetterById(funcId); + bool otherValueAfter = executeBoolGetterById(otherFuncId); + + assert valueAfter == val; + assert (otherFuncId != funcId => otherValueAfter == otherValueBefore); +} diff --git a/certora/specs/UserConfiguration.spec b/certora/basic/specs/UserConfiguration.spec similarity index 100% rename from certora/specs/UserConfiguration.spec rename to certora/basic/specs/UserConfiguration.spec diff --git a/certora/specs/VariableDebtToken.spec b/certora/basic/specs/VariableDebtToken.spec similarity index 100% rename from certora/specs/VariableDebtToken.spec rename to certora/basic/specs/VariableDebtToken.spec diff --git a/certora/Makefile b/certora/deprecated/Makefile similarity index 100% rename from certora/Makefile rename to certora/deprecated/Makefile diff --git a/certora/deprecated/README.md b/certora/deprecated/README.md new file mode 100644 index 00000000..201ac15b --- /dev/null +++ b/certora/deprecated/README.md @@ -0,0 +1,56 @@ +# Running the certora verification tool + +These instructions detail the process for running CVT on the contracts. + +Documentation for CVT and the specification language are available +[here](https://certora.atlassian.net/wiki/spaces/CPD/overview) + +## Running the verification + +Initial step: if certora prover is not installed follow the steps [here](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) + +First step is to create the munged/ directory. Enter the certora/ directory and run the following: + +```sh +touch applyHarness.patch +``` + +```sh +make munged +``` + +The second and major step is to run all the verification rules. +The script `certora/scripts/run-all.sh` is used to submit all verification +jobs to the Certora verification service. These scripts should be run from the +root directory: + +```sh +bash certora/scripts/run-all.sh +``` + +_Note: When running the rules locally, please remove the solc version from the `.conf` files as when using solc-select solc version should not be specified in `.conf`_ + +After the jobs are complete, the results will be available on +[the Certora portal](https://prover.certora.com/). + +## Adapting to changes + +Some of our rules require the code to be simplified in various ways. Our +primary tool for performing these simplifications is to run verification on a +contract that extends the original contracts and overrides some of the methods. +These "harness" contracts can be found in the `certora/harness` directory. + +This pattern does require some modifications to the original code: some methods +need to be made virtual or public, for example. These changes are handled by +applying a patch to the code before verification. + +When one of the `verify` scripts is executed, it first applies the patch file +`certora/applyHarness.patch` to the `contracts` directory, placing the output +in the `certora/munged` directory. We then verify the contracts in the +`certora/munged` directory. + +If the original contracts change, it is possible to create a conflict with the +patch. In this case, the verify scripts will report an error message and output +rejected changes in the `munged` directory. After merging the changes, run +`make record` in the `certora` directory; this will regenerate the patch file, +which can then be checked into git. diff --git a/certora/deprecated/applyHarness.patch b/certora/deprecated/applyHarness.patch new file mode 100644 index 00000000..06b4e1ca --- /dev/null +++ b/certora/deprecated/applyHarness.patch @@ -0,0 +1,47 @@ +diff -ruN contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol +--- contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol 2024-03-27 12:57:15.497294747 +0200 ++++ contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol 2024-03-27 13:08:22.155984803 +0200 +@@ -34,7 +34,7 @@ + } + + /// @inheritdoc IScaledBalanceToken +- function scaledBalanceOf(address user) external view override returns (uint256) { ++ function scaledBalanceOf(address user) public view override returns (uint256) { + return super.balanceOf(user); + } + +diff -ruN contracts/instances/ATokenInstance.sol contracts/instances/ATokenInstance.sol +--- contracts/instances/ATokenInstance.sol 2024-03-27 12:57:15.497294747 +0200 ++++ contracts/instances/ATokenInstance.sol 2024-03-27 13:14:17.971198372 +0200 +@@ -35,15 +35,15 @@ + + _domainSeparator = _calculateDomainSeparator(); + +- emit Initialized( +- underlyingAsset, +- address(POOL), +- treasury, +- address(incentivesController), +- aTokenDecimals, +- aTokenName, +- aTokenSymbol, +- params +- ); ++ // emit Initialized( ++ // underlyingAsset, ++ // address(POOL), ++ // treasury, ++ // address(incentivesController), ++ // aTokenDecimals, ++ // aTokenName, ++ // aTokenSymbol, ++ // params ++ //); + } + } +diff -ruN .gitignore .gitignore +--- .gitignore 1970-01-01 02:00:00.000000000 +0200 ++++ .gitignore 2024-03-27 13:08:22.155984803 +0200 +@@ -0,0 +1,2 @@ ++* ++!.gitignore diff --git a/certora/conf/AToken.conf b/certora/deprecated/conf/AToken.conf similarity index 100% rename from certora/conf/AToken.conf rename to certora/deprecated/conf/AToken.conf diff --git a/certora/conf/NEW-pool-no-summarizations.conf b/certora/deprecated/conf/NEW-pool-no-summarizations.conf similarity index 100% rename from certora/conf/NEW-pool-no-summarizations.conf rename to certora/deprecated/conf/NEW-pool-no-summarizations.conf diff --git a/certora/conf/NEW-pool-simple-properties.conf b/certora/deprecated/conf/NEW-pool-simple-properties.conf similarity index 100% rename from certora/conf/NEW-pool-simple-properties.conf rename to certora/deprecated/conf/NEW-pool-simple-properties.conf diff --git a/certora/conf/ReserveConfiguration.conf b/certora/deprecated/conf/ReserveConfiguration.conf similarity index 100% rename from certora/conf/ReserveConfiguration.conf rename to certora/deprecated/conf/ReserveConfiguration.conf diff --git a/certora/conf/UserConfiguration.conf b/certora/deprecated/conf/UserConfiguration.conf similarity index 100% rename from certora/conf/UserConfiguration.conf rename to certora/deprecated/conf/UserConfiguration.conf diff --git a/certora/conf/VariableDebtToken.conf b/certora/deprecated/conf/VariableDebtToken.conf similarity index 100% rename from certora/conf/VariableDebtToken.conf rename to certora/deprecated/conf/VariableDebtToken.conf diff --git a/certora/deprecated/harness/ATokenHarness.sol b/certora/deprecated/harness/ATokenHarness.sol new file mode 100644 index 00000000..bcb5d32a --- /dev/null +++ b/certora/deprecated/harness/ATokenHarness.sol @@ -0,0 +1,45 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.19; + +import {Pool} from '../munged/contracts/protocol/pool/Pool.sol'; +import {ATokenInstance} from '../munged/contracts/instances/ATokenInstance.sol'; +import {WadRayMath} from '../munged/contracts/protocol/libraries/math/WadRayMath.sol'; +import {ScaledBalanceTokenBase} from '../munged/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol'; +import {IScaledBalanceToken} from '../munged/contracts/interfaces/IScaledBalanceToken.sol'; + +/* + * @title Certora harness for Aave ERC20 AToken + * + * @dev Certora's harness contract for the verification of Aave ERC20 AToken. + */ +contract ATokenHarness is ATokenInstance { + using WadRayMath for uint256; + + constructor(Pool pool) public ATokenInstance(pool) {} + + function scaledTotalSupply() + public + view + override(IScaledBalanceToken, ScaledBalanceTokenBase) + returns (uint256) + { + uint256 val = super.scaledTotalSupply(); + return val; + } + + function additionalData(address user) public view returns (uint128) { + return _userState[user].additionalData; + } + + function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) { + return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset)); + } + + function ATokenBalanceOf(address user) public view returns (uint256) { + return super.balanceOf(user); + } + + function superBalance(address user) public view returns (uint256) { + return scaledBalanceOf(user); + } +} diff --git a/certora/harness/PoolHarness.sol b/certora/deprecated/harness/PoolHarness.sol similarity index 100% rename from certora/harness/PoolHarness.sol rename to certora/deprecated/harness/PoolHarness.sol diff --git a/certora/harness/ReserveConfigurationHarness.sol b/certora/deprecated/harness/ReserveConfigurationHarness.sol similarity index 100% rename from certora/harness/ReserveConfigurationHarness.sol rename to certora/deprecated/harness/ReserveConfigurationHarness.sol diff --git a/certora/deprecated/harness/SimpleERC20.sol b/certora/deprecated/harness/SimpleERC20.sol new file mode 100644 index 00000000..68733603 --- /dev/null +++ b/certora/deprecated/harness/SimpleERC20.sol @@ -0,0 +1,58 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; + +import {IERC20} from '../munged/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; + +/** +A simple ERC implementation used as the underlying_asset for the verification process. + */ +contract SimpleERC20 is IERC20 { + uint256 t; + mapping(address => uint256) b; + mapping(address => mapping(address => uint256)) a; + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a + b; + require(c >= a); + return c; + } + + function sub(uint a, uint b) internal pure returns (uint256) { + require(a >= b); + return a - b; + } + + function totalSupply() external view override returns (uint256) { + return t; + } + + function balanceOf(address account) external view override returns (uint256) { + return b[account]; + } + + function transfer(address recipient, uint256 amount) external override returns (bool) { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + return true; + } + + function allowance(address owner, address spender) external view override returns (uint256) { + return a[owner][spender]; + } + + function approve(address spender, uint256 amount) external override returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external override returns (bool) { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return true; + } +} diff --git a/certora/deprecated/harness/SymbolicPriceOracle.sol b/certora/deprecated/harness/SymbolicPriceOracle.sol new file mode 100644 index 00000000..d268e5d0 --- /dev/null +++ b/certora/deprecated/harness/SymbolicPriceOracle.sol @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; + +import {IPriceOracleGetter} from '../munged/contracts/interfaces/IPriceOracleGetter.sol'; + +contract SymbolicPriceOracle is IPriceOracleGetter { + address public base; + uint256 public unit; + mapping(address => uint256) public price; + + function BASE_CURRENCY() external view returns (address) { + return base; + } + + function BASE_CURRENCY_UNIT() external view override returns (uint256) { + return unit; + } + + function getAssetPrice(address asset) external view override returns (uint256) { + return price[asset]; + } +} diff --git a/certora/deprecated/harness/UserConfigurationHarness.sol b/certora/deprecated/harness/UserConfigurationHarness.sol new file mode 100644 index 00000000..3f1637ea --- /dev/null +++ b/certora/deprecated/harness/UserConfigurationHarness.sol @@ -0,0 +1,74 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; +pragma experimental ABIEncoderV2; + +import {UserConfiguration} from '../munged/contracts/protocol/libraries/configuration/UserConfiguration.sol'; +import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol'; +import {PoolStorage} from '../munged/contracts/protocol/pool/PoolStorage.sol'; + +/* +A wrapper contract for calling functions from the library UserConfiguration. +*/ +contract UserConfigurationHarness is PoolStorage { + DataTypes.UserConfigurationMap public usersConfig; + + // Sets if the user is borrowing the reserve identified by reserveIndex + function setBorrowing(uint256 reserveIndex, bool borrowing) public { + UserConfiguration.setBorrowing(usersConfig, reserveIndex, borrowing); + } + + //Sets if the user is using as collateral the reserve identified by reserveIndex + function setUsingAsCollateral(uint256 reserveIndex, bool _usingAsCollateral) public { + UserConfiguration.setUsingAsCollateral(usersConfig, reserveIndex, _usingAsCollateral); + } + + // Returns if a user has been using the reserve for borrowing or as collateral + function isUsingAsCollateralOrBorrowing(uint256 reserveIndex) public view returns (bool) { + return UserConfiguration.isUsingAsCollateralOrBorrowing(usersConfig, reserveIndex); + } + + // Validate a user has been using the reserve for borrowing + function isBorrowing(uint256 reserveIndex) public view returns (bool) { + return UserConfiguration.isBorrowing(usersConfig, reserveIndex); + } + + // Validate a user has been using the reserve as collateral + function isUsingAsCollateral(uint256 reserveIndex) public view returns (bool) { + return UserConfiguration.isUsingAsCollateral(usersConfig, reserveIndex); + } + + // Checks if a user has been supplying only one reserve as collateral + function isUsingAsCollateralOne() public view returns (bool) { + return UserConfiguration.isUsingAsCollateralOne(usersConfig); + } + + // Checks if a user has been supplying any reserve as collateral + function isUsingAsCollateralAny() public view returns (bool) { + return UserConfiguration.isUsingAsCollateralAny(usersConfig); + } + + // Checks if a user has been borrowing only one asset + function isBorrowingOne() public view returns (bool) { + return UserConfiguration.isBorrowingOne(usersConfig); + } + + // Checks if a user has been borrowing from any reserve + function isBorrowingAny() public view returns (bool) { + return UserConfiguration.isBorrowingAny(usersConfig); + } + + // Checks if a user has not been using any reserve for borrowing or supply + function isEmpty() public view returns (bool) { + return UserConfiguration.isEmpty(usersConfig); + } + + // Returns the Isolation Mode state of the user + function getIsolationModeState() public view returns (bool, address, uint256) { + return UserConfiguration.getIsolationModeState(usersConfig, _reserves, _reservesList); + } + + // Returns the siloed borrowing state for the user + function getSiloedBorrowingState() public view returns (bool, address) { + return UserConfiguration.getSiloedBorrowingState(usersConfig, _reserves, _reservesList); + } +} diff --git a/certora/deprecated/harness/VariableDebtTokenHarness.sol b/certora/deprecated/harness/VariableDebtTokenHarness.sol new file mode 100644 index 00000000..ca2696a6 --- /dev/null +++ b/certora/deprecated/harness/VariableDebtTokenHarness.sol @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.19; + +import {VariableDebtTokenInstance} from '../munged/contracts/instances/VariableDebtTokenInstance.sol'; +import {WadRayMath} from '../munged/contracts/protocol/libraries/math/WadRayMath.sol'; +import {IPool} from '../munged/contracts/interfaces/IPool.sol'; + +contract VariableDebtTokenHarness is VariableDebtTokenInstance { + using WadRayMath for uint256; + + constructor(IPool pool) public VariableDebtTokenInstance(pool) {} + + function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) { + return bal.rayMul(POOL.getReserveNormalizedVariableDebt(_underlyingAsset)); + } +} diff --git a/certora/deprecated/munged/.gitignore b/certora/deprecated/munged/.gitignore new file mode 100644 index 00000000..d6b7ef32 --- /dev/null +++ b/certora/deprecated/munged/.gitignore @@ -0,0 +1,2 @@ +* +!.gitignore diff --git a/certora/scripts/run-all.sh b/certora/deprecated/scripts/run-all.sh similarity index 100% rename from certora/scripts/run-all.sh rename to certora/deprecated/scripts/run-all.sh diff --git a/certora/deprecated/specs/AToken.spec b/certora/deprecated/specs/AToken.spec new file mode 100644 index 00000000..bd15c698 --- /dev/null +++ b/certora/deprecated/specs/AToken.spec @@ -0,0 +1,309 @@ +/** + - values of gRNI passing: ray, 2 * ray +*/ +using SimpleERC20 as _underlyingAsset; + +methods { + function nonces(address) external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; + function _.handleAction(address, uint256, uint256) external => NONDET; + function _.getReserveNormalizedIncome(address u) external => gRNI() expect uint256 ALL; + function balanceOf(address) external returns (uint256) envfree; + function additionalData(address) external returns uint128 envfree; + function _.finalizeTransfer(address, address, address, uint256, uint256, uint256) external => NONDET; + + function scaledTotalSupply() external returns (uint256); + function scaledBalanceOf(address) external returns (uint256); + function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree; +} + +function PLUS256(uint256 x, uint256 y) returns uint256 { + return (assert_uint256( (x+y) % 2^256) ); +} +function MINUS256(uint256 x, uint256 y) returns uint256 { + return (assert_uint256( (x-y) % 2^256) ); +} + +definition ray() returns uint = 1000000000000000000000000000; +definition bound() returns mathint = ((gRNI() / ray()) + 1 ) / 2; + +/* + Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2. +*/ +definition bounded_error_eq(uint x, uint y, uint scale) returns bool = + to_mathint(x) <= to_mathint(y) + (bound() * scale) && + to_mathint(x) + (bound() * scale) >= to_mathint(y); + +persistent ghost sumAllBalance() returns mathint { + init_state axiom sumAllBalance() == 0; +} + +// summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul) +ghost gRNI() returns uint256 { + axiom to_mathint(gRNI()) == 7 * ray(); +} + +hook Sstore _userState[KEY address a].balance uint128 balance (uint128 old_balance) { + havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance; +} + +invariant totalSupplyEqualsSumAllBalance(env e) + totalSupply(e) == scaledBalanceOfToBalanceOf(require_uint256(sumAllBalance())) + filtered { f -> !f.isView } + { + preserved mint(address caller, address onBehalfOf, uint256 amount, uint256 index) with (env e2) { + require index == gRNI(); + } + preserved burn(address from, address receiverOfUnderlying, uint256 amount, uint256 index) with (env e3) { + require index == gRNI(); + } + } + +// Rule to verify that permit sets the allowance correctly. +rule permitIntegrity(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { + env e; + uint256 nonceBefore = nonces(owner); + permit(e, owner, spender, value, deadline, v, r, s); + assert allowance(owner, spender) == value; + assert to_mathint(nonces(owner)) == nonceBefore + 1; +} + +// can't mint zero Tokens +rule mintArgsPositive(address user, uint256 amount, uint256 index) { + env e; + address caller; + mint@withrevert(e, caller, user, amount, index); + assert amount == 0 => lastReverted; +} + +/** + Check that each possible operation changes the balance of at most two users +*/ +rule balanceOfChange(address a, address b, address c, method f ) + filtered { f -> !f.isView } +{ + env e; + require a!=b && a!=c && b!=c; + uint256 balanceABefore = balanceOf(a); + uint256 balanceBBefore = balanceOf(b); + uint256 balanceCBefore = balanceOf(c); + + calldataarg arg; + f(e, arg); + + uint256 balanceAAfter = balanceOf(a); + uint256 balanceBAfter = balanceOf(b); + uint256 balanceCAfter = balanceOf(c); + + assert ( balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter || balanceCBefore == balanceCAfter); +} + +/** + Mint to user u amount of x tokens, increases his balanceOf the underlying asset by x and + AToken total suplly should increase. +*/ +rule integrityMint(address a, address b, uint256 x) { + env e; + uint256 indexRay = gRNI(); + + uint256 underlyingBalanceBefore = balanceOf(a); + uint256 atokenBlanceBefore = scaledBalanceOf(e, a); + uint256 totalATokenSupplyBefore = scaledTotalSupply(e); + + mint(e,b,a,x,indexRay); + + uint256 underlyingBalanceAfter = balanceOf(a); + uint256 atokenBlanceAfter = scaledBalanceOf(e, a); + uint256 totalATokenSupplyAfter = scaledTotalSupply(e); + + assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore; + assert totalATokenSupplyAfter > totalATokenSupplyBefore; + assert bounded_error_eq(underlyingBalanceAfter, PLUS256(underlyingBalanceBefore,x), 1); +} + +/* + Mint is additive, can performed either all at once or gradually + mint(u,x); mint(u,y) ~ mint(u,x+y) at the same initial state +*/ +rule additiveMint(address a, address b, address c, uint256 x, uint256 y) { + env e; + uint256 indexRay = gRNI(); + require(balanceOf(a) == balanceOf(b) && a != b); + uint256 balanceScenario0 = balanceOf(a); + mint(e,c,a,x,indexRay); + mint(e,c,a,y,indexRay); + uint256 balanceScenario1 = balanceOf(a); + mint(e, c, b, PLUS256(x,y) ,indexRay); + + uint256 balanceScenario2 = balanceOf(b); + assert bounded_error_eq(balanceScenario1, balanceScenario2, 3), "mint is not additive"; +} + +/* + transfers amount from _userState[from].balance to _userState[to].balance + while balance of returns _userState[account].balance normalized by gNRI(); + transfer is incentivizedERC20 +*/ +rule integrityTransfer(address from, address to, uint256 amount) { + env e; + require e.msg.sender == from; + address other; // for any address including from, to, currentContract the underlying asset balance should stay the same + + uint256 balanceBeforeFrom = balanceOf(from); + uint256 balanceBeforeTo = balanceOf(to); + uint256 underlyingBeforeOther = _underlyingAsset.balanceOf(e, other); + + require(amount <= balanceBeforeFrom); // Add this require inorder to move to CVL2 + + transfer(e, to, amount); + + uint256 balanceAfterFrom = balanceOf(from); + uint256 balanceAfterTo = balanceOf(to); + uint256 underlyingAfterOther = _underlyingAsset.balanceOf(e, other); + + assert underlyingAfterOther == underlyingBeforeOther, "unexpected change in underlying asserts"; + + if (from != to) { + assert bounded_error_eq(balanceAfterFrom, MINUS256(balanceBeforeFrom,amount), 1) && + bounded_error_eq(balanceAfterTo, PLUS256(balanceBeforeTo,amount), 1), "unexpected balance of from/to, when from!=to"; + } else { + assert balanceAfterFrom == balanceAfterTo , "unexpected balance of from/to, when from==to"; + } +} + + +/* + Transfer is additive, can performed either all at once or gradually + transfer(from,to,x); transfer(from,to,y) ~ transfer(from,to,x+y) at the same initial state +*/ +rule additiveTransfer(address from1, address from2, address to1, address to2, uint256 x, uint256 y) { + env e1; + env e2; + uint256 indexRay = gRNI(); + require ( + from1 != from2 && to1 != to2 && from1 != to2 && from2 != to1 && + (from1 == to1 <=> from2 == to2) && + balanceOf(from1) == balanceOf(from2) && balanceOf(to1) == balanceOf(to2) + ); + + require e1.msg.sender == from1; + require e2.msg.sender == from2; + transfer(e1, to1, x); + transfer(e1, to1, y); + uint256 balanceFromScenario1 = balanceOf(from1); + uint256 balanceToScenario1 = balanceOf(to1); + + transfer(e2, to2, PLUS256(x,y)); + + uint256 balanceFromScenario2 = balanceOf(from2); + uint256 balanceToScenario2 = balanceOf(to2); + + assert + bounded_error_eq(balanceFromScenario1, balanceFromScenario2, 3) && + bounded_error_eq(balanceToScenario1, balanceToScenario2, 3), "transfer is not additive"; +} + + +/* + Burn scaled amount of Atoken from 'user' and transfers amount of the underlying asset to 'to'. +*/ +rule integrityBurn(address user, address to, uint256 amount) { + env e; + uint256 indexRay = gRNI(); + + require user != currentContract; + uint256 balanceBeforeUser = balanceOf(user); + uint256 balanceBeforeTo = balanceOf(to); + uint256 underlyingBeforeTo = _underlyingAsset.balanceOf(e, to); + uint256 underlyingBeforeUser = _underlyingAsset.balanceOf(e, user); + uint256 underlyingBeforeSystem = _underlyingAsset.balanceOf(e, currentContract); + uint256 totalSupplyBefore = totalSupply(e); + + require(amount <= underlyingBeforeSystem); // Add this require inorder to move to CVL2 + require(amount <= balanceBeforeUser); // Add this require inorder to move to CVL2 + require(amount <= totalSupplyBefore); // Add this require inorder to move to CVL2 + + burn(e, user, to, amount, indexRay); + + uint256 balanceAfterUser = balanceOf(user); + uint256 balanceAfterTo = balanceOf(to); + uint256 underlyingAfterTo = _underlyingAsset.balanceOf(e, to); + uint256 underlyingAfterUser = _underlyingAsset.balanceOf(e, user); + uint256 underlyingAfterSystem = _underlyingAsset.balanceOf(e, currentContract); + uint256 totalSupplyAfter = totalSupply(e); + + if (user != to) { + assert balanceAfterTo == balanceBeforeTo && // balanceOf To should not change + bounded_error_eq(underlyingBeforeUser, underlyingAfterUser, 1), "integrity break on user!=to"; + } + + if (to != currentContract) { + assert bounded_error_eq(underlyingAfterSystem, MINUS256(underlyingBeforeSystem,amount), 1) && // system transfer underlying_asset + bounded_error_eq(underlyingAfterTo, PLUS256(underlyingBeforeTo,amount), 1) , "integrity break on to!=currentContract"; + } else { + assert underlyingAfterSystem == underlyingBeforeSystem, "integrity break on to==currentContract"; + } + + assert bounded_error_eq(totalSupplyAfter, MINUS256(totalSupplyBefore,amount), 1), "total supply integrity"; // total supply reduced + assert bounded_error_eq(balanceAfterUser, MINUS256(balanceBeforeUser,amount), 1), "integrity break"; // user burns ATokens to recieve underlying +} + +/* + Burn is additive, can performed either all at once or gradually + burn(from,to,x,index); burn(from,to,y,index) ~ burn(from,to,x+y,index) at the same initial state +*/ +rule additiveBurn(address user1, address user2, address to1, address to2, uint256 x, uint256 y) { + env e; + uint256 indexRay = gRNI(); + require ( + user1 != user2 && to1 != to2 && user1 != to2 && user2 != to1 && + (user1 == to1 <=> user2 == to2) && + balanceOf(user1) == balanceOf(user2) && balanceOf(to1) == balanceOf(to2) + ); + require user1 != currentContract && user2 != currentContract; + + burn(e, user1, to1, x, indexRay); + burn(e, user1, to1, y, indexRay); + uint256 balanceUserScenario1 = balanceOf(user1); + + burn(e, user2, to2, PLUS256(x,y), indexRay); + uint256 balanceUserScenario2 = balanceOf(user2); + + assert bounded_error_eq(balanceUserScenario1, balanceUserScenario2, 3), "burn is not additive"; +} + +/* + Burning one user atokens should have no effect on other users that are not involved in the action. +*/ +rule burnNoChangeToOther(address user, address recieverOfUnderlying, uint256 amount, uint256 index, address other) { + require other != user && other != recieverOfUnderlying; + env e; + uint256 otherDataBefore = additionalData(other); + uint256 otherBalanceBefore = balanceOf(other); + + burn(e, user, recieverOfUnderlying, amount, index); + + uint256 otherDataAfter = additionalData(other); + uint256 otherBalanceAfter = balanceOf(other); + + assert otherDataBefore == otherDataAfter && + otherBalanceBefore == otherBalanceAfter; +} + +/* + Minting ATokens for a user should have no effect on other users that are not involved in the action. +*/ +rule mintNoChangeToOther(address user, uint256 amount, uint256 index, address other) { + require other != user; + + env e; + uint128 otherDataBefore = additionalData(other); + uint256 otherBalanceBefore = balanceOf(other); + address caller; + mint(e, caller, user, amount, index); + + uint128 otherDataAfter = additionalData(other); + uint256 otherBalanceAfter = balanceOf(other); + + assert otherBalanceBefore == otherBalanceAfter && otherDataBefore == otherDataAfter; +} diff --git a/certora/deprecated/specs/NEW-CVLMath.spec b/certora/deprecated/specs/NEW-CVLMath.spec new file mode 100644 index 00000000..a18d40f1 --- /dev/null +++ b/certora/deprecated/specs/NEW-CVLMath.spec @@ -0,0 +1,198 @@ +/****************************************** +----------- CVL Math Library -------------- +*******************************************/ + +// A restriction on the value of w = x * y / z +// The ratio between x (or y) and z is a rational number a/b or b/a. +// Important : do not set a = 0 or b = 0. +// Note: constRatio(x,y,z,a,b,w) <=> constRatio(x,y,z,b,a,w) +definition constRatio(uint256 x, uint256 y, uint256 z, uint256 a, uint256 b, uint256 w) returns bool = + ( a * x == b * z && to_mathint(w) == (b * y) / a ) || + ( b * x == a * z && to_mathint(w) == (a * y) / b ) || + ( a * y == b * z && to_mathint(w) == (b * x) / a ) || + ( b * y == a * z && to_mathint(w) == (a * x) / b ); + +// A restriction on the value of w = x * y / z +// The division quotient between x (or y) and z is an integer q or 1/q. +// Important : do not set q=0 +definition constQuotient(uint256 x, uint256 y, uint256 z, uint256 q, uint256 w) returns bool = + ( to_mathint(x) == q * z && to_mathint(w) == q * y ) || + ( q * x == to_mathint(z) && to_mathint(w) == y / q ) || + ( to_mathint(y) == q * z && to_mathint(w) == q * x ) || + ( q * y == to_mathint(z) && to_mathint(w) == x / q ); + +/// Equivalent to the one above, but with implication +definition constQuotientImply(uint256 x, uint256 y, uint256 z, uint256 q, uint256 w) returns bool = + ( to_mathint(x) == q * z => to_mathint(w) == q * y ) && + ( q * x == to_mathint(z) => to_mathint(w) == y / q ) && + ( to_mathint(y) == q * z => to_mathint(w) == q * x ) && + ( q * y == to_mathint(z) => to_mathint(w) == x / q ); + +definition ONE18() returns uint256 = 1000000000000000000; +definition RAY() returns uint256 = 10^27; + +definition _monotonicallyIncreasing(uint256 x, uint256 y, uint256 fx, uint256 fy) returns bool = + (x > y => fx >= fy); + +definition _monotonicallyDecreasing(uint256 x, uint256 y, uint256 fx, uint256 fy) returns bool = + (x > y => fx <= fy); + +definition abs(mathint x) returns mathint = + x >= 0 ? x : 0 - x; + +definition min(mathint x, mathint y) returns mathint = + x > y ? y : x; + +definition max(mathint x, mathint y) returns mathint = + x > y ? x : y; + +/// Returns whether y is equal to x up to error bound of 'err' (18 decs). +/// e.g. 10% relative error => err = 1e17 +definition relativeErrorBound(mathint x, mathint y, mathint err) returns bool = + (x != 0 + ? abs(x - y) * ONE18() <= abs(x) * err + : abs(y) <= err); + +/// Axiom for a weighted average of the form WA = (x * y) / (y + z) +/// This is valid as long as z + y > 0 => make certain of that condition in the use of this definition. +definition weightedAverage(mathint x, mathint y, mathint z, mathint WA) returns bool = + ((x > 0 && y > 0) => (WA >= 0 && WA <= x)) + && + ((x < 0 && y > 0) => (WA <= 0 && WA >= x)) + && + ((x > 0 && y < 0) => (WA <= 0 && WA - x <= 0)) + && + ((x < 0 && y < 0) => (WA >= 0 && WA + x <= 0)) + && + ((x == 0 || y == 0) => (WA == 0)); + + +function mulDivDownAbstract(uint256 x, uint256 y, uint256 z) returns uint256 { + require z !=0; + uint256 xy = require_uint256(x * y); + uint256 res; + mathint rem; + require z * res + rem == to_mathint(xy); + require rem < to_mathint(z); + return res; +} + +function mulDivDownAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 { + uint256 res; + require z != 0; + uint256 xy = require_uint256(x * y); + uint256 fz = require_uint256(res * z); + + require xy >= fz; + require fz + z > to_mathint(xy); + return res; +} + +function mulDivUpAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 { + uint256 res; + require z != 0; + uint256 xy = require_uint256(x * y); + uint256 fz = require_uint256(res * z); + require xy >= fz; + require fz + z > to_mathint(xy); + + if (xy == fz) { + return res; + } + return require_uint256(res + 1); +} + +function mulDownWad(uint256 x, uint256 y) returns uint256 { + return mulDivDownAbstractPlus(x, y, ONE18()); +} + +function mulUpWad(uint256 x, uint256 y) returns uint256 { + return mulDivUpAbstractPlus(x, y, ONE18()); +} + +function divDownWad(uint256 x, uint256 y) returns uint256 { + return mulDivDownAbstractPlus(x, ONE18(), y); +} + +function divUpWad(uint256 x, uint256 y) returns uint256 { + return mulDivUpAbstractPlus(x, ONE18(), y); +} + +function discreteQuotientMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 { + uint256 res; + require z != 0 && noOverFlowMul(x, y); + // Discrete quotients: + require( + ((x ==0 || y ==0) && res == 0) || + (x == z && res == y) || + (y == z && res == x) || + constQuotient(x, y, z, 2, res) || // Division quotient is 1/2 or 2 + constQuotient(x, y, z, 5, res) || // Division quotient is 1/5 or 5 + constQuotient(x, y, z, 100, res) // Division quotient is 1/100 or 100 + ); + return res; +} + +function discreteRatioMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 { + uint256 res; + require z != 0 && noOverFlowMul(x, y); + // Discrete ratios: + require( + ((x ==0 || y ==0) && res == 0) || + (x == z && res == y) || + (y == z && res == x) || + constRatio(x, y, z, 2, 1, res) || // f = 2*x or f = x/2 (same for y) + constRatio(x, y, z, 5, 1, res) || // f = 5*x or f = x/5 (same for y) + constRatio(x, y, z, 2, 3, res) || // f = 2*x/3 or f = 3*x/2 (same for y) + constRatio(x, y, z, 2, 7, res) // f = 2*x/7 or f = 7*x/2 (same for y) + ); + return res; +} + +function noOverFlowMul(uint256 x, uint256 y) returns bool { + return x * y <= max_uint; +} + +/// @doc Ghost power function that incorporates mathematical pure x^y axioms. +/// @warning Some of these axioms might be false, depending on the Solidity implementation +/// The user must bear in mind that equality-like axioms can be violated because of rounding errors. +ghost _ghostPow(uint256, uint256) returns uint256 { + /// x^0 = 1 + axiom forall uint256 x. _ghostPow(x, 0) == ONE18(); + /// 0^x = 1 + axiom forall uint256 y. _ghostPow(0, y) == 0; + /// x^1 = x + axiom forall uint256 x. _ghostPow(x, ONE18()) == x; + /// 1^y = 1 + axiom forall uint256 y. _ghostPow(ONE18(), y) == ONE18(); + + /// I. x > 1 && y1 > y2 => x^y1 > x^y2 + /// II. x < 1 && y1 > y2 => x^y1 < x^y2 + axiom forall uint256 x. forall uint256 y1. forall uint256 y2. + x >= ONE18() && y1 > y2 => _ghostPow(x, y1) >= _ghostPow(x, y2); + axiom forall uint256 x. forall uint256 y1. forall uint256 y2. + x < ONE18() && y1 > y2 => (_ghostPow(x, y1) <= _ghostPow(x, y2) && _ghostPow(x,y2) <= ONE18()); + axiom forall uint256 x. forall uint256 y. + x < ONE18() && y > ONE18() => (_ghostPow(x, y) <= x); + axiom forall uint256 x. forall uint256 y. + x < ONE18() && y <= ONE18() => (_ghostPow(x, y) >= x); + axiom forall uint256 x. forall uint256 y. + x >= ONE18() && y > ONE18() => (_ghostPow(x, y) >= x); + axiom forall uint256 x. forall uint256 y. + x >= ONE18() && y <= ONE18() => (_ghostPow(x, y) <= x); + /// x1 > x2 && y > 0 => x1^y > x2^y + axiom forall uint256 x1. forall uint256 x2. forall uint256 y. + x1 > x2 => _ghostPow(x1, y) >= _ghostPow(x2, y); +} + +function CVLPow(uint256 x, uint256 y) returns uint256 { + if (y == 0) {return ONE18();} + if (x == 0) {return 0;} + return _ghostPow(x, y); +} + +function CVLSqrt(uint256 x) returns uint256 { + mathint SQRT; + require SQRT*SQRT <= to_mathint(x) && (SQRT + 1)*(SQRT + 1) > to_mathint(x); + return require_uint256(SQRT); +} diff --git a/certora/specs/NEW-pool-base.spec b/certora/deprecated/specs/NEW-pool-base.spec similarity index 100% rename from certora/specs/NEW-pool-base.spec rename to certora/deprecated/specs/NEW-pool-base.spec diff --git a/certora/deprecated/specs/NEW-pool-no-summarizations.spec b/certora/deprecated/specs/NEW-pool-no-summarizations.spec new file mode 100644 index 00000000..826b0fb7 --- /dev/null +++ b/certora/deprecated/specs/NEW-pool-no-summarizations.spec @@ -0,0 +1,156 @@ +import "NEW-pool-base.spec"; + +methods { + function _.hasRole(bytes32 b ,address a) external => DISPATCHER(true); + + function _.getReservesList() external => DISPATCHER(true); + function _.getReserveData(address a) external => DISPATCHER(true); + + function _.symbol() external => DISPATCHER(true); + function _.isFlashBorrower(address a) external => DISPATCHER(true); + + // function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true); + + function _.isPoolAdmin(address a) external => DISPATCHER(true); + function _.getConfiguration(address a) external => DISPATCHER(true); + + function _.rayMul(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, b, 10^27) expect uint256 ALL; + function _.rayDiv(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, 10^27, b) expect uint256 ALL; + + // IPriceOracleSentinel + function _.isBorrowAllowed() external => DISPATCHER(true); + function _.isLiquidationAllowed() external => DISPATCHER(true); + function _.setSequencerOracle(address newSequencerOracle) external => DISPATCHER(true); + function _.setGracePeriod(uint256 newGracePeriod) external => DISPATCHER(true); + function _.getGracePeriod() external => DISPATCHER(true); + + // Modification of index is tracked by incrementCounter: + function _.incrementCounter() external => ghostUpdate() expect bool ALL; +} + +ghost mathint counterUpdateIndexes; + +function ghostUpdate() returns bool { + counterUpdateIndexes = counterUpdateIndexes + 1; + return true; +} + + +function calculateInterestRatesMock(DataTypes.CalculateInterestRatesParams params) returns (uint256, uint256) { + uint256 liquidityRate = 1; + uint256 variableBorrowRate = 1; + return (liquidityRate, variableBorrowRate); +} + + +/* ================================================================================================= + @title Rule checking, that the ghostUpdate summary is correct and that it is being applied + This rule is part of a check, that the liquidity index cannot decrease. + + Nissan remark on 26/03/2024: This rule fails! + See here: https://prover.certora.com/output/66114/812c9675658a4d4d935a8e0a3e1f4a99/?anonymousKey=46e0337ab421a402e525e156b4aa1fb7a9b2fce9 + ================================================================================================ */ +rule _updateIndexesWrapperReachable(env e, method f) { + calldataarg args; + + mathint updateIndexesCallCountBefore = counterUpdateIndexes; + f(e, args); + + mathint updateIndexesCallCountAfter = counterUpdateIndexes; + + satisfy updateIndexesCallCountBefore != updateIndexesCallCountAfter; +} + +// @title cumulateToLiquidityIndex does not decrease the liquidity index. +// This rule is part of a check, that the liquidity index cannot decrease. +// Proved here: +// https://prover.certora.com/output/40577/bb018f9a52b64b27a0ac364e0c22cd79/?anonymousKey=21613bfbfc0f479ed2c99ce5fa2dd16e581baf5e +rule liquidityIndexNonDecresingFor_cumulateToLiquidityIndex() { + address asset; + uint256 totalLiquidity; + uint256 amount; + env e; + + uint256 reserveLiquidityIndexBefore = getReserveLiquidityIndex(e, asset); + require reserveLiquidityIndexBefore >= RAY(); + + uint256 reserveLiquidityIndexAfter = cumulateToLiquidityIndex(e, asset, totalLiquidity, amount); + + assert reserveLiquidityIndexAfter >= reserveLiquidityIndexBefore; +} + + +function get_AToken_of_asset(env e, address asset) returns address { + DataTypes.ReserveData data = getReserveDataExtended(e, asset); + return data.aTokenAddress; +} + + +/* =========================================================================================== + When a user deposits X amount of an asset and the current liquidity index for this asset is 1, + his scaled balance (=superBalance) increases by X. + + Note: Using superBalance is easier for the prover as we do not need to compute the balance + from the scaled balance. + WE ALLOW OFF BY ONE RAY. + =========================================================================================== */ +rule depositUpdatesUserATokenSuperBalance(env e) { + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; + + require to_mathint(amount) == 30*RAY(); //under approx + require asset != onBehalfOf; + require onBehalfOf != _aToken; + require e.msg.sender != _aToken; + require e.msg.sender != asset; + require asset == _aToken.UNDERLYING_ASSET_ADDRESS(e); + require get_AToken_of_asset(e,asset) == _aToken; + + mathint superBalanceBefore = _aToken.superBalance(e, onBehalfOf); + require superBalanceBefore == 20*RAY(); //under approx + mathint liquidityIndexBefore = getLiquidityIndex(e, asset); + require liquidityIndexBefore == 1*RAY(); //under approx + mathint currentLiquidityRateBefore = getCurrentLiquidityRate(e, asset); + require currentLiquidityRateBefore == 1; //under approx + + deposit(e, asset, amount, onBehalfOf, referralCode); + + mathint superBalanceAfter = _aToken.superBalance(e, onBehalfOf); + mathint currentLiquidityRateAfter = getCurrentLiquidityRate(e, asset); + require currentLiquidityRateAfter == currentLiquidityRateBefore; + + mathint liquidityIndexAfter = getLiquidityIndex(e, asset); + + require liquidityIndexAfter == liquidityIndexBefore; + assert superBalanceAfter >= superBalanceBefore + amount - 1 * RAY(); + assert superBalanceAfter <= superBalanceBefore + amount + 1 * RAY(); +} + +/* =========================================================================================== + Depositing on behalf of user A does not change balance of user other than A. + ========================================================================================= */ +rule depositCannotChangeOthersATokenSuperBalance(env e) { + address asset; + uint256 amount; + address onBehalfOf; + address otherUser; + uint16 referralCode; + + require to_mathint(amount) == 30*RAY(); //under approx + require asset != onBehalfOf; + require onBehalfOf != _aToken; + require e.msg.sender != _aToken; + require e.msg.sender != asset; + require asset == _aToken.UNDERLYING_ASSET_ADDRESS(e); + require otherUser != onBehalfOf; + require otherUser != _aToken; + + mathint superBalanceBefore = _aToken.superBalance(e, otherUser); + + deposit(e, asset, amount, onBehalfOf, referralCode); + + mathint superBalanceAfter = _aToken.superBalance(e, otherUser); + assert superBalanceAfter == superBalanceBefore; +} diff --git a/certora/deprecated/specs/NEW-pool-simple-properties.spec b/certora/deprecated/specs/NEW-pool-simple-properties.spec new file mode 100644 index 00000000..b9e024a3 --- /dev/null +++ b/certora/deprecated/specs/NEW-pool-simple-properties.spec @@ -0,0 +1,207 @@ +import "NEW-pool-base.spec"; + +methods { + function _._getUserDebtInBaseCurrency(address user, DataTypes.ReserveData storage reserve, uint256 assetPrice, uint256 assetUnit) internal => NONDET; + + function _.rayMul(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, b, 10^27) expect uint256 ALL; + function _.rayDiv(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, 10^27, b) expect uint256 ALL; +} + +ghost mapping(uint256 => mapping(uint256 => uint256)) rayMulSummariztionValues; +ghost mapping(uint256 => mapping(uint256 => uint256)) rayDivSummariztionValues; + +function rayMulSummariztion(uint256 x, uint256 y) returns uint256 { + if ((x == 0) || (y == 0)) { + return 0; + } + if (x == RAY()) { + return y; + } + if (y == RAY()) { + return x; + } + + if (y > x) { + if (y > RAY()) { + require rayMulSummariztionValues[y][x] >= x; + } + if (x > RAY()) { + require rayMulSummariztionValues[y][x] >= y; + } + return rayMulSummariztionValues[y][x]; + } + else { + if (x > RAY()) { + require rayMulSummariztionValues[x][y] >= y; + } + if (y > RAY()) { + require rayMulSummariztionValues[x][y] >= x; + } + return rayMulSummariztionValues[x][y]; + } +} + +function rayDivSummariztion(uint256 x, uint256 y) returns uint256 { + if (x == 0) { + return 0; + } + if (y == RAY()) { + return x; + } + if (y == x) { + return RAY(); + } + require y > RAY() => rayDivSummariztionValues[x][y] <= x; + require y < RAY() => x <= rayDivSummariztionValues[x][y]; + return rayDivSummariztionValues[x][y]; +} + +// Passing for PoolHarness: +// https://prover.certora.com/output/40577/e75bfa369a10490ca0cc71992984dc54/?anonymousKey=c12450d39df13d66fd92b82819c9dcc7f66d2012 +rule method_reachability(env e, method f) { + calldataarg args; + f(e, args); + satisfy true; +} + +// @title It is impossible to deposit an inactive reserve +// Proved: +// https://prover.certora.com/output/40577/b8bd6244053e42e4bddb129f04e1dd93/?anonymousKey=5374001e512e1149d120f0efa19c18a3d531d115 +// Note, that getFlags must not be NONDET. +rule cannotDepositInInactiveReserve(env e) { + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; + bool reserveIsActive = isActiveReserve(e, asset); + + deposit(e, asset, amount, onBehalfOf, referralCode); + + assert reserveIsActive; +} + +// @title It is impossible to deposit a frozen reserve +// Proved: +// https://prover.certora.com/output/40577/d4f2bfae10ae4092bb7dab309e72b166/?anonymousKey=a370279a63e87a810fd79cb20d33ef00aead7c2b +// Note, that getFlags must not be NONDET. +rule cannotDepositInFrozenReserve(env e) { + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; + bool reserveIsFrozen = isFrozenReserve(e, asset); + + deposit(e, asset, amount, onBehalfOf, referralCode); + + assert !reserveIsFrozen; +} + +// @title It is impossible to deposit zero amount +// Proved +// https://prover.certora.com/output/40577/400f77e9ca1948b9896ca35435b0ea03/?anonymousKey=760e8acd1473e9eb801aa4bcaf60d50927f9f026 +rule cannotDepositZeroAmount(env e) { + address asset; + uint256 amount; + address onBehalfOf; + uint16 referralCode; + + deposit(e, asset, amount, onBehalfOf, referralCode); + + assert amount != 0; +} + +// @title It is impossible to withdraw zero amount +// Proved +// https://prover.certora.com/output/40577/869e48220a2d40369884dd6a0cbd1734/?anonymousKey=7cf6aced7660c59314f767f4f14de508e38a37ea +rule cannotWithdrawZeroAmount(env e) { + address asset; + uint256 amount; + address to; + uint16 referralCode; + + withdraw(e, asset, amount, to); + + assert amount != 0; +} + +// @title It is impossible to withdraw an inactive reserve +// Proved +// https://prover.certora.com/output/40577/a4eb1d4472ae43c2a1bfe202f070453a/?anonymousKey=05c0ddc494d371d6a28fc40ed4cc1902bba29eba +// Note, that getFlags must not be NONDET. +rule cannotWithdrawFromInactiveReserve(env e) { + address asset; + uint256 amount; + address to; + uint16 referralCode; + bool reserveIsActive = isActiveReserve(e, asset); + + withdraw(e, asset, amount, to); + + assert reserveIsActive; +} + +// @title It is impossible to borrow zero amount +// Proved +// https://prover.certora.com/output/40577/13a0a08cbc6f448888bcdb28716d856b/?anonymousKey=48621623ac7255815e8a6465d72d38f39d55f0f4 +rule cannotBorrowZeroAmount(env e) { + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + + assert amount != 0; +} + +// @title It is impossible to borrow on inactive reserve. +// Proved +// https://prover.certora.com/output/40577/2e93cd5ce80f4aa491b9d648e1a73583/?anonymousKey=64bbd85099c3ae4a387bd0a24ce565c23094ee4f +// Note, that getFlags must not be NONDET. +rule cannotBorrowOnInactiveReserve(env e) { + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + bool reserveIsActive = isActiveReserve(e, asset); + + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + + assert reserveIsActive; +} + +// It is impossible to borrow on a reserve, that is disabled for borrowing. +// Proved +// https://prover.certora.com/output/40577/1b50faf4cbb3459c9563e4af75658525/?anonymousKey=e04b8838d1f6eceb3fb29504969ecf0817269679 +// Note, that getFlags must not be NONDET. +rule cannotBorrowOnReserveDisabledForBorrowing(env e) { + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + bool reserveIsEnabledForBorrow = isEnabledForBorrow(e, asset); + + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + + assert reserveIsEnabledForBorrow; +} + +// @title It is impossible to borrow on frozen reserve. +// Proved +// https://prover.certora.com/output/40577/b25ecb5e5b804832b3aa75e3bd54079c/?anonymousKey=8029d9f6ac5edf386f4795c4de0e7928f0487722 +// Note, that getFlags must not be NONDET. +rule cannotBorrowOnFrozenReserve(env e) { + address asset; + uint256 amount; + uint256 interestRateMode; + uint16 referralCode; + address onBehalfOf; + bool reserveIsFrozen = isFrozenReserve(e, asset); + + borrow(e, asset, amount, interestRateMode, referralCode, onBehalfOf); + + assert !reserveIsFrozen; +} diff --git a/certora/specs/ReserveConfiguration.spec b/certora/deprecated/specs/ReserveConfiguration.spec similarity index 100% rename from certora/specs/ReserveConfiguration.spec rename to certora/deprecated/specs/ReserveConfiguration.spec diff --git a/certora/deprecated/specs/UserConfiguration.spec b/certora/deprecated/specs/UserConfiguration.spec new file mode 100644 index 00000000..77404c28 --- /dev/null +++ b/certora/deprecated/specs/UserConfiguration.spec @@ -0,0 +1,103 @@ +methods { + function setBorrowing(uint256, bool) external envfree; + function setUsingAsCollateral(uint256, bool) external envfree; + function isUsingAsCollateralOrBorrowing(uint256) external returns bool envfree; + function isBorrowing(uint256) external returns bool envfree; + function isUsingAsCollateral(uint256) external returns bool envfree; + function isUsingAsCollateralOne() external returns bool envfree; + function isUsingAsCollateralAny() external returns bool envfree; + function isBorrowingOne() external returns (bool) envfree; + function isBorrowingAny() external returns bool envfree; + function isEmpty() external returns bool envfree; + function getIsolationModeState() external returns (bool, address, uint256) envfree; + function getSiloedBorrowingState() external returns (bool, address) envfree; +} + + +// checks the integrity of set Borrowing function and correct retrieval of the corresponding getter +rule setBorrowing(uint256 reserveIndex, bool borrowing) { + setBorrowing(reserveIndex, borrowing); + assert isBorrowing(reserveIndex) == borrowing, "unexpected result"; +} + +// checks that changes made to a specific borrowing asset doesnt effect the other assets +rule setBorrowingNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool borrowing) { + // reserveIndexOther info + bool otherReserveBorrowingBefore = isBorrowing(reserveIndexOther); + bool otherReserveCollateralBefore = isUsingAsCollateral(reserveIndexOther); + + setBorrowing(reserveIndex, borrowing); + + // reserveIndex info + bool ReserveBorrowingAfter = isBorrowing(reserveIndex); + // reserveIndexOther info + bool otherReserveBorrowingAfter = isBorrowing(reserveIndexOther); + bool otherReserveCollateralAfter = isUsingAsCollateral(reserveIndexOther); + + assert (reserveIndex != reserveIndexOther => + (otherReserveBorrowingAfter == otherReserveBorrowingBefore && + otherReserveCollateralAfter == otherReserveCollateralBefore)); +} + +// checks the integrity of set UsingAsCollateral function and correct retrieval of the corresponding getter +rule setUsingAsCollateral(uint256 reserveIndex, bool usingAsCollateral) { + setUsingAsCollateral(reserveIndex, usingAsCollateral); + assert isUsingAsCollateral(reserveIndex) == usingAsCollateral; +} + +// checks that changes made to a specific borrowing asset doesnt effect the other assets +rule setCollateralNoChangeToOther(uint256 reserveIndex, uint256 reserveIndexOther, bool usingAsCollateral) { + // reserveIndexOther info + bool otherReserveBorrowingBefore = isBorrowing(reserveIndexOther); + bool otherReserveCollateralBefore = isUsingAsCollateral(reserveIndexOther); + + setUsingAsCollateral(reserveIndex, usingAsCollateral); + + // reserveIndex info + bool ReserveBorrowingAfter = isBorrowing(reserveIndex); + // reserveIndexOther info + bool otherReserveBorrowingAfter = isBorrowing(reserveIndexOther); + bool otherReserveCollateralAfter = isUsingAsCollateral(reserveIndexOther); + + assert (reserveIndex != reserveIndexOther => + (otherReserveBorrowingAfter == otherReserveBorrowingBefore && + otherReserveCollateralAfter == otherReserveCollateralBefore)); +} + +invariant isUsingAsCollateralOrBorrowing(uint256 reserveIndex ) + (isUsingAsCollateral(reserveIndex) || isBorrowing(reserveIndex)) <=> + isUsingAsCollateralOrBorrowing(reserveIndex); + +invariant integrityOfisUsingAsCollateralOne(uint256 reserveIndex, uint256 reserveIndexOther) + isUsingAsCollateral(reserveIndex) && isUsingAsCollateralOne() => + !isUsingAsCollateral(reserveIndexOther) || reserveIndexOther == reserveIndex; + +invariant integrityOfisUsingAsCollateralAny(uint256 reserveIndex) + isUsingAsCollateral(reserveIndex) => isUsingAsCollateralAny(); + +invariant integrityOfisBorrowingOne(uint256 reserveIndex, uint256 reserveIndexOther) + isBorrowing(reserveIndex) && isBorrowingOne() => !isBorrowing(reserveIndexOther) || reserveIndexOther == reserveIndex; + +invariant integrityOfisBorrowingAny(uint256 reserveIndex) + isBorrowing(reserveIndex) => isBorrowingAny(); + +invariant integrityOfEmpty(uint256 reserveIndex) + isEmpty() => !isBorrowingAny() && !isUsingAsCollateralOrBorrowing(reserveIndex); + +// if IsolationModeState is active then there must be exactly one asset register as collateral. +// note that this is a necessary requirement, but it is not sufficient. +rule integrityOfIsolationModeState() { + bool existExactlyOneCollateral = isUsingAsCollateralOne(); + bool answer; address asset; uint256 ceiling; + answer, asset, ceiling = getIsolationModeState(); + assert answer => existExactlyOneCollateral; +} + +// if IsolationModeState is active then there must be exactly one asset register as collateral. +// note that this is a necessary requirement, but it is not sufficient. +rule integrityOfSiloedBorrowingState() { + bool existExactlyOneBorrow = isBorrowingOne(); + bool answer; address asset; + answer, asset = getSiloedBorrowingState(); + assert answer => existExactlyOneBorrow; +} diff --git a/certora/deprecated/specs/VariableDebtToken.spec b/certora/deprecated/specs/VariableDebtToken.spec new file mode 100644 index 00000000..4f1c97b0 --- /dev/null +++ b/certora/deprecated/specs/VariableDebtToken.spec @@ -0,0 +1,257 @@ +methods { + // summarization for elimination the raymul operation in balance of and totalSupply. + function _.getReserveNormalizedVariableDebt(address asset) external => gRNVB() expect uint256 ALL; + function _.handleAction(address, uint256, uint256) external => NONDET; + function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; +} + +function PLUS256(uint256 x, uint256 y) returns uint256 { + return (assert_uint256( (x+y) % 2^256) ); +} + +definition ray() returns uint = 1000000000000000000000000000; +definition bound() returns mathint = ((gRNVB() / ray()) + 1 ) / 2; + +// summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul) +ghost gRNVB() returns uint256 { + axiom to_mathint(gRNVB()) == 7 * ray(); +} + +/* + Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2. +*/ +definition bounded_error_eq(mathint x, mathint y, mathint scale) returns bool = + x <= y + (bound() * scale) && x + (bound() * scale) >= y; + +definition disAllowedFunctions(method f) returns bool = + f.selector == sig:transfer(address, uint256).selector || + f.selector == sig:allowance(address, address).selector || + f.selector == sig:approve(address, uint256).selector || + f.selector == sig:transferFrom(address, address, uint256).selector || + f.selector == sig:increaseAllowance(address, uint256).selector || + f.selector == sig:decreaseAllowance(address, uint256).selector; + +ghost sumAllBalance() returns mathint { + init_state axiom sumAllBalance() == 0; +} +hook Sstore _userState[KEY address a].balance uint128 balance (uint128 old_balance) { + havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance; +} + +invariant totalSupplyEqualsSumAllBalance(env e) + totalSupply(e) == scaledBalanceOfToBalanceOf(require_uint256(sumAllBalance())) + filtered { f -> !f.isView && !disAllowedFunctions(f) } + { + preserved mint(address user, address onBehalfOf, uint256 amount, uint256 index) with (env e2) { + require index == gRNVB(); + } + preserved burn(address from, uint256 amount, uint256 index) with (env e3) { + require index == gRNVB(); + } + } + +// Only the pool with burn or mint operation can change the total supply. (assuming the getReserveNormalizedVariableDebt is not changed) +rule whoChangeTotalSupply(method f) + filtered { f -> !f.isView && !disAllowedFunctions(f) } +{ + env e; + uint256 oldTotalSupply = totalSupply(e); + calldataarg args; + f(e, args); + uint256 newTotalSupply = totalSupply(e); + assert oldTotalSupply != newTotalSupply => + (e.msg.sender == POOL(e) && + (f.selector == sig:burn(address, uint256, uint256).selector || + f.selector == sig:mint(address, address, uint256, uint256).selector)); +} + +/* + Each operation of Variable Debt Token can change at most one user's balance. +*/ +rule balanceOfChange(address a, address b, method f) + filtered { f -> !f.isView && !disAllowedFunctions(f) } +{ + env e; + require a != b; + uint256 balanceABefore = balanceOf(a); + uint256 balanceBBefore = balanceOf(b); + + calldataarg arg; + f(e, arg); + + uint256 balanceAAfter = balanceOf(a); + uint256 balanceBAfter = balanceOf(b); + + assert (balanceABefore == balanceAAfter || balanceBBefore == balanceBAfter); +} + +// only delegationWithSig operation can change the nonce. +rule nonceChangePermits(method f) + filtered { f -> !f.isView && !disAllowedFunctions(f) } +{ + env e; + address user; + uint256 oldNonce = nonces(e, user); + calldataarg args; + f(e, args); + uint256 newNonce = nonces(e, user); + assert oldNonce != newNonce => f.selector == sig:delegationWithSig(address, address, uint256, uint256, uint8, bytes32, bytes32).selector; +} + +// minting and then buring Variable Debt Token should have no effect on the users balance +rule inverseMintBurn(address a, address delegatedUser, uint256 amount, uint256 index) { + env e; + uint256 balancebefore = balanceOf(a); + mint(e, delegatedUser, a, amount, index); + burn(e, a, amount, index); + uint256 balanceAfter = balanceOf(a); + assert balancebefore == balanceAfter, "burn is not the inverse of mint"; +} + +rule integrityDelegationWithSig(address delegator, address delegatee, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { + env e; + uint256 oldNonce = nonces(e, delegator); + delegationWithSig(e, delegator, delegatee, value, deadline, v, r, s); + assert to_mathint(nonces(e, delegator)) == oldNonce + 1 + && + borrowAllowance(e, delegator, delegatee) == value; +} + +/** + Burning user u amount of amount tokens, decreases his balanceOf the user by amount. + (balance is decreased by amount and not scaled amount because of the summarization to one ray) +*/ +rule integrityOfBurn(address u, uint256 amount) { + env e; + uint256 index = gRNVB(); + uint256 balanceBeforeUser = balanceOf(u); + uint256 totalSupplyBefore = totalSupply(e); + + burn(e, u, amount, index); + + uint256 balanceAfterUser = balanceOf(u); + uint256 totalSupplyAfter = totalSupply(e); + + assert bounded_error_eq(totalSupplyAfter, totalSupplyBefore - amount, 1), "total supply integrity"; // total supply reduced + assert bounded_error_eq(balanceAfterUser, balanceBeforeUser - amount, 1), "integrity break"; // user burns ATokens to recieve underlying +} + +/* + Burn is additive, can performed either all at once or gradually + burn(from,to,x,index); burn(from,to,y,index) ~ burn(from,to,x+y,index) at the same initial state +*/ +rule additiveBurn(address user1, address user2, uint256 x, uint256 y) { + env e; + uint256 index = gRNVB(); + require (user1 != user2 && balanceOf(user1) == balanceOf(user2)); + require user1 != currentContract && user2 != currentContract; + + burn(e, user1, x, index); + burn(e, user1, y, index); + uint256 balanceScenario1 = balanceOf(user1); + + burn(e, user2, PLUS256(x,y), index); + uint256 balanceScenario2 = balanceOf(user2); + + assert bounded_error_eq(balanceScenario1, balanceScenario2, 3), "burn is not additive"; +} + +/* + Mint is additive, can performed either all at once or gradually + mint(from,to,x,index); mint(from,to,y,index) ~ mint(from,to,x+y,index) at the same initial state +*/ +rule additiveMint(address user1, address user2, address user3, uint256 x, uint256 y) { + env e; + uint256 index = gRNVB(); + require (user1 != user2 && balanceOf(user1) == balanceOf(user2)); + + mint(e, user3, user1, x, index); + mint(e, user3, user1, y, index); + uint256 balanceScenario1 = balanceOf(user1); + + mint(e, user3, user2, PLUS256(x,y), index); + uint256 balanceScenario2 = balanceOf(user2); + + assert bounded_error_eq(balanceScenario1, balanceScenario2, 3), "burn is not additive"; +} + +/** + Mint to user u amount of x tokens, increases his balanceOf the user by x. + (balance is increased by x and not scaled x because of the summarization to one ray) +*/ +rule integrityMint(address a, uint256 x) { + env e; + address delegatedUser; + uint256 index = gRNVB(); + uint256 underlyingBalanceBefore = balanceOf(a); + uint256 atokenBlanceBefore = scaledBalanceOf(e, a); + uint256 totalATokenSupplyBefore = scaledTotalSupply(e); + mint(e, delegatedUser, a, x, index); + + uint256 underlyingBalanceAfter = balanceOf(a); + uint256 atokenBlanceAfter = scaledBalanceOf(e, a); + uint256 totalATokenSupplyAfter = scaledTotalSupply(e); + + assert atokenBlanceAfter - atokenBlanceBefore == totalATokenSupplyAfter - totalATokenSupplyBefore; + assert totalATokenSupplyAfter > totalATokenSupplyBefore; + assert bounded_error_eq(underlyingBalanceAfter, underlyingBalanceBefore+x, 1); +} + +// Buring zero amount of tokens should have no effect. +rule burnZeroDoesntChangeBalance(address u, uint256 index) { + env e; + uint256 balanceBefore = balanceOf(u); + burn@withrevert(e, u, 0, index); + uint256 balanceAfter = balanceOf(u); + assert balanceBefore == balanceAfter; +} + +/* + Burning one user atokens should have no effect on other users that are not involved in the action. +*/ +rule burnNoChangeToOther(address user, uint256 amount, uint256 index, address other) { + require other != user; + + env e; + uint256 otherBalanceBefore = balanceOf(other); + + burn(e, user, amount, index); + + uint256 otherBalanceAfter = balanceOf(other); + + assert otherBalanceBefore == otherBalanceAfter; +} + +/* + Minting ATokens for a user should have no effect on other users that are not involved in the action. +*/ +rule mintNoChangeToOther(address user, address onBehalfOf, uint256 amount, uint256 index, address other) { + require other != user && other != onBehalfOf; + + env e; + uint256 userBalanceBefore = balanceOf(user); + uint256 otherBalanceBefore = balanceOf(other); + + mint(e, user, onBehalfOf, amount, index); + + uint256 userBalanceAfter = balanceOf(user); + uint256 otherBalanceAfter = balanceOf(other); + + if (user != onBehalfOf) { + assert userBalanceBefore == userBalanceAfter ; + } + + assert otherBalanceBefore == otherBalanceAfter ; +} + +/* + Ensuring that the defined disallowed functions revert in any case. +*/ +rule disallowedFunctionalities(method f) + filtered { f -> disAllowedFunctions(f) } +{ + env e; calldataarg args; + f@withrevert(e, args); + assert lastReverted; +} diff --git a/certora/stata/applyHarness.patch b/certora/stata/applyHarness.patch index 98c12412..9756bc6b 100644 --- a/certora/stata/applyHarness.patch +++ b/certora/stata/applyHarness.patch @@ -6,8 +6,8 @@ diff -ruN .gitignore .gitignore +!.gitignore \ No newline at end of file diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstance.sol ---- src/core/instances/ATokenInstance.sol 2024-09-05 19:01:54 -+++ src/core/instances/ATokenInstance.sol 2024-09-05 11:33:23 +--- src/contracts/instances/ATokenInstance.sol 2024-09-05 19:01:54 ++++ src/contracts/instances/ATokenInstance.sol 2024-09-05 11:33:23 @@ -35,15 +35,15 @@ _domainSeparator = _calculateDomainSeparator(); @@ -35,8 +35,8 @@ diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstanc } } diff -ruN src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol ---- src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 19:01:54 -+++ src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 13:48:31 +--- src/contracts/extensions/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 19:01:54 ++++ src/contracts/extensions/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 13:48:31 @@ -147,7 +147,7 @@ } diff --git a/certora/stata/conf/verifyAToken.conf b/certora/stata/conf/verifyAToken.conf index 154a46f7..4f920500 100644 --- a/certora/stata/conf/verifyAToken.conf +++ b/certora/stata/conf/verifyAToken.conf @@ -6,7 +6,7 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", ], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", + // "aave-v3-core/=certora/stata/munged/src/core", + // "aave-v3-periphery/=certora/stata/munged/src/periphery", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/conf/verifyDoubleClaim.conf b/certora/stata/conf/verifyDoubleClaim.conf index 52cc582d..7c71fa79 100644 --- a/certora/stata/conf/verifyDoubleClaim.conf +++ b/certora/stata/conf/verifyDoubleClaim.conf @@ -6,7 +6,7 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", ], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", +// "aave-v3-core/=certora/stata/munged/src/core", + // "aave-v3-periphery/=certora/stata/munged/src/periphery", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/conf/verifyERC4626.conf b/certora/stata/conf/verifyERC4626.conf index 06900f28..74e08a5a 100644 --- a/certora/stata/conf/verifyERC4626.conf +++ b/certora/stata/conf/verifyERC4626.conf @@ -6,8 +6,8 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", - ], + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", +], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", +// "aave-v3-core/=certora/stata/munged/src/contracts", +// "aave-v3-periphery/=certora/stata/munged/src/contracts/extensions", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/conf/verifyERC4626DepositSummarization.conf b/certora/stata/conf/verifyERC4626DepositSummarization.conf index d2ce588f..cc18484d 100644 --- a/certora/stata/conf/verifyERC4626DepositSummarization.conf +++ b/certora/stata/conf/verifyERC4626DepositSummarization.conf @@ -6,7 +6,7 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", ], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", +// "aave-v3-core/=certora/stata/munged/src/core", +// "aave-v3-periphery/=certora/stata/munged/src/periphery", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/conf/verifyERC4626Extended.conf b/certora/stata/conf/verifyERC4626Extended.conf index fedbbffe..b9e5e77c 100644 --- a/certora/stata/conf/verifyERC4626Extended.conf +++ b/certora/stata/conf/verifyERC4626Extended.conf @@ -6,7 +6,7 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", ], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", +// "aave-v3-core/=certora/stata/munged/src/core", + // "aave-v3-periphery/=certora/stata/munged/src/periphery", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/conf/verifyERC4626MintDepositSummarization.conf b/certora/stata/conf/verifyERC4626MintDepositSummarization.conf index d0c76fba..b968b7ea 100644 --- a/certora/stata/conf/verifyERC4626MintDepositSummarization.conf +++ b/certora/stata/conf/verifyERC4626MintDepositSummarization.conf @@ -6,7 +6,7 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", ], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", + //"aave-v3-core/=certora/stata/munged/src/core", + //"aave-v3-periphery/=certora/stata/munged/src/periphery", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/conf/verifyStataToken.conf b/certora/stata/conf/verifyStataToken.conf index a1406810..fa701c86 100644 --- a/certora/stata/conf/verifyStataToken.conf +++ b/certora/stata/conf/verifyStataToken.conf @@ -6,7 +6,7 @@ "certora/stata/harness/rewards/TransferStrategyHarness.sol", "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", - "certora/stata/munged/src/core/instances/ATokenInstance.sol", + "certora/stata/munged/src/contracts/instances/ATokenInstance.sol", ], "link": [ "SymbolicLendingPool:aToken=ATokenInstance", @@ -21,8 +21,8 @@ "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ - "aave-v3-core/=certora/stata/munged/src/core", - "aave-v3-periphery/=certora/stata/munged/src/periphery", +// "aave-v3-core/=certora/stata/munged/src/core", + // "aave-v3-periphery/=certora/stata/munged/src/periphery", "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", "forge-std/=certora/stata/munged/lib/forge-std/src", "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", diff --git a/certora/stata/harness/StataTokenV2Harness.sol b/certora/stata/harness/StataTokenV2Harness.sol index 08e81398..8b61aec7 100644 --- a/certora/stata/harness/StataTokenV2Harness.sol +++ b/certora/stata/harness/StataTokenV2Harness.sol @@ -2,7 +2,7 @@ pragma solidity ^0.8.10; import {IERC20} from 'openzeppelin-contracts/contracts/interfaces/IERC20.sol'; -import {StataTokenV2, IPool, IRewardsController} from 'aave-v3-periphery/contracts/static-a-token/StataTokenV2.sol'; +import {StataTokenV2, IPool, IRewardsController} from '../munged/src/contracts/extensions/static-a-token/StataTokenV2.sol'; import {SymbolicLendingPool} from './pool/SymbolicLendingPool.sol'; contract StataTokenV2Harness is StataTokenV2 { diff --git a/certora/stata/harness/pool/SymbolicLendingPool.sol b/certora/stata/harness/pool/SymbolicLendingPool.sol index af9c6c19..e9df7cc6 100644 --- a/certora/stata/harness/pool/SymbolicLendingPool.sol +++ b/certora/stata/harness/pool/SymbolicLendingPool.sol @@ -1,9 +1,9 @@ pragma solidity ^0.8.10; pragma experimental ABIEncoderV2; -import {IERC20} from 'aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; -import {IAToken} from 'aave-v3-core/contracts/interfaces/IAToken.sol'; -import {DataTypes} from 'aave-v3-core/contracts/protocol/libraries/types/DataTypes.sol'; +import {IERC20} from '../../munged/src/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {IAToken} from '../../munged/src/contracts/interfaces/IAToken.sol'; +import {DataTypes} from '../../munged/src/contracts/protocol/libraries/types/DataTypes.sol'; contract SymbolicLendingPool { // an underlying asset in the pool @@ -63,24 +63,24 @@ contract SymbolicLendingPool { ) external view returns (DataTypes.ReserveDataLegacy memory) { DataTypes.ReserveDataLegacy memory res; - res.configuration = reserve.configuration; - res.liquidityIndex = reserve.liquidityIndex; - res.currentLiquidityRate = reserve.currentLiquidityRate; - res.variableBorrowIndex = reserve.variableBorrowIndex; - res.currentVariableBorrowRate = reserve.currentVariableBorrowRate; - res.currentStableBorrowRate = reserve.currentStableBorrowRate; - res.lastUpdateTimestamp = reserve.lastUpdateTimestamp; - res.id = reserve.id; - res.aTokenAddress = reserve.aTokenAddress; - res.stableDebtTokenAddress = reserve.stableDebtTokenAddress; - res.variableDebtTokenAddress = reserve.variableDebtTokenAddress; - res.interestRateStrategyAddress = reserve.interestRateStrategyAddress; - res.accruedToTreasury = reserve.accruedToTreasury; - res.unbacked = reserve.unbacked; - res.isolationModeTotalDebt = reserve.isolationModeTotalDebt; + res.configuration = reserveLegacy.configuration; + res.liquidityIndex = reserveLegacy.liquidityIndex; + res.currentLiquidityRate = reserveLegacy.currentLiquidityRate; + res.variableBorrowIndex = reserveLegacy.variableBorrowIndex; + res.currentVariableBorrowRate = reserveLegacy.currentVariableBorrowRate; + res.currentStableBorrowRate = reserveLegacy.currentStableBorrowRate; + res.lastUpdateTimestamp = reserveLegacy.lastUpdateTimestamp; + res.id = reserveLegacy.id; + res.aTokenAddress = reserveLegacy.aTokenAddress; + res.stableDebtTokenAddress = reserveLegacy.stableDebtTokenAddress; + res.variableDebtTokenAddress = reserveLegacy.variableDebtTokenAddress; + res.interestRateStrategyAddress = reserveLegacy.interestRateStrategyAddress; + res.accruedToTreasury = reserveLegacy.accruedToTreasury; + res.unbacked = reserveLegacy.unbacked; + res.isolationModeTotalDebt = reserveLegacy.isolationModeTotalDebt; return res; } - + function getReserveDataExtended( address asset ) external view returns (DataTypes.ReserveData memory) { diff --git a/certora/stata/harness/rewards/RewardsControllerHarness.sol b/certora/stata/harness/rewards/RewardsControllerHarness.sol index 737a976c..36af81cf 100644 --- a/certora/stata/harness/rewards/RewardsControllerHarness.sol +++ b/certora/stata/harness/rewards/RewardsControllerHarness.sol @@ -1,6 +1,6 @@ pragma solidity ^0.8.10; -import {RewardsController, RewardsDataTypes} from 'aave-v3-periphery/contracts/rewards/RewardsController.sol'; +import {RewardsController, RewardsDataTypes} from '../../munged/src/contracts/rewards/RewardsController.sol'; contract RewardsControllerHarness is RewardsController { constructor(address emissionManager) RewardsController(emissionManager) {} diff --git a/certora/stata/harness/rewards/TransferStrategyHarness.sol b/certora/stata/harness/rewards/TransferStrategyHarness.sol index 9f861a90..50fda90f 100644 --- a/certora/stata/harness/rewards/TransferStrategyHarness.sol +++ b/certora/stata/harness/rewards/TransferStrategyHarness.sol @@ -1,7 +1,7 @@ pragma solidity ^0.8.10; -import {IERC20} from 'aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; -import {TransferStrategyBase} from 'aave-v3-periphery/contracts/rewards/transfer-strategies/TransferStrategyBase.sol'; +import {IERC20} from '../../munged/src/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {TransferStrategyBase} from 'src/contracts/rewards/transfer-strategies/TransferStrategyBase.sol'; contract TransferStrategyHarness is TransferStrategyBase { constructor( diff --git a/certora/stata/scripts/run-all.sh b/certora/stata/scripts/run-all.sh index d970a7d2..143df093 100644 --- a/certora/stata/scripts/run-all.sh +++ b/certora/stata/scripts/run-all.sh @@ -2,11 +2,10 @@ echo "******** Running: 1 ***************" certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance previewMintIndependentOfAllowance \ - maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert \ --msg "1: verifyERC4626.conf" echo "******** Running: 1.5 ***************" -certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw \ +certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert \ --msg "1.5: verifyERC4626.conf" echo "******** Running: 2 ***************" @@ -18,8 +17,7 @@ certoraRun $CMN certora/stata/conf/verifyERC4626DepositSummarization.conf --rule --msg "3: " echo "******** Running: 4 ***************" -certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint \ - maxDepositConstant \ +certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant \ --msg "4: " echo "******** Running: 5 ***************"